matita/tests/coercions_russell.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/test/russell/".
  16
  17 include "nat/orders.ma".
  18 include "list/list.ma".
  19 include "datatypes/constructors.ma".
  20
  21 inductive sigma (A:Type) (P:A → Prop) : Type ≝
  22  sig_intro: ∀a:A. P a → sigma A P.
  23
  24 interpretation "sigma" 'exists \eta.x =
  25   (cic:/matita/test/russell/sigma.ind#xpointer(1/1) _ x).
  26
  27 definition inject ≝ λP.λa:list nat.λp:P a. sig_intro ? P ? p.
  28
  29 coercion cic:/matita/test/russell/inject.con 0 1.
  30
  31 definition eject ≝ λP.λc: ∃n:list nat.P n. match c with [ sig_intro w _ ⇒ w].
  32
  33 coercion cic:/matita/test/russell/eject.con.
  34
  35 alias symbol "exists" (instance 2) = "exists".
  36 lemma tl : ∀l:list nat. l ≠ [] → ∃l1.∃a.a :: l1 = l.
  37 letin program ≝
  38   (λl:list nat. λH:l ≠ [].match l with [ nil ⇒ λH.[] | cons x l1 ⇒ λH.l1] H);
  39 letin program_spec ≝ (program : ∀l:list nat. l ≠ [] → ∃l1.∃a.a :: l1 = l);
  40  [ generalize in match H; cases l; [intros (h1); cases (h1 ?); reflexivity]
  41    intros; apply (ex_intro ? ? n); apply eq_f; reflexivity; ]
  42 exact program_spec;
  43 qed.
  44
  45 alias symbol "exists" (instance 3) = "exists".
  46 lemma tl2 : ∀l:∃l:list nat. l ≠ []. ∃l1.∃a.a :: l1 = l.
  47 letin program ≝
  48   (λl:list nat. match l with [ nil ⇒ [] | cons x l1 ⇒ l1]);
  49 letin program_spec ≝
  50   (program : ∀l:∃l:list nat. l ≠ []. ∃l1.∃a.a :: l1 = l);
  51   [ autobatch; | generalize in match H; clear H; cases s; simplify;
  52     intros; cases (H H1); ]
  53 exact program_spec.
  54 qed.
  55
  56 definition nat_return := λn:nat. Some ? n.
  57
  58 coercion cic:/matita/test/russell/nat_return.con.
  59
  60 definition raise_exn := None nat.
  61
  62 definition try_with :=
  63  λx,e. match x with [ None => e | Some (x : nat) => x].
  64
  65 lemma hd : list nat → option nat :=
  66   λl.match l with [ nil ⇒ raise_exn | cons x _ ⇒ nat_return x ].
  67
  68 axiom f : nat -> nat.
  69
  70 definition bind ≝ λf:nat->nat.λx.
  71   match x with [None ⇒ raise_exn| Some x ⇒ nat_return(f x)].
  72
  73 include "datatypes/bool.ma".
  74 include "list/sort.ma".
  75 include "nat/compare.ma".
  76
  77 definition inject_opt ≝ λP.λa:option nat.λp:P a. sig_intro ? P ? p.
  78
  79 coercion cic:/matita/test/russell/inject_opt.con 0 1.
  80
  81 definition eject_opt ≝ λP.λc: ∃n:option nat.P n. match c with [ sig_intro w _ ⇒ w].
  82
  83 coercion cic:/matita/test/russell/eject_opt.con.
  84
  85 (* we may define mem as in the following lemma and get rid of it *)
  86 definition find_spec ≝
  87   λl,p.λres:option nat.
  88    match res with
  89     [ None ⇒ ∀y. mem ? eqb y l = true → p y = false
  90     | Some x ⇒ mem ? eqb x l = true ∧
  91                p x = true ∧
  92                ∀y.mem ? eqb y l = true → p y = true → x ≠ y →
  93                     ∃l1,l2,l3.l = l1 @ [x] @ l2 @ [y] @ l3].
  94
  95 lemma mem_x_to_ex_l1_l2 : ∀l,x.mem ? eqb x l = true → ∃l1,l2.l = l1 @ [x] @ l2.
  96 intros 2; elim l (H hd tl IH H); [simplify in H; destruct H]
  97 generalize in match H; clear H;
  98 simplify; apply (eqb_elim x hd); simplify; intros;
  99 [1:clear IH; rewrite < H; apply (ex_intro ? ? []);
 100 |2:lapply(IH H1); clear H1 IH; decompose; rewrite > H2; clear H2]
 101 simplify; autobatch;
 102 qed.
 103
 104 definition if : ∀A:Type.bool → A → A → A ≝
 105  λA,b,t,f. match b with [ true ⇒ t | false ⇒ f].
 106
 107 notation < "'If' \nbsp b \nbsp 'Then' \nbsp t \nbsp 'Else' \nbsp f" for @{ 'if $b $t $f }.
 108 notation > "'If' b 'Then' t 'Else' f" for @{ 'if $b $t $f }.
 109 interpretation "if" 'if a b c = (cic:/matita/test/russell/if.con _ a b c).
 110
 111 definition sigma_find_spec : ∀p,l. sigma ? (λres.find_spec l p res).
 112 (* define the find function *)
 113 letin find ≝ (λp.
 114   let rec aux l ≝
 115     match l with
 116     [ nil ⇒ raise_exn
 117     | cons x l ⇒ If p x Then nat_return x Else aux l]
 118     in aux);
 119 (* manca una delta?! *) unfold if in find;
 120 apply (find: ∀p.∀l.sigma ? (λres.find_spec l p res)); clear find;
 121 (* l = x::tl ∧ p x = false *)
 122 [1: cases (aux l1); clear aux;
 123     generalize in match H2; clear H2; cases a; clear a; simplify;
 124     [1: intros 2; apply (eqb_elim y n); intros (Eyn); [rewrite > Eyn; assumption]
 125         apply H3; simplify in H2; assumption;
 126     |2: intros; decompose; repeat split; [2: assumption]; intros;
 127         [1: cases (eqb n1 n); simplify; autobatch;
 128         |2: generalize in match (refl_eq ? (eqb y n)); generalize in ⊢ (? ? ? %→?);
 129             intro; cases b; clear b; intro Eyn; rewrite > Eyn in H3; simplify in H3;
 130             [1: rewrite > (eqb_true_to_eq ? ? Eyn) in H6; rewrite > H1 in H6; destruct H6;
 131             |2: lapply H4; try assumption; decompose; clear H4; rewrite > H8;
 132                 simplify; autobatch depth = 4;]]]
 133 (* l = x::tl ∧ p x = true *)
 134 |2: unfold find_spec; unfold nat_return; simplify; repeat split; [2: assumption]
 135     [1: rewrite > eqb_n_n; reflexivity
 136     |2: intro; generalize in match (refl_eq ? (eqb y n)); generalize in ⊢ (? ? ? %→?);
 137         intro; cases b; clear b; intro Eyn; rewrite > Eyn;
 138         [1: rewrite > (eqb_true_to_eq ? ? Eyn);] clear Eyn; simplify; intros;
 139         [1: cases H4; reflexivity
 140         |2: lapply (mem_x_to_ex_l1_l2 ? ? H2); decompose; rewrite > H6;
 141             apply (ex_intro ? ? []); simplify; autobatch;]]
 142 (* l = [] *)
 143 |3: unfold raise_exn; simplify; intros; destruct H1;]
 144 qed.