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 (*
  58 theorem test5: nat → ∃n. 0 ≤ n.
  59  apply (λn:nat.?);
  60  apply
  61   (match n return λ_.∃n.0 ≤ n with [O ⇒ (0 : ∃n.0 ≤ n) | S n' ⇒ ex_intro ? ? n' ?]
  62   : ∃n. 0 ≤ n);
  63  autobatch.
  64 qed.
  65 *)