From 06e40b8c8f37a0afbe97d2e6e17cd4e45fabddcf Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 16 Jul 2011 20:35:06 +0000
Subject: Added a characterization of unique existence.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14277 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/Logic.v | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index c72193c0b0..8551ca97dc 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -407,6 +407,29 @@ Proof.
   auto.
 Qed.
 
+Lemma forall_exists_unique_domain_coincide :
+  forall A (P:A->Prop), (exists! x, P x) ->
+  forall Q:A->Prop, (forall x, P x -> Q x) <-> (exists x, P x /\ Q x).
+Proof.
+  intros A P (x & Hp & Huniq); split.
+  intro; exists x; auto.
+  intros (x0 & HPx0 & HQx0) x1 HPx1.
+  replace x1 with x0 by (transitivity x; [symmetry|]; auto).
+  assumption.
+Qed.   
+
+Lemma forall_exists_coincide_unique_domain :
+  forall A (P:A->Prop),
+  (forall Q:A->Prop, (forall x, P x -> Q x) <-> (exists x, P x /\ Q x))
+  -> (exists! x, P x).
+Proof.
+  intros A P H.
+  destruct H with (Q:=P) as ((x & Hx & _),_); [trivial|].
+  exists x. split; [trivial|].
+  destruct H with (Q:=fun x'=>x=x') as (_,Huniq).
+  apply Huniq. exists x; auto.
+Qed.       
+
 (** * Being inhabited *)
 
 (** The predicate [inhabited] can be used in different contexts. If [A] is
-- 
cgit v1.2.3