Library Epsilon

Require Import ClassicalEpsilon.

Set Implicit Arguments.

Lemma ex_unique_introduction :
   ∀ (A:Type)(P:A→Prop),
    (∃ x, P x) →
    (∀ a b, P a → P b → a = b)->
    ∃! x, P x.
Proof.
intros.
case (unique_existence P).
destruct 1.
split;auto.
case H;intros x0 Hx0.
∃ x0;auto.
case H1.
split;auto.
Qed.

Ltac ex_unique_intro :=
    match goal with [ |- ex (unique ?P) ] ⇒
       apply ex_unique_introduction end.

Theorem epsilon_ind :
   ∀ (A:Type)(i : inhabited A)(P:A→Prop)
          (Q:A→Prop), (∃ x, P x)->
                       (∀ x : A, P x → Q x) →
                       Q (epsilon i P).
Proof.
intros A a P Q exP P_Q.
apply P_Q.
  apply epsilon_spec; assumption.
Qed.

Theorem epsilon_equiv : ∀ (A:Type)(i : inhabited A)(P:A→Prop),
  (∃ x, P x )<-> P (epsilon i P).
Proof.
split.
intros; apply epsilon_ind; auto.
∃ (epsilon i P); auto.
Qed.

Definition tau (A:Type)(i:inhabited A)(P:A→Prop) :=
     epsilon i (fun y ⇒ ¬ (P y )).

Lemma forall_def : (∀ P, P ∨ ¬ P) →
                    ∀ (A:Type)(i:inhabited A)(P:A→Prop),
                    (∀ y, P y ) ↔ P (tau i P).
Proof.
intros class A a P; split.
auto.
intros H y .
case (class (P y));auto.
intro Hy.
revert H.
pattern (tau a P).
unfold tau;apply epsilon_ind;auto.
∃ y;auto.
tauto.
Qed.

Definition iota (A:Type)(i : inhabited A)(P: A→ Prop) : A :=
epsilon i (unique P).

Lemma iota_e : ∀ (A:Type) (i: inhabited A) (P : A → Prop),
                     ex (unique P) →
                     unique P (iota i P).
Proof.
intros A a P H; unfold iota.
apply epsilon_ind;auto.
Qed.

Lemma iota_e_weak : ∀ (A:Type) (i: inhabited A) (P : A → Prop),
                     ex (unique P) →
                      P (iota i P).
Proof.
intros.
case (iota_e i H).
auto.
Qed.

Theorem iota_ind :
   ∀ (A:Type)(i: inhabited A)(P:A→Prop)
          (Q:A→Prop),
                      (∀ b : A, unique P b → Q b) →
                       ex (unique P) →
                       Q (iota i P).
Proof.
  intros A a P Q H (x,H0).
apply H.
apply iota_e.
  ∃ x;auto.
Qed.

Theorem iota_ind_weak : ∀ (A:Type)(i: inhabited A)(P:A→Prop)
          (Q:A→Prop),
              (∀ b : A, P b → Q b) →
              ex (unique P) →
              Q (iota i P).
Proof.
intros.
apply H.
apply iota_e_weak.
auto.
Qed.

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.

Ltac iota_elim_aux :=
  match goal with [ |- (?P (iota (A:=?X) ?i ?Q))] ⇒
    apply iota_ind; auto
  end.

Ltac iota_elim := iota_elim_aux ||
  match goal with
  [ |- (?P (?k ?arg))] ⇒
   (let v := eval cbv zeta beta delta [k] in (k arg) in
     (match v with (iota ?w ?d) ⇒ change (P v); iota_elim_aux end))
| [ |- (?P (?k ?arg ?arg1))] ⇒
   (let v := eval cbv zeta beta delta [k] in (k arg arg1) in
     (match v with (iota ?w ?d) ⇒ change (P v); iota_elim_aux end))
| [ |- (?P ?k)] ⇒
   (let v := eval cbv zeta beta delta [k] in k in
     (match v with (iota ?w ?d) ⇒ change (P v); iota_elim_aux end))
  end.

