Imported Upstream version 8.0pl1upstream/8.0pl1

3 files changed, 470 insertions, 0 deletions

diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
new file mode 100644
index 00000000..41594749
--- /dev/null
+++ b/theories/Sorting/Heap.v
@@ -0,0 +1,227 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: Heap.v,v 1.3.2.1 2004/07/16 19:31:19 herbelin Exp $ i*)
+
+(** A development of Treesort on Heap trees *)
+
+(* G. Huet 1-9-95 uses Multiset *)
+
+Require Import List.
+Require Import Multiset.
+Require Import Permutation.
+Require Import Relations.
+Require Import Sorting.
+
+
+Section defs.
+
+Variable A : Set.
+Variable leA : relation A.
+Variable eqA : relation A.
+
+Let gtA (x y:A) := ~ leA x y.
+
+Hypothesis leA_dec : forall x y:A, {leA x y} + {leA y x}.
+Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
+Hypothesis leA_refl : forall x y:A, eqA x y -> leA x y.
+Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z.
+Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y.
+
+Hint Resolve leA_refl.
+Hint Immediate eqA_dec leA_dec leA_antisym.
+
+Let emptyBag := EmptyBag A.
+Let singletonBag := SingletonBag _ eqA_dec.
+
+Inductive Tree : Set :=
+  | Tree_Leaf : Tree
+  | Tree_Node : A -> Tree -> Tree -> Tree.
+
+(** [a] is lower than a Tree [T] if [T] is a Leaf
+    or [T] is a Node holding [b>a] *)
+
+Definition leA_Tree (a:A) (t:Tree) :=
+  match t with
+  | Tree_Leaf => True
+  | Tree_Node b T1 T2 => leA a b
+  end.
+
+Lemma leA_Tree_Leaf : forall a:A, leA_Tree a Tree_Leaf.
+Proof.
+simpl in |- *; auto with datatypes.
+Qed.
+
+Lemma leA_Tree_Node :
+ forall (a b:A) (G D:Tree), leA a b -> leA_Tree a (Tree_Node b G D).
+Proof.
+simpl in |- *; auto with datatypes.
+Qed.
+
+Hint Resolve leA_Tree_Leaf leA_Tree_Node.
+
+
+(** The heap property *)
+
+Inductive is_heap : Tree -> Prop :=
+  | nil_is_heap : is_heap Tree_Leaf
+  | node_is_heap :
+      forall (a:A) (T1 T2:Tree),
+        leA_Tree a T1 ->
+        leA_Tree a T2 ->
+        is_heap T1 -> is_heap T2 -> is_heap (Tree_Node a T1 T2).
+
+Hint Constructors is_heap.
+
+Lemma invert_heap :
+ forall (a:A) (T1 T2:Tree),
+   is_heap (Tree_Node a T1 T2) ->
+   leA_Tree a T1 /\ leA_Tree a T2 /\ is_heap T1 /\ is_heap T2.
+Proof.
+intros; inversion H; auto with datatypes.
+Qed.
+
+(* This lemma ought to be generated automatically by the Inversion tools *)
+Lemma is_heap_rec :
+ forall P:Tree -> Set,
+   P Tree_Leaf ->
+   (forall (a:A) (T1 T2:Tree),
+      leA_Tree a T1 ->
+      leA_Tree a T2 ->
+      is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
+   forall T:Tree, is_heap T -> P T.
+Proof.
+simple induction T; auto with datatypes.
+intros a G PG D PD PN. 
+elim (invert_heap a G D); auto with datatypes.
+intros H1 H2; elim H2; intros H3 H4; elim H4; intros.
+apply H0; auto with datatypes.
+Qed.
+
+Lemma low_trans :
+ forall (T:Tree) (a b:A), leA a b -> leA_Tree b T -> leA_Tree a T.
+Proof.
+simple induction T; auto with datatypes.
+intros; simpl in |- *; apply leA_trans with b; auto with datatypes.
+Qed.
+
+(** contents of a tree as a multiset *)
+
+(** Nota Bene : In what follows the definition of SingletonBag
+    in not used. Actually, we could just take as postulate:
+    [Parameter SingletonBag : A->multiset].  *)
+
+Fixpoint contents (t:Tree) : multiset A :=
+  match t with
+  | Tree_Leaf => emptyBag
+  | Tree_Node a t1 t2 =>
+      munion (contents t1) (munion (contents t2) (singletonBag a))
+  end.
+
+
+(** equivalence of two trees is equality of corresponding multisets *)
+
+Definition equiv_Tree (t1 t2:Tree) := meq (contents t1) (contents t2).
+
+
+(** specification of heap insertion *)
+
+Inductive insert_spec (a:A) (T:Tree) : Set :=
+    insert_exist :
+      forall T1:Tree,
+        is_heap T1 ->
+        meq (contents T1) (munion (contents T) (singletonBag a)) ->
+        (forall b:A, leA b a -> leA_Tree b T -> leA_Tree b T1) ->
+        insert_spec a T.
+
+
+Lemma insert : forall T:Tree, is_heap T -> forall a:A, insert_spec a T.
+Proof.
+simple induction 1; intros.
+apply insert_exist with (Tree_Node a Tree_Leaf Tree_Leaf);
+ auto with datatypes.
+simpl in |- *; unfold meq, munion in |- *; auto with datatypes.
+elim (leA_dec a a0); intros.
+elim (H3 a0); intros.
+apply insert_exist with (Tree_Node a T2 T0); auto with datatypes.
+simpl in |- *; apply treesort_twist1; trivial with datatypes. 
+elim (H3 a); intros T3 HeapT3 ConT3 LeA.
+apply insert_exist with (Tree_Node a0 T2 T3); auto with datatypes.
+apply node_is_heap; auto with datatypes.
+apply low_trans with a; auto with datatypes.
+apply LeA; auto with datatypes.
+apply low_trans with a; auto with datatypes.
+simpl in |- *; apply treesort_twist2; trivial with datatypes. 
+Qed.
+
+(** building a heap from a list *)
+
+Inductive build_heap (l:list A) : Set :=
+    heap_exist :
+      forall T:Tree,
+        is_heap T ->
+        meq (list_contents _ eqA_dec l) (contents T) -> build_heap l.
+
+Lemma list_to_heap : forall l:list A, build_heap l.
+Proof.
+simple induction l.
+apply (heap_exist nil Tree_Leaf); auto with datatypes.
+simpl in |- *; unfold meq in |- *; auto with datatypes.
+simple induction 1.
+intros T i m; elim (insert T i a).
+intros; apply heap_exist with T1; simpl in |- *; auto with datatypes.
+apply meq_trans with (munion (contents T) (singletonBag a)).
+apply meq_trans with (munion (singletonBag a) (contents T)).
+apply meq_right; trivial with datatypes.
+apply munion_comm.
+apply meq_sym; trivial with datatypes.
+Qed.
+
+
+(** building the sorted list *)
+
+Inductive flat_spec (T:Tree) : Set :=
+    flat_exist :
+      forall l:list A,
+        sort leA l ->
+        (forall a:A, leA_Tree a T -> lelistA leA a l) ->
+        meq (contents T) (list_contents _ eqA_dec l) -> flat_spec T.
+
+Lemma heap_to_list : forall T:Tree, is_heap T -> flat_spec T.
+Proof.
+  intros T h; elim h; intros.
+  apply flat_exist with (nil (A:=A)); auto with datatypes.
+  elim H2; intros l1 s1 i1 m1; elim H4; intros l2 s2 i2 m2.
+  elim (merge _ leA_dec eqA_dec s1 s2); intros.
+  apply flat_exist with (a :: l); simpl in |- *; auto with datatypes.
+  apply meq_trans with
+   (munion (list_contents _ eqA_dec l1)
+      (munion (list_contents _ eqA_dec l2) (singletonBag a))).
+  apply meq_congr; auto with datatypes.
+  apply meq_trans with
+   (munion (singletonBag a)
+      (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2))).
+  apply munion_rotate.
+  apply meq_right; apply meq_sym; trivial with datatypes.
+Qed.
+
+(** specification of treesort *)
+
+Theorem treesort :
+ forall l:list A, {m : list A | sort leA m &  permutation _ eqA_dec l m}.
+Proof.
+  intro l; unfold permutation in |- *.
+  elim (list_to_heap l).
+  intros.
+  elim (heap_to_list T); auto with datatypes.
+  intros.
+  exists l0; auto with datatypes.
+  apply meq_trans with (contents T); trivial with datatypes.
+Qed.
+
+End defs.
\ No newline at end of file
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
new file mode 100644
index 00000000..43a0f0bc
--- /dev/null
+++ b/theories/Sorting/Permutation.v
@@ -0,0 +1,120 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: Permutation.v,v 1.4.2.1 2004/07/16 19:31:19 herbelin Exp $ i*)
+
+Require Import Relations.
+Require Import List.
+Require Import Multiset.
+
+Set Implicit Arguments.
+
+Section defs.
+
+Variable A : Set.
+Variable leA : relation A.
+Variable eqA : relation A.
+
+Let gtA (x y:A) := ~ leA x y.
+
+Hypothesis leA_dec : forall x y:A, {leA x y} + {~ leA x y}.
+Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
+Hypothesis leA_refl : forall x y:A, eqA x y -> leA x y.
+Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z.
+Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y.
+
+Hint Resolve leA_refl: default.
+Hint Immediate eqA_dec leA_dec leA_antisym: default.
+
+Let emptyBag := EmptyBag A.
+Let singletonBag := SingletonBag _ eqA_dec.
+
+(** contents of a list *)
+
+Fixpoint list_contents (l:list A) : multiset A :=
+  match l with
+  | nil => emptyBag
+  | a :: l => munion (singletonBag a) (list_contents l)
+  end.
+
+Lemma list_contents_app :
+ forall l m:list A,
+   meq (list_contents (l ++ m)) (munion (list_contents l) (list_contents m)).
+Proof.
+simple induction l; simpl in |- *; auto with datatypes.
+intros.
+apply meq_trans with
+ (munion (singletonBag a) (munion (list_contents l0) (list_contents m)));
+ auto with datatypes.
+Qed.
+Hint Resolve list_contents_app.
+
+Definition permutation (l m:list A) :=
+  meq (list_contents l) (list_contents m).
+
+Lemma permut_refl : forall l:list A, permutation l l.
+Proof.
+unfold permutation in |- *; auto with datatypes.
+Qed.
+Hint Resolve permut_refl.
+
+Lemma permut_tran :
+ forall l m n:list A, permutation l m -> permutation m n -> permutation l n.
+Proof.
+unfold permutation in |- *; intros.
+apply meq_trans with (list_contents m); auto with datatypes.
+Qed.
+
+Lemma permut_right :
+ forall l m:list A,
+   permutation l m -> forall a:A, permutation (a :: l) (a :: m).
+Proof.
+unfold permutation in |- *; simpl in |- *; auto with datatypes.
+Qed.
+Hint Resolve permut_right.
+
+Lemma permut_app :
+ forall l l' m m':list A,
+   permutation l l' -> permutation m m' -> permutation (l ++ m) (l' ++ m').
+Proof.
+unfold permutation in |- *; intros.
+apply meq_trans with (munion (list_contents l) (list_contents m));
+ auto with datatypes.
+apply meq_trans with (munion (list_contents l') (list_contents m'));
+ auto with datatypes.
+apply meq_trans with (munion (list_contents l') (list_contents m));
+ auto with datatypes.
+Qed.
+Hint Resolve permut_app.
+
+Lemma permut_cons :
+ forall l m:list A,
+   permutation l m -> forall a:A, permutation (a :: l) (a :: m).
+Proof.
+intros l m H a.
+change (permutation ((a :: nil) ++ l) ((a :: nil) ++ m)) in |- *.
+apply permut_app; auto with datatypes.
+Qed.
+Hint Resolve permut_cons.
+
+Lemma permut_middle :
+ forall (l m:list A) (a:A), permutation (a :: l ++ m) (l ++ a :: m).
+Proof.
+unfold permutation in |- *.
+simple induction l; simpl in |- *; auto with datatypes.
+intros.
+apply meq_trans with
+ (munion (singletonBag a)
+    (munion (singletonBag a0) (list_contents (l0 ++ m))));
+ auto with datatypes.
+apply munion_perm_left; auto with datatypes.
+Qed.
+Hint Resolve permut_middle.
+
+End defs.
+Unset Implicit Arguments.
diff --git a/theories/Sorting/Sorting.v b/theories/Sorting/Sorting.v
new file mode 100644
index 00000000..aa829fea
--- /dev/null
+++ b/theories/Sorting/Sorting.v
@@ -0,0 +1,123 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: Sorting.v,v 1.4.2.1 2004/07/16 19:31:19 herbelin Exp $ i*)
+
+Require Import List.
+Require Import Multiset.
+Require Import Permutation.
+Require Import Relations.
+
+Set Implicit Arguments.
+
+Section defs.
+
+Variable A : Set.
+Variable leA : relation A.
+Variable eqA : relation A.
+
+Let gtA (x y:A) := ~ leA x y.
+
+Hypothesis leA_dec : forall x y:A, {leA x y} + {leA y x}.
+Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
+Hypothesis leA_refl : forall x y:A, eqA x y -> leA x y.
+Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z.
+Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y.
+
+Hint Resolve leA_refl.
+Hint Immediate eqA_dec leA_dec leA_antisym.
+
+Let emptyBag := EmptyBag A.
+Let singletonBag := SingletonBag _ eqA_dec.
+
+(** [lelistA] *)
+
+Inductive lelistA (a:A) : list A -> Prop :=
+  | nil_leA : lelistA a nil
+  | cons_leA : forall (b:A) (l:list A), leA a b -> lelistA a (b :: l).
+Hint Constructors lelistA.
+
+Lemma lelistA_inv : forall (a b:A) (l:list A), lelistA a (b :: l) -> leA a b.
+Proof.
+  intros; inversion H; trivial with datatypes.
+Qed.
+
+(** definition for a list to be sorted *)
+
+Inductive sort : list A -> Prop :=
+  | nil_sort : sort nil
+  | cons_sort :
+      forall (a:A) (l:list A), sort l -> lelistA a l -> sort (a :: l).
+Hint Constructors sort.
+
+Lemma sort_inv :
+ forall (a:A) (l:list A), sort (a :: l) -> sort l /\ lelistA a l.
+Proof.
+intros; inversion H; auto with datatypes.
+Qed.
+
+Lemma sort_rec :
+ forall P:list A -> Set,
+   P nil ->
+   (forall (a:A) (l:list A), sort l -> P l -> lelistA a l -> P (a :: l)) ->
+   forall y:list A, sort y -> P y.
+Proof.
+simple induction y; auto with datatypes.
+intros; elim (sort_inv (a:=a) (l:=l)); auto with datatypes.
+Qed.
+
+(** merging two sorted lists *)
+
+Inductive merge_lem (l1 l2:list A) : Set :=
+    merge_exist :
+      forall l:list A,
+        sort l ->
+        meq (list_contents _ eqA_dec l)
+          (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2)) ->
+        (forall a:A, lelistA a l1 -> lelistA a l2 -> lelistA a l) ->
+        merge_lem l1 l2.
+
+Lemma merge :
+ forall l1:list A, sort l1 -> forall l2:list A, sort l2 -> merge_lem l1 l2.
+Proof.
+  simple induction 1; intros.
+  apply merge_exist with l2; auto with datatypes.
+  elim H3; intros.
+  apply merge_exist with (a :: l); simpl in |- *; auto with datatypes.
+  elim (leA_dec a a0); intros.
+
+(* 1 (leA a a0) *)
+  cut (merge_lem l (a0 :: l0)); auto with datatypes.
+  intros [l3 l3sorted l3contents Hrec].
+  apply merge_exist with (a :: l3); simpl in |- *; auto with datatypes.
+  apply meq_trans with
+   (munion (singletonBag a)
+      (munion (list_contents _ eqA_dec l)
+         (list_contents _ eqA_dec (a0 :: l0)))).
+  apply meq_right; trivial with datatypes.
+  apply meq_sym; apply munion_ass.
+  intros; apply cons_leA.
+  apply lelistA_inv with l; trivial with datatypes.
+
+(* 2 (leA a0 a) *)
+  elim H5; simpl in |- *; intros.
+  apply merge_exist with (a0 :: l3); simpl in |- *; auto with datatypes.
+  apply meq_trans with
+   (munion (singletonBag a0)
+      (munion (munion (singletonBag a) (list_contents _ eqA_dec l))
+         (list_contents _ eqA_dec l0))).
+  apply meq_right; trivial with datatypes.
+  apply munion_perm_left.
+  intros; apply cons_leA; apply lelistA_inv with l0; trivial with datatypes.
+Qed.
+
+End defs.
+
+Unset Implicit Arguments.
+Hint Constructors sort: datatypes v62.
+Hint Constructors lelistA: datatypes v62.
\ No newline at end of file