library: more lemmas on lists

completed proof of mergesort_list (tail rec version of merge)

examples/mergesort_list.mlw

 
-(* Sorting a list of integers using mergesort *)
+(** Sorting a list of integers using mergesort
+
+    Author: Jean-Christophe Filliâtre (CNRS)
+*)
 
 module Elt
 
@@ -15,13 +18,14 @@ module Elt
 
 end
 
-module Merge
+module Merge (* : MergeSpec *)
 
-  use export Elt
+  clone export Elt
 
   let rec merge (l1 l2: list elt) : list elt
     requires { sorted l1 /\ sorted l2 }
-    ensures  { sorted result /\ permut result (l1 ++ l2) }
+    ensures  { sorted result }
+    ensures  { permut result (l1 ++ l2) }
     variant  { length l1 + length l2 }
   = match l1, l2 with
     | Nil, _ -> l2
@@ -32,19 +36,25 @@ module Merge
 
 end
 
-(* TODO: proof to be completed
-module EfficientMerge
+(** tail recursive implementation *)
 
-  use export Elt
+module EfficientMerge (* : MergeSpec *)
+
+  clone export Elt
   use import list.Mem
   use import list.Reverse
   use import list.RevAppend
 
+  lemma sorted_reverse_cons:
+    forall acc x1. sorted (reverse acc) ->
+    (forall x. mem x acc -> le x x1) -> sorted (reverse (Cons x1 acc))
+
   let rec merge_aux (acc l1 l2: list elt) : list elt
     requires { sorted (reverse acc) /\ sorted l1 /\ sorted l2 }
     requires { forall x y: elt. mem x acc -> mem y l1 -> le x y }
     requires { forall x y: elt. mem x acc -> mem y l2 -> le x y }
-    ensures  { sorted result /\ permut result (acc ++ l1 ++ l2) }
+    ensures  { sorted result }
+    ensures  { permut result (acc ++ l1 ++ l2) }
     variant  { length l1 + length l2 }
   = match l1, l2 with
     | Nil, _ -> rev_append acc l2
@@ -61,11 +71,10 @@ module EfficientMerge
     merge_aux Nil l1 l2
 
 end
-*)
 
 module Mergesort
 
-  use import Merge
+  clone import Merge
 
   let split (l0: list 'a) : (list 'a, list 'a)
     requires { length l0 >= 2 }

lib/coq/list/NumOcc.v

@@ -7,6 +7,7 @@ Require list.List.
 Require list.Length.
 Require list.Mem.
 Require list.Append.
+Require list.Reverse.
 
 (* Why3 goal *)
 Definition num_occ: forall {a:Type} {a_WT:WhyType a}, a -> (list a) -> Z.
@@ -83,3 +84,16 @@ rewrite Zplus_assoc.
 now case why_decidable_eq.
 Qed.
 
+(* Why3 goal *)
+Lemma reverse_num_occ : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
+  (l:(list a)), ((num_occ x l) = (num_occ x (Lists.List.rev l))).
+intros a a_WT x l.
+induction l; simpl.
+auto.
+rewrite Append_Num_Occ.
+rewrite <- IHl.
+ring_simplify.
+simpl (num_occ x (a0 :: nil))%list.
+ring.
+Qed.
+

lib/coq/list/Permut.v

@@ -7,6 +7,7 @@ Require list.List.
 Require list.Length.
 Require list.Mem.
 Require list.Append.
+Require list.Reverse.
 Require list.NumOcc.
 
 (* Why3 assumption *)

lib/coq/list/RevAppend.v

@@ -7,17 +7,18 @@ Require list.List.
 Require list.Length.
 Require list.Mem.
 Require list.Append.
+Require list.Reverse.
 
 (* Why3 goal *)
-Lemma rev_append_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(list a))
+Lemma rev_append_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s:(list a))
   (t:(list a)),
   ((Lists.List.rev_append s t) = match s with
   | (Init.Datatypes.cons x r) =>
       (Lists.List.rev_append r (Init.Datatypes.cons x t))
   | Init.Datatypes.nil => t
   end).
-Proof.
-now intros a a_WT [|sh st] t.
+intros a a_WT s t.
+destruct s; simpl; auto.
 Qed.
 
 (* Why3 goal *)
@@ -61,3 +62,15 @@ change (Length.length (sh :: st)) with (1 + Length.length st)%Z.
 ring.
 Qed.
 
