Ajout exists! et restructuration/extension des fichiers sur la

description et le choix


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

1 files changed, 27 insertions, 5 deletions

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 4907c93a40..53a5268954 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -280,13 +280,35 @@ Qed.
 
 Hint Immediate sym_eq sym_not_eq: core v62.
 
-(** Other notations *)
+(** Basic definitions about relations and properties *)
 
-Notation "'exists' ! x , P" := 
-  (exists x',  (fun x => P) x' /\ forall x'', (fun x => P) x'' -> x' = x'')
+Definition subrelation (A B : Type) (R R' : A->B->Prop) :=
+  forall x y, R x y -> R' x y.
+
+Definition singleton (A : Type) (P : A->Prop) (x:A) :=
+  P x /\ forall (x':A), P x' -> x=x'.
+
+Definition uniqueness (A:Type) (P:A->Prop) := forall x y, P x -> P y -> x = y.
+
+(** Unique existence *)
+
+Notation "'exists' ! x , P" := (exists x', singleton (fun x => P) x')
   (at level 200, x ident, right associativity,
    format "'[' 'exists' !  '/  ' x ,  '/  ' P ']'") : type_scope.
-Notation "'exists' ! x : A , P" := 
-  (exists x' : A,  (fun x => P) x' /\ forall x'':A, (fun x => P) x'' -> x' = x'')
+Notation "'exists' ! x : A , P" := (exists x':A, singleton (fun x:A => P) x')
   (at level 200, x ident, right associativity,
    format "'[' 'exists' !  '/  ' x  :  A ,  '/  ' P ']'") : type_scope.
+
+Lemma unique_existence : forall (A:Type) (P:A->Prop),
+  ((exists x, P x) /\ uniqueness P) <-> (exists! x, P x).
+Proof.
+intros A P; split.
+  intros ((x,Hx),Huni); exists x; red; auto.
+  intros (x,(Hx,Huni)); split. 
+    exists x; assumption.
+    intros x' x'' Hx' Hx''; transitivity x.
+      symmetry; auto.
+      auto.
+Qed.
+
+