Library hilbert.OldEpsilon

Set Implicit Arguments.

Definition ex_1 (A:Type)(P:A->Prop) :=
  ex (fun x:A => P x /\ forall y, P y -> x =y ).

Implicit Arguments ex_1 [A].


Lemma ex_1_introduction :
   forall (A:Type)(P:A->Prop),
    (exists a : A, P a) ->
    (forall a b, P a -> P b -> a = b)->
    ex_1 P.
Proof.
  intros A P Ex Un;case Ex;intros a Ha.
  exists a;repeat split;auto.
Qed.

Ltac ex_1_intro :=
    match goal with [ |- ex_1 ?P ] =>
        apply ex_1_introduction end.

Definition inhabited(A : Type):= sigT (fun t:A => True).

Definition inh_proj : forall A , (inhabited A) -> A.
 destruct 1 ; auto.
Defined.

Parameter epsilon : forall A : Type, A -> (A -> Prop) -> A.

An axiom for epsilon

Axiom epsax : forall A w a (P:A->Prop) , (P a) -> (P (epsilon w P)).

Epsilon elimination

Theorem epsilon_e : forall A i (P:A->Prop),
   ex P -> P (epsilon i P).
Proof.
 intros.
 case H.
 intros x Hx; apply epsax with x.
 assumption.
Qed.

Opaque epsilon.

Theorem epsilon_ind :
   forall (A:Type)(a: A)(P:A->Prop)
          (Q:A->Prop), ex P ->
                       (forall a : A, P a -> Q a) ->
                       Q (epsilon a P).
Proof.
 intros A a P Q exP P_Q.
 apply P_Q.
 apply epsilon_e.
 assumption.
Qed.

Theorem epsilon_equiv : forall (A:Type)(a: A)(P:A->Prop),
  ex P <-> P (epsilon a P).
Proof.
 split.
 intros; apply epsilon_ind; auto.
 exists (epsilon a P); auto.
Qed.

Lemma forall_def : (forall P, P \/ ~ P) ->
                    forall (A:Type)(a:A)(P:A->Prop),
                    (forall y, P y) <-> P (epsilon a (fun y => ~ (P y))).
Proof.
 intros class A a P; split.
 auto.
 intros H y .
 case (class (P y));auto.
 intro Hy.
 revert H.
 pattern (epsilon a (fun y0 : A => ~ P y0)).
 apply epsilon_ind;auto.
 exists y;auto.
 tauto.
Qed.


Definition iota (A:Type)(a : A)(P: A-> Prop) :=
   epsilon a (fun x => P x /\ forall y, P y -> x = y).

Lemma iota_e : forall (A:Type) (a: A) (P : A -> Prop),
                     (exists a, P a /\
                     forall b, P b -> a = b) ->
                     P (iota a P).
Proof.
 intros A a P H.
 unfold iota.
 apply epsilon_ind.
 auto.
 case H.
 intros.
 case H1;auto.
Qed.

Theorem iota_ind :
   forall (A:Type)(a: A)(P:A->Prop)
          (Q:A->Prop), (exists b:A, P b /\
                         (forall c:A, P c -> b = c)) ->
                       (forall b : A, P b -> Q b) ->
                       (Q (iota a P)).
Proof.
  intros.
  apply H0.
  apply iota_e;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 : forall (A:Type)(a b:A)(P:A-> Prop),
  (exists x :A, P x /\ (forall y : A, P y -> x = y)) ->
   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.
Qed.

Structures for descriptions and specifications

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

Definition some(A:Type)(a: A)(P:A->Prop)(pi:ex P)
  : A
  := epsilon a P.

Implicit Arguments some [A P].

Definition the (A:Type)(a: A)(P:A->Prop)
                       (pi:ex_1 P)
           : A
           := iota a P.

Implicit Arguments the [A P].

Lemma some_e : forall (A:Type)(a: A)(P:A->Prop)(pi:ex P),
                 P (some a pi).
Proof.
 intros.
 unfold some.
 epsilon_elim.
Qed.

Implicit Arguments some_e [A P].

Theorem some_ind :forall (A:Type)(a: A)(P Q:A->Prop)(pi:ex P),
                 (forall a, P a -> Q a) -> Q (some a pi).
Proof.
 intros.
 apply H;apply some_e.
Qed.

Theorem the_e : forall (A:Type)(a:A)(P:A->Prop)
                               (pi:ex_1 P),
  P (the a pi).
