Induction¶

While techniques such as unrolling and simplification can get us a long way towards formally verifying our software, variants of mathematical induction are in general required for verifying properties of systems with infinite state-spaces.

Induction is a proof technique that can be used to prove that some property φ(x) holds for all the elements x of a recursively defined structure (e.g. natural numbers, lists, trees, execution traces, etc). The proof consists of:

a proof that φ(base) is true for each base case
a proof that if φ(c) is true (called the inductive hypothesis), then φ(step(c)) is also true, for all the recursive steps of the property we're trying to prove

Induction can be done in many ways, and finding the "right" way to induct is often the key to difficult problems. Imandra has deep automation for finding and applying the "right" induction for a problem. If this fails, the user can instruct Imandra how to induct, with various forms of instructions.

A method of induction is given by an induction scheme.

Induction schemes can automatically be derived by Imandra in many ways. By default, with [@@auto] or [@@induct], Imandra analyses the recursive functions involved in the conjecture and constructs a functional induction scheme derived from their recursive structure, in a manner that is justified by the ordinal measures used to prove their termination. Imandra also supports structural induction principles derived from the definitions of (well-founded) algebraic datatypes such as lists and trees.

Some example induction schemes are:

for the natural numbers, φ(Zero) && φ(n) ==> φ(Succ(n))
for lists, φ([]) && (lst <> [] && φ(List.tl(lst)) ==> φ (lst))
for the function repeat as defined below, n <= 0 ==> φ(n, c) && (n > 0 && φ(n - 1, c)) ==> φ(n, c)

Try this!

In [1]:

let rec repeat c n =
  if n <= 0 then
    []
  else
    c :: (repeat c (n-1))

Out[1]:

val repeat : 'a -> Z.t -> 'a list = <fun>

termination proof

Termination proof

call `repeat c (n - 1)` from `repeat c n`

original:

repeat c n

sub:

repeat c (n - 1)

original ordinal:

Ordinal.Int (_cnt n)

sub ordinal:

Ordinal.Int (_cnt (n - 1))

path:

[not (n <= 0)]

proof:

detailed proof

summary
full

ground_instances:

definitions:

inductions:

search_time:

0.014s

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:	1099
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:	5374254
final checks:	1
added eqs:	4
del clause:	5
arith eq adapter:	2
memory:	15.200000
max memory:	15.200000

Expand

start[0.014s]
  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
  not (n <= 0) && ((_x_0 >= 0) && (_x_2 >= 0))
  ==> (_x_1 <= 0) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)

simplify

into:	(n <= 0) \|\| (n <= 1) \|\| 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_381/server 1) (+ (- 1) n_381/server)…
expansions:

Unsat

In Imandra, induction schemes are "destructor style." So, an actual scheme Imandra would produce for a goal involving n : nat (where type nat = Zero | Succ of nat) is:

 (n = Zero ==> φ n)
 && (not (n = Zero) && φ (Destruct(Succ, 0, n)) ==> φ n).

Let us see a few example inductions.

Try this!

In [2]:

lemma assoc_append x y z =
 x @ (y @ z) = (x @ y) @ z [@@auto] [@@rw]

Out[2]:

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

x @ (y @ z) = x @ y @ z.

1 nontautological subgoal.

Subgoal 1:

|---------------------------------------------------------------------------
 List.append x (List.append y z) = List.append (List.append x y) 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 List.append.

Induction scheme:

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

2 nontautological subgoals.

Subgoal 1.2:

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

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

Subgoal 1.1:

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

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

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

Proved

proof

ground_instances:	0
definitions:	5
inductions:	1
search_time:	0.073s

Expand

start[0.073s, "Goal"]
  List.append ( :var_0: ) (List.append ( :var_1: ) ( :var_2: ))
  = List.append (List.append ( :var_0: ) ( :var_1: )) ( :var_2: )

subproof

List.append x (List.append y z) = List.append (List.append x y) z

start[0.073s, "1"]
  List.append x (List.append y z) = List.append (List.append x y) z

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

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

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

