# Verifying Merge Sort in Imandra¶

Merge sort is a widely used efficient general purpose sorting algorithm invented by John von Neumann in 1945. It is a prototypical divide and conquer algorithm and forms the basis of standard library sorting functions in languages like OCaml, Java and Python.

Let's verify it in Imandra! ## The main idea¶

The main idea of merge sort is as follows:

• Divide the input list into sublists
• Sort the sublists
• Merge the sorted sublists to obtain a sorted version of the original list

## Merging two lists¶

We'll start by defining a function to merge two lists in a "sorted" way. Note that our termination proof involves both arguments l and m, using a lexicographic product (via the [@@adm l,m] admission annotation).

In :
let rec merge (l : int list) (m : int list) =
match l, m with
| [], _ -> m
| _, [] -> l
| a :: ls, b :: ms ->
if a < b then
a :: (merge ls m)
else
b :: (merge l ms)

Out:
val merge : Z.t list -> Z.t list -> Z.t list = <fun>

termination proof

### Termination proof

call merge (List.tl l) m from merge l m
original:merge l m
sub:merge (List.tl l) m
original ordinal:Ordinal.of_list [Ordinal.Int (_cnt l); Ordinal.Int (_cnt m)]
sub ordinal:Ordinal.of_list [Ordinal.Int (_cnt (List.tl l)); Ordinal.Int (_cnt m)]
path:[List.hd l < List.hd m && m <> [] && l <> []]
proof:
detailed proof
ground_instances:8
definitions:0
inductions:0
search_time:
0.014s
details:
Expand
smt_stats:
 arith offset eqs: 6 num checks: 18 arith assert lower: 134 arith tableau max rows: 20 arith tableau max columns: 42 arith pivots: 99 rlimit count: 49758 mk clause: 206 datatype occurs check: 224 mk bool var: 638 arith assert upper: 131 datatype splits: 40 decisions: 304 arith row summations: 223 arith bound prop: 3 propagations: 336 interface eqs: 10 conflicts: 36 arith fixed eqs: 85 arith assume eqs: 10 datatype accessor ax: 84 minimized lits: 2 arith conflicts: 6 arith num rows: 20 arith assert diseq: 30 datatype constructor ax: 94 num allocs: 1.20189e+07 final checks: 29 added eqs: 867 del clause: 149 arith eq adapter: 106 memory: 15.76 max memory: 15.98
