# 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)
In :
let rec repeat c n =
if n <= 0 then
[]
else
c :: (repeat c (n-1))

Out:
val repeat : 'a -> int -> 'a list = <fun>

termination proof

### Termination proof

call repeat c (n - 1) from repeat c n
originalrepeat c n
subrepeat c (n - 1)
original ordinalOrdinal.Int (_cnt n)
sub ordinalOrdinal.Int (_cnt (n - 1))
path[not (n <= 0)]
proof
detailed proof
ground_instances1
definitions0
inductions0
search_time
0.021s
details
Expand
smt_stats
 num checks 3 arith-make-feasible 5 arith-max-columns 11 arith-conflicts 1 rlimit count 1165 mk clause 5 datatype occurs check 2 mk bool var 18 arith-lower 3 decisions 2 arith-propagations 3 propagations 2 arith-bound-propagations-cheap 3 arith-max-rows 4 conflicts 2 datatype accessor ax 2 num allocs 9.3457e+08 final checks 1 added eqs 6 del clause 5 arith eq adapter 2 arith-upper 6 memory 11.29 max memory 24.34
Expand
• start[0.021s]
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.<<_119| (|Ordinal.Int_108| (ite (>= n_2675 1) (+ (- 1) n_2675) 0)) (|Ord… 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.

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

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

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

2 nontautological subgoals.

Subgoal 1.2:

H0. x = []
|---------------------------------------------------------------------------
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. not (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.320s
Expand
• start[0.320s, "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.320s, "1"]
List.append x (List.append y z) = List.append (List.append x y) z
• induction on (functional )
:scheme (x = [] ==> φ x y z)
&& (not (x = []) && φ (List.tl x) y z ==> φ x y z)
• Split (let (_x_0 : bool) = not (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 [not (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
(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 (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.083s, "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
(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
not (x = []) || List.append x (List.append y z) = List.append (List.append x y) z
• start[0.083s, "1.2"]
not (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
In :
lemma rev_append x y =
List.rev (x @ y) = List.rev y @ List.rev x
[@@auto]

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

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

2 nontautological subgoals.

Subgoal 1.2:

H0. x = []
|---------------------------------------------------------------------------
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. not (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.284s
Expand
• start[0.284s, "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.284s, "1"]
List.rev (List.append x y) = List.append (List.rev y) (List.rev x)
• induction on (functional )
:scheme (x = [] ==> φ x y) && (not (x = []) && φ (List.tl x) y ==> φ x y)
• Split (let (_x_0 : bool) = not (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 [not (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
(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 (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.217s, "1.1"]
let (_x_0 : sko_ty_0 list) = List.tl x in
let (_x_1 : sko_ty_0 list) = List.rev y in
(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.hd x] in let (_x_3 : sko_ty_0 list) = List.rev y in let (_x_4 : sko_ty_0 list) = List.rev _x_0 in (List.append _x_1 _x_2 = List.append _x_3 (List.append _x_4 _x_2) || x = []) || not (_x_1 = 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
not (x = []) || List.rev (List.append x y) = List.append (List.rev y) (List.rev x)
• start[0.217s, "1.2"]
not (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
In :
verify (fun lst ->
List.for_all (fun x -> x > 0) lst ==>
List.fold_right (+) ~base:1 lst > 0)
[@@auto]

Out:
- : int list -> bool = <fun>
Goal:

List.for_all (fun x -> x > 0) lst ==> List.fold_right ( + ) 1 lst > 0.

1 nontautological subgoal.

Subgoal 1:

H0. List.for_all (fun x -> x > 0) 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:

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

2 nontautological subgoals.

Subgoal 1.2:

H0. List.for_all (fun x -> x > 0) lst
H1. List.fold_right ( + ) 1 lst <= 0
H2. lst = []
|---------------------------------------------------------------------------
false

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

Subgoal 1.1:

H0. List.for_all (fun x -> x > 0) lst
H1. List.fold_right ( + ) 1 lst <= 0
H2. not (lst = [])
H3. not (List.for_all (fun x -> x > 0) (List.tl lst))
|| not (List.fold_right ( + ) 1 (List.tl 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.162s
Expand
• start[0.162s, "Goal"]
List.for_all (fun x -> x > 0) :var_0:
==> List.fold_right ( + ) 1 :var_0: > 0
• #### subproof

not (List.for_all (fun x -> x > 0) lst) || not (List.fold_right ( + ) 1 lst <= 0)
• start[0.162s, "1"]
not (List.for_all (fun x -> x > 0) lst)
|| not (List.fold_right ( + ) 1 lst <= 0)
• induction on (functional )
:scheme (lst = [] ==> φ lst)
&& (not (lst = []) && φ (List.tl lst) ==> φ lst)
• Split (let (_x_0 : bool)
= not (List.for_all (fun x -> x > 0) lst)
|| not (List.fold_right ( + ) 1 lst <= 0)
in
let (_x_1 : bool) = not (lst = []) in
let (_x_2 : int list) = List.tl lst in
(_x_0 || _x_1)
&& (_x_0
|| not
(_x_1
&& (not (List.for_all (fun x -> x > 0) _x_2)
|| not (List.fold_right ( + ) 1 _x_2 <= 0))))
:cases [(not (List.for_all (fun x -> x > 0) lst)
|| not (List.fold_right ( + ) 1 lst <= 0))
|| not (lst = []);
let (_x_0 : int list) = List.tl lst in
((not (List.for_all (fun x -> x > 0) lst)
|| not (List.fold_right ( + ) 1 lst <= 0))
|| lst = [])
|| not
(not (List.for_all (fun x -> x > 0) _x_0)
|| not (List.fold_right ( + ) 1 _x_0 <= 0))])
• ##### subproof
let (_x_0 : int list) = List.tl lst in ((not (List.for_all (fun x -> x > 0) lst) || not (List.fold_right ( + ) 1 lst <= 0)) || lst = []) || not (not (List.for_all (fun x -> x > 0) _x_0) || not (List.fold_right ( + ) 1 _x_0 <= 0))
• start[0.098s, "1.1"]
let (_x_0 : int list) = List.tl lst in
((not (List.for_all (fun x -> x > 0) lst)
|| not (List.fold_right ( + ) 1 lst <= 0))
|| lst = [])
|| not
(not (List.for_all (fun x -> x > 0) _x_0)
|| not (List.fold_right ( + ) 1 _x_0 <= 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 (fun x -> x > 0) lst) || not (List.fold_right ( + ) 1 lst <= 0)) || not (lst = [])
• start[0.098s, "1.2"]
(not (List.for_all (fun x -> x > 0) lst)
|| not (List.fold_right ( + ) 1 lst <= 0))
|| not (lst = [])
• ###### simplify
 into true expansions List.fold_right rewrite_steps forward_chaining

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

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

Out:
val repeat_len : 'a -> int -> 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.128s
Expand
• start[0.128s, "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.128s, "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) = List.length (repeat c n) = n in
let (_x_1 : bool) = not (n <= 0) in
let (_x_2 : bool) = not (n >= 0) in
let (_x_3 : int) = -1 + n in
((_x_0 || _x_1) || _x_2)
&& ((not
(_x_1 && (not (n >= 1) || List.length (repeat c _x_3) = _x_3))
|| _x_0)
|| _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.067s, "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_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegative
• ##### subproof
(not (n <= 0) || not (n >= 0)) || List.length (repeat c n) = n
• start[0.067s, "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

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.

In :
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:
val sum : int -> int = <fun>
val induct_scheme : int -> bool = <fun>

termination proof

### Termination proof

call sum (n - 1) from sum n
originalsum n
subsum (n - 1)
original ordinalOrdinal.Int (_cnt n)
sub ordinalOrdinal.Int (_cnt (n - 1))
path[not (n <= 0)]
proof
detailed proof
ground_instances1
definitions0
inductions0
search_time
0.017s
details
Expand
smt_stats
 num checks 3 arith-make-feasible 5 arith-max-columns 11 arith-conflicts 1 rlimit count 1165 mk clause 5 datatype occurs check 2 mk bool var 18 arith-lower 3 decisions 2 arith-propagations 3 propagations 2 arith-bound-propagations-cheap 3 arith-max-rows 4 conflicts 2 datatype accessor ax 2 num allocs 2.79694e+09 final checks 1 added eqs 6 del clause 5 arith eq adapter 2 arith-upper 6 memory 26.38 max memory 46.45
Expand
• start[0.017s]
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.<<_119| (|Ordinal.Int_108| (ite (>= n_3108 1) (+ (- 1) n_3108) 0)) (|Ord… expansions
• Unsat

termination proof

### Termination proof

call induct_scheme (n - 1) from induct_scheme n
originalinduct_scheme n
subinduct_scheme (n - 1)
original ordinalOrdinal.Int (_cnt n)
sub ordinalOrdinal.Int (_cnt (n - 1))
path[not (n = 1) && not (n <= 0)]
proof
detailed proof
ground_instances1
definitions0
inductions0
search_time
0.033s
details
Expand
smt_stats
 num checks 3 arith-make-feasible 5 arith-max-columns 12 arith-conflicts 1 rlimit count 1277 mk clause 5 datatype occurs check 2 mk bool var 22 arith-lower 3 arith-diseq 3 decisions 2 arith-propagations 5 propagations 3 arith-bound-propagations-cheap 5 arith-max-rows 5 conflicts 2 datatype accessor ax 2 num allocs 2.87353e+09 final checks 1 added eqs 6 del clause 5 arith eq adapter 4 arith-upper 8 memory 26.64 max memory 46.45
Expand
• start[0.033s]
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.<<_119| (|Ordinal.Int_108| (ite (>= n_3134 1) (+ (- 1) n_3134) 0)) (|Ord… expansions
• Unsat

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

Out:
- : int -> 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!

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.249s
Expand
• start[0.249s, "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.248s, "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.247s, "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.247s, "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

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.

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

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

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

Out:
val size : 'a tree -> int = <fun>

termination proof

### Termination proof

call size (Destruct(Node, 1, x)) from size x
originalsize x
subsize (Destruct(Node, 1, x))
original ordinalOrdinal.Int (_cnt x)
sub ordinalOrdinal.Int (_cnt (Destruct(Node, 1, x)))
path[Is_a(Node, x)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.017s
details
Expand
smt_stats
 num checks 8 arith-make-feasible 34 arith-max-columns 17 arith-conflicts 3 rlimit count 5874 mk clause 40 datatype occurs check 19 mk bool var 121 arith-lower 33 arith-diseq 4 datatype splits 5 decisions 37 arith-propagations 2 propagations 27 arith-bound-propagations-cheap 2 arith-max-rows 5 conflicts 11 datatype accessor ax 11 datatype constructor ax 25 num allocs 3.68093e+09 final checks 5 added eqs 110 del clause 23 arith eq adapter 23 arith-upper 24 memory 30.01 max memory 46.45
Expand
• start[0.017s]
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) = not Is_a(Node, _x_1) in
Is_a(Node, 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, 1, x) in let (_x_1 : int) = count.tree (const 0) _x_0 in let (_x_2 : int) = count.tree (const 0) x in (not Is_a(Node, _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not ((Is_a(Node, x) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count.tree (const 0)_3259| x_3246) expansions
• unroll
 expr (|count.tree (const 0)_3259| (|get.Node.1_3240| x_3246)) expansions
• unroll
 expr (|Ordinal.<<_119| (|Ordinal.Int_108| (|count.tree (const 0)_3259| … expansions
• Unsat

call size (Destruct(Node, 2, x)) from size x
originalsize x
subsize (Destruct(Node, 2, x))
original ordinalOrdinal.Int (_cnt x)
sub ordinalOrdinal.Int (_cnt (Destruct(Node, 2, x)))
path[Is_a(Node, x)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.016s
details
Expand
smt_stats
 num checks 8 arith-make-feasible 34 arith-max-columns 17 arith-conflicts 3 rlimit count 2937 mk clause 40 datatype occurs check 19 mk bool var 121 arith-lower 33 arith-diseq 4 datatype splits 5 decisions 37 arith-propagations 2 propagations 27 arith-bound-propagations-cheap 2 arith-max-rows 5 conflicts 11 datatype accessor ax 11 datatype constructor ax 25 num allocs 3.63722e+09 final checks 5 added eqs 110 del clause 23 arith eq adapter 23 arith-upper 24 memory 27.44 max memory 46.45
Expand
• start[0.016s]
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) = not Is_a(Node, _x_1) in
Is_a(Node, 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 (not Is_a(Node, _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not ((Is_a(Node, x) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count.tree (const 0)_3259| x_3246) expansions
• unroll
 expr (|count.tree (const 0)_3259| (|get.Node.2_3241| x_3246)) expansions
• unroll
 expr (|Ordinal.<<_119| (|Ordinal.Int_108| (|count.tree (const 0)_3259| … expansions
• Unsat

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

Out:
- : '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.033s
Expand
• start[0.033s, "Goal"] size :var_0: > 0
• #### subproof

not (size x <= 0)
• start[0.033s, "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.032s, "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.032s, "2"] not (size Leaf <= 0)
• ###### simplify
 into true expansions size rewrite_steps forward_chaining

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:

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

Out:
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
originalinterleave_strict x y
subinterleave_strict (List.tl x) (List.tl y)
original ordinalOrdinal.Int (_cnt x)
sub ordinalOrdinal.Int (_cnt (List.tl x))
path[not (x = [] || y = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.013s
details
Expand
smt_stats
 num checks 7 arith-make-feasible 10 arith-max-columns 13 arith-conflicts 1 rlimit count 2129 mk clause 3 datatype occurs check 31 mk bool var 66 arith-lower 4 datatype splits 6 decisions 17 propagations 2 arith-max-rows 5 conflicts 11 datatype accessor ax 7 datatype constructor ax 17 num allocs 4.01621e+09 final checks 6 added eqs 55 del clause 1 arith eq adapter 3 arith-upper 6 memory 27.99 max memory 46.45
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
not (x = [] || y = []) && _x_0 >= 0 && _x_2 >= 0
==> (_x_1 = [] || List.tl y = [])
|| 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 ((_x_0 = [] || List.tl y = []) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not ((not (x = [] || y = []) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count.list (const 0)_3386| x_3373) expansions
• unroll
 expr (|count.list (const 0)_3386| (|get.::.1_3365| x_3373)) expansions
• unroll
 expr (|Ordinal.<<_119| (|Ordinal.Int_108| (|count.list (const 0)_3386| (|get.::.… 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:

In :
verify (fun x y ->
List.length @@ interleave_strict x y <= List.length x + List.length y)

Out:
- : '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.127s
Expand
• start[0.127s, "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.127s, "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.127s, "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_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegative
• ###### simplify
 into true expansions List.length rewrite_steps forward_chaining List.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegative
• ##### subproof
List.length (interleave_strict [] y) <= (List.length [] + List.length y)
• start[0.127s, "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_nonnegativeList.len_nonnegativeList.len_nonnegative
• ##### subproof
List.length (interleave_strict x []) <= (List.length x + List.length [])
• start[0.127s, "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_nonnegativeList.len_nonnegativeList.len_nonnegative
In :
verify (fun x y ->
List.length @@ interleave_strict x y <= List.length x + List.length y)
[@@induct structural_mult (x,y)]

Out:
- : '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.129s
Expand
• start[0.129s, "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.129s, "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
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.128s, "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_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegative
• ###### simplify
 into true expansions List.length rewrite_steps forward_chaining List.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.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.128s, "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_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.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.128s, "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_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegative
• ##### subproof
List.length (interleave_strict [] []) <= (2 * List.length [])
• start[0.128s, "4"]
List.length (interleave_strict [] []) <= (2 * List.length [])
• ###### simplify
 into true expansions [List.length, List.length, interleave_strict] rewrite_steps forward_chaining List.len_nonnegativeList.len_nonnegative

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.