Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 139 insertions, 135 deletions

diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
index 31e3ac447..95a40ab12 100644
--- a/theories/Sorting/Heap.v
+++ b/theories/Sorting/Heap.v
@@ -12,103 +12,102 @@
 
 (* G. Huet 1-9-95 uses Multiset *)
 
-Require PolyList.
-Require Multiset.
-Require Permutation.
-Require Relations.
-Require Sorting.
+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).
+Variable leA : relation A.
+Variable eqA : relation A.
 
-Local gtA := [x,y:A]~(leA x y).
+Let 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).
+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.
 
-Hints Resolve leA_refl.
-Hints Immediate eqA_dec leA_dec leA_antisym.
+Hint Resolve leA_refl.
+Hint Immediate eqA_dec leA_dec leA_antisym.
 
-Local emptyBag := (EmptyBag A).
-Local singletonBag := (SingletonBag eqA_dec).
+Let emptyBag := EmptyBag A.
+Let singletonBag := SingletonBag _ eqA_dec.
 
 Inductive Tree : Set :=
-      Tree_Leaf : Tree
-    | Tree_Node : A -> Tree -> Tree -> Tree.
+  | 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.
+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 : (a:A)(leA_Tree a Tree_Leaf).
+Lemma leA_Tree_Leaf : forall a:A, leA_Tree a Tree_Leaf.
 Proof.
-Simpl; Auto with datatypes.
+simpl in |- *; 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)).
+Lemma leA_Tree_Node :
+ forall (a b:A) (G D:Tree), leA a b -> leA_Tree a (Tree_Node b G D).
 Proof.
-Simpl; Auto with datatypes.
+simpl in |- *; auto with datatypes.
 Qed.
 
-Hints Resolve leA_Tree_Leaf leA_Tree_Node.
+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 : (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).
+  | 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.
+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).
+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.
-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.
+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 : 
-  (T:Tree)(a,b:A)(leA a b) -> (leA_Tree b T) -> (leA_Tree a T).
+Lemma low_trans :
+ forall (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.
+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 *)
@@ -117,107 +116,112 @@ Qed.
     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.
+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)).
+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).
+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 : (T:Tree)(is_heap T) -> (a:A)(insert_spec a T).
+Lemma insert : forall T:Tree, is_heap T -> forall 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. 
+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 : (T:Tree)(is_heap T) ->
-                (meq (list_contents eqA_dec l)(contents T)) ->
-                (build_heap l).
+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 : (l:(list A))(build_heap l).
+Lemma list_to_heap : forall 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.
+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 : (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).
+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 : (T:Tree)(is_heap T) -> (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); 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.
+  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 : (l:(list A))
-  {m:(list A) | (sort leA m) & (permutation eqA_dec l m)}.
+Theorem treesort :
+ forall 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.
+  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.
+End defs.
\ No newline at end of file