# 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:

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

2 nontautological subgoals.

Subgoal 1.2:

H0. x = []
|---------------------------------------------------------------------------
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. not (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.083s
Expand
• start[0.083s, "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.083s, "1"]
List.length (List.append x y) = List.length x + List.length y
• induction on (functional )
:scheme (x = [] ==> φ y x) && (not (x = []) && φ y (List.tl x) ==> φ y x)
• Split ((not (x = [])
|| List.length (List.append x y) = List.length x + List.length y)
&& (not
(not (x = [])
&& 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)
:cases [not (x = [])
|| List.length (List.append x y) =
List.length x + List.length y;
(x = []
|| not
(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])
• ##### subproof
(x = [] || not (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
• start[0.031s, "1.1"]
(x = []
|| not
(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
• ###### 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
not (x = []) || List.length (List.append x y) = List.length x + List.length y
• start[0.031s, "1.2"]
not (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_nonnegative
In :
verify (fun x -> x @ [] @ x = x @ x) [@@simp]

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

Proved
proof
ground_instances0
definitions1
inductions0
search_time
0.060s
details
Expand
smt_stats
 rlimit count 225 mk bool var 5 num allocs 3.25772e+07 memory 8.86 max memory 12.06
Expand
• start[0.060s]
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

(mp (asserted (not true)) (rewrite (= (not true) false)) false)
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:

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

2 nontautological subgoals.

Subgoal 1.2:

H0. x = []
|---------------------------------------------------------------------------
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. not (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.076s
Expand
• start[0.076s, "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.076s, "1"]
List.length (List.append x y) = List.length x + List.length y
• induction on (functional )
:scheme (x = [] ==> φ y x) && (not (x = []) && φ y (List.tl x) ==> φ y x)
• Split ((not (x = [])
|| List.length (List.append x y) = List.length x + List.length y)
&& (not
(not (x = [])
&& 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)
:cases [not (x = [])
|| List.length (List.append x y) =
List.length x + List.length y;
(x = []
|| not
(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])
• ##### subproof
(x = [] || not (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
• start[0.033s, "1.1"]
(x = []
|| not
(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
• ###### 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
not (x = []) || List.length (List.append x y) = List.length x + List.length y
• start[0.033s, "1.2"]
not (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_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_instances0
definitions0
inductions0
search_time
0.040s
details
Expand
smt_stats
 rlimit count 229 mk bool var 5 num allocs 1.26815e+08 memory 12.54 max memory 15.56
Expand
• start[0.040s] List.length :var_0: >= 0
• #### simplify

 into true expansions [] rewrite_steps forward_chaining List.len_nonnegative
• #### unsat

(mp (asserted (not true)) (rewrite (= (not true) false)) false)
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.016s
Expand
• start[0.016s, "Goal"] List.append :var_0: [] = :var_0:
• #### subproof

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