diff options
author | 2003-11-02 21:16:10 +0000 | |
---|---|---|
committer | 2003-11-02 21:16:10 +0000 | |
commit | d0f9e61aa3f944b2da80ca3359346c8e6dbccd5f (patch) | |
tree | fcf82e9190e3f87f33cad262fcdbb87d1c9de960 /theories/Logic/ChoiceFacts.v | |
parent | 1922c8a403f4d4686efe6115eecf7f56121e99da (diff) |
Relations entre le choix (forme relationnelle) avec restriction ou non
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4771 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Logic/ChoiceFacts.v')
-rw-r--r-- | theories/Logic/ChoiceFacts.v | 55 |
1 files changed, 55 insertions, 0 deletions
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index d0798d7a2..d9d8b7670 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -77,3 +77,58 @@ Intro H; Split; [ | Exact (funct_choice_imp_description H)]. Intros [H H0]; Exact (description_rel_choice_imp_funct_choice H0 H). Qed. + +(* We show that the guarded relational formulation of the axiom of Choice + comes from the non guarded formulation in presence either of the + independance of premises or proof-irrelevance *) + +Definition GuardedRelationalChoice := + (A:Type;B:Type;P:A->Prop;R: A->B->Prop) + ((x:A)(P x)->(EX y:B|(R x y))) + -> (EXT R':A->B->Prop | + ((x:A)(P x)->(EX y:B|(R x y)/\(R' x y)/\ ((y':B) (R' x y') -> y=y')))). + +Definition ProofIrrelevance := (A:Prop)(a1,a2:A) a1==a2. + +Lemma rel_choice_and_proof_irrel_imp_guarded_rel_choice : + RelationalChoice -> ProofIrrelevance -> GuardedRelationalChoice. +Proof. +Intros rel_choice proof_irrel. +Red; Intros A B P R H. +NewDestruct (rel_choice ? ? [x:(sigT ? P);y:B](R (projT1 ? ? x) y)) as [R' H0]. +Intros [x HPx]. +NewDestruct (H x HPx) as [y HRxy]. +Exists y; Exact HRxy. +Pose R'':=[x:A;y:B](EXT H:(P x) | (R' (existT ? P x H) y)). +Exists R''; Intros x HPx. +NewDestruct (H0 (existT ? P x HPx)) as [y [HRxy [HR'xy Huniq]]]. +Exists y. Split. + Exact HRxy. + Split. + Red; Exists HPx; Exact HR'xy. + Intros y' HR''xy'. + Apply Huniq. + Unfold R'' in HR''xy'. + NewDestruct HR''xy' as [H'Px HR'xy']. + Rewrite proof_irrel with a1:=HPx a2:=H'Px. + Exact HR'xy'. +.Qed. + +Definition IndependenceOfPremises := + (A:Type)(P:A->Prop)(Q:Prop)(Q->(EXT x|(P x)))->(EXT x|Q->(P x)). + +Lemma rel_choice_indep_of_premises_imp_guarded_rel_choice : + RelationalChoice -> IndependenceOfPremises -> GuardedRelationalChoice. +Proof. +Intros RelCh IndPrem. +Red; Intros A B P R H. +NewDestruct (RelCh A B [x,y](P x)->(R x y)) as [R' H0]. + Intro x. Apply IndPrem. + Apply H. + Exists R'. + Intros x HPx. + NewDestruct (H0 x) as [y [H1 H2]]. + Exists y. Split. + Apply (H1 HPx). + Exact H2. +Qed. |