new programs: mergesort_list (shows a bug related to implicit arguments in Coq output)

parent 12c14e88
......@@ -23,6 +23,6 @@ let rec insertion_sort l variant { length l } =
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/insertion_sort_list"
compile-command: "unset LANG; make -C ../.. examples/programs/insertion_sort_list.gui"
End:
*)
{
use import list.Length
use import list.Sorted
use import list.Append
use import list.Permut
lemma Permut_append:
forall l1 l2 k1 k2 : list 'a.
permut l1 k1 -> permut l2 k2 -> permut (append l1 l2) (append k1 k2)
}
let split l0 =
{ length l0 >= 2 }
let rec split_aux (l1 : list 'a) l2 l variant { length l } =
{ length l2 = length l1 or length l2 = length l1 + 1 }
match l with
| Nil -> (l1, l2)
| Cons x r -> split_aux l2 (Cons x l1) r
end
{ let r1, r2 = result in
(length r2 = length r1 or length r2 = length r1 + 1) and
permut (append r1 r2) (append l1 (append l2 l)) }
in
split_aux Nil Nil l0
{ let (l1, l2) = result in
1 <= length l1 and 1 <= length l2 and permut l0 (append l1 l2) }
let rec merge l1 l2 variant { length l1 + length l2 } =
{ sorted l1 and sorted l2 }
match l1, l2 with
| Nil, _ -> l2
| _, Nil -> l1
| Cons x1 r1, Cons x2 r2 ->
if x1 <= x2 then Cons x1 (merge r1 l2) else Cons x2 (merge l1 r2)
end
{ sorted result and permut result (append l1 l2) }
let rec mergesort l variant { length l } =
{ }
match l with
| Nil | Cons _ Nil -> l
| _ -> let l1, l2 = split l in merge (mergesort l1) (mergesort l2)
end
{ sorted result and permut l result }
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/mergesort_list.gui"
End:
*)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment