# 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 -> 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
ground_instances:1
definitions:0
inductions:0
search_time:
0.022s
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: 5.37425e+06 final checks: 1 added eqs: 4 del clause: 5 arith eq adapter: 2 memory: 15.2 max memory: 15.2
Expand
• start[0.022s]
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_380/server 1) (+ (- 1) n_380/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.

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:

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

(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.144s
Expand
• start[0.144s, "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.144s, "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.107s, "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.107s, "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:
In :
verify (fun lst ->
List.for_all (fun x -> x > 0) lst ==>
List.fold_right (+) ~base:1 lst > 0)
[@@auto]

Out:
- : 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.172s
Expand
• start[0.172s, "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.172s, "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.124s, "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.124s, "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:

## 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 -> 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.148s
Expand
• start[0.148s, "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.148s, "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.064s, "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_nonnegative
• ##### subproof
not (n <= 0) || not (n >= 0) || (List.length (repeat c n) = n)
• start[0.064s, "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 : 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
ground_instances:1
definitions:0
inductions:0
search_time:
0.018s
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: 7.65005e+08 final checks: 1 added eqs: 4 del clause: 5 arith eq adapter: 2 memory: 17.33 max memory: 17.71
Expand
• start[0.018s]
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_834/server 1) (+ (- 1) n_834/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
ground_instances:1
definitions:0
inductions:0
search_time:
0.009s
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: 8.06279e+08 final checks: 1 added eqs: 4 del clause: 5 arith eq adapter: 4 memory: 17.57 max memory: 17.71
Expand
• start[0.009s]
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_860/server 1) (+ (- 1) n_860/server)… expansions:
• Unsat
In :
verify (fun n -> n >= 0 ==> sum n = (n * (n+1)) / 2) [@@induct functional induct_scheme]

Out:
- : 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.100s
Expand
• start[0.100s, "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.100s, "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.099s, "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.099s, "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 -> 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
ground_instances:3
definitions:0
inductions:0
search_time:
0.011s
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: 5676 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: 1.25554e+09 final checks: 5 added eqs: 55 del clause: 5 arith ineq splits: 1 arith eq adapter: 8 memory: 17.92 max memory: 17.99
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 : ty_0 tree) = Destruct(Node, 1, x) in let (_x_1 : int) = count.tree (const 0) x in let (_x_2 : int) = count.tree (const 0) _x_0 in Is_a(Leaf, _x_0) || not (not Is_a(Leaf, x) && (_x_1 >= 0) && (_x_2 >= 0)) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_1) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.tree_987/server| (|get.Node.1_967/serve… expansions:
• unroll
 expr: (|count.tree_987/server| (|get.Node.1_967/server| x_974/server)) expansions:
• unroll
 expr: (|count.tree_987/server| x_974/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
ground_instances:3
definitions:0
inductions:0
search_time:
0.014s
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: 1.20856e+09 final checks: 5 added eqs: 55 del clause: 5 arith ineq splits: 1 arith eq adapter: 8 memory: 17.87 max memory: 17.99
Expand
• start[0.014s]
let (_x_0 : ty_0 tree) = Destruct(Node, 2, …) in
let (_x_1 : int) = count.tree (const 0) _x_0 in
let (_x_2 : bool) = Is_a(Leaf, _x_0) in
not Is_a(Leaf, x) && ((count.tree (const 0) x >= 0) && (_x_1 >= 0))
==> (_x_2 && _x_2)
|| Ordinal.( << ) (Ordinal.Int _x_1)
(Ordinal.Int (count.tree (const 0) …))
• ###### simplify
 into: let (_x_0 : ty_0 tree) = Destruct(Node, 2, …) in let (_x_1 : int) = count.tree (const 0) _x_0 in let (_x_2 : int) = count.tree (const 0) … in Is_a(Leaf, _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) || not (not Is_a(Leaf, …) && (_x_2 >= 0) && (_x_1 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.tree_987/server| (|get.Node.2_968/serve… expansions:
• unroll
 expr: (|count.tree_987/server| (|get.Node.2_968/server| x_974/server)) expansions:
• unroll
 expr: (|count.tree_987/server| x_974/server) 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.042s
Expand
• start[0.042s, "Goal"] size ( :var_0: ) > 0
• #### subproof

not (size x <= 0)
• start[0.042s, "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.041s, "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.041s, "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
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
ground_instances:3
definitions:0
inductions:0
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: 1.41945e+09 final checks: 4 added eqs: 57 del clause: 5 arith eq adapter: 8 memory: 18.41 max memory: 18.56
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_1125/server| (|g… expansions:
• unroll
 expr: (|count.list_1125/server| (|get.::.1_1098/server| x_1112/server)) expansions:
• unroll
 expr: (|count.list_1125/server| x_1112/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:

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.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 φ 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.117s, "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.117s, "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.117s, "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.147s
Expand
• start[0.147s, "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.147s, "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.146s, "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.146s, "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.146s, "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.146s, "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.