Functional choice <-> [inhabited] and [forall] commute

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) :=