diff options
author | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-30 13:10:48 +0200 |
---|---|---|
committer | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-30 13:10:48 +0200 |
commit | fdd5a8452bd2da22ffd1cab3b1888f2261f193b9 (patch) | |
tree | f343f448f683430a6fc00f9e246745047279e1c3 | |
parent | 991b78fd9627ee76f1a1a39b8460bf361c6af53d (diff) |
Functional choice <-> [inhabited] and [forall] commute
-rw-r--r-- | theories/Init/Logic.v | 5 | ||||
-rw-r--r-- | theories/Init/Specif.v | 11 | ||||
-rw-r--r-- | theories/Logic/ChoiceFacts.v | 33 |
3 files changed, 49 insertions, 0 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 9ae9dde28..3eefe9a84 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -609,6 +609,11 @@ Proof. destruct 1; auto. Qed. +Lemma inhabited_covariant (A B : Type) : (A -> B) -> inhabited A -> inhabited B. +Proof. + intros f [x];exact (inhabits (f x)). +Qed. + (** Declaration of stepl and stepr for eq and iff *) Lemma eq_stepl : forall (A : Type) (x y z : A), x = y -> x = z -> z = y. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 2cc2ecbc2..43a441fc5 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -207,6 +207,17 @@ Definition sig2_eta {A P Q} (p : { a : A | P a & Q a }) : p = exist2 _ _ (proj1_sig (sig_of_sig2 p)) (proj2_sig (sig_of_sig2 p)) (proj3_sig p). Proof. destruct p; reflexivity. Defined. +(** [exists x : A, B] is equivalent to [inhabited {x : A | B}] *) +Lemma exists_to_inhabited_sig {A P} : (exists x : A, P x) -> inhabited {x : A | P x}. +Proof. + intros [x y]. exact (inhabits (exist _ x y)). +Qed. + +Lemma inhabited_sig_to_exists {A P} : inhabited {x : A | P x} -> exists x : A, P x. +Proof. + intros [[x y]];exists x;exact y. +Qed. + (** [sumbool] is a boolean type equipped with the justification of their value *) diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 07e8b6ef8..f1f20606b 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -760,6 +760,39 @@ Proof. destruct Heq using eq_indd; trivial. Qed. +(** Functional choice can be reformulated as a property on [inhabited] *) + +Definition InhabitedForallCommute_on (A : Type) (B : A -> Type) := + (forall x, inhabited (B x)) -> inhabited (forall x, B x). + +Notation InhabitedForallCommute := + (forall A (B : A -> Type), InhabitedForallCommute_on B). + +Theorem functional_choice_to_inhabited_forall_commute : + FunctionalChoice -> InhabitedForallCommute. +Proof. + intros choose0 A B Hinhab. + pose proof (non_dep_dep_functional_choice choose0) as choose;clear choose0. + assert (Hexists : forall x, exists _ : B x, True). + { intros x;apply inhabited_sig_to_exists. + refine (inhabited_covariant _ (Hinhab x)). + intros y;exists y;exact I. } + apply choose in Hexists. + destruct Hexists as [f _]. + exact (inhabits f). +Qed. + +Theorem inhabited_forall_commute_to_functional_choice : + InhabitedForallCommute -> FunctionalChoice. +Proof. + intros choose A B R Hexists. + assert (Hinhab : forall x, inhabited {y : B | R x y}). + { intros x;apply exists_to_inhabited_sig;trivial. } + apply choose in Hinhab. destruct Hinhab as [f]. + exists (fun x => proj1_sig (f x)). + exact (fun x => proj2_sig (f x)). +Qed. + (** ** Reification of dependent and non dependent functional relation are equivalent *) Definition DependentFunctionalRelReification_on (A:Type) (B:A -> Type) := |