helm/software/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
  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/tests/coercions_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/tests/coercions_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/tests/coercions_russell/eject.con.
  34
  35 alias symbol "exists" (instance 2) = "exists".
  36 lemma tl : ∀l:list nat. l ≠ [] → ∃l1.∃a.a :: l1 = l.
  37  apply rule (λl:list nat. λ_.match l with [ nil ⇒ [] | cons x l1 ⇒ l1]);
  38   [ exists; [2: reflexivity | skip]
  39   | destruct; elim H; reflexivity]
  40 qed.
  41
  42 alias symbol "exists" (instance 3) = "exists".
  43 lemma tl2 : ∀l:∃l:list nat. l ≠ []. ∃l1.∃a.a :: l1 = l.
  44 apply rule (λl:list nat. match l with [ nil ⇒ [] | cons x l1 ⇒ l1]);
  45 [ autobatch;
  46 | cases s in H; simplify; intros; cases (H H1); ]
  47 qed.
  48
  49 definition nat_return := λn:nat. Some ? n.
  50
  51 coercion cic:/matita/tests/coercions_russell/nat_return.con.
  52
  53 definition raise_exn := None nat.
  54
  55 definition try_with :=
  56  λx,e. match x with [ None => e | Some (x : nat) => x].
  57
  58 lemma hd : list nat → option nat :=
  59   λl.match l with [ nil ⇒ raise_exn | cons x _ ⇒ nat_return x ].
  60
  61 axiom f : nat -> nat.
  62
  63 definition bind ≝ λf:nat->nat.λx.
  64   match x with [None ⇒ raise_exn| Some x ⇒ nat_return(f x)].
  65
  66 include "datatypes/bool.ma".
  67 include "list/sort.ma".
  68 include "nat/compare.ma".
  69
  70 definition inject_opt ≝ λP.λa:option nat.λp:P a. sig_intro ? P ? p.
  71
  72 coercion cic:/matita/tests/coercions_russell/inject_opt.con 0 1.
  73
  74 definition eject_opt ≝ λP.λc: ∃n:option nat.P n. match c with [ sig_intro w _ ⇒ w].
  75
  76 coercion cic:/matita/tests/coercions_russell/eject_opt.con.
  77
  78 (* we may define mem as in the following lemma and get rid of it *)
  79 definition find_spec ≝
  80   λl,p.λres:option nat.
  81    match res with
  82     [ None ⇒ ∀y. mem ? eqb y l = true → p y = false
  83     | Some x ⇒ mem ? eqb x l = true ∧
  84                p x = true ∧
  85                ∀y.mem ? eqb y l = true → p y = true → x ≠ y →
  86                     ∃l1,l2,l3.l = l1 @ [x] @ l2 @ [y] @ l3].
  87
  88 lemma mem_x_to_ex_l1_l2 : ∀l,x.mem ? eqb x l = true → ∃l1,l2.l = l1 @ [x] @ l2.
  89 intros 2; elim l (H hd tl IH H); [simplify in H; destruct H]
  90 generalize in match H; clear H;
  91 simplify; apply (eqb_elim x hd); simplify; intros;
  92 [1:clear IH; rewrite < H; apply (ex_intro ? ? []);
  93 |2:lapply(IH H1); clear H1 IH; decompose; rewrite > H2; clear H2]
  94 simplify; autobatch;
  95 qed.
  96
  97 notation > "'If' b 'Then' t 'Else' f" non associative
  98 with precedence 90 for @{ match $b with [ true ⇒ $t | _ ⇒ $f ] }.
  99
 100 alias symbol "exists" = "sigma".
 101 definition sigma_find_spec : ∀p,l. ∃res.find_spec l p res.
 102 apply rule (λp.
 103   let rec aux l ≝
 104     match l with
 105     [ nil ⇒ raise_exn
 106     | cons x l ⇒ If p x Then nat_return x Else aux l]
 107     in aux);
 108 (* l = x::tl ∧ p x = false *)
 109 [1: cases (aux l1); clear aux;
 110     cases a in H2; simplify;
 111     [1: intros 2; apply (eqb_elim y n); intros (Eyn); autobatch;
 112     |2: intros; decompose; repeat split; [2: assumption]; intros;
 113         [1: cases (eqb n1 n); simplify; autobatch;
 114         |2: generalize in match (refl_eq ? (eqb y n));
 115             generalize in ⊢ (? ? ? %→?);
 116             intro; cases b; clear b; intro Eyn; rewrite > Eyn in H3; simplify in H3;
 117             [1: rewrite > (eqb_true_to_eq ? ? Eyn) in H6; rewrite > H1 in H6; destruct H6;
 118             |2: lapply H4; try assumption; decompose; clear H4; rewrite > H8;
 119                 simplify; autobatch depth = 4;]]]
 120 (* l = x::tl ∧ p x = true *)
 121 |2: unfold find_spec; unfold nat_return; simplify; repeat split; [2: assumption]
 122     [1: rewrite > eqb_n_n; reflexivity
 123     |2: intro; generalize in match (refl_eq ? (eqb y n)); generalize in ⊢ (? ? ? %→?);
 124         intro; cases b; clear b; intro Eyn; rewrite > Eyn;
 125         [1: rewrite > (eqb_true_to_eq ? ? Eyn);] clear Eyn; simplify; intros;
 126           [1: cases H4; reflexivity
 127           |2: lapply (mem_x_to_ex_l1_l2 ? ? H2); decompose; rewrite > H6;
 128               apply (ex_intro ? ? []); simplify; autobatch;]]
 129 (* l = [] *)
 130 |3: unfold raise_exn; simplify; intros; destruct H1;]
 131 qed.