diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-03 14:41:25 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-03 14:41:25 +0000 |
commit | 95483a55c228a0c3d9628a8b4e6cc45c84b8c894 (patch) | |
tree | 392b1080d0c4f22020db6566c12210551f120701 /theories/Logic/IndefiniteDescription.v | |
parent | 1bead2a1ef23f2a281613093d7861815279e336d (diff) |
Révision de theories/Logic concernant les axiomes de descriptions.
Mise à jour du tableau des axiomes dans la FAQ.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10170 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Logic/IndefiniteDescription.v')
-rw-r--r-- | theories/Logic/IndefiniteDescription.v | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/theories/Logic/IndefiniteDescription.v b/theories/Logic/IndefiniteDescription.v new file mode 100644 index 000000000..ce9405f85 --- /dev/null +++ b/theories/Logic/IndefiniteDescription.v @@ -0,0 +1,39 @@ +(************************************************************************) +(* 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 a constructive form of indefinite description that + allows to build choice functions; this is weaker than Hilbert's + epsilon operator (which implies weakly classical properties) but + stronger than the axiom of choice (which cannot be used outside + the context of a theorem proof). *) + +Require Import ChoiceFacts. + +Set Implicit Arguments. + +Axiom constructive_indefinite_description : + forall (A : Type) (P : A->Prop), + (exists x, P x) -> { x : A | P x }. + +Lemma constructive_definite_description : + forall (A : Type) (P : A->Prop), + (exists! x, P x) -> { x : A | P x }. +Proof. + intros; apply constructive_indefinite_description; firstorder. +Qed. + +Lemma functional_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. + apply constructive_indefinite_descr_fun_choice. + exact constructive_indefinite_description. +Qed. |