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, 87 insertions, 78 deletions

diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index 8f7e76d51d..22476505fa 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -25,125 +25,134 @@
 Set Implicit Arguments.
 
   (** Bijection between [eq] and [eqT] *)
-  Definition eq2eqT: (A:Set)(x,y:A)x=y->x==y :=
-    [A,x,_,eqxy]<[y:A]x==y>Cases eqxy of refl_equal => (refl_eqT ? x) end.
-
-  Definition eqT2eq: (A:Set)(x,y:A)x==y->x=y :=
-    [A,x,_,eqTxy]<[y:A]x=y>Cases eqTxy of refl_eqT => (refl_equal ? x) end.
-
-  Lemma eq_eqT_bij: (A:Set)(x,y:A)(p:x=y)p==(eqT2eq (eq2eqT p)).
-Intros.
-Case p; Reflexivity.
+  Definition eq2eqT (A:Set) (x y:A) (eqxy:x = y) : 
+    x = y :=
+    match eqxy in (_ = y) return x = y with
+    | refl_equal => refl_equal x
+    end.
+
+  Definition eqT2eq (A:Set) (x y:A) (eqTxy:x = y) : 
+    x = y :=
+    match eqTxy in (_ = y) return x = y with
+    | refl_equal => refl_equal x
+    end.
+
+  Lemma eq_eqT_bij : forall (A:Set) (x y:A) (p:x = y), p = eqT2eq (eq2eqT p).
+intros.
+case p; reflexivity.
 Qed.
 
-  Lemma eqT_eq_bij: (A:Set)(x,y:A)(p:x==y)p==(eq2eqT (eqT2eq p)).
-Intros.
-Case p; Reflexivity.
+  Lemma eqT_eq_bij : forall (A:Set) (x y:A) (p:x = y), p = eq2eqT (eqT2eq p).
+intros.
+case p; reflexivity.
 Qed.
 
 
 Section DecidableEqDep.
 
-  Variable A: Type.
+  Variable A : Type.
 
