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/Epsilon.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/Epsilon.v')
-rw-r--r-- | theories/Logic/Epsilon.v | 72 |
1 files changed, 72 insertions, 0 deletions
diff --git a/theories/Logic/Epsilon.v b/theories/Logic/Epsilon.v new file mode 100644 index 000000000..ead91c9ec --- /dev/null +++ b/theories/Logic/Epsilon.v @@ -0,0 +1,72 @@ +(************************************************************************) +(* 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 indefinite description under the form of + Hilbert's epsilon operator; it does not assume classical logic. *) + +Require Import ChoiceFacts. + +Set Implicit Arguments. + +(** Hilbert's epsilon: operator and specification in one statement *) + +Axiom epsilon_statement : + forall (A : Type) (P : A->Prop), inhabited A -> + { x : A | (exists x, P x) -> P x }. + +Lemma constructive_indefinite_description : + forall (A : Type) (P : A->Prop), + (exists x, P x) -> { x : A | P x }. +Proof. + apply epsilon_imp_constructive_indefinite_description. + exact epsilon_statement. +Qed. + +Lemma small_drinkers'_paradox : + forall (A:Type) (P:A -> Prop), inhabited A -> + exists x, (exists x, P x) -> P x. +Proof. + apply epsilon_imp_small_drinker. + exact epsilon_statement. +Qed. + +Theorem iota_statement : + forall (A : Type) (P : A->Prop), inhabited A -> + { x : A | (exists! x : A, P x) -> P x }. +Proof. + intros; destruct epsilon_statement with (P:=P); firstorder. +Qed. + +Lemma constructive_definite_description : + forall (A : Type) (P : A->Prop), + (exists! x, P x) -> { x : A | P x }. +Proof. + apply iota_imp_constructive_definite_description. + exact iota_statement. +Qed. + +(** Hilbert's epsilon operator and its specification *) + +Definition epsilon (A : Type) (i:inhabited A) (P : A->Prop) : A + := proj1_sig (epsilon_statement P i). + +Definition epsilon_spec (A : Type) (i:inhabited A) (P : A->Prop) : + (exists x, P x) -> P (epsilon i P) + := proj2_sig (epsilon_statement P i). + +(** Church's iota operator and its specification *) + +Definition iota (A : Type) (i:inhabited A) (P : A->Prop) : A + := proj1_sig (iota_statement P i). + +Definition iota_spec (A : Type) (i:inhabited A) (P : A->Prop) : + (exists! x:A, P x) -> P (iota i P) + := proj2_sig (iota_statement P i). + |