Simplification¶

At the heart of Imandra is a powerful symbolic simplifier and partial evaluator. The simplifier is integrated with the inductive waterfall (e.g., [@@auto]), and is the main way in which previously proved lemmas are used during proofs, through the automatic application of rules. The simplifier can also be used as a pre-processing step before unrolling, via the [@@simp] attribute.

As the name suggests, simplification is a process that attempts to transform a formula into a "simpler" form, bringing the salient features of a formula or conjecture to the surface. Simplification can also prove goals by reducing them to true, and refute them by reducing them to false.

Notably, because the symbolic evaluation semantics of the simplifier operate on a compact digraph representation of formulas and function definitions, simplification can be thought as having memoized semantics for free.

We can see an example of this by using the following naive recursive version of the fibonacci function:

Try this!

In [1]:

let rec fib n =
  if n <= 1 then
    1
  else
    fib (n-1) + fib (n-2)

Out[1]:

val fib : Z.t -> Z.t = <fun>

termination proof

Termination proof

call `fib (n - 1)` from `fib n`

original:

fib n

sub:

fib (n - 1)

original ordinal:

Ordinal.Int (_cnt n)

sub ordinal:

Ordinal.Int (_cnt (n - 1))

path:

[not (n <= 1)]

proof:

detailed proof

summary
full

ground_instances:

definitions:

inductions:

search_time:

0.016s

details:

Expand

smt_stats:

num checks:	3
arith assert lower:	6
arith tableau max rows:	4
arith tableau max columns:	9
arith pivots:	2
rlimit count:	2202
mk clause:	5
datatype occurs check:	2
mk bool var:	17
arith assert upper:	3
decisions:	2
arith row summations:	3
propagations:	2
conflicts:	2
arith fixed eqs:	2
datatype accessor ax:	2
arith conflicts:	1
arith num rows:	4
num allocs:	9389053
final checks:	1
added eqs:	4
del clause:	5
arith eq adapter:	2
memory:	15.230000
max memory:	15.230000

Expand

start[0.016s]
  let (_x_0 : int) = if n >= 0 then n else 0 in
  let (_x_1 : int) = n - 1 in
  let (_x_2 : int) = if _x_1 >= 0 then _x_1 else 0 in
  let (_x_3 : bool) = _x_1 <= 1 in
  not (n <= 1) && ((_x_0 >= 0) && (_x_2 >= 0))
  ==> (_x_3 && _x_3) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)

simplify

into:	(n <= 1) \|\| (n <= 2) \|\| Ordinal.( << ) (Ordinal.Int (if n >= 1 then (-1) + n else 0)) (Ordinal.Int (if n >= 0 then n else 0))
expansions:	[]
rewrite_steps:
forward_chaining:

unroll