-  Local comp [x,y,y':A]: x==y->x==y'->y==y' :=
-    [eq1,eq2](eqT_ind ? ? [a]a==y' eq2 ? eq1).
+  Let comp (x y y':A) (eq1:x = y) (eq2:x = y') : y = y' :=
+    eq_ind _ (fun a => a = y') eq2 _ eq1.
 
-  Remark trans_sym_eqT: (x,y:A)(u:x==y)(comp u u)==(refl_eqT ? y).
-Intros.
-Case u; Trivial.
+  Remark trans_sym_eqT : forall (x y:A) (u:x = y), comp u u = refl_equal y.
+intros.
+case u; trivial.
 Qed.
 
 
 
-  Variable eq_dec: (x,y:A) x==y \/ ~x==y.
+  Variable eq_dec : forall x y:A, x = y \/ x <> y.
 
-  Variable x: A.
+  Variable x : A.
 
 
-  Local nu [y:A]: x==y->x==y :=
-    [u]Cases (eq_dec x y) of
-       (or_introl eqxy)  => eqxy
-     | (or_intror neqxy) => (False_ind ? (neqxy u))
-     end.
+  Let nu (y:A) (u:x = y) : x = y :=
+    match eq_dec x y with
+    | or_introl eqxy => eqxy
+    | or_intror neqxy => False_ind _ (neqxy u)
+    end.
 
-  Local nu_constant : (y:A)(u,v:x==y) (nu u)==(nu v).
-Intros.
-Unfold nu.
-Case (eq_dec x y); Intros.
-Reflexivity.
+  Let nu_constant : forall (y:A) (u v:x = y), nu u = nu v.
+intros.
+unfold nu in |- *.
+case (eq_dec x y); intros.
+reflexivity.
 
-Case n; Trivial.
+case n; trivial.
 Qed.
 
 
-  Local nu_inv [y:A]: x==y->x==y := [v](comp (nu (refl_eqT ? x)) v).
+  Let nu_inv (y:A) (v:x = y) : x = y := comp (nu (refl_equal x)) v.
 
 
-  Remark nu_left_inv : (y:A)(u:x==y) (nu_inv (nu u))==u.
-Intros.
-Case u; Unfold nu_inv.
-Apply trans_sym_eqT.
+  Remark nu_left_inv : forall (y:A) (u:x = y), nu_inv (nu u) = u.
+intros.
+case u; unfold nu_inv in |- *.
+apply trans_sym_eqT.
 Qed.
 
 
-  Theorem eq_proofs_unicity: (y:A)(p1,p2:x==y) p1==p2.
-Intros.
-Elim nu_left_inv with u:=p1.
-Elim nu_left_inv with u:=p2.
-Elim nu_constant with y p1 p2.
-Reflexivity.
+  Theorem eq_proofs_unicity : forall (y:A) (p1 p2:x = y), p1 = p2.
+intros.
+elim nu_left_inv with (u := p1).
+elim nu_left_inv with (u := p2).
+elim nu_constant with y p1 p2.
+reflexivity.
 Qed.
 
-  Theorem K_dec: (P:x==x->Prop)(P (refl_eqT ? x)) -> (p:x==x)(P p).
-Intros.
-Elim eq_proofs_unicity with x (refl_eqT ? x) p.
-Trivial.
+  Theorem K_dec :
+   forall P:x = x -> Prop, P (refl_equal x) -> forall p:x = x, P p.
+intros.
+elim eq_proofs_unicity with x (refl_equal x) p.
+trivial.
 Qed.
 
 
   (** The corollary *)
 
-  Local proj: (P:A->Prop)(ExT P)->(P x)->(P x) :=
-    [P,exP,def]Cases exP of
-      (exT_intro x' prf) =>
-        Cases (eq_dec x' x) of
-          (or_introl eqprf) => (eqT_ind ? x' P prf x eqprf)
+  Let proj (P:A -> Prop) (exP:ex P) (def:P x) : P x :=
+    match exP with
+    | ex_intro x' prf =>
+        match eq_dec x' x with
+        | or_introl eqprf => eq_ind x' P prf x eqprf
         | _ => def
         end
-      end.
+    end.
 
 
-  Theorem inj_right_pair: (P:A->Prop)(y,y':(P x))
-    (exT_intro ? P x y)==(exT_intro ? P x y') -> y==y'.
-Intros.
-Cut (proj (exT_intro A P x y) y)==(proj (exT_intro A P x y') y).
-Simpl.
-Case (eq_dec x x).
-Intro e.
-Elim e using K_dec; Trivial.
+  Theorem inj_right_pair :
+   forall (P:A -> Prop) (y y':P x),
+     ex_intro P x y = ex_intro P x y' -> y = y'.
+intros.
+cut (proj (ex_intro P x y) y = proj (ex_intro P x y') y).
+simpl in |- *.
+case (eq_dec x x).
+intro e.
+elim e using K_dec; trivial.
 
-Intros.
-Case n; Trivial.
+intros.
+case n; trivial.
 
-Case H.
-Reflexivity.
+case H.
+reflexivity.
 Qed.
 
 End DecidableEqDep.
 
   (** We deduce the [K] axiom for (decidable) Set *)
-  Theorem K_dec_set: (A:Set)((x,y:A){x=y}+{~x=y})
-                       ->(x:A)(P: x=x->Prop)(P (refl_equal ? x))
-                         ->(p:x=x)(P p).
-Intros.
-Rewrite eq_eqT_bij.
-Elim (eq2eqT p) using K_dec.
-Intros.
-Case (H x0 y); Intros.
-Elim e; Left ; Reflexivity.
-
-Right ; Red; Intro neq; Apply n; Elim neq; Reflexivity.
-
-Trivial.
-Qed.
+  Theorem K_dec_set :
+   forall A:Set,
+     (forall x y:A, {x = y} + {x <> y}) ->
+     forall (x:A) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
+intros.
+rewrite eq_eqT_bij.
+elim (eq2eqT p) using K_dec.
+intros.
+case (H x0 y); intros.
+elim e; left; reflexivity.
+
+right; red in |- *; intro neq; apply n; elim neq; reflexivity.
+
+trivial.
+Qed.
\ No newline at end of file