Lemma iota_parameter_rw : ∀ (A:Type)(a b:inhabited A)(P:A→ Prop),
  (ex (unique P)) →
   iota a P = iota b P.
Proof.
intros.
pattern (iota a P).
iota_elim.
pattern (iota b P).
iota_elim.
intros b0 H0 b1 H1.
revert H;intros (x,(Hx,H')).
transitivity x;auto.
symmetry;auto.
red in H1;decompose [and] H1.

auto.
  red in H0;decompose [and] H0.
auto.

Qed.

Structures for descriptions and specifications

The operators "some" and "the" correspond to epsilon and iota applied to the proof they expect

Definition select(A:Type)(P:A→Prop)(pi:∃ x, P x)
  : A
  := proj1_sig (constructive_indefinite_description P pi).

Implicit Arguments select [A P].

Definition select_the (A:Type)(P:A→Prop)
                      (pi:∃! x, P x)
           : A
           := proj1_sig (constructive_indefinite_description (unique P) pi).

Implicit Arguments select_the [A P].

Lemma select_e : ∀ (A:Type)(P:A→Prop)(pi:∃ x, P x),
                 P (select pi).
Proof.
intros.
unfold select.
case (constructive_indefinite_description P pi).
auto.
Qed.

Implicit Arguments select_e [A P].

Theorem select_ind :∀ (A:Type)(P Q:A→Prop)
                 (pi:∃ x, P x),
                 (∀ a, P a → Q a) → Q (select pi).
Proof.
intros.
apply H ;apply select_e.
Qed.

Theorem select_the_e : ∀ (A:Type)(P:A→Prop)
                               (pi:∃! x, P x),
  unique P (select_the pi).
Proof.
unfold select_the.
intros.
case (constructive_indefinite_description (unique P) pi);auto.
Qed.

Implicit Arguments select_the_e [A P].

Theorem select_the_ind : ∀ (A:Type)(P Q:A→Prop)
                               (pi:ex (unique P)),
  (∀ b, unique P b → Q b) → Q (select_the pi).
Proof.
intros A P Q pi H;apply H. apply select_the_e.
Qed.

Implicit Arguments select_the_ind [A P].

Theorem select_the_rw : ∀ (A:Type)(P:A→Prop)
                        (pi:∃! x, P x) b,
                 P b → b = select_the pi.
Proof.
intros A P pi b Hb.
case pi; intros x (Px,Eqx).

unfold select_the.
  case (constructive_indefinite_description (unique P)
        (ex_intro (unique (fun x0 : A ⇒ P x0)) x (conj Px Eqx))).
simpl;firstorder.
Qed.

Implicit Arguments select_the_rw [A P].

Ltac select_the_elim_aux :=
  match goal with [ |- (?Q (select_the ?d))] ⇒
    apply select_the_ind
  end.

Ltac select_the_elim := select_the_elim_aux ||
  match goal with [ |- (?P ?k)] ⇒
   (let v := eval cbv beta zeta delta [k] in k in
     (match v with (select_the ?d) ⇒ change (P v); select_the_elim_aux end))
  end.

Ltac select_elim_aux :=
  match goal with [ |- (?P (select ?d))] ⇒
    generalize (select d) (select_e d); simpl
  end.

Ltac select_elim := select_elim_aux ||
  match goal with [ |- (?P ?k)] ⇒
   (let v := eval cbv beta zeta delta [k] in k in
     (match v with (select ?d) ⇒ change (P v); select_elim_aux end))
  end.

Ltac hilbert_e :=
select_the_elim || select_elim || iota_elim || epsilon_elim .

Tactic Notation "epsilon_e" constr(T) "at" integer(n) :=
       pattern T at n; hilbert_e.

Tactic Notation "epsilon_e" constr(T) :=
       pattern T ; hilbert_e.

Ltac select_i P :=
   refine (select (P:=P) _).

Ltac select_the_i P :=
   refine (select_the (P:=P) _).

Building partial functions

Definition functional(A B : Type) (R: A → B → Prop ) :=
∀ x y , R x y → ∀ z, R x z → y = z.

Implicit Arguments functional [A B].

Section AB_fixed.
Variables A B: Type.

description of some partial function by a Domain and a binary relation

Definition choice_fun (i : inhabited B)(DA : A→Prop)(R:A→B→Prop)(a:A):=
      (epsilon i (fun (b':B) ⇒ DA a ∧ R a b')).

Definition iota_fun (b : inhabited B)(DA : A→Prop)(R:A→B→Prop)(a:A):=
      (iota b (fun (b':B) ⇒ DA a ∧ R a b')).

Lemma choice_fun_e : ∀ i : inhabited B,
  ∀ (DA : A→Prop)(R:A→B→Prop)(a:A),
   (∃ d : B , R a d) →
   DA a → R a (choice_fun i DA R a).
Proof.
intros.
unfold choice_fun.
pattern (epsilon i (fun b : B ⇒ DA a ∧ R a b)).
epsilon_elim.
intros.
case H;intuition.
∃ x;auto.
tauto.
Qed.

Lemma choice_fun_ind : ∀ i : inhabited B,
  ∀ (P : A→Prop)(Q R:A→B→Prop)(a x:A),
   (∃ d : B , R a d) → a = x →
   P a → (∀ b, P a → R a b → Q a b) →
   Q x (choice_fun i P R a).
Proof.
intros.
subst x.
apply H2.
auto. apply choice_fun_e;auto.
Qed.

a partial function equipped with a proof of its partial correctness

Definition the_fun (i : inhabited B)(D : A→Prop)(R:A→B→Prop)
(pi : ∀ a, D a → ∃! b, R a b): A → B :=
fun a:A ⇒ iota i (fun (b:B) ⇒ D a ∧ R a b).

same stuff but without unicity of the result

Definition some_fun (i : inhabited B)(D : A→Prop)(R:A→B→Prop)
       (pi : ∀ a, D a → ∃ b: B , R a b) : A → B :=
      fun a:A ⇒ epsilon i (fun (b:B) ⇒ D a ∧ R a b).

Lemma iota_fun_e : ∀ b : inhabited B,
  ∀ (DA : A→Prop)(R:A→B→Prop)(a:A),
   (ex (unique (R a))) →
   DA a → unique (R a) (iota_fun b DA R a).
Proof.
intros.
unfold iota_fun.
pattern (iota b (fun b' : B ⇒ DA a ∧ R a b')).
iota_elim.
case H;intros.
case H2; auto.
case H;intros.
case H4;auto.
case H;intros.
split.
auto.
intros.
case H6.
firstorder.
case H.
intros x (e,u). ∃ x.
split;auto.
firstorder.
Qed.

Lemma iota_fun_ind : ∀ b : inhabited B,
  ∀ (P : A→Prop)(Q R:A→B→Prop)(a x:A),
   a = x → (ex (unique (R a))) →
   P a → (∀ b, P a → unique (R a) b → Q a b) →
   Q x (iota_fun b P R a).
Proof.
intros.
subst x.
apply H2.
auto. apply iota_fun_e.
case H0;intros d (Hd,Hd').
∃ d;auto.
auto.
red.
auto.
auto.
Qed.

Lemma iota_fun_rw : ∀ b: inhabited B,
  ∀ (P : A→Prop)(R:A→B→Prop)(a:A)(b':B),
   (ex (unique ( R a))) →
   P a →
   R a b' → b'= (iota_fun b P R a ).
Proof.
intros.
  unfold iota_fun.
  pattern (iota b (fun b0 : B ⇒ P a ∧ R a b0)).
iota_elim.
   case H;intros d (Hd,Hd').
intuition.
transitivity d;auto.
symmetry;auto.
  red in H2.
firstorder.
firstorder.
Qed.

Theorem the_fun_e : ∀ (b :inhabited B)(P: A→ Prop)(R:A→B→Prop)
(pi : ∀ a, P a → ex (unique (R a))) (a:A),
      P a → R a (the_fun b P R pi a) .
Proof.
intros b P R pi a H.
unfold the_fun.
pattern (iota b (fun b0 : B ⇒ P a ∧ R a b0)).
iota_elim.
case (pi a H).
intros x (Hx,H'x).
firstorder.
firstorder.
Qed.

Theorem some_fun_e : ∀ (i : inhabited B)(P: A→ Prop)(R:A→B→Prop)
(pi : ∀ a, P a → ∃ b0: B , R a b0) (a:A),
      P a → R a (some_fun i P R pi a) .
Proof.
intros i P R pi a H.
unfold some_fun.
pattern (epsilon i (fun b0 : B ⇒ P a ∧ R a b0)).
epsilon_elim.
case (pi a H).
intros x Hx.
∃ x.
split;auto.
destruct 1;auto.
Qed.

Theorem the_fun_rw : ∀ (b : inhabited B)(P: A→ Prop)(R:A→B→Prop)
(pi : ∀ a, P a → ex (unique ( R a))) (a:A)(b0:B),
      P a → R a b0 → b0 = (the_fun b P R pi a ) .
Proof.
intros b P R pi a b0 H H0.
unfold the_fun.
pattern (iota b (fun b1 : B ⇒ P a ∧ R a b1)).
iota_elim.
firstorder.
case (pi a H).

intros x (Hx,H'x).
∃ x.
firstorder.
Qed.

Theorem the_fun_ind : ∀ (b : inhabited B)(P: A→ Prop)(Q R:A→B→Prop)
(pi : ∀ a, P a → ex (unique (R a))) (a x:A),
      P a → a = x →
(∀ b0, P a → unique (R a) b0 → Q a b0) →
Q x (the_fun b P R pi a) .
Proof.
intros.
subst x.
apply H1. auto.
case (pi a H).
destruct 1.
split.
eapply the_fun_e.
auto.
intros.
replace x' with x.
symmetry;apply (the_fun_rw b P R pi a);auto.
auto.
Qed.

Theorem some_fun_ind : ∀ (i : inhabited B)(P: A→ Prop)(Q R:A→B→Prop)
(pi : ∀ a, P a → ∃ b: B , R a b) (a x:A),
      a = x → P a → (∀ b0, P a → R a b0 → Q a b0) →
      Q x (some_fun i P R pi a) .
Proof.
intros.
subst x.
apply H1. auto. eapply some_fun_e.
auto.
Qed.

End AB_fixed.

tactic for building a partial function

Opaque the_fun some_fun.

Ltac the_fun_i P R:=
   refine (the_fun _ P R _).

Ltac some_fun_i P R:=
   refine (some_fun _ P R _).

Ltac the_fun_elim :=
match goal with [ |- (?Q ?a (?f ?t)) ] ⇒
(let v := eval cbv beta zeta delta [f] in f in
       (match v with (the_fun ?i ?P ?R ?d) ⇒ change (Q a (v t));
                 apply the_fun_ind ; auto end)) end.

Ltac some_fun_elim :=
match goal with [ |- (?Q ?a (?f ?t)) ] ⇒
(let v := eval cbv beta zeta delta [f] in f in
       (match v with (some_fun ?i ?P ?R ?d) ⇒ change (Q a (v t));
                 apply some_fun_ind ; auto end)) end.

Ltac iota_fun_elim :=
match goal with [ |- (?Q ?a (?f ?t)) ] ⇒
(let v := eval cbv beta zeta delta [f] in f in
       (match v with (iota_fun ?i ?P ?R ) ⇒ change (Q a (v t));
                 apply iota_fun_ind ; auto end)) end.

Ltac choice_fun_elim :=
match goal with [ |- (?Q ?a (?f ?t)) ] ⇒
(let v := eval cbv beta zeta delta [f] in f in
       (match v with (choice_fun ?i ?P ?R ) ⇒ change (Q a (v t));
                 apply choice_fun_ind ; auto end)) end.

Ltac pfun_e := choice_fun_elim || iota_fun_elim || some_fun_elim ||
              the_fun_elim.

Ltac partial_fun_e arg result := pattern arg, result;pfun_e.

Ltac iota_fun_rewrite :=
match goal with [ |- (?f ?x = ?y) ] ⇒
    (let v := eval cbv beta zeta delta [f] in f in
           (match v with (iota_fun ?i ?P ?R ) ⇒
                         change (v x = y);symmetry; apply iota_fun_rw; auto
                          end)) end.

Ltac the_fun_rewrite :=
match goal with [ |- (?f ?x = ?y) ] ⇒
    (let v := eval cbv beta zeta delta [f] in f in
           (match v with (the_fun ?i ?P ?R ?d ) ⇒
                         change (v x = y);symmetry; apply the_fun_rw; auto
                          end)) end.

Section definite_description.

Lemma dd'' : ∀ (A:Type)(B:A→Type)
                         (R:∀ x:A, B x → Prop),
      (∀ x: A, inhabited (B x)) →
      (sigT (fun f : ∀ x:A, B x ⇒
                     (∀ x:A, (∃ y:B x , R x y) → R x (f x)))).
Proof.
intros A B R i.
∃ (fun (x:A) ⇒ (epsilon (i x) (fun y ⇒ (R x y)))).
intros x [y ry].
apply (epsilon_ind). ∃ y; trivial.
auto.
Qed.

Lemma dd' : ∀ (A:Type) (B:A → Type)
                             (R:∀ x:A, B x → Prop),
      (∀ x, inhabited (B x)) →
      (∀ x:A, ∃ y : B x , R x y ) →
       sigT (fun f : ∀ x:A, B x ⇒ (∀ x:A, R x (f x))).
Proof.
intros.
case (dd'' B R H).
intros.
∃ x.
intros;apply r.
auto.
Qed.

End definite_description.

Definition epsilon_extensionality :=
  ∀ (A:Type)(i: inhabited A)(P Q:A→Prop),
  (∀ a, P a ↔ Q a) →
  epsilon i P = epsilon i Q.

Definition restricted_epsilon_extensionality :=
  ∀ (A:Type)(i: inhabited A)(P Q:A→Prop),
  (∀ a, P a ↔ Q a) →
  ex P →
  epsilon i P = epsilon i Q.

Lemma inhabited_bool : inhabited bool.
constructor.
exact true.
Qed.

Lemma or_to_sumbool : ∀ P Q : Prop, P ∨ Q → {P }+{Q }.
Proof.
intros P Q H.
pose (y := epsilon inhabited_bool (fun b ⇒ b =true ∧ P ∨ b =false ∧ Q)).
case_eq y.
intro eg.
left.
generalize eg;pattern y; hilbert_e.
  case H.
  ∃ true;auto.
  ∃ false;auto.
  destruct 1.
  tauto.
  case H0;intros; subst x; discriminate.
  intro eg;right.
  generalize eg;pattern y; hilbert_e.
  case H.
  ∃ true;auto.
  ∃ false;auto.
  destruct 1.
  intro; subst x.
  case H0. discriminate 1.
  tauto.
Qed.

Lemma iota_rw : ∀ (A:Type)(a: inhabited A)(P:A→Prop)(x:A),
              unique P x →
              iota a P = x.
Proof.
intros.
case H ;intros H1 H2.
symmetry;apply H2;auto.
epsilon_e (iota a P).
firstorder.
∃ x;firstorder.
Qed.

Opaque epsilon.

Definition unspec (A:Type)(i:inhabited A) := epsilon i (fun x ⇒ True).

Lemma quasi_classic : ∀ (A:Type), A + (A→False ).
Proof.
intro A;case (or_to_sumbool (classic (inhabited A))).
intro i; left;exact (epsilon i (fun a ⇒True)).
intro H;right;intro a.
case H.
constructor.
auto.
Qed.