Library hilbert.Epsilon_Examples

Require Import Epsilon.
Require Import PartialFun.

examples
Require Import Arith.
Require Import Omega.

Notation eps_nat := (epsilon 0).

Definition some_positive := eps_nat (fun n:nat => 0 < n).

Lemma one_le_some_positive : 1 <= some_positive.
Proof.
 pattern some_positive.
 hilbert_e.
 exists 1515; auto with arith.
Qed.

Ltac descr_e cst := pattern cst; hilbert_e.

Lemma one_le_some_positive2 : 1 <= some_positive.
Proof.
 descr_e some_positive.
 exists 42;auto with arith.
Qed.

Notation iota_nat := (iota 0).

Definition zero := iota_nat (fun n:nat => forall p, n <= p).

Lemma zero_eq_0 : zero=0.
Proof.
 descr_e zero;auto.
 exists 0;auto with arith.
 intros;apply le_antisym;auto with arith.
Qed.

Definition two : nat.
 the_i (fun n : nat => 1 < n < 3);auto.
 exact 0.
exists 2; split;auto with arith.
 intros;omega.
Defined.

Lemma L_two_2 :two=2.
 descr_e two.
 intros;omega.
Qed.

Lemma L_two_2' : two=2.
 unfold two;symmetry;apply the_rw.
 auto with arith.
Qed.

Definition bad_two : nat.
 some_i (fun n:nat => 1 <n).
 auto.
 exact 0.
exists 2; auto with arith.
Defined.

Goal bad_two=2.
 descr_e bad_two.
 Abort.

Definition ppred (n:nat) := iota_nat (fun p => S p = n).

Goal ppred 2 = 1.
Proof.
 descr_e (ppred 2).
 exists 1; split;auto.
 injection 1;auto.
Qed.

Goal 0 * (ppred 0) = 0.
 simpl.
 trivial.
Qed.

Goal ppred 0=0.
 descr_e (ppred 0).
Abort.


Definition pred2 : nat -> nat.
 the_fun_i (fun n :nat => 0<n)
           (fun n p : nat => p < n <= S p).
 auto.
 exact 0.
destruct a.
 inversion 1.
 exists a.
 split;auto with arith.
 intro x';destruct 1.
 omega.
Defined.

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

Lemma pred2_lt : forall a, 0 < a -> pred2 a < a.
Proof.
 intros.
 pf_e a (pred2 a).
 tauto.
Qed.

Lemma pred_42 : pred2 42 = 41.
 the_fun_rewrite.
 auto with arith.
Qed.

Lemma one_le_some_positive' : 1 <= some_positive*0 + some_positive.
Proof.
 h_elim some_positive.
 Restart.
 h_elim some_positive at 2.
 exists 42; auto with arith.
 rewrite mult_0_r.
 simpl.
 auto with arith.
Qed.

Definition some_lt : nat -> nat.
 some_fun_i (fun n :nat => 0 < n)
            (fun n p : nat => p < n ).
 auto.
  exact 0.
exists 0;auto.
Defined.

Goal forall n, 0 < n -> some_lt n < n.
Proof.
 intros.
 pattern n ,(some_lt n).
 pfun_e;auto.
Qed.

Definition my_pred := iota_fun 0 (fun n => 0 < n)
                                 (fun n p => S p = n).

Goal forall i, 0< i -> my_pred i < i.
Proof.
 intros.
 pattern i, (my_pred i).
 pfun_e.
 inversion H.
 exists 0;auto with arith.
 split;auto.
 injection 1;auto.
 exists m;auto with arith.
 split;auto.
 injection 1;auto.
 intros;subst i;auto with arith.
Qed.

Goal my_pred 42 = 41.
 iota_fun_rewrite.
 exists 41;split;auto with arith.
 injection 1;auto.
 auto with arith.
Qed.