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.