expr:	(\|Ordinal.<<\| (\|Ordinal.Int_79/boot\| (ite (>= n_371/server 1) (+ (- 1) n_371/server)…
expansions:

Unsat

call `fib (n - 2)` from `fib n`

original:

fib n

sub:

fib (n - 2)

original ordinal:

Ordinal.Int (_cnt n)

sub ordinal:

Ordinal.Int (_cnt (n - 2))

path:

[not (n <= 1)]

proof:

detailed proof

summary
full

ground_instances:

definitions:

inductions:

search_time:

0.016s

details:

Expand

smt_stats:

num checks:	3
arith assert lower:	6
arith tableau max rows:	4
arith tableau max columns:	10
arith pivots:	2
rlimit count:	1101
mk clause:	5
datatype occurs check:	2
mk bool var:	17
arith assert upper:	3
decisions:	2
arith row summations:	3
propagations:	2
conflicts:	2
arith fixed eqs:	2
datatype accessor ax:	2
arith conflicts:	1
arith num rows:	4
num allocs:	5374681
final checks:	1
added eqs:	4
del clause:	5
arith eq adapter:	2
memory:	15.200000
max memory:	15.200000

Expand

start[0.016s]
  let (_x_0 : int) = if n >= 0 then n else 0 in
  let (_x_1 : int) = n - 2 in
  let (_x_2 : int) = if _x_1 >= 0 then _x_1 else 0 in
  let (_x_3 : bool) = _x_1 <= 1 in
  not (n <= 1) && ((_x_0 >= 0) && (_x_2 >= 0))
  ==> (_x_3 && _x_3) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)

simplify

into:	(n <= 1) \|\| (n <= 3) \|\| Ordinal.( << ) (Ordinal.Int (if n >= 2 then (-2) + n else 0)) (Ordinal.Int (if n >= 0 then n else 0))
expansions:	[]
rewrite_steps:
forward_chaining:

unroll

expr:	(\|Ordinal.<<\| (\|Ordinal.Int_79/boot\| (ite (>= n_371/server 2) (+ (- 2) n_371/server)…
expansions:

Unsat

If we try to use Imandra's simplification to search for a solution for fib 200, Imandra comes back to us with a solution immediately:

Try this!

In [2]:

#check_models false;;
instance (fun x -> x = fib 200) [@@simp];;
#check_models true;;

Out[2]:

- : Z.t -> bool = <fun>
module CX : sig val x : Z.t end

Instance (after 0 steps, 0.088s):
let x : int = 453973694165307953197296969697410619233826

Instance

call graph
proof

proof attempt

ground_instances:

definitions:

201

inductions:

search_time:

0.089s

details:

Expand

smt_stats:

eliminated vars:	1
rlimit count:	8149
num allocs:	33118257
time:	0.013000
memory:	15.720000
max memory:	16.170000

Expand

```
start[0.089s] ( :var_0: ) = fib 200
```

simplify

into:	x = 453973694165307953197296969697410619233826
expansions:	[fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib]
rewrite_steps:
forward_chaining:

Sat (Some let x : int = (Z.of_string "453973694165307953197296969697410619233826") )

digraph "proof" {
p_10 [label="Start (( :var_0: ) = fib 200 :time 0.089s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_10 -> p_9 [label=""];
p_9 [label="Simplify (x = 453973694165307953197296969697410619233826\l          :expansions [fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib;\l                       fib]\l          :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_9 -> p_8 [label=""];
p_8 [label="Sat (Some let x : int = (Z.of_string \"453973694165307953197296969697410619233826\")\l)",shape=box,style=filled,fontname="courier",fontsize=14];
}

If, however, we tried to use normal OCaml evaluation to compute fib 200, OCaml would take over 10 minutes in order to come back with a response (the #check_models false command here is used to tell Imandra not to check the instance Imandra computed using OCaml evaluation, as that requires the expensive computation of fib 200 via standard OCaml evaluation, which is not memoized).

Now that we know what simplification does, let's learn about how to influence it using rewrite and forward chaining rules.

Rewrite Rules¶

A rewrite rule is a theorem of the form

h_1 && ... && h_k ==> lhs = rhs

which Imandra can use in further proofs to replace terms that match with lhs (the "left hand side") with the appropriate instantiation of rhs (the "right hand side"), provided that the instantiations of the hypotheses can be established. Observe that rewrite rules are both conditional (requiring in general the establishment of hypotheses) and directed (replacing lhs with rhs). The lhs is also called the "pattern" of the rule.

An enabled rewrite rule causes Imandra to look for matches of the lhs, replacing the matched term with the (suitably instantiated) rhs, provided that Imandra can establish ("relieve") the (suitably instantiated) hypotheses of the rule.

For example, consider the lemma rev_len below. This lemma expresses the fact that the length of a list x is equal to the length of List.rev x, i.e., if we reverse a list, we end up with a list of the same length. This rule is unconditional: it has no hypotheses. Thus, it will always be able to fire on terms that match its left-hand side. Notice that Imandra uses a previously defined rewrite rule in order to prove this lemma! The lemma rev_len would make an excellent rewrite rule, so we use the [@@rw] annotation to install it:

Try this!

In [3]:

lemma rev_len x =
  List.length (List.rev x) = List.length x
[@@auto] [@@rw]

Out[3]:

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

List.length (List.rev x) = List.length x.

1 nontautological subgoal.

Subgoal 1:

|---------------------------------------------------------------------------
 List.length (List.rev x) = List.length x


Must try induction.

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

We shall induct according to a scheme derived from List.rev.

Induction scheme:

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

2 nontautological subgoals.

Subgoal 1.2:

|---------------------------------------------------------------------------
 C0. x <> []
 C1. List.length (List.rev x) = List.length x

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

Subgoal 1.1:

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

This simplifies, using the definitions of List.length and List.rev to:

Subgoal 1.1':

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


We can eliminate destructors by the following substitution:
 x -> x1 :: x2

This produces the modified subgoal:

Subgoal 1.1'':

 H0. List.length (List.rev x2) = List.length x2
|---------------------------------------------------------------------------
 List.length (List.append (List.rev x2) [x1]) = 1 + List.length x2


Cross-fertilizing with:

 List.length (List.rev x2) = List.length x2

This produces the modified subgoal:

Subgoal 1.1''':

|---------------------------------------------------------------------------
 List.length (List.append (List.rev x2) [x1]) = 1 + List.length (List.rev x2)


Candidates for generalization:

 List.rev x2

This produces the modified subgoal:

Subgoal 1.1'''':

|---------------------------------------------------------------------------
 List.length (List.append gen_1 [x1]) = 1 + List.length gen_1


Must try induction.

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

We shall induct according to a scheme derived from List.append.

Induction scheme:

 (not (gen_1 <> []) ==> φ gen_1 x1)
 && (gen_1 <> [] && φ (List.tl gen_1) x1 ==> φ gen_1 x1).

2 nontautological subgoals.

Subgoal 1.1''''.2:

|---------------------------------------------------------------------------
 C0. gen_1 <> []
 C1. List.length (List.append gen_1 [x1]) = 1 + List.length gen_1

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

Subgoal 1.1''''.1:

 H0. gen_1 <> []
 H1. List.length (List.append (List.tl gen_1) [x1])
     = 1 + List.length (List.tl gen_1)
|---------------------------------------------------------------------------
 List.length (List.append gen_1 [x1]) = 1 + List.length gen_1

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

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

Proved

proof

ground_instances:	0
definitions:	12
inductions:	2
search_time:	0.358s

Expand

start[0.358s, "Goal"]
  List.length (List.rev ( :var_0: )) = List.length ( :var_0: )

subproof

List.length (List.rev x) = List.length x

start[0.358s, "1"] List.length (List.rev x) = List.length x

induction on (functional ?)
:scheme (not (x <> []) ==> φ x) && (x <> [] && φ (List.tl x) ==> φ x)

Split (let (_x_0 : bool) = x <> [] in
       let (_x_1 : bool) = List.length (List.rev x) = List.length x in
       let (_x_2 : sko_ty_0 list) = List.tl x in
       (_x_0 || _x_1)
       && (not (_x_0 && (List.length (List.rev _x_2) = List.length _x_2))
           || _x_1)
       :cases [x <> [] || (List.length (List.rev x) = List.length x);
               let (_x_0 : sko_ty_0 list) = List.tl x in
               not (x <> [])
               || not (List.length (List.rev _x_0) = List.length _x_0)
               || (List.length (List.rev x) = List.length x)])

subproof

let (_x_0 : sko_ty_0 list) = List.tl x in not (x <> []) || not (List.length (List.rev _x_0) = List.length _x_0) || (List.length (List.rev x) = List.length x)

start[0.321s, "1.1"]
  let (_x_0 : sko_ty_0 list) = List.tl x in
  not (x <> []) || not (List.length (List.rev _x_0) = List.length _x_0)
  || (List.length (List.rev x) = List.length x)

simplify

into:	let (_x_0 : sko_ty_0 list) = List.tl x in let (_x_1 : sko_ty_0 list) = List.rev _x_0 in let (_x_2 : int) = List.length _x_0 in not (x <> []) \|\| not (List.length _x_1 = _x_2) \|\| (List.length (List.append _x_1 [List.hd x]) = 1 + _x_2)
expansions:	[List.length, List.rev]
rewrite_steps:
forward_chaining:	List.len_nonnegative List.len_nonnegative List.len_nonnegative List.len_nonnegative List.len_nonnegative List.len_nonnegative List.len_nonnegative List.len_nonnegative List.len_nonnegative List.len_nonnegative List.len_nonnegative

Elim_destructor (:cstor ( :: ) :replace x1 :: x2 :context [])

Generalize (let (_x_0 : sko_ty_0 list) = List.rev x2 in
            List.length (List.append _x_0 [x1]) = 1 + List.length _x_0
            :as (gen_1 : sko_ty_0 list))

induction on (functional ?)
:scheme (not (gen_1 <> []) ==> φ gen_1 x1)
        && (gen_1 <> [] && φ (List.tl gen_1) x1 ==> φ gen_1 x1)

Split (let (_x_0 : bool) = gen_1 <> [] in
       let (_x_1 : sko_ty_0 list) = [x1] in
       let (_x_2 : bool)
           = List.length (List.append gen_1 _x_1) = 1 + List.length gen_1
       in
       let (_x_3 : sko_ty_0 list) = List.tl gen_1 in
       (_x_0 || _x_2)
       && (not
           (_x_0
            && (List.length (List.append _x_3 _x_1) = 1 + List.length _x_3))
           || _x_2)
       :cases [gen_1 <> []
               || (List.length (List.append gen_1 [x1])
                   = 1 + List.length gen_1);
               let (_x_0 : sko_ty_0 list) = List.tl gen_1 in
               let (_x_1 : sko_ty_0 list) = [x1] in
               not (gen_1 <> [])
               || not
                  (List.length (List.append _x_0 _x_1) = 1 + List.length _x_0)
               || (List.length (List.append gen_1 _x_1)
                   = 1 + List.length gen_1)])

```
Subproof
```
```
Subproof
```

subproof
x <> [] || (List.length (List.rev x) = List.length x)
- start[0.321s, "1.2"] x <> [] || (List.length (List.rev x) = List.length x)
- simplify
  into:
  true
  expansions:
  [List.length, List.length, List.rev]
  rewrite_steps:
  forward_chaining:
  List.len_nonnegative
  List.len_nonnegative
  List.len_nonnegative
  List.len_nonnegative

digraph "proof" {
p_86 [label="Start (List.length (List.rev ( :var_0: )) = List.length ( :var_0: )\l       :name \"Goal\" :time 0.358s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_86 -> p_84 [label=""];
subgraph cluster_85 {
  color=blue;
p_84 [label="Start (List.length (List.rev x) = List.length x :name \"1\" :time 0.358s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_84 -> p_83 [label=""];
p_83 [label="Induct ((functional ?),\l        :scheme (not (x \<\> []) ==\> φ x)\l                && (x \<\> [] && φ (List.tl x) ==\> φ x))",shape=box,style=filled,fontname="courier",fontsize=14];
p_83 -> p_82 [label=""];
p_82 [label="Split (let (_x_0 : bool) = x \<\> [] in\l       let (_x_1 : bool) = List.length (List.rev x) = List.length x in\l       let (_x_2 : sko_ty_0 list) = List.tl x in\l       (_x_0 \|\| _x_1)\l       && (not (_x_0 && (List.length (List.rev _x_2) = List.length _x_2))\l           \|\| _x_1)\l       :cases [x \<\> [] \|\| (List.length (List.rev x) = List.length x);\l               let (_x_0 : sko_ty_0 list) = List.tl x in\l               not (x \<\> [])\l               \|\| not (List.length (List.rev _x_0) = List.length _x_0)\l               \|\| (List.length (List.rev x) = List.length x)])",shape=box,style=filled,fontname="courier",fontsize=14];
p_82 -> p_77 [label=""];
subgraph cluster_78 {
  color=blue;
p_77 [label="Start (let (_x_0 : sko_ty_0 list) = List.tl x in\l       not (x \<\> []) \|\| not (List.length (List.rev _x_0) = List.length _x_0)\l       \|\| (List.length (List.rev x) = List.length x) :name \"1.1\" :time 0.321s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_77 -> p_76 [label=""];
p_76 [label="Simplify (let (_x_0 : sko_ty_0 list) = List.tl x in\l          let (_x_1 : sko_ty_0 list) = List.rev _x_0 in\l          let (_x_2 : int) = List.length _x_0 in\l          not (x \<\> []) \|\| not (List.length _x_1 = _x_2)\l          \|\| (List.length (List.append _x_1 [List.hd x]) = 1 + _x_2)\l          :expansions [List.length; List.rev] :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;\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];
p_76 -> p_75 [label=""];
p_75 [label="Elim_destructor (:cstor ( :: ) :replace x1 :: x2 :context [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_75 -> p_74 [label=""];
p_74 [label="Generalize (let (_x_0 : sko_ty_0 list) = List.rev x2 in\l            List.length (List.append _x_0 [x1]) = 1 + List.length _x_0\l            :as (gen_1 : sko_ty_0 list))",shape=box,style=filled,fontname="courier",fontsize=14];
p_74 -> p_73 [label=""];
p_73 [label="Induct ((functional ?),\l        :scheme (not (gen_1 \<\> []) ==\> φ gen_1 x1)\l                && (gen_1 \<\> [] && φ (List.tl gen_1) x1 ==\> φ gen_1 x1))",shape=box,style=filled,fontname="courier",fontsize=14];
p_73 -> p_72 [label=""];
p_72 [label="Split (let (_x_0 : bool) = gen_1 \<\> [] in\l       let (_x_1 : sko_ty_0 list) = [x1] in\l       let (_x_2 : bool)\l           = List.length (List.append gen_1 _x_1) = 1 + List.length gen_1\l       in\l       let (_x_3 : sko_ty_0 list) = List.tl gen_1 in\l       (_x_0 \|\| _x_2)\l       && (not\l           (_x_0\l            && (List.length (List.append _x_3 _x_1) = 1 + List.length _x_3))\l           \|\| _x_2)\l       :cases [gen_1 \<\> []\l               \|\| (List.length (List.append gen_1 [x1])\l                   = 1 + List.length gen_1);\l               let (_x_0 : sko_ty_0 list) = List.tl gen_1 in\l               let (_x_1 : sko_ty_0 list) = [x1] in\l               not (gen_1 \<\> [])\l               \|\| not\l                  (List.length (List.append _x_0 _x_1) = 1 + List.length _x_0)\l               \|\| (List.length (List.append gen_1 _x_1)\l                   = 1 + List.length gen_1)])",shape=box,style=filled,fontname="courier",fontsize=14];
p_72 -> p_67 [label=""];
subgraph cluster_68 {
  color=blue;
p_67 [label="Start (let (_x_0 : sko_ty_0 list) = List.tl gen_1 in\l       let (_x_1 : sko_ty_0 list) = [x1] in\l       not (gen_1 \<\> [])\l       \|\| not (List.length (List.append _x_0 _x_1) = 1 + List.length _x_0)\l       \|\| (List.length (List.append gen_1 _x_1) = 1 + List.length gen_1)\l       :name \"1.1''''.1\" :time 0.015s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_67 -> p_66 [label=""];
p_66 [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])",shape=box,style=filled,fontname="courier",fontsize=14];
}
p_72 -> p_70 [label=""];
subgraph cluster_71 {
  color=blue;
p_70 [label="Start (gen_1 \<\> []\l       \|\| (List.length (List.append gen_1 [x1]) = 1 + List.length gen_1)\l       :name \"1.1''''.2\" :time 0.015s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_70 -> p_69 [label=""];
p_69 [label="Simplify (true\l          :expansions [List.length; List.length; List.length; List.append]\l          :rw []\l          :fc [List.len_nonnegative;\l               List.len_nonnegative;\l               List.len_nonnegative;\l               List.len_nonnegative])",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
p_82 -> p_80 [label=""];
subgraph cluster_81 {
  color=blue;
p_80 [label="Start (x \<\> [] \|\| (List.length (List.rev x) = List.length x) :name \"1.2\"\l       :time 0.321s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_80 -> p_79 [label=""];
p_79 [label="Simplify (true :expansions [List.length; List.length; List.rev] :rw []\l          :fc [List.len_nonnegative;\l               List.len_nonnegative;\l               List.len_nonnegative;\l               List.len_nonnegative])",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
}

With this rule installed and enabled, if Imandra's simplifier encounters a term of the form List.length (List.rev <term>), it will replace it with the simpler form List.length <term>.

Both the hypotheses and rhs can be omitted, in which case Imandra will default them to true. That is, h_1 && ... && h_k ==> lhs is equivalent to h_1 && h_k ==> lhs = true and lhs = rhs is equal to true ==> lhs = rhs.

Imandra's rewriting is:

conditional: rewrite rules may contain conditions (hypotheses), and eligible rules are only applied when their hypotheses are established. Once the pattern of a rule has been matched, Imandra uses backward-chaining ("backchaining") to relieve the rule's hypotheses, recursively attempting to simplify them to true modulo the current simplification context. This is important to keep in mind when developing your theories: rewrite rules will not fire unless Imandra can simplify their instantiated hypotheses to true.
oriented: given a rule whose conclusion is of the form lhs = rhs, rewriting happens by replacing the (instantiated) lhs with the (instantiated) rhs.

When adding a new rewrite rule, users should take care to orient the equality so that rhs is simpler or more canonical than lhs. If it's not clear what it means for an rhs to be "better" than the lhs, e.g., in the case of the proof for the associativity of append x @ (y @ z) = (x @ y) @ z, a canonical form should typically be chosen (e.g., associating to the left in this case) and kept in mind for further rules.

By default, the lhs must contain all the top-level variables of the theorem (i.e. the arguments to the lambda term representing the goal). There is an exception to this rule: if the lhs does not contain all the variables of the theorem but the rule hypotheses have subterms containing the remaining free variables, these terms can be annotated with [@trigger rw], signaling Imandra that the annotated terms should be used to complete the matching.

It's helpful to see an example where the use of [@trigger rw] is necessary. Let's first define a subset function on lists:

Try this!

In [4]:

let rec subset x y =
  match x with
  | [] -> true
  | x :: xs ->
    if List.mem x y then subset xs y
    else false

Out[4]:

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

termination proof

Termination proof

call `subset (List.tl x) y` from `subset x y`

original:

subset x y

sub:

subset (List.tl x) y

original ordinal:

Ordinal.Int (_cnt x)

sub ordinal:

Ordinal.Int (_cnt (List.tl x))

path:

[List.mem (List.hd x) y && x <> []]

proof:

detailed proof

summary
full

ground_instances:

definitions:

inductions:

search_time:

0.013s

details:

Expand

smt_stats:

num checks:	8
arith assert lower:	5
arith tableau max rows:	4
arith tableau max columns:	11
arith pivots:	4
rlimit count:	1980
mk clause:	11
datatype occurs check:	12
mk bool var:	50
arith assert upper:	5
datatype splits:	1
decisions:	10
arith row summations:	7
propagations:	10
conflicts:	7
arith fixed eqs:	4
datatype accessor ax:	9
arith conflicts:	1
arith num rows:	4
datatype constructor ax:	7
num allocs:	534275276
final checks:	4
added eqs:	34
del clause:	3
arith eq adapter:	4
memory:	16.660000
max memory:	16.980000

Expand

start[0.013s]
  let (_x_0 : int) = count.list (const 0) x in
  let (_x_1 : ty_0 list) = List.tl x in
  let (_x_2 : int) = count.list (const 0) _x_1 in
  List.mem (List.hd x) y && (x <> [] && ((_x_0 >= 0) && (_x_2 >= 0)))
  ==> not (List.mem (List.hd _x_1) y && _x_1 <> [])
      || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)

simplify

into:	let (_x_0 : ty_0 list) = List.tl x in let (_x_1 : int) = count.list (const 0) _x_0 in let (_x_2 : int) = count.list (const 0) x in not (List.mem (List.hd _x_0) y && _x_0 <> []) \|\| Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) \|\| not (List.mem (List.hd x) y && x <> [] && (_x_2 >= 0) && (_x_1 >= 0))
expansions:	[]
rewrite_steps:
forward_chaining:

unroll

expr:	(\|Ordinal.<<\| (\|Ordinal.Int_79/boot\| (\|count.list_698/server\| (\|get.::.1_674/server\|…
expansions:

unroll

expr:	(\|count.list_698/server\| (\|get.::.1_674/server\| x_685/server))
expansions:

unroll
expr:
(|count.list_698/server| x_685/server)
expansions:
Unsat

Let's now suppose that we want to verify the transitivity of subset:

Try this!

In [5]:

#max_induct 1;;

verify (fun x y z -> subset x y && subset y z ==> subset x z) [@@auto];;

Out[5]:

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

subset x y && subset y z ==> subset x z.

1 nontautological subgoal.

Subgoal 1:

 H0. subset x y
 H1. subset y z
|---------------------------------------------------------------------------
 subset x z


Must try induction.

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

However, scheme scoring gives us a clear winner.
We shall induct according to a scheme derived from subset.

Induction scheme:

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

2 nontautological subgoals.

Subgoal 1.2:

 H0. subset y z
 H1. subset x y
|---------------------------------------------------------------------------
 C0. subset x z
 C1. List.mem (List.hd x) z && x <> []

This simplifies, using the definition of subset to:

Subgoal 1.2':

 H0. subset y z
 H1. subset x y
 H2. x <> []
|---------------------------------------------------------------------------
 List.mem (List.hd x) z


We can eliminate destructors by the following substitution:
 x -> x1 :: x2

This produces the modified subgoal:

Subgoal 1.2'':

 H0. subset y z
 H1. subset (x1 :: x2) y
|---------------------------------------------------------------------------
 List.mem x1 z

This simplifies, using the definition of subset to:

Subgoal 1.2''':

 H0. subset x2 y
 H1. subset y z
 H2. List.mem x1 y
|---------------------------------------------------------------------------
 List.mem x1 z


Must try induction.

 ⚠  Aborting proof attempt for _verify_target.

 ⓘ  Rules:
    (:def subset)
    (:induct subset)

Checkpoints:

 H0. subset x2 y
 H1. subset y z
 H2. List.mem x1 y
|---------------------------------------------------------------------------
 List.mem x1 z

Error:
  Maximum induction depth reached (1). You can set this with #max_induct.
  At <none>:1

It looks like Imandra needs an additional lemma in order to prove this. By inspecting the checkpoint, it looks like all we need is a rule relating subset and List.mem. Let's attempt to prove it:

Try this!

In [6]:

lemma mem_subset x y z =
  List.mem x y && subset y z ==> List.mem x z
[@@auto] [@@rewrite]

Out[6]:

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

List.mem x y && subset y z ==> List.mem x z.

1 nontautological subgoal.

Subgoal 1:

 H0. List.mem x y
 H1. subset y z
|---------------------------------------------------------------------------
 List.mem x z


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 subset.

Induction scheme:

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

2 nontautological subgoals.

Subgoal 1.2:

 H0. subset y z
 H1. List.mem x y
|---------------------------------------------------------------------------
 C0. List.mem x z
 C1. List.mem (List.hd y) z && y <> []

This simplifies, using the definitions of List.mem and subset to:

Subgoal 1.2':

 H0. List.mem x y
|---------------------------------------------------------------------------
 C0. List.mem x z
 C1. List.mem (List.hd y) z
 C2. y <> []

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

Subgoal 1.1:

 H0. subset y z
 H1. List.mem x y
 H2. y <> []
 H3. List.mem (List.hd y) z
 H4. List.mem x (List.tl y) && subset (List.tl y) z ==> List.mem x z
|---------------------------------------------------------------------------
 List.mem x z

But simplification reduces this to true, using the definitions of List.mem
and subset.

 ⓘ  Rules:
    (:def List.mem)
    (:def subset)
    (:induct subset)

Error:
  unsupported: in rewrite rule,
  variable (y : 'a list) does not occur in left-hand side of the rule
  or in `[@trigger rw]` terms
  See https://docs.imandra.ai/imandra-docs/notebooks/verification-simplification/#Rewrite-Rules
  At jupyter cell 6:1,0--91
  1 | lemma mem_subset x y z =
  2 |   List.mem x y && subset y z ==> List.mem x z
  3 | [@@auto] [@@rewrite]

While Imandra was successful in proving this lemma, it raised an error while trying to turn this lemma into a rewrite rule. As Imandra tells us, this is because the free variable y does not appear in the lhs term List.mem x z. If we, however, annotate the subset y z term with the appropriate [@trigger rw] attribute, Imandra can then successfully turn this term into a valid rewrite rule:

Try this!

In [7]:

lemma mem_subset x y z =
  List.mem x y && (subset y z [@trigger rw]) ==> List.mem x z
[@@auto] [@@rewrite]

Out[7]:

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

List.mem x y && subset y z ==> List.mem x z.

1 nontautological subgoal.

Subgoal 1:

 H0. List.mem x y
 H1. subset y z
|---------------------------------------------------------------------------
 List.mem x z


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 subset.

Induction scheme:

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

2 nontautological subgoals.

Subgoal 1.2:

 H0. List.mem x y
 H1. subset y z
|---------------------------------------------------------------------------
 C0. List.mem x z
 C1. List.mem (List.hd y) z && y <> []

But simplification reduces this to true, using the definitions of List.mem
and subset.

Subgoal 1.1:

 H0. List.mem x y
 H1. subset y z
 H2. y <> []
 H3. List.mem (List.hd y) z
 H4. List.mem x (List.tl y) && subset (List.tl y) z ==> List.mem x z
|---------------------------------------------------------------------------
 List.mem x z

But simplification reduces this to true, using the definitions of List.mem
and subset.

 ⓘ  Rules:
    (:def List.mem)
    (:def subset)
    (:induct subset)

Proved

proof

ground_instances:	0
definitions:	6
inductions:	1
search_time:	0.166s

Expand

start[0.166s, "Goal"]
  List.mem ( :var_0: ) ( :var_1: ) && subset ( :var_1: ) ( :var_2: )
  ==> List.mem ( :var_0: ) ( :var_2: )

subproof

not (List.mem x y) || not (subset y z) || List.mem x z

start[0.166s, "1"] not (List.mem x y) || not (subset y z) || List.mem x z

induction on (functional ?)
:scheme (not (List.mem (List.hd y) z && y <> []) ==> φ x y z)
        && (y <> [] && (List.mem (List.hd y) z && φ x (List.tl y) z)
            ==> φ x y z)

Split (let (_x_0 : bool) = List.mem x z in
       let (_x_1 : bool) = _x_0 || not (List.mem x y) || not (subset y z) in
       let (_x_2 : bool) = List.mem (List.hd y) z in
       let (_x_3 : bool) = y <> [] in
       let (_x_4 : sko_ty_0 list) = List.tl y in
       (_x_1 || (_x_2 && _x_3))
       && (_x_1
           || not
              (_x_3 && _x_2
               && (not (List.mem x _x_4) || not (subset _x_4 z) || _x_0)))
       :cases [not (List.mem x y) || not (subset y z) || List.mem x z
               || (List.mem (List.hd y) z && y <> []);
               let (_x_0 : sko_ty_0 list) = List.tl y in
               let (_x_1 : bool) = List.mem x z in
               not (List.mem x y) || not (subset y z) || not (y <> [])
               || not (List.mem (List.hd y) z)
               || not (List.mem x _x_0 && subset _x_0 z ==> _x_1) || _x_1])

subproof
let (_x_0 : sko_ty_0 list) = List.tl y in let (_x_1 : bool) = List.mem x z in not (List.mem x y) || not (subset y z) || not (y <> []) || not (List.mem (List.hd y) z) || not (List.mem x _x_0 && subset _x_0 z ==> _x_1) || _x_1
- start[0.100s, "1.1"] let (_x_0 : sko_ty_0 list) = List.tl y in let (_x_1 : bool) = List.mem x z in not (List.mem x y) || not (subset y z) || not (y <> []) || not (List.mem (List.hd y) z) || not (List.mem x _x_0 && subset _x_0 z ==> _x_1) || _x_1
- simplify
  into:
  true
  expansions:
  [List.mem, subset]
  rewrite_steps:
  forward_chaining:
subproof
not (List.mem x y) || not (subset y z) || List.mem x z || (List.mem (List.hd y) z && y <> [])
- start[0.100s, "1.2"] not (List.mem x y) || not (subset y z) || List.mem x z || (List.mem (List.hd y) z && y <> [])
- simplify
  into:
  true
  expansions:
  [List.mem, subset, List.mem, subset]
  rewrite_steps:
  forward_chaining:

digraph "proof" {
p_165 [label="Start (List.mem ( :var_0: ) ( :var_1: ) && subset ( :var_1: ) ( :var_2: )\l       ==\> List.mem ( :var_0: ) ( :var_2: ) :name \"Goal\" :time 0.166s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_165 -> p_163 [label=""];
subgraph cluster_164 {
  color=blue;
p_163 [label="Start (not (List.mem x y) \|\| not (subset y z) \|\| List.mem x z :name \"1\"\l       :time 0.166s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_163 -> p_162 [label=""];
p_162 [label="Induct ((functional ?),\l        :scheme (not (List.mem (List.hd y) z && y \<\> []) ==\> φ x y z)\l                && (y \<\> [] && (List.mem (List.hd y) z && φ x (List.tl y) z)\l                    ==\> φ x y z))",shape=box,style=filled,fontname="courier",fontsize=14];
p_162 -> p_161 [label=""];
p_161 [label="Split (let (_x_0 : bool) = List.mem x z in\l       let (_x_1 : bool) = _x_0 \|\| not (List.mem x y) \|\| not (subset y z) in\l       let (_x_2 : bool) = List.mem (List.hd y) z in\l       let (_x_3 : bool) = y \<\> [] in\l       let (_x_4 : sko_ty_0 list) = List.tl y in\l       (_x_1 \|\| (_x_2 && _x_3))\l       && (_x_1\l           \|\| not\l              (_x_3 && _x_2\l               && (not (List.mem x _x_4) \|\| not (subset _x_4 z) \|\| _x_0)))\l       :cases [not (List.mem x y) \|\| not (subset y z) \|\| List.mem x z\l               \|\| (List.mem (List.hd y) z && y \<\> []);\l               let (_x_0 : sko_ty_0 list) = List.tl y in\l               let (_x_1 : bool) = List.mem x z in\l               not (List.mem x y) \|\| not (subset y z) \|\| not (y \<\> [])\l               \|\| not (List.mem (List.hd y) z)\l               \|\| not (List.mem x _x_0 && subset _x_0 z ==\> _x_1) \|\| _x_1])",shape=box,style=filled,fontname="courier",fontsize=14];
p_161 -> p_156 [label=""];
subgraph cluster_157 {
  color=blue;
p_156 [label="Start (let (_x_0 : sko_ty_0 list) = List.tl y in\l       let (_x_1 : bool) = List.mem x z in\l       not (List.mem x y) \|\| not (subset y z) \|\| not (y \<\> [])\l       \|\| not (List.mem (List.hd y) z)\l       \|\| not (List.mem x _x_0 && subset _x_0 z ==\> _x_1) \|\| _x_1 :name \"1.1\"\l       :time 0.100s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_156 -> p_155 [label=""];
p_155 [label="Simplify (true :expansions [List.mem; subset] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
}
p_161 -> p_159 [label=""];
subgraph cluster_160 {
  color=blue;
p_159 [label="Start (not (List.mem x y) \|\| not (subset y z) \|\| List.mem x z\l       \|\| (List.mem (List.hd y) z && y \<\> []) :name \"1.2\" :time 0.100s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_159 -> p_158 [label=""];
p_158 [label="Simplify (true :expansions [List.mem; subset; List.mem; subset] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
}

And finally, let's verify that the rewrite rule can indeed match as we expect:

Try this!

In [8]:

verify (fun x y z -> subset x y && subset y z ==> subset x z) [@@auto]

Out[8]:

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

subset x y && subset y z ==> subset x z.

1 nontautological subgoal.

Subgoal 1:

 H0. subset x y
 H1. subset y z
|---------------------------------------------------------------------------
 subset x z


Must try induction.

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

However, scheme scoring gives us a clear winner.
We shall induct according to a scheme derived from subset.

Induction scheme:

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

2 nontautological subgoals.

Subgoal 1.2:

 H0. subset y z
 H1. subset x y
|---------------------------------------------------------------------------
 C0. subset x z
 C1. List.mem (List.hd x) z && x <> []

This simplifies, using the definition of subset to:

Subgoal 1.2':

 H0. subset y z
 H1. subset x y
 H2. x <> []
|---------------------------------------------------------------------------
 List.mem (List.hd x) z

But simplification reduces this to true, using the definition of List.mem,
and the rewrite rule mem_subset.

Subgoal 1.1:

 H0. x <> []
 H1. List.mem (List.hd x) z
 H2. subset (List.tl x) y && subset y z ==> subset (List.tl x) z
 H3. subset y z
 H4. subset x y
|---------------------------------------------------------------------------
 subset x z

But simplification reduces this to true, using the definitions of List.mem
and subset, and the rewrite rule mem_subset.

 ⓘ  Rules:
    (:def List.mem)
    (:def subset)
    (:rw mem_subset)
    (:induct subset)

Proved

proof

ground_instances:	0
definitions:	7
inductions:	1
search_time:	0.298s

Expand

start[0.298s, "Goal"]
  subset ( :var_0: ) ( :var_1: ) && subset ( :var_1: ) ( :var_2: )
  ==> subset ( :var_0: ) ( :var_2: )

subproof

not (subset x y) || not (subset y z) || subset x z

start[0.298s, "1"] not (subset x y) || not (subset y z) || subset x z

induction on (functional ?)
:scheme (not (List.mem (List.hd x) z && x <> []) ==> φ x y z)
        && (x <> [] && (List.mem (List.hd x) z && φ (List.tl x) y z)
            ==> φ x y z)

Split (let (_x_0 : bool) = subset x z in
       let (_x_1 : bool) = not (subset y z) in
       let (_x_2 : bool) = not (subset x y) in
       let (_x_3 : bool) = List.mem (List.hd x) z in
       let (_x_4 : bool) = x <> [] in
       let (_x_5 : sko_ty_0 list) = List.tl x in
       (_x_0 || _x_1 || _x_2 || (_x_3 && _x_4))
       && (not
           (_x_4 && _x_3 && (subset _x_5 z || not (subset _x_5 y) || _x_1))
           || _x_0 || _x_1 || _x_2)
       :cases [not (subset y z) || not (subset x y) || subset x z
               || (List.mem (List.hd x) z && x <> []);
               let (_x_0 : sko_ty_0 list) = List.tl x in
               let (_x_1 : bool) = subset y z in
               not (x <> []) || not (List.mem (List.hd x) z)
               || not (subset _x_0 y && _x_1 ==> subset _x_0 z) || not _x_1
               || not (subset x y) || subset x z])

subproof
let (_x_0 : sko_ty_0 list) = List.tl x in let (_x_1 : bool) = subset y z in not (x <> []) || not (List.mem (List.hd x) z) || not (subset _x_0 y && _x_1 ==> subset _x_0 z) || not _x_1 || not (subset x y) || subset x z
- start[0.219s, "1.1"] let (_x_0 : sko_ty_0 list) = List.tl x in let (_x_1 : bool) = subset y z in not (x <> []) || not (List.mem (List.hd x) z) || not (subset _x_0 y && _x_1 ==> subset _x_0 z) || not _x_1 || not (subset x y) || subset x z
- simplify
  into:
  true
  expansions:
  [subset, subset, List.mem]
  rewrite_steps:
  mem_subset
  mem_subset
  mem_subset
  forward_chaining:
subproof
not (subset y z) || not (subset x y) || subset x z || (List.mem (List.hd x) z && x <> [])
- start[0.219s, "1.2"] not (subset y z) || not (subset x y) || subset x z || (List.mem (List.hd x) z && x <> [])
- simplify
  into:
  not (subset y z) || not (subset x y) || List.mem (List.hd x) z || not (x <> [])
  expansions:
  [subset, subset, subset]
  rewrite_steps:
  forward_chaining:
- simplify
  into:
  true
  expansions:
  List.mem
  rewrite_steps:
  mem_subset
  mem_subset
  forward_chaining:

digraph "proof" {
p_187 [label="Start (subset ( :var_0: ) ( :var_1: ) && subset ( :var_1: ) ( :var_2: )\l       ==\> subset ( :var_0: ) ( :var_2: ) :name \"Goal\" :time 0.298s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_187 -> p_185 [label=""];
subgraph cluster_186 {
  color=blue;
p_185 [label="Start (not (subset x y) \|\| not (subset y z) \|\| subset x z :name \"1\"\l       :time 0.298s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_185 -> p_184 [label=""];
p_184 [label="Induct ((functional ?),\l        :scheme (not (List.mem (List.hd x) z && x \<\> []) ==\> φ x y z)\l                && (x \<\> [] && (List.mem (List.hd x) z && φ (List.tl x) y z)\l                    ==\> φ x y z))",shape=box,style=filled,fontname="courier",fontsize=14];
p_184 -> p_183 [label=""];
p_183 [label="Split (let (_x_0 : bool) = subset x z in\l       let (_x_1 : bool) = not (subset y z) in\l       let (_x_2 : bool) = not (subset x y) in\l       let (_x_3 : bool) = List.mem (List.hd x) z in\l       let (_x_4 : bool) = x \<\> [] in\l       let (_x_5 : sko_ty_0 list) = List.tl x in\l       (_x_0 \|\| _x_1 \|\| _x_2 \|\| (_x_3 && _x_4))\l       && (not\l           (_x_4 && _x_3 && (subset _x_5 z \|\| not (subset _x_5 y) \|\| _x_1))\l           \|\| _x_0 \|\| _x_1 \|\| _x_2)\l       :cases [not (subset y z) \|\| not (subset x y) \|\| subset x z\l               \|\| (List.mem (List.hd x) z && x \<\> []);\l               let (_x_0 : sko_ty_0 list) = List.tl x in\l               let (_x_1 : bool) = subset y z in\l               not (x \<\> []) \|\| not (List.mem (List.hd x) z)\l               \|\| not (subset _x_0 y && _x_1 ==\> subset _x_0 z) \|\| not _x_1\l               \|\| not (subset x y) \|\| subset x z])",shape=box,style=filled,fontname="courier",fontsize=14];
p_183 -> p_177 [label=""];
subgraph cluster_178 {
  color=blue;
p_177 [label="Start (let (_x_0 : sko_ty_0 list) = List.tl x in\l       let (_x_1 : bool) = subset y z in\l       not (x \<\> []) \|\| not (List.mem (List.hd x) z)\l       \|\| not (subset _x_0 y && _x_1 ==\> subset _x_0 z) \|\| not _x_1\l       \|\| not (subset x y) \|\| subset x z :name \"1.1\" :time 0.219s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_177 -> p_176 [label=""];
p_176 [label="Simplify (true :expansions [subset; subset; List.mem]\l          :rw [mem_subset; mem_subset; mem_subset] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
}
p_183 -> p_181 [label=""];
subgraph cluster_182 {
  color=blue;
p_181 [label="Start (not (subset y z) \|\| not (subset x y) \|\| subset x z\l       \|\| (List.mem (List.hd x) z && x \<\> []) :name \"1.2\" :time 0.219s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_181 -> p_180 [label=""];
p_180 [label="Simplify (not (subset y z) \|\| not (subset x y) \|\| List.mem (List.hd x) z\l          \|\| not (x \<\> []) :expansions [subset; subset; subset] :rw [] \l          :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_180 -> p_179 [label=""];
p_179 [label="Simplify (true :expansions [List.mem] :rw [mem_subset; mem_subset] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
}

Permutative Restriction¶

The @@permutative annotation applies only to rewrite rules and is used to restrict the rule so that it will only apply if the instantiated rhs is lexicographically smaller than the matched lhs. This restriction can be particularly useful in order to break out of infinite rewrite loops while trying to "canonicalize" a form, for example distributing the "simplest" terms to the left.

Let's say we want to prove the commutativity of Peano_nat.plus and install it as a rewrite rule:

Try this!

In [9]:

#max_induct 2;;

lemma comm_plus x y =
  Peano_nat.(plus x y = plus y x)
 [@@auto] [@@rw] [@@permutative]

Out[9]:

val comm_plus : Peano_nat.t -> Peano_nat.t -> bool = <fun>
Goal:

Peano_nat.( = ) (Peano_nat.plus x y) (Peano_nat.plus y x).

1 nontautological subgoal.

Subgoal 1:

|---------------------------------------------------------------------------
 Peano_nat.plus x y = Peano_nat.plus y x


Must try induction.

The recursive terms in the conjecture suggest 2 inductions.

As we have backtracked, we break ties by purity.
We shall induct according to a scheme derived from Peano_nat.plus.

Induction scheme:

 (not Is_a(Peano_nat.S, x) ==> φ x y)
 && (Is_a(Peano_nat.S, x) && φ (Destruct(Peano_nat.S, 0, x)) y ==> φ x y).

2 nontautological subgoals.

Subgoal 1.2:

|---------------------------------------------------------------------------
 C0. Is_a(Peano_nat.S, x)
 C1. Peano_nat.plus x y = Peano_nat.plus y x

This simplifies, using the definition of Peano_nat.plus to:

Subgoal 1.2':

|---------------------------------------------------------------------------
 C0. Is_a(Peano_nat.S, x)
 C1. y = Peano_nat.plus y x


Must try induction.

We shall induct according to a scheme derived from Peano_nat.plus.

Induction scheme:

 (not Is_a(Peano_nat.S, y) ==> φ x y)
 && (Is_a(Peano_nat.S, y) && φ x (Destruct(Peano_nat.S, 0, y)) ==> φ x y).

2 nontautological subgoals.

Subgoal 1.2'.2:

|---------------------------------------------------------------------------
 C0. y = Peano_nat.plus y x
 C1. Is_a(Peano_nat.S, x)
 C2. Is_a(Peano_nat.S, y)

But simplification reduces this to true, using the definition of
Peano_nat.plus.

Subgoal 1.2'.1:

 H0. Is_a(Peano_nat.S, y)
 H1. Is_a(Peano_nat.S, x)
     || (Destruct(Peano_nat.S, 0, y)
         = Peano_nat.plus (Destruct(Peano_nat.S, 0, y)) x)
|---------------------------------------------------------------------------
 C0. y = Peano_nat.plus y x
 C1. Is_a(Peano_nat.S, x)

But simplification reduces this to true, using the definition of
Peano_nat.plus.

Subgoal 1.1:

 H0. Is_a(Peano_nat.S, x)
 H1. Peano_nat.plus (Destruct(Peano_nat.S, 0, x)) y
     = Peano_nat.plus y (Destruct(Peano_nat.S, 0, x))
|---------------------------------------------------------------------------
 Peano_nat.plus x y = Peano_nat.plus y x

This simplifies, using the definition of Peano_nat.plus to:

Subgoal 1.1':

 H0. Is_a(Peano_nat.S, x)
 H1. Peano_nat.plus (Destruct(Peano_nat.S, 0, x)) y
     = Peano_nat.plus y (Destruct(Peano_nat.S, 0, x))
|---------------------------------------------------------------------------
 Peano_nat.S (Peano_nat.plus (Destruct(Peano_nat.S, 0, x)) y)
 = Peano_nat.plus y x


We can eliminate destructors by the following
substitution:
 x -> Peano_nat.S x1

This produces the modified subgoal:

Subgoal 1.1'':

 H0. Peano_nat.plus x1 y = Peano_nat.plus y x1
|---------------------------------------------------------------------------
 Peano_nat.S (Peano_nat.plus x1 y) = Peano_nat.plus y (Peano_nat.S x1)


Cross-fertilizing with:

 Peano_nat.plus x1 y = Peano_nat.plus y x1

This produces the modified subgoal:

Subgoal 1.1''':

|---------------------------------------------------------------------------
 Peano_nat.S (Peano_nat.plus y x1) = Peano_nat.plus y (Peano_nat.S x1)


Must try induction.

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

We shall induct according to a scheme derived from Peano_nat.plus.

Induction scheme:

 (not Is_a(Peano_nat.S, y) ==> φ x1 y)
 && (Is_a(Peano_nat.S, y) && φ x1 (Destruct(Peano_nat.S, 0, y)) ==> φ x1 y).

2 nontautological subgoals.

Subgoal 1.1'''.2:

|---------------------------------------------------------------------------
 C0. Is_a(Peano_nat.S, y)
 C1. Peano_nat.S (Peano_nat.plus y x1) = Peano_nat.plus y (Peano_nat.S x1)

But simplification reduces this to true, using the definition of
Peano_nat.plus.

Subgoal 1.1'''.1:

 H0. Is_a(Peano_nat.S, y)
 H1. Peano_nat.S (Peano_nat.plus (Destruct(Peano_nat.S, 0, y)) x1)
     = Peano_nat.plus (Destruct(Peano_nat.S, 0, y)) (Peano_nat.S x1)
|---------------------------------------------------------------------------
 Peano_nat.S (Peano_nat.plus y x1) = Peano_nat.plus y (Peano_nat.S x1)

But simplification reduces this to true, using the definition of
Peano_nat.plus.

 ⓘ  Rules:
    (:def Peano_nat.plus)
    (:induct Peano_nat.plus)

Proved

proof

ground_instances:	0
definitions:	8
inductions:	3
search_time:	0.415s

Expand

start[0.415s, "Goal"]
  Peano_nat.plus ( :var_0: ) ( :var_1: )
  = Peano_nat.plus ( :var_1: ) ( :var_0: )

subproof

Peano_nat.plus x y = Peano_nat.plus y x

start[0.415s, "1"] Peano_nat.plus x y = Peano_nat.plus y x

induction on (functional ?)
:scheme (not Is_a(Peano_nat.S, x) ==> φ x y)
        && (Is_a(Peano_nat.S, x) && φ (Destruct(Peano_nat.S, 0, x)) y
            ==> φ x y)

Split (let (_x_0 : bool) = Is_a(Peano_nat.S, x) in
       let (_x_1 : bool) = Peano_nat.plus x y = Peano_nat.plus y x in
       let (_x_2 : Peano_nat.t) = Destruct(Peano_nat.S, 0, x) in
       (_x_0 || _x_1)
       && (not (_x_0 && (Peano_nat.plus _x_2 y = Peano_nat.plus y _x_2))
           || _x_1)
       :cases [Is_a(Peano_nat.S, x)
               || (Peano_nat.plus x y = Peano_nat.plus y x);
               let (_x_0 : Peano_nat.t) = Destruct(Peano_nat.S, 0, x) in
               not Is_a(Peano_nat.S, x)
               || not (Peano_nat.plus _x_0 y = Peano_nat.plus y _x_0)
               || (Peano_nat.plus x y = Peano_nat.plus y x)])

subproof

let (_x_0 : Peano_nat.t) = Destruct(Peano_nat.S, 0, x) in not Is_a(Peano_nat.S, x) || not (Peano_nat.plus _x_0 y = Peano_nat.plus y _x_0) || (Peano_nat.plus x y = Peano_nat.plus y x)

start[0.378s, "1.1"]
  let (_x_0 : Peano_nat.t) = Destruct(Peano_nat.S, 0, x) in
  not Is_a(Peano_nat.S, x)
  || not (Peano_nat.plus _x_0 y = Peano_nat.plus y _x_0)
  || (Peano_nat.plus x y = Peano_nat.plus y x)

simplify

into:	let (_x_0 : Peano_nat.t) = Destruct(Peano_nat.S, 0, x) in let (_x_1 : Peano_nat.t) = Peano_nat.plus _x_0 y in not Is_a(Peano_nat.S, x) \|\| not (_x_1 = Peano_nat.plus y _x_0) \|\| (Peano_nat.S _x_1 = Peano_nat.plus y x)
expansions:	Peano_nat.plus
rewrite_steps:
forward_chaining:

Elim_destructor (:cstor Peano_nat.S :replace Peano_nat.S x1 :context [])

induction on (functional ?)
:scheme (not Is_a(Peano_nat.S, y) ==> φ x1 y)
        && (Is_a(Peano_nat.S, y) && φ x1 (Destruct(Peano_nat.S, 0, y))
            ==> φ x1 y)

Split (let (_x_0 : bool) = Is_a(Peano_nat.S, y) in
       let (_x_1 : Peano_nat.t) = Peano_nat.S x1 in
       let (_x_2 : bool)
           = Peano_nat.S (Peano_nat.plus y x1) = Peano_nat.plus y _x_1
       in
       let (_x_3 : Peano_nat.t) = Destruct(Peano_nat.S, 0, y) in
       (_x_0 || _x_2)
       && (not
           (_x_0
            && (Peano_nat.S (Peano_nat.plus _x_3 x1)
                = Peano_nat.plus _x_3 _x_1))
           || _x_2)
       :cases [Is_a(Peano_nat.S, y)
               || (Peano_nat.S (Peano_nat.plus y x1)
                   = Peano_nat.plus y (Peano_nat.S x1));
               let (_x_0 : Peano_nat.t) = Destruct(Peano_nat.S, 0, y) in
               let (_x_1 : Peano_nat.t) = Peano_nat.S x1 in
               not Is_a(Peano_nat.S, y)
               || not
                  (Peano_nat.S (Peano_nat.plus _x_0 x1)
                   = Peano_nat.plus _x_0 _x_1)
               || (Peano_nat.S (Peano_nat.plus y x1) = Peano_nat.plus y _x_1)])

```
Subproof
```
```
Subproof
```

subproof

Is_a(Peano_nat.S, x) || (Peano_nat.plus x y = Peano_nat.plus y x)

start[0.378s, "1.2"]
  Is_a(Peano_nat.S, x) || (Peano_nat.plus x y = Peano_nat.plus y x)

simplify

into:	Is_a(Peano_nat.S, x) \|\| (y = Peano_nat.plus y x)
expansions:	Peano_nat.plus
rewrite_steps:
forward_chaining:

induction on (functional ?)
:scheme (not Is_a(Peano_nat.S, y) ==> φ x y)
        && (Is_a(Peano_nat.S, y) && φ x (Destruct(Peano_nat.S, 0, y))
            ==> φ x y)

Split (let (_x_0 : bool) = Is_a(Peano_nat.S, x) in
       let (_x_1 : bool) = (y = Peano_nat.plus y x) || _x_0 in
       let (_x_2 : bool) = Is_a(Peano_nat.S, y) in
       let (_x_3 : Peano_nat.t) = Destruct(Peano_nat.S, 0, y) in
       (_x_1 || _x_2)
       && (_x_1 || not (_x_2 && (_x_0 || (_x_3 = Peano_nat.plus _x_3 x))))
       :cases [(y = Peano_nat.plus y x) || Is_a(Peano_nat.S, x)
               || Is_a(Peano_nat.S, y);
               let (_x_0 : bool) = Is_a(Peano_nat.S, x) in
               let (_x_1 : Peano_nat.t) = Destruct(Peano_nat.S, 0, y) in
               not Is_a(Peano_nat.S, y)
               || not (_x_0 || (_x_1 = Peano_nat.plus _x_1 x))
               || (y = Peano_nat.plus y x) || _x_0])

```
Subproof
```
```
Subproof
```

digraph "proof" {
p_261 [label="Start (Peano_nat.plus ( :var_0: ) ( :var_1: )\l       = Peano_nat.plus ( :var_1: ) ( :var_0: ) :name \"Goal\" :time 0.415s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_261 -> p_259 [label=""];
subgraph cluster_260 {
  color=blue;
p_259 [label="Start (Peano_nat.plus x y = Peano_nat.plus y x :name \"1\" :time 0.415s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_259 -> p_258 [label=""];
p_258 [label="Induct ((functional ?),\l        :scheme (not Is_a(Peano_nat.S, x) ==\> φ x y)\l                && (Is_a(Peano_nat.S, x)\l                    && φ (Destruct(Peano_nat.S, 0, x)) y ==\> φ x y))",shape=box,style=filled,fontname="courier",fontsize=14];
p_258 -> p_257 [label=""];
p_257 [label="Split (let (_x_0 : bool) = Is_a(Peano_nat.S, x) in\l       let (_x_1 : bool) = Peano_nat.plus x y = Peano_nat.plus y x in\l       let (_x_2 : Peano_nat.t) = Destruct(Peano_nat.S, 0, x) in\l       (_x_0 \|\| _x_1)\l       && (not (_x_0 && (Peano_nat.plus _x_2 y = Peano_nat.plus y _x_2))\l           \|\| _x_1)\l       :cases [Is_a(Peano_nat.S, x)\l               \|\| (Peano_nat.plus x y = Peano_nat.plus y x);\l               let (_x_0 : Peano_nat.t) = Destruct(Peano_nat.S, 0, x) in\l               not Is_a(Peano_nat.S, x)\l               \|\| not (Peano_nat.plus _x_0 y = Peano_nat.plus y _x_0)\l               \|\| (Peano_nat.plus x y = Peano_nat.plus y x)])",shape=box,style=filled,fontname="courier",fontsize=14];
p_257 -> p_244 [label=""];
subgraph cluster_245 {
  color=blue;
p_244 [label="Start (let (_x_0 : Peano_nat.t) = Destruct(Peano_nat.S, 0, x) in\l       not Is_a(Peano_nat.S, x)\l       \|\| not (Peano_nat.plus _x_0 y = Peano_nat.plus y _x_0)\l       \|\| (Peano_nat.plus x y = Peano_nat.plus y x) :name \"1.1\" :time 0.378s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_244 -> p_243 [label=""];
p_243 [label="Simplify (let (_x_0 : Peano_nat.t) = Destruct(Peano_nat.S, 0, x) in\l          let (_x_1 : Peano_nat.t) = Peano_nat.plus _x_0 y in\l          not Is_a(Peano_nat.S, x) \|\| not (_x_1 = Peano_nat.plus y _x_0)\l          \|\| (Peano_nat.S _x_1 = Peano_nat.plus y x)\l          :expansions [Peano_nat.plus] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_243 -> p_242 [label=""];
p_242 [label="Elim_destructor (:cstor Peano_nat.S :replace Peano_nat.S x1 :context [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_242 -> p_241 [label=""];
p_241 [label="Induct ((functional ?),\l        :scheme (not Is_a(Peano_nat.S, y) ==\> φ x1 y)\l                && (Is_a(Peano_nat.S, y)\l                    && φ x1 (Destruct(Peano_nat.S, 0, y)) ==\> φ x1 y))",shape=box,style=filled,fontname="courier",fontsize=14];
p_241 -> p_240 [label=""];
p_240 [label="Split (let (_x_0 : bool) = Is_a(Peano_nat.S, y) in\l       let (_x_1 : Peano_nat.t) = Peano_nat.S x1 in\l       let (_x_2 : bool)\l           = Peano_nat.S (Peano_nat.plus y x1) = Peano_nat.plus y _x_1\l       in\l       let (_x_3 : Peano_nat.t) = Destruct(Peano_nat.S, 0, y) in\l       (_x_0 \|\| _x_2)\l       && (not\l           (_x_0\l            && (Peano_nat.S (Peano_nat.plus _x_3 x1)\l                = Peano_nat.plus _x_3 _x_1))\l           \|\| _x_2)\l       :cases [Is_a(Peano_nat.S, y)\l               \|\| (Peano_nat.S (Peano_nat.plus y x1)\l                   = Peano_nat.plus y (Peano_nat.S x1));\l               let (_x_0 : Peano_nat.t) = Destruct(Peano_nat.S, 0, y) in\l               let (_x_1 : Peano_nat.t) = Peano_nat.S x1 in\l               not Is_a(Peano_nat.S, y)\l               \|\| not\l                  (Peano_nat.S (Peano_nat.plus _x_0 x1)\l                   = Peano_nat.plus _x_0 _x_1)\l               \|\| (Peano_nat.S (Peano_nat.plus y x1) = Peano_nat.plus y _x_1)])",shape=box,style=filled,fontname="courier",fontsize=14];
p_240 -> p_235 [label=""];
subgraph cluster_236 {
  color=blue;
p_235 [label="Start (let (_x_0 : Peano_nat.t) = Destruct(Peano_nat.S, 0, y) in\l       let (_x_1 : Peano_nat.t) = Peano_nat.S x1 in\l       not Is_a(Peano_nat.S, y)\l       \|\| not\l          (Peano_nat.S (Peano_nat.plus _x_0 x1) = Peano_nat.plus _x_0 _x_1)\l       \|\| (Peano_nat.S (Peano_nat.plus y x1) = Peano_nat.plus y _x_1)\l       :name \"1.1'''.1\" :time 0.016s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_235 -> p_234 [label=""];
p_234 [label="Simplify (true :expansions [Peano_nat.plus; Peano_nat.plus] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
}
p_240 -> p_238 [label=""];
subgraph cluster_239 {
  color=blue;
p_238 [label="Start (Is_a(Peano_nat.S, y)\l       \|\| (Peano_nat.S (Peano_nat.plus y x1)\l           = Peano_nat.plus y (Peano_nat.S x1))\l       :name \"1.1'''.2\" :time 0.016s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_238 -> p_237 [label=""];
p_237 [label="Simplify (true :expansions [Peano_nat.plus; Peano_nat.plus] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
p_257 -> p_255 [label=""];
subgraph cluster_256 {
  color=blue;
p_255 [label="Start (Is_a(Peano_nat.S, x) \|\| (Peano_nat.plus x y = Peano_nat.plus y x)\l       :name \"1.2\" :time 0.378s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_255 -> p_254 [label=""];
p_254 [label="Simplify (Is_a(Peano_nat.S, x) \|\| (y = Peano_nat.plus y x)\l          :expansions [Peano_nat.plus] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_254 -> p_253 [label=""];
p_253 [label="Induct ((functional ?),\l        :scheme (not Is_a(Peano_nat.S, y) ==\> φ x y)\l                && (Is_a(Peano_nat.S, y)\l                    && φ x (Destruct(Peano_nat.S, 0, y)) ==\> φ x y))",shape=box,style=filled,fontname="courier",fontsize=14];
p_253 -> p_252 [label=""];
p_252 [label="Split (let (_x_0 : bool) = Is_a(Peano_nat.S, x) in\l       let (_x_1 : bool) = (y = Peano_nat.plus y x) \|\| _x_0 in\l       let (_x_2 : bool) = Is_a(Peano_nat.S, y) in\l       let (_x_3 : Peano_nat.t) = Destruct(Peano_nat.S, 0, y) in\l       (_x_1 \|\| _x_2)\l       && (_x_1 \|\| not (_x_2 && (_x_0 \|\| (_x_3 = Peano_nat.plus _x_3 x))))\l       :cases [(y = Peano_nat.plus y x) \|\| Is_a(Peano_nat.S, x)\l               \|\| Is_a(Peano_nat.S, y);\l               let (_x_0 : bool) = Is_a(Peano_nat.S, x) in\l               let (_x_1 : Peano_nat.t) = Destruct(Peano_nat.S, 0, y) in\l               not Is_a(Peano_nat.S, y)\l               \|\| not (_x_0 \|\| (_x_1 = Peano_nat.plus _x_1 x))\l               \|\| (y = Peano_nat.plus y x) \|\| _x_0])",shape=box,style=filled,fontname="courier",fontsize=14];
p_252 -> p_247 [label=""];
subgraph cluster_248 {
  color=blue;
p_247 [label="Start (let (_x_0 : bool) = Is_a(Peano_nat.S, x) in\l       let (_x_1 : Peano_nat.t) = Destruct(Peano_nat.S, 0, y) in\l       not Is_a(Peano_nat.S, y)\l       \|\| not (_x_0 \|\| (_x_1 = Peano_nat.plus _x_1 x))\l       \|\| (y = Peano_nat.plus y x) \|\| _x_0 :name \"1.2'.1\" :time 0.296s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_247 -> p_246 [label=""];
p_246 [label="Simplify (true :expansions [Peano_nat.plus] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
}
p_252 -> p_250 [label=""];
subgraph cluster_251 {
  color=blue;
p_250 [label="Start ((y = Peano_nat.plus y x) \|\| Is_a(Peano_nat.S, x)\l       \|\| Is_a(Peano_nat.S, y) :name \"1.2'.2\" :time 0.296s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_250 -> p_249 [label=""];
p_249 [label="Simplify (true :expansions [Peano_nat.plus] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
}
}

Had we not restricted comm_plus as a permutative rule, the simplifier would have entered a rewrite loop every time it encountered a term matching plus <x> <y>, while with the permutative restriction in place, this has the effect of directing all the "simplest" terms to the left of plus, which will help with making further rewrite rules applicable and with simplification in general.

Forward-chaining Rules¶

Forward chaining is the second type of rule that Imandra allows us to register and participate automatically in proofs.

A forward chaining rule is a theorem containing a collection of trigger terms which must include all free variables of the theorem. If Imandra can appropriately match the triggers with terms in the goal, then an instantiation of the rule is added to the context. The context of a goal is not displayed in the goal itself (i.e., when the goal is printed), but is rather used in the background to aid the simplifier in closing branches, relieving hypotheses of rewrite rules during backchaining, and so on.

For example, let us prove the following theorem and install it as a forward-chaining rule:

Try this!

In [10]:

lemma len_nonnegative x =
  List.length x [@trigger] >= 0
[@@simp] [@@fc]

Out[10]:

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

Proved

proof
call graph

proof

ground_instances:

definitions:

inductions:

search_time:

0.031s

details:

Expand

smt_stats:

rlimit count:	514
time:	0.008000
memory:	19.070000
max memory:	20.200000
num allocs:	10654537835.000000

Expand

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

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

Now when Imandra encounters a term of the form List.length <term>, the formula List.length <term> >= 0 will be added to the context of the goal under focus. In other words, a forward chaining rule allows Imandra to extend the database of background logical facts it knows about a goal. These facts are made available to the simplifier, and can thus be used to enhance simplification by closing branches and relieving hypotheses of conditional rewrite rules.

A forward chaining rule can contain multiple disjoint triggers. In this case, if either of the triggers matches, the forward chaining rule fires. For example, the following forward chaining version of the rev_len rewrite rule we added above will fire if either List.length x or List.length (List.rev x) matches.

Try this!

In [11]:

lemma rev_len_fc x =
   List.length x [@trigger] = List.length (List.rev x) [@trigger]
[@@auto] [@@fc]

Out[11]:

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

List.length x = List.length (List.rev x).

1 nontautological subgoal.

Subgoal 1:

|---------------------------------------------------------------------------
 List.length x = List.length (List.rev x)

But simplification reduces this to true, using the rewrite rule rev_len.

 ⓘ  Rules:
    (:rw rev_len)
    (:fc List.len_nonnegative)
    (:fc len_nonnegative)

Proved

proof

ground_instances:	0
definitions:	0
inductions:	0
search_time:	0.015s

Expand

start[0.015s, "Goal"]
  List.length ( :var_0: ) = List.length (List.rev ( :var_0: ))

subproof
List.length x = List.length (List.rev x)
- start[0.015s, "1"] List.length x = List.length (List.rev x)
- simplify
  into:
  true
  expansions:
  []
  rewrite_steps:
  rev_len
  forward_chaining:
  List.len_nonnegative
  len_nonnegative
  List.len_nonnegative
  len_nonnegative

Additionally, a forward chaining rule can contain multiple conjoined triggers, forming a trigger cluster. In this case, all the triggers must match in order for the forward chaining rule to apply.

To create a trigger cluster multiple terms must be annotated with [@trigger <x>i], where <x> is a numeric identifier common to all the triggers in the cluster. For example:

Try this!

In [12]:

theorem subset_trans l1 l2 l3 =
  (subset l1 l2 [@trigger 0i]) && (subset l2 l3 [@trigger 0i])
  ==>
  subset l1 l3
 [@@auto] [@@forward_chaining]

Out[12]:

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

subset l1 l2 && subset l2 l3 ==> subset l1 l3.

1 nontautological subgoal.

Subgoal 1:

 H0. subset l1 l2
 H1. subset l2 l3
|---------------------------------------------------------------------------
 subset l1 l3


Must try induction.

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

However, scheme scoring gives us a clear winner.
We shall induct according to a scheme derived from subset.

Induction scheme:

 (not (List.mem (List.hd l1) l3 && l1 <> []) ==> φ l1 l2 l3)
 && (l1 <> [] && (List.mem (List.hd l1) l3 && φ (List.tl l1) l2 l3)
     ==> φ l1 l2 l3).

2 nontautological subgoals.

Subgoal 1.2:

 H0. subset l2 l3
 H1. subset l1 l2
|---------------------------------------------------------------------------
 C0. subset l1 l3
 C1. List.mem (List.hd l1) l3 && l1 <> []

This simplifies, using the definition of subset to:

Subgoal 1.2':

 H0. subset l2 l3
 H1. subset l1 l2
 H2. l1 <> []
|---------------------------------------------------------------------------
 List.mem (List.hd l1) l3

But simplification reduces this to true, using the definition of List.mem,
and the rewrite rule mem_subset.

Subgoal 1.1:

 H0. l1 <> []
 H1. List.mem (List.hd l1) l3
 H2. subset (List.tl l1) l2 && subset l2 l3 ==> subset (List.tl l1) l3
 H3. subset l2 l3
 H4. subset l1 l2
|---------------------------------------------------------------------------
 subset l1 l3

But simplification reduces this to true, using the definitions of List.mem
and subset, and the rewrite rule mem_subset.

 ⓘ  Rules:
    (:def List.mem)
    (:def subset)
    (:rw mem_subset)
    (:induct subset)

Proved

proof

ground_instances:	0
definitions:	9
inductions:	1
search_time:	0.378s

Expand

start[0.378s, "Goal"]
  subset ( :var_0: ) ( :var_1: ) && subset ( :var_1: ) ( :var_2: )
  ==> subset ( :var_0: ) ( :var_2: )

subproof

not (subset l1 l2) || not (subset l2 l3) || subset l1 l3

start[0.378s, "1"] not (subset l1 l2) || not (subset l2 l3) || subset l1 l3

induction on (functional ?)
:scheme (not (List.mem (List.hd l1) l3 && l1 <> []) ==> φ l1 l2 l3)
        && (l1 <> [] && (List.mem (List.hd l1) l3 && φ (List.tl l1) l2 l3)
            ==> φ l1 l2 l3)

Split (let (_x_0 : bool) = subset l1 l3 in
       let (_x_1 : bool) = not (subset l2 l3) in
       let (_x_2 : bool) = not (subset l1 l2) in
       let (_x_3 : bool) = List.mem (List.hd l1) l3 in
       let (_x_4 : bool) = l1 <> [] in
       let (_x_5 : sko_ty_0 list) = List.tl l1 in
       (_x_0 || _x_1 || _x_2 || (_x_3 && _x_4))
       && (not
           (_x_4 && _x_3 && (subset _x_5 l3 || not (subset _x_5 l2) || _x_1))
           || _x_0 || _x_1 || _x_2)
       :cases [not (subset l2 l3) || not (subset l1 l2) || subset l1 l3
               || (List.mem (List.hd l1) l3 && l1 <> []);
               let (_x_0 : sko_ty_0 list) = List.tl l1 in
               let (_x_1 : bool) = subset l2 l3 in
               not (l1 <> []) || not (List.mem (List.hd l1) l3)
               || not (subset _x_0 l2 && _x_1 ==> subset _x_0 l3) || 
               not _x_1 || not (subset l1 l2) || subset l1 l3])

subproof
let (_x_0 : sko_ty_0 list) = List.tl l1 in let (_x_1 : bool) = subset l2 l3 in not (l1 <> []) || not (List.mem (List.hd l1) l3) || not (subset _x_0 l2 && _x_1 ==> subset _x_0 l3) || not _x_1 || not (subset l1 l2) || subset l1 l3
- start[0.303s, "1.1"] let (_x_0 : sko_ty_0 list) = List.tl l1 in let (_x_1 : bool) = subset l2 l3 in not (l1 <> []) || not (List.mem (List.hd l1) l3) || not (subset _x_0 l2 && _x_1 ==> subset _x_0 l3) || not _x_1 || not (subset l1 l2) || subset l1 l3
- simplify
  into:
  true
  expansions:
  [subset, List.mem, subset, subset, List.mem]
  rewrite_steps:
  mem_subset
  mem_subset
  mem_subset
  mem_subset
  mem_subset
  forward_chaining:
subproof
not (subset l2 l3) || not (subset l1 l2) || subset l1 l3 || (List.mem (List.hd l1) l3 && l1 <> [])
- start[0.303s, "1.2"] not (subset l2 l3) || not (subset l1 l2) || subset l1 l3 || (List.mem (List.hd l1) l3 && l1 <> [])
- simplify
  into:
  not (subset l2 l3) || not (subset l1 l2) || List.mem (List.hd l1) l3 || not (l1 <> [])
  expansions:
  [subset, subset, subset]
  rewrite_steps:
  forward_chaining:
- simplify
  into:
  true
  expansions:
  List.mem
  rewrite_steps:
  mem_subset
  mem_subset
  forward_chaining:

digraph "proof" {
p_290 [label="Start (subset ( :var_0: ) ( :var_1: ) && subset ( :var_1: ) ( :var_2: )\l       ==\> subset ( :var_0: ) ( :var_2: ) :name \"Goal\" :time 0.378s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_290 -> p_288 [label=""];
subgraph cluster_289 {
  color=blue;
p_288 [label="Start (not (subset l1 l2) \|\| not (subset l2 l3) \|\| subset l1 l3 :name \"1\"\l       :time 0.378s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_288 -> p_287 [label=""];
p_287 [label="Induct ((functional ?),\l        :scheme (not (List.mem (List.hd l1) l3 && l1 \<\> []) ==\> φ l1 l2 l3)\l                && (l1 \<\> []\l                    && (List.mem (List.hd l1) l3 && φ (List.tl l1) l2 l3)\l                    ==\> φ l1 l2 l3))",shape=box,style=filled,fontname="courier",fontsize=14];
p_287 -> p_286 [label=""];
p_286 [label="Split (let (_x_0 : bool) = subset l1 l3 in\l       let (_x_1 : bool) = not (subset l2 l3) in\l       let (_x_2 : bool) = not (subset l1 l2) in\l       let (_x_3 : bool) = List.mem (List.hd l1) l3 in\l       let (_x_4 : bool) = l1 \<\> [] in\l       let (_x_5 : sko_ty_0 list) = List.tl l1 in\l       (_x_0 \|\| _x_1 \|\| _x_2 \|\| (_x_3 && _x_4))\l       && (not\l           (_x_4 && _x_3 && (subset _x_5 l3 \|\| not (subset _x_5 l2) \|\| _x_1))\l           \|\| _x_0 \|\| _x_1 \|\| _x_2)\l       :cases [not (subset l2 l3) \|\| not (subset l1 l2) \|\| subset l1 l3\l               \|\| (List.mem (List.hd l1) l3 && l1 \<\> []);\l               let (_x_0 : sko_ty_0 list) = List.tl l1 in\l               let (_x_1 : bool) = subset l2 l3 in\l               not (l1 \<\> []) \|\| not (List.mem (List.hd l1) l3)\l               \|\| not (subset _x_0 l2 && _x_1 ==\> subset _x_0 l3) \|\| \l               not _x_1 \|\| not (subset l1 l2) \|\| subset l1 l3])",shape=box,style=filled,fontname="courier",fontsize=14];
p_286 -> p_280 [label=""];
subgraph cluster_281 {
  color=blue;
p_280 [label="Start (let (_x_0 : sko_ty_0 list) = List.tl l1 in\l       let (_x_1 : bool) = subset l2 l3 in\l       not (l1 \<\> []) \|\| not (List.mem (List.hd l1) l3)\l       \|\| not (subset _x_0 l2 && _x_1 ==\> subset _x_0 l3) \|\| not _x_1\l       \|\| not (subset l1 l2) \|\| subset l1 l3 :name \"1.1\" :time 0.303s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_280 -> p_279 [label=""];
p_279 [label="Simplify (true :expansions [subset; List.mem; subset; subset; List.mem]\l          :rw [mem_subset; mem_subset; mem_subset; mem_subset; mem_subset]\l          :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
}
p_286 -> p_284 [label=""];
subgraph cluster_285 {
  color=blue;
p_284 [label="Start (not (subset l2 l3) \|\| not (subset l1 l2) \|\| subset l1 l3\l       \|\| (List.mem (List.hd l1) l3 && l1 \<\> []) :name \"1.2\" :time 0.303s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_284 -> p_283 [label=""];
p_283 [label="Simplify (not (subset l2 l3) \|\| not (subset l1 l2)\l          \|\| List.mem (List.hd l1) l3 \|\| not (l1 \<\> [])\l          :expansions [subset; subset; subset] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_283 -> p_282 [label=""];
p_282 [label="Simplify (true :expansions [List.mem] :rw [mem_subset; mem_subset] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
}

This forward chaining rule will match only if a goal contains terms that match both subset l1 l2 and subset l2 l3.

It should be noted that Imandra supports automatic trigger selection, meaning it's often not necessary to annotate the trigger terms manually. Imandra can typically infer for us both simple triggers and trigger clusters. In fact for both the single trigger examples above, we could have omitted the trigger annotations altogether, and Imandra would have found some for us automatically.

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

into:	not (subset y z) \|\| not (subset x y) \|\| List.mem (List.hd x) z \|\| not (x <> [])
expansions:	[subset, subset, subset]
rewrite_steps:
forward_chaining:

into:	not (subset l2 l3) \|\| not (subset l1 l2) \|\| List.mem (List.hd l1) l3 \|\| not (l1 <> [])
expansions:	[subset, subset, subset]
rewrite_steps:
forward_chaining: