Library Iota_examples
Require
Import
Iota.
Set Implicit
Arguments.
Require
Import
Arith.
Lemma
inh_nat : inhabited nat.
exists 0.
trivial.
Qed
.
Hint
Resolve inh_nat.
Axiom
epsi_nat : epsilonax inh_nat.
Hint
Resolve epsi_nat.
Lemma
iota_nat : iotax inh_nat.
Proof
.
auto.
Qed
.
Hint
Resolve iota_nat.
Definition
some_positive := epsilon inh_nat (fun n:nat => 0 < n).
Lemma
one_le_some_positive : 1 <= some_positive.
unfold some_positive.
apply epsilon_ind ; auto.
exists 1.
auto with arith.
Qed
.
Definition
positive_spec : choice inh_nat (fun n => 0 < n).
split ; auto.
exists 42; auto with arith.
Defined
.
Ltac
pattern_1 f := match goal with
[|- ?P ] =>
(match P with
context [(f ?t)] => pattern (f t) end) end.
Definition
a_positive_number : nat := some positive_spec.
Lemma
one_leq_positive : 1 <= a_positive_number.
pattern a_positive_number.
compute.
apply epsilon_ind;auto.
Print
positive_spec.
case positive_spec.
case positive_spec;auto.
Qed
.
Goal 42 = a_positive_number.
pattern a_positive_number.
epsilon_e.
Abort.
Definition
zero := iota inh_nat (fun n:nat => forall p, n <= p).
Lemma
zero_eq_0 : zero=0.
pattern zero.
iota_e; auto.
intros.
assert (n <= 0).
apply H.
exists 0;auto with arith.
intros;apply le_antisym;auto.
inversion H0.
auto.
Qed
.
Definition
zero_def : def inh_nat (fun n => forall p, n <= p).
def_tac .
auto.
exists 0;auto with arith.
intros;apply le_antisym;auto.
Defined
.
Goal (the zero_def =0).
pattern (the zero_def).
iota_e.
intros.
generalize (H 0);inversion 1;auto.
Save
zero_def_ok.
Remark
R0 : exists d, d < 1.
exists 0.
auto with arith.
Qed
.
Remark
R1 : forall d d', d < 1 -> d' < 1 -> d = d'.
inversion_clear 1.
inversion_clear 1;auto.
inversion H0.
inversion H0.
Qed
.
Definition
zero' : nat.
define inh_nat (fun n:nat => n < 1).
exact R0.
exact R1.
Defined
.
Goal zero'=0.
pattern zero'.
iota_e.
inversion 1 as [|H1 H2 H3] ;auto.
inversion H2.
Qed
.
Definition
is_pred (n p : nat) := S p = n.
Definition
is_pos (n:nat) := 0 < n.
Definition
my_pred := iota_fun inh_nat is_pos is_pred.
Goal my_pred 1 = 0.
pattern (my_pred 1).
iota_e.
red;auto with arith.
exists 0;red;auto with arith.
unfold is_pred.
intros.
rewrite <- H2 in H;injection H;auto.
red in H3.
injection H3;auto.
Qed
.
Definition
pred_defun : defun is_pos is_pred.
eapply Build_defun.
eexact iota_nat.
inversion 1.
exists 0.
red;auto.
exists m;auto.
subst d.
red;auto.
unfold is_pred.
destruct 2.
injection 1;auto.
Defined
.
Definition
my_pred' := the_fun pred_defun.
Lemma
my_pred_of_succ : forall n, my_pred' (S n)=n.
Proof
.
intros; pattern (my_pred' (S n)).
iota_e.
red;
auto with arith.
injection 1; auto.
Qed
.
Lemma
my_pred_is_pred : forall n:nat, 0< n -> my_pred n = pred n.
Proof
.
intro n; case n; simpl.
inversion 1.
intros; pattern (my_pred (S n0)).
iota_e.
exists n0;red;auto.
injection 1;auto.
injection 2;auto.
subst n0;auto.
injection H4.
auto.
Qed
.
Lemma
failure : my_pred 0 = 0.
Proof
.
pattern (my_pred 0).
iota_e.
red.
Abort.
Goal defined
(fun b : nat => 1 <= 2 /\ S b = 2)( my_pred 2).
unfold my_pred.
unfold iota_fun.
unfold is_pred.
split.
exists 1;split;auto with arith.
red;auto with arith.
intros a b (H1,H2) (H3,H4).
injection H2.
injection H4.
intro;subst b;auto.
Save
def_pred_2.
Goal not ( defined
(fun b : nat => 1 <= 0 /\ S b = 0)( my_pred 0)).
red.
inversion 1.
case H1.
intros x (Hx,_);inversion Hx.
Qed
.
Definition
pred' : nat -> nat.
fun_define inh_nat is_pos is_pred.
inversion 1.
exists 0.
red;auto.
exists m;auto.
subst d.
red;auto.
unfold is_pred.
destruct 2.
injection 1;auto.
Defined
.
Goal (pred' 1)=0.
pattern (pred' 1).
iota_e.
red;auto with arith.
inversion 1.
auto.
Qed
.
Definition
toujours_plus (n:nat) := epsilon inh_nat (fun p => n < p).
Check toujours_plus.
Goal forall n, n < toujours_plus n.
Proof
.
intro n.
unfold toujours_plus.
pattern (epsilon inh_nat (fun p : nat => n < p)).
epsilon_e.
intros.
apply H.
exists (S n);auto with arith.
Defined
.
Eval compute in (toujours_plus 6).
Definition
toujours_moins (n:nat) := epsilon inh_nat (fun p => p < n).
Lemma
bug : forall n, toujours_moins n < n.
Proof
.
intro n.
pattern (toujours_moins n).
epsilon_e.
intros.
apply H.
Abort.
Lemma
pas_bug : forall n, 0 < n -> toujours_moins n < n.
Proof
.
intro n;pattern (toujours_moins n).
epsilon_e.
intros.
apply H.
exists 0;auto.
Qed
.
Goal (2+3=5).
pattern (2+3).
match goal with [ |- (?P ?x)] =>
(match x with context G [plus] =>
let t := context G [plus]
in simpl t end) end.
cbv beta.
auto.
Qed
.
Definition
cf : choice_defun (fun n => 0 < n)
(fun n p => p < n).
esplit.
eauto.
exists 0;auto.
Defined
.
Definition
less := some_fun cf.
Goal less 4 < 4.
unfold less.
pattern (some_fun cf 4).
generalize (some_fun cf 4) (choice_defun_ok cf 4).
intros.
apply H;auto with arith.
Qed
.
Goal less 4 < 4.
pattern (less 4).
epsilon_e.
trivial.
Qed
.
Goal less 0 < 2.
pattern (less 0).
epsilon_e.
Abort.
Index
This page has been generated by coqdoc