diff options
Diffstat (limited to 'theories/Logic/ClassicalDescription.v')
-rw-r--r-- | theories/Logic/ClassicalDescription.v | 42 |
1 files changed, 15 insertions, 27 deletions
diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v index 7053266a..1f1c34bf 100644 --- a/theories/Logic/ClassicalDescription.v +++ b/theories/Logic/ClassicalDescription.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalDescription.v 8892 2006-06-04 17:59:53Z herbelin $ i*) +(*i $Id: ClassicalDescription.v 9514 2007-01-22 14:58:50Z herbelin $ i*) (** This file provides classical logic and definite description *) @@ -57,14 +57,11 @@ Definition iota_spec (A : Type) (i:inhabited A) (P : A->Prop) : (exists! x:A, P x) -> P (iota i P) := proj2_sig (classical_definite_description P i). -(** Weaker lemmas (compatibility lemmas) *) - -Unset Implicit Arguments. - -Lemma dependent_description : - 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)). +(** Axiom of unique "choice" (functional reification of functional relations) *) +Theorem 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)). Proof. intros A B R H. assert (Hexuni:forall x, exists! y, R x y). @@ -74,27 +71,18 @@ intro x. apply (proj2_sig (constructive_definite_description (R x) (Hexuni x))). Qed. -Theorem description : - 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)). +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_description A (fun _ => B)). +apply dependent_unique_choice with (B:=fun _:A => B). Qed. -(** Axiom of unique "choice" (functional reification of functional relations) *) +(** Compatibility lemmas *) -Set Implicit Arguments. - -Require Import Setoid. +Unset Implicit Arguments. -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 R H. -apply (description A B). -intro x. apply H. -Qed. +Definition dependent_description := dependent_unique_choice. +Definition description := unique_choice. |