Proof.
 unfold the.
 intros.
 iota_elim.
Qed.

Implicit Arguments the_e [A P].

Theorem the_ind : forall (A:Type)(a: A)(P Q:A->Prop)
                               (pi:ex_1 P),
  (forall b, P b -> Q b) -> Q (the a pi).
Proof.
 intros A a P Q pi H;apply H;apply the_e.
Qed.

Implicit Arguments the_ind [A P].

Theorem the_rw : forall (A:Type)(a: A)(P:A->Prop)
                        (pi:ex_1 P) b,
                 P b -> b= the a pi.
Proof.
 intros A a P pi b Hb.
 case pi; intros x (Px,Eqx).

 unfold the.
 pattern (iota a P).
 iota_elim.
 intros.
 rewrite <- (Eqx b0).
 symmetry.
 auto.
 auto.
Qed.

Implicit Arguments the_rw [A P].

Ltac the_elim_aux :=
  match goal with [ |- (?Q (the ?w ?d))] =>
    apply the_ind   end.

Ltac the_elim := the_elim_aux ||
  match goal with [ |- (?P ?k)] =>
   (let v := eval cbv beta zeta delta [k] in k in
     (match v with (the ?w ?d) => change (P v); the_elim_aux end))
  end.

Ltac some_elim_aux :=
  match goal with [ |- (?P (some ?w ?d))] =>
    generalize (some w d) (some_e w d); simpl
  end.

Ltac some_elim := some_elim_aux ||
  match goal with [ |- (?P ?k)] =>
   (let v := eval cbv beta zeta delta [k] in k in
     (match v with (some ?w ?d) => change (P v); some_elim_aux end))
  end.

Ltac hilbert_e := epsilon_elim || iota_elim || some_elim || the_elim.

Ltac some_i P :=
   refine (some _ (P:=P) _).

Ltac the_i P :=
   refine (the _ (P:=P) _).

Building partial functions

Section AB_fixed.
 Variables A B: Type.

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

