Library Coqtail.Fresh.Inhabited.Examples

Require Import Monad.

Lemma ex_inhabited_sig : ∀ A (f : A → Prop), ex f → [ sig f ].
Proof.
intros A f Hex.
destruct Hex as (x, fx).
constructor.
∃ x.
apply fx.
Qed.

Lemma ex_is_inhabited_sig A (f : A → Prop) : ex f ↔ [ sig f ].
Proof.
split; repeat intros []; eauto.
Qed.

Lemma Prop_inhabited_stable : ∀ P : Prop, P → [P].
Proof.
auto.
Qed.

Lemma Prop_inhabited_inversion : ∀ P : Prop, [P] → P.
Proof.
intros ? []; apply id.
Qed.

Lemma Type_inhabited_stable : ∀ P : Type, P → [P].
Proof.
auto.
Qed.

Definition epsilon := ∀ (A : Type) (f : A → Prop), (∃ x, f x) → { x | f x }.

Definition algebraic := ∀ P : Type, [ P ] → P.

Lemma Type_inhabited_inversion_implies_epsilon : algebraic → epsilon.
Proof.
intros Hs A f Hex.
apply Hs.
apply ex_inhabited_sig; assumption.
Qed.

Require Import InhabitedTactics.

Lemma unlift_example : ∀ (P Q : Type) (R : Prop), [ P ] → [ P → Q ] → [ Q → R ] → R.
Proof.
intros P Q R p pq qr.
unlift.
tauto.
Qed.

Lemma unlift_example2 : ∀ (P Q R : Type), [ P ] → [ P → Q ] → [ Q → R ] → [ R ].
Proof.
intros P Q R p pq qr.
unlift.
tauto.
Qed.

Lemma unlift_example3 : ∀ (P Q R : Type), [ P ] → [ P → Q ] → [ Q → R ] → R.
Proof.
intros P Q R p pq qr.
intuition.
Admitted.

Lemma stronger_inhabited_in_hypothese : ∀ A B, ([A] → [B]) → (A → [B]).
Proof.
eauto.
Qed.

Definition not (A : Type) : Type := A → False.


Lemma stronger_inhabited_in_hypothese' :
  (∀ A B, (A → [B]) → ([A] → [B])) →
  True .
Proof.
intros HH.
apply I.
Qed.

Lemma inhabited_sum_or : ∀ (A B : Type) (P : Prop),
 (([A] ∨ [B]) → P) ↔ ((A + B) → P).
Proof.
intros; split.
  intuition.
  intros ? [ [ ] | [ ] ]; auto.
Qed.