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 [1]:
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)
[@@adm l, m]
Out[1]:
val merge : int list -> int list -> int 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 (Ordinal.count l); Ordinal.Int (Ordinal.count m)] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub ordinal | Ordinal.of_list [Ordinal.Int (Ordinal.count (List.tl l)); Ordinal.Int (Ordinal.count m)] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| path | [List.hd l < List.hd m && not (m = []) && not (l = [])] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| proof | detailed proof
Expand
|
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 (Ordinal.count l); Ordinal.Int (Ordinal.count m)] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub ordinal | Ordinal.of_list [Ordinal.Int (Ordinal.count l); Ordinal.Int (Ordinal.count (List.tl m))] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| path | [not (List.hd l < List.hd m) && not (m = []) && not (l = [])] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| proof | detailed proof
Expand
|
Let's experiment a bit with merge.
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 [5]:
let rec odds l =
match l with
| [] -> []
| [x] -> [x]
| x :: y :: rst -> x :: odds rst
Out[5]:
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 (Ordinal.count l) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub ordinal | Ordinal.Int (Ordinal.count (List.tl (List.tl l))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| path | [not (List.tl l = [] && l <> []) && not (l = [])] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| proof | detailed proof
Expand
|
Let's compute a bit with odds to better understand how it works.
Defining Merge Sort¶
We can now put the pieces together and define our main merge_sort function, as follows:
In [8]:
let rec merge_sort l =
match l with
| [] -> []
| [_] -> l
| _ :: ls -> merge (merge_sort (odds l)) (merge_sort (odds ls))
Out[8]:
val merge_sort : int list -> int list = <fun>
File "jupyter cell 8", line 1, characters 0-129:
Error: 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 (List.tl l = [] && l <> []) and not (l = [])
could not be proved to decrease (measured subset: (l))
See https://docs.imandra.ai/imandra-docs/notebooks/proving-program-termination/
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 [9]:
let merge_sort_measure x =
Ordinal.of_int (List.length x)
Out[9]:
val merge_sort_measure : 'a list -> Ordinal.t = <fun>
In [10]:
theorem odds_len_1 x =
x <> [] && List.tl x <> []
==>
(List.length (odds x) [@trigger]) < List.length x
[@@induct functional odds] [@@forward_chaining]
Out[10]:
val odds_len_1 : 'a list -> bool = <fun> Goal: x <> [] && List.tl x <> [] ==> List.length (odds x) < List.length x. 1 nontautological subgoal. Subgoal 1: H0. not (x = []) H1. not (List.tl x = []) H2. List.length x <= List.length (odds x) |--------------------------------------------------------------------------- false This simplifies, using the definition of List.length to: Subgoal 1': H0. x <> [] H1. (List.tl x) <> [] H2. List.length (List.tl x) <= (-1 + List.length (odds x)) |--------------------------------------------------------------------------- false We can eliminate destructors by the following substitution: x -> x1 :: x2 This produces the modified subgoal: Subgoal 1'': H0. x2 <> [] H1. List.length x2 <= (-1 + List.length (odds (x1 :: x2))) |--------------------------------------------------------------------------- false Must try induction. Note: We must proceed by induction, but our current subgoal is less appropriate for induction than our original conjecture. Thus, we prefer to abandon our work until now and return our focus to the original conjecture which we shall attempt to prove by induction directly. We shall induct according to a scheme derived from odds. Induction scheme: (not (not (List.tl x = [] && x <> []) && not (x = [])) ==> φ x) && (not (x = []) && not (List.tl x = [] && x <> []) && φ (List.tl (List.tl x)) ==> φ x). 2 nontautological subgoals. Subgoal 2: H0. not (x = []) H1. not (List.tl x = []) H2. List.length x <= List.length (odds x) |--------------------------------------------------------------------------- not (List.tl x = [] && x <> []) && not (x = []) But simplification reduces this to true, using the forward-chaining rule List.len_nonnegative. Subgoal 1: H0. not (x = []) H1. not (List.tl x = [] && x <> []) H2. not (not (List.tl (List.tl x) = []) && not (List.tl (List.tl (List.tl x)) = [])) || not (List.length (List.tl (List.tl x)) <= List.length (odds (List.tl (List.tl x)))) H3. not (x = []) H4. not (List.tl x = []) H5. List.length x <= List.length (odds 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.tl (List.tl x) = [] H3. 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.tl (List.tl x)) <> [] H3. (List.tl (List.tl (List.tl x))) <> [] H4. 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))) This simplifies, using the definition of List.length to: Subgoal 1.2': H0. x <> [] H1. (List.tl x) <> [] H2. (List.tl (List.tl x)) <> [] H3. (List.tl (List.tl (List.tl x))) <> [] H4. List.length (List.tl (List.tl x)) <= (-1 + List.length (odds (List.tl (List.tl x)))) |--------------------------------------------------------------------------- List.length (List.tl (List.tl (List.tl x))) <= (-1 + List.length (odds (List.tl (List.tl x)))) But simplification reduces this to true, using the definition of List.length. Subgoal 1.1: H0. x <> [] H1. (List.tl x) <> [] H2. (List.tl (List.tl x)) <> [] H3. List.tl (List.tl (List.tl x)) = [] H4. 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.1': H0. x <> [] H1. (List.tl x) <> [] H2. (List.tl (List.tl x)) <> [] H3. List.tl (List.tl (List.tl x)) = [] H4. List.length (List.tl (List.tl x)) <= List.length (List.tl (List.tl (List.tl x))) |--------------------------------------------------------------------------- false But simplification reduces this to true, using the definition of List.length.
Proved
proof
| ground_instances | 0 |
| definitions | 14 |
| inductions | 1 |
| search_time | 1.429s |
Expand
start[1.429s, "Goal"] not (:var_0: = []) && not (List.tl :var_0: = []) ==> List.length (odds :var_0:) < List.length :var_0:
subproof
(x = [] || List.tl x = []) || not (List.length x <= List.length (odds x))start[1.429s, "1"] (x = [] || List.tl x = []) || not (List.length x <= List.length (odds x))
simplify
into (x = [] || List.tl x = []) || not (List.length (List.tl x) <= (-1 + List.length (odds x)))
expansions List.length
rewrite_steps forward_chaining List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
Elim_destructor (:cstor :: :replace x1 :: x2 :context [])
induction on (functional odds) :scheme (not (not (List.tl x = [] && x <> []) && not (x = [])) ==> φ x) && (not (x = []) && not (List.tl x = [] && x <> []) && φ (List.tl (List.tl x)) ==> φ x)Split (((not (List.tl x = [] && x <> []) && not (x = []) || not (not (x = []) && not (List.tl x = []))) || not (List.length x <= List.length (odds x))) && ((not ((not (x = []) && not (List.tl x = [] && x <> [])) && (not (not (List.tl (List.tl x) = []) && not (List.tl (List.tl (List.tl x)) = [])) || not (List.length (List.tl (List.tl x)) <= List.length (odds (List.tl (List.tl x)))))) || not (not (x = []) && not (List.tl x = []))) || not (List.length x <= List.length (odds x))) :cases [((x = [] || List.tl x = []) || not (List.length x <= List.length (odds x))) || not (List.tl x = [] && x <> []) && not (x = []); (((x = [] || List.tl x = [] && x <> []) || not (not (not (List.tl (List.tl x) = []) && not (List.tl (List.tl (List.tl x)) = [])) || not (List.length (List.tl (List.tl x)) <= List.length (odds (List.tl (List.tl x)))))) || List.tl x = []) || not (List.length x <= List.length (odds x))])subproof
(((x = [] || List.tl x = [] && x <> []) || not (not (not (List.tl (List.tl x) = []) && not (List.tl (List.tl (List.tl x)) = [])) || not (List.length (List.tl (List.tl x)) <= List.length (odds (List.tl (List.tl x)))))) || List.tl x = []) || not (List.length x <= List.length (odds x))start[0.927s, "1"] (((x = [] || List.tl x = [] && x <> []) || not (not (not (List.tl (List.tl x) = []) && not (List.tl (List.tl (List.tl x)) = [])) || not (List.length (List.tl (List.tl x)) <= List.length (odds (List.tl (List.tl x)))))) || List.tl x = []) || not (List.length x <= List.length (odds x))simplify
into ((((x = [] || List.tl x = []) || not (List.tl (List.tl x) = [])) || not (List.length (List.tl x) <= List.length (odds (List.tl (List.tl x))))) && (((((x = [] || List.tl x = []) || List.length (List.tl (List.tl x)) <= List.length (odds (List.tl (List.tl x)))) || List.tl (List.tl x) = []) || List.tl (List.tl (List.tl x)) = []) || not (List.length (List.tl x) <= List.length (odds (List.tl (List.tl x)))))) && ((((x = [] || List.tl x = []) || List.tl (List.tl x) = []) || not (List.tl (List.tl (List.tl x)) = [])) || not (List.length (List.tl x) <= List.length (odds (List.tl (List.tl x)))))expansions [List.length, odds, List.length]
rewrite_steps forward_chaining List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
Subproof
Subproof
Subproof
subproof
((x = [] || List.tl x = []) || not (List.length x <= List.length (odds x))) || not (List.tl x = [] && x <> []) && not (x = [])start[0.927s, "2"] ((x = [] || List.tl x = []) || not (List.length x <= List.length (odds x))) || not (List.tl x = [] && x <> []) && not (x = [])
simplify
into true
expansions []
rewrite_steps forward_chaining List.len_nonnegative
List.len_nonnegative
Loading..
Now we're ready to define merge_sort. Imandra is able prove it terminating using our custom measure (and lemma!).
In [11]:
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[11]:
val merge_sort : int list -> int 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 (List.tl l = [] && l <> []) && not (l = [])] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| proof | detailed proof
Expand
|
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 (List.tl l = [] && l <> []) && not (l = [])] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| proof | detailed proof
Expand
|
Let's experiment a bit with merge_sort to gain confidence we've defined it correctly.
In [13]:
merge_sort [9;100;6;2;34;19;3;4;7;6]
Out[13]:
- : int 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 [14]:
let rec is_sorted (x : int list) =
match x with
| [] -> true
| [_] -> true
| x :: x' :: xs -> x <= x' && is_sorted (x' :: xs)
Out[14]:
val is_sorted : int list -> bool = <fun>
termination proof
Termination proof
call `is_sorted (List.tl x)` from `is_sorted x`
| original | is_sorted x | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub | is_sorted (List.tl x) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| original ordinal | Ordinal.Int (Ordinal.count x) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub ordinal | Ordinal.Int (Ordinal.count (List.tl x)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| path | [List.hd x <= List.hd (List.tl x) && not (List.tl x = [] && x <> []) && not (x = [])] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| proof | detailed proof
Expand
|
As usual, let's experiment a bit with this definition.
In [18]:
instance (fun x -> List.length x >= 5 && is_sorted x)
Out[18]:
- : int list -> bool = <fun> module CX : sig val x : int list end
Instance (after 11 steps, 0.054s): let (x : int list) = [7719; 7719; 16574; 18856; 24709]
Instance
Loading..
proof attempt
| ground_instances | 11 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||
| definitions | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||
| inductions | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||
| search_time | 0.054s | ||||||||||||||||||||||||||||||||||||||||||||||||||||||
| details | Expand
|
Expand
start[0.054s] List.length :var_0: >= 5 && is_sorted :var_0:
- unroll
expr (is_sorted_1009 x_1014)
expansions - unroll
expr (|List.length_1885| x_1014)
expansions - unroll
expr (|List.length_1885| (|get.::.1_1884| x_1014))
expansions - unroll
expr (|List.length_1885| (|get.::.1_1884| (|get.::.1_1884| x_1014)))
expansions - unroll
expr (is_sorted_1009 (|get.::.1_1884| x_1014))
expansions - unroll
expr (|List.length_1885| (|get.::.1_1884| (|get.::.1_1884| (|get.::.1_1884| x_1014))))
expansions - unroll
expr (is_sorted_1009 (|get.::.1_1884| (|get.::.1_1884| x_1014)))
expansions - unroll
expr (let ((a!1 (|get.::.1_1884| (|get.::.1_1884| (|get.::.1_1884| (|get.::.1_1884| x_1014)))))) (|List…
expansions - unroll
expr (is_sorted_1009 (|get.::.1_1884| (|get.::.1_1884| (|get.::.1_1884| x_1014))))
expansions - unroll
expr (let ((a!1 (|get.::.1_1884| (|get.::.1_1884| (|get.::.1_1884| (|get.::.1_1884| x_1014)))))) (|List…
expansions - unroll
expr (let ((a!1 (|get.::.1_1884| (|get.::.1_1884| (|get.::.1_1884| (|get.::.1_1884| x_1014)))))) (is_so…
expansions - Sat (Some let (x : int list) = [7719; 7719; 16574; 18856; 24709] )
Loading..
In [19]:
instance (fun x -> List.length x >= 5 && is_sorted x && is_sorted (List.rev x))
Out[19]:
- : int list -> bool = <fun> module CX : sig val x : int list end
Instance (after 38 steps, 0.152s): let (x : int list) = [6436; 6436; 6436; 6436; 6436]
Instance
Loading..
proof attempt
| ground_instances | 38 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| definitions | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| inductions | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| search_time | 0.153s | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| details | Expand
|
Expand
start[0.153s] 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 (|List.rev_1898| x_1016)
expansions - unroll
expr (is_sorted_1009 (|List.rev_1898| x_1016))
expansions - unroll
expr (is_sorted_1009 x_1016)
expansions - unroll
expr (|List.length_1895| x_1016)
expansions - unroll
expr (|List.rev_1898| (|get.::.1_1894| x_1016))
expansions - unroll
expr (|List.append_1902| (|List.rev_1898| (|get.::.1_1894| x_1016)) (|::_3| (|get.::.0_1893| x_1016) …
expansions - unroll
expr (|List.length_1895| (|get.::.1_1894| x_1016))
expansions - unroll
expr (|List.rev_1898| (|get.::.1_1894| (|get.::.1_1894| x_1016)))
expansions - unroll
expr (|List.append_1902| (|List.rev_1898| (|get.::.1_1894| (|get.::.1_1894| x_1016))) (|::_3| (|get.:…
expansions - unroll
expr (is_sorted_1009 (|get.::.1_1894| (|List.rev_1898| x_1016)))
expansions - unroll
expr (|List.length_1895| (|get.::.1_1894| (|get.::.1_1894| x_1016)))
expansions - unroll
expr (is_sorted_1009 (|get.::.1_1894| x_1016))
expansions - unroll
expr (|List.append_1902| (|get.::.1_1894| (|List.rev_1898| (|get.::.1_1894| x_1016))) (|::_3| (|get.:…
expansions - unroll
expr (|List.rev_1898| (|get.::.1_1894| (|get.::.1_1894| (|get.::.1_1894| x_1016))))
expansions - unroll
expr (let ((a!1 (|List.rev_1898| (|get.::.1_1894| (|get.::.1_1894| (|get.::.1_1894| x_1016))))) (a!…expansions - unroll
expr (|List.length_1895| (|get.::.1_1894| (|get.::.1_1894| (|get.::.1_1894| x_1016))))
expansions - unroll
expr (is_sorted_1009 (|get.::.1_1894| (|get.::.1_1894| x_1016)))
expansions - unroll
expr (let ((a!1 (|get.::.1_1894| (|List.rev_1898| (|get.::.1_1894| (|get.::.1_1894| x_1016)))))) (|List…
expansions - unroll
expr (let ((a!1 (|get.::.1_1894| (|get.::.1_1894| (|List.rev_1898| (|get.::.1_1894| x_1016)))))) (|List…
expansions - unroll
expr (is_sorted_1009 (|get.::.1_1894| (|get.::.1_1894| (|List.rev_1898| x_1016))))
expansions - unroll
expr (let ((a!1 (|get.::.1_1894| (|get.::.1_1894| (|get.::.1_1894| (|get.::.1_1894| x_1016)))))) (|List…
expansions - unroll
expr (let ((a!1 (|get.::.1_1894| (|get.::.1_1894| (|get.::.1_1894| (|get.::.1_1894| x_1016))))) (a!…expansions - unroll
expr (let ((a!1 (|get.::.1_1894| (|get.::.1_1894| (|get.::.1_1894| (|get.::.1_1894| x_1016)))))) (|List…
expansions - unroll
expr (is_sorted_1009 (|get.::.1_1894| (|get.::.1_1894| (|get.::.1_1894| x_1016))))
expansions - unroll
expr (let ((a!1 (|List.rev_1898| (|get.::.1_1894| (|get.::.1_1894| (|get.::.1_1894| x_1016))))) (a!…expansions - unroll
expr (let ((a!1 (|get.::.1_1894| (|List.rev_1898| (|get.::.1_1894| (|get.::.1_1894| x_1016)))))) (|List…
expansions - unroll
expr (let ((a!1 (|get.::.1_1894| (|get.::.1_1894| (|get.::.1_1894| (|get.::.1_1894| x_1016)))))) (|List…
expansions - unroll
expr (let ((a!1 (|get.::.1_1894| (|get.::.1_1894| (|get.::.1_1894| (|get.::.1_1894| x_1016)))))) (|List…
expansions - unroll
expr (let ((a!1 (|get.::.1_1894| (|get.::.1_1894| (|get.::.1_1894| (|get.::.1_1894| x_1016)))))) (|List…
expansions - unroll
expr (let ((a!1 (|get.::.1_1894| (|get.::.1_1894| (|List.rev_1898| (|get.::.1_1894| x_1016)))))) (|List…
expansions - unroll
expr (let ((a!1 (|get.::.1_1894| (|get.::.1_1894| (|get.::.1_1894| (|get.::.1_1894| x_1016)))))) (is_so…
expansions - unroll
expr (let ((a!1 (|get.::.1_1894| (|get.::.1_1894| (|get.::.1_1894| (|get.::.1_1894| x_1016))))) (a!…expansions - unroll
expr (let ((a!1 (|List.rev_1898| (|get.::.1_1894| (|get.::.1_1894| (|get.::.1_1894| x_1016))))) (a!…expansions - unroll
expr (let ((a!1 (|get.::.1_1894| (|List.rev_1898| (|get.::.1_1894| (|get.::.1_1894| x_1016)))))) (|List…
expansions - unroll
expr (let ((a!1 (|get.::.1_1894| (|get.::.1_1894| (|get.::.1_1894| (|List.rev_1898| x_1016)))))) (is_so…
expansions - unroll
expr (let ((a!1 (|get.::.1_1894| (|get.::.1_1894| (|List.rev_1898| (|get.::.1_1894| x_1016)))))) (|List…
expansions - unroll
expr (let ((a!1 (|List.rev_1898| (|get.::.1_1894| (|get.::.1_1894| (|get.::.1_1894| x_1016))))) (a!…expansions - unroll
expr (let ((a!1 (|get.::.1_1894| (|get.::.1_1894| (|get.::.1_1894| (|List.rev_1898| x_1016)))))) (is_so…
expansions - Sat (Some let (x : int list) = [6436; 6436; 6436; 6436; 6436] )
Loading..
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 [20]:
verify (fun x -> is_sorted (merge_sort x))
Out[20]:
- : int list -> bool = <fun>
Unknown (Verified up to bound 100)
Expand
| expanded |
|
| blocked |
|
Loading..
proof attempt
| ground_instances | 100 |
| definitions | 0 |
| inductions | 0 |
| search_time | 4.291s |
Expand
start[4.291s] is_sorted (merge_sort :var_0:)
- unroll
expr (merge_sort_1005 x_1018)
expansions - unroll
expr (is_sorted_1009 (merge_sort_1005 x_1018))
expansions - unroll
expr (odds_1916 (|get.::.1_1915| x_1018))
expansions - unroll
expr (merge_sort_1005 (odds_1916 (|get.::.1_1915| x_1018)))
expansions - unroll
expr (odds_1916 x_1018)
expansions - unroll
expr (merge_sort_1005 (odds_1916 x_1018))
expansions - unroll
expr (merge_982 (merge_sort_1005 (odds_1916 x_1018)) (merge_sort_1005 (odds_1916 (|get.::.1_19…expansions - unroll
expr (odds_1916 (|get.::.1_1915| (|get.::.1_1915| x_1018)))
expansions - unroll
expr (odds_1916 (|get.::.1_1915| (|get.::.1_1915| (|get.::.1_1915| x_1018))))
expansions - unroll
expr (is_sorted_1009 (|get.::.1_1915| (merge_sort_1005 x_1018)))
expansions - unroll
expr (odds_1916 (|get.::.1_1915| (odds_1916 (|get.::.1_1915| x_1018))))
expansions - unroll
expr (let ((a!1 (odds_1916 (|get.::.1_1915| (odds_1916 (|get.::.1_1915| x_1018)))))) (merge_sort_1005 a…
expansions - unroll
expr (odds_1916 (odds_1916 (|get.::.1_1915| x_1018)))
expansions - unroll
expr (odds_1916 (|get.::.1_1915| (odds_1916 x_1018)))
expansions - unroll
expr (merge_sort_1005 (odds_1916 (odds_1916 (|get.::.1_1915| x_1018))))
expansions - unroll
expr (let ((a!1 (merge_sort_1005 (odds_1916 (odds_1916 (|get.::.1_1915| x_1018))))) (a!2 (odds_1916…expansions - unroll
expr (let ((a!1 (|get.::.0_1914| (merge_sort_1005 (odds_1916 (|get.::.1_1915| x_1018))))) (a!4 (|ge…expansions - unroll
expr (merge_sort_1005 (odds_1916 (|get.::.1_1915| (odds_1916 x_1018))))
expansions - unroll
expr (odds_1916 (odds_1916 x_1018))
expansions - unroll
expr (merge_sort_1005 (odds_1916 (odds_1916 x_1018)))
expansions - unroll
expr (let ((a!1 (merge_sort_1005 (odds_1916 (|get.::.1_1915| (odds_1916 x_1018)))))) (merge_982 (merge_…
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (|get.::.1_1915| (odds_1916 (|get.::.1_1915| x_1018)))))) (odds_1916 a…
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (|get.::.1_1915| (|get.::.1_1915| (|get.::.1_1915| x_1018)))))) (odds_…
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (|get.::.1_1915| (odds_1916 (|get.::.1_1915| x_1018)))))) (odds_1916 (…
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (|get.::.1_1915| (|get.::.1_1915| (|get.::.1_1915| x_1018)))))) (odds_…
expansions - unroll
expr (let ((a!1 (odds_1916 (odds_1916 (odds_1916 (|get.::.1_1915| x_1018))))) (a!2 (|get.::.1_1915|…expansions - unroll
expr (odds_1916 (|get.::.1_1915| (|get.::.1_1915| (odds_1916 x_1018))))
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (|get.::.1_1915| (|get.::.1_1915| (odds_1916 x_1018)))))) (odds_1916 a…
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (odds_1916 (|get.::.1_1915| (odds_1916 x_1018)))))) (odds_1916 a!1))
expansions - unroll
expr (is_sorted_1009 (|get.::.1_1915| (|get.::.1_1915| (merge_sort_1005 x_1018))))
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (odds_1916 (|get.::.1_1915| (odds_1916 x_1018)))))) (merge_sort_1005 (…
expansions - unroll
expr (odds_1916 (odds_1916 (|get.::.1_1915| (odds_1916 x_1018))))
expansions - unroll
expr (let ((a!1 (odds_1916 (odds_1916 (|get.::.1_1915| (odds_1916 x_1018)))))) (merge_sort_1005 a!1))
expansions - unroll
expr (let ((a!1 (odds_1916 (odds_1916 (|get.::.1_1915| (odds_1916 x_1018))))) (a!2 (|get.::.1_1915|…expansions - unroll
expr (let ((a!1 (odds_1916 (|get.::.1_1915| (odds_1916 (|get.::.1_1915| x_1018)))))) (odds_1916 (|get.:…
expansions - unroll
expr (odds_1916 (|get.::.1_1915| (odds_1916 (odds_1916 x_1018))))
expansions - unroll
expr (let ((a!1 (odds_1916 (|get.::.1_1915| (odds_1916 (odds_1916 x_1018)))))) (merge_sort_1005 a!1))
expansions - unroll
expr (odds_1916 (odds_1916 (odds_1916 x_1018)))
expansions - unroll
expr (merge_sort_1005 (odds_1916 (odds_1916 (odds_1916 x_1018))))
expansions - unroll
expr (let ((a!1 (odds_1916 (|get.::.1_1915| (odds_1916 (|get.::.1_1915| x_1018)))))) (merge_sort_1005 (…
expansions - unroll
expr (let ((a!1 (merge_sort_1005 (odds_1916 (odds_1916 (odds_1916 x_1018))))) (a!2 (odds_1916 (|get…expansions - unroll
expr (let ((a!1 (merge_sort_1005 (odds_1916 (|get.::.1_1915| (odds_1916 x_1018))))) (a!2 (|get.::.0…expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (odds_1916 (odds_1916 (|get.::.1_1915| x_1018)))))) (odds_1916 a!1))
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (odds_1916 (odds_1916 (|get.::.1_1915| x_1018)))))) (merge_sort_1005 (…
expansions - unroll
expr (let ((a!1 (odds_1916 (|get.::.1_1915| (odds_1916 (|get.::.1_1915| x_1018)))))) (odds_1916 a!1))
expansions - unroll
expr (odds_1916 (odds_1916 (odds_1916 (|get.::.1_1915| x_1018))))
expansions - unroll
expr (let ((a!1 (odds_1916 (odds_1916 (odds_1916 (|get.::.1_1915| x_1018)))))) (merge_sort_1005 a!1))
expansions - unroll
expr (let ((a!1 (|get.::.0_1914| (merge_sort_1005 (odds_1916 (|get.::.1_1915| x_1018))))) (a!3 (|ge…expansions - unroll
expr (let ((a!1 (odds_1916 (|get.::.1_1915| (odds_1916 (|get.::.1_1915| x_1018))))) (a!2 (merge_sor…expansions - unroll
expr (let ((a!1 (odds_1916 (|get.::.1_1915| (odds_1916 (|get.::.1_1915| x_1018)))))) (merge_sort_1005 (…
expansions - unroll
expr (let ((a!1 (odds_1916 (|get.::.1_1915| (odds_1916 (|get.::.1_1915| x_1018)))))) (merge_982 (merge_…
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (|get.::.1_1915| (|get.::.1_1915| (merge_sort_1005 x_1018)))))) (is_so…
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (odds_1916 (|get.::.1_1915| (odds_1916 x_1018)))))) (odds_1916 (|get.:…
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (|get.::.1_1915| (odds_1916 (odds_1916 x_1018)))))) (odds_1916 a!1))
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (|get.::.1_1915| (odds_1916 (|get.::.1_1915| x_1018)))))) (odds_1916 (…
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (|get.::.1_1915| (|get.::.1_1915| (odds_1916 x_1018)))))) (odds_1916 (…
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (|get.::.1_1915| (|get.::.1_1915| (|get.::.1_1915| x_1018)))))) (odds_…
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (|get.::.1_1915| (|get.::.1_1915| (|get.::.1_1915| x_1018)))))) (odds_…
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (|get.::.1_1915| (odds_1916 (odds_1916 x_1018)))))) (odds_1916 (|get.:…
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (|get.::.1_1915| (odds_1916 (|get.::.1_1915| x_1018)))))) (odds_1916 (…
expansions - unroll
expr (let ((a!1 (odds_1916 (|get.::.1_1915| (odds_1916 (odds_1916 x_1018)))))) (odds_1916 (|get.::.1_19…
expansions - unroll
expr (let ((a!1 (odds_1916 (|get.::.1_1915| (odds_1916 (odds_1916 x_1018)))))) (merge_sort_1005 (odds_1…
expansions - unroll
expr (let ((a!1 (odds_1916 (|get.::.1_1915| (odds_1916 (odds_1916 x_1018)))))) (odds_1916 a!1))
expansions - unroll
expr (let ((a!1 (odds_1916 (|get.::.1_1915| (odds_1916 (odds_1916 x_1018)))))) (merge_sort_1005 (odds_1…
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (odds_1916 (odds_1916 (|get.::.1_1915| x_1018))))) (a!2 (odds_1916…expansions - unroll
expr (let ((a!1 (odds_1916 (|get.::.1_1915| (odds_1916 (odds_1916 x_1018)))))) (merge_982 (merge_sort_1…
expansions - unroll
expr (let ((a!1 (odds_1916 (|get.::.1_1915| (odds_1916 (odds_1916 x_1018))))) (a!2 (merge_sort_1005…expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (odds_1916 (odds_1916 (odds_1916 x_1018)))))) (odds_1916 a!1))
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (odds_1916 (odds_1916 (odds_1916 x_1018)))))) (merge_sort_1005 (odds_1…
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (|get.::.1_1915| (|get.::.1_1915| (odds_1916 x_1018)))))) (odds_1916 (…
expansions - unroll
expr (odds_1916 (odds_1916 (odds_1916 (odds_1916 x_1018))))
expansions - unroll
expr (let ((a!1 (odds_1916 (odds_1916 (odds_1916 (odds_1916 x_1018)))))) (merge_sort_1005 a!1))
expansions - unroll
expr (let ((a!1 (odds_1916 (odds_1916 (odds_1916 (odds_1916 x_1018))))) (a!2 (|get.::.1_1915| (odds…expansions - unroll
expr (let ((a!1 (merge_sort_1005 (odds_1916 (|get.::.1_1915| (odds_1916 x_1018))))) (a!2 (|get.::.0…expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (odds_1916 (|get.::.1_1915| (odds_1916 x_1018)))))) (odds_1916 (|get.:…
expansions - unroll
expr (let ((a!1 (odds_1916 (|get.::.1_1915| (odds_1916 (|get.::.1_1915| x_1018)))))) (odds_1916 (|get.:…
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (odds_1916 (odds_1916 (|get.::.1_1915| x_1018)))))) (odds_1916 (|get.:…
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (odds_1916 (|get.::.1_1915| (odds_1916 x_1018)))))) (odds_1916 (|get.:…
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (odds_1916 (|get.::.1_1915| (odds_1916 x_1018)))))) (merge_sort_1005 (…
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (odds_1916 (|get.::.1_1915| (odds_1916 x_1018)))))) (odds_1916 (odds_1…
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (odds_1916 (|get.::.1_1915| (odds_1916 x_1018)))))) (merge_sort_1005 (…
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (odds_1916 (|get.::.1_1915| (odds_1916 x_1018)))))) (let ((a!2 (merge_so…
expansions - unroll
expr (let ((a!1 (odds_1916 (odds_1916 (|get.::.1_1915| (odds_1916 x_1018)))))) (odds_1916 (|get.::.1_19…
expansions - unroll
expr (let ((a!1 (odds_1916 (odds_1916 (|get.::.1_1915| (odds_1916 x_1018)))))) (merge_sort_1005 (odds_1…
expansions - unroll
expr (let ((a!1 (odds_1916 (odds_1916 (|get.::.1_1915| (odds_1916 x_1018)))))) (odds_1916 a!1))
expansions - unroll
expr (let ((a!1 (odds_1916 (odds_1916 (|get.::.1_1915| (odds_1916 x_1018)))))) (merge_sort_1005 (odds_1…
expansions - unroll
expr (let ((a!1 (odds_1916 (odds_1916 (|get.::.1_1915| (odds_1916 x_1018)))))) (merge_982 (merge_sort_1…
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (odds_1916 (|get.::.1_1915| (odds_1916 x_1018))))) (a!2 (odds_1916…expansions - unroll
expr (let ((a!1 (odds_1916 (|get.::.1_1915| (odds_1916 (|get.::.1_1915| x_1018)))))) (odds_1916 (|get.:…
expansions - unroll
expr (let ((a!1 (odds_1916 (|get.::.1_1915| (odds_1916 (|get.::.1_1915| x_1018)))))) (odds_1916 (|get.:…
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (odds_1916 (odds_1916 (|get.::.1_1915| x_1018)))))) (odds_1916 (|get.:…
expansions - unroll
expr (let ((a!1 (odds_1916 (odds_1916 (odds_1916 (|get.::.1_1915| x_1018)))))) (merge_sort_1005 (odds_1…
expansions - unroll
expr (let ((a!1 (|get.::.0_1914| (merge_sort_1005 (odds_1916 (|get.::.1_1915| x_1018))))) (a!3 (|ge…expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (odds_1916 (odds_1916 (|get.::.1_1915| x_1018)))))) (odds_1916 (|get.:…
expansions - unroll
expr (let ((a!1 (odds_1916 (|get.::.1_1915| (odds_1916 (|get.::.1_1915| x_1018)))))) (let ((a!2 (odds_191…
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (odds_1916 (odds_1916 (|get.::.1_1915| x_1018)))))) (merge_sort_1005 (…
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (odds_1916 (odds_1916 (|get.::.1_1915| x_1018)))))) (odds_1916 (odds_1…
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (odds_1916 (odds_1916 (|get.::.1_1915| x_1018)))))) (merge_sort_1005 (…
expansions - unroll
expr (let ((a!1 (|get.::.1_1915| (odds_1916 (odds_1916 (|get.::.1_1915| x_1018)))))) (let ((a!2 (merge_so…
expansions - unroll
expr (let ((a!1 (odds_1916 (|get.::.1_1915| (odds_1916 (|get.::.1_1915| x_1018)))))) (odds_1916 (odds_1…
expansions
Loading..
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 [22]:
theorem merge_sort_sorts x =
is_sorted (merge_sort x)
[@@induct functional merge_sort]
Out[22]:
val merge_sort_sorts : int list -> bool = <fun> Goal: is_sorted (merge_sort x). 1 nontautological subgoal. Subgoal 1: |--------------------------------------------------------------------------- is_sorted (merge_sort x) Must try induction. We shall induct according to a scheme derived from merge_sort. Induction scheme: (not (not (List.tl x = [] && x <> []) && not (x = [])) ==> φ x) && (not (x = []) && not (List.tl x = [] && x <> []) && φ (odds (List.tl x)) && φ (odds x) ==> φ x). 2 nontautological subgoals. Subgoal 1.2: |--------------------------------------------------------------------------- C0. not (List.tl x = [] && x <> []) && not (x = []) C1. is_sorted (merge_sort x) But simplification reduces this to true, using the definitions of is_sorted and merge_sort. Subgoal 1.1: H0. not (x = []) H1. not (List.tl x = [] && 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.1': H0. x <> [] H1. (List.tl x) <> [] H2. is_sorted (merge_sort (odds (List.tl x))) H3. is_sorted (merge_sort (odds x)) |--------------------------------------------------------------------------- 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.1'': H0. x2 <> [] H1. is_sorted (merge_sort (odds x2)) H2. is_sorted (merge_sort (odds (x1 :: x2))) |--------------------------------------------------------------------------- is_sorted (merge (merge_sort (odds (x1 :: x2))) (merge_sort (odds x2))) Candidates for generalization: merge_sort (odds x2) merge_sort (odds (x1 :: x2)) This produces the modified subgoal: Subgoal 1.1''': H0. x2 <> [] H1. is_sorted gen_1 H2. is_sorted gen_2 |--------------------------------------------------------------------------- is_sorted (merge gen_2 gen_1) Must try induction. Checkpoints: H0. x2 <> [] H1. is_sorted gen_1 H2. is_sorted gen_2 |--------------------------------------------------------------------------- is_sorted (merge gen_2 gen_1) Error: Maximum induction depth reached (1). You can set this with #max_induct.
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 [23]:
#max_induct 2;;
theorem merge_sorts x y =
is_sorted x && is_sorted y
==>
is_sorted (merge x y)
[@@induct functional merge]
[@@rewrite]
Out[23]:
val merge_sorts : int list -> int list -> bool = <fun> Goal: is_sorted x && is_sorted y ==> is_sorted (merge x y). 1 nontautological subgoal. Subgoal 1: H0. is_sorted x H1. is_sorted y |--------------------------------------------------------------------------- is_sorted (merge x y) Must try induction. We shall induct according to a scheme derived from merge. Induction scheme: (not (List.hd x < List.hd y && not (y = []) && not (x = [])) && not (not (List.hd x < List.hd y) && not (y = []) && not (x = [])) ==> φ y x) && (not (x = []) && not (y = []) && not (List.hd x < List.hd y) && φ (List.tl y) x ==> φ y x) && (not (x = []) && not (y = []) && List.hd x < List.hd y && φ y (List.tl x) ==> φ y x). 3 nontautological subgoals. Subgoal 1.3: H0. not ((not (List.hd y <= List.hd x) && not (y = [])) && not (x = [])) H1. not ((List.hd y <= List.hd x && not (y = [])) && not (x = [])) H2. is_sorted x H3. is_sorted y |--------------------------------------------------------------------------- is_sorted (merge x y) But simplification reduces this to true, using the definition of merge. Subgoal 1.2: H0. not (x = []) H1. not (y = []) H2. List.hd y <= List.hd x H3. is_sorted x && is_sorted (List.tl y) ==> is_sorted (merge x (List.tl y)) H4. is_sorted x H5. is_sorted y |--------------------------------------------------------------------------- is_sorted (merge x y) This simplifies, using the definitions of is_sorted and merge to the following 3 subgoals: Subgoal 1.2.3: H0. x <> [] H1. y <> [] H2. List.hd y <= List.hd x H3. is_sorted (merge x (List.tl y)) H4. is_sorted x H5. is_sorted (List.tl y) H6. (List.tl y) <> [] H7. List.hd y <= List.hd (List.tl y) H8. (merge x (List.tl y)) <> [] |--------------------------------------------------------------------------- List.hd y <= List.hd (merge x (List.tl y)) But we verify Subgoal 1.2.3 by recursive unrolling. Subgoal 1.2.2: H0. x <> [] H1. y <> [] H2. List.hd y <= List.hd x H3. is_sorted x H4. List.tl y = [] H5. (merge x (List.tl y)) <> [] |--------------------------------------------------------------------------- List.hd y <= List.hd (merge x (List.tl y)) But simplification reduces this to true, using the definition of merge. Subgoal 1.2.1: H0. x <> [] H1. y <> [] H2. List.hd y <= List.hd x H3. is_sorted x H4. List.tl y = [] H5. (merge x (List.tl y)) <> [] H6. List.hd y <= List.hd (merge x (List.tl y)) |--------------------------------------------------------------------------- is_sorted (merge x (List.tl y)) But simplification reduces this to true, using the definition of merge. Subgoal 1.1: H0. not (x = []) H1. not (y = []) H2. not (List.hd y <= List.hd x) H3. is_sorted (List.tl x) && is_sorted y ==> is_sorted (merge (List.tl x) y) H4. is_sorted x H5. is_sorted y |--------------------------------------------------------------------------- is_sorted (merge x y) This simplifies, using the definitions of is_sorted and merge to the following 3 subgoals: Subgoal 1.1.3: H0. x <> [] H1. y <> [] H2. is_sorted (merge (List.tl x) y) H3. is_sorted (List.tl x) H4. (List.tl x) <> [] H5. List.hd x <= List.hd (List.tl x) H6. is_sorted y H7. (merge (List.tl x) y) <> [] |--------------------------------------------------------------------------- C0. List.hd y <= List.hd x C1. List.hd x <= List.hd (merge (List.tl x) y) But we verify Subgoal 1.1.3 by recursive unrolling. Subgoal 1.1.2: H0. x <> [] H1. y <> [] H2. List.tl x = [] H3. is_sorted y H4. (merge (List.tl x) y) <> [] |--------------------------------------------------------------------------- C0. List.hd y <= List.hd x C1. List.hd x <= List.hd (merge (List.tl x) y) But simplification reduces this to true, using the definition of merge. Subgoal 1.1.1: H0. x <> [] H1. y <> [] H2. List.tl x = [] H3. is_sorted y H4. (merge (List.tl x) y) <> [] H5. List.hd x <= List.hd (merge (List.tl x) y) |--------------------------------------------------------------------------- C0. List.hd y <= List.hd x C1. is_sorted (merge (List.tl x) y) But simplification reduces this to true, using the definition of merge.
Proved
proof
| ground_instances | 6 | ||||||||||||||||||||||||||||||||||||||||||||||||||
| definitions | 21 | ||||||||||||||||||||||||||||||||||||||||||||||||||
| inductions | 1 | ||||||||||||||||||||||||||||||||||||||||||||||||||
| search_time | 2.729s | ||||||||||||||||||||||||||||||||||||||||||||||||||
| details | Expand
|
Expand
start[2.729s, "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[2.729s, "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 && not (y = []) && not (x = [])) && not (not (List.hd x < List.hd y) && not (y = []) && not (x = [])) ==> φ y x) && (not (x = []) && not (y = []) && not (List.hd x < List.hd y) && φ (List.tl y) x ==> φ y x) && (not (x = []) && not (y = []) && List.hd x < List.hd y && φ y (List.tl x) ==> φ y x)Split (((((not (not ((not (List.hd y <= List.hd x) && not (y = [])) && not (x = [])) && not ((List.hd y <= List.hd x && not (y = [])) && not (x = []))) || not (is_sorted x)) || not (is_sorted y)) || is_sorted (merge x y)) && (((not (((not (x = []) && not (y = [])) && List.hd y <= List.hd x) && ((not (is_sorted x) || not (is_sorted (List.tl y))) || is_sorted (merge x (List.tl y)))) || not (is_sorted x)) || not (is_sorted y)) || is_sorted (merge x y))) && (((not (((not (x = []) && not (y = [])) && not (List.hd y <= List.hd x)) && ((not (is_sorted (List.tl x)) || not (is_sorted y)) || is_sorted (merge (List.tl x) y))) || not (is_sorted x)) || not (is_sorted y)) || is_sorted (merge x y)) :cases [((((not (List.hd y <= List.hd x) && not (y = [])) && not (x = []) || (List.hd y <= List.hd x && not (y = [])) && not (x = [])) || not (is_sorted x)) || not (is_sorted y)) || is_sorted (merge x y); (((((x = [] || y = []) || not (List.hd y <= List.hd x)) || not (not (is_sorted x && is_sorted (List.tl y)) || is_sorted (merge x (List.tl y)))) || not (is_sorted x)) || not (is_sorted y)) || is_sorted (merge x y); (((((x = [] || y = []) || List.hd y <= List.hd x) || not (not (is_sorted (List.tl x) && is_sorted y) || is_sorted (merge (List.tl x) y))) || not (is_sorted x)) || not (is_sorted y)) || is_sorted (merge x y)])subproof
(((((x = [] || y = []) || List.hd y <= List.hd x) || not (not (is_sorted (List.tl x) && is_sorted y) || is_sorted (merge (List.tl x) y))) || not (is_sorted x)) || not (is_sorted y)) || is_sorted (merge x y)start[2.492s, "1.1"] (((((x = [] || y = []) || List.hd y <= List.hd x) || not (not (is_sorted (List.tl x) && is_sorted y) || is_sorted (merge (List.tl x) y))) || not (is_sorted x)) || not (is_sorted y)) || is_sorted (merge x y)simplify
into ((((((((((x = [] || y = []) || List.hd y <= List.hd x) || not (is_sorted (merge (List.tl x) y))) || not (is_sorted (List.tl x))) || List.tl x = []) || not (List.hd x <= List.hd (List.tl x))) || not (is_sorted y)) || merge (List.tl x) y = []) || List.hd x <= List.hd (merge (List.tl x) y)) && ((((((x = [] || y = []) || List.hd y <= List.hd x) || not (List.tl x = [])) || not (is_sorted y)) || merge (List.tl x) y = []) || List.hd x <= List.hd (merge (List.tl x) y))) && (((((((x = [] || y = []) || List.hd y <= List.hd x) || not (List.tl x = [])) || not (is_sorted y)) || is_sorted (merge (List.tl x) y)) || merge (List.tl x) y = []) || not (List.hd x <= List.hd (merge (List.tl x) y)))expansions [merge, is_sorted, is_sorted, merge, is_sorted, is_sorted, is_sorted, merge]
rewrite_steps forward_chaining Subproof
Subproof
Subproof
subproof
(((((x = [] || y = []) || not (List.hd y <= List.hd x)) || not (not (is_sorted x && is_sorted (List.tl y)) || is_sorted (merge x (List.tl y)))) || not (is_sorted x)) || not (is_sorted y)) || is_sorted (merge x y)start[2.492s, "1.2"] (((((x = [] || y = []) || not (List.hd y <= List.hd x)) || not (not (is_sorted x && is_sorted (List.tl y)) || is_sorted (merge x (List.tl y)))) || not (is_sorted x)) || not (is_sorted y)) || is_sorted (merge x y)simplify
into ((((((((((x = [] || y = []) || not (List.hd y <= List.hd x)) || not (is_sorted (merge x (List.tl y)))) || not (is_sorted x)) || not (is_sorted (List.tl y))) || List.tl y = []) || not (List.hd y <= List.hd (List.tl y))) || merge x (List.tl y) = []) || List.hd y <= List.hd (merge x (List.tl y))) && ((((((x = [] || y = []) || not (List.hd y <= List.hd x)) || not (is_sorted x)) || not (List.tl y = [])) || merge x (List.tl y) = []) || List.hd y <= List.hd (merge x (List.tl y)))) && (((((((x = [] || y = []) || not (List.hd y <= List.hd x)) || not (is_sorted x)) || not (List.tl y = [])) || is_sorted (merge x (List.tl y))) || merge x (List.tl y) = []) || not (List.hd y <= List.hd (merge x (List.tl y))))expansions [merge, is_sorted, is_sorted, merge, is_sorted, is_sorted, is_sorted, merge]
rewrite_steps forward_chaining Subproof
Subproof
Subproof
subproof
((((not (List.hd y <= List.hd x) && not (y = [])) && not (x = []) || (List.hd y <= List.hd x && not (y = [])) && not (x = [])) || not (is_sorted x)) || not (is_sorted y)) || is_sorted (merge x y)start[2.493s, "1.3"] ((((not (List.hd y <= List.hd x) && not (y = [])) && not (x = []) || (List.hd y <= List.hd x && not (y = [])) && not (x = [])) || not (is_sorted x)) || not (is_sorted y)) || is_sorted (merge x y)simplify
into true
expansions merge
rewrite_steps forward_chaining
Loading..
Excellent! Now that we have that key lemma proved and available as a rewrite rule, let's return to our original goal:
In [24]:
theorem merge_sort_sorts x =
is_sorted (merge_sort x)
[@@induct functional merge_sort]
Out[24]:
val merge_sort_sorts : int list -> bool = <fun> Goal: is_sorted (merge_sort x). 1 nontautological subgoal. Subgoal 1: |--------------------------------------------------------------------------- is_sorted (merge_sort x) Must try induction. We shall induct according to a scheme derived from merge_sort. Induction scheme: (not (not (List.tl x = [] && x <> []) && not (x = [])) ==> φ x) && (not (x = []) && not (List.tl x = [] && x <> []) && φ (odds (List.tl x)) && φ (odds x) ==> φ x). 2 nontautological subgoals. Subgoal 1.2: |--------------------------------------------------------------------------- C0. not (List.tl x = [] && x <> []) && not (x = []) C1. is_sorted (merge_sort x) But simplification reduces this to true, using the definitions of is_sorted and merge_sort. Subgoal 1.1: H0. not (x = []) H1. not (List.tl x = [] && 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.1': H0. x <> [] H1. (List.tl x) <> [] H2. is_sorted (merge_sort (odds (List.tl x))) H3. is_sorted (merge_sort (odds x)) |--------------------------------------------------------------------------- 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.
Proved
proof
| ground_instances | 0 |
| definitions | 7 |
| inductions | 1 |
| search_time | 1.992s |
Expand
start[1.992s, "Goal"] is_sorted (merge_sort :var_0:)
subproof
is_sorted (merge_sort x)start[1.992s, "1"] is_sorted (merge_sort x)
induction on (functional merge_sort) :scheme (not (not (List.tl x = [] && x <> []) && not (x = [])) ==> φ x) && (not (x = []) && not (List.tl x = [] && x <> []) && φ (odds (List.tl x)) && φ (odds x) ==> φ x)Split ((not (List.tl x = [] && x <> []) && not (x = []) || is_sorted (merge_sort x)) && (not (((not (x = []) && not (List.tl x = [] && x <> [])) && is_sorted (merge_sort (odds (List.tl x)))) && is_sorted (merge_sort (odds x))) || is_sorted (merge_sort x)) :cases [not (List.tl x = [] && x <> []) && not (x = []) || is_sorted (merge_sort x); (((x = [] || List.tl x = [] && x <> []) || not (is_sorted (merge_sort (odds (List.tl x))))) || not (is_sorted (merge_sort (odds x)))) || is_sorted (merge_sort x)])subproof
(((x = [] || List.tl x = [] && x <> []) || not (is_sorted (merge_sort (odds (List.tl x))))) || not (is_sorted (merge_sort (odds x)))) || is_sorted (merge_sort x)start[1.806s, "1.1"] (((x = [] || List.tl x = [] && x <> []) || not (is_sorted (merge_sort (odds (List.tl x))))) || not (is_sorted (merge_sort (odds x)))) || is_sorted (merge_sort x)simplify
into (((x = [] || List.tl x = []) || not (is_sorted (merge_sort (odds (List.tl x))))) || not (is_sorted (merge_sort (odds x)))) || is_sorted (merge (merge_sort (odds x)) (merge_sort (odds (List.tl x))))
expansions merge_sort
rewrite_steps forward_chaining simplify
into true
expansions []
rewrite_steps merge_sorts
forward_chaining
subproof
not (List.tl x = [] && x <> []) && not (x = []) || is_sorted (merge_sort x)start[1.806s, "1.2"] not (List.tl x = [] && x <> []) && not (x = []) || is_sorted (merge_sort x)
simplify
into true
expansions [is_sorted, merge_sort, is_sorted, merge_sort, is_sorted, merge_sort]
rewrite_steps forward_chaining
Loading..
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 [25]:
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[25]:
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 (Ordinal.count y) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub ordinal | Ordinal.Int (Ordinal.count (List.tl y)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| path | [y <> [] && List.hd y = x && not (y = [])] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| proof | detailed proof
Expand
|
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 (Ordinal.count y) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub ordinal | Ordinal.Int (Ordinal.count (List.tl y)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| path | [not (y <> [] && List.hd y = x) && not (y = [])] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| proof | detailed proof
Expand
|
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 [26]:
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[26]:
val num_occur_merge : int -> int list -> int list -> bool = <fun> Goal: num_occurs a (merge x y) = num_occurs a x + num_occurs a y. 1 nontautological subgoal. Subgoal 1: |--------------------------------------------------------------------------- num_occurs a (merge x y) = num_occurs a x + num_occurs a y Must try induction. We shall induct according to a scheme derived from merge. Induction scheme: (not (List.hd x < List.hd y && not (y = []) && not (x = [])) && not (not (List.hd x < List.hd y) && not (y = []) && not (x = [])) ==> φ y x a) && (not (x = []) && not (y = []) && not (List.hd x < List.hd y) && φ (List.tl y) x a ==> φ y x a) && (not (x = []) && not (y = []) && List.hd x < List.hd y && φ y (List.tl x) a ==> φ y x a). 3 nontautological subgoals. Subgoal 1.3: H0. not ((not (List.hd y <= List.hd x) && not (y = [])) && not (x = [])) H1. not ((List.hd y <= List.hd x && not (y = [])) && not (x = [])) |--------------------------------------------------------------------------- num_occurs a (merge x y) = num_occurs a x + num_occurs a y This simplifies, using the definition of merge to the following 3 subgoals: Subgoal 1.3.3: H0. y = [] H1. x <> [] |--------------------------------------------------------------------------- C0. List.hd y <= List.hd x C1. 0 = num_occurs a y But simplification reduces this to true, using the definition of num_occurs. Subgoal 1.3.2: H0. y = [] H1. List.hd y <= List.hd x H2. x <> [] |--------------------------------------------------------------------------- 0 = num_occurs a y But simplification reduces this to true, using the definition of num_occurs. Subgoal 1.3.1: H0. x = [] |--------------------------------------------------------------------------- 0 = num_occurs a x But simplification reduces this to true, using the definition of num_occurs. Subgoal 1.2: H0. not (x = []) H1. not (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.1: H0. not (x = []) H1. not (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.
Proved
proof
| ground_instances | 0 |
| definitions | 10 |
| inductions | 1 |
| search_time | 0.297s |
Expand
start[0.297s, "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 ystart[0.297s, "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 && not (y = []) && not (x = [])) && not (not (List.hd x < List.hd y) && not (y = []) && not (x = [])) ==> φ y x a) && (not (x = []) && not (y = []) && not (List.hd x < List.hd y) && φ (List.tl y) x a ==> φ y x a) && (not (x = []) && not (y = []) && List.hd x < List.hd y && φ y (List.tl x) a ==> φ y x a)Split (((not (not ((not (List.hd y <= List.hd x) && not (y = [])) && not (x = [])) && not ((List.hd y <= List.hd x && not (y = [])) && not (x = []))) || num_occurs a (merge x y) = num_occurs a x + num_occurs a y) && (not (((not (x = []) && not (y = [])) && List.hd y <= List.hd x) && 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)) && (not (((not (x = []) && not (y = [])) && not (List.hd y <= List.hd x)) && 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) :cases [((not (List.hd y <= List.hd x) && not (y = [])) && not (x = []) || (List.hd y <= List.hd x && not (y = [])) && not (x = [])) || num_occurs a (merge x y) = num_occurs a x + num_occurs a y; (((x = [] || y = []) || not (List.hd y <= List.hd x)) || not (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; (((x = [] || y = []) || List.hd y <= List.hd x) || not (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])subproof
(((x = [] || y = []) || List.hd y <= List.hd x) || not (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 ystart[0.220s, "1.1"] (((x = [] || y = []) || List.hd y <= List.hd x) || not (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 ysimplify
into true
expansions [num_occurs, num_occurs, merge]
rewrite_steps forward_chaining
subproof
(((x = [] || y = []) || not (List.hd y <= List.hd x)) || not (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 ystart[0.220s, "1.2"] (((x = [] || y = []) || not (List.hd y <= List.hd x)) || not (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 ysimplify
into true
expansions [num_occurs, num_occurs, merge]
rewrite_steps forward_chaining
subproof
((not (List.hd y <= List.hd x) && not (y = [])) && not (x = []) || (List.hd y <= List.hd x && not (y = [])) && not (x = [])) || num_occurs a (merge x y) = num_occurs a x + num_occurs a ystart[0.220s, "1.3"] ((not (List.hd y <= List.hd x) && not (y = [])) && not (x = []) || (List.hd y <= List.hd x && not (y = [])) && not (x = [])) || num_occurs a (merge x y) = num_occurs a x + num_occurs a y
simplify
into ((((not (y = []) || List.hd y <= List.hd x) || 0 = num_occurs a y) || x = []) && (((not (y = []) || not (List.hd y <= List.hd x)) || 0 = num_occurs a y) || x = [])) && (0 = num_occurs a x || not (x = []))expansions merge
rewrite_steps forward_chaining Subproof
Subproof
Subproof
Loading..
In [27]:
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[27]:
val num_occurs_arith : int list -> int -> 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. Subgoal 1: H0. not (x = []) H1. not (List.tl x = []) |--------------------------------------------------------------------------- num_occurs a (odds (List.tl x)) = num_occurs a x + -1 * num_occurs a (odds x) This simplifies, using the definition of num_occurs to the following 2 subgoals: Subgoal 1.2: H0. x <> [] H1. (List.tl x) <> [] |--------------------------------------------------------------------------- C0. num_occurs a (odds (List.tl x)) = num_occurs a (List.tl x) + -1 * num_occurs a (odds x) C1. List.hd x = a We can eliminate destructors by the following substitution: x -> x1 :: x2 This produces the modified subgoal: Subgoal 1.2': H0. x2 <> [] |--------------------------------------------------------------------------- C0. num_occurs a (odds x2) = num_occurs a x2 + -1 * num_occurs a (odds (x1 :: x2)) C1. x1 = a Note: We must proceed by induction, but our current subgoal is less appropriate for induction than our original conjecture. Thus, we prefer to abandon our work until now and return our focus to the original conjecture which we shall attempt to prove by induction directly. We shall induct according to a scheme derived from num_occurs. Induction scheme: (not ((x <> [] && List.hd x = a) && not (x = [])) && not (not (x <> [] && List.hd x = a) && not (x = [])) ==> φ a x) && (not (x = []) && not (x <> [] && List.hd x = a) && φ a (List.tl x) ==> φ a x) && (not (x = []) && (x <> [] && List.hd x = a) && φ a (List.tl x) ==> φ a x). 3 nontautological subgoals. Subgoal 3: H0. not ((x <> [] && List.hd x = a) && not (x = [])) H1. not (not (x <> [] && List.hd x = a) && not (x = [])) H2. not (x = []) H3. not (List.tl 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 (x <> [] && List.hd x = a) H2. 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)) H3. not (x = []) H4. not (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 3 subgoals: Subgoal 2.3: H0. x <> [] H1. 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)) H2. (List.tl (List.tl x)) <> [] H3. (List.tl x) <> [] |--------------------------------------------------------------------------- C0. List.hd x = a C1. List.hd (List.tl x) = a C2. 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 2.2: H0. x <> [] H1. 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)) H2. (List.tl (List.tl x)) <> [] H3. List.hd (List.tl x) = a H4. (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))) But simplification reduces this to true, using the definition of num_occurs. Subgoal 2.1: H0. x <> [] H1. List.tl (List.tl x) = [] H2. (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))) But simplification reduces this to true, using the definitions of num_occurs and odds. Subgoal 1: H0. not (x = []) H1. x <> [] H2. List.hd x = a H3. 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)) H4. not (x = []) H5. not (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 3 subgoals: Subgoal 1.3: H0. x <> [] H1. 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)) H2. (List.tl (List.tl x)) <> [] H3. (List.tl x) <> [] |--------------------------------------------------------------------------- C0. List.hd (List.tl x) = List.hd x C1. 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 1.2: H0. x <> [] H1. 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)) H2. (List.tl (List.tl x)) <> [] H3. List.hd (List.tl x) = List.hd x H4. (List.tl 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 1.1: H0. x <> [] H1. List.tl (List.tl x) = [] H2. (List.tl 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 definitions of num_occurs and odds.
Proved
proof
| ground_instances | 0 |
| definitions | 27 |
| inductions | 1 |
| search_time | 1.759s |
Expand
start[1.759s, "Goal"] not (:var_0: = []) && not (List.tl :var_0: = []) ==> num_occurs :var_1: (odds (List.tl :var_0:)) = num_occurs :var_1: :var_0: - num_occurs :var_1: (odds :var_0:)subproof
(x = [] || List.tl x = []) || num_occurs a (odds (List.tl x)) = num_occurs a x + -1 * num_occurs a (odds x)start[1.759s, "1"] (x = [] || List.tl x = []) || num_occurs a (odds (List.tl x)) = num_occurs a x + -1 * num_occurs a (odds x)simplify
into (((x = [] || List.tl x = []) || num_occurs a (odds (List.tl x)) = num_occurs a (List.tl x) + -1 * num_occurs a (odds x)) || List.hd x = a) && (((x = [] || List.tl x = []) || num_occurs a (odds (List.tl x)) = (1 + num_occurs a (List.tl x)) + -1 * num_occurs a (odds x)) || not (List.hd x = a))expansions num_occurs
rewrite_steps forward_chaining subproof
((x = [] || List.tl x = []) || num_occurs a (odds (List.tl x)) = (1 + num_occurs a (List.tl x)) + -1 * num_occurs a (odds x)) || not (List.hd x = a)start[1.614s, "1.1"] ((x = [] || List.tl x = []) || num_occurs a (odds (List.tl x)) = (1 + num_occurs a (List.tl x)) + -1 * num_occurs a (odds x)) || not (List.hd x = a)subproof
((x = [] || List.tl x = []) || num_occurs a (odds (List.tl x)) = num_occurs a (List.tl x) + -1 * num_occurs a (odds x)) || List.hd x = astart[1.615s, "1.2"] ((x = [] || List.tl x = []) || num_occurs a (odds (List.tl x)) = num_occurs a (List.tl x) + -1 * num_occurs a (odds x)) || List.hd x = aElim_destructor (:cstor :: :replace x1 :: x2 :context [])
induction on (functional num_occurs) :scheme (not ((x <> [] && List.hd x = a) && not (x = [])) && not (not (x <> [] && List.hd x = a) && not (x = [])) ==> φ a x) && (not (x = []) && not (x <> [] && List.hd x = a) && φ a (List.tl x) ==> φ a x) && (not (x = []) && (x <> [] && List.hd x = a) && φ a (List.tl x) ==> φ a x)Split ((((not (not ((x <> [] && List.hd x = a) && not (x = [])) && not (not (x <> [] && List.hd x = a) && not (x = []))) || not (not (x = []) && not (List.tl x = []))) || num_occurs a (odds (List.tl x)) = num_occurs a x + -1 * num_occurs a (odds x)) && ((not ((not (x = []) && not (x <> [] && List.hd x = a)) && (not (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)))) || not (not (x = []) && not (List.tl x = []))) || num_occurs a (odds (List.tl x)) = num_occurs a x + -1 * num_occurs a (odds x))) && ((not (((not (x = []) && x <> []) && List.hd x = a) && (not (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)))) || not (not (x = []) && not (List.tl x = []))) || num_occurs a (odds (List.tl x)) = num_occurs a x + -1 * num_occurs a (odds x)) :cases [((((x <> [] && List.hd x = a) && not (x = []) || not (x <> [] && List.hd x = a) && not (x = [])) || x = []) || List.tl x = []) || num_occurs a (odds (List.tl x)) = num_occurs a x + -1 * num_occurs a (odds x); (((x = [] || x <> [] && List.hd x = a) || not (not (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)))) || List.tl x = []) || num_occurs a (odds (List.tl x)) = num_occurs a x + -1 * num_occurs a (odds x); ((((x = [] || not (x <> [])) || not (List.hd x = a)) || not (not (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)))) || List.tl x = []) || num_occurs a (odds (List.tl x)) = num_occurs a x + -1 * num_occurs a (odds x)])Subproof
Subproof
Subproof
Loading..
Finally, let's put the pieces together and prove our main remaining theorem.
And now, our second main theorem at last:
In [28]:
theorem merge_sort_elements a (x : int list) =
num_occurs a x = num_occurs a (merge_sort x)
[@@induct functional merge_sort]
Out[28]:
val merge_sort_elements : int -> int list -> bool = <fun> Goal: num_occurs a x = num_occurs a (merge_sort x). 1 nontautological subgoal. Subgoal 1: |--------------------------------------------------------------------------- num_occurs a x = num_occurs a (merge_sort x) Must try induction. We shall induct according to a scheme derived from merge_sort. Induction scheme: (not (not (List.tl x = [] && x <> []) && not (x = [])) ==> φ x a) && (not (x = []) && not (List.tl x = [] && x <> []) && φ (odds (List.tl x)) a && φ (odds x) a ==> φ x a). 2 nontautological subgoals. Subgoal 1.2: |--------------------------------------------------------------------------- C0. not (List.tl x = [] && x <> []) && not (x = []) C1. num_occurs a x = num_occurs a (merge_sort x) But simplification reduces this to true, using the definitions of merge_sort and num_occurs. Subgoal 1.1: H0. not (x = []) H1. not (List.tl x = [] && 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.1.2: H0. x <> [] H1. (List.tl x) <> [] H2. num_occurs a (List.tl x) + -1 * num_occurs a (odds x) = num_occurs a (merge_sort (odds (List.tl x))) H3. num_occurs a (odds x) = num_occurs a (merge_sort (odds x)) |--------------------------------------------------------------------------- C0. num_occurs a (List.tl x) = num_occurs a (merge (merge_sort (odds x)) (merge_sort (odds (List.tl x)))) C1. List.hd x = a But simplification reduces this to true, using the rewrite rule num_occur_merge. Subgoal 1.1.1: H0. x <> [] H1. (List.tl x) <> [] H2. num_occurs a (List.tl x) + -1 * num_occurs a (odds x) = -1 + num_occurs a (merge_sort (odds (List.tl x))) H3. num_occurs a (odds x) = num_occurs a (merge_sort (odds x)) H4. List.hd x = a |--------------------------------------------------------------------------- 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.
Proved
proof
| ground_instances | 0 |
| definitions | 15 |
| inductions | 1 |
| search_time | 7.103s |
Expand
start[7.103s, "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[7.103s, "1"] num_occurs a x = num_occurs a (merge_sort x)
induction on (functional merge_sort) :scheme (not (not (List.tl x = [] && x <> []) && not (x = [])) ==> φ x a) && (not (x = []) && not (List.tl x = [] && x <> []) && φ (odds (List.tl x)) a && φ (odds x) a ==> φ x a)Split ((not (List.tl x = [] && x <> []) && not (x = []) || num_occurs a x = num_occurs a (merge_sort x)) && (not (((not (x = []) && not (List.tl x = [] && x <> [])) && num_occurs a (odds (List.tl x)) = num_occurs a (merge_sort (odds (List.tl x)))) && num_occurs a (odds x) = num_occurs a (merge_sort (odds x))) || num_occurs a x = num_occurs a (merge_sort x)) :cases [not (List.tl x = [] && x <> []) && not (x = []) || num_occurs a x = num_occurs a (merge_sort x); (((x = [] || List.tl x = [] && x <> []) || not (num_occurs a (odds (List.tl x)) = num_occurs a (merge_sort (odds (List.tl x))))) || not (num_occurs a (odds x) = num_occurs a (merge_sort (odds x)))) || num_occurs a x = num_occurs a (merge_sort x)])subproof
(((x = [] || List.tl x = [] && x <> []) || not (num_occurs a (odds (List.tl x)) = num_occurs a (merge_sort (odds (List.tl x))))) || not (num_occurs a (odds x) = num_occurs a (merge_sort (odds x)))) || num_occurs a x = num_occurs a (merge_sort x)start[6.987s, "1.1"] (((x = [] || List.tl x = [] && x <> []) || not (num_occurs a (odds (List.tl x)) = num_occurs a (merge_sort (odds (List.tl x))))) || not (num_occurs a (odds x) = num_occurs a (merge_sort (odds x)))) || num_occurs a x = num_occurs a (merge_sort x)simplify
into (((((x = [] || List.tl x = []) || not (num_occurs a (List.tl x) + -1 * num_occurs a (odds x) = num_occurs a (merge_sort (odds (List.tl x))))) || not (num_occurs a (odds x) = num_occurs a (merge_sort (odds x)))) || num_occurs a (List.tl x) = num_occurs a (merge (merge_sort (odds x)) (merge_sort (odds (List.tl x))))) || List.hd x = a) && (((((x = [] || List.tl x = []) || not (num_occurs a (List.tl x) + -1 * num_occurs a (odds x) = -1 + num_occurs a (merge_sort (odds (List.tl x))))) || not (num_occurs a (odds x) = num_occurs a (merge_sort (odds x)))) || num_occurs a (List.tl x) = -1 + num_occurs a (merge (merge_sort (odds x)) (merge_sort (odds (List.tl x))))) || not (List.hd x = a))expansions [num_occurs, num_occurs, merge_sort, num_occurs]
rewrite_steps num_occurs_arith
num_occurs_arith
forward_chaining Subproof
Subproof
subproof
not (List.tl x = [] && x <> []) && not (x = []) || num_occurs a x = num_occurs a (merge_sort x)start[6.987s, "1.2"] not (List.tl x = [] && x <> []) && not (x = []) || num_occurs a x = num_occurs a (merge_sort x)
simplify
into true
expansions [num_occurs, merge_sort, num_occurs, num_occurs, merge_sort, num_occurs, num_occurs, num_occurs, num_occurs, merge_sort, num_occurs]
rewrite_steps forward_chaining
Loading..
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)!