Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

3 files changed, 0 insertions, 451 deletions

diff --git a/theories7/Sorting/Heap.v b/theories7/Sorting/Heap.v
deleted file mode 100644
index 63e7f324..00000000
--- a/theories7/Sorting/Heap.v
+++ /dev/null
@@ -1,223 +0,0 @@
-(************************************************************************)
-(*  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.1.2.1 2004/07/16 19:31:41 herbelin Exp $ i*)
-
-(** A development of Treesort on Heap trees *)
-
-(* G. Huet 1-9-95 uses Multiset *)
-
-Require PolyList.
-Require Multiset.
-Require Permutation.
-Require Relations.
-Require Sorting.
-
-
-Section defs.
-
-Variable A : Set.
-Variable leA : (relation A).
-Variable eqA : (relation A).
-
-Local gtA := [x,y:A]~(leA x y).
-
-Hypothesis leA_dec : (x,y:A){(leA x y)}+{(leA y x)}.
-Hypothesis eqA_dec : (x,y:A){(eqA x y)}+{~(eqA x y)}.
-Hypothesis leA_refl : (x,y:A) (eqA x y) -> (leA x y).
-Hypothesis leA_trans : (x,y,z:A) (leA x y) -> (leA y z) -> (leA x z).
-Hypothesis leA_antisym : (x,y:A)(leA x y) -> (leA y x) -> (eqA x y).
-
-Hints Resolve leA_refl.
-Hints Immediate eqA_dec leA_dec leA_antisym.
-
-Local emptyBag := (EmptyBag A).
-Local 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]
- Cases t of 
-   Tree_Leaf           => True
- | (Tree_Node b T1 T2) => (leA a b)
- end.
-
-Lemma leA_Tree_Leaf : (a:A)(leA_Tree a Tree_Leaf).
-Proof.
-Simpl; Auto with datatypes.
-Qed.
-
-Lemma leA_Tree_Node : (a,b:A)(G,D:Tree)(leA a b) ->
-                        (leA_Tree a (Tree_Node b G D)).
-Proof.
-Simpl; Auto with datatypes.
-Qed.
-
-Hints 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 : (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 constr_is_heap := Constructors is_heap.
-
-Lemma invert_heap : (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 : (P:Tree->Set)
-        (P Tree_Leaf)->
-         ((a:A)
-           (T1:Tree)
-            (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)))
-         -> (T:Tree)(is_heap T) -> (P T).
-Proof.
-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 : 
-  (T:Tree)(a,b:A)(leA a b) -> (leA_Tree b T) -> (leA_Tree a T).
-Proof.
-Induction T; Auto with datatypes.
-Intros; Simpl; 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) :=
- Cases t of
-   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 : (T1:Tree)(is_heap T1) ->
-                  (meq (contents T1) (munion (contents T) (singletonBag a))) ->
-                  ((b:A)(leA b a)->(leA_Tree b T)->(leA_Tree b T1)) ->
-                  (insert_spec a T).
-
-
-Lemma insert : (T:Tree)(is_heap T) -> (a:A)(insert_spec a T).
-Proof.
-Induction 1; Intros.
-Apply insert_exist with (Tree_Node a Tree_Leaf Tree_Leaf); Auto with datatypes.
-Simpl; Unfold meq munion; 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; 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; Apply treesort_twist2; Trivial with datatypes. 
-Qed.
-
-(** building a heap from a list *)
-
-Inductive build_heap [l:(list A)] : Set :=
-   heap_exist : (T:Tree)(is_heap T) ->
-                (meq (list_contents eqA_dec l)(contents T)) ->
-                (build_heap l).
-
-Lemma list_to_heap : (l:(list A))(build_heap l).
-Proof.
-Induction l.
-Apply (heap_exist (nil  A) Tree_Leaf); Auto with datatypes.
-Simpl; Unfold meq; Auto with datatypes.
-Induction 1.
-Intros T i m; Elim (insert T i a).
-Intros; Apply heap_exist with T1; Simpl; 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 : (l:(list A))(sort leA l) ->
-              ((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 : (T:Tree)(is_heap T) -> (flat_spec T).
-Proof.
-  Intros T h; Elim h; Intros.
-  Apply flat_exist with (nil 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 (cons a l); Simpl; 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 : (l:(list A))
-  {m:(list A) | (sort leA m) & (permutation eqA_dec l m)}.
-Proof.
-  Intro l; Unfold permutation.
-  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.
diff --git a/theories7/Sorting/Permutation.v b/theories7/Sorting/Permutation.v
deleted file mode 100644
index 46b8da00..00000000
--- a/theories7/Sorting/Permutation.v
+++ /dev/null
@@ -1,111 +0,0 @@
-(************************************************************************)
-(*  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.1.2.1 2004/07/16 19:31:41 herbelin Exp $ i*)
-
-Require Relations.
-Require PolyList.
-Require Multiset.
-
-Set Implicit Arguments.
-
-Section defs.
-
-Variable A : Set.
-Variable leA : (relation A).
-Variable eqA : (relation A).
-
-Local gtA := [x,y:A]~(leA x y).
-
-Hypothesis leA_dec : (x,y:A){(leA x y)}+{~(leA x y)}.
-Hypothesis eqA_dec : (x,y:A){(eqA x y)}+{~(eqA x y)}.
-Hypothesis leA_refl : (x,y:A) (eqA x y) -> (leA x y).
-Hypothesis leA_trans : (x,y,z:A) (leA x y) -> (leA y z) -> (leA x z).
-Hypothesis leA_antisym : (x,y:A)(leA x y) -> (leA y x) -> (eqA x y).
-
-Hints Resolve leA_refl : default.
-Hints Immediate eqA_dec leA_dec leA_antisym : default.
-
-Local emptyBag := (EmptyBag A).
-Local singletonBag := (SingletonBag eqA_dec).
-
-(** contents of a list *)
-
-Fixpoint list_contents [l:(list A)] : (multiset A) :=
- Cases l of
-   nil        => emptyBag
- | (cons a l) => (munion (singletonBag a) (list_contents l))
- end.
-
-Lemma list_contents_app : (l,m:(list A))
-  (meq (list_contents (app l m)) (munion (list_contents l) (list_contents m))).
-Proof.
-Induction l; Simpl; Auto with datatypes.
-Intros.
-Apply meq_trans with  
- (munion (singletonBag a) (munion (list_contents l0) (list_contents m))); Auto with datatypes.
-Qed.
-Hints Resolve list_contents_app.
-
-Definition permutation := [l,m:(list A)](meq (list_contents l) (list_contents m)).
-
-Lemma permut_refl : (l:(list A))(permutation l l).
-Proof.
-Unfold permutation; Auto with datatypes.
-Qed.
-Hints Resolve permut_refl.
-
-Lemma permut_tran : (l,m,n:(list A))
-   (permutation l m) -> (permutation m n) -> (permutation l n).
-Proof.
-Unfold permutation; Intros.
-Apply meq_trans with (list_contents m); Auto with datatypes.
-Qed.
-
-Lemma permut_right : (l,m:(list A))
-   (permutation l m) -> (a:A)(permutation (cons a l) (cons a m)).
-Proof.
-Unfold permutation; Simpl; Auto with datatypes.
-Qed.
-Hints Resolve permut_right.
-
-Lemma permut_app : (l,l',m,m':(list A))
-   (permutation l l') -> (permutation m m') ->
-   (permutation (app l m) (app l' m')).
-Proof.
-Unfold permutation; 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.
-Hints Resolve permut_app.
-
-Lemma permut_cons : (l,m:(list A))(permutation l m) ->
-    (a:A)(permutation (cons a l) (cons a m)).
-Proof.
-Intros l m H a.
-Change (permutation (app (cons a (nil A)) l) (app (cons a (nil A)) m)).
-Apply permut_app; Auto with datatypes.
-Qed.
-Hints Resolve permut_cons.
-
-Lemma permut_middle : (l,m:(list A))
-   (a:A)(permutation (cons a (app l m)) (app l (cons a m))).
-Proof.
-Unfold permutation.
-Induction l; Simpl; Auto with datatypes.
-Intros.
-Apply meq_trans with (munion (singletonBag a)
-          (munion (singletonBag a0) (list_contents (app l0 m)))); Auto with datatypes.
-Apply munion_perm_left; Auto with datatypes.
-Qed.
-Hints Resolve permut_middle.
-
-End defs.
-Unset Implicit Arguments.
-
diff --git a/theories7/Sorting/Sorting.v b/theories7/Sorting/Sorting.v
deleted file mode 100644
index a6e38976..00000000
--- a/theories7/Sorting/Sorting.v
+++ /dev/null
@@ -1,117 +0,0 @@
-(************************************************************************)
-(*  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.1.2.1 2004/07/16 19:31:41 herbelin Exp $ i*)
-
-Require PolyList.
-Require Multiset.
-Require Permutation.
-Require Relations.
-
-Set Implicit Arguments.
-
-Section defs.
-
-Variable A : Set.
-Variable leA : (relation A).
-Variable eqA : (relation A).
-
-Local gtA := [x,y:A]~(leA x y).
-
-Hypothesis leA_dec : (x,y:A){(leA x y)}+{(leA y x)}.
-Hypothesis eqA_dec : (x,y:A){(eqA x y)}+{~(eqA x y)}.
-Hypothesis leA_refl : (x,y:A) (eqA x y) -> (leA x y).
-Hypothesis leA_trans : (x,y,z:A) (leA x y) -> (leA y z) -> (leA x z).
-Hypothesis leA_antisym : (x,y:A)(leA x y) -> (leA y x) -> (eqA x y).
-
-Hints Resolve leA_refl.
-Hints Immediate eqA_dec leA_dec leA_antisym.
-
-Local emptyBag := (EmptyBag A).
-Local singletonBag := (SingletonBag eqA_dec).
-
-(** [lelistA] *)
-
-Inductive lelistA [a:A] : (list A) -> Prop :=
-      nil_leA : (lelistA a (nil A))
-    | cons_leA : (b:A)(l:(list A))(leA a b)->(lelistA a (cons b l)).
-Hint constr_lelistA := Constructors lelistA.
-
-Lemma lelistA_inv : (a,b:A)(l:(list A))
-      (lelistA a (cons 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 A))
- | cons_sort : (a:A)(l:(list A))(sort l) -> (lelistA a l) -> (sort (cons a l)).
-Hint constr_sort := Constructors sort.
-
-Lemma sort_inv : (a:A)(l:(list A))(sort (cons a l))->(sort l) /\ (lelistA a l).
-Proof.
-Intros; Inversion H; Auto with datatypes.
-Qed.
-
-Lemma sort_rec : (P:(list A)->Set)
-     (P (nil A)) ->
-     ((a:A)(l:(list A))(sort l)->(P l)->(lelistA a l)->(P (cons a l))) ->
-     (y:(list A))(sort y) -> (P y).
-Proof.
-Induction y; Auto with datatypes.
-Intros; Elim (!sort_inv a l); Auto with datatypes.
-Qed.
-
-(** merging two sorted lists *)
-
-Inductive merge_lem [l1:(list A);l2:(list A)] : Set :=
-  merge_exist : (l:(list A))(sort l) ->
-    (meq (list_contents eqA_dec l)
-         (munion (list_contents eqA_dec l1) (list_contents eqA_dec l2))) ->
-    ((a:A)(lelistA a l1)->(lelistA a l2)->(lelistA a l)) ->
-    (merge_lem l1 l2).
-
-Lemma merge : (l1:(list A))(sort l1)->(l2:(list A))(sort l2)->(merge_lem l1 l2).
-Proof.
-  Induction 1; Intros.
-  Apply merge_exist with l2; Auto with datatypes.
-  Elim H3; Intros.
-  Apply merge_exist with (cons a l); Simpl; Auto with datatypes.
-  Elim (leA_dec a a0); Intros.
-
-(* 1 (leA a a0) *)
-  Cut (merge_lem l (cons a0 l0)); Auto with datatypes.
-  Intros (l3, l3sorted, l3contents, Hrec).
-  Apply merge_exist with (cons a l3); Simpl; Auto with datatypes.
-  Apply meq_trans with (munion (singletonBag a)
-	                       (munion (list_contents eqA_dec l)
-                                       (list_contents eqA_dec (cons 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; Intros.
-  Apply merge_exist with (cons a0 l3); Simpl; 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 constr_sort : datatypes v62 := Constructors sort.
-Hint constr_lelistA : datatypes v62 := Constructors lelistA.