Definition choice_fun (b : B)(DA : A->Prop)(R:A->B->Prop)(a:A):=
      (epsilon b (fun (b':B) => DA a /\ R a b')).

Definition iota_fun (b : B)(DA : A->Prop)(R:A->B->Prop)(a:A):=
      (iota b (fun (b':B) => DA a /\ R a b')).

Lemma choice_fun_e : forall b : B,
  forall (DA : A->Prop)(R:A->B->Prop)(a:A),
   (exists d : B, R a d) ->
   DA a -> R a (choice_fun b DA R a).
Proof.
 intros.
 unfold choice_fun.
 pattern (epsilon b (fun b : B => DA a /\ R a b)).
 epsilon_elim.
 intros.
 case H;intuition.
 exists x;auto.
 tauto.
Qed.

Lemma choice_fun_ind : forall b : B,
  forall (P : A->Prop)(Q R:A->B->Prop)(a x:A),
   (exists d : B, R a d) -> a = x ->
   P a -> (forall b, P a -> R a b -> Q a b) ->
   Q x (choice_fun b 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 (b : B)(DA : A->Prop)(R:A->B->Prop)
       (pi : forall a, DA a -> ex_1 (R a)) (a:A):=
      (iota b (fun (b:B) => DA a /\ R a b)).

same stuff but without unicity of the result

Definition some_fun (b : B)(DA : A->Prop)(R:A->B->Prop)
       (pi : forall a, DA a -> exists b: B, R a b) (a:A):=
      (epsilon b (fun (b:B) => DA a /\ R a b)).

Lemma iota_fun_e : forall b : B,
  forall (DA : A->Prop)(R:A->B->Prop)(a:A),
   (ex_1 (R a)) ->
   DA a -> 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 H1; exists x;try tauto.
 split;auto.
 destruct 1;auto.
 tauto.
Qed.

Lemma iota_fun_ind : forall b : B,
  forall (P : A->Prop)(Q R:A->B->Prop)(a x:A),
   a = x -> (ex_1 (R a)) ->
   P a -> (forall b, P a -> 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').
 exists d;auto.
 auto.
Qed.

Lemma iota_fun_rw : forall b: B,
  forall (P : A->Prop)(R:A->B->Prop)(a:A)(b':B),
   (ex_1 ( 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.
 exists b';repeat split;auto.
 case H;intros d (Hd,Hd').
 intuition.
 transitivity d;auto.
 symmetry;auto.
  case H;intros d (Hd,Hd').
 destruct 1;auto.
  transitivity d;auto.
 symmetry;auto.
Qed.

Theorem the_fun_e : forall (b : B)(P: A-> Prop)(R:A->B->Prop)
(pi : forall a, P a -> ex_1 (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).
 exists x.
 split;auto.
 destruct 1;auto.
 tauto.
Qed.

Theorem some_fun_e : forall (b : B)(P: A-> Prop)(R:A->B->Prop)
(pi : forall a, P a -> exists b0: B, R a b0) (a:A),
      P a -> R a (some_fun b P R pi a) .
Proof.
 intros b P R pi a H.
 unfold some_fun.
 pattern (epsilon b (fun b0 : B => P a /\ R a b0)).
 epsilon_elim.
 case (pi a H).
 intros x Hx.
 exists x.
 split;auto.
 destruct 1;auto.
Qed.

Theorem the_fun_rw : forall (b : B)(P: A-> Prop)(R:A->B->Prop)
(pi : forall a, P a -> ex_1 ( 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.
 exists b0.
 repeat split;auto.

 case (pi a H).

 intros x (Hx,H'x) a' (Ha',Ha'').
 transitivity x.
 symmetry;auto.
 auto.
 destruct 1.
 case (pi a H).
 intros x (H3,H4).
 transitivity x;auto.
 symmetry;auto.
Qed.

Theorem the_fun_ind : forall (b : B)(P: A-> Prop)(Q R:A->B->Prop)
(pi : forall a, P a -> ex_1 (R a)) (a x:A),
      P a -> a = x ->
(forall b0, P a -> R a b0 -> Q a b0) -> Q x (the_fun b P R pi a) .
 intros.
 subst x.
 apply H1. auto. eapply the_fun_e.
 auto.
Qed.

Theorem some_fun_ind : forall (b : B)(P: A-> Prop)(Q R:A->B->Prop)
(pi : forall a, P a -> exists b: B, R a b) (a x:A),
      a = x -> P a -> (forall b0, P a -> R a b0 -> Q a b0) ->
      Q x (some_fun b P R pi a) .
 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 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'' : forall (A:Type)(B:A->Type)
                         (R:forall x:A, B x -> Prop),
      (forall x: A, (B x)) ->
      (sigT (fun f : forall x:A, B x =>
                     (forall x:A, (exists y:B x, R x y) -> R x (f x)))).
Proof.
 intros A B R i.
 exists (fun (x:A) => (epsilon (i x) (fun y => (R x y)))).
 intros x [y ry].
 apply (epsax (i x) y) ; trivial.
Qed.

Lemma dd' : forall (A:Type) (B:A -> Type)
                             (R:forall x:A, B x -> Prop),
      (forall x, (B x)) ->
      (forall x:A, exists y : B x, R x y ) ->
       sigT (fun f : forall x:A, B x => (forall x:A, R x (f x))).
Proof.
 intros.
 case (dd'' B R X).
 intros.
 exists x.
 intros;apply r.
 auto.
Qed.

End definite_description.

Lemma FunctionalChoice :
  forall (A B:Type) (R:A -> B -> Prop),
     B ->
    (forall x:A, exists y : B, R x y) ->
     exists f : A -> B, (forall x:A, R x (f x)).
Proof.
 intros A B R b H.
 exists (fun a:A => epsilon b (R a)).
 intros; pattern (epsilon b (R x)).
 hilbert_e.
 case (H x).
 intros y Hy;exists y;auto.
Qed.

Section quasi_classic.
 Variables A B : Prop.

 Let P := fun b:bool => A /\ (b=true) \/ B /\ ( b=false).

 Let x : bool := epsilon true P.

 Remark R0 : x=true -> B -> A.
 Proof.
   intros eg Hb.
   assert (P x).
   unfold x.
   epsilon_elim.
   exists false;red;auto.
    case H.
    tauto.
    rewrite eg;destruct 1;discriminate.
 Qed.

 Remark R1 : x=false -> A -> B.
 Proof.
   intros eg Ha.
   assert (P x).
   unfold x.
   epsilon_elim.
   exists true;red;auto.
    case H.
    rewrite eg;destruct 1;discriminate.
   tauto.
 Qed.

  Lemma arrow_disj : (A->B) \/ (B->A).
 Proof.
   generalize (refl_equal x).
   pattern x at -1 .
   case x; intro e.
   right;apply R0;auto.
  left;apply R1;auto.
 Qed.

End quasi_classic.

Lemma quasi_classic : forall (A:Prop), ~ A \/ ~~ A.
Proof.
   intros A.
   case (arrow_disj A (~A));tauto.
Qed.

Lemma or_to_sum : forall (A B : Prop), A \/ B -> {A}+{B}.
 intros A B H.
 pose (y := epsilon true (fun b => b=true /\ A \/ b=false /\ B)).
 case_eq y.
 intro eg.
 left.
 generalize eg;pattern y; hilbert_e.
  case H.
  exists true;auto.
  exists false;auto.
  destruct 1.
  tauto.
  case H0;intros; subst a; discriminate.
  intro eg;right.
  generalize eg;pattern y; hilbert_e.
  case H.
  exists true;auto.
  exists false;auto.
  destruct 1.
  intro; subst a.
  case H0. discriminate 1.
  tauto.
 Qed.

Lemma ex_to_sig : forall (A:Type)(a: A)(P : A -> Prop),
         ex P -> (sigT P).
Proof.
 intros.
 exists (epsilon a P).
 apply epsilon_ind;auto.
Qed.

Definition epsilon_extensionality :=
  forall (A:Type)(a: A)(P Q:A->Prop),
  (forall a, P a <-> Q a) ->
  epsilon a P = epsilon a Q.

Definition restricted_epsilon_extensionality :=
  forall (A:Type)(a: A)(P Q:A->Prop),
  (forall a0, P a0 <-> Q a0) ->
  ex P ->
  epsilon a P = epsilon a Q.

Section epsilon_extensionality.
 Hypothesis e_ext : restricted_epsilon_extensionality.

 Section LEMMA.

  Variable A: Type.


  Variable P : A-> Prop.

  Let Q (x:A)(y:bool) := y=false \/ P x.
  Let R (x:A)(y:bool) := y=true \/ P x.

  Let s (x:A) := epsilon true (Q x).
  Let t (x:A) := epsilon true (R x).


 Remark R00 : forall x, Q x (s x) /\ R x (t x).
 intro x;split.
  pattern (s x);epsilon_elim.
  exists false;left;auto.
  pattern (t x);epsilon_elim.
  exists true; left;auto.
 Qed.



 Remark R2 : forall x, P x -> (forall y, Q x y <-> R x y) -> s x = t x.
 Proof.
  intros; unfold s,t.
  apply e_ext.
  auto.
  exists false;red;auto.
 Qed.

 Remark R3 : forall x, P x -> s x = t x.
  intros;apply R2.
  auto.
  split ;right; auto.
 Qed.


 Remark R4 : forall x, (s x = false \/ P x) /\ (t x = true \/ P x).
 Proof.
  intro x; case (R00 x);unfold Q, R;tauto.
 Qed.


 Remark R5 : forall x, (s x = false /\ t x = true) \/ P x.
 intro x; case (R4 x);try tauto.
 Qed.

 Remark R6 : forall x, s x <> t x \/ P x.
 Proof.
  intro x; case (R5 x); auto.
  intros (e1,e2);left;rewrite e1;rewrite e2;discriminate.
 Qed.

 Remark R7 : forall x, s x <> t x -> ~ (P x).
 red;intros x ex Ax.
 case ex;apply R3;auto.
 Qed.

 Lemma Bells_lemma : forall x, P x \/ ~ (P x).
 Proof.
  intro x; case (R6 x).
  right;apply R7;assumption.
  auto.
 Qed.

 End LEMMA.

Lemma eps_extentional_exm : forall (P:Prop), P \/ ~P.
Proof.
 intro P.
 case (Bells_lemma (fun (b:bool)=> P) true);auto.
Qed.

Lemma eps_extensional_forall_def : forall (A:Type)(a:A)(P:A->Prop),
                    (forall y, P y) <-> P (epsilon a (fun y => ~ (P y))).
Proof.
 intros A a P; apply forall_def.
 apply eps_extentional_exm.
Qed.

Definition Prop_dec : forall P:Prop, {P}+{~P}.
  intro P.
  apply or_to_sum.
  apply eps_extentional_exm.
Qed.

End epsilon_extensionality.