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¶

Try this!

In [1]:

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

Out[1]:

- : '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.081s

Expand

start[0.081s, "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.039s, "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_nonnegative
  List.len_nonnegative
  List.len_nonnegative
  List.len_nonnegative
  List.len_nonnegative
subproof
x <> [] || (List.length (List.append x y) = List.length x + List.length y)
- start[0.039s, "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_nonnegative
  List.len_nonnegative
  List.len_nonnegative
  List.len_nonnegative
  List.len_nonnegative
  List.len_nonnegative

digraph "proof" {
p_19 [label="Start (List.length (List.append ( :var_0: ) ( :var_1: ))\l       = List.length ( :var_0: ) + List.length ( :var_1: ) :name \"Goal\"\l       :time 0.081s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_19 -> p_17 [label=""];
subgraph cluster_18 {
  color=blue;
p_17 [label="Start (List.length (List.append x y) = List.length x + List.length y\l       :name \"1\" :time 0.080s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_17 -> p_16 [label=""];
p_16 [label="Induct ((functional ?),\l        :scheme (not (x \<\> []) ==\> φ x y)\l                && (x \<\> [] && φ (List.tl x) y ==\> φ x y))",shape=box,style=filled,fontname="courier",fontsize=14];
p_16 -> p_15 [label=""];
p_15 [label="Split (let (_x_0 : bool) = x \<\> [] in\l       let (_x_1 : int) = List.length y in\l       let (_x_2 : bool)\l           = List.length (List.append x y) = List.length x + _x_1\l       in\l       let (_x_3 : sko_ty_0 list) = List.tl x in\l       (_x_0 \|\| _x_2)\l       && (not\l           (_x_0\l            && (List.length (List.append _x_3 y) = List.length _x_3 + _x_1))\l           \|\| _x_2)\l       :cases [x \<\> []\l               \|\| (List.length (List.append x y)\l                   = List.length x + List.length y);\l               let (_x_0 : sko_ty_0 list) = List.tl x in\l               let (_x_1 : int) = List.length y in\l               not (x \<\> [])\l               \|\| not\l                  (List.length (List.append _x_0 y) = List.length _x_0 + _x_1)\l               \|\| (List.length (List.append x y) = List.length x + _x_1)])",shape=box,style=filled,fontname="courier",fontsize=14];
p_15 -> p_10 [label=""];
subgraph cluster_11 {
  color=blue;
p_10 [label="Start (let (_x_0 : sko_ty_0 list) = List.tl x in\l       let (_x_1 : int) = List.length y in\l       not (x \<\> [])\l       \|\| not (List.length (List.append _x_0 y) = List.length _x_0 + _x_1)\l       \|\| (List.length (List.append x y) = List.length x + _x_1) :name \"1.1\"\l       :time 0.039s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_10 -> p_9 [label=""];
p_9 [label="Simplify (true :expansions [List.length; List.length; List.append] :rw []\l          :fc [List.len_nonnegative;\l               List.len_nonnegative;\l               List.len_nonnegative;\l               List.len_nonnegative;\l               List.len_nonnegative])",shape=box,style=filled,fontname="courier",fontsize=14];
}
p_15 -> p_13 [label=""];
subgraph cluster_14 {
  color=blue;
p_13 [label="Start (x \<\> []\l       \|\| (List.length (List.append x y) = List.length x + List.length y)\l       :name \"1.2\" :time 0.039s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_13 -> p_12 [label=""];
p_12 [label="Simplify (true :expansions [List.length; List.append] :rw []\l          :fc [List.len_nonnegative;\l               List.len_nonnegative;\l               List.len_nonnegative;\l               List.len_nonnegative;\l               List.len_nonnegative;\l               List.len_nonnegative])",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
}

Try this!

In [2]:

verify (fun x -> x @ [] @ x = x @ x) [@@simp]

Out[2]:

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

Proved

proof
call graph

proof

ground_instances:

definitions:

inductions:

search_time:

0.042s

details:

Expand

smt_stats:

rlimit count:	430
num allocs:	54829479
time:	0.008000
memory:	15.510000
max memory:	15.980000

Expand

start[0.042s]
  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

Try this!

In [3]:

lemma len_append x y = List.length (x@y) = List.length x + List.length y [@@auto] [@@rw]

Out[3]:

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.090s

Expand

start[0.090s, "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.090s, "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.043s, "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_nonnegative
  List.len_nonnegative
  List.len_nonnegative
  List.len_nonnegative
  List.len_nonnegative
subproof
x <> [] || (List.length (List.append x y) = List.length x + List.length y)
- start[0.043s, "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_nonnegative
  List.len_nonnegative
  List.len_nonnegative
  List.len_nonnegative
  List.len_nonnegative
  List.len_nonnegative

digraph "proof" {
p_42 [label="Start (List.length (List.append ( :var_0: ) ( :var_1: ))\l       = List.length ( :var_0: ) + List.length ( :var_1: ) :name \"Goal\"\l       :time 0.090s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_42 -> p_40 [label=""];
subgraph cluster_41 {
  color=blue;
p_40 [label="Start (List.length (List.append x y) = List.length x + List.length y\l       :name \"1\" :time 0.090s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_40 -> p_39 [label=""];
p_39 [label="Induct ((functional ?),\l        :scheme (not (x \<\> []) ==\> φ x y)\l                && (x \<\> [] && φ (List.tl x) y ==\> φ x y))",shape=box,style=filled,fontname="courier",fontsize=14];
p_39 -> p_38 [label=""];
p_38 [label="Split (let (_x_0 : bool) = x \<\> [] in\l       let (_x_1 : int) = List.length y in\l       let (_x_2 : bool)\l           = List.length (List.append x y) = List.length x + _x_1\l       in\l       let (_x_3 : sko_ty_0 list) = List.tl x in\l       (_x_0 \|\| _x_2)\l       && (not\l           (_x_0\l            && (List.length (List.append _x_3 y) = List.length _x_3 + _x_1))\l           \|\| _x_2)\l       :cases [x \<\> []\l               \|\| (List.length (List.append x y)\l                   = List.length x + List.length y);\l               let (_x_0 : sko_ty_0 list) = List.tl x in\l               let (_x_1 : int) = List.length y in\l               not (x \<\> [])\l               \|\| not\l                  (List.length (List.append _x_0 y) = List.length _x_0 + _x_1)\l               \|\| (List.length (List.append x y) = List.length x + _x_1)])",shape=box,style=filled,fontname="courier",fontsize=14];
p_38 -> p_33 [label=""];
subgraph cluster_34 {
  color=blue;
p_33 [label="Start (let (_x_0 : sko_ty_0 list) = List.tl x in\l       let (_x_1 : int) = List.length y in\l       not (x \<\> [])\l       \|\| not (List.length (List.append _x_0 y) = List.length _x_0 + _x_1)\l       \|\| (List.length (List.append x y) = List.length x + _x_1) :name \"1.1\"\l       :time 0.043s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_33 -> p_32 [label=""];
p_32 [label="Simplify (true :expansions [List.length; List.length; List.append] :rw []\l          :fc [List.len_nonnegative;\l               List.len_nonnegative;\l               List.len_nonnegative;\l               List.len_nonnegative;\l               List.len_nonnegative])",shape=box,style=filled,fontname="courier",fontsize=14];
}
p_38 -> p_36 [label=""];
subgraph cluster_37 {
  color=blue;
p_36 [label="Start (x \<\> []\l       \|\| (List.length (List.append x y) = List.length x + List.length y)\l       :name \"1.2\" :time 0.043s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_36 -> p_35 [label=""];
p_35 [label="Simplify (true :expansions [List.length; List.append] :rw []\l          :fc [List.len_nonnegative;\l               List.len_nonnegative;\l               List.len_nonnegative;\l               List.len_nonnegative;\l               List.len_nonnegative;\l               List.len_nonnegative])",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
}

Try this!

In [4]:

theorem len_non_neg x = (List.length x) [@trigger] >= 0 [@@simp] [@@fc]

Out[4]:

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

Proved

proof
call graph

proof

ground_instances:

definitions:

inductions:

search_time:

0.029s

details:

Expand

smt_stats:

rlimit count:	514
num allocs:	174727728
time:	0.007000
memory:	16.080000
max memory:	16.570000

Expand

start[0.029s] List.length ( :var_0: ) >= 0

simplify
into:
true
expansions:
[]
rewrite_steps:
forward_chaining:
List.len_nonnegative
Unsat

Try this!

In [5]:

lemma foo = (fun x -> x @ [] = x) [@@induct x] [@@disable List.append_to_nil]

Out[5]:

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.013s

Expand

start[0.013s, "Goal"] List.append ( :var_0: ) [] = ( :var_0: )

subproof
List.append x [] = x
- start[0.013s, "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.012s, "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.012s, "2"] List.append [] [] = []
  simplify
  into:
  true
  expansions:
  List.append
  rewrite_steps:
  forward_chaining:

digraph "proof" {
p_56 [label="Start (List.append ( :var_0: ) [] = ( :var_0: ) :name \"Goal\" :time 0.013s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_56 -> p_54 [label=""];
subgraph cluster_55 {
  color=blue;
p_54 [label="Start (List.append x [] = x :name \"1\" :time 0.013s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_54 -> p_53 [label=""];
p_53 [label="Induct ((structural+ x),\l        :scheme φ [] && (x \<\> [] && φ (List.tl x) ==\> φ x))",shape=box,style=filled,fontname="courier",fontsize=14];
p_53 -> p_52 [label=""];
p_52 [label="Split (let (_x_0 : sko_ty_0 list) = List.tl x in\l       (List.append [] [] = [])\l       && (not (x \<\> [] && (List.append _x_0 [] = _x_0))\l           \|\| (List.append x [] = x))\l       :cases [List.append [] [] = [];\l               let (_x_0 : sko_ty_0 list) = List.tl x in\l               not (x \<\> []) \|\| not (List.append _x_0 [] = _x_0)\l               \|\| (List.append x [] = x)])",shape=box,style=filled,fontname="courier",fontsize=14];
p_52 -> p_47 [label=""];
subgraph cluster_48 {
  color=blue;
p_47 [label="Start (let (_x_0 : sko_ty_0 list) = List.tl x in\l       not (x \<\> []) \|\| not (List.append _x_0 [] = _x_0)\l       \|\| (List.append x [] = x) :name \"1\" :time 0.012s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_47 -> p_46 [label=""];
p_46 [label="Simplify (true :expansions [List.append] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
}
p_52 -> p_50 [label=""];
subgraph cluster_51 {
  color=blue;
p_50 [label="Start (List.append [] [] = [] :name \"2\" :time 0.012s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_50 -> p_49 [label=""];
p_49 [label="Simplify (true :expansions [List.append] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
}

into:	true
expansions:	[List.length, List.length, List.append]
rewrite_steps:
forward_chaining:	List.len_nonnegative List.len_nonnegative List.len_nonnegative List.len_nonnegative List.len_nonnegative

Attributes¶

Verification Hints¶

Rule Classes¶

Examples¶

subproof

subproof

simplify

subproof

simplify

simplify

subproof

subproof

simplify

subproof

simplify

simplify

subproof

subproof

simplify

subproof

simplify