Expand
• start[0.014s]
let (_x_0 : int) = List.hd m in
let (_x_1 : bool) = m <> [] in
let (_x_2 : bool) = count.list mk_nat m >= 0 in
let (_x_3 : int list) = List.tl l in
let (_x_4 : bool) = List.hd _x_3 < _x_0 in
let (_x_5 : bool) = _x_1 && _x_3 <> [] in
let (_x_6 : Ordinal.t) = if … <> [] then … else … in
(List.hd l < _x_0)
&& (_x_1
&& (l <> []
&& ((count.list mk_nat l >= 0)
&& (_x_2 && ((count.list mk_nat _x_3 >= 0) && _x_2)))))
==> (not (_x_4 && _x_5) && not (not _x_4 && _x_5))
|| Ordinal.( << ) _x_6 _x_6
• ###### simplify
 into: let (_x_0 : int list) = List.tl l in let (_x_1 : int) = count.list mk_nat _x_0 in let (_x_2 : Ordinal.t) = Ordinal.Int 1 in let (_x_3 : int) = count.list mk_nat m in let (_x_4 : Ordinal.t) = Ordinal.Int _x_3 in let (_x_5 : int) = count.list mk_nat l in let (_x_6 : int) = List.hd m in let (_x_7 : bool) = m <> [] in let (_x_8 : bool) = _x_6 <= List.hd _x_0 in let (_x_9 : bool) = _x_0 <> [] in Ordinal.( << ) (Ordinal.plus (Ordinal.shift (Ordinal.Int _x_1) _x_2) _x_4) (Ordinal.plus (Ordinal.shift (Ordinal.Int _x_5) _x_2) _x_4) || not (not (_x_6 <= List.hd l) && _x_7 && l <> [] && (_x_5 >= 0) && (_x_3 >= 0) && (_x_1 >= 0)) || (not (not _x_8 && _x_7 && _x_9) && not (_x_8 && _x_7 && _x_9)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (let ((a!1 (|Ordinal.shift| (|Ordinal.Int_79/boot| (|count.list_384/se… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift| (|Ordinal.Int_79/boot| (|count.list_384/se… expansions:
• unroll
 expr: (|Ordinal.shift| (|Ordinal.Int_79/boot| (|count.list_384/server| … expansions:
• unroll
 expr: (|count.list_384/server| (|get.::.1_368/server| l_369/server)) expansions:
• unroll
 expr: (|Ordinal.plus| (|Ordinal.shift| (|Ordinal.Int_79/boot| (|count.l… expansions:
• unroll
 expr: (|Ordinal.shift| (|Ordinal.Int_79/boot| (|count.list_384/server| l_369/server)) (|O… expansions:
• unroll
 expr: (|count.list_384/server| m_370/server) expansions:
• unroll
 expr: (|count.list_384/server| l_369/server) expansions:
• Unsat
call merge l (List.tl m) from merge l m
original:merge l m
sub:merge l (List.tl m)
original ordinal:Ordinal.of_list [Ordinal.Int (_cnt l); Ordinal.Int (_cnt m)]
sub ordinal:Ordinal.of_list [Ordinal.Int (_cnt l); Ordinal.Int (_cnt (List.tl m))]
path:[not (List.hd l < List.hd m) && m <> [] && l <> []]
proof:
detailed proof
ground_instances:12
definitions:0
inductions:0
search_time:
0.023s
details:
Expand
smt_stats:
 arith offset eqs: 20 num checks: 26 arith assert lower: 458 arith tableau max rows: 36 arith tableau max columns: 70 arith pivots: 208 rlimit count: 33926 mk clause: 428 datatype occurs check: 490 mk bool var: 1276 arith assert upper: 353 datatype splits: 73 decisions: 644 arith row summations: 501 arith bound prop: 24 propagations: 1261 interface eqs: 2 conflicts: 67 arith fixed eqs: 213 arith assume eqs: 2 datatype accessor ax: 148 minimized lits: 6 arith conflicts: 12 arith num rows: 36 arith assert diseq: 88 datatype constructor ax: 196 num allocs: 6.01952e+06 final checks: 35 added eqs: 1829 del clause: 333 arith eq adapter: 287 memory: 15.89 max memory: 15.98
Expand
• start[0.023s]
let (_x_0 : int) = List.hd l in
let (_x_1 : bool) = l <> [] in
let (_x_2 : bool) = count.list mk_nat l >= 0 in
let (_x_3 : int list) = List.tl m in
let (_x_4 : bool) = _x_0 < List.hd _x_3 in
let (_x_5 : bool) = _x_3 <> [] && _x_1 in
let (_x_6 : Ordinal.t) = if … <> [] then … else … in
not (_x_0 < List.hd m)
&& (m <> []
&& (_x_1
&& (_x_2
&& ((count.list mk_nat m >= 0)
&& (_x_2 && (count.list mk_nat _x_3 >= 0))))))
==> (not (_x_4 && _x_5) && not (not _x_4 && _x_5))
|| Ordinal.( << ) _x_6 _x_6
• ###### simplify
 into: let (_x_0 : int list) = List.tl m in let (_x_1 : int) = List.hd l in let (_x_2 : bool) = List.hd _x_0 <= _x_1 in let (_x_3 : bool) = _x_0 <> [] in let (_x_4 : bool) = l <> [] in let (_x_5 : Ordinal.t) = Ordinal.Int 1 in let (_x_6 : int) = count.list mk_nat … in (not (not _x_2 && _x_3 && _x_4) && not (_x_2 && _x_3 && _x_4)) || Ordinal.( << ) (Ordinal.plus (Ordinal.shift (Ordinal.Int (count.list mk_nat l)) _x_5) (Ordinal.Int (count.list mk_nat _x_0))) (Ordinal.plus (Ordinal.shift (Ordinal.Int …) _x_5) (Ordinal.Int _x_6)) || not ((List.hd … <= _x_1) && … <> [] && _x_4 && (… >= 0) && (_x_6 >= 0) && (count.list mk_nat (List.tl …) >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (let ((a!1 (|Ordinal.plus| (|Ordinal.shift| (|Ordinal.Int_79/boot| … expansions:
• unroll
 expr: (|Ordinal.plus| (|Ordinal.shift| (|Ordinal.Int_79/boot| (|count.l… expansions:
• unroll
 expr: (|Ordinal.plus| (|Ordinal.shift| (|Ordinal.Int_79/boot| (|count.l… expansions:
• unroll
 expr: (|Ordinal.shift| (|Ordinal.Int_79/boot| (|count.list_384/server| l_369/server)) (|O… expansions:
• unroll
 expr: (|count.list_384/server| (|get.::.1_368/server| m_370/server)) expansions:
• unroll
 expr: (|count.list_384/server| m_370/server) expansions:
• unroll
 expr: (|count.list_384/server| l_369/server) expansions:
• unroll
 expr: (|count.list_384/server| (|get.::.1_368/server| (|get.::.1_368/server| m_370/server))) expansions:
• unroll
 expr: (|count.list_384/server| (|get.::.1_368/server| l_369/server)) expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.plus| (|Ordinal.shift| (|Ordinal.Int_79/boot| … expansions:
• unroll
 expr: (let ((a!1 (|get.Ordinal.Cons.2_375/server| (|Ordinal.shift| (|Ordinal.Int_79/boot| … expansions:
• unroll
 expr: (let ((a!1 (|get.Ordinal.Cons.2_375/server| (|Ordinal.shift| (|Ordinal.Int_79/boot| … expansions:
• Unsat

Let's experiment a bit with merge.

In :
merge [1;2;3] [4;5;6]

Out:
- : Z.t list = [1;2;3;4;5;6]

In :
merge [1;4;5] [2;3;4]

Out:
- : Z.t list = [1;2;3;4;4;5]

In :
merge [1;5;2] [2;3]

Out:
- : Z.t list = [1;2;3;5;2]


Observe that merge will merge sorted lists in a manner that respects their sortedness. But, if the lists given to merge aren't sorted, the output of merge need not be sorted.

# Dividing into sublists¶

In merge sort, we need to divide a list into sublists. We'll do this in a simple way using the function odds which computes "every other" element of a list. We'll then be able to split a list x into sublists by taking odds x and odds (List.tl x).

In :
let rec odds l =
match l with
| []  -> []
| [x] -> [x]
| x :: y :: rst -> x :: odds rst

Out:
val odds : 'a list -> 'a list = <fun>

termination proof

### Termination proof

call odds (List.tl (List.tl l)) from odds l
original:odds l
sub:odds (List.tl (List.tl l))
original ordinal:Ordinal.Int (_cnt l)
sub ordinal:Ordinal.Int (_cnt (List.tl (List.tl l)))
path:[(List.tl l) <> [] && l <> []]
proof:
detailed proof
ground_instances:6
definitions:0
inductions:0
search_time:
0.011s
details:
Expand
smt_stats:
 num checks: 14 arith assert lower: 33 arith tableau max rows: 12 arith tableau max columns: 27 arith pivots: 24 rlimit count: 5485 mk clause: 82 datatype occurs check: 29 mk bool var: 196 arith assert upper: 30 datatype splits: 3 decisions: 80 arith row summations: 50 propagations: 87 conflicts: 19 arith fixed eqs: 26 datatype accessor ax: 18 arith conflicts: 2 arith num rows: 12 arith assert diseq: 2 datatype constructor ax: 27 num allocs: 2.04961e+07 final checks: 8 added eqs: 160 del clause: 42 arith eq adapter: 30 memory: 15.98 max memory: 15.98
Expand
• start[0.011s]
let (_x_0 : ty_0 list) = List.tl l in
let (_x_1 : int) = count.list (const 0) l in
let (_x_2 : ty_0 list) = List.tl _x_0 in
let (_x_3 : int) = count.list (const 0) _x_2 in
_x_0 <> [] && (l <> [] && ((_x_1 >= 0) && (_x_3 >= 0)))
==> not ((List.tl _x_2) <> [] && _x_2 <> [])
|| Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_1)
• ###### simplify
 into: let (_x_0 : ty_0 list) = List.tl l in let (_x_1 : ty_0 list) = List.tl _x_0 in let (_x_2 : int) = count.list (const 0) _x_1 in let (_x_3 : int) = count.list (const 0) l in not ((List.tl _x_1) <> [] && _x_1 <> []) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_3) || not (_x_0 <> [] && l <> [] && (_x_3 >= 0) && (_x_2 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (let ((a!1 (|Ordinal.Int_79/boot| (|count.list_543/server| (|get.::.1_52… expansions:
• unroll
 expr: (|count.list_543/server| (|get.::.1_525/server| (|get.::.1_525/server| l_532/server))) expansions:
• unroll
 expr: (|count.list_543/server| l_532/server) expansions:
• unroll
 expr: (|count.list_543/server| (|get.::.1_525/server| (|get.::.1_525/server| (|get.::.1_525/server| … expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.Int_79/boot| (|count.list_543/server| (|get.::.1_52… expansions:
• unroll
 expr: (|count.list_543/server| (|get.::.1_525/server| l_532/server)) expansions:
• Unsat

Let's compute a bit with odds to better understand how it works.

In :
odds [1;2;3;4;5;6]

Out:
- : Z.t list = [1;3;5]

In :
odds (List.tl [1;2;3;4;5;6])

Out:
- : Z.t list = [2;4;6]


# Defining Merge Sort¶

We can now put the pieces together and define our main merge_sort function, as follows:

In :
let rec merge_sort l =
match l with
| []  -> []
| [_] -> l
| _ :: ls -> merge (merge_sort (odds l)) (merge_sort (odds ls))

Out:
val merge_sort : Z.t list -> Z.t list = <fun>
Error:
unsupported: rejected definition for function merge_sort,
Imandra could not prove termination.
hint: problematic sub-call from merge_sort l
to merge_sort (odds (List.tl l))  under path
not Is_a([], List.tl l) and l <> []
could not be proved to decrease (measured subset: (l))
See https://docs.imandra.ai/imandra-docs/notebooks/proving-program-termination/
At jupyter cell 8:1,0--129
1 | let rec merge_sort l =
2 |  match l with
3 |   | []  -> []
4 |   | [_] -> l
5 |   | _ :: ls -> merge (merge_sort (odds l)) (merge_sort (odds ls))


To admit merge_sort into Imandra, we must prove it terminating. We can do this with a custom measure function which we'll call merge_sort_measure. We'll prove a lemma about odds (by functional induction) to make it clear why the measure is decreasing in every recursive call. We'll install the lemma as a forward_chaining rule, which is a good strategy for making it effective during termination analysis.

In :
let merge_sort_measure x =
Ordinal.of_int (List.length x)

Out:
val merge_sort_measure : 'a list -> Ordinal.t = <fun>

In :
theorem odds_len_1 x =
x <> [] && List.tl x <> []
==>
(List.length (odds x) [@trigger]) < List.length x
[@@induct functional odds] [@@forward_chaining]

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

(x <> []) && (List.tl x <> []) ==> List.length (odds x) < List.length x.

1 nontautological subgoal.

We shall induct according to a scheme derived from odds.

Induction scheme:

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

2 nontautological subgoals.

Subgoal 2:

H0. List.length x <= List.length (odds x)
H1. not (x = [])
H2. not (List.tl x = [])
|---------------------------------------------------------------------------
(List.tl x) <> [] && x <> []

But simplification reduces this to true, using the forward-chaining rule
List.len_nonnegative.

Subgoal 1:

H0. List.length x <= List.length (odds x)
H1. not (x = [])
H2. not (List.tl x = [])
H3. x <> []
H4. (List.tl x) <> []
H5. not
(List.length (List.tl (List.tl x))
<= List.length (odds (List.tl (List.tl x))))
|| not
(not (List.tl (List.tl x) = [])
&& not (List.tl (List.tl (List.tl x)) = []))
|---------------------------------------------------------------------------
false

This simplifies, using the definitions of List.length and odds to the
following 3 subgoals:

Subgoal 1.3:

H0. x <> []
H1. (List.tl x) <> []
H2. List.length (List.tl (List.tl x))
<= List.length (odds (List.tl (List.tl x)))
H3. List.tl (List.tl x) = []
H4. List.length (List.tl x) <= List.length (odds (List.tl (List.tl x)))
|---------------------------------------------------------------------------
false

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

Subgoal 1.2:

H0. x <> []
H1. (List.tl x) <> []
H2. List.length (List.tl (List.tl x))
<= List.length (odds (List.tl (List.tl x)))
H3. (List.tl (List.tl x)) <> []
H4. List.tl (List.tl (List.tl x)) = []
H5. List.length (List.tl x) <= List.length (odds (List.tl (List.tl x)))
|---------------------------------------------------------------------------
false

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

Subgoal 1.2':

H0. List.tl (List.tl (List.tl x)) = []
H1. (List.tl x) <> []
H2. x <> []
H3. (List.tl (List.tl x)) <> []
H4. List.length (List.tl (List.tl (List.tl x))) <= 0
H5. List.length (List.tl (List.tl x)) <= 0
|---------------------------------------------------------------------------
false

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

Subgoal 1.1:

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

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

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


Proved
proof
 ground_instances: 0 definitions: 22 inductions: 1 search_time: 0.235s
Expand
• start[0.235s, "Goal"]
not (( :var_0: ) = []) && not (List.tl ( :var_0: ) = [])
==> List.length (odds ( :var_0: )) < List.length ( :var_0: )
• #### subproof

not (List.length x <= List.length (odds x)) || (x = []) || (List.tl x = [])
• start[0.235s, "1"]
not (List.length x <= List.length (odds x)) || (x = []) || (List.tl x = [])
• induction on (functional odds)
:scheme (not ((List.tl x) <> [] && x <> []) ==> φ x)
&& (x <> [] && ((List.tl x) <> [] && φ (List.tl (List.tl x)))
==> φ x)
• Split (let (_x_0 : sko_ty_0 list) = List.tl x in
let (_x_1 : bool) = _x_0 <> [] in
let (_x_2 : bool) = x <> [] in
let (_x_3 : bool) = not (List.length x <= List.length (odds x)) in
let (_x_4 : bool) = not (not (x = []) && not (_x_0 = [])) in
let (_x_5 : sko_ty_0 list) = List.tl _x_0 in
((_x_1 && _x_2) || _x_3 || _x_4)
&& (_x_3 || _x_4
|| not
(_x_2 && _x_1
&& (not (List.length _x_5 <= List.length (odds _x_5))
|| not (not (_x_5 = []) && not (List.tl _x_5 = [])))))
:cases [let (_x_0 : sko_ty_0 list) = List.tl x in
not (List.length x <= List.length (odds x)) || (x = [])
|| (_x_0 = []) || (_x_0 <> [] && x <> []);
let (_x_0 : sko_ty_0 list) = List.tl x in
let (_x_1 : sko_ty_0 list) = List.tl _x_0 in
not (List.length x <= List.length (odds x)) || (x = [])
|| (_x_0 = []) || not (x <> []) || not (_x_0 <> [])
|| not
(not (List.length _x_1 <= List.length (odds _x_1))
|| not (not (_x_1 = []) && not (List.tl _x_1 = [])))])
• ##### subproof
let (_x_0 : sko_ty_0 list) = List.tl x in let (_x_1 : sko_ty_0 list) = List.tl _x_0 in not (List.length x <= List.length (odds x)) || (x = []) || (_x_0 = []) || not (x <> []) || not (_x_0 <> []) || not (not (List.length _x_1 <= List.length (odds _x_1)) || not (not (_x_1 = []) && not (List.tl _x_1 = [])))
• start[0.234s, "1"]
let (_x_0 : sko_ty_0 list) = List.tl x in
let (_x_1 : sko_ty_0 list) = List.tl _x_0 in
not (List.length x <= List.length (odds x)) || (x = []) || (_x_0 = [])
|| not (x <> []) || not (_x_0 <> [])
|| not
(not (List.length _x_1 <= List.length (odds _x_1))
|| not (not (_x_1 = []) && not (List.tl _x_1 = [])))
• ###### simplify
 into: let (_x_0 : sko_ty_0 list) = List.tl x in let (_x_1 : bool) = (x = []) || (_x_0 = []) in let (_x_2 : sko_ty_0 list) = List.tl _x_0 in let (_x_3 : int) = List.length (odds _x_2) in let (_x_4 : bool) = List.length _x_2 <= _x_3 in let (_x_5 : bool) = _x_1 || not _x_4 in let (_x_6 : bool) = _x_2 = [] in let (_x_7 : bool) = not (List.length _x_0 <= _x_3) in (_x_5 || not _x_6 || _x_7) && (_x_5 || _x_6 || not (List.tl _x_2 = []) || _x_7) && (_x_1 || _x_4 || _x_7) expansions: [List.length, odds, List.length, List.length, odds, List.length, List.length, odds, List.length] 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_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_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegative
• Subproof
• Subproof
• Subproof
• ##### subproof
let (_x_0 : sko_ty_0 list) = List.tl x in not (List.length x <= List.length (odds x)) || (x = []) || (_x_0 = []) || (_x_0 <> [] && x <> [])
• start[0.234s, "2"]
let (_x_0 : sko_ty_0 list) = List.tl x in
not (List.length x <= List.length (odds x)) || (x = []) || (_x_0 = [])
|| (_x_0 <> [] && x <> [])
• ###### simplify
 into: true expansions: [] rewrite_steps: forward_chaining: List.len_nonnegativeList.len_nonnegative

Now we're ready to define merge_sort. Imandra is able prove it terminating using our custom measure (and lemma!).

In :
let rec merge_sort l =
match l with
| []  -> []
| [_] -> l
| _ :: ls -> merge (merge_sort (odds l)) (merge_sort (odds ls))
[@@measure merge_sort_measure l]

Out:
val merge_sort : Z.t list -> Z.t list = <fun>

termination proof

### Termination proof

call merge_sort (odds l) from merge_sort l
original:merge_sort l
sub:merge_sort (odds l)
original ordinal:merge_sort_measure l
sub ordinal:merge_sort_measure (odds l)
path:[not Is_a([], List.tl l) && l <> []]
proof:
detailed proof
ground_instances:2
definitions:0
inductions:0
search_time:
0.008s
details:
Expand
smt_stats:
 num checks: 6 arith assert lower: 6 arith tableau max rows: 2 arith tableau max columns: 6 arith pivots: 2 rlimit count: 5220 mk clause: 4 datatype occurs check: 20 mk bool var: 43 arith assert upper: 2 datatype splits: 4 decisions: 10 arith row summations: 1 propagations: 5 conflicts: 5 datatype accessor ax: 7 arith num rows: 2 datatype constructor ax: 8 num allocs: 2.97171e+09 final checks: 4 added eqs: 31 del clause: 3 arith eq adapter: 1 memory: 19.97 max memory: 27.09
Expand
• start[0.008s]
let (_x_0 : int) = List.length l in
let (_x_1 : int) = if _x_0 >= 0 then _x_0 else 0 in
let (_x_2 : int list) = odds l in
let (_x_3 : int) = List.length _x_2 in
let (_x_4 : int) = if _x_3 >= 0 then _x_3 else 0 in
let (_x_5 : bool) = not (not Is_a([], List.tl _x_2) && _x_2 <> []) in
not Is_a([], List.tl l) && (l <> [] && ((_x_1 >= 0) && (_x_4 >= 0)))
==> (_x_5 && _x_5) || Ordinal.( << ) (Ordinal.Int _x_4) (Ordinal.Int _x_1)
• ###### simplify
 into: let (_x_0 : int list) = odds … in let (_x_1 : int) = List.length _x_0 in let (_x_2 : int) = List.length … in Ordinal.( << ) (Ordinal.Int (if _x_1 >= 0 then _x_1 else 0)) (Ordinal.Int (if _x_2 >= 0 then _x_2 else 0)) || not (not Is_a([], List.tl …) && … <> []) || not (not Is_a([], List.tl _x_0) && _x_0 <> []) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|List.length_941/server| (odds_946/server l_952/server)) expansions:
• unroll
 expr: (let ((a!1 (ite (>= (|List.length_941/server| (odds_946/server l_952/server)) 0) (|L… expansions:
• Unsat
call merge_sort (odds (List.tl l)) from merge_sort l
original:merge_sort l
sub:merge_sort (odds (List.tl l))
original ordinal:merge_sort_measure l
sub ordinal:merge_sort_measure (odds (List.tl l))
path:[not Is_a([], List.tl l) && l <> []]
proof:
detailed proof
ground_instances:4
definitions:0
inductions:0
search_time:
0.011s
details:
Expand
smt_stats:
 num checks: 10 arith assert lower: 7 arith tableau max rows: 4 arith tableau max columns: 10 arith pivots: 6 rlimit count: 3204 mk clause: 12 datatype occurs check: 67 mk bool var: 95 arith assert upper: 7 datatype splits: 14 decisions: 26 arith row summations: 8 propagations: 20 conflicts: 12 datatype accessor ax: 13 arith conflicts: 1 arith num rows: 4 datatype constructor ax: 19 num allocs: 2.87204e+09 final checks: 13 added eqs: 87 del clause: 9 arith eq adapter: 2 memory: 19.98 max memory: 27.09
Expand
• start[0.011s]
let (_x_0 : int list) = List.tl … in
let (_x_1 : int) = List.length … in
let (_x_2 : int) = if _x_1 >= 0 then _x_1 else 0 in
let (_x_3 : int list) = odds _x_0 in
let (_x_4 : int) = List.length _x_3 in
let (_x_5 : int) = if _x_4 >= 0 then _x_4 else 0 in
let (_x_6 : bool) = not (not Is_a([], List.tl _x_3) && _x_3 <> []) in
not Is_a([], _x_0) && (… <> [] && ((_x_2 >= 0) && (_x_5 >= 0)))
==> (_x_6 && _x_6) || Ordinal.( << ) (Ordinal.Int _x_5) (Ordinal.Int _x_2)
• ###### simplify
 into: let (_x_0 : int list) = List.tl … in let (_x_1 : int list) = odds _x_0 in let (_x_2 : int) = List.length _x_1 in let (_x_3 : int) = List.length … in not (not Is_a([], List.tl _x_1) && _x_1 <> []) || Ordinal.( << ) (Ordinal.Int (if _x_2 >= 0 then _x_2 else 0)) (Ordinal.Int (if _x_3 >= 0 then _x_3 else 0)) || not (not Is_a([], _x_0) && … <> []) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (let ((a!1 (>= (|List.length_941/server| (odds_946/server (|get.::.1_934/server| l_… expansions:
• unroll
 expr: (|List.length_941/server| (odds_946/server (|get.::.1_934/server| l_952/server))) expansions:
• unroll
 expr: (|List.length_941/server| l_952/server) expansions:
• unroll
 expr: (odds_946/server (|get.::.1_934/server| l_952/server)) expansions:
• Unsat

Let's experiment a bit with merge_sort to gain confidence we've defined it correctly.

In :
merge_sort [1;2;3]

Out:
- : Z.t list = [1;2;3]

In :
merge_sort [9;100;6;2;34;19;3;4;7;6]

Out:
- : Z.t list = [2;3;4;6;6;7;9;19;34;100]


This looks pretty good! Let's now use Imandra to prove it correct.

# Proving Merge Sort correct¶

What does it mean for a sorting algorithm to be correct? There are two main components:

• The result is sorted
• The result has the same elements as the original

Let's start by defining what it means for a list to be sorted.

In :
let rec is_sorted (x : int list) =
match x with
| []  -> true
| [_] -> true
| x :: x' :: xs -> x <= x' && is_sorted (x' :: xs)

Out:
val is_sorted : Z.t list -> bool = <fun>

termination proof

### Termination proof

call let (_x_0 : int list) = List.tl x in is_sorted ((List.hd _x_0) :: (List.tl _x_0)) from is_sorted x
original:is_sorted x
sub:let (_x_0 : int list) = List.tl x in is_sorted ((List.hd _x_0) :: (List.tl _x_0))
original ordinal:Ordinal.Int (_cnt x)
sub ordinal:let (_x_0 : int list) = List.tl x in Ordinal.Int (_cnt ((List.hd _x_0) :: (List.tl _x_0)))
path:[List.hd x <= List.hd (List.tl x) && (List.tl x) <> [] && x <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.008s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 19 arith tableau max rows: 10 arith tableau max columns: 24 arith pivots: 11 rlimit count: 2817 mk clause: 31 datatype occurs check: 12 mk bool var: 87 arith assert upper: 23 datatype splits: 1 decisions: 17 arith row summations: 18 arith bound prop: 1 propagations: 26 interface eqs: 1 conflicts: 10 arith fixed eqs: 6 arith assume eqs: 1 datatype accessor ax: 10 arith conflicts: 3 arith num rows: 10 datatype constructor ax: 8 num allocs: 3.08034e+09 final checks: 5 added eqs: 52 del clause: 22 arith eq adapter: 17 memory: 20.32 max memory: 27.09
Expand
• start[0.008s]
let (_x_0 : int list) = List.tl x in
let (_x_1 : int) = List.hd _x_0 in
let (_x_2 : int) = count.list mk_nat x in
let (_x_3 : int) = count.list mk_nat (_x_1 :: …) in
(List.hd x <= _x_1)
&& (_x_0 <> [] && (x <> [] && ((_x_2 >= 0) && (_x_3 >= 0))))
==> not ((_x_1 <= List.hd …) && … <> [])
|| Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_2)
• ###### simplify
 into: let (_x_0 : int list) = List.tl x in let (_x_1 : int) = List.hd _x_0 in let (_x_2 : int) = count.list mk_nat (_x_1 :: …) in let (_x_3 : int) = count.list mk_nat x in not ((_x_1 <= List.hd …) && … <> []) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_3) || not ((List.hd x <= _x_1) && _x_0 <> [] && x <> [] && (_x_3 >= 0) && (_x_2 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (let ((a!1 (|count.list_1044/server| (|::| (|get.::.0_1031/server| … expansions:
• unroll
 expr: (|count.list_1044/server| (|::| (|get.::.0_1031/server| (|get.::.1_1032/server| x_1033/server)) … expansions:
• unroll
 expr: (|count.list_1044/server| x_1033/server) expansions:
• Unsat

As usual, let's experiment a bit with this definition.

In :
is_sorted [1;2;3;4;5]

Out:
- : bool = true

In :
is_sorted [1;4;2]

Out:
- : bool = false

In :
is_sorted 

Out:
- : bool = true

In :
instance (fun x -> List.length x >= 5 && is_sorted x)

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

Instance (after 11 steps, 0.012s):
let x : int list = [0; 1; 1237; 3033; 3482]

Instance
proof attempt
ground_instances:11
definitions:0
inductions:0
search_time:
0.012s
details:
Expand
smt_stats:
 arith offset eqs: 2 num checks: 23 arith assert lower: 57 arith tableau max rows: 18 arith tableau max columns: 34 arith pivots: 26 rlimit count: 7292 mk clause: 103 datatype occurs check: 71 mk bool var: 324 arith assert upper: 43 datatype splits: 21 decisions: 94 arith row summations: 66 arith bound prop: 2 propagations: 173 conflicts: 29 arith fixed eqs: 24 datatype accessor ax: 16 minimized lits: 4 arith conflicts: 8 arith num rows: 18 arith assert diseq: 27 datatype constructor ax: 64 num allocs: 3.18828e+09 final checks: 29 added eqs: 324 del clause: 78 arith eq adapter: 51 memory: 20.55 max memory: 27.09
Expand
• start[0.012s] (List.length ( :var_0: ) >= 5) && is_sorted ( :var_0: )
• unroll
 expr: (is_sorted_1282/client x_1289/client) expansions:
• unroll
 expr: (|List.length_1085/server| x_1289/client) expansions:
• unroll
 expr: (|List.length_1085/server| (|get.::.1_1084/server| x_1289/client)) expansions:
• unroll
 expr: (is_sorted_1282/client (|::| (|get.::.0_1083/server| (|get.::.1_1084/server| x_1289/client)) … expansions:
• unroll
 expr: (|List.length_1085/server| (|get.::.1_1084/server| (|get.::.1_1084/server| x_1289/client))) expansions:
• unroll
 expr: (let ((a!1 (|::| (|get.::.0_1083/server| (|get.::.1_1084/server| … expansions:
• unroll
 expr: (|List.length_1085/server| (|get.::.1_1084/server| (|get.::.1_1084/server| (|get.::.1_1084/ser… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1084/server| (|get.::.1_1084/server| (|get.::.1_10… expansions:
• unroll
 expr: (let ((a!1 (|get.::.0_1083/server| (|get.::.1_1084/server| (|get.::.1_10… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1084/server| (|get.::.1_1084/server| (|get.::.1_10… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1084/server| (|get.::.1_1084/server| (|get.::.1_10… expansions:
• Sat (Some let x : int list = [(Z.of_nativeint (0n)); (Z.of_nativeint (1n)); (Z.of_nativeint (1237n)); (Z.of_nativeint (3033n)); (Z.of_nativeint (3482n))] )
In :
instance (fun x -> List.length x >= 5 && is_sorted x && is_sorted (List.rev x))

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

Instance (after 44 steps, 0.047s):
let x : int list = [3634; 3634; 3634; 3634; 3634]

Instance
proof attempt
ground_instances:44
definitions:0
inductions:0
search_time:
0.047s
details:
Expand
smt_stats:
 arith offset eqs: 441 num checks: 89 arith assert lower: 510 arith tableau max rows: 45 arith tableau max columns: 69 arith pivots: 230 rlimit count: 95999 mk clause: 728 datatype occurs check: 1982 mk bool var: 3175 arith assert upper: 700 datatype splits: 425 decisions: 2894 arith row summations: 1420 arith bound prop: 54 propagations: 4833 interface eqs: 56 conflicts: 186 arith fixed eqs: 447 arith assume eqs: 56 datatype accessor ax: 364 minimized lits: 25 arith conflicts: 10 arith num rows: 45 arith assert diseq: 202 datatype constructor ax: 962 num allocs: 3.32287e+09 final checks: 192 added eqs: 8843 del clause: 463 arith eq adapter: 266 time: 0.001 memory: 21.94 max memory: 27.09
Expand
• start[0.047s]
(List.length ( :var_0: ) >= 5)
&& (is_sorted ( :var_0: ) && is_sorted (List.rev ( :var_0: )))
• #### simplify

 into: (List.length ( :var_0: ) >= 5) && is_sorted ( :var_0: ) && is_sorted (List.rev ( :var_0: )) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (is_sorted_1282/client (|List.rev_1128/server| x_1291/client)) expansions:
• unroll
 expr: (|List.rev_1128/server| x_1291/client) expansions:
• unroll
 expr: (is_sorted_1282/client x_1291/client) expansions:
• unroll
 expr: (|List.length_1124/server| x_1291/client) expansions:
• unroll
 expr: (let ((a!1 (|::| (|get.::.0_1122/server| (|get.::.1_1123/server| … expansions:
• unroll
 expr: (|List.append_1132/server| (|List.rev_1128/server| (|get.::.1_1123/server| x_1291/client)) (|::|… expansions:
• unroll
 expr: (|List.rev_1128/server| (|get.::.1_1123/server| x_1291/client)) expansions:
• unroll
 expr: (|List.length_1124/server| (|get.::.1_1123/server| x_1291/client)) expansions:
• unroll
 expr: (is_sorted_1282/client (|::| (|get.::.0_1122/server| (|get.::.1_1123/server| x_1291/client)) … expansions:
• unroll
 expr: (let ((a!1 (|get.::.0_1122/server| (|get.::.1_1123/server| (|get.::.1_11… expansions:
• unroll
 expr: (|List.append_1132/server| (|List.rev_1128/server| (|get.::.1_1123/server| (|get.::.1_1123/ser… expansions:
• unroll
 expr: (|List.rev_1128/server| (|get.::.1_1123/server| (|get.::.1_1123/server| x_1291/client))) expansions:
• unroll
 expr: (|List.length_1124/server| (|get.::.1_1123/server| (|get.::.1_1123/server| x_1291/client))) expansions:
• unroll
 expr: (|List.append_1132/server| (|get.::.1_1123/server| (|List.rev_1128/server| (|get.::.1_1123/ser… expansions:
• unroll
 expr: (let ((a!1 (|::| (|get.::.0_1122/server| (|get.::.1_1123/server| … expansions:
• unroll
 expr: (let ((a!1 (|List.rev_1128/server| (|get.::.1_1123/server| (|get.::.1_11… expansions:
• unroll
 expr: (|List.rev_1128/server| (|get.::.1_1123/server| (|get.::.1_1123/server| (|get.::.1_1123/server… expansions:
• unroll
 expr: (|List.length_1124/server| (|get.::.1_1123/server| (|get.::.1_1123/server| (|get.::.1_1123/ser… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1123/server| (|List.rev_1128/server| (|get.::.1_11… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1123/server| (|get.::.1_1123/server| (|get.::.1_11… expansions:
• unroll
 expr: (let ((a!1 (|get.::.0_1122/server| (|get.::.1_1123/server| (|get.::.1_11… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1123/server| (|get.::.1_1123/server| (|get.::.1_11… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1123/server| (|get.::.1_1123/server| (|get.::.1_11… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1123/server| (|get.::.1_1123/server| (|get.::.1_11… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1123/server| (|get.::.1_1123/server| (|List.rev_11… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1123/server| (|get.::.1_1123/server| (|get.::.1_11… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1123/server| (|get.::.1_1123/server| (|get.::.1_11… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1123/server| (|get.::.1_1123/server| (|get.::.1_11… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1123/server| (|get.::.1_1123/server| (|get.::.1_11… expansions:
• unroll
 expr: (let ((a!1 (|List.rev_1128/server| (|get.::.1_1123/server| (|get.::.1_11… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1123/server| (|get.::.1_1123/server| (|get.::.1_11… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1123/server| (|List.rev_1128/server| (|get.::.1_11… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1123/server| (|get.::.1_1123/server| (|get.::.1_11… expansions:
• unroll
 expr: (let ((a!1 (|List.rev_1128/server| (|get.::.1_1123/server| (|get.::.1_11… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1123/server| (|get.::.1_1123/server| (|get.::.1_11… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1123/server| (|List.rev_1128/server| (|get.::.1_11… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1123/server| (|get.::.1_1123/server| (|List.rev_11… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1123/server| (|List.rev_1128/server| (|get.::.1_11… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1123/server| (|get.::.1_1123/server| (|get.::.1_11… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1123/server| (|get.::.1_1123/server| (|get.::.1_11… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1123/server| (|get.::.1_1123/server| (|get.::.1_11… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1123/server| (|get.::.1_1123/server| (|get.::.1_11… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1123/server| (|get.::.1_1123/server| (|get.::.1_11… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1123/server| (|get.::.1_1123/server| (|List.rev_11… expansions:
• Sat (Some let x : int list = [(Z.of_nativeint (3634n)); (Z.of_nativeint (3634n)); (Z.of_nativeint (3634n)); (Z.of_nativeint (3634n)); (Z.of_nativeint (3634n))] )

## Proving Merge Sort sorts¶

Now that we've defined our is_sorted predicate, we're ready to state one of our main verification goals: that merge_sort sorts!

We can write this this way:

theorem merge_sort_sorts x =
is_sorted (merge_sort x)


Before we try to prove this for all possible cases by induction, let's ask Imandra to verify that this property holds up to our current recursion unrolling bound (100).

In :
verify (fun x -> is_sorted (merge_sort x))

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

Unknown (Verified up to bound 100)
Expand
 expanded: let (_x_0 : int list) = odds (odds …) in merge (merge_sort (odds _x_0)) (merge_sort (odds (List.tl _x_0)))let (_x_0 : int list) = odds (List.tl (odds …)) in merge (merge_sort (odds _x_0)) (merge_sort (odds (List.tl _x_0)))merge_sort (odds (List.tl (odds (List.tl x))))let (_x_0 : int list) = List.tl (List.tl (merge_sort x)) in is_sorted ((List.hd _x_0) :: (List.tl _x_0))let (_x_0 : int list) = merge_sort (odds x) in let (_x_1 : int list) = merge_sort (odds (List.tl x)) in let (_x_2 : bool) = not (List.hd _x_1 <= List.hd _x_0) && _x_1 <> [] && _x_0 <> [] in merge (if _x_2 then List.tl _x_0 else _x_0) (if _x_2 then _x_1 else (List.tl _x_1))let (_x_0 : int list) = odds … in merge (merge_sort (odds _x_0)) (merge_sort (odds (List.tl _x_0)))odds (odds (List.tl (odds x)))odds (odds (List.tl x))odds (odds (odds …))odds (odds (List.tl (odds (List.tl (odds …)))))odds (List.tl (odds …))merge_sort (odds x)odds (odds …)let (_x_0 : int list) = merge_sort (odds x) in let (_x_1 : int list) = merge_sort (odds (List.tl x)) in let (_x_2 : bool) = not (List.hd _x_1 <= List.hd _x_0) && _x_1 <> [] && _x_0 <> [] in let (_x_3 : int list) = if _x_2 then List.tl _x_0 else _x_0 in let (_x_4 : int list) = if _x_2 then _x_1 else List.tl _x_1 in let (_x_5 : bool) = not (List.hd _x_4 <= List.hd _x_3) && _x_4 <> [] && _x_3 <> [] in merge (if _x_5 then List.tl _x_3 else _x_3) (if _x_5 then _x_4 else (List.tl _x_4))odds (List.tl (odds (odds …)))odds (List.tl (odds (List.tl (odds (List.tl (odds x))))))odds xmerge_sort (odds (List.tl (odds (odds …))))merge_sort (odds (List.tl (odds (List.tl (odds (List.tl (odds x)))))))odds (List.tl (odds (List.tl x)))let (_x_0 : int list) = odds x in let (_x_1 : int list) = merge_sort (odds _x_0) in let (_x_2 : int list) = merge_sort (odds (List.tl _x_0)) in let (_x_3 : bool) = not (List.hd _x_2 <= List.hd _x_1) && _x_2 <> [] && _x_1 <> [] in let (_x_4 : int list) = if _x_3 then List.tl _x_1 else _x_1 in let (_x_5 : int list) = if _x_3 then _x_2 else List.tl _x_2 in let (_x_6 : bool) = not (List.hd _x_5 <= List.hd _x_4) && _x_5 <> [] && _x_4 <> [] in merge (if _x_6 then List.tl _x_4 else _x_4) (if _x_6 then _x_5 else (List.tl _x_5))odds (List.tl (List.tl (odds (odds (List.tl …)))))odds (List.tl (List.tl (List.tl (odds …))))odds (odds …)odds (List.tl (odds (List.tl (odds x))))odds (List.tl (List.tl (List.tl (List.tl (List.tl …)))))let (_x_0 : int list) = List.tl (List.tl (List.tl (merge_sort x))) in is_sorted ((List.hd _x_0) :: (List.tl _x_0))odds (List.tl (List.tl (odds (List.tl (odds (List.tl …))))))let (_x_0 : int list) = odds (odds (List.tl (odds …))) in merge (merge_sort (odds _x_0)) (merge_sort (odds (List.tl _x_0)))odds (List.tl (List.tl (List.tl (odds (List.tl (odds …))))))merge_sort (odds (odds (List.tl (odds …))))odds (odds x)let (_x_0 : int list) = odds (List.tl x) in merge (merge_sort (odds _x_0)) (merge_sort (odds (List.tl _x_0)))let (_x_0 : int list) = odds … in let (_x_1 : int list) = merge_sort (odds _x_0) in let (_x_2 : int list) = merge_sort (odds (List.tl _x_0)) in let (_x_3 : bool) = not (List.hd _x_2 <= List.hd _x_1) && _x_2 <> [] && _x_1 <> [] in merge (if _x_3 then List.tl _x_1 else _x_1) (if _x_3 then _x_2 else (List.tl _x_2))odds (List.tl (List.tl (List.tl x)))merge_sort (odds (odds (odds …)))merge_sort (odds (odds (List.tl (odds (List.tl (odds …))))))merge_sort (odds (List.tl (odds (List.tl (odds …)))))let (_x_0 : int list) = odds (List.tl …) in let (_x_1 : int list) = merge_sort (odds _x_0) in let (_x_2 : int list) = merge_sort (odds (List.tl _x_0)) in let (_x_3 : bool) = not (List.hd _x_2 <= List.hd _x_1) && _x_2 <> [] && _x_1 <> [] in let (_x_4 : int list) = if _x_3 then List.tl _x_1 else _x_1 in let (_x_5 : int list) = if _x_3 then _x_2 else List.tl _x_2 in let (_x_6 : bool) = not (List.hd _x_5 <= List.hd _x_4) && _x_5 <> [] && _x_4 <> [] in merge (if _x_6 then List.tl _x_4 else _x_4) (if _x_6 then _x_5 else (List.tl _x_5))odds (List.tl (List.tl (List.tl (List.tl (odds x)))))is_sorted (merge_sort x)odds (List.tl (List.tl (List.tl (odds x))))merge_sort (odds (odds (List.tl x)))odds (List.tl (List.tl (List.tl (List.tl (List.tl (odds x))))))merge_sort (odds (List.tl (odds (odds (List.tl x)))))let (_x_0 : int list) = odds (odds x) in merge (merge_sort (odds _x_0)) (merge_sort (odds (List.tl _x_0)))merge_sort (odds (odds (List.tl (odds x))))merge_sort (odds (List.tl (odds (List.tl (odds …)))))odds (List.tl (List.tl (List.tl (List.tl x))))odds (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))let (_x_0 : int list) = odds (List.tl (odds (odds (List.tl …)))) in merge (merge_sort (odds _x_0)) (merge_sort (odds (List.tl _x_0)))odds (odds (odds (List.tl x)))odds (List.tl (odds (odds x)))let (_x_0 : int list) = odds (List.tl (odds x)) in merge (merge_sort (odds _x_0)) (merge_sort (odds (List.tl _x_0)))let (_x_0 : int list) = odds (odds x) in let (_x_1 : int list) = merge_sort (odds _x_0) in let (_x_2 : int list) = merge_sort (odds (List.tl _x_0)) in let (_x_3 : bool) = not (List.hd _x_2 <= List.hd _x_1) && _x_2 <> [] && _x_1 <> [] in merge (if _x_3 then List.tl _x_1 else _x_1) (if _x_3 then _x_2 else (List.tl _x_2))odds (List.tl (odds x))odds (List.tl (odds (odds (List.tl (odds x)))))let (_x_0 : int list) = merge_sort (odds (odds (List.tl (odds (List.tl x))))) in let (_x_1 : int list) = merge_sort (odds (List.tl (odds (List.tl (odds (List.tl …)))))) in let (_x_2 : bool) = not (List.hd _x_1 <= List.hd _x_0) && _x_1 <> [] && _x_0 <> [] in merge (if _x_2 then List.tl _x_0 else _x_0) (if _x_2 then _x_1 else (List.tl _x_1))odds (List.tl (odds (odds (odds x))))odds (List.tl (List.tl (List.tl (odds (List.tl (odds (List.tl …)))))))let (_x_0 : int list) = List.tl (List.tl (List.tl (List.tl (merge_sort …)))) in is_sorted ((List.hd _x_0) :: (List.tl _x_0))merge (merge_sort (odds (odds (List.tl (odds (List.tl x)))))) (merge_sort (odds (List.tl (odds …))))let (_x_0 : int list) = odds (odds …) in merge (merge_sort (odds _x_0)) (merge_sort (odds (List.tl _x_0)))odds (List.tl (List.tl (odds x)))let (_x_0 : int list) = odds (List.tl x) in let (_x_1 : int list) = merge_sort (odds _x_0) in let (_x_2 : int list) = merge_sort (odds (List.tl _x_0)) in let (_x_3 : bool) = not (List.hd _x_2 <= List.hd _x_1) && _x_2 <> [] && _x_1 <> [] in merge (if _x_3 then List.tl _x_1 else _x_1) (if _x_3 then _x_2 else (List.tl _x_2))odds (List.tl (List.tl x))merge (merge_sort (odds x)) (merge_sort (odds (List.tl x)))odds (List.tl (List.tl (odds …)))odds (List.tl (odds (List.tl (odds …))))odds (List.tl (List.tl (odds (odds x))))odds (List.tl (odds (odds (List.tl x))))odds (List.tl (List.tl (List.tl (List.tl (List.tl (odds (List.tl …)))))))merge_sort (odds (odds (odds x)))odds (List.tl (List.tl (List.tl (odds (odds (List.tl x))))))let (_x_0 : int list) = odds (List.tl (odds (odds x))) in merge (merge_sort (odds _x_0)) (merge_sort (odds (List.tl _x_0)))merge_sort (odds (odds x))merge_sort (odds (odds (odds …)))merge_sort (odds (List.tl (odds (odds (odds x)))))let (_x_0 : int list) = odds x in let (_x_1 : int list) = merge_sort (odds _x_0) in let (_x_2 : int list) = merge_sort (odds (List.tl _x_0)) in let (_x_3 : bool) = not (List.hd _x_2 <= List.hd _x_1) && _x_2 <> [] && _x_1 <> [] in merge (if _x_3 then List.tl _x_1 else _x_1) (if _x_3 then _x_2 else (List.tl _x_2))let (_x_0 : int list) = List.tl (merge_sort x) in is_sorted ((List.hd _x_0) :: (List.tl _x_0))merge_sort (odds (odds (odds (odds x))))let (_x_0 : int list) = merge_sort (odds x) in let (_x_1 : int list) = merge_sort … in let (_x_2 : bool) = not (List.hd _x_1 <= List.hd _x_0) && _x_1 <> [] && _x_0 <> [] in let (_x_3 : int list) = if _x_2 then List.tl _x_0 else _x_0 in let (_x_4 : int list) = if _x_2 then _x_1 else List.tl _x_1 in let (_x_5 : bool) = not (List.hd _x_4 <= List.hd _x_3) && _x_4 <> [] && _x_3 <> [] in let (_x_6 : int list) = if _x_5 then List.tl _x_3 else _x_3 in let (_x_7 : int list) = if _x_5 then _x_4 else List.tl _x_4 in let (_x_8 : bool) = not (List.hd _x_7 <= List.hd _x_6) && _x_7 <> [] && _x_6 <> [] in merge (if _x_8 then List.tl _x_6 else _x_6) (if _x_8 then _x_7 else (List.tl _x_7))let (_x_0 : int list) = odds (odds (List.tl …)) in let (_x_1 : int list) = merge_sort (odds _x_0) in let (_x_2 : int list) = merge_sort (odds (List.tl _x_0)) in let (_x_3 : bool) = not (List.hd _x_2 <= List.hd _x_1) && _x_2 <> [] && _x_1 <> [] in merge (if _x_3 then List.tl _x_1 else _x_1) (if _x_3 then _x_2 else (List.tl _x_2))merge_sort (odds (List.tl (odds (odds (List.tl (odds x))))))odds (List.tl (List.tl (List.tl (odds (List.tl x)))))let (_x_0 : int list) = odds x in merge (merge_sort (odds _x_0)) (merge_sort (odds (List.tl _x_0)))odds (List.tl (List.tl (odds (List.tl x))))odds (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl …)))))))merge_sort (odds (List.tl (odds x)))odds (List.tl (List.tl (List.tl (List.tl (odds (List.tl …))))))merge_sort (odds (List.tl x))merge_sort (odds (odds (List.tl (odds (List.tl x)))))merge_sort (odds (List.tl (odds (List.tl (odds x)))))odds (List.tl x)merge_sort (odds (odds (odds (List.tl x))))merge_sort (odds (List.tl (odds (odds x))))odds (odds (odds (odds x)))odds (odds (odds x))odds (List.tl (List.tl (List.tl (List.tl (List.tl x)))))merge_sort x blocked: odds (List.tl (List.tl (odds (odds …))))odds (List.tl (List.tl (odds (List.tl (odds …)))))odds (List.tl (List.tl (List.tl (odds (List.tl (odds (odds x)))))))odds (odds (List.tl (odds (odds …))))odds (List.tl (odds (odds (List.tl (odds (odds x))))))odds (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x)))))))))odds (List.tl (List.tl (List.tl (List.tl (List.tl (odds (odds (List.tl x))))))))let (_x_0 : int list) = odds … in let (_x_1 : int list) = merge_sort (odds _x_0) in let (_x_2 : int list) = merge_sort (odds (List.tl _x_0)) in let (_x_3 : bool) = not (List.hd _x_2 <= List.hd _x_1) && _x_2 <> [] && _x_1 <> [] in let (_x_4 : int list) = if _x_3 then List.tl _x_1 else _x_1 in let (_x_5 : int list) = if _x_3 then _x_2 else List.tl _x_2 in let (_x_6 : bool) = not (List.hd _x_5 <= List.hd _x_4) && _x_5 <> [] && _x_4 <> [] in merge (if _x_6 then List.tl _x_4 else _x_4) (if _x_6 then _x_5 else (List.tl _x_5))merge_sort (odds (List.tl (odds (odds (odds …)))))merge_sort (odds (odds (odds (odds …))))merge_sort (odds (odds (odds (List.tl (odds (List.tl (odds …)))))))merge_sort (odds (List.tl (odds (List.tl (odds (odds (odds x)))))))merge_sort (odds (odds (List.tl (odds (List.tl (odds (odds x)))))))let (_x_0 : int list) = odds (odds …) in let (_x_1 : int list) = merge_sort (odds _x_0) in let (_x_2 : int list) = merge_sort (odds (List.tl _x_0)) in let (_x_3 : bool) = not (List.hd _x_2 <= List.hd _x_1) && _x_2 <> [] && _x_1 <> [] in merge (if _x_3 then List.tl _x_1 else _x_1) (if _x_3 then _x_2 else (List.tl _x_2))let (_x_0 : int list) = odds (List.tl (odds (List.tl (odds …)))) in let (_x_1 : int list) = merge_sort (odds _x_0) in let (_x_2 : int list) = merge_sort _x_0 in let (_x_3 : bool) = not (List.hd _x_2 <= List.hd _x_1) && _x_2 <> [] && _x_1 <> [] in merge (if _x_3 then List.tl _x_1 else _x_1) (if _x_3 then _x_2 else (List.tl _x_2))odds (List.tl (odds (odds (odds …))))odds (odds (odds (odds …)))merge_sort (odds (List.tl (odds (List.tl (odds …)))))odds (List.tl (List.tl (List.tl (List.tl (odds (odds …))))))odds (List.tl (List.tl (List.tl (List.tl (List.tl (odds (odds x)))))))odds (List.tl (List.tl (odds (List.tl (odds (odds x))))))let (_x_0 : int list) = odds (odds …) in merge (merge_sort _x_0) (merge_sort (odds (List.tl (odds _x_0))))merge (merge_sort (odds (odds …))) (merge_sort (odds (List.tl (odds (List.tl (odds (odds (odds x))))))))odds (List.tl (List.tl (List.tl (List.tl (List.tl …)))))let (_x_0 : int list) = merge_sort (odds (odds (odds (odds x)))) in let (_x_1 : int list) = merge_sort (odds …) in let (_x_2 : bool) = not (List.hd _x_1 <= List.hd _x_0) && _x_1 <> [] && _x_0 <> [] in merge (if _x_2 then List.tl _x_0 else _x_0) (if _x_2 then _x_1 else (List.tl _x_1))merge_sort (odds (List.tl (odds (odds (odds (odds x))))))merge_sort (odds (odds (odds (List.tl (odds (odds x))))))let (_x_0 : int list) = odds … in merge (merge_sort (odds _x_0)) (merge_sort (odds (List.tl _x_0)))let (_x_0 : int list) = odds … in merge (merge_sort (odds _x_0)) (merge_sort (odds (List.tl _x_0)))merge_sort (odds (odds (odds (odds …))))odds (List.tl (odds …))odds (List.tl (odds …))let (_x_0 : int list) = merge_sort (odds (odds (List.tl (odds (List.tl x))))) in let (_x_1 : int list) = merge_sort (odds (List.tl (odds …))) in let (_x_2 : bool) = not (List.hd _x_1 <= List.hd _x_0) && _x_1 <> [] && _x_0 <> [] in let (_x_3 : int list) = if _x_2 then List.tl _x_0 else _x_0 in let (_x_4 : int list) = if _x_2 then _x_1 else List.tl _x_1 in let (_x_5 : bool) = not (List.hd _x_4 <= List.hd _x_3) && _x_4 <> [] && _x_3 <> [] in merge (if _x_5 then List.tl _x_3 else _x_3) (if _x_5 then _x_4 else (List.tl _x_4))merge_sort (odds (List.tl (odds (odds (odds …)))))let (_x_0 : int list) = odds … in merge (merge_sort (odds (odds (List.tl (odds _x_0))))) (merge_sort (odds (List.tl _x_0)))odds (List.tl (odds …))odds (odds …)odds (odds …)odds (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (odds x)))))))))odds (List.tl (List.tl …))odds (List.tl (List.tl …))let (_x_0 : int list) = List.tl (List.tl (List.tl (List.tl (List.tl (merge_sort x))))) in is_sorted ((List.hd _x_0) :: (List.tl _x_0))odds (List.tl (odds (odds (odds (odds x)))))odds (odds (odds (List.tl (odds (odds x)))))merge_sort (odds (List.tl (odds …)))merge_sort (odds (odds …))merge_sort (odds (odds …))let (_x_0 : int list) = odds (List.tl (odds …)) in let (_x_1 : int list) = merge_sort (odds _x_0) in let (_x_2 : int list) = merge_sort (odds (List.tl _x_0)) in let (_x_3 : bool) = not (List.hd _x_2 <= List.hd _x_1) && _x_2 <> [] && _x_1 <> [] in merge (if _x_3 then List.tl _x_1 else _x_1) (if _x_3 then _x_2 else (List.tl _x_2))odds (List.tl (List.tl (List.tl (odds (odds (List.tl (odds …)))))))odds (List.tl (odds (List.tl (odds (List.tl (odds …))))))odds (List.tl (odds (odds (odds (List.tl (odds …))))))odds (odds (odds (odds …)))odds (odds (odds (List.tl (odds (List.tl (odds …))))))odds (List.tl (odds (List.tl (odds (odds (odds …))))))odds (odds (List.tl (odds (List.tl (odds (odds …))))))let (_x_0 : int list) = odds (odds …) in let (_x_1 : int list) = merge_sort (odds _x_0) in let (_x_2 : int list) = merge_sort (odds (List.tl _x_0)) in let (_x_3 : bool) = not (List.hd _x_2 <= List.hd _x_1) && _x_2 <> [] && _x_1 <> [] in let (_x_4 : int list) = if _x_3 then List.tl _x_1 else _x_1 in let (_x_5 : int list) = if _x_3 then _x_2 else List.tl _x_2 in let (_x_6 : bool) = not (List.hd _x_5 <= List.hd _x_4) && _x_5 <> [] && _x_4 <> [] in merge (if _x_6 then List.tl _x_4 else _x_4) (if _x_6 then _x_5 else (List.tl _x_5))odds (List.tl (List.tl (List.tl (List.tl (odds (List.tl (odds …)))))))odds (List.tl (List.tl (List.tl (List.tl (List.tl (odds (List.tl (odds …))))))))merge_sort (odds (odds (List.tl (odds (odds …)))))merge_sort (odds (List.tl (odds (odds (List.tl (odds (odds x)))))))let (_x_0 : int list) = merge_sort (odds (odds (List.tl (odds (odds …))))) in let (_x_1 : int list) = merge_sort (odds (List.tl (odds (List.tl (odds (odds (List.tl …))))))) in let (_x_2 : bool) = not (List.hd _x_1 <= List.hd _x_0) && _x_1 <> [] && _x_0 <> [] in merge (if _x_2 then List.tl _x_0 else _x_0) (if _x_2 then _x_1 else (List.tl _x_1))odds (List.tl (List.tl (odds (odds (odds …)))))odds (odds (List.tl (odds (odds …))))odds (odds (odds (List.tl (odds …))))odds (List.tl (List.tl (List.tl (List.tl (odds (List.tl (odds …)))))))odds (List.tl (List.tl (List.tl (odds (odds (odds …))))))odds (List.tl (odds (List.tl (odds (odds (List.tl …))))))odds (odds (List.tl (odds (List.tl (odds …)))))merge_sort (odds (odds (odds (odds (odds …)))))let (_x_0 : int list) = odds (odds (List.tl (odds (odds x)))) in merge (merge_sort (odds _x_0)) (merge_sort (odds (List.tl _x_0)))odds (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (odds …))))))))let (_x_0 : int list) = merge_sort (odds x) in let (_x_1 : int list) = merge_sort (odds (List.tl x)) in let (_x_2 : bool) = not (List.hd _x_1 <= List.hd _x_0) && _x_1 <> [] && _x_0 <> [] in let (_x_3 : int list) = if _x_2 then List.tl _x_0 else _x_0 in let (_x_4 : int list) = List.tl _x_3 in let (_x_5 : int list) = if _x_2 then _x_1 else List.tl _x_1 in let (_x_6 : bool) = not (List.hd _x_5 <= List.hd _x_3) && _x_5 <> [] && _x_3 <> [] in let (_x_7 : int list) = if _x_6 then _x_4 else _x_3 in let (_x_8 : int list) = List.tl _x_7 in let (_x_9 : int list) = List.tl _x_5 in let (_x_10 : int list) = if _x_6 then _x_5 else _x_9 in let (_x_11 : bool) = not (List.hd _x_10 <= List.hd _x_7) && _x_10 <> [] && _x_7 <> [] in let (_x_12 : int list) = if _x_11 then _x_8 else if _x_6 then _x_4 else … in let (_x_13 : int list) = List.tl _x_10 in let (_x_14 : int list) = if _x_11 then if _x_6 then … else _x_9 else _x_13 in let (_x_15 : bool) = not (List.hd (if _x_11 then _x_10 else _x_13) <= List.hd (if _x_11 then _x_8 else _x_7)) && _x_14 <> [] && _x_12 <> [] in merge (if _x_15 then List.tl _x_12 else _x_12) (if _x_15 then _x_14 else (List.tl _x_14))merge_sort (odds (List.tl (odds (List.tl (odds (odds (List.tl …)))))))merge_sort (odds (odds (List.tl (odds (List.tl (odds …))))))merge_sort (odds (odds (odds …)))let (_x_0 : int list) = odds (List.tl x) in let (_x_1 : int list) = merge_sort (odds _x_0) in let (_x_2 : int list) = merge_sort (odds (List.tl _x_0)) in let (_x_3 : bool) = not (List.hd _x_2 <= List.hd _x_1) && _x_2 <> [] && _x_1 <> [] in let (_x_4 : int list) = if _x_3 then List.tl _x_1 else _x_1 in let (_x_5 : int list) = if _x_3 then _x_2 else List.tl _x_2 in let (_x_6 : bool) = not (List.hd _x_5 <= List.hd _x_4) && _x_5 <> [] && _x_4 <> [] in let (_x_7 : int list) = if _x_6 then List.tl _x_4 else _x_4 in let (_x_8 : int list) = if _x_6 then _x_5 else List.tl _x_5 in let (_x_9 : bool) = not (List.hd _x_8 <= List.hd _x_7) && _x_8 <> [] && _x_7 <> [] in merge (if _x_9 then List.tl _x_7 else _x_7) (if _x_9 then _x_8 else (List.tl _x_8))merge_sort (odds (odds (List.tl (odds …))))merge_sort (odds (List.tl (odds (List.tl (odds (odds …))))))merge_sort (odds (List.tl (odds (List.tl (odds …)))))let (_x_0 : int list) = odds (List.tl (odds (List.tl (odds …)))) in merge (merge_sort (odds _x_0)) (merge_sort _x_0)odds (List.tl (List.tl (List.tl (List.tl …))))let (_x_0 : int list) = odds (odds (odds …)) in merge (merge_sort (odds _x_0)) (merge_sort (odds (List.tl _x_0)))odds (List.tl (List.tl (List.tl (List.tl (List.tl (odds (List.tl (odds (List.tl x)))))))))odds (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl x))))))))merge_sort (odds (odds (List.tl (odds …))))let (_x_0 : int list) = odds (odds (odds …)) in merge (merge_sort (odds _x_0)) (merge_sort (odds (List.tl _x_0)))let (_x_0 : int list) = odds (odds (List.tl (odds (List.tl (odds …))))) in merge (merge_sort (odds _x_0)) (merge_sort (odds (List.tl _x_0)))merge (merge_sort (odds (odds (List.tl (odds (List.tl (odds (odds x)))))))) (merge_sort (odds (List.tl (odds …))))odds (List.tl (odds (odds (odds …))))odds (List.tl (odds (odds (List.tl (odds (List.tl (odds …)))))))odds (List.tl (odds …))merge (merge_sort (odds (odds (odds (odds (odds …)))))) (merge_sort (odds (List.tl (odds (odds (odds (odds x)))))))odds (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl …)))))))let (_x_0 : int list) = odds … in let (_x_1 : int list) = merge_sort (odds _x_0) in let (_x_2 : int list) = merge_sort (odds (List.tl _x_0)) in let (_x_3 : bool) = not (List.hd _x_2 <= List.hd _x_1) && _x_2 <> [] && _x_1 <> [] in let (_x_4 : int list) = if _x_3 then List.tl _x_1 else _x_1 in let (_x_5 : int list) = if _x_3 then _x_2 else List.tl _x_2 in let (_x_6 : bool) = not (List.hd _x_5 <= List.hd _x_4) && _x_5 <> [] && _x_4 <> [] in let (_x_7 : int list) = if _x_6 then List.tl _x_4 else _x_4 in let (_x_8 : int list) = if _x_6 then _x_5 else List.tl _x_5 in let (_x_9 : bool) = not (List.hd _x_8 <= List.hd _x_7) && _x_8 <> [] && _x_7 <> [] in merge (if _x_9 then List.tl _x_7 else _x_7) (if _x_9 then _x_8 else (List.tl _x_8))odds (odds (odds (odds (List.tl (odds …)))))odds (odds (List.tl (odds (odds (odds …)))))let (_x_0 : int list) = odds (odds …) in let (_x_1 : int list) = merge_sort (odds _x_0) in let (_x_2 : int list) = merge_sort (odds (List.tl _x_0)) in let (_x_3 : bool) = not (List.hd _x_2 <= List.hd _x_1) && _x_2 <> [] && _x_1 <> [] in let (_x_4 : int list) = if _x_3 then List.tl _x_1 else _x_1 in let (_x_5 : int list) = if _x_3 then _x_2 else List.tl _x_2 in let (_x_6 : bool) = not (List.hd _x_5 <= List.hd _x_4) && _x_5 <> [] && _x_4 <> [] in merge (if _x_6 then List.tl _x_4 else _x_4) (if _x_6 then _x_5 else (List.tl _x_5))merge_sort (odds (List.tl (odds (odds (odds …)))))let (_x_0 : int list) = odds … in let (_x_1 : int list) = merge_sort (odds (odds _x_0)) in let (_x_2 : int list) = merge_sort (odds (List.tl (odds (odds (List.tl _x_0))))) in let (_x_3 : bool) = not (List.hd _x_2 <= List.hd _x_1) && _x_2 <> [] && _x_1 <> [] in merge (if _x_3 then List.tl _x_1 else _x_1) (if _x_3 then _x_2 else (List.tl _x_2))merge_sort (odds (List.tl (odds (odds (List.tl (odds (List.tl (odds …))))))))odds (odds (odds (odds (odds …))))merge_sort (odds (List.tl (odds (List.tl (odds …)))))
proof attempt
 ground_instances: 100 definitions: 0 inductions: 0 search_time: 1.275s
Expand
• start[1.275s] is_sorted (merge_sort ( :var_0: ))
• unroll
 expr: (is_sorted_1282/client (merge_sort_1276/client x_1293/client)) expansions:
• unroll
 expr: (merge_sort_1276/client x_1293/client) expansions:
• unroll
 expr: (merge_sort_1276/client (odds_1289/server x_1293/client)) expansions:
• unroll
 expr: (merge_1244/client (merge_sort_1276/client (odds_1289/server x_1293/client)) (merge_sort_1276/cl… expansions:
• unroll
 expr: (let ((a!1 (|::| (|get.::.0_1287/server| (|get.::.1_1288/server| … expansions:
• unroll
 expr: (merge_sort_1276/client (odds_1289/server (|get.::.1_1288/server| x_1293/client))) expansions:
• unroll
 expr: (odds_1289/server (|get.::.1_1288/server| x_1293/client)) expansions:
• unroll
 expr: (odds_1289/server x_1293/client) expansions:
• unroll
 expr: (odds_1289/server (|get.::.1_1288/server| (|get.::.1_1288/server| x_1293/client)… expansions:
• unroll
 expr: (let ((a!1 (merge_sort_1276/client (odds_1289/server (|get.::.1_1288/server| … expansions:
• unroll
 expr: (let ((a!1 (|get.::.0_1287/server| (merge_sort_1276/client (odds_1289/se… expansions:
• unroll
 expr: (merge_sort_1276/client (odds_1289/server (|get.::.1_1288/server| (odds_1289/server x_1293/client)… expansions:
• unroll
 expr: (odds_1289/server (|get.::.1_1288/server| (odds_1289/server x_1293/client))) expansions:
• unroll
 expr: (merge_sort_1276/client (odds_1289/server (odds_1289/server x_1293/client))) expansions:
• unroll
 expr: (odds_1289/server (odds_1289/server x_1293/client)) expansions:
• unroll
 expr: (odds_1289/server (|get.::.1_1288/server| (|get.::.1_1288/server| … expansions:
• unroll
 expr: (let ((a!1 (merge_sort_1276/client (odds_1289/server (odds_1289/server (|get.::.1_1288/… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (|get.::.1_1288/server| (odds_1289/serve… expansions:
• unroll
 expr: (odds_1289/server (|get.::.1_1288/server| (odds_1289/server (|get.::.1_1288/serv… expansions:
• unroll
 expr: (let ((a!1 (|get.::.0_1287/server| (|get.::.1_1288/server| (|get.::.1_12… expansions:
• unroll
 expr: (merge_sort_1276/client (odds_1289/server (odds_1289/server (|get.::.1_1288/server| x_1293/client)… expansions:
• unroll
 expr: (odds_1289/server (|get.::.1_1288/server| (|get.::.1_1288/server| (odds_1289/ser… expansions:
• unroll
 expr: (odds_1289/server (odds_1289/server (|get.::.1_1288/server| x_1293/client))) expansions:
• unroll
 expr: (let ((a!1 (merge_sort_1276/client (odds_1289/server (|get.::.1_1288/server| … expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (|get.::.1_1288/server| (|get.::.1_12… expansions:
• unroll
 expr: (let ((a!1 (|get.::.0_1287/server| (merge_sort_1276/client (odds_1289/se… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (|get.::.1_1288/server| (|get.::.1_12… expansions:
• unroll
 expr: (let ((a!1 (merge_sort_1276/client (odds_1289/server (odds_1289/server (odds_1289/serve… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (|get.::.1_1288/server| (odds_1289/serve… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (odds_1289/server (|get.::.1_1288/server| … expansions:
• unroll
 expr: (odds_1289/server (|get.::.1_1288/server| (odds_1289/server (odds_1289/server x_… expansions:
• unroll
 expr: (merge_sort_1276/client (odds_1289/server (odds_1289/server (odds_1289/server x_1293/client)))) expansions:
• unroll
 expr: (odds_1289/server (odds_1289/server (odds_1289/server x_1293/client))) expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (|get.::.1_1288/server| (|get.::.1_12… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (odds_1289/server (|get.::.1_1288/server| … expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (odds_1289/server (|get.::.1_1288/server| … expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (odds_1289/server (|get.::.1_1288/server| … expansions:
• unroll
 expr: (odds_1289/server (odds_1289/server (|get.::.1_1288/server| (o… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (|get.::.1_1288/server| (|get.::.1_12… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (|get.::.1_1288/server| (odds_1289/serve… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (|get.::.1_1288/server| (odds_1289/se… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (|get.::.1_1288/server| (odds_1289/se… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (|get.::.1_1288/server| (odds_1289/serve… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (|get.::.1_1288/server| (odds_1289/serve… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (|get.::.1_1288/server| (odds_1289/serve… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (|get.::.1_1288/server| (odds_1289/serve… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (|get.::.1_1288/server| (odds_1289/serve… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (|get.::.1_1288/server| (|get.::.1_12… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (odds_1289/server (odds_1289/server (|get.::.1_1288/server| … expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (odds_1289/server (odds_1289/server (|get.::.1_1288/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (odds_1289/server (odds_1289/server (|get.::.1_1288/… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (odds_1289/server (odds_1289/server (|get.::.1_1288/server| … expansions:
• unroll
 expr: (odds_1289/server (odds_1289/server (odds_1289/server (|get.::.1_1288/server| … expansions:
• unroll
 expr: (let ((a!1 (merge_sort_1276/client (odds_1289/server (|get.::.1_1288/server| … expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (|get.::.1_1288/server| (|get.::.1_12… expansions:
• unroll
 expr: (let ((a!1 (|get.::.0_1287/server| (merge_sort_1276/client (odds_1289/se… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (|get.::.1_1288/server| (odds_1289/se… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (|get.::.1_1288/server| (odds_1289/serve… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (|get.::.1_1288/server| (odds_1289/serve… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (|get.::.1_1288/server| (|get.::.1_12… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (|get.::.1_1288/server| (odds_1289/serve… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (|get.::.1_1288/server| (odds_1289/serve… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (|get.::.1_1288/server| (odds_1289/serve… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (|get.::.1_1288/server| (odds_1289/serve… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (odds_1289/server (|get.::.1_1288/server| … expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (|get.::.1_1288/server| (odds_1289/se… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (odds_1289/server (odds_1289/server (odds_1289/server x_1293/client))))… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (odds_1289/server (odds_1289/server (odds_1289/serve… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (odds_1289/server (odds_1289/server (odds_1289/serve… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (odds_1289/server (odds_1289/server (odds_1289/server x_1293/client))))… expansions:
• unroll
 expr: (odds_1289/server (odds_1289/server (odds_1289/server (odds_1289/server x_1293/client)))) expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (odds_1289/server (|get.::.1_1288/server| … expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (odds_1289/server (|get.::.1_1288/server| … expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (odds_1289/server (|get.::.1_1288/server| … expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (|get.::.1_1288/server| (|get.::.1_12… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (odds_1289/server (|get.::.1_1288/server| … expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (odds_1289/server (|get.::.1_1288/server| … expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (odds_1289/server (|get.::.1_1288/server| … expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (|get.::.1_1288/server| (|get.::.1_12… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (odds_1289/server (|get.::.1_1288/server| … expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (|get.::.1_1288/server| (odds_1289/serve… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (|get.::.1_1288/server| (odds_1289/se… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (|get.::.1_1288/server| (odds_1289/serve… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (|get.::.1_1288/server| (odds_1289/serve… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (odds_1289/server (|get.::.1_1288/server| … expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (|get.::.1_1288/server| (odds_1289/serve… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (|get.::.1_1288/server| (odds_1289/serve… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (|get.::.1_1288/server| (odds_1289/serve… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (|get.::.1_1288/server| (odds_1289/serve… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (odds_1289/server (|get.::.1_1288/server| … expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (|get.::.1_1288/server| (odds_1289/serve… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (|get.::.1_1288/server| (odds_1289/serve… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (|get.::.1_1288/server| (|get.::.1_12… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (odds_1289/server (odds_1289/server (|get.::.1_1288/… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (odds_1289/server (|get.::.1_1288/server| … expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (odds_1289/server (odds_1289/server (|get.::.1_1288/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (|get.::.1_1288/server| (odds_1289/se… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (odds_1289/server (odds_1289/server (|get.::.1_1288/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1288/server| (odds_1289/server (odds_1289/server (|get.::.1_1288/… expansions:
• unroll
 expr: (let ((a!1 (odds_1289/server (odds_1289/server (|get.::.1_1288/server| … expansions:

Excellent. This gives us quite some confidence that this result is true. Let's now try to prove it by induction. We'll want to use an induction principle suggested by the definition of merge_sort. Let's use our usual strategy of #max_induct 1, so we can analyse Imandra's output to help us find needed lemmata.

Note, we could prove this theorem directly without any lemmas by using #max_induct 3, but it's good practice to use #max_induct 1 and have Imandra help us develop useful collections of lemmas.

In :
#max_induct 1

Out:

In :
theorem merge_sort_sorts x =
is_sorted (merge_sort x)
[@@induct functional merge_sort]

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

is_sorted (merge_sort x).

1 nontautological subgoal.

We shall induct according to a scheme derived from merge_sort.

Induction scheme:

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

2 nontautological subgoals.

Subgoal 2:

|---------------------------------------------------------------------------
C0. not Is_a([], List.tl x) && x <> []
C1. is_sorted (merge_sort x)

But simplification reduces this to true, using the definitions of is_sorted
and merge_sort.

Subgoal 1:

H0. x <> []
H1. not Is_a([], List.tl x)
H2. is_sorted (merge_sort (odds (List.tl x)))
H3. is_sorted (merge_sort (odds x))
|---------------------------------------------------------------------------
is_sorted (merge_sort x)

This simplifies, using the definition of merge_sort to:

Subgoal 1':

H0. is_sorted (merge_sort (odds x))
H1. x <> []
H2. is_sorted (merge_sort (odds (List.tl x)))
|---------------------------------------------------------------------------
C0. Is_a([], List.tl x)
C1. is_sorted (merge (merge_sort (odds x)) (merge_sort (odds (List.tl x))))

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

This produces the modified subgoal:

Subgoal 1'':

H0. is_sorted (merge_sort (odds x2))
H1. is_sorted (merge_sort (odds (x1 :: x2)))
|---------------------------------------------------------------------------
C0. is_sorted (merge (merge_sort (odds (x1 :: x2))) (merge_sort (odds x2)))
C1. Is_a([], x2)

Candidates for generalization:

odds (x1 :: x2)
odds x2

This produces the modified subgoal:

Subgoal 1''':

H0. is_sorted (merge_sort gen_2)
H1. is_sorted (merge_sort gen_1)
|---------------------------------------------------------------------------
C0. is_sorted (merge (merge_sort gen_1) (merge_sort gen_2))
C1. Is_a([], x2)

Candidates for generalization:

merge_sort gen_1
merge_sort gen_2

This produces the modified subgoal:

Subgoal 1'''':

H0. is_sorted gen_4
H1. is_sorted gen_3
|---------------------------------------------------------------------------
C0. is_sorted (merge gen_3 gen_4)
C1. Is_a([], x2)

Must try induction.

⚠  Aborting proof attempt for merge_sort_sorts.

ⓘ  Rules:
(:def is_sorted)
(:def merge_sort)
(:induct merge_sort)

Checkpoints:

H0. is_sorted gen_4
H1. is_sorted gen_3
|---------------------------------------------------------------------------
C0. is_sorted (merge gen_3 gen_4)
C1. Is_a([], x2)

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


Analysing the output of this proof attempt, we notice the following components of our Checkpoint:

H1. is_sorted gen_1
H2. is_sorted gen_2
|---------------------------------------------------------------------------
is_sorted (merge gen_2 gen_1)


Ah, of course! We need to prove a lemma that merge respects the sortedness of its inputs.

Let's do this by functional induction following the definition of merge and install it as a rewrite rule. We'll allow nested induction (#max_induct 2), but it's a good exercise to do this proof without it (deriving an additional lemma!).

In :
#max_induct 2;;

theorem merge_sorts x y =
is_sorted x && is_sorted y
==>
is_sorted (merge x y)
[@@induct functional merge]
[@@rewrite]

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

is_sorted x && is_sorted y ==> is_sorted (merge x y).

1 nontautological subgoal.

We shall induct according to a scheme derived from merge.

Induction scheme:

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

3 nontautological subgoals.

Subgoal 3:

H0. is_sorted x
H1. is_sorted y
H2. not (not (List.hd y <= List.hd x) && y <> [] && x <> [])
H3. not ((List.hd y <= List.hd x) && y <> [] && x <> [])
|---------------------------------------------------------------------------
is_sorted (merge x y)

But simplification reduces this to true, using the definitions of is_sorted
and merge.

Subgoal 2:

H0. is_sorted x
H1. is_sorted y
H2. x <> []
H3. y <> []
H4. List.hd y <= List.hd x
H5. is_sorted x && is_sorted (List.tl y) ==> is_sorted (merge x (List.tl y))
|---------------------------------------------------------------------------
is_sorted (merge x y)

This simplifies, using the definition of merge to the following 2 subgoals:

Subgoal 2.2:

H0. List.hd y <= List.hd x
H1. is_sorted x
H2. is_sorted y
H3. x <> []
H4. y <> []
|---------------------------------------------------------------------------
C0. is_sorted (merge x (List.tl y))
C1. is_sorted (List.tl y)
C2. is_sorted ((List.hd y) :: (merge x (List.tl y)))

But we verify Subgoal 2.2 by recursive unrolling.

Subgoal 2.1:

H0. List.hd y <= List.hd x
H1. is_sorted x
H2. is_sorted y
H3. x <> []
H4. y <> []
H5. is_sorted (merge x (List.tl y))
|---------------------------------------------------------------------------
is_sorted ((List.hd y) :: (merge x (List.tl y)))

But we verify Subgoal 2.1 by recursive unrolling.

Subgoal 1:

H0. is_sorted x
H1. is_sorted y
H2. x <> []
H3. y <> []
H4. not (List.hd y <= List.hd x)
H5. is_sorted (List.tl x) && is_sorted y ==> is_sorted (merge (List.tl x) y)
|---------------------------------------------------------------------------
is_sorted (merge x y)

This simplifies, using the definition of merge to the following 2 subgoals:

Subgoal 1.2:

H0. is_sorted x
H1. is_sorted y
H2. x <> []
H3. y <> []
|---------------------------------------------------------------------------
C0. is_sorted (merge (List.tl x) y)
C1. is_sorted (List.tl x)
C2. List.hd y <= List.hd x
C3. is_sorted ((List.hd x) :: (merge (List.tl x) y))

But we verify Subgoal 1.2 by recursive unrolling.

Subgoal 1.1:

H0. is_sorted x
H1. is_sorted y
H2. x <> []
H3. y <> []
H4. is_sorted (merge (List.tl x) y)
|---------------------------------------------------------------------------
C0. List.hd y <= List.hd x
C1. is_sorted ((List.hd x) :: (merge (List.tl x) y))

But we verify Subgoal 1.1 by recursive unrolling.

ⓘ  Rules:
(:def is_sorted)
(:def merge)
(:induct merge)


Proved
proof
ground_instances:16
definitions:12
inductions:1
search_time:
0.894s
details:
Expand
smt_stats:
 num checks: 12 arith-make-feasible: 30 arith-max-columns: 19 arith-conflicts: 4 rlimit count: 281359 mk clause: 265 datatype occurs check: 78 mk bool var: 353 arith-lower: 22 arith-diseq: 2 datatype splits: 21 decisions: 93 propagations: 283 arith-max-rows: 9 conflicts: 19 datatype accessor ax: 18 minimized lits: 5 arith-bound-propagations-lp: 1 datatype constructor ax: 48 final checks: 14 added eqs: 540 del clause: 214 arith eq adapter: 12 arith-upper: 18 memory: 34.43 max memory: 44.37 num allocs: 4.87482e+10
Expand
• start[0.894s, "Goal"]
is_sorted ( :var_0: ) && is_sorted ( :var_1: )
==> is_sorted (merge ( :var_0: ) ( :var_1: ))
• #### subproof

not (is_sorted x) || not (is_sorted y) || is_sorted (merge x y)
• start[0.894s, "1"]
not (is_sorted x) || not (is_sorted y) || is_sorted (merge x y)
• induction on (functional merge)
:scheme (not ((List.hd x < List.hd y) && (y <> [] && x <> []))
&& not (not (List.hd x < List.hd y) && (y <> [] && x <> []))
==> φ x y)
&& ((x <> []
&& (y <> [] && (not (List.hd x < List.hd y) && φ x (List.tl y)))
==> φ x y)
&& (x <> []
&& (y <> [] && ((List.hd x < List.hd y) && φ (List.tl x) y))
==> φ x y))
• Split (let (_x_0 : bool) = is_sorted x in
let (_x_1 : bool) = is_sorted y in
let (_x_2 : bool) = is_sorted (merge x y) || not (_x_0 && _x_1) in
let (_x_3 : bool) = List.hd y <= List.hd x in
let (_x_4 : bool) = not _x_3 in
let (_x_5 : bool) = y <> [] in
let (_x_6 : bool) = x <> [] in
let (_x_7 : bool) = _x_6 && _x_5 in
let (_x_8 : int list) = List.tl y in
let (_x_9 : int list) = List.tl x in
(_x_2
|| not (not (_x_4 && _x_5 && _x_6) && not (_x_3 && _x_5 && _x_6)))
&& (_x_2
|| not
(_x_7 && _x_3
&& (is_sorted (merge x _x_8) || not (_x_0 && is_sorted _x_8))))
&& (_x_2
|| not
(_x_7 && _x_4
&& (is_sorted (merge _x_9 y) || not (is_sorted _x_9 && _x_1))))
:cases [let (_x_0 : bool) = List.hd y <= List.hd x in
let (_x_1 : bool) = y <> [] in
let (_x_2 : bool) = x <> [] in
not (is_sorted x) || not (is_sorted y)
|| (not _x_0 && _x_1 && _x_2) || (_x_0 && _x_1 && _x_2)
|| is_sorted (merge x y);
let (_x_0 : bool) = is_sorted x in
let (_x_1 : int list) = List.tl y in
not _x_0 || not (is_sorted y) || not (x <> [])
|| not (y <> []) || not (List.hd y <= List.hd x)
|| not (_x_0 && is_sorted _x_1 ==> is_sorted (merge x _x_1))
|| is_sorted (merge x y);
let (_x_0 : bool) = is_sorted y in
let (_x_1 : int list) = List.tl x in
not (is_sorted x) || not _x_0 || not (x <> [])
|| not (y <> []) || (List.hd y <= List.hd x)
|| not (is_sorted _x_1 && _x_0 ==> is_sorted (merge _x_1 y))
|| is_sorted (merge x y)])
• ##### subproof
let (_x_0 : bool) = is_sorted y in let (_x_1 : int list) = List.tl x in not (is_sorted x) || not _x_0 || not (x <> []) || not (y <> []) || (List.hd y <= List.hd x) || not (is_sorted _x_1 && _x_0 ==> is_sorted (merge _x_1 y)) || is_sorted (merge x y)
• start[0.894s, "1"]
let (_x_0 : bool) = is_sorted y in
let (_x_1 : int list) = List.tl x in
not (is_sorted x) || not _x_0 || not (x <> []) || not (y <> [])
|| (List.hd y <= List.hd x)
|| not (is_sorted _x_1 && _x_0 ==> is_sorted (merge _x_1 y))
|| is_sorted (merge x y)
• ###### simplify
 into: let (_x_0 : int list) = List.tl x in let (_x_1 : int list) = merge _x_0 y in let (_x_2 : bool) = is_sorted _x_1 in let (_x_3 : int) = List.hd x in let (_x_4 : bool) = List.hd y <= _x_3 in let (_x_5 : bool) = not (is_sorted x) in let (_x_6 : bool) = not (is_sorted y) in let (_x_7 : bool) = not (x <> []) in let (_x_8 : bool) = not (y <> []) in let (_x_9 : bool) = is_sorted (_x_3 :: _x_1) in (_x_2 || is_sorted _x_0 || _x_4 || _x_5 || _x_6 || _x_7 || _x_8 || _x_9) && (_x_4 || _x_5 || _x_6 || _x_7 || _x_8 || _x_9 || not _x_2) expansions: [merge, merge] rewrite_steps: forward_chaining:
• Subproof
• Subproof
• ##### subproof
let (_x_0 : bool) = is_sorted x in let (_x_1 : int list) = List.tl y in not _x_0 || not (is_sorted y) || not (x <> []) || not (y <> []) || not (List.hd y <= List.hd x) || not (_x_0 && is_sorted _x_1 ==> is_sorted (merge x _x_1)) || is_sorted (merge x y)
• start[0.894s, "2"]
let (_x_0 : bool) = is_sorted x in
let (_x_1 : int list) = List.tl y in
not _x_0 || not (is_sorted y) || not (x <> []) || not (y <> [])
|| not (List.hd y <= List.hd x)
|| not (_x_0 && is_sorted _x_1 ==> is_sorted (merge x _x_1))
|| is_sorted (merge x y)
• ###### simplify
 into: let (_x_0 : int list) = List.tl y in let (_x_1 : int list) = merge x _x_0 in let (_x_2 : bool) = is_sorted _x_1 in let (_x_3 : int) = List.hd y in let (_x_4 : bool) = not (_x_3 <= List.hd x) in let (_x_5 : bool) = not (is_sorted x) in let (_x_6 : bool) = not (is_sorted y) in let (_x_7 : bool) = not (x <> []) in let (_x_8 : bool) = not (y <> []) in let (_x_9 : bool) = is_sorted (_x_3 :: _x_1) in (_x_2 || is_sorted _x_0 || _x_4 || _x_5 || _x_6 || _x_7 || _x_8 || _x_9) && (_x_4 || _x_5 || _x_6 || _x_7 || _x_8 || _x_9 || not _x_2) expansions: [merge, merge] rewrite_steps: forward_chaining:
• Subproof
• Subproof
• ##### subproof
let (_x_0 : bool) = List.hd y <= List.hd x in let (_x_1 : bool) = y <> [] in let (_x_2 : bool) = x <> [] in not (is_sorted x) || not (is_sorted y) || (not _x_0 && _x_1 && _x_2) || (_x_0 && _x_1 && _x_2) || is_sorted (merge x y)
• start[0.894s, "3"]
let (_x_0 : bool) = List.hd y <= List.hd x in
let (_x_1 : bool) = y <> [] in
let (_x_2 : bool) = x <> [] in
not (is_sorted x) || not (is_sorted y) || (not _x_0 && _x_1 && _x_2)
|| (_x_0 && _x_1 && _x_2) || is_sorted (merge x y)
• ###### simplify
 into: true expansions: [merge, is_sorted, merge, is_sorted, merge, is_sorted, merge, is_sorted] rewrite_steps: forward_chaining:

Excellent! Now that we have that key lemma proved and available as a rewrite rule, let's return to our original goal:

In :
theorem merge_sort_sorts x =
is_sorted (merge_sort x)
[@@induct functional merge_sort]

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

is_sorted (merge_sort x).

1 nontautological subgoal.

We shall induct according to a scheme derived from merge_sort.

Induction scheme:

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

2 nontautological subgoals.

Subgoal 2:

|---------------------------------------------------------------------------
C0. not Is_a([], List.tl x) && x <> []
C1. is_sorted (merge_sort x)

But simplification reduces this to true, using the definitions of is_sorted
and merge_sort.

Subgoal 1:

H0. x <> []
H1. not Is_a([], List.tl x)
H2. is_sorted (merge_sort (odds (List.tl x)))
H3. is_sorted (merge_sort (odds x))
|---------------------------------------------------------------------------
is_sorted (merge_sort x)

This simplifies, using the definition of merge_sort to:

Subgoal 1':

H0. is_sorted (merge_sort (odds x))
H1. x <> []
H2. is_sorted (merge_sort (odds (List.tl x)))
|---------------------------------------------------------------------------
C0. Is_a([], List.tl x)
C1. is_sorted (merge (merge_sort (odds x)) (merge_sort (odds (List.tl x))))

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

ⓘ  Rules:
(:def is_sorted)
(:def merge_sort)
(:rw merge_sorts)
(:induct merge_sort)


Proved
proof
 ground_instances: 0 definitions: 5 inductions: 1 search_time: 0.194s
Expand
• start[0.194s, "Goal"] is_sorted (merge_sort ( :var_0: ))
• #### subproof

is_sorted (merge_sort x)
• start[0.194s, "1"] is_sorted (merge_sort x)
• induction on (functional merge_sort)
:scheme (not (not Is_a([], List.tl x) && x <> []) ==> φ x)
&& (x <> []
&& (not Is_a([], List.tl x)
&& (φ (odds (List.tl x)) && φ (odds x)))
==> φ x)
• Split (let (_x_0 : int list) = List.tl x in
let (_x_1 : bool) = not Is_a([], _x_0) in
let (_x_2 : bool) = x <> [] in
let (_x_3 : bool) = is_sorted (merge_sort x) in
((_x_1 && _x_2) || _x_3)
&& (_x_3
|| not
(_x_2 && _x_1 && is_sorted (merge_sort (odds _x_0))
&& is_sorted (merge_sort (odds x))))
:cases [(not Is_a([], List.tl x) && x <> [])
|| is_sorted (merge_sort x);
let (_x_0 : int list) = List.tl x in
not (x <> []) || Is_a([], _x_0)
|| not (is_sorted (merge_sort (odds _x_0)))
|| not (is_sorted (merge_sort (odds x)))
|| is_sorted (merge_sort x)])
• ##### subproof
let (_x_0 : int list) = List.tl x in not (x <> []) || Is_a([], _x_0) || not (is_sorted (merge_sort (odds _x_0))) || not (is_sorted (merge_sort (odds x))) || is_sorted (merge_sort x)
• start[0.193s, "1"]
let (_x_0 : int list) = List.tl x in
not (x <> []) || Is_a([], _x_0) || not (is_sorted (merge_sort (odds _x_0)))
|| not (is_sorted (merge_sort (odds x))) || is_sorted (merge_sort x)
• ###### simplify
 into: let (_x_0 : int list) = List.tl x in let (_x_1 : int list) = merge_sort (odds x) in let (_x_2 : int list) = merge_sort (odds _x_0) in Is_a([], _x_0) || not (is_sorted _x_1) || not (x <> []) || not (is_sorted _x_2) || is_sorted (merge _x_1 _x_2) expansions: merge_sort rewrite_steps: forward_chaining:
• ###### simplify
 into: true expansions: [] rewrite_steps: merge_sorts forward_chaining:
• ##### subproof
(not Is_a([], List.tl x) && x <> []) || is_sorted (merge_sort x)
• start[0.193s, "2"]
(not Is_a([], List.tl x) && x <> []) || is_sorted (merge_sort x)
• ###### simplify
 into: true expansions: [is_sorted, merge_sort, is_sorted, merge_sort] rewrite_steps: forward_chaining:

Beautiful! So now we've proved half of our specification: merge_sort sorts!

# Merge Sort contains the right elements¶

Let's now turn to the second half of our correctness criterion: That merge_sort x contains "the same" elements as x.

What does this mean, and why does it matter?

## An incorrect sorting function¶

Consider the sorting function bad_sort defined as bad_sort x = [].

Clearly, we could prove theorem bad_sort_sorts x = is_sorted (bad_sort x), even though we'd never want to use bad_sort as a sorting function in practice.

That is, computing a sorted list is only one piece of the puzzle. We must also verify that merge_sort x contains exactly the same elements as x, including their multiplicity).

## Multiset equivalence¶

How can we express this concept? We'll use the notion of a multiset and count the number of occurrences of each element of x, and make sure these are respected by merge_sort.

We'll begin by defining a function num_occurs x y which counts the number of times an element x appears in the list y.

In :
let rec num_occurs x y =
match y with
| [] -> 0
| hd :: tl when hd = x ->
1 + num_occurs x tl
| _ :: tl ->
num_occurs x tl

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

termination proof

### Termination proof

call num_occurs x (List.tl y) from num_occurs x y
original:num_occurs x y
sub:num_occurs x (List.tl y)
original ordinal:Ordinal.Int (_cnt y)
sub ordinal:Ordinal.Int (_cnt (List.tl y))
path:[List.hd y = x && y <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.008s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 12 arith tableau max rows: 6 arith tableau max columns: 13 arith pivots: 6 rlimit count: 4911 mk clause: 26 datatype occurs check: 22 mk bool var: 89 arith assert upper: 10 datatype splits: 3 decisions: 27 arith row summations: 10 propagations: 47 conflicts: 11 arith fixed eqs: 7 datatype accessor ax: 14 arith conflicts: 1 arith num rows: 6 datatype constructor ax: 16 final checks: 6 added eqs: 88 del clause: 9 arith eq adapter: 10 memory: 34.26 max memory: 44.37 num allocs: 5.38063e+10
Expand
• start[0.008s]
let (_x_0 : int) = count.list (const 0) y in
let (_x_1 : ty_0 list) = List.tl y in
let (_x_2 : int) = count.list (const 0) _x_1 in
let (_x_3 : bool) = List.hd _x_1 = x in
let (_x_4 : bool) = _x_1 <> [] in
(List.hd y = x) && (y <> [] && ((_x_0 >= 0) && (_x_2 >= 0)))
==> (not (_x_3 && _x_4) && not (not _x_3 && _x_4))
|| Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ###### simplify
 into: let (_x_0 : ty_0 list) = List.tl y in let (_x_1 : bool) = List.hd _x_0 = x in let (_x_2 : bool) = _x_0 <> [] in let (_x_3 : int) = count.list (const 0) _x_0 in let (_x_4 : int) = count.list (const 0) y in (not (_x_1 && _x_2) && not (not _x_1 && _x_2)) || Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_4) || not ((List.hd y = x) && y <> [] && (_x_4 >= 0) && (_x_3 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.list_3720/server| (|g… expansions:
• unroll
 expr: (|count.list_3720/server| (|get.::.1_3699/server| y_3706/server)) expansions:
• unroll
 expr: (|count.list_3720/server| y_3706/server) expansions:
• Unsat
call num_occurs x (List.tl y) from num_occurs x y
original:num_occurs x y
sub:num_occurs x (List.tl y)
original ordinal:Ordinal.Int (_cnt y)
sub ordinal:Ordinal.Int (_cnt (List.tl y))
path:[not (List.hd y = x) && y <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.010s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 12 arith tableau max rows: 6 arith tableau max columns: 13 arith pivots: 6 rlimit count: 2466 mk clause: 26 datatype occurs check: 22 mk bool var: 89 arith assert upper: 10 datatype splits: 3 decisions: 27 arith row summations: 10 propagations: 47 conflicts: 11 arith fixed eqs: 7 datatype accessor ax: 14 arith conflicts: 1 arith num rows: 6 datatype constructor ax: 16 final checks: 6 added eqs: 81 del clause: 9 arith eq adapter: 10 memory: 34.21 max memory: 44.37 num allocs: 5.33701e+10
Expand
• start[0.010s]
let (_x_0 : int) = count.list (const 0) y in
let (_x_1 : ty_0 list) = List.tl y in
let (_x_2 : int) = count.list (const 0) _x_1 in
let (_x_3 : bool) = List.hd _x_1 = x in
let (_x_4 : bool) = _x_1 <> [] in
not (List.hd y = x) && (y <> [] && ((_x_0 >= 0) && (_x_2 >= 0)))
==> (not (_x_3 && _x_4) && not (not _x_3 && _x_4))
|| Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ###### simplify
 into: let (_x_0 : ty_0 list) = List.tl y in let (_x_1 : bool) = List.hd _x_0 = x in let (_x_2 : bool) = _x_0 <> [] in let (_x_3 : int) = count.list (const 0) _x_0 in let (_x_4 : int) = count.list (const 0) y in (not (_x_1 && _x_2) && not (not _x_1 && _x_2)) || Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_4) || not (not (List.hd y = x) && y <> [] && (_x_4 >= 0) && (_x_3 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.list_3720/server| (|g… expansions:
• unroll
 expr: (|count.list_3720/server| (|get.::.1_3699/server| y_3706/server)) expansions:
• unroll
 expr: (|count.list_3720/server| y_3706/server) expansions:
• Unsat

Anticipating the need to reason about the interplay of num_occurs and merge, let's prove the following nice lemmas characterising their relationship (applying the max_induct 1 strategy to find these lemmas as above is a great exercise).

In :
theorem num_occur_merge a x y =
num_occurs a (merge x y) = num_occurs a x + num_occurs a y
[@@induct functional merge]
[@@rewrite]

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

num_occurs a (merge x y) = num_occurs a x + num_occurs a y.

1 nontautological subgoal.

We shall induct according to a scheme derived from merge.

Induction scheme:

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

3 nontautological subgoals.

Subgoal 3:

H0. not (not (List.hd y <= List.hd x) && y <> [] && x <> [])
H1. not ((List.hd y <= List.hd x) && y <> [] && x <> [])
|---------------------------------------------------------------------------
num_occurs a (merge x y) = num_occurs a x + num_occurs a y

But simplification reduces this to true, using the definitions of merge and
num_occurs.

Subgoal 2:

H0. x <> []
H1. y <> []
H2. List.hd y <= List.hd x
H3. num_occurs a (merge x (List.tl y))
= num_occurs a x + num_occurs a (List.tl y)
|---------------------------------------------------------------------------
num_occurs a (merge x y) = num_occurs a x + num_occurs a y

But simplification reduces this to true, using the definitions of merge and
num_occurs.

Subgoal 1:

H0. x <> []
H1. y <> []
H2. not (List.hd y <= List.hd x)
H3. num_occurs a (merge (List.tl x) y)
= num_occurs a (List.tl x) + num_occurs a y
|---------------------------------------------------------------------------
num_occurs a (merge x y) = num_occurs a x + num_occurs a y

But simplification reduces this to true, using the definitions of merge and
num_occurs.

ⓘ  Rules:
(:def merge)
(:def num_occurs)
(:induct merge)


Proved
proof
 ground_instances: 0 definitions: 14 inductions: 1 search_time: 0.142s
Expand
• start[0.142s, "Goal"]
num_occurs ( :var_0: ) (merge ( :var_1: ) ( :var_2: ))
= num_occurs ( :var_0: ) ( :var_1: ) + num_occurs ( :var_0: ) ( :var_2: )
• #### subproof

num_occurs a (merge x y) = num_occurs a x + num_occurs a y
• start[0.142s, "1"] num_occurs a (merge x y) = num_occurs a x + num_occurs a y
• induction on (functional merge)
:scheme (not ((List.hd x < List.hd y) && (y <> [] && x <> []))
&& not (not (List.hd x < List.hd y) && (y <> [] && x <> []))
==> φ a x y)
&& ((x <> []
&& (y <> []
&& (not (List.hd x < List.hd y) && φ a x (List.tl y)))
==> φ a x y)
&& (x <> []
&& (y <> []
&& ((List.hd x < List.hd y) && φ a (List.tl x) y))
==> φ a x y))
• Split (let (_x_0 : bool) = List.hd y <= List.hd x in
let (_x_1 : bool) = not _x_0 in
let (_x_2 : bool) = y <> [] in
let (_x_3 : bool) = x <> [] in
let (_x_4 : int) = num_occurs a x in
let (_x_5 : int) = num_occurs a y in
let (_x_6 : bool) = num_occurs a (merge x y) = _x_4 + _x_5 in
let (_x_7 : bool) = _x_3 && _x_2 in
let (_x_8 : int list) = List.tl y in
let (_x_9 : int list) = List.tl x in
(not (not (_x_1 && _x_2 && _x_3) && not (_x_0 && _x_2 && _x_3))
|| _x_6)
&& (not
(_x_7 && _x_0
&& (num_occurs a (merge x _x_8) = _x_4 + num_occurs a _x_8))
|| _x_6)
&& (not
(_x_7 && _x_1
&& (num_occurs a (merge _x_9 y) = num_occurs a _x_9 + _x_5))
|| _x_6)
:cases [let (_x_0 : bool) = List.hd y <= List.hd x in
let (_x_1 : bool) = y <> [] in
let (_x_2 : bool) = x <> [] in
(not _x_0 && _x_1 && _x_2) || (_x_0 && _x_1 && _x_2)
|| (num_occurs a (merge x y) = num_occurs a x + num_occurs a y);
let (_x_0 : int list) = List.tl y in
let (_x_1 : int) = num_occurs a x in
not (x <> []) || not (y <> []) || not (List.hd y <= List.hd x)
|| not
(num_occurs a (merge x _x_0) = _x_1 + num_occurs a _x_0)
|| (num_occurs a (merge x y) = _x_1 + num_occurs a y);
let (_x_0 : int list) = List.tl x in
let (_x_1 : int) = num_occurs a y in
not (x <> []) || not (y <> []) || (List.hd y <= List.hd x)
|| not
(num_occurs a (merge _x_0 y) = num_occurs a _x_0 + _x_1)
|| (num_occurs a (merge x y) = num_occurs a x + _x_1)])
• ##### subproof
let (_x_0 : int list) = List.tl x in let (_x_1 : int) = num_occurs a y in not (x <> []) || not (y <> []) || (List.hd y <= List.hd x) || not (num_occurs a (merge _x_0 y) = num_occurs a _x_0 + _x_1) || (num_occurs a (merge x y) = num_occurs a x + _x_1)
• start[0.141s, "1"]
let (_x_0 : int list) = List.tl x in
let (_x_1 : int) = num_occurs a y in
not (x <> []) || not (y <> []) || (List.hd y <= List.hd x)
|| not (num_occurs a (merge _x_0 y) = num_occurs a _x_0 + _x_1)
|| (num_occurs a (merge x y) = num_occurs a x + _x_1)
• ###### simplify
 into: true expansions: [num_occurs, num_occurs, merge] rewrite_steps: forward_chaining:
• ##### subproof
let (_x_0 : int list) = List.tl y in let (_x_1 : int) = num_occurs a x in not (x <> []) || not (y <> []) || not (List.hd y <= List.hd x) || not (num_occurs a (merge x _x_0) = _x_1 + num_occurs a _x_0) || (num_occurs a (merge x y) = _x_1 + num_occurs a y)
• start[0.141s, "2"]
let (_x_0 : int list) = List.tl y in
let (_x_1 : int) = num_occurs a x in
not (x <> []) || not (y <> []) || not (List.hd y <= List.hd x)
|| not (num_occurs a (merge x _x_0) = _x_1 + num_occurs a _x_0)
|| (num_occurs a (merge x y) = _x_1 + num_occurs a y)
• ###### simplify
 into: true expansions: [num_occurs, num_occurs, merge] rewrite_steps: forward_chaining:
• ##### subproof
let (_x_0 : bool) = List.hd y <= List.hd x in let (_x_1 : bool) = y <> [] in let (_x_2 : bool) = x <> [] in (not _x_0 && _x_1 && _x_2) || (_x_0 && _x_1 && _x_2) || (num_occurs a (merge x y) = num_occurs a x + num_occurs a y)
• start[0.141s, "3"]
let (_x_0 : bool) = List.hd y <= List.hd x in
let (_x_1 : bool) = y <> [] in
let (_x_2 : bool) = x <> [] in
(not _x_0 && _x_1 && _x_2) || (_x_0 && _x_1 && _x_2)
|| (num_occurs a (merge x y) = num_occurs a x + num_occurs a y)
• ###### simplify
 into: true expansions: [num_occurs, merge, num_occurs, merge, num_occurs, merge, num_occurs, merge] rewrite_steps: forward_chaining:
In :
theorem num_occurs_arith (x : int list) (a : int) =
x <> [] && List.tl x <> []
==>
num_occurs a (odds (List.tl x))
=
num_occurs a x - num_occurs a (odds x)
[@@induct functional num_occurs]
[@@rewrite]

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

(x <> []) && (List.tl x <> [])
==> num_occurs a (odds (List.tl x)) = num_occurs a x - num_occurs a (odds x).

1 nontautological subgoal.

We shall induct according to a scheme derived from num_occurs.

Induction scheme:

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

3 nontautological subgoals.

Subgoal 3:

H0. not (x = [])
H1. not (List.tl x = [])
H2. not (not (List.hd x = a) && x <> [])
H3. not ((List.hd x = a) && x <> [])
|---------------------------------------------------------------------------
num_occurs a (odds (List.tl x))
= num_occurs a x + (-1) * num_occurs a (odds x)

But simplification reduces this to true.

Subgoal 2:

H0. not (x = [])
H1. not (List.tl x = [])
H2. x <> []
H3. List.hd x = a
H4. not (List.tl x = []) && not (List.tl (List.tl x) = [])
==> num_occurs a (odds (List.tl (List.tl x)))
= num_occurs a (List.tl x) + (-1) * num_occurs a (odds (List.tl x))
|---------------------------------------------------------------------------
num_occurs a (odds (List.tl x))
= num_occurs a x + (-1) * num_occurs a (odds x)

This simplifies, using the definitions of num_occurs and odds to the
following 4 subgoals:

Subgoal 2.4:

H0. x <> []
H1. (List.tl x) <> []
H2. (List.tl (List.tl x)) <> []
H3. num_occurs (List.hd x) (odds (List.tl (List.tl x)))
= num_occurs (List.hd x) (List.tl (List.tl x))
+ (-1) * num_occurs (List.hd x) (odds (List.tl x))
|---------------------------------------------------------------------------
C0. num_occurs (List.hd x) (odds (List.tl x))
= num_occurs (List.hd x) (List.tl x)
+ (-1) * num_occurs (List.hd x) (odds (List.tl (List.tl x)))
C1. List.hd (List.tl x) = List.hd x

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

Subgoal 2.3:

H0. x <> []
H1. (List.tl x) <> []
H2. (List.tl (List.tl x)) <> []
H3. num_occurs (List.hd x) (odds (List.tl (List.tl x)))
= 1 + num_occurs (List.hd x) (List.tl (List.tl x))
+ (-1) * num_occurs (List.hd x) (odds (List.tl x))
H4. List.hd (List.tl x) = List.hd x
|---------------------------------------------------------------------------
num_occurs (List.hd x) (odds (List.tl x))
= num_occurs (List.hd x) (List.tl x)
+ (-1) * num_occurs (List.hd x) (odds (List.tl (List.tl x)))

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

Subgoal 2.2:

H0. x <> []
H1. (List.tl x) <> []
H2. List.tl (List.tl x) = []
|---------------------------------------------------------------------------
C0. 0
= num_occurs (List.hd x) (List.tl x)
+ (-1) * num_occurs (List.hd x) (odds (List.tl (List.tl x)))
C1. List.hd (List.tl x) = List.hd x

This simplifies, using the definitions of num_occurs and odds to:

Subgoal 2.2':

H0. List.tl (List.tl x) = []
H1. x <> []
H2. (List.tl x) <> []
|---------------------------------------------------------------------------
C0. 0 = num_occurs (List.hd x) (List.tl (List.tl x))
C1. List.hd (List.tl x) = List.hd x

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

Subgoal 2.1:

H0. x <> []
H1. (List.tl x) <> []
H2. List.tl (List.tl x) = []
H3. List.hd (List.tl x) = List.hd x
|---------------------------------------------------------------------------
1
= num_occurs (List.hd x) (List.tl x)
+ (-1) * num_occurs (List.hd x) (odds (List.tl (List.tl x)))

This simplifies, using the definitions of num_occurs and odds to:

Subgoal 2.1':

H0. List.tl (List.tl x) = []
H1. x <> []
H2. List.hd (List.tl x) = List.hd x
H3. (List.tl x) <> []
|---------------------------------------------------------------------------
0 = num_occurs (List.hd x) (List.tl (List.tl x))

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

Subgoal 1:

H0. not (x = [])
H1. not (List.tl x = [])
H2. x <> []
H3. not (List.hd x = a)
H4. not (List.tl x = []) && not (List.tl (List.tl x) = [])
==> num_occurs a (odds (List.tl (List.tl x)))
= num_occurs a (List.tl x) + (-1) * num_occurs a (odds (List.tl x))
|---------------------------------------------------------------------------
num_occurs a (odds (List.tl x))
= num_occurs a x + (-1) * num_occurs a (odds x)

This simplifies, using the definitions of num_occurs and odds to the
following 4 subgoals:

Subgoal 1.4:

H0. x <> []
H1. (List.tl x) <> []
H2. (List.tl (List.tl x)) <> []
H3. num_occurs a (odds (List.tl (List.tl x)))
= num_occurs a (List.tl (List.tl x))
+ (-1) * num_occurs a (odds (List.tl x))
|---------------------------------------------------------------------------
C0. List.hd x = a
C1. num_occurs a (odds (List.tl x))
= num_occurs a (List.tl x)
+ (-1) * num_occurs a (odds (List.tl (List.tl x)))
C2. List.hd (List.tl x) = a

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

Subgoal 1.3:

H0. x <> []
H1. (List.tl x) <> []
H2. (List.tl (List.tl x)) <> []
H3. num_occurs a (odds (List.tl (List.tl x)))
= 1 + num_occurs a (List.tl (List.tl x))
+ (-1) * num_occurs a (odds (List.tl x))
H4. List.hd (List.tl x) = a
|---------------------------------------------------------------------------
C0. List.hd x = a
C1. num_occurs a (odds (List.tl x))
= num_occurs a (List.tl x)
+ (-1) * num_occurs a (odds (List.tl (List.tl x)))

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

Subgoal 1.2:

H0. x <> []
H1. (List.tl x) <> []
H2. List.tl (List.tl x) = []
|---------------------------------------------------------------------------
C0. List.hd x = a
C1. 0
= num_occurs a (List.tl x)
+ (-1) * num_occurs a (odds (List.tl (List.tl x)))
C2. List.hd (List.tl x) = a

This simplifies, using the definitions of num_occurs and odds to:

Subgoal 1.2':

H0. List.tl (List.tl x) = []
H1. x <> []
H2. (List.tl x) <> []
|---------------------------------------------------------------------------
C0. List.hd x = a
C1. 0 = num_occurs a (List.tl (List.tl x))
C2. List.hd (List.tl x) = a

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

Subgoal 1.1:

H0. x <> []
H1. (List.tl x) <> []
H2. List.tl (List.tl x) = []
H3. List.hd (List.tl x) = a
|---------------------------------------------------------------------------
C0. List.hd x = a
C1. 1
= num_occurs a (List.tl x)
+ (-1) * num_occurs a (odds (List.tl (List.tl x)))

This simplifies, using the definitions of num_occurs and odds to:

Subgoal 1.1':

H0. List.tl (List.tl x) = []
H1. x <> []
H2. (List.tl x) <> []
|---------------------------------------------------------------------------
C0. 0 = num_occurs (List.hd (List.tl x)) (List.tl (List.tl x))
C1. List.hd x = List.hd (List.tl x)

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

ⓘ  Rules:
(:def num_occurs)
(:def odds)
(:induct num_occurs)


Proved
proof
 ground_instances: 0 definitions: 48 inductions: 1 search_time: 0.828s
Expand
• start[0.828s, "Goal"]
let (_x_0 : int list) = List.tl ( :var_0: ) in
not (( :var_0: ) = []) && not (_x_0 = [])
==> num_occurs ( :var_1: ) (odds _x_0)
= num_occurs ( :var_1: ) ( :var_0: )
- num_occurs ( :var_1: ) (odds ( :var_0: ))
• #### subproof

let (_x_0 : int list) = List.tl x in (x = []) || (_x_0 = []) || (num_occurs a (odds _x_0) = num_occurs a x + (-1) * num_occurs a (odds x))
• start[0.828s, "1"]
let (_x_0 : int list) = List.tl x in
(x = []) || (_x_0 = [])
|| (num_occurs a (odds _x_0)
= num_occurs a x + (-1) * num_occurs a (odds x))
• induction on (functional num_occurs)
:scheme (not (not (List.hd x = a) && x <> [])
&& not ((List.hd x = a) && x <> []) ==> φ a x)
&& ((x <> [] && ((List.hd x = a) && φ a (List.tl x)) ==> φ a x)
&& (x <> [] && (not (List.hd x = a) && φ a (List.tl x))
==> φ a x))
• Split (let (_x_0 : int list) = List.tl x in
let (_x_1 : bool) = not (_x_0 = []) in
let (_x_2 : int) = num_occurs a (odds _x_0) in
let (_x_3 : bool)
= not (not (x = []) && _x_1)
|| (_x_2 = num_occurs a x + (-1) * num_occurs a (odds x))
in
let (_x_4 : bool) = List.hd x = a in
let (_x_5 : bool) = not _x_4 in
let (_x_6 : bool) = x <> [] in
let (_x_7 : int list) = List.tl _x_0 in
let (_x_8 : bool)
= not (_x_1 && not (_x_7 = []))
|| (num_occurs a (odds _x_7) = num_occurs a _x_0 + (-1) * _x_2)
in
(_x_3 || not (not (_x_5 && _x_6) && not (_x_4 && _x_6)))
&& (_x_3 || not (_x_6 && _x_4 && _x_8))
&& (_x_3 || not (_x_6 && _x_5 && _x_8))
:cases [let (_x_0 : int list) = List.tl x in
let (_x_1 : bool) = List.hd x = a in
let (_x_2 : bool) = x <> [] in
(x = []) || (_x_0 = []) || (not _x_1 && _x_2)
|| (_x_1 && _x_2)
|| (num_occurs a (odds _x_0)
= num_occurs a x + (-1) * num_occurs a (odds x));
let (_x_0 : int list) = List.tl x in
let (_x_1 : bool) = _x_0 = [] in
let (_x_2 : int list) = List.tl _x_0 in
let (_x_3 : int) = num_occurs a (odds _x_0) in
(x = []) || _x_1 || not (x <> []) || not (List.hd x = a)
|| not
(not _x_1 && not (_x_2 = [])
==> num_occurs a (odds _x_2)
= num_occurs a _x_0 + (-1) * _x_3)
|| (_x_3 = num_occurs a x + (-1) * num_occurs a (odds x));
let (_x_0 : int list) = List.tl x in
let (_x_1 : bool) = _x_0 = [] in
let (_x_2 : int list) = List.tl _x_0 in
let (_x_3 : int) = num_occurs a (odds _x_0) in
(x = []) || _x_1 || not (x <> []) || (List.hd x = a)
|| not
(not _x_1 && not (_x_2 = [])
==> num_occurs a (odds _x_2)
= num_occurs a _x_0 + (-1) * _x_3)
|| (_x_3 = num_occurs a x + (-1) * num_occurs a (odds x))])
• ##### subproof
let (_x_0 : int list) = List.tl x in let (_x_1 : bool) = _x_0 = [] in let (_x_2 : int list) = List.tl _x_0 in let (_x_3 : int) = num_occurs a (odds _x_0) in (x = []) || _x_1 || not (x <> []) || (List.hd x = a) || not (not _x_1 && not (_x_2 = []) ==> num_occurs a (odds _x_2) = num_occurs a _x_0 + (-1) * _x_3) || (_x_3 = num_occurs a x + (-1) * num_occurs a (odds x))
• start[0.827s, "1"]
let (_x_0 : int list) = List.tl x in
let (_x_1 : bool) = _x_0 = [] in
let (_x_2 : int list) = List.tl _x_0 in
let (_x_3 : int) = num_occurs a (odds _x_0) in
(x = []) || _x_1 || not (x <> []) || (List.hd x = a)
|| not
(not _x_1 && not (_x_2 = [])
==> num_occurs a (odds _x_2) = num_occurs a _x_0 + (-1) * _x_3)
|| (_x_3 = num_occurs a x + (-1) * num_occurs a (odds x))
• ###### simplify
 into: let (_x_0 : int list) = List.tl x in let (_x_1 : bool) = (List.hd x = a) || (x = []) || (_x_0 = []) in let (_x_2 : int list) = List.tl _x_0 in let (_x_3 : bool) = _x_2 = [] in let (_x_4 : bool) = _x_1 || _x_3 in let (_x_5 : int) = num_occurs a (odds _x_2) in let (_x_6 : int) = num_occurs a _x_2 in let (_x_7 : int) = num_occurs a (odds _x_0) in let (_x_8 : int) = (-1) * _x_7 in let (_x_9 : int) = num_occurs a _x_0 + (-1) * _x_5 in let (_x_10 : bool) = _x_7 = _x_9 in let (_x_11 : bool) = List.hd _x_0 = a in let (_x_12 : bool) = not _x_11 in let (_x_13 : bool) = _x_1 || not _x_3 in (_x_4 || not (_x_5 = _x_6 + _x_8) || _x_10 || _x_11) && (_x_4 || _x_10 || not (_x_5 = 1 + _x_6 + _x_8) || _x_12) && (_x_13 || (0 = _x_9) || _x_11) && (_x_13 || (1 = _x_9) || _x_12) expansions: [num_occurs, odds, num_occurs, num_occurs, num_occurs, num_occurs, odds, num_occurs, odds, num_occurs, num_occurs, odds, num_occurs, num_occurs] rewrite_steps: forward_chaining:
• Subproof
• Subproof
• Subproof
• Subproof
• ##### subproof
let (_x_0 : int list) = List.tl x in let (_x_1 : bool) = _x_0 = [] in let (_x_2 : int list) = List.tl _x_0 in let (_x_3 : int) = num_occurs a (odds _x_0) in (x = []) || _x_1 || not (x <> []) || not (List.hd x = a) || not (not _x_1 && not (_x_2 = []) ==> num_occurs a (odds _x_2) = num_occurs a _x_0 + (-1) * _x_3) || (_x_3 = num_occurs a x + (-1) * num_occurs a (odds x))
• start[0.827s, "2"]
let (_x_0 : int list) = List.tl x in
let (_x_1 : bool) = _x_0 = [] in
let (_x_2 : int list) = List.tl _x_0 in
let (_x_3 : int) = num_occurs a (odds _x_0) in
(x = []) || _x_1 || not (x <> []) || not (List.hd x = a)
|| not
(not _x_1 && not (_x_2 = [])
==> num_occurs a (odds _x_2) = num_occurs a _x_0 + (-1) * _x_3)
|| (_x_3 = num_occurs a x + (-1) * num_occurs a (odds x))
• ###### simplify
 into: let (_x_0 : int list) = List.tl x in let (_x_1 : bool) = (x = []) || (_x_0 = []) in let (_x_2 : int list) = List.tl _x_0 in let (_x_3 : bool) = _x_2 = [] in let (_x_4 : bool) = _x_1 || _x_3 in let (_x_5 : int) = List.hd x in let (_x_6 : int) = num_occurs _x_5 (odds _x_0) in let (_x_7 : int) = num_occurs _x_5 (odds _x_2) in let (_x_8 : int) = num_occurs _x_5 _x_0 + (-1) * _x_7 in let (_x_9 : bool) = _x_6 = _x_8 in let (_x_10 : int) = num_occurs _x_5 _x_2 in let (_x_11 : int) = (-1) * _x_6 in let (_x_12 : bool) = List.hd _x_0 = _x_5 in let (_x_13 : bool) = not _x_12 in let (_x_14 : bool) = _x_1 || not _x_3 in (_x_4 || _x_9 || not (_x_7 = _x_10 + _x_11) || _x_12) && (_x_4 || not (_x_7 = 1 + _x_10 + _x_11) || _x_13 || _x_9) && (_x_14 || (0 = _x_8) || _x_12) && (_x_14 || (1 = _x_8) || _x_13) expansions: [num_occurs, odds, num_occurs, num_occurs, num_occurs, num_occurs, odds, num_occurs, odds, num_occurs, num_occurs, odds, num_occurs, num_occurs] rewrite_steps: forward_chaining:
• Subproof
• Subproof
• Subproof
• Subproof
• ##### subproof
let (_x_0 : int list) = List.tl x in let (_x_1 : bool) = List.hd x = a in let (_x_2 : bool) = x <> [] in (x = []) || (_x_0 = []) || (not _x_1 && _x_2) || (_x_1 && _x_2) || (num_occurs a (odds _x_0) = num_occurs a x + (-1) * num_occurs a (odds x))
• start[0.827s, "3"]
let (_x_0 : int list) = List.tl x in
let (_x_1 : bool) = List.hd x = a in
let (_x_2 : bool) = x <> [] in
(x = []) || (_x_0 = []) || (not _x_1 && _x_2) || (_x_1 && _x_2)
|| (num_occurs a (odds _x_0)
= num_occurs a x + (-1) * num_occurs a (odds x))
• ###### simplify
 into: true expansions: [] rewrite_steps: forward_chaining:

Finally, let's put the pieces together and prove our main remaining theorem.

And now, our second main theorem at last:

In :
theorem merge_sort_elements a (x : int list) =
num_occurs a x = num_occurs a (merge_sort x)
[@@induct functional merge_sort]

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

num_occurs a x = num_occurs a (merge_sort x).

1 nontautological subgoal.

We shall induct according to a scheme derived from merge_sort.

Induction scheme:

(not (not Is_a([], List.tl x) && x <> []) ==> φ a x)
&& (x <> []
&& (not Is_a([], List.tl x)
&& (φ a (odds (List.tl x)) && φ a (odds x)))
==> φ a x).

2 nontautological subgoals.

Subgoal 2:

|---------------------------------------------------------------------------
C0. not Is_a([], List.tl x) && x <> []
C1. num_occurs a x = num_occurs a (merge_sort x)

This simplifies, using the definitions of merge_sort and num_occurs to the
following 3 subgoals:

Subgoal 2.3:

H0. Is_a([], List.tl x)
|---------------------------------------------------------------------------
C0. x <> []
C1. num_occurs a x = 0

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

Subgoal 2.2:

H0. Is_a([], List.tl x)
H1. x <> []
|---------------------------------------------------------------------------
C0. List.hd x = a
C1. num_occurs a x = 0

This simplifies, using the definition of num_occurs to:

Subgoal 2.2':

H0. Is_a([], List.tl x)
H1. x <> []
|---------------------------------------------------------------------------
C0. List.hd x = a
C1. num_occurs a (List.tl x) = 0

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

Subgoal 2.1:

H0. Is_a([], List.tl x)
H1. x <> []
H2. List.hd x = a
|---------------------------------------------------------------------------
num_occurs a x = 1

This simplifies, using the definition of num_occurs to:

Subgoal 2.1':

H0. Is_a([], List.tl x)
H1. x <> []
|---------------------------------------------------------------------------
num_occurs (List.hd x) (List.tl x) = 0

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

Subgoal 1:

H0. x <> []
H1. not Is_a([], List.tl x)
H2. num_occurs a (odds (List.tl x))
= num_occurs a (merge_sort (odds (List.tl x)))
H3. num_occurs a (odds x) = num_occurs a (merge_sort (odds x))
|---------------------------------------------------------------------------
num_occurs a x = num_occurs a (merge_sort x)

This simplifies, using the definitions of merge_sort and num_occurs, and the
rewrite rule num_occurs_arith to the following 2 subgoals:

Subgoal 1.2:

H0. num_occurs a (odds x) = num_occurs a (merge_sort (odds x))
H1. x <> []
H2. num_occurs a (List.tl x) + (-1) * num_occurs a (odds x)
= num_occurs a (merge_sort (odds (List.tl x)))
|---------------------------------------------------------------------------
C0. Is_a([], List.tl x)
C1. List.hd x = a
C2. num_occurs a (List.tl x)
= num_occurs a
(merge (merge_sort (odds x)) (merge_sort (odds (List.tl x))))

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

Subgoal 1.1:

H0. num_occurs a (odds x) = num_occurs a (merge_sort (odds x))
H1. x <> []
H2. List.hd x = a
H3. num_occurs a (List.tl x) + (-1) * num_occurs a (odds x)
= (-1) + num_occurs a (merge_sort (odds (List.tl x)))
|---------------------------------------------------------------------------
C0. Is_a([], List.tl x)
C1. num_occurs a (List.tl x)
= (-1)
+ num_occurs a
(merge (merge_sort (odds x)) (merge_sort (odds (List.tl x))))

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

ⓘ  Rules:
(:def merge_sort)
(:def num_occurs)
(:rw num_occur_merge)
(:rw num_occurs_arith)
(:induct merge_sort)


Proved
proof
 ground_instances: 0 definitions: 17 inductions: 1 search_time: 1.272s
Expand
• start[1.272s, "Goal"]
num_occurs ( :var_0: ) ( :var_1: )
= num_occurs ( :var_0: ) (merge_sort ( :var_1: ))
• #### subproof

num_occurs a x = num_occurs a (merge_sort x)
• start[1.272s, "1"] num_occurs a x = num_occurs a (merge_sort x)
• induction on (functional merge_sort)
:scheme (not (not Is_a([], List.tl x) && x <> []) ==> φ a x)
&& (x <> []
&& (not Is_a([], List.tl x)
&& (φ a (odds (List.tl x)) && φ a (odds x)))
==> φ a x)
• Split (let (_x_0 : int list) = List.tl x in
let (_x_1 : bool) = not Is_a([], _x_0) in
let (_x_2 : bool) = x <> [] in
let (_x_3 : bool) = num_occurs a x = num_occurs a (merge_sort x) in
let (_x_4 : int list) = odds _x_0 in
let (_x_5 : int list) = odds x in
((_x_1 && _x_2) || _x_3)
&& (not
(_x_2 && _x_1
&& (num_occurs a _x_4 = num_occurs a (merge_sort _x_4))
&& (num_occurs a _x_5 = num_occurs a (merge_sort _x_5)))
|| _x_3)
:cases [(not Is_a([], List.tl x) && x <> [])
|| (num_occurs a x = num_occurs a (merge_sort x));
let (_x_0 : int list) = List.tl x in
let (_x_1 : int list) = odds _x_0 in
let (_x_2 : int list) = odds x in
not (x <> []) || Is_a([], _x_0)
|| not (num_occurs a _x_1 = num_occurs a (merge_sort _x_1))
|| not (num_occurs a _x_2 = num_occurs a (merge_sort _x_2))
|| (num_occurs a x = num_occurs a (merge_sort x))])
• ##### subproof
let (_x_0 : int list) = List.tl x in let (_x_1 : int list) = odds _x_0 in let (_x_2 : int list) = odds x in not (x <> []) || Is_a([], _x_0) || not (num_occurs a _x_1 = num_occurs a (merge_sort _x_1)) || not (num_occurs a _x_2 = num_occurs a (merge_sort _x_2)) || (num_occurs a x = num_occurs a (merge_sort x))
• start[1.272s, "1"]
let (_x_0 : int list) = List.tl x in
let (_x_1 : int list) = odds _x_0 in
let (_x_2 : int list) = odds x in
not (x <> []) || Is_a([], _x_0)
|| not (num_occurs a _x_1 = num_occurs a (merge_sort _x_1))
|| not (num_occurs a _x_2 = num_occurs a (merge_sort _x_2))
|| (num_occurs a x = num_occurs a (merge_sort x))
• ###### simplify
 into: let (_x_0 : int list) = List.tl x in let (_x_1 : int list) = odds x in let (_x_2 : int) = num_occurs a _x_1 in let (_x_3 : int list) = merge_sort _x_1 in let (_x_4 : bool) = Is_a([], _x_0) || not (_x_2 = num_occurs a _x_3) || not (x <> []) in let (_x_5 : bool) = List.hd x = a in let (_x_6 : int) = num_occurs a _x_0 in let (_x_7 : int) = _x_6 + (-1) * _x_2 in let (_x_8 : int list) = merge_sort (odds _x_0) in let (_x_9 : int) = num_occurs a _x_8 in let (_x_10 : int) = num_occurs a (merge _x_3 _x_8) in (_x_4 || _x_5 || not (_x_7 = _x_9) || (_x_6 = _x_10)) && (_x_4 || not _x_5 || (_x_6 = (-1) + _x_10) || not (_x_7 = (-1) + _x_9)) expansions: [merge_sort, num_occurs, merge_sort, num_occurs, num_occurs] rewrite_steps: num_occurs_arith forward_chaining:
• Subproof
• Subproof
• ##### subproof
(not Is_a([], List.tl x) && x <> []) || (num_occurs a x = num_occurs a (merge_sort x))
• start[1.272s, "2"]
(not Is_a([], List.tl x) && x <> [])
|| (num_occurs a x = num_occurs a (merge_sort x))
• ###### simplify
 into: let (_x_0 : bool) = not Is_a([], List.tl x) in let (_x_1 : bool) = x <> [] in let (_x_2 : int) = num_occurs a x in let (_x_3 : bool) = _x_2 = 0 in let (_x_4 : bool) = _x_0 || not _x_1 in let (_x_5 : bool) = List.hd x = a in (_x_0 || _x_1 || _x_3) && (_x_4 || _x_5 || _x_3) && (_x_4 || not _x_5 || (_x_2 = 1)) expansions: [num_occurs, merge_sort, num_occurs, num_occurs, num_occurs, num_occurs, merge_sort] rewrite_steps: forward_chaining:
• Subproof
• Subproof
• Subproof

So now we're sure merge_sort really is a proper sorting function.

# Merge Sort is Correct!¶

To recap, we've proved:

theorem merge_sort_sorts x =
is_sorted (merge_sort x)


and

theorem merge_sort_elements a (x : int list) =
num_occurs a x = num_occurs a (merge_sort x)


Beautiful! Happy proving (and sorting)!