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