From 6eeef4f694e5833c3244604bda5fa44f82e2d039 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 28 Aug 2006 09:35:33 +0000
Subject: "Essai de remplacement de "ex P" par "exists x, P x" suite à
 l'introduction d'unification de motifs à la Miller permettant une forme
 restreinte canonique d'unification du second ordre

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9091 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Logic/ClassicalEpsilon.v | 18 ++++++++----------
 1 file changed, 8 insertions(+), 10 deletions(-)

diff --git a/theories/Logic/ClassicalEpsilon.v b/theories/Logic/ClassicalEpsilon.v
index 79c1e56d21..9c3d07238a 100644
--- a/theories/Logic/ClassicalEpsilon.v
+++ b/theories/Logic/ClassicalEpsilon.v
@@ -25,11 +25,11 @@ Notation Local "'inhabited' A" := A (at level 200, only parsing).
 
 Axiom constructive_indefinite_description :
   forall (A : Type) (P : A->Prop), 
-  (ex P) -> { x : A | P x }.
+  (exists x, P x) -> { x : A | P x }.
 
 Lemma constructive_definite_description :
   forall (A : Type) (P : A->Prop), 
-  (exists! x : A, P x) -> { x : A | P x }.
+  (exists! x, P x) -> { x : A | P x }.
 Proof.
 intros; apply constructive_indefinite_description; firstorder.
 Qed.
@@ -43,11 +43,12 @@ Qed.
 
 Theorem classical_indefinite_description : 
   forall (A : Type) (P : A->Prop), inhabited A ->
-  { x : A | ex P -> P x }.
+  { x : A | (exists x, P x) -> P x }.
 Proof.
 intros A P i.
 destruct (excluded_middle_informative (exists x, P x)) as [Hex|HnonP].
-  apply constructive_indefinite_description with (P:= fun x => ex P -> P x).
+  apply constructive_indefinite_description 
+    with (P:= fun x => (exists x, P x) -> P x).
   destruct Hex as (x,Hx).
     exists x; intros _; exact Hx.
     firstorder.
@@ -59,7 +60,7 @@ Definition epsilon (A : Type) (i:inhabited A) (P : A->Prop) : A
   := proj1_sig (classical_indefinite_description P i).
 
 Definition epsilon_spec (A : Type) (i:inhabited A) (P : A->Prop) : 
-  (ex P) -> P (epsilon i P)
+  (exists x, P x) -> P (epsilon i P)
   := proj2_sig (classical_indefinite_description P i).
 
 Opaque epsilon.
@@ -72,9 +73,6 @@ Opaque epsilon.
     [classical_indefinite_description] is provable (see
     [relative_non_contradiction_of_indefinite_desc]). *)
 
-(** Remark: we use [ex P] rather than [exists x, P x] (which is [ex
-    (fun x => P x)] to ease unification *)
-
 (** *** Weaker lemmas (compatibility lemmas) *)
 
 Theorem choice :
@@ -83,8 +81,8 @@ Theorem choice :
    (exists f : A->B, forall x : A, R x (f x)).
 Proof.
 intros A B R H.
-exists (fun x => proj1_sig (constructive_indefinite_description (H x))).
+exists (fun x => proj1_sig (constructive_indefinite_description _ (H x))).
 intro x.
-apply (proj2_sig (constructive_indefinite_description  (H x))).
+apply (proj2_sig (constructive_indefinite_description _ (H x))).
 Qed.
 
-- 
cgit v1.2.3