Library Coq.Logic.ChoiceFacts
Definition RelationalChoice :=
forall (A B:Type) (R:A -> B -> Prop),
(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')).
Definition FunctionalChoice :=
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)).
Definition ParamDefiniteDescription :=
forall (A B:Type) (R:A -> B -> Prop),
(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 :
ParamDefiniteDescription -> RelationalChoice -> FunctionalChoice.
intros Descr RelCh.
red in |- *; intros A B R H.
destruct (RelCh A B R H) as [R' H0].
destruct (Descr A B R') as [f H1].
intro x.
elim (H0 x); intros y [H2 [H3 H4]]; exists y; split; [ exact H3 | exact H4 ].
exists f; intro x.
elim (H0 x); intros y [H2 [H3 H4]].
rewrite <- (H4 (f x) (H1 x)).
exact H2.
Qed.
Lemma funct_choice_imp_rel_choice : FunctionalChoice -> RelationalChoice.
intros FunCh.
red in |- *; intros A B R H.
destruct (FunCh A B R H) as [f H0].
exists (fun x y => y = f x).
intro x; exists (f x); split;
[ apply H0
| split; [ reflexivity | intros y H1; symmetry in |- *; exact H1 ] ].
Qed.
Lemma funct_choice_imp_description :
FunctionalChoice -> ParamDefiniteDescription.
intros FunCh.
red in |- *; intros A B R H.
destruct (FunCh A B R) as [f H0].
intro x.
elim (H x); intros y [H0 H1].
exists y; exact H0.
exists f; exact H0.
Qed.
Theorem FunChoice_Equiv_RelChoice_and_ParamDefinDescr :
FunctionalChoice <-> RelationalChoice /\ ParamDefiniteDescription.
split.
intro H; split;
[ exact (funct_choice_imp_rel_choice H)
| exact (funct_choice_imp_description H) ].
intros [H H0]; exact (description_rel_choice_imp_funct_choice H0 H).
Qed.
Definition GuardedRelationalChoice :=
forall (A B:Type) (P:A -> Prop) (R:A -> B -> Prop),
(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')).
Definition ProofIrrelevance := forall (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 in |- *; intros A B P R H.
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).
exists R''; intros x HPx.
destruct (H0 (existT P x HPx)) as [y [HRxy [HR'xy Huniq]]].
exists y. split.
exact HRxy.
split.
red in |- *; exists HPx; exact HR'xy.
intros y' HR''xy'.
apply Huniq.
unfold R'' in HR''xy'.
destruct HR''xy' as [H'Px HR'xy'].
rewrite proof_irrel with (a1:= HPx) (a2:= H'Px).
exact HR'xy'.
Qed.
Definition IndependenceOfPremises :=
forall (A:Type) (P:A -> Prop) (Q:Prop),
(Q -> exists x : _, P x) -> exists x : _, Q -> P x.
Lemma rel_choice_indep_of_premises_imp_guarded_rel_choice :
RelationalChoice -> IndependenceOfPremises -> GuardedRelationalChoice.
Proof.
intros RelCh IndPrem.
red in |- *; intros A B P R H.
destruct (RelCh A B (fun x y => P x -> R x y)) as [R' H0].
intro x. apply IndPrem.
apply H.
exists R'.
intros x HPx.
destruct (H0 x) as [y [H1 H2]].
exists y. split.
apply (H1 HPx).
exact H2.
Qed.
Index
This page has been generated by coqdoc