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

2 files changed, 16 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 *)