matita/tests/coercions_propagation.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/coercions_propagation/".
  16
  17 include "logic/connectives.ma".
  18 include "nat/orders.ma".
  19 alias num (instance 0) = "natural number".
  20
  21 inductive sigma (A:Type) (P:A → Prop) : Type ≝
  22  sigma_intro: ∀a:A. P a → sigma A P.
  23
  24 interpretation "sigma" 'exists \eta.x =
  25   (cic:/matita/test/coercions_propagation/sigma.ind#xpointer(1/1) _ x).
  26
  27 definition inject ≝ λP.λa:nat.λp:P a. sigma_intro ? P ? p.
  28
  29 coercion cic:/matita/test/coercions_propagation/inject.con 0 1.
  30
  31 definition eject ≝ λP.λc: ∃n:nat.P n. match c with [ sigma_intro w _ ⇒ w].
  32
  33 coercion cic:/matita/test/coercions_propagation/eject.con.
  34
  35 alias num (instance 0) = "natural number".
  36
  37 theorem test: ∃n. 0 ≤ n.
  38  apply (S O : ∃n. 0 ≤ n).
  39  autobatch.
  40 qed.
  41
  42 theorem test2: nat → ∃n. 0 ≤ n.
  43  apply ((λn:nat. 0) : nat → ∃n. 0 ≤ n);
  44  autobatch.
  45 qed.
  46
  47 theorem test3: (∃n. 0 ≤ n) → nat.
  48  apply ((λn:nat.n) : (∃n. 0 ≤ n) → nat).
  49 qed.
  50
  51 theorem test4: (∃n. 1 ≤ n) → ∃n. 0 < n.
  52  apply ((λn:nat.n) : (∃n. 1 ≤ n) → ∃n. 0 < n);
  53  cases name_con;
  54  assumption.
  55 qed.
  56
  57 theorem test5: nat → ∃n. 1 ≤ n.
  58 apply (
  59  let rec aux n : nat ≝
  60   match n with
  61    [ O ⇒ 1
  62    | S m ⇒ S (aux m)
  63    ]
  64  in
  65   aux
  66 : nat → ∃n. 1 ≤ n);
  67 [ cases (aux name_con); simplify; ] autobatch;
  68 qed.
  69
  70 inductive NN (A:Type) : nat -> Type ≝
  71  | NO : NN A O
  72  | NS : ∀n:nat. NN A n → NN A (S n).
  73
  74 definition injectN ≝ λA,k.λP.λa:NN A k.λp:P a. sigma_intro ? P ? p.
  75
  76 coercion cic:/matita/test/coercions_propagation/injectN.con 0 1.
  77
  78 definition ejectN ≝ λA,k.λP.λc: ∃n:NN A k.P n. match c with [ sigma_intro w _ ⇒ w].
  79
  80 coercion cic:/matita/test/coercions_propagation/ejectN.con.
  81
  82 definition PN :=
  83  λA,k.λx:NN A k. 1 <= k.
  84
  85 theorem test51_byhand: ∀A,k. NN A k → ∃n:NN A (S k). PN ? ? n.
  86 intros 1;
  87 apply (
  88  let rec aux (w : nat) (n : NN A w) on n : ∃p:NN A (S w).PN ? ? p ≝
  89   match n in NN return λx.λm:NN A x.∃p:NN A (S x).PN ? ? p with
  90    [ NO ⇒ injectN ? ? ? (NS A ? (NO A)) ?
  91    | NS x m ⇒ injectN ? ? ? (NS A (S x) (ejectN ? ? ? (aux ? m))) ?
  92    ]
  93  in
  94   aux
  95 : ∀n:nat. NN A n → ∃m:NN A (S n). PN ? ? m);
  96 [2: cases (aux x m); simplify; autobatch ] unfold PN; autobatch;
  97 qed.
  98
  99 theorem f : nat -> nat -> ∃n:nat.O <= n.
 100 apply (λx,y:nat.y : nat -> nat -> ∃n:nat. O <= n).
 101 apply le_O_n;
 102 qed.
 103
 104 axiom F : nat -> nat -> nat.
 105
 106 theorem f1 : nat -> nat -> ∃n:nat.O <= n.
 107 apply (F : nat -> nat -> ∃n:nat. O <= n).
 108 apply le_O_n;
 109 qed.
 110
 111 theorem test51: ∀A,k. NN A k → ∃n:NN A (S k). PN ? ? n.
 112 intros 1;
 113 (* MANCA UN LIFT forse NEL FIX *)
 114 apply (
 115  let rec aux (w : nat) (n : NN A w) on n : NN A (S w) ≝
 116   match n in NN return λx.λm:NN A x.NN A (S x) with
 117    [ NO ⇒ NS A ? (NO A)
 118    | NS x m ⇒ NS A (S x) (aux ? m)
 119    ]
 120  in
 121   aux
 122 : ∀n:nat. NN A n → ∃m:NN A (S n). PN ? ? m);
 123 [ cases (aux name_con); simplify; ] autobatch;
 124 qed.
 125
 126 (* guarded troppo debole
 127 theorem test5: nat → ∃n. 1 ≤ n.
 128 apply (
 129  let rec aux n : nat ≝
 130   match n with
 131    [ O ⇒ 1
 132    | S m ⇒ S (aux m)
 133    ]
 134  in
 135   aux
 136 : nat → ∃n. 1 ≤ n);
 137 cases name_con;
 138 simplify;
 139  [ autobatch
 140  | cases (aux n);
 141    simplify;
 142    apply lt_O_S
 143  ]
 144 qed.
 145 *)
 146
 147 (*
 148 theorem test5: nat → ∃n. 1 ≤ n.
 149 apply (
 150  let rec aux (n : nat) : ∃n. 1 ≤ n ≝
 151    match n with
 152    [ O => (S O : ∃n. 1 ≤ n)
 153    | S m => (S (aux m) : ∃n. 1 ≤ n)
 154 (*
 155    inject ? (S (eject ? (aux m))) ? *)
 156    ]
 157  in
 158   aux
 159  : nat → ∃n. 1 ≤ n);
 160  [ autobatch
 161  | elim (aux m);
 162    simplify;
 163    autobatch
 164  ]
 165 qed.
 166
 167 Re1: nat => nat |- body[Rel1] : nat => nat
 168 Re1: nat => X |- body[Rel1] : nat => nat : nat => X
 169 Re1: Y => X |- body[Rel1] : nat => nat : Y => X
 170
 171 nat => nat
 172 nat => X
 173
 174 theorem test5: (∃n. 2 ≤ n) → ∃n. 1 ≤ n.
 175 apply (
 176  λk: ∃n. 2 ≤ n.
 177  let rec aux n : eject ? n = eject ? k → ∃n. 1 ≤ n ≝
 178   match eject ? n return λx:nat. x = eject ? k → ∃n. 1 ≤ n with
 179    [ O ⇒ λH: 0 = eject ? k.
 180           sigma_intro ? ? 0 ?
 181    | S m ⇒ λH: S m = eject ? k.
 182           sigma_intro ? ? (S m) ?
 183    ]
 184  in
 185   aux k (refl_eq ? (eject ? k)));
 186
 187
 188 intro;
 189 cases s; clear s;
 190 generalize in match H; clear H;
 191 elim a;
 192  [ apply (sigma_intro ? ? 0);
 193  | apply (sigma_intro ? ? (S n));
 194  ].
 195
 196 apply (
 197  λk.
 198  let rec aux n : ∃n. 1 ≤ n ≝
 199   inject ?
 200    (match n with
 201      [ O ⇒ O
 202      | S m ⇒ S (eject ? (aux m))
 203      ]) ?
 204  in aux (eject ? k)).
 205
 206
 207 apply (
 208  let rec aux n : nat ≝
 209   match n with
 210    [ O ⇒ O
 211    | S m ⇒ S (aux m)
 212    ]
 213  in
 214   aux
 215 : (∃n. 2 ≤ n) → ∃n. 1 ≤ n);
 216
 217 qed.
 218
 219 (*
 220 theorem test5: nat → ∃n. 0 ≤ n.
 221  apply (λn:nat.?);
 222  apply
 223   (match n return λ_.∃n.0 ≤ n with [O ⇒ (0 : ∃n.0 ≤ n) | S n' ⇒ ex_intro ? ? n' ?]
 224   : ∃n. 0 ≤ n);
 225  autobatch.
 226 qed.
 227 *)
 228 *)