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 definition find :
  86  ∀p:nat → bool.
  87   ∀l:list nat. sigma ? (λ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 ∧ p x = true ]).
  91 letin program ≝
  92  (λp.
  93   let rec aux l ≝
  94    match l with
  95     [ nil ⇒ raise_exn
  96     | cons x l ⇒ match p x with [ true ⇒ nat_return x | false ⇒ aux l ]
  97     ]
  98   in
  99    aux);
 100 apply
 101  (program : ∀p:nat → bool.
 102   ∀l:list nat. ∃res:option nat.
 103    match res with
 104     [ None ⇒ ∀y:nat. (mem nat eqb y l = true : Prop) → p y = false
 105     | Some (x:nat) ⇒ mem nat eqb x l = true ∧ p x = true ]);
 106 clear program;
 107  [ cases (aux l1); clear aux;
 108    simplify in ⊢ (match % in option return ? with [None⇒?|Some⇒?]);
 109    generalize in match H2; clear H2;
 110    cases a;
 111     [ simplify;
 112       intros 2;
 113       apply (eqb_elim y n);
 114        [ intros;
 115          autobatch
 116        | intros;
 117          apply H2;
 118          simplify in H4;
 119          exact H4
 120        ]
 121     | simplify;
 122       intros;
 123       cases H2; clear H2;
 124       split;
 125        [ elim (eqb n1 n);
 126          simplify;
 127          autobatch
 128        | assumption
 129        ]
 130     ]
 131  | unfold nat_return; simplify;
 132    split;
 133     [ rewrite > eqb_n_n;
 134       reflexivity
 135     | assumption
 136     ]
 137  | unfold raise_exn; simplify;
 138    intros;
 139    change in H1 with (false = true);
 140    destruct H1
 141  ]
 142 qed.