+(* Why3 goal *)
+Lemma rev_append_def : forall {a:Type} {a_WT:WhyType a}, forall (r:(list a))
+  (s:(list a)),
+  ((Lists.List.rev_append r s) = (Init.Datatypes.app (Lists.List.rev r) s)).
+Proof.
+induction r; simpl.
+now auto.
+intro s; rewrite IHr.
+rewrite <- Append.Append_assoc.
+simpl. reflexivity.
+Qed.
+

lib/coq/list/Reverse.v

@@ -29,6 +29,15 @@ simpl.
 now rewrite <- List.app_assoc.
 Qed.
 
+(* Why3 goal *)
+Lemma reverse_cons : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a))
+  (x:a),
+  ((Lists.List.rev (Init.Datatypes.cons x l)) = (Init.Datatypes.app (Lists.List.rev l) (Init.Datatypes.cons x Init.Datatypes.nil))).
+intros a a_WT l x.
+simpl.
+auto.
+Qed.
+
 (* Why3 goal *)
 Lemma reverse_reverse : forall {a:Type} {a_WT:WhyType a},
   forall (l:(list a)), ((Lists.List.rev (Lists.List.rev l)) = l).
@@ -37,6 +46,21 @@ intros a a_WT l.
 apply List.rev_involutive.
 Qed.
 
+(* Why3 goal *)
+Lemma reverse_mem : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a))
+  (x:a), (list.Mem.mem x l) <-> (list.Mem.mem x (Lists.List.rev l)).
+intros a a_WT l x.
+induction l; simpl; intuition.
+rewrite Append.mem_append.
+right; simpl; now intuition.
+rewrite Append.mem_append.
+now auto.
+assert (Mem.mem x (List.rev l) \/ Mem.mem x (a0 :: nil))%list.
+rewrite <- Append.mem_append; assumption.
+intuition; simpl in *.
+intuition.
+Qed.
+
 (* Why3 goal *)
 Lemma Reverse_length : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
   ((list.Length.length (Lists.List.rev l)) = (list.Length.length l)).

theories/list.why

@@ -219,9 +219,18 @@ theory Reverse
     forall l1 l2: list 'a, x: 'a.
     (reverse (Cons x l1)) ++ l2 = (reverse l1) ++ (Cons x l2)
 
+  lemma reverse_cons:
+    forall l: list 'a, x: 'a.
+    reverse (Cons x l) = reverse l ++ Cons x Nil
+
   lemma reverse_reverse:
     forall l: list 'a. reverse (reverse l) = l
 
+  use import Mem
+
+  lemma reverse_mem:
+    forall l: list 'a, x: 'a. mem x l <-> mem x (reverse l)
+
   use import Length
 
   lemma Reverse_length:
@@ -258,6 +267,11 @@ theory RevAppend
     forall s t: list 'a.
       length (rev_append s t) = length s + length t
 
+  use import Reverse
+
+  lemma rev_append_def:
+    forall r s: list 'a. rev_append r s = reverse r ++ s
+
 end
 
 (** {2 Zip} *)
@@ -298,6 +312,14 @@ theory Sorted
     forall x: t, l: list t.
     (forall y: t. mem y l -> le x y) /\ sorted l <-> sorted (Cons x l)
 
+  use import Append
+
+  lemma sorted_append:
+    forall l1 l2: list t.
+    sorted l1 -> sorted l2 ->
+    (forall x y: t. mem x l1 -> mem y l2 -> le x y) ->
+    sorted (l1 ++ l2)
+
 end
 
 (** {2 Sorted lists of integers} *)
@@ -338,15 +360,6 @@ theory RevSorted
       Decr.sorted (rev_append s t) <->
         Incr.sorted s /\ Decr.sorted t /\ compat t s
 
-  (*
-  use import Reverse
-
-  lemma rev_sorted_incr:
-    forall s: list t. Incr.sorted (reverse s) <-> Decr.sorted s
-
-  lemma rev_sorted_decr:
-    forall s: list t. Decr.sorted (reverse s) <-> Incr.sorted s
-  *)
 end
 
 (** {2 Number of occurrences in a list} *)
@@ -374,6 +387,12 @@ theory NumOcc
     forall x: 'a, l1 l2: list 'a.
     num_occ x (l1 ++ l2) = num_occ x l1 + num_occ x l2
 
+  use import Reverse
+
+  lemma reverse_num_occ :
+    forall x: 'a, l: list 'a.
+    num_occ x l = num_occ x (reverse l)
+
 end
 
 (** {2 Permutation of lists} *)