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@8893 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 163 insertions, 0 deletions

diff --git a/theories/Logic/ClassicalEpsilon.v b/theories/Logic/ClassicalEpsilon.v
new file mode 100644
index 000000000..b3efa5fad
--- /dev/null
+++ b/theories/Logic/ClassicalEpsilon.v
@@ -0,0 +1,84 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id:$ i*)
+
+(** This file provides classical logic and indefinite description
+    (Hilbert's epsilon operator) *)
+
+(** Classical epsilon's operator (i.e. indefinite description) implies
+    excluded-middle in [Set] and leads to a classical world populated
+    with non computable functions. It conflicts with the
+    impredicativity of [Set] *)
+
+Require Export Classical.
+Require Import ChoiceFacts.
+
+Set Implicit Arguments.
+
+Notation Local "'inhabited' A" := A (at level 200, only parsing).
+
+Axiom constructive_indefinite_description :
+  forall (A : Type) (P : A->Prop), 
+  (exists x : A, 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 }.
+Proof.
+intros; apply constructive_indefinite_description; firstorder.
+Qed.
+
+Theorem excluded_middle_informative : forall P:Prop, {P} + {~ P}.
+Proof.
+apply 
+  (constructive_definite_descr_excluded_middle 
+   constructive_definite_description classic).
+Qed.
+
+Theorem classical_indefinite_description : 
+  forall (A : Type) (P : A->Prop), inhabited A ->
+  { x : A | (exists x : A, 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 => (exists x, P x) -> P x).
+  destruct Hex as (x,Hx).
+    exists x; intros _; exact Hx.
+    firstorder.
+Qed.
+
+(** Hilbert's epsilon operator *)
+
+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) : 
+  (exists x:A, P x) -> P (epsilon i P)
+  := proj2_sig (classical_indefinite_description P i).
+
+(** Open question: is classical_indefinite_description constructively
+    provable from [relational_choice] and
+    [constructive_definite_description] (at least, using the fact that
+    [functional_choice] is provable from [relational_choice] and
+    [unique_choice], we know that the double negation of
+    [classical_indefinite_description] is provable (see
+    [relative_non_contradiction_of_indefinite_desc]). *)
+
+(** Weaker lemmas (compatibility lemmas) *)
+
+Theorem choice :
+ forall (A B : Type) (R : A->B->Prop),
+   (forall x : A, exists y : B, R x y) ->
+   (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 (R x) (H x))).
+intro x.
+apply (proj2_sig (constructive_indefinite_description (R x) (H x))).
+Qed.
diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v
new file mode 100644
index 000000000..2be5a0eb6
--- /dev/null
+++ b/theories/Logic/ClassicalUniqueChoice.v
@@ -0,0 +1,79 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+(** This file provides classical logic and unique choice *)
+
+(** Classical logic and unique choice, as shown in
+    [ChicliPottierSimpson02], implies the double-negation of
+    excluded-middle in [Set], hence it implies a strongly classical
+    world. Especially it conflicts with the impredicativity of [Set].
+
+    [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos
+    Simpson, Mathematical Quotients and Quotient Types in Coq,
+    Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646,
+    Springer Verlag.  *)
+
+Require Export Classical.
+
+Axiom
+  dependent_unique_choice :
+    forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop),
+      (forall x : A, exists! y : B x, R x y) ->
+      (exists f : (forall x:A, B x), forall x:A, R x (f x)).
+
+(** Unique choice reifies functional relations into functions *)
+
+Theorem unique_choice :
+ forall (A B:Type) (R:A -> B -> Prop),
+   (forall x:A,  exists! y : B, R x y) ->
+   (exists f:A->B, forall x:A, R x (f x)).
+Proof.
+intros A B.
+apply (dependent_unique_choice A (fun _ => B)).
+Qed.
+
+(** The followig proof comes from [ChicliPottierSimpson02] *)
+
+Require Import Setoid.
+
+Theorem classic_set : ((forall P:Prop, {P} + {~ P}) -> False) -> False.
+Proof.
+intro HnotEM.
+set (R := fun A b => A /\ true = b \/ ~ A /\ false = b).
+assert (H :  exists f : Prop -> bool, (forall A:Prop, R A (f A))).
+apply unique_choice.
+intro A.
+destruct (classic A) as [Ha| Hnota].
+  exists true; split.
+    left; split; [ assumption | reflexivity ].
+    intros y [[_ Hy]| [Hna _]].
+      assumption.
+      contradiction.
+  exists false; split.
+    right; split; [ assumption | reflexivity ].
+    intros y [[Ha _]| [_ Hy]].
+      contradiction.
+      assumption.
+destruct H as [f Hf].
+apply HnotEM.
+intro P.
+assert (HfP := Hf P).
+(* Elimination from Hf to Set is not allowed but from f to Set yes ! *)
+destruct (f P).
+  left.
+  destruct HfP as [[Ha _]| [_ Hfalse]].
+    assumption.
+    discriminate.
+  right.
+  destruct HfP as [[_ Hfalse]| [Hna _]].
+    discriminate.
+    assumption.
+Qed.
+