Library hydras.Schutte.MoreEpsilonIota
From Coq Require Export Ensembles Logic.Epsilon.
Print epsilon_statement.
Print epsilon.
Check constructive_indefinite_description.
Check iota_statement.
Print iota.
Print iota_spec.
Set Implicit Arguments.
Arguments In {U} _ _.
Lemma epsilon_ind {A:Type} (inh : inhabited A) (P Q : A → Prop):
(ex P ) → (∀ a, P a → Q a) → Q (epsilon inh P).
Theorem epsilon_equiv {A:Type}(a: inhabited A)(P:A→Prop):
(ex P)<-> P (epsilon a P).
Ltac epsilon_elim_aux :=
match goal with [ |- (?P (epsilon (A:=?X) ?a ?Q))] ⇒
apply epsilon_ind; auto
end.
Ltac epsilon_elim := epsilon_elim_aux ||
match goal with
[ |- (?P (?k ?d))] ⇒
(let v := eval cbv zeta beta delta [k] in (k d) in
(match v with (epsilon ?w ?d) ⇒ change (P v); epsilon_elim_aux end))
| [ |- (?P (?k ?arg ?arg1))] ⇒
(let v := eval cbv zeta beta delta [k] in (k arg arg1) in
(match v with (epsilon ?w ?d) ⇒ change (P v); epsilon_elim_aux end))
| [ |- (?P ?k)] ⇒
(let v := eval cbv zeta beta delta [k] in k in
(match v with (epsilon ?w ?d) ⇒ change (P v); epsilon_elim_aux end))
end.
Section On_Iota.
Variables (A:Type)(P: A → Prop).
Hypothesis inhA : inhabited A.
Hypothesis unique_P : ∃ ! x, P x.
Lemma iota_spec_1 : unique P (iota inhA P).
Lemma iota_eq : ∀ a, P a → a = iota inhA P.
Lemma iota_ind (Q:A → Prop) :
(∀ a, unique P a → Q a) → Q (iota inhA P).
End On_Iota.
Ltac iota_elim :=
match goal with |- context c [(iota ?b ?P)] ⇒
apply iota_ind end.
Class InH (A: Type) : Prop :=
InHWit : inhabited A.
Definition some {A:Type} {H : InH A} (P: A → Prop)
:= epsilon (@InHWit A H) P.
Definition the {A:Type} {H : InH A} (P: A → Prop)
:= iota (@InHWit A H) P.
#[ global ] Instance inhNat : InH nat.
Qed.
A small example