aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Logic/ChoiceFacts.v
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-03-05 10:59:47 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-03-05 10:59:47 +0000
commit4577b6684e8a725d21c37e5fec627bdec198594d (patch)
treec750b16be1c4bbbba5ce1b5194fdca839eb82681 /theories/Logic/ChoiceFacts.v
parent73a86067cdb72a260164caec8d30029de3c0b10e (diff)
Renommage du IP classique pour éviter confusion avec IP constructif
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8132 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Logic/ChoiceFacts.v')
-rw-r--r--theories/Logic/ChoiceFacts.v24
1 files changed, 12 insertions, 12 deletions
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 723434512..5180bf5b2 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -23,19 +23,19 @@ Variables A B :Type.
Definition RelationalChoice :=
forall (R:A -> B -> Prop),
- (forall x:A, exists y : B, R x y) ->
+ (forall x:A, exists y : B, R x y) ->
exists R' : A -> B -> Prop,
(forall x:A,
- exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
+ exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
Definition FunctionalChoice :=
forall (R:A -> B -> Prop),
- (forall x:A, exists y : B, R x y) ->
+ (forall x:A, exists y : B, R x y) ->
exists f : A -> B, (forall x:A, R x (f x)).
Definition ParamDefiniteDescription :=
forall (R:A -> B -> Prop),
- (forall x:A, exists y : B, R x y /\ (forall y':B, R x y' -> y = y')) ->
+ (forall x:A, exists y : B, R x y /\ (forall y':B, R x y' -> y = y')) ->
exists f : A -> B, (forall x:A, R x (f x)).
Lemma description_rel_choice_imp_funct_choice :
@@ -92,11 +92,11 @@ End ChoiceEquivalences.
Definition GuardedRelationalChoice (A B:Type) :=
forall (P:A -> Prop) (R:A -> B -> Prop),
- (forall x:A, P x -> exists y : B, R x y) ->
+ (forall x:A, P x -> exists y : B, R x y) ->
exists R' : A -> B -> Prop,
(forall x:A,
P x ->
- exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
+ exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
Definition ProofIrrelevance := forall (A:Prop) (a1 a2:A), a1 = a2.
@@ -110,7 +110,7 @@ destruct (rel_choice _ _ (fun (x:sigT P) (y:B) => R (projT1 x) y)) as [R' H0].
intros [x HPx].
destruct (H x HPx) as [y HRxy].
exists y; exact HRxy.
-set (R'' := fun (x:A) (y:B) => exists H : P x, R' (existT P x H) y).
+set (R'' := fun (x:A) (y:B) => exists H : P x, R' (existT P x H) y).
exists R''; intros x HPx.
destruct (H0 (existT P x HPx)) as [y [HRxy [HR'xy Huniq]]].
exists y. split.
@@ -125,13 +125,13 @@ exists y. split.
exact HR'xy'.
Qed.
-Definition IndependenceOfPremises :=
+Definition IndependenceOfGeneralPremises :=
forall (A:Type) (P:A -> Prop) (Q:Prop),
- (Q -> exists x : _, P x) -> exists x : _, Q -> P x.
+ (Q -> exists x, P x) -> exists x, Q -> P x.
-Lemma rel_choice_indep_of_premises_imp_guarded_rel_choice :
+Lemma rel_choice_indep_of_general_premises_imp_guarded_rel_choice :
forall A B, RelationalChoice A B ->
- IndependenceOfPremises -> GuardedRelationalChoice A B.
+ IndependenceOfGeneralPremises -> GuardedRelationalChoice A B.
Proof.
intros A B RelCh IndPrem.
red in |- *; intros P R H.
@@ -200,7 +200,7 @@ destruct (H n0) as [(n,(Hltn,(Hmin,Huniqn)))|]; [exists n | exists n0];
Qed.
Definition FunctionalChoice_on (A B:Type) (R:A->B->Prop) :=
- (forall x:A, exists y : B, R x y) ->
+ (forall x:A, exists y : B, R x y) ->
exists f : A -> B, (forall x:A, R x (f x)).
Lemma classical_denumerable_description_imp_fun_choice :