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 (* guarded troppo debole
  58 theorem test5: nat → ∃n. 1 ≤ n.
  59 apply (
  60  let rec aux n : nat ≝
  61   match n with
  62    [ O ⇒ 1
  63    | S m ⇒ S (aux m)
  64    ]
  65  in
  66   aux
  67 : nat → ∃n. 1 ≤ n);
  68 cases name_con;
  69 simplify;
  70  [ autobatch
  71  | cases (aux n);
  72    simplify;
  73    apply lt_O_S
  74  ]
  75 qed.
  76 *)
  77
  78 (*
  79 theorem test5: nat → ∃n. 1 ≤ n.
  80 apply (
  81  let rec aux (n : nat) : ∃n. 1 ≤ n ≝
  82    match n with
  83    [ O => (S O : ∃n. 1 ≤ n)
  84    | S m => (S (aux m) : ∃n. 1 ≤ n)
  85 (*
  86    inject ? (S (eject ? (aux m))) ? *)
  87    ]
  88  in
  89   aux
  90  : nat → ∃n. 1 ≤ n);
  91  [ autobatch
  92  | elim (aux m);
  93    simplify;
  94    autobatch
  95  ]
  96 qed.
  97
  98 Re1: nat => nat |- body[Rel1] : nat => nat
  99 Re1: nat => X |- body[Rel1] : nat => nat : nat => X
 100 Re1: Y => X |- body[Rel1] : nat => nat : Y => X
 101
 102 nat => nat
 103 nat => X
 104
 105 theorem test5: (∃n. 2 ≤ n) → ∃n. 1 ≤ n.
 106 apply (
 107  λk: ∃n. 2 ≤ n.
 108  let rec aux n : eject ? n = eject ? k → ∃n. 1 ≤ n ≝
 109   match eject ? n return λx:nat. x = eject ? k → ∃n. 1 ≤ n with
 110    [ O ⇒ λH: 0 = eject ? k.
 111           sigma_intro ? ? 0 ?
 112    | S m ⇒ λH: S m = eject ? k.
 113           sigma_intro ? ? (S m) ?
 114    ]
 115  in
 116   aux k (refl_eq ? (eject ? k)));
 117
 118
 119 intro;
 120 cases s; clear s;
 121 generalize in match H; clear H;
 122 elim a;
 123  [ apply (sigma_intro ? ? 0);
 124  | apply (sigma_intro ? ? (S n));
 125  ].
 126
 127 apply (
 128  λk.
 129  let rec aux n : ∃n. 1 ≤ n ≝
 130   inject ?
 131    (match n with
 132      [ O ⇒ O
 133      | S m ⇒ S (eject ? (aux m))
 134      ]) ?
 135  in aux (eject ? k)).
 136
 137
 138 apply (
 139  let rec aux n : nat ≝
 140   match n with
 141    [ O ⇒ O
 142    | S m ⇒ S (aux m)
 143    ]
 144  in
 145   aux
 146 : (∃n. 2 ≤ n) → ∃n. 1 ≤ n);
 147
 148 qed.
 149
 150 (*
 151 theorem test5: nat → ∃n. 0 ≤ n.
 152  apply (λn:nat.?);
 153  apply
 154   (match n return λ_.∃n.0 ≤ n with [O ⇒ (0 : ∃n.0 ≤ n) | S n' ⇒ ex_intro ? ? n' ?]
 155   : ∃n. 0 ≤ n);
 156  autobatch.
 157 qed.
 158 *)
 159 *)