digraph "proof" {
p_23 [label="Start (List.append ( :var_0: ) (List.append ( :var_1: ) ( :var_2: ))\l       = List.append (List.append ( :var_0: ) ( :var_1: )) ( :var_2: )\l       :name \"Goal\" :time 0.073s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_23 -> p_21 [label=""];
subgraph cluster_22 {
  color=blue;
p_21 [label="Start (List.append x (List.append y z) = List.append (List.append x y) z\l       :name \"1\" :time 0.073s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_21 -> p_20 [label=""];
p_20 [label="Induct ((functional ?),\l        :scheme (not (x \<\> []) ==\> φ x y z)\l                && (x \<\> [] && φ (List.tl x) y z ==\> φ x y z))",shape=box,style=filled,fontname="courier",fontsize=14];
p_20 -> p_19 [label=""];
p_19 [label="Split (let (_x_0 : bool) = x \<\> [] in\l       let (_x_1 : sko_ty_0 list) = List.append y z in\l       let (_x_2 : bool)\l           = List.append x _x_1 = List.append (List.append x y) z\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.append _x_3 _x_1 = List.append (List.append _x_3 y) z))\l           \|\| _x_2)\l       :cases [x \<\> []\l               \|\| (List.append x (List.append y z)\l                   = List.append (List.append x y) z);\l               let (_x_0 : sko_ty_0 list) = List.tl x in\l               let (_x_1 : sko_ty_0 list) = List.append y z in\l               not (x \<\> [])\l               \|\| not\l                  (List.append _x_0 _x_1 = List.append (List.append _x_0 y) z)\l               \|\| (List.append x _x_1 = List.append (List.append x y) z)])",shape=box,style=filled,fontname="courier",fontsize=14];
p_19 -> p_14 [label=""];
subgraph cluster_15 {
  color=blue;
p_14 [label="Start (let (_x_0 : sko_ty_0 list) = List.tl x in\l       let (_x_1 : sko_ty_0 list) = List.append y z in\l       not (x \<\> [])\l       \|\| not (List.append _x_0 _x_1 = List.append (List.append _x_0 y) z)\l       \|\| (List.append x _x_1 = List.append (List.append x y) z) :name \"1.1\"\l       :time 0.039s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_14 -> p_13 [label=""];
p_13 [label="Simplify (true :expansions [List.append; List.append; List.append] :rw []\l          :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
}
p_19 -> p_17 [label=""];
subgraph cluster_18 {
  color=blue;
p_17 [label="Start (x \<\> []\l       \|\| (List.append x (List.append y z) = List.append (List.append x y) z)\l       :name \"1.2\" :time 0.039s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_17 -> p_16 [label=""];
p_16 [label="Simplify (true :expansions [List.append; List.append] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
}

Try this!

In [3]:

lemma rev_append x y =
 List.rev (x @ y) = List.rev y @ List.rev x
 [@@auto]

Out[3]:

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

List.rev (x @ y) = List.rev y @ List.rev x.

1 nontautological subgoal.

Subgoal 1:

|---------------------------------------------------------------------------
 List.rev (List.append x y) = List.append (List.rev y) (List.rev x)


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.rev (List.append x y) = List.append (List.rev y) (List.rev x)

But simplification reduces this to true, using the definitions of List.append
and List.rev, and the rewrite rule List.append_to_nil.

Subgoal 1.1:

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

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

Subgoal 1.1':

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

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

 ⓘ  Rules:
    (:def List.append)
    (:def List.rev)
    (:rw List.append_to_nil)
    (:rw assoc_append)
    (:induct List.append)

Proved

proof

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

Expand

start[0.151s, "Goal"]
  List.rev (List.append ( :var_0: ) ( :var_1: ))
  = List.append (List.rev ( :var_1: )) (List.rev ( :var_0: ))

subproof

List.rev (List.append x y) = List.append (List.rev y) (List.rev x)

start[0.151s, "1"]
  List.rev (List.append x y) = List.append (List.rev y) (List.rev x)

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 : sko_ty_0 list) = List.rev y in
       let (_x_2 : bool)
           = List.rev (List.append x y) = List.append _x_1 (List.rev x)
       in
       let (_x_3 : sko_ty_0 list) = List.tl x in
       (_x_0 || _x_2)
       && (not
           (_x_0
            && (List.rev (List.append _x_3 y)
                = List.append _x_1 (List.rev _x_3)))
           || _x_2)
       :cases [x <> []
               || (List.rev (List.append x y)
                   = List.append (List.rev y) (List.rev x));
               let (_x_0 : sko_ty_0 list) = List.tl x in
               let (_x_1 : sko_ty_0 list) = List.rev y in
               not (x <> [])
               || not
                  (List.rev (List.append _x_0 y)
                   = List.append _x_1 (List.rev _x_0))
               || (List.rev (List.append x y) = List.append _x_1 (List.rev x))])

subproof

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

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

simplify

into:	let (_x_0 : sko_ty_0 list) = List.tl x in let (_x_1 : sko_ty_0 list) = List.rev (List.append _x_0 y) in let (_x_2 : sko_ty_0 list) = List.rev y in let (_x_3 : sko_ty_0 list) = List.rev _x_0 in let (_x_4 : sko_ty_0 list) = [List.hd x] in not (x <> []) \|\| not (_x_1 = List.append _x_2 _x_3) \|\| (List.append _x_1 _x_4 = List.append _x_2 (List.append _x_3 _x_4))
expansions:	[List.rev, List.rev, List.append]
rewrite_steps:
forward_chaining:

simplify
into:
true
expansions:
[]
rewrite_steps:
assoc_append
forward_chaining:

subproof
x <> [] || (List.rev (List.append x y) = List.append (List.rev y) (List.rev x))
- start[0.109s, "1.2"] x <> [] || (List.rev (List.append x y) = List.append (List.rev y) (List.rev x))
- simplify
  into:
  true
  expansions:
  [List.append, List.rev, List.append]
  rewrite_steps:
  List.append_to_nil
  forward_chaining:

digraph "proof" {
p_44 [label="Start (List.rev (List.append ( :var_0: ) ( :var_1: ))\l       = List.append (List.rev ( :var_1: )) (List.rev ( :var_0: ))\l       :name \"Goal\" :time 0.151s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_44 -> p_42 [label=""];
subgraph cluster_43 {
  color=blue;
p_42 [label="Start (List.rev (List.append x y) = List.append (List.rev y) (List.rev x)\l       :name \"1\" :time 0.151s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_42 -> p_41 [label=""];
p_41 [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_41 -> p_40 [label=""];
p_40 [label="Split (let (_x_0 : bool) = x \<\> [] in\l       let (_x_1 : sko_ty_0 list) = List.rev y in\l       let (_x_2 : bool)\l           = List.rev (List.append x y) = List.append _x_1 (List.rev x)\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.rev (List.append _x_3 y)\l                = List.append _x_1 (List.rev _x_3)))\l           \|\| _x_2)\l       :cases [x \<\> []\l               \|\| (List.rev (List.append x y)\l                   = List.append (List.rev y) (List.rev x));\l               let (_x_0 : sko_ty_0 list) = List.tl x in\l               let (_x_1 : sko_ty_0 list) = List.rev y in\l               not (x \<\> [])\l               \|\| not\l                  (List.rev (List.append _x_0 y)\l                   = List.append _x_1 (List.rev _x_0))\l               \|\| (List.rev (List.append x y) = List.append _x_1 (List.rev x))])",shape=box,style=filled,fontname="courier",fontsize=14];
p_40 -> p_35 [label=""];
subgraph cluster_36 {
  color=blue;
p_35 [label="Start (let (_x_0 : sko_ty_0 list) = List.tl x in\l       let (_x_1 : sko_ty_0 list) = List.rev y in\l       not (x \<\> [])\l       \|\| not\l          (List.rev (List.append _x_0 y) = List.append _x_1 (List.rev _x_0))\l       \|\| (List.rev (List.append x y) = List.append _x_1 (List.rev x))\l       :name \"1.1\" :time 0.109s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_35 -> p_34 [label=""];
p_34 [label="Simplify (let (_x_0 : sko_ty_0 list) = List.tl x in\l          let (_x_1 : sko_ty_0 list) = List.rev (List.append _x_0 y) in\l          let (_x_2 : sko_ty_0 list) = List.rev y in\l          let (_x_3 : sko_ty_0 list) = List.rev _x_0 in\l          let (_x_4 : sko_ty_0 list) = [List.hd x] in\l          not (x \<\> []) \|\| not (_x_1 = List.append _x_2 _x_3)\l          \|\| (List.append _x_1 _x_4\l              = List.append _x_2 (List.append _x_3 _x_4))\l          :expansions [List.rev; List.rev; List.append] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_34 -> p_33 [label=""];
p_33 [label="Simplify (true :expansions [] :rw [assoc_append] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
}
p_40 -> p_38 [label=""];
subgraph cluster_39 {
  color=blue;
p_38 [label="Start (x \<\> []\l       \|\| (List.rev (List.append x y) = List.append (List.rev y) (List.rev x))\l       :name \"1.2\" :time 0.109s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_38 -> p_37 [label=""];
p_37 [label="Simplify (true :expansions [List.append; List.rev; List.append]\l          :rw [List.append_to_nil] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
}

Try this!

In [4]:

verify (fun lst ->
  List.for_all (fun x -> x > 0) lst ==>
    List.fold_right (+) ~base:1 lst > 0)
[@@auto]

Out[4]:

- : Z.t list -> bool = <fun>
Goal:

List.for_all anon_fun._verify_target.1 lst
==> List.fold_right ( + ) 1 lst > 0.

1 nontautological subgoal.

Subgoal 1:

 H0. List.for_all anon_fun._verify_target.1 lst
 H1. List.fold_right ( + ) 1 lst <= 0
|---------------------------------------------------------------------------
 false


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

Induction scheme:

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

2 nontautological subgoals.

Subgoal 1.2:

 H0. List.for_all anon_fun._verify_target.1 lst
 H1. List.fold_right ( + ) 1 lst <= 0
|---------------------------------------------------------------------------
 lst <> []

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

Subgoal 1.1:

 H0. lst <> []
 H1. not (List.for_all anon_fun._verify_target.1 (List.tl lst))
     || not (List.fold_right ( + ) 1 (List.tl lst) <= 0)
 H2. List.for_all anon_fun._verify_target.1 lst
 H3. List.fold_right ( + ) 1 lst <= 0
|---------------------------------------------------------------------------
 false

But simplification reduces this to true, using the definitions of
List.fold_right and List.for_all.

 ⓘ  Rules:
    (:def List.fold_right)
    (:def List.for_all)
    (:induct List.for_all)

Proved

proof

ground_instances:	0
definitions:	5
inductions:	1
search_time:	0.163s

Expand

start[0.163s, "Goal"]
  List.for_all anon_fun._verify_target.1 ( :var_0: )
  ==> List.fold_right ( + ) 1 ( :var_0: ) > 0

subproof

not (List.for_all anon_fun._verify_target.1 lst) || not (List.fold_right ( + ) 1 lst <= 0)

start[0.162s, "1"]
  not (List.for_all anon_fun._verify_target.1 lst)
  || not (List.fold_right ( + ) 1 lst <= 0)

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

Split (let (_x_0 : bool) = not (List.for_all anon_fun._verify_target.1 lst)
       in
       let (_x_1 : bool) = not (List.fold_right ( + ) 1 lst <= 0) in
       let (_x_2 : bool) = lst <> [] in
       let (_x_3 : int list) = List.tl lst in
       (_x_0 || _x_1 || _x_2)
       && (not
           (_x_2
            && (not (List.for_all anon_fun._verify_target.1 _x_3)
                || not (List.fold_right ( + ) 1 _x_3 <= 0)))
           || _x_0 || _x_1)
       :cases [not (List.for_all anon_fun._verify_target.1 lst)
               || not (List.fold_right ( + ) 1 lst <= 0) || lst <> [];
               let (_x_0 : int list) = List.tl lst in
               not (lst <> [])
               || not
                  (not (List.for_all anon_fun._verify_target.1 _x_0)
                   || not (List.fold_right ( + ) 1 _x_0 <= 0))
               || not (List.for_all anon_fun._verify_target.1 lst)
               || not (List.fold_right ( + ) 1 lst <= 0)])

subproof
let (_x_0 : int list) = List.tl lst in not (lst <> []) || not (not (List.for_all anon_fun._verify_target.1 _x_0) || not (List.fold_right ( + ) 1 _x_0 <= 0)) || not (List.for_all anon_fun._verify_target.1 lst) || not (List.fold_right ( + ) 1 lst <= 0)
- start[0.112s, "1.1"] let (_x_0 : int list) = List.tl lst in not (lst <> []) || not (not (List.for_all anon_fun._verify_target.1 _x_0) || not (List.fold_right ( + ) 1 _x_0 <= 0)) || not (List.for_all anon_fun._verify_target.1 lst) || not (List.fold_right ( + ) 1 lst <= 0)
- simplify
  into:
  true
  expansions:
  [List.for_all, List.fold_right, List.for_all, List.fold_right]
  rewrite_steps:
  forward_chaining:
subproof
not (List.for_all anon_fun._verify_target.1 lst) || not (List.fold_right ( + ) 1 lst <= 0) || lst <> []
- start[0.112s, "1.2"] not (List.for_all anon_fun._verify_target.1 lst) || not (List.fold_right ( + ) 1 lst <= 0) || lst <> []
- simplify
  into:
  true
  expansions:
  List.fold_right
  rewrite_steps:
  forward_chaining:

digraph "proof" {
p_64 [label="Start (List.for_all anon_fun._verify_target.1 ( :var_0: )\l       ==\> List.fold_right ( + ) 1 ( :var_0: ) \> 0 :name \"Goal\" :time 0.163s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_64 -> p_62 [label=""];
subgraph cluster_63 {
  color=blue;
p_62 [label="Start (not (List.for_all anon_fun._verify_target.1 lst)\l       \|\| not (List.fold_right ( + ) 1 lst \<= 0) :name \"1\" :time 0.162s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_62 -> p_61 [label=""];
p_61 [label="Induct ((functional ?),\l        :scheme (not (lst \<\> []) ==\> φ lst)\l                && (lst \<\> [] && φ (List.tl lst) ==\> φ lst))",shape=box,style=filled,fontname="courier",fontsize=14];
p_61 -> p_60 [label=""];
p_60 [label="Split (let (_x_0 : bool) = not (List.for_all anon_fun._verify_target.1 lst)\l       in\l       let (_x_1 : bool) = not (List.fold_right ( + ) 1 lst \<= 0) in\l       let (_x_2 : bool) = lst \<\> [] in\l       let (_x_3 : int list) = List.tl lst in\l       (_x_0 \|\| _x_1 \|\| _x_2)\l       && (not\l           (_x_2\l            && (not (List.for_all anon_fun._verify_target.1 _x_3)\l                \|\| not (List.fold_right ( + ) 1 _x_3 \<= 0)))\l           \|\| _x_0 \|\| _x_1)\l       :cases [not (List.for_all anon_fun._verify_target.1 lst)\l               \|\| not (List.fold_right ( + ) 1 lst \<= 0) \|\| lst \<\> [];\l               let (_x_0 : int list) = List.tl lst in\l               not (lst \<\> [])\l               \|\| not\l                  (not (List.for_all anon_fun._verify_target.1 _x_0)\l                   \|\| not (List.fold_right ( + ) 1 _x_0 \<= 0))\l               \|\| not (List.for_all anon_fun._verify_target.1 lst)\l               \|\| not (List.fold_right ( + ) 1 lst \<= 0)])",shape=box,style=filled,fontname="courier",fontsize=14];
p_60 -> p_55 [label=""];
subgraph cluster_56 {
  color=blue;
p_55 [label="Start (let (_x_0 : int list) = List.tl lst in\l       not (lst \<\> [])\l       \|\| not\l          (not (List.for_all anon_fun._verify_target.1 _x_0)\l           \|\| not (List.fold_right ( + ) 1 _x_0 \<= 0))\l       \|\| not (List.for_all anon_fun._verify_target.1 lst)\l       \|\| not (List.fold_right ( + ) 1 lst \<= 0) :name \"1.1\" :time 0.112s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_55 -> p_54 [label=""];
p_54 [label="Simplify (true\l          :expansions [List.for_all;\l                       List.fold_right;\l                       List.for_all;\l                       List.fold_right]\l          :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
}
p_60 -> p_58 [label=""];
subgraph cluster_59 {
  color=blue;
p_58 [label="Start (not (List.for_all anon_fun._verify_target.1 lst)\l       \|\| not (List.fold_right ( + ) 1 lst \<= 0) \|\| lst \<\> [] :name \"1.2\"\l       :time 0.112s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_58 -> p_57 [label=""];
p_57 [label="Simplify (true :expansions [List.fold_right] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
}

Functional Induction¶

By default, Imandra uses functional induction (also known as recursion induction).

A functional induction scheme is one derived from the recursive structure of a function definition. The termination measure used to admit the function is also used to justify the soundness of the functional induction scheme. Unless instructed otherwise, Imandra will consider all recursive functions in a goal, analyse their recursions and instances, and apply various heuristics to merge and score them and adapt them to the conjecture being proved. In general, there may be more than one plausible induction scheme to choose from, and selecting the "right" way to induct can often be a key step in difficult proofs. Imandra will often make the "right" decision. However, in case it doesn't, it is also possible to manually specify the induction that Imandra should do.

Let us return to the function repeat above and see functional induction in action.

Try this!

In [5]:

lemma repeat_len c n =
  n >= 0 ==>
  List.length (repeat c n) = n [@@auto]

Out[5]:

val repeat_len : 'a -> Z.t -> bool = <fun>
Goal:

n >= 0 ==> List.length (repeat c n) = n.

1 nontautological subgoal.

Subgoal 1:

 H0. n >= 0
|---------------------------------------------------------------------------
 List.length (repeat c n) = n


Must try induction.

We shall induct according to a scheme derived from repeat.

Induction scheme:

 (n <= 0 ==> φ c n) && (not (n <= 0) && φ c (n - 1) ==> φ c n).

2 nontautological subgoals.

Subgoal 1.2:

 H0. n <= 0
 H1. n >= 0
|---------------------------------------------------------------------------
 List.length (repeat c n) = n

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

Subgoal 1.1:

 H0. not (n <= 0)
 H1. n >= 1 ==> List.length (repeat c ((-1) + n)) = (-1) + n
 H2. n >= 0
|---------------------------------------------------------------------------
 List.length (repeat c n) = n

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

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

Proved

proof

ground_instances:	0
definitions:	4
inductions:	1
search_time:	0.090s

Expand

start[0.090s, "Goal"]
  ( :var_0: ) >= 0
  ==> List.length (repeat ( :var_1: ) ( :var_0: )) = ( :var_0: )

subproof

not (n >= 0) || (List.length (repeat c n) = n)

start[0.090s, "1"] not (n >= 0) || (List.length (repeat c n) = n)

induction on (functional ?)
:scheme (n <= 0 ==> φ c n) && (not (n <= 0) && φ c (n - 1) ==> φ c n)

Split (let (_x_0 : bool) = not (n <= 0) in
       let (_x_1 : bool) = List.length (repeat c n) = n in
       let (_x_2 : bool) = not (n >= 0) in
       let (_x_3 : int) = (-1) + n in
       (_x_0 || _x_1 || _x_2)
       && (_x_1
           || not
              (_x_0 && (not (n >= 1) || (List.length (repeat c _x_3) = _x_3)))
           || _x_2)
       :cases [not (n <= 0) || not (n >= 0) || (List.length (repeat c n) = n);
               let (_x_0 : int) = (-1) + n in
               (n <= 0)
               || not (n >= 1 ==> List.length (repeat c _x_0) = _x_0)
               || not (n >= 0) || (List.length (repeat c n) = n)])

subproof
let (_x_0 : int) = (-1) + n in (n <= 0) || not (n >= 1 ==> List.length (repeat c _x_0) = _x_0) || not (n >= 0) || (List.length (repeat c n) = n)
- start[0.042s, "1.1"] let (_x_0 : int) = (-1) + n in (n <= 0) || not (n >= 1 ==> List.length (repeat c _x_0) = _x_0) || not (n >= 0) || (List.length (repeat c n) = n)
- simplify
  into:
  true
  expansions:
  [List.length, repeat]
  rewrite_steps:
  forward_chaining:
  List.len_nonnegative
  List.len_nonnegative
  List.len_nonnegative
  List.len_nonnegative
  List.len_nonnegative
  List.len_nonnegative
subproof
not (n <= 0) || not (n >= 0) || (List.length (repeat c n) = n)
- start[0.042s, "1.2"] not (n <= 0) || not (n >= 0) || (List.length (repeat c n) = n)
- simplify
  into:
  true
  expansions:
  [List.length, repeat]
  rewrite_steps:
  forward_chaining:
  List.len_nonnegative

digraph "proof" {
p_84 [label="Start (( :var_0: ) \>= 0\l       ==\> List.length (repeat ( :var_1: ) ( :var_0: )) = ( :var_0: )\l       :name \"Goal\" :time 0.090s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_84 -> p_82 [label=""];
subgraph cluster_83 {
  color=blue;
p_82 [label="Start (not (n \>= 0) \|\| (List.length (repeat c n) = n) :name \"1\" :time 0.090s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_82 -> p_81 [label=""];
p_81 [label="Induct ((functional ?),\l        :scheme (n \<= 0 ==\> φ c n)\l                && (not (n \<= 0) && φ c (n - 1) ==\> φ c n))",shape=box,style=filled,fontname="courier",fontsize=14];
p_81 -> p_80 [label=""];
p_80 [label="Split (let (_x_0 : bool) = not (n \<= 0) in\l       let (_x_1 : bool) = List.length (repeat c n) = n in\l       let (_x_2 : bool) = not (n \>= 0) in\l       let (_x_3 : int) = (-1) + n in\l       (_x_0 \|\| _x_1 \|\| _x_2)\l       && (_x_1\l           \|\| not\l              (_x_0 && (not (n \>= 1) \|\| (List.length (repeat c _x_3) = _x_3)))\l           \|\| _x_2)\l       :cases [not (n \<= 0) \|\| not (n \>= 0) \|\| (List.length (repeat c n) = n);\l               let (_x_0 : int) = (-1) + n in\l               (n \<= 0)\l               \|\| not (n \>= 1 ==\> List.length (repeat c _x_0) = _x_0)\l               \|\| not (n \>= 0) \|\| (List.length (repeat c n) = n)])",shape=box,style=filled,fontname="courier",fontsize=14];
p_80 -> p_75 [label=""];
subgraph cluster_76 {
  color=blue;
p_75 [label="Start (let (_x_0 : int) = (-1) + n in\l       (n \<= 0) \|\| not (n \>= 1 ==\> List.length (repeat c _x_0) = _x_0)\l       \|\| not (n \>= 0) \|\| (List.length (repeat c n) = n) :name \"1.1\"\l       :time 0.042s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_75 -> p_74 [label=""];
p_74 [label="Simplify (true :expansions [List.length; repeat] :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];
}
p_80 -> p_78 [label=""];
subgraph cluster_79 {
  color=blue;
p_78 [label="Start (not (n \<= 0) \|\| not (n \>= 0) \|\| (List.length (repeat c n) = n)\l       :name \"1.2\" :time 0.042s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_78 -> p_77 [label=""];
p_77 [label="Simplify (true :expansions [List.length; repeat] :rw []\l          :fc [List.len_nonnegative])",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
}

Functional induction schemes tailored to a problem can also be manually specified.

In order to manually specify a functional induction, one must define a recursive function encoding the recursion scheme one wants available in induction (Imandra doesn't care what the function does, it only looks at how it recurses). As always, Imandra must be able to prove that the recursive function terminates in order for it to be admitted into the logic. The ordinal measures used in the termination proof are then used to justify subsequent functional induction schemes derived from the function.

Let's see a simple example. Note that we could trivially prove this goal with [@@auto], but we shall use it to illustrate the process of manual induction schemes nevertheless! For fun, we'll make our custom induction scheme have two base-cases.

Try this!

In [6]:

let rec sum n =
 if n <= 0 then 0
 else n + sum (n-1)

let rec induct_scheme (n : int) =
 if n <= 0 then true
 else if n = 1 then true
 else induct_scheme (n-1)

Out[6]:

val sum : Z.t -> Z.t = <fun>
val induct_scheme : Z.t -> bool = <fun>

termination proof

Termination proof

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

original:

sum n

sub:

sum (n - 1)

original ordinal:

Ordinal.Int (_cnt n)

sub ordinal:

Ordinal.Int (_cnt (n - 1))

path:

[not (n <= 0)]

proof:

detailed proof

summary
full

ground_instances:

definitions:

inductions:

search_time:

0.010s

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:	1099
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:	763519891
final checks:	1
added eqs:	4
del clause:	5
arith eq adapter:	2
memory:	17.400000
max memory:	17.780000

Expand

start[0.010s]
  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
  not (n <= 0) && ((_x_0 >= 0) && (_x_2 >= 0))
  ==> (_x_1 <= 0) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)

simplify

into:	(n <= 0) \|\| (n <= 1) \|\| 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_837/server 1) (+ (- 1) n_837/server)…
expansions:

Unsat

termination proof

Termination proof

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

original:

induct_scheme n

sub:

induct_scheme (n - 1)

original ordinal:

Ordinal.Int (_cnt n)

sub ordinal:

Ordinal.Int (_cnt (n - 1))

path:

[not (n = 1) && not (n <= 0)]

proof:

detailed proof

summary
full

ground_instances:

definitions:

inductions:

search_time:

0.016s

details:

Expand

smt_stats:

num checks:	3
arith assert lower:	8
arith tableau max rows:	4
arith tableau max columns:	11
arith pivots:	2
rlimit count:	1265
mk clause:	5
datatype occurs check:	2
mk bool var:	21
arith assert upper:	3
decisions:	2
arith row summations:	3
propagations:	3
conflicts:	2
arith fixed eqs:	2
datatype accessor ax:	2
arith conflicts:	1
arith num rows:	4
arith assert diseq:	3
num allocs:	804994748
final checks:	1
added eqs:	4
del clause:	5
arith eq adapter:	4
memory:	17.650000
max memory:	17.780000

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
  not (n = 1) && (not (n <= 0) && ((_x_0 >= 0) && (_x_2 >= 0)))
  ==> not (not (_x_1 = 1) && not (_x_1 <= 0))
      || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)

simplify

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

unroll

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

Unsat

Try this!

In [7]:

verify (fun n -> n >= 0 ==> sum n = (n * (n+1)) / 2) [@@induct functional induct_scheme]

Out[7]:

- : Z.t -> bool = <fun>
Goal:

n >= 0 ==> sum n = (n * (n + 1)) / 2.

1 nontautological subgoal.

Note: Thank you for your explicit request for a non-present functional
induction on `induct_scheme`!

We shall induct according to a scheme derived from induct_scheme.

Induction scheme:

 (not (not (n = 1) && not (n <= 0)) ==> φ n)
 && (not (n <= 0) && (not (n = 1) && φ (n - 1)) ==> φ n).

2 nontautological subgoals.

Subgoal 2:

 H0. n >= 0
|---------------------------------------------------------------------------
 C0. not (n = 1) && not (n <= 0)
 C1. sum n = (n * (1 + n)) / 2

This simplifies to the following 2 subgoals:

Subgoal 2.2:

 H0. n = 1
|---------------------------------------------------------------------------
 sum n = (n * (1 + n)) / 2

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

Subgoal 2.1:

 H0. n <= 0
 H1. n >= 0
|---------------------------------------------------------------------------
 C0. n = 1
 C1. sum n = (n * (1 + n)) / 2

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

Subgoal 1:

 H0. n >= 0
 H1. not (n <= 0)
 H2. not (n = 1)
 H3. n >= 1 ==> sum ((-1) + n) = (n * ((-1) + n)) / 2
|---------------------------------------------------------------------------
 sum n = (n * (1 + n)) / 2

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

 ⓘ  Rules:
    (:def sum)
    (:induct induct_scheme)

Proved

proof

ground_instances:	0
definitions:	4
inductions:	1
search_time:	0.150s

Expand

start[0.150s, "Goal"]
  ( :var_0: ) >= 0
  ==> sum ( :var_0: ) = (( :var_0: ) * (( :var_0: ) + 1)) / 2

subproof

not (n >= 0) || (sum n = (n * (1 + n)) / 2)

start[0.150s, "1"] not (n >= 0) || (sum n = (n * (1 + n)) / 2)

induction on (functional induct_scheme)
:scheme (not (not (n = 1) && not (n <= 0)) ==> φ n)
        && (not (n <= 0) && (not (n = 1) && φ (n - 1)) ==> φ n)

Split (let (_x_0 : bool) = not (n = 1) in
       let (_x_1 : bool) = not (n <= 0) in
       let (_x_2 : bool) = not (n >= 0) in
       let (_x_3 : bool) = sum n = (n * (1 + n)) / 2 in
       let (_x_4 : int) = (-1) + n in
       ((_x_0 && _x_1) || _x_2 || _x_3)
       && (_x_2 || _x_3
           || not
              (_x_1 && _x_0 && (not (n >= 1) || (sum _x_4 = (n * _x_4) / 2))))
       :cases [not (n >= 0) || (not (n = 1) && not (n <= 0))
               || (sum n = (n * (1 + n)) / 2);
               let (_x_0 : int) = (-1) + n in
               not (n >= 0) || (n <= 0) || (n = 1)
               || not (n >= 1 ==> sum _x_0 = (n * _x_0) / 2)
               || (sum n = (n * (1 + n)) / 2)])

subproof
let (_x_0 : int) = (-1) + n in not (n >= 0) || (n <= 0) || (n = 1) || not (n >= 1 ==> sum _x_0 = (n * _x_0) / 2) || (sum n = (n * (1 + n)) / 2)
- start[0.149s, "1"] let (_x_0 : int) = (-1) + n in not (n >= 0) || (n <= 0) || (n = 1) || not (n >= 1 ==> sum _x_0 = (n * _x_0) / 2) || (sum n = (n * (1 + n)) / 2)
- simplify
  into:
  true
  expansions:
  sum
  rewrite_steps:
  forward_chaining:
subproof
not (n >= 0) || (not (n = 1) && not (n <= 0)) || (sum n = (n * (1 + n)) / 2)
- start[0.149s, "2"] not (n >= 0) || (not (n = 1) && not (n <= 0)) || (sum n = (n * (1 + n)) / 2)
- simplify
  into:
  let (_x_0 : bool) = n = 1 in let (_x_1 : bool) = sum n = (n * (1 + n)) / 2 in (not _x_0 || _x_1) && (_x_0 || not (n <= 0) || not (n >= 0) || _x_1)
  expansions:
  []
  rewrite_steps:
  forward_chaining:
  Subproof
  Subproof

digraph "proof" {
p_109 [label="Start (( :var_0: ) \>= 0\l       ==\> sum ( :var_0: ) = (( :var_0: ) * (( :var_0: ) + 1)) / 2\l       :name \"Goal\" :time 0.150s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_109 -> p_107 [label=""];
subgraph cluster_108 {
  color=blue;
p_107 [label="Start (not (n \>= 0) \|\| (sum n = (n * (1 + n)) / 2) :name \"1\" :time 0.150s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_107 -> p_106 [label=""];
p_106 [label="Induct ((functional induct_scheme),\l        :scheme (not (not (n = 1) && not (n \<= 0)) ==\> φ n)\l                && (not (n \<= 0) && (not (n = 1) && φ (n - 1)) ==\> φ n))",shape=box,style=filled,fontname="courier",fontsize=14];
p_106 -> p_105 [label=""];
p_105 [label="Split (let (_x_0 : bool) = not (n = 1) in\l       let (_x_1 : bool) = not (n \<= 0) in\l       let (_x_2 : bool) = not (n \>= 0) in\l       let (_x_3 : bool) = sum n = (n * (1 + n)) / 2 in\l       let (_x_4 : int) = (-1) + n in\l       ((_x_0 && _x_1) \|\| _x_2 \|\| _x_3)\l       && (_x_2 \|\| _x_3\l           \|\| not\l              (_x_1 && _x_0 && (not (n \>= 1) \|\| (sum _x_4 = (n * _x_4) / 2))))\l       :cases [not (n \>= 0) \|\| (not (n = 1) && not (n \<= 0))\l               \|\| (sum n = (n * (1 + n)) / 2);\l               let (_x_0 : int) = (-1) + n in\l               not (n \>= 0) \|\| (n \<= 0) \|\| (n = 1)\l               \|\| not (n \>= 1 ==\> sum _x_0 = (n * _x_0) / 2)\l               \|\| (sum n = (n * (1 + n)) / 2)])",shape=box,style=filled,fontname="courier",fontsize=14];
p_105 -> p_94 [label=""];
subgraph cluster_95 {
  color=blue;
p_94 [label="Start (let (_x_0 : int) = (-1) + n in\l       not (n \>= 0) \|\| (n \<= 0) \|\| (n = 1)\l       \|\| not (n \>= 1 ==\> sum _x_0 = (n * _x_0) / 2)\l       \|\| (sum n = (n * (1 + n)) / 2) :name \"1\" :time 0.149s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_94 -> p_93 [label=""];
p_93 [label="Simplify (true :expansions [sum] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
}
p_105 -> p_103 [label=""];
subgraph cluster_104 {
  color=blue;
p_103 [label="Start (not (n \>= 0) \|\| (not (n = 1) && not (n \<= 0))\l       \|\| (sum n = (n * (1 + n)) / 2) :name \"2\" :time 0.149s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_103 -> p_102 [label=""];
p_102 [label="Simplify (let (_x_0 : bool) = n = 1 in\l          let (_x_1 : bool) = sum n = (n * (1 + n)) / 2 in\l          (not _x_0 \|\| _x_1)\l          && (_x_0 \|\| not (n \<= 0) \|\| not (n \>= 0) \|\| _x_1) :expansions []\l          :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_102 -> p_97 [label=""];
subgraph cluster_98 {
  color=blue;
p_97 [label="Start ((n = 1) \|\| not (n \<= 0) \|\| not (n \>= 0) \|\| (sum n = (n * (1 + n)) / 2)\l       :name \"2.1\" :time 0.059s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_97 -> p_96 [label=""];
p_96 [label="Simplify (true :expansions [sum] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
}
p_102 -> p_100 [label=""];
subgraph cluster_101 {
  color=blue;
p_100 [label="Start (not (n = 1) \|\| (sum n = (n * (1 + n)) / 2) :name \"2.2\" :time 0.059s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_100 -> p_99 [label=""];
p_99 [label="Simplify (true :expansions [sum; sum] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
}
}

Note that it's rare to have to manually instruct Imandra how to induct in this way. Usually, if you need to instruct Imandra to use a different scheme than the one it automatically picked, you'll simply need to give Imandra the hint of "inducting following key recursive function foo" in your goal. For example, if Imandra had made a wrong selection in a goal involving sum and some other recursive functions, we might tell Imandra [@@induct functional sum] to get it to select a scheme derived from the recursive structure of sum.

Structural Induction¶

Imandra also supports structural induction. Unlike functional induction schemes which are derived from recursive functions, structural induction schemes are derived from type definitions.

For example, we can define a type of binary trees and prove a property about them by structural induction.

Try this!

In [8]:

type 'a tree = Node of 'a * 'a tree * 'a tree | Leaf

Out[8]:

type 'a tree = Node of 'a * 'a tree * 'a tree | Leaf

Try this!

In [9]:

let rec size (x : 'a tree) =
 match x with
 | Node (_, a,b) -> size a + size b
 | Leaf -> 1

Out[9]:

val size : 'a tree -> Z.t = <fun>

termination proof

Termination proof

call `size (Destruct(Node, 1, x))` from `size x`

original:

size x

sub:

size (Destruct(Node, 1, x))

original ordinal:

Ordinal.Int (_cnt x)

sub ordinal:

Ordinal.Int (_cnt (Destruct(Node, 1, x)))

path:

[not Is_a(Leaf, x)]

proof:

detailed proof

summary
full

ground_instances:

definitions:

inductions:

search_time:

0.011s

details:

Expand

smt_stats:

num checks:	8
arith assert lower:	19
arith tableau max rows:	7
arith tableau max columns:	18
arith pivots:	18
rlimit count:	6098
mk clause:	15
datatype occurs check:	15
mk bool var:	78
arith gcd tests:	4
arith assert upper:	14
datatype splits:	3
decisions:	23
arith row summations:	42
arith branch var:	1
propagations:	10
arith patches:	1
conflicts:	6
arith fixed eqs:	10
datatype accessor ax:	7
arith conflicts:	2
arith num rows:	7
datatype constructor ax:	11
num allocs:	1258749198
final checks:	5
added eqs:	64
del clause:	8
arith ineq splits:	1
arith eq adapter:	11
memory:	17.980000
max memory:	18.150000

Expand

start[0.011s]
  let (_x_0 : int) = count.tree (const 0) x in
  let (_x_1 : ty_0 tree) = Destruct(Node, 1, x) in
  let (_x_2 : int) = count.tree (const 0) _x_1 in
  let (_x_3 : bool) = Is_a(Leaf, _x_1) in
  not Is_a(Leaf, x) && ((_x_0 >= 0) && (_x_2 >= 0))
  ==> (_x_3 && _x_3) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)

simplify

into:	let (_x_0 : int) = count.tree (const 0) x in let (_x_1 : ty_0 tree) = Destruct(Node, 1, x) in let (_x_2 : int) = count.tree (const 0) _x_1 in not (not Is_a(Leaf, x) && (_x_0 >= 0) && (_x_2 >= 0)) \|\| Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0) \|\| Is_a(Leaf, _x_1)
expansions:	[]
rewrite_steps:
forward_chaining:

unroll

expr:	(\|count.tree_990/server\| (\|get.Node.1_970/server\| x_977/server))
expansions:

unroll

expr:	(\|Ordinal.<<\| (\|Ordinal.Int_79/boot\| (\|count.tree_990/server\| (\|get.Node.1_970/serve…
expansions:

unroll
expr:
(|count.tree_990/server| x_977/server)
expansions:
Unsat

call `size (Destruct(Node, 2, x))` from `size x`

original:

size x

sub:

size (Destruct(Node, 2, x))

original ordinal:

Ordinal.Int (_cnt x)

sub ordinal:

Ordinal.Int (_cnt (Destruct(Node, 2, x)))

path:

[not Is_a(Leaf, x)]

proof:

detailed proof

summary
full

ground_instances:

definitions:

inductions:

search_time:

0.012s

details:

Expand

smt_stats:

num checks:	8
arith assert lower:	14
arith tableau max rows:	7
arith tableau max columns:	18
arith pivots:	12
rlimit count:	2814
mk clause:	12
datatype occurs check:	14
mk bool var:	73
arith gcd tests:	4
arith assert upper:	11
datatype splits:	3
decisions:	18
arith row summations:	30
arith branch var:	1
propagations:	7
arith patches:	1
conflicts:	6
arith fixed eqs:	7
datatype accessor ax:	7
arith conflicts:	2
arith num rows:	7
datatype constructor ax:	11
num allocs:	1211576902
final checks:	5
added eqs:	55
del clause:	5
arith ineq splits:	1
arith eq adapter:	8
memory:	17.920000
max memory:	18.150000

Expand

start[0.012s]
  let (_x_0 : int) = count.tree (const 0) x in
  let (_x_1 : ty_0 tree) = Destruct(Node, 2, x) in
  let (_x_2 : int) = count.tree (const 0) _x_1 in
  let (_x_3 : bool) = Is_a(Leaf, _x_1) in
  not Is_a(Leaf, x) && ((_x_0 >= 0) && (_x_2 >= 0))
  ==> (_x_3 && _x_3) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)

simplify

into:	let (_x_0 : ty_0 tree) = Destruct(Node, 2, x) in let (_x_1 : int) = count.tree (const 0) _x_0 in let (_x_2 : int) = count.tree (const 0) x in Is_a(Leaf, _x_0) \|\| Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) \|\| not (not Is_a(Leaf, x) && (_x_2 >= 0) && (_x_1 >= 0))
expansions:	[]
rewrite_steps:
forward_chaining:

unroll

expr:	(\|Ordinal.<<\| (\|Ordinal.Int_79/boot\| (\|count.tree_990/server\| (\|get.Node.2_971/serve…
expansions:

unroll

expr:	(\|count.tree_990/server\| (\|get.Node.2_971/server\| x_977/server))
expansions:

unroll
expr:
(|count.tree_990/server| x_977/server)
expansions:
Unsat

Try this!

In [10]:

verify (fun x -> size x > 0) [@@induct structural x]

Out[10]:

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

size x > 0.

1 nontautological subgoal.

Induction scheme:

 φ Leaf
 && (Is_a(Node, x)
     && (φ (Destruct(Node, 1, x)) && φ (Destruct(Node, 2, x))) ==> 
     φ x).

2 nontautological subgoals.

Subgoal 2:

|---------------------------------------------------------------------------
 not (size Leaf <= 0)

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

Subgoal 1:

 H0. size x <= 0
 H1. Is_a(Node, x)
 H2. not (size (Destruct(Node, 1, x)) <= 0)
 H3. not (size (Destruct(Node, 2, x)) <= 0)
|---------------------------------------------------------------------------
 false

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

 ⓘ  Rules:
    (:def size)
    (:induct struct tree)

Proved

proof

ground_instances:	0
definitions:	2
inductions:	1
search_time:	0.030s

Expand

start[0.030s, "Goal"] size ( :var_0: ) > 0

subproof

not (size x <= 0)

```
start[0.030s, "1"] not (size x <= 0)
```

induction on (structural+ x)
:scheme φ Leaf
        && (Is_a(Node, x)
            && (φ (Destruct(Node, 1, x)) && φ (Destruct(Node, 2, x)))
            ==> φ x)

Split (not (size Leaf <= 0)
       && (not (size x <= 0)
           || not
              (Is_a(Node, x) && not (size (Destruct(Node, 1, x)) <= 0)
               && not (size (Destruct(Node, 2, x)) <= 0)))
       :cases [not (size Leaf <= 0);
               not (size x <= 0) || not Is_a(Node, x)
               || (size (Destruct(Node, 1, x)) <= 0)
               || (size (Destruct(Node, 2, x)) <= 0)])

subproof
not (size x <= 0) || not Is_a(Node, x) || (size (Destruct(Node, 1, x)) <= 0) || (size (Destruct(Node, 2, x)) <= 0)
- start[0.030s, "1"] not (size x <= 0) || not Is_a(Node, x) || (size (Destruct(Node, 1, x)) <= 0) || (size (Destruct(Node, 2, x)) <= 0)
- simplify
  into:
  true
  expansions:
  size
  rewrite_steps:
  forward_chaining:
subproof
not (size Leaf <= 0)
- start[0.030s, "2"] not (size Leaf <= 0)
- simplify
  into:
  true
  expansions:
  size
  rewrite_steps:
  forward_chaining:

digraph "proof" {
p_132 [label="Start (size ( :var_0: ) \> 0 :name \"Goal\" :time 0.030s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_132 -> p_130 [label=""];
subgraph cluster_131 {
  color=blue;
p_130 [label="Start (not (size x \<= 0) :name \"1\" :time 0.030s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_130 -> p_129 [label=""];
p_129 [label="Induct ((structural+ x),\l        :scheme φ Leaf\l                && (Is_a(Node, x)\l                    && (φ (Destruct(Node, 1, x))\l                        && φ (Destruct(Node, 2, x)))\l                    ==\> φ x))",shape=box,style=filled,fontname="courier",fontsize=14];
p_129 -> p_128 [label=""];
p_128 [label="Split (not (size Leaf \<= 0)\l       && (not (size x \<= 0)\l           \|\| not\l              (Is_a(Node, x) && not (size (Destruct(Node, 1, x)) \<= 0)\l               && not (size (Destruct(Node, 2, x)) \<= 0)))\l       :cases [not (size Leaf \<= 0);\l               not (size x \<= 0) \|\| not Is_a(Node, x)\l               \|\| (size (Destruct(Node, 1, x)) \<= 0)\l               \|\| (size (Destruct(Node, 2, x)) \<= 0)])",shape=box,style=filled,fontname="courier",fontsize=14];
p_128 -> p_123 [label=""];
subgraph cluster_124 {
  color=blue;
p_123 [label="Start (not (size x \<= 0) \|\| not Is_a(Node, x)\l       \|\| (size (Destruct(Node, 1, x)) \<= 0)\l       \|\| (size (Destruct(Node, 2, x)) \<= 0) :name \"1\" :time 0.030s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_123 -> p_122 [label=""];
p_122 [label="Simplify (true :expansions [size] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
}
p_128 -> p_126 [label=""];
subgraph cluster_127 {
  color=blue;
p_126 [label="Start (not (size Leaf \<= 0) :name \"2\" :time 0.030s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_126 -> p_125 [label=""];
p_125 [label="Simplify (true :expansions [size] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
}

Structural induction comes in both additive and multiplicative flavors.

This distinction only manifests when one is performing structural induction over multiple variables simultaneously. It affects the way base cases and inductive steps are mixed. Let's assume one needs to do induction on x, y:

addictive structural induction gives you 3 cases: two base cases φ(x_base, y), φ(x, y_base) and one inductive step φ(x,y) ==> φ(step(x), step(y))
multiplicative structural induction gives you 4 cases: one base case φ(x_base, y_base) and three inductive steps φ(x, y_base) ==> φ(step(x), y_base), φ(x_base, y) ==> φ(x_base, step(y)) and φ(x,y) ==> φ(step(x), step(y))

We can see the difference using the following function:

Try this!

In [11]:

let rec interleave_strict x y = match x, y with
  | [], _ | _ , [] -> []
  | x::xs, y::ys -> x::y::(interleave_strict xs ys)

Out[11]:

val interleave_strict : 'a list -> 'a list -> 'a list = <fun>

termination proof

Termination proof

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

original:

interleave_strict x y

sub:

interleave_strict (List.tl x) (List.tl y)

original ordinal:

Ordinal.Int (_cnt x)

sub ordinal:

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

path:

[y <> [] && x <> []]

proof:

detailed proof

summary
full

ground_instances:

definitions:

inductions:

search_time:

0.011s

details:

Expand

smt_stats:

num checks:	8
arith assert lower:	7
arith tableau max rows:	5
arith tableau max columns:	12
arith pivots:	6
rlimit count:	1992
mk clause:	13
datatype occurs check:	17
mk bool var:	71
arith assert upper:	7
datatype splits:	2
decisions:	13
arith row summations:	9
propagations:	14
conflicts:	7
arith fixed eqs:	4
datatype accessor ax:	11
arith conflicts:	1
arith num rows:	5
arith assert diseq:	1
datatype constructor ax:	12
num allocs:	1423325949
final checks:	4
added eqs:	57
del clause:	5
arith eq adapter:	8
memory:	18.440000
max memory:	18.610000

Expand

start[0.011s]
  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
  y <> [] && (x <> [] && ((_x_0 >= 0) && (_x_2 >= 0)))
  ==> not ((List.tl 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.tl y) <> [] && _x_0 <> []) \|\| Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) \|\| not (y <> [] && x <> [] && (_x_2 >= 0) && (_x_1 >= 0))
expansions:	[]
rewrite_steps:
forward_chaining:

unroll

expr:	(\|Ordinal.<<\| (\|Ordinal.Int_79/boot\| (\|count.list_1131/server\| (\|g…
expansions:

unroll

expr:	(\|count.list_1131/server\| (\|get.::.1_1104/server\| x_1118/server))
expansions:

unroll

expr:	(\|count.list_1131/server\| x_1118/server)
expansions:

Unsat

Let's prove that the length of interleave_strict x y is always less than or equal to the sum of the lengths of x and y. We'll do it first using additive and then using multiplicative structural induction:

Try this!

In [12]:

verify (fun x y ->
  List.length @@ interleave_strict x y <= List.length x + List.length y)
[@@induct structural_add (x,y)]

Out[12]:

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

List.length @@ interleave_strict x y <= List.length x + List.length y.

1 nontautological subgoal.

Induction scheme:

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

3 nontautological subgoals.

Subgoal 3:

|---------------------------------------------------------------------------
 List.length (interleave_strict x []) <= List.length x + List.length []

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

Subgoal 2:

|---------------------------------------------------------------------------
 List.length (interleave_strict [] y) <= List.length [] + List.length y

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

Subgoal 1:

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

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

Subgoal 1':

 H0. y <> []
 H1. x <> []
 H2. List.length (interleave_strict (List.tl x) (List.tl y))
     <= List.length (List.tl x) + List.length (List.tl y)
|---------------------------------------------------------------------------
 List.length ((List.hd y) :: (interleave_strict (List.tl x) (List.tl y)))
 <= 1 + List.length (List.tl x) + List.length (List.tl y)

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

 ⓘ  Rules:
    (:def List.length)
    (:def interleave_strict)
    (:fc List.len_nonnegative)
    (:induct struct list)

Proved

proof

ground_instances:	0
definitions:	11
inductions:	1
search_time:	0.171s

Expand

start[0.171s, "Goal"]
  List.length (interleave_strict ( :var_0: ) ( :var_1: ))
  <= List.length ( :var_0: ) + List.length ( :var_1: )

subproof

List.length (interleave_strict x y) <= List.length x + List.length y

start[0.170s, "1"]
  List.length (interleave_strict x y) <= List.length x + List.length y

induction on (structural+ x, y)
:scheme φ x []
        && (φ [] y
            && (y <> [] && (x <> [] && φ (List.tl x) (List.tl y)) ==> φ x y))

Split (let (_x_0 : int) = List.length x in
       let (_x_1 : int) = List.length [] in
       let (_x_2 : int) = List.length y in
       let (_x_3 : sko_ty_0 list) = List.tl x in
       let (_x_4 : sko_ty_0 list) = List.tl y in
       (List.length (interleave_strict x []) <= _x_0 + _x_1)
       && (List.length (interleave_strict [] y) <= _x_1 + _x_2)
       && (not
           (y <> [] && x <> []
            && (List.length (interleave_strict _x_3 _x_4)
                <= List.length _x_3 + List.length _x_4))
           || (List.length (interleave_strict x y) <= _x_0 + _x_2))
       :cases [List.length (interleave_strict x [])
               <= List.length x + List.length [];
               List.length (interleave_strict [] y)
               <= List.length [] + List.length y;
               let (_x_0 : sko_ty_0 list) = List.tl x in
               let (_x_1 : sko_ty_0 list) = List.tl y in
               not (y <> []) || not (x <> [])
               || not
                  (List.length (interleave_strict _x_0 _x_1)
                   <= List.length _x_0 + List.length _x_1)
               || (List.length (interleave_strict x y)
                   <= List.length x + List.length y)])

subproof

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

start[0.170s, "1"]
  let (_x_0 : sko_ty_0 list) = List.tl x in
  let (_x_1 : sko_ty_0 list) = List.tl y in
  not (y <> []) || not (x <> [])
  || not
     (List.length (interleave_strict _x_0 _x_1)
      <= List.length _x_0 + List.length _x_1)
  || (List.length (interleave_strict x y) <= List.length x + List.length y)

simplify

into:	let (_x_0 : sko_ty_0 list) = List.tl x in let (_x_1 : sko_ty_0 list) = List.tl y in let (_x_2 : sko_ty_0 list) = interleave_strict _x_0 _x_1 in let (_x_3 : int) = List.length _x_0 in let (_x_4 : int) = List.length _x_1 in (List.length ((List.hd y) :: _x_2) <= 1 + _x_3 + _x_4) \|\| not (y <> []) \|\| not (x <> []) \|\| not (List.length _x_2 <= _x_3 + _x_4)
expansions:	[List.length, List.length, List.length, interleave_strict]
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 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 List.len_nonnegative List.len_nonnegative List.len_nonnegative

simplify

into:	true
expansions:	List.length
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 List.len_nonnegative List.len_nonnegative List.len_nonnegative List.len_nonnegative List.len_nonnegative

subproof
List.length (interleave_strict [] y) <= List.length [] + List.length y
- start[0.170s, "2"] List.length (interleave_strict [] y) <= List.length [] + List.length y
- simplify
  into:
  true
  expansions:
  [List.length, List.length, interleave_strict]
  rewrite_steps:
  forward_chaining:
  List.len_nonnegative
  List.len_nonnegative
  List.len_nonnegative
subproof
List.length (interleave_strict x []) <= List.length x + List.length []
- start[0.170s, "3"] List.length (interleave_strict x []) <= List.length x + List.length []
- simplify
  into:
  true
  expansions:
  [List.length, List.length, interleave_strict]
  rewrite_steps:
  forward_chaining:
  List.len_nonnegative
  List.len_nonnegative
  List.len_nonnegative

digraph "proof" {
p_153 [label="Start (List.length (interleave_strict ( :var_0: ) ( :var_1: ))\l       \<= List.length ( :var_0: ) + List.length ( :var_1: ) :name \"Goal\"\l       :time 0.171s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_153 -> p_151 [label=""];
subgraph cluster_152 {
  color=blue;
p_151 [label="Start (List.length (interleave_strict x y) \<= List.length x + List.length y\l       :name \"1\" :time 0.170s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_151 -> p_150 [label=""];
p_150 [label="Induct ((structural+ x, y),\l        :scheme φ x []\l                && (φ [] y\l                    && (y \<\> [] && (x \<\> [] && φ (List.tl x) (List.tl y))\l                        ==\> φ x y)))",shape=box,style=filled,fontname="courier",fontsize=14];
p_150 -> p_149 [label=""];
p_149 [label="Split (let (_x_0 : int) = List.length x in\l       let (_x_1 : int) = List.length [] in\l       let (_x_2 : int) = List.length y in\l       let (_x_3 : sko_ty_0 list) = List.tl x in\l       let (_x_4 : sko_ty_0 list) = List.tl y in\l       (List.length (interleave_strict x []) \<= _x_0 + _x_1)\l       && (List.length (interleave_strict [] y) \<= _x_1 + _x_2)\l       && (not\l           (y \<\> [] && x \<\> []\l            && (List.length (interleave_strict _x_3 _x_4)\l                \<= List.length _x_3 + List.length _x_4))\l           \|\| (List.length (interleave_strict x y) \<= _x_0 + _x_2))\l       :cases [List.length (interleave_strict x [])\l               \<= List.length x + List.length [];\l               List.length (interleave_strict [] y)\l               \<= List.length [] + List.length y;\l               let (_x_0 : sko_ty_0 list) = List.tl x in\l               let (_x_1 : sko_ty_0 list) = List.tl y in\l               not (y \<\> []) \|\| not (x \<\> [])\l               \|\| not\l                  (List.length (interleave_strict _x_0 _x_1)\l                   \<= List.length _x_0 + List.length _x_1)\l               \|\| (List.length (interleave_strict x y)\l                   \<= List.length x + List.length y)])",shape=box,style=filled,fontname="courier",fontsize=14];
p_149 -> p_141 [label=""];
subgraph cluster_142 {
  color=blue;
p_141 [label="Start (let (_x_0 : sko_ty_0 list) = List.tl x in\l       let (_x_1 : sko_ty_0 list) = List.tl y in\l       not (y \<\> []) \|\| not (x \<\> [])\l       \|\| not\l          (List.length (interleave_strict _x_0 _x_1)\l           \<= List.length _x_0 + List.length _x_1)\l       \|\| (List.length (interleave_strict x y)\l           \<= List.length x + List.length y)\l       :name \"1\" :time 0.170s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_141 -> p_140 [label=""];
p_140 [label="Simplify (let (_x_0 : sko_ty_0 list) = List.tl x in\l          let (_x_1 : sko_ty_0 list) = List.tl y in\l          let (_x_2 : sko_ty_0 list) = interleave_strict _x_0 _x_1 in\l          let (_x_3 : int) = List.length _x_0 in\l          let (_x_4 : int) = List.length _x_1 in\l          (List.length ((List.hd y) :: _x_2) \<= 1 + _x_3 + _x_4)\l          \|\| not (y \<\> []) \|\| not (x \<\> [])\l          \|\| not (List.length _x_2 \<= _x_3 + _x_4)\l          :expansions [List.length;\l                       List.length;\l                       List.length;\l                       interleave_strict]\l          :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;\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;\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_140 -> p_139 [label=""];
p_139 [label="Simplify (true :expansions [List.length] :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;\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_149 -> p_144 [label=""];
subgraph cluster_145 {
  color=blue;
p_144 [label="Start (List.length (interleave_strict [] y) \<= List.length [] + List.length y\l       :name \"2\" :time 0.170s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_144 -> p_143 [label=""];
p_143 [label="Simplify (true :expansions [List.length; List.length; interleave_strict]\l          :rw []\l          :fc [List.len_nonnegative;\l               List.len_nonnegative;\l               List.len_nonnegative])",shape=box,style=filled,fontname="courier",fontsize=14];
}
p_149 -> p_147 [label=""];
subgraph cluster_148 {
  color=blue;
p_147 [label="Start (List.length (interleave_strict x []) \<= List.length x + List.length []\l       :name \"3\" :time 0.170s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_147 -> p_146 [label=""];
p_146 [label="Simplify (true :expansions [List.length; List.length; interleave_strict]\l          :rw []\l          :fc [List.len_nonnegative;\l               List.len_nonnegative;\l               List.len_nonnegative])",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
}

Try this!

In [13]:

verify (fun x y ->
  List.length @@ interleave_strict x y <= List.length x + List.length y)
[@@induct structural_mult (x,y)]

Out[13]:

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

List.length @@ interleave_strict x y <= List.length x + List.length y.

1 nontautological subgoal.

Induction scheme:

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

4 nontautological subgoals.

Subgoal 4:

|---------------------------------------------------------------------------
 List.length (interleave_strict [] []) <= 2 * List.length []

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

Subgoal 3:

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

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

Subgoal 2:

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

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

Subgoal 1:

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

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

Subgoal 1':

 H0. y <> []
 H1. x <> []
 H2. List.length (interleave_strict (List.tl x) (List.tl y))
     <= List.length (List.tl x) + List.length (List.tl y)
|---------------------------------------------------------------------------
 List.length ((List.hd y) :: (interleave_strict (List.tl x) (List.tl y)))
 <= 1 + List.length (List.tl x) + List.length (List.tl y)

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

 ⓘ  Rules:
    (:def List.length)
    (:def interleave_strict)
    (:fc List.len_nonnegative)
    (:induct struct list)

Proved

proof

ground_instances:	0
definitions:	16
inductions:	1
search_time:	0.118s

Expand

start[0.118s, "Goal"]
  List.length (interleave_strict ( :var_0: ) ( :var_1: ))
  <= List.length ( :var_0: ) + List.length ( :var_1: )

subproof

List.length (interleave_strict x y) <= List.length x + List.length y

start[0.118s, "1"]
  List.length (interleave_strict x y) <= List.length x + List.length y

induction on (structural* x, y)
:scheme φ [] []
        && ((y <> [] && φ [] (List.tl y) ==> φ [] y)
            && ((x <> [] && φ (List.tl x) [] ==> φ x [])
                && (y <> [] && (x <> [] && φ (List.tl x) (List.tl y))
                    ==> φ x y)))

Split (let (_x_0 : int) = List.length [] in
       let (_x_1 : bool) = y <> [] in
       let (_x_2 : sko_ty_0 list) = List.tl y in
       let (_x_3 : int) = List.length _x_2 in
       let (_x_4 : int) = List.length y in
       let (_x_5 : bool) = x <> [] in
       let (_x_6 : sko_ty_0 list) = List.tl x in
       let (_x_7 : int) = List.length _x_6 in
       let (_x_8 : int) = List.length x in
       (List.length (interleave_strict [] []) <= 2 * _x_0)
       && (not
           (_x_1 && (List.length (interleave_strict [] _x_2) <= _x_0 + _x_3))
           || (List.length (interleave_strict [] y) <= _x_0 + _x_4))
       && (not
           (_x_5 && (List.length (interleave_strict _x_6 []) <= _x_7 + _x_0))
           || (List.length (interleave_strict x []) <= _x_8 + _x_0))
       && (not
           (_x_1 && _x_5
            && (List.length (interleave_strict _x_6 _x_2) <= _x_7 + _x_3))
           || (List.length (interleave_strict x y) <= _x_8 + _x_4))
       :cases [List.length (interleave_strict [] []) <= 2 * List.length [];
               let (_x_0 : sko_ty_0 list) = List.tl y in
               let (_x_1 : int) = List.length [] in
               not (y <> [])
               || not
                  (List.length (interleave_strict [] _x_0)
                   <= _x_1 + List.length _x_0)
               || (List.length (interleave_strict [] y)
                   <= _x_1 + List.length y);
               let (_x_0 : sko_ty_0 list) = List.tl x in
               let (_x_1 : int) = List.length [] in
               not (x <> [])
               || not
                  (List.length (interleave_strict _x_0 [])
                   <= List.length _x_0 + _x_1)
               || (List.length (interleave_strict x [])
                   <= List.length x + _x_1);
               let (_x_0 : sko_ty_0 list) = List.tl x in
               let (_x_1 : sko_ty_0 list) = List.tl y in
               not (y <> []) || not (x <> [])
               || not
                  (List.length (interleave_strict _x_0 _x_1)
                   <= List.length _x_0 + List.length _x_1)
               || (List.length (interleave_strict x y)
                   <= List.length x + List.length y)])

subproof

start[0.118s, "1"]
  let (_x_0 : sko_ty_0 list) = List.tl x in
  let (_x_1 : sko_ty_0 list) = List.tl y in
  not (y <> []) || not (x <> [])
  || not
     (List.length (interleave_strict _x_0 _x_1)
      <= List.length _x_0 + List.length _x_1)
  || (List.length (interleave_strict x y) <= List.length x + List.length y)

simplify

into:	let (_x_0 : sko_ty_0 list) = List.tl x in let (_x_1 : sko_ty_0 list) = List.tl y in let (_x_2 : sko_ty_0 list) = interleave_strict _x_0 _x_1 in let (_x_3 : int) = List.length _x_0 in let (_x_4 : int) = List.length _x_1 in not (y <> []) \|\| not (x <> []) \|\| not (List.length _x_2 <= _x_3 + _x_4) \|\| (List.length ((List.hd y) :: _x_2) <= 1 + _x_3 + _x_4)
expansions:	[List.length, List.length, List.length, interleave_strict]
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 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 List.len_nonnegative List.len_nonnegative List.len_nonnegative

simplify

into:	true
expansions:	List.length
rewrite_steps:
forward_chaining:	List.len_nonnegative List.len_nonnegative List.len_nonnegative List.len_nonnegative

subproof

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

start[0.118s, "2"]
  let (_x_0 : sko_ty_0 list) = List.tl x in
  let (_x_1 : int) = List.length [] in
  not (x <> [])
  || not (List.length (interleave_strict _x_0 []) <= List.length _x_0 + _x_1)
  || (List.length (interleave_strict x []) <= List.length x + _x_1)

simplify

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

subproof

let (_x_0 : sko_ty_0 list) = List.tl y in let (_x_1 : int) = List.length [] in not (y <> []) || not (List.length (interleave_strict [] _x_0) <= _x_1 + List.length _x_0) || (List.length (interleave_strict [] y) <= _x_1 + List.length y)

start[0.118s, "3"]
  let (_x_0 : sko_ty_0 list) = List.tl y in
  let (_x_1 : int) = List.length [] in
  not (y <> [])
  || not (List.length (interleave_strict [] _x_0) <= _x_1 + List.length _x_0)
  || (List.length (interleave_strict [] y) <= _x_1 + List.length y)

simplify

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

subproof
List.length (interleave_strict [] []) <= 2 * List.length []
- start[0.118s, "4"] List.length (interleave_strict [] []) <= 2 * List.length []
- simplify
  into:
  true
  expansions:
  [List.length, List.length, interleave_strict]
  rewrite_steps:
  forward_chaining:
  List.len_nonnegative
  List.len_nonnegative

digraph "proof" {
p_171 [label="Start (List.length (interleave_strict ( :var_0: ) ( :var_1: ))\l       \<= List.length ( :var_0: ) + List.length ( :var_1: ) :name \"Goal\"\l       :time 0.118s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_171 -> p_169 [label=""];
subgraph cluster_170 {
  color=blue;
p_169 [label="Start (List.length (interleave_strict x y) \<= List.length x + List.length y\l       :name \"1\" :time 0.118s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_169 -> p_168 [label=""];
p_168 [label="Induct ((structural* x, y),\l        :scheme φ [] []\l                && ((y \<\> [] && φ [] (List.tl y) ==\> φ [] y)\l                    && ((x \<\> [] && φ (List.tl x) [] ==\> φ x [])\l                        && (y \<\> []\l                            && (x \<\> [] && φ (List.tl x) (List.tl y))\l                            ==\> φ x y))))",shape=box,style=filled,fontname="courier",fontsize=14];
p_168 -> p_167 [label=""];
p_167 [label="Split (let (_x_0 : int) = List.length [] in\l       let (_x_1 : bool) = y \<\> [] in\l       let (_x_2 : sko_ty_0 list) = List.tl y in\l       let (_x_3 : int) = List.length _x_2 in\l       let (_x_4 : int) = List.length y in\l       let (_x_5 : bool) = x \<\> [] in\l       let (_x_6 : sko_ty_0 list) = List.tl x in\l       let (_x_7 : int) = List.length _x_6 in\l       let (_x_8 : int) = List.length x in\l       (List.length (interleave_strict [] []) \<= 2 * _x_0)\l       && (not\l           (_x_1 && (List.length (interleave_strict [] _x_2) \<= _x_0 + _x_3))\l           \|\| (List.length (interleave_strict [] y) \<= _x_0 + _x_4))\l       && (not\l           (_x_5 && (List.length (interleave_strict _x_6 []) \<= _x_7 + _x_0))\l           \|\| (List.length (interleave_strict x []) \<= _x_8 + _x_0))\l       && (not\l           (_x_1 && _x_5\l            && (List.length (interleave_strict _x_6 _x_2) \<= _x_7 + _x_3))\l           \|\| (List.length (interleave_strict x y) \<= _x_8 + _x_4))\l       :cases [List.length (interleave_strict [] []) \<= 2 * List.length [];\l               let (_x_0 : sko_ty_0 list) = List.tl y in\l               let (_x_1 : int) = List.length [] in\l               not (y \<\> [])\l               \|\| not\l                  (List.length (interleave_strict [] _x_0)\l                   \<= _x_1 + List.length _x_0)\l               \|\| (List.length (interleave_strict [] y)\l                   \<= _x_1 + List.length y);\l               let (_x_0 : sko_ty_0 list) = List.tl x in\l               let (_x_1 : int) = List.length [] in\l               not (x \<\> [])\l               \|\| not\l                  (List.length (interleave_strict _x_0 [])\l                   \<= List.length _x_0 + _x_1)\l               \|\| (List.length (interleave_strict x [])\l                   \<= List.length x + _x_1);\l               let (_x_0 : sko_ty_0 list) = List.tl x in\l               let (_x_1 : sko_ty_0 list) = List.tl y in\l               not (y \<\> []) \|\| not (x \<\> [])\l               \|\| not\l                  (List.length (interleave_strict _x_0 _x_1)\l                   \<= List.length _x_0 + List.length _x_1)\l               \|\| (List.length (interleave_strict x y)\l                   \<= List.length x + List.length y)])",shape=box,style=filled,fontname="courier",fontsize=14];
p_167 -> p_156 [label=""];
subgraph cluster_157 {
  color=blue;
p_156 [label="Start (let (_x_0 : sko_ty_0 list) = List.tl x in\l       let (_x_1 : sko_ty_0 list) = List.tl y in\l       not (y \<\> []) \|\| not (x \<\> [])\l       \|\| not\l          (List.length (interleave_strict _x_0 _x_1)\l           \<= List.length _x_0 + List.length _x_1)\l       \|\| (List.length (interleave_strict x y)\l           \<= List.length x + List.length y)\l       :name \"1\" :time 0.118s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_156 -> p_155 [label=""];
p_155 [label="Simplify (let (_x_0 : sko_ty_0 list) = List.tl x in\l          let (_x_1 : sko_ty_0 list) = List.tl y in\l          let (_x_2 : sko_ty_0 list) = interleave_strict _x_0 _x_1 in\l          let (_x_3 : int) = List.length _x_0 in\l          let (_x_4 : int) = List.length _x_1 in\l          not (y \<\> []) \|\| not (x \<\> [])\l          \|\| not (List.length _x_2 \<= _x_3 + _x_4)\l          \|\| (List.length ((List.hd y) :: _x_2) \<= 1 + _x_3 + _x_4)\l          :expansions [List.length;\l                       List.length;\l                       List.length;\l                       interleave_strict]\l          :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;\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;\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_155 -> p_154 [label=""];
p_154 [label="Simplify (true :expansions [List.length] :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_167 -> p_159 [label=""];
subgraph cluster_160 {
  color=blue;
p_159 [label="Start (let (_x_0 : sko_ty_0 list) = List.tl x in\l       let (_x_1 : int) = List.length [] in\l       not (x \<\> [])\l       \|\| not\l          (List.length (interleave_strict _x_0 []) \<= List.length _x_0 + _x_1)\l       \|\| (List.length (interleave_strict x []) \<= List.length x + _x_1)\l       :name \"2\" :time 0.118s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_159 -> p_158 [label=""];
p_158 [label="Simplify (true\l          :expansions [List.length;\l                       List.length;\l                       List.length;\l                       interleave_strict]\l          :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_167 -> p_162 [label=""];
subgraph cluster_163 {
  color=blue;
p_162 [label="Start (let (_x_0 : sko_ty_0 list) = List.tl y in\l       let (_x_1 : int) = List.length [] in\l       not (y \<\> [])\l       \|\| not\l          (List.length (interleave_strict [] _x_0) \<= _x_1 + List.length _x_0)\l       \|\| (List.length (interleave_strict [] y) \<= _x_1 + List.length y)\l       :name \"3\" :time 0.118s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_162 -> p_161 [label=""];
p_161 [label="Simplify (true\l          :expansions [List.length;\l                       List.length;\l                       List.length;\l                       interleave_strict]\l          :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_167 -> p_165 [label=""];
subgraph cluster_166 {
  color=blue;
p_165 [label="Start (List.length (interleave_strict [] []) \<= 2 * List.length [] :name \"4\"\l       :time 0.118s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_165 -> p_164 [label=""];
p_164 [label="Simplify (true :expansions [List.length; List.length; interleave_strict]\l          :rw [] :fc [List.len_nonnegative; List.len_nonnegative])",shape=box,style=filled,fontname="courier",fontsize=14];
}
}
}

Imandra was able to prove the property using both flavors of structural induction, but we can see that the proof using the additive flavor was shorter. Multiplicative schemes will often result in longer proofs than additive schemes, and thus Imandra uses the additive flavor by default when [@@induct structural ...] is used.

into:	let (_x_0 : bool) = n = 1 in let (_x_1 : bool) = sum n = (n * (1 + n)) / 2 in (not _x_0 \|\| _x_1) && (_x_0 \|\| not (n <= 0) \|\| not (n >= 0) \|\| _x_1)
expansions:	[]
rewrite_steps:
forward_chaining: