# Attributes¶

Attributes can be used to give Imandra verification hints, and to instruct Imandra how it should use a proved theorem in subsequent verification efforts, via the installation of a theorem as a "rule".

## Verification Hints¶

• [@@auto]: apply Imandra's inductive waterfall proof strategy, which combines simplification (including automatic subgoaling, conditional rewriting and forward-chaining using previously proved lemmas, decision procedures for datatypes and arithmetic, etc.), and may decide to do induction. This is the most common way to prove a theorem in Imandra.

• [@@induct <flag?>]: apply Imandra's inductive waterfall proof strategy, but control the top-level induction. The <flag?> can be one of:

• functional <func_name> - perform functional induction using an induction scheme derived from <func_name>
• structural <args?> - perform structural induction on the arguments <args?> if given, else on a heuristically chosen collection of variables. The types of the induction variables must be algebraic datatypes / variant types. An additive approach (linear in the total number of constructors) is taken for combining the schemes of individual variables into a composite induction scheme.
• structural_mult <args?> - like structural, except uses a "multiplicative" scheme, rather than an additive one
• structural_add <args?> - a synonym for structural
• [@@simp] or [@@simplify]: apply simplification to the goal before unrolling.

• [@@disable <f_1>,...,<f_k>]: If f_i is a rule, instructs Imandra to ignore f_i during the proof attempt. If f_i is a function, instructs Imandra to leave the function definition unexpanded during the proof attempt. This is especially useful in the presence of rewrite rules about non-recursive functions, as such rules will typically not apply unless the relevant non-recursive function is disabled. Imandra might choose to ignore this hint if ignoring it leads to immediate closure of the goal, or to the construction of a valid counterexample. Note that rules and functions can be globally disabled, using the #disable directive.

• [@@enable <f_1>,...,<f_k>]: The dual of @@disable. Note that rules and functions can be globally enabled, using the #enable directive.

• [@@apply <thm <arg_1> ... <arg_k>>]: instantiate thm with the given arguments and add its instantiation to the hypotheses of the goal. This is especially useful when thm is not naturally useable as a @@rewrite or @@forward-chaining rule, but is nevertheless needed (in an instantiated form) to prove a given theorem.

• [@@blast]: apply Imandra's blast procedure, which combines symbolic execution and SAT-based bit-blasting. This is useful for difficult combinatorial problems, and problems involving nontrivial (i.e., nonlinear) arithmetic over bounded discrete domains.

## Rule Classes¶

Theorems may be installed as rules, which instructs Imandra to apply them in certain ways during subsequent proof attempts. The development of an appropriate collection of rules can be used to "teach" Imandra how to reason in a new domain.

• [@@rw] or [@@rewrite]: install theorem as a rewrite rule
• [@@permutative]: restrict rewrite rule as permutative
• [@@fc] or [@@forward-chaining]: install theorem as a forward chaining rule
• [@@elim] or [@@elimination]: install theorem as an elimination rule
• [@@gen] or [@@generalization]: install theorem as a generalization rule

## Examples¶

In :
verify (fun x y -> List.length (x@y) = List.length x + List.length y) [@@auto]

Out:
- : 'a list -> 'a list -> bool = <fun>
Goal:

List.length (x @ y) = List.length x + List.length y.

1 nontautological subgoal.

Subgoal 1:

|---------------------------------------------------------------------------
List.length (List.append x y) = List.length x + List.length y

Must try induction.

The recursive terms in the conjecture suggest 3 inductions.
Subsumption and merging reduces this to 2.

Only 1 of those schemes are unflawed.
We shall induct according to a scheme derived from List.append.

Induction scheme:

(not (x <> []) ==> φ x y) && (x <> [] && φ (List.tl x) y ==> φ x y).

2 nontautological subgoals.

Subgoal 1.2:

|---------------------------------------------------------------------------
C0. x <> []
C1. List.length (List.append x y) = List.length x + List.length y

But simplification reduces this to true, using the definitions of List.append
and List.length.

Subgoal 1.1:

H0. x <> []
H1. List.length (List.append (List.tl x) y)
= List.length (List.tl x) + List.length y
|---------------------------------------------------------------------------
List.length (List.append x y) = List.length x + List.length y

But simplification reduces this to true, using the definitions of List.append
and List.length.

ⓘ  Rules:
(:def List.append)
(:def List.length)
(:fc List.len_nonnegative)
(:induct List.append)


Proved
proof
 ground_instances: 0 definitions: 5 inductions: 1 search_time: 0.080s
Expand
• start[0.080s, "Goal"]
List.length (List.append ( :var_0: ) ( :var_1: ))
= List.length ( :var_0: ) + List.length ( :var_1: )
• #### subproof

List.length (List.append x y) = List.length x + List.length y
• start[0.080s, "1"]
List.length (List.append x y) = List.length x + List.length y
• induction on (functional ?)
:scheme (not (x <> []) ==> φ x y)
&& (x <> [] && φ (List.tl x) y ==> φ x y)
• Split (let (_x_0 : bool) = x <> [] in
let (_x_1 : int) = List.length y in
let (_x_2 : bool)
= List.length (List.append x y) = List.length x + _x_1
in
let (_x_3 : sko_ty_0 list) = List.tl x in
(_x_0 || _x_2)
&& (not
(_x_0
&& (List.length (List.append _x_3 y) = List.length _x_3 + _x_1))
|| _x_2)
:cases [x <> []
|| (List.length (List.append x y)
= List.length x + List.length y);
let (_x_0 : sko_ty_0 list) = List.tl x in
let (_x_1 : int) = List.length y in
not (x <> [])
|| not
(List.length (List.append _x_0 y) = List.length _x_0 + _x_1)
|| (List.length (List.append x y) = List.length x + _x_1)])
• ##### subproof
let (_x_0 : sko_ty_0 list) = List.tl x in let (_x_1 : int) = List.length y in not (x <> []) || not (List.length (List.append _x_0 y) = List.length _x_0 + _x_1) || (List.length (List.append x y) = List.length x + _x_1)
• start[0.040s, "1.1"]
let (_x_0 : sko_ty_0 list) = List.tl x in
let (_x_1 : int) = List.length y in
not (x <> [])
|| not (List.length (List.append _x_0 y) = List.length _x_0 + _x_1)
|| (List.length (List.append x y) = List.length x + _x_1)
• ###### simplify
 into: true expansions: [List.length, List.length, List.append] rewrite_steps: forward_chaining: List.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegative
• ##### subproof
x <> [] || (List.length (List.append x y) = List.length x + List.length y)
• start[0.040s, "1.2"]
x <> [] || (List.length (List.append x y) = List.length x + List.length y)
• ###### simplify
 into: true expansions: [List.length, List.append] rewrite_steps: forward_chaining: List.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegative
In :
verify (fun x -> x @ [] @ x = x @ x) [@@simp]

Out:
- : 'a list -> bool = <fun>

Proved
proof
ground_instances:0
definitions:1
inductions:0
search_time:
0.030s
details:
Expand
smt_stats:
 rlimit count: 430 num allocs: 5.42233e+07 time: 0.009 memory: 15.52 max memory: 15.99
Expand
• start[0.030s]
List.append ( :var_0: ) (List.append [] ( :var_0: ))
= List.append ( :var_0: ) ( :var_0: )
• #### simplify

 into: true expansions: List.append rewrite_steps: forward_chaining:
• Unsat
In :
lemma len_append x y = List.length (x@y) = List.length x + List.length y [@@auto] [@@rw]

Out:
val len_append : 'a list -> 'a list -> bool = <fun>
Goal:

List.length (x @ y) = List.length x + List.length y.

1 nontautological subgoal.

Subgoal 1:

|---------------------------------------------------------------------------
List.length (List.append x y) = List.length x + List.length y

Must try induction.

The recursive terms in the conjecture suggest 3 inductions.
Subsumption and merging reduces this to 2.

Only 1 of those schemes are unflawed.
We shall induct according to a scheme derived from List.append.

Induction scheme:

(not (x <> []) ==> φ x y) && (x <> [] && φ (List.tl x) y ==> φ x y).

2 nontautological subgoals.

Subgoal 1.2:

|---------------------------------------------------------------------------
C0. x <> []
C1. List.length (List.append x y) = List.length x + List.length y

But simplification reduces this to true, using the definitions of List.append
and List.length.

Subgoal 1.1:

H0. x <> []
H1. List.length (List.append (List.tl x) y)
= List.length (List.tl x) + List.length y
|---------------------------------------------------------------------------
List.length (List.append x y) = List.length x + List.length y

But simplification reduces this to true, using the definitions of List.append
and List.length.

ⓘ  Rules:
(:def List.append)
(:def List.length)
(:fc List.len_nonnegative)
(:induct List.append)


Proved
proof
 ground_instances: 0 definitions: 5 inductions: 1 search_time: 0.087s
Expand
• start[0.087s, "Goal"]
List.length (List.append ( :var_0: ) ( :var_1: ))
= List.length ( :var_0: ) + List.length ( :var_1: )
• #### subproof

List.length (List.append x y) = List.length x + List.length y
• start[0.087s, "1"]
List.length (List.append x y) = List.length x + List.length y
• induction on (functional ?)
:scheme (not (x <> []) ==> φ x y)
&& (x <> [] && φ (List.tl x) y ==> φ x y)
• Split (let (_x_0 : bool) = x <> [] in
let (_x_1 : int) = List.length y in
let (_x_2 : bool)
= List.length (List.append x y) = List.length x + _x_1
in
let (_x_3 : sko_ty_0 list) = List.tl x in
(_x_0 || _x_2)
&& (not
(_x_0
&& (List.length (List.append _x_3 y) = List.length _x_3 + _x_1))
|| _x_2)
:cases [x <> []
|| (List.length (List.append x y)
= List.length x + List.length y);
let (_x_0 : sko_ty_0 list) = List.tl x in
let (_x_1 : int) = List.length y in
not (x <> [])
|| not
(List.length (List.append _x_0 y) = List.length _x_0 + _x_1)
|| (List.length (List.append x y) = List.length x + _x_1)])
• ##### subproof
let (_x_0 : sko_ty_0 list) = List.tl x in let (_x_1 : int) = List.length y in not (x <> []) || not (List.length (List.append _x_0 y) = List.length _x_0 + _x_1) || (List.length (List.append x y) = List.length x + _x_1)
• start[0.044s, "1.1"]
let (_x_0 : sko_ty_0 list) = List.tl x in
let (_x_1 : int) = List.length y in
not (x <> [])
|| not (List.length (List.append _x_0 y) = List.length _x_0 + _x_1)
|| (List.length (List.append x y) = List.length x + _x_1)
• ###### simplify
 into: true expansions: [List.length, List.length, List.append] rewrite_steps: forward_chaining: List.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegative
• ##### subproof
x <> [] || (List.length (List.append x y) = List.length x + List.length y)
• start[0.044s, "1.2"]
x <> [] || (List.length (List.append x y) = List.length x + List.length y)
• ###### simplify
 into: true expansions: [List.length, List.append] rewrite_steps: forward_chaining: List.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegative
In :
theorem len_non_neg x = (List.length x) [@trigger] >= 0 [@@simp] [@@fc]

Out:
val len_non_neg : 'a list -> bool = <fun>

Proved
proof
ground_instances:0
definitions:0
inductions:0
search_time:
0.043s
details:
Expand
smt_stats:
 rlimit count: 514 num allocs: 1.7313e+08 time: 0.011 memory: 16.09 max memory: 16.58
Expand
• start[0.043s] List.length ( :var_0: ) >= 0
• #### simplify

 into: true expansions: [] rewrite_steps: forward_chaining: List.len_nonnegative
• Unsat
In :
lemma foo = (fun x -> x @ [] = x) [@@induct x] [@@disable List.append_to_nil]

Out:
val foo : 'a list -> bool = <fun>
Goal:

x @ [] = x.

1 nontautological subgoal.

Induction scheme:

φ [] && (x <> [] && φ (List.tl x) ==> φ x).

2 nontautological subgoals.

Subgoal 2:

|---------------------------------------------------------------------------
List.append [] [] = []

But simplification reduces this to true, using the definition of List.append.

Subgoal 1:

H0. x <> []
H1. List.append (List.tl x) [] = List.tl x
|---------------------------------------------------------------------------
List.append x [] = x

But simplification reduces this to true, using the definition of List.append.

ⓘ  Rules:
(:def List.append)
(:induct struct list)


Proved
proof
 ground_instances: 0 definitions: 2 inductions: 1 search_time: 0.014s
Expand
• start[0.014s, "Goal"] List.append ( :var_0: ) [] = ( :var_0: )
• #### subproof

List.append x [] = x
• start[0.014s, "1"] List.append x [] = x
• induction on (structural+ x)
:scheme φ [] && (x <> [] && φ (List.tl x) ==> φ x)
• Split (let (_x_0 : sko_ty_0 list) = List.tl x in
(List.append [] [] = [])
&& (not (x <> [] && (List.append _x_0 [] = _x_0))
|| (List.append x [] = x))
:cases [List.append [] [] = [];
let (_x_0 : sko_ty_0 list) = List.tl x in
not (x <> []) || not (List.append _x_0 [] = _x_0)
|| (List.append x [] = x)])
• ##### subproof
let (_x_0 : sko_ty_0 list) = List.tl x in not (x <> []) || not (List.append _x_0 [] = _x_0) || (List.append x [] = x)
• start[0.013s, "1"]
let (_x_0 : sko_ty_0 list) = List.tl x in
not (x <> []) || not (List.append _x_0 [] = _x_0) || (List.append x [] = x)
• ###### simplify
 into: true expansions: List.append rewrite_steps: forward_chaining:
• ##### subproof
List.append [] [] = []
• start[0.013s, "2"] List.append [] [] = []
• ###### simplify
 into: true expansions: List.append rewrite_steps: forward_chaining: