matita/tests/coercions.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/tests/coercions/".
  16
  17 include "nat/compare.ma".
  18 include "datatypes/bool.ma".
  19
  20 inductive pos: Set \def
  21 | one : pos
  22 | next : pos \to pos.
  23
  24 inductive int: Set \def
  25 | positive: nat \to int
  26 | negative : nat \to int.
  27
  28 inductive empty : Set \def .
  29
  30 let rec pos2nat x \def
  31   match x with
  32   [ one \Rightarrow (S O)
  33   | (next z) \Rightarrow S (pos2nat z)].
  34
  35 definition nat2int \def \lambda x. positive x.
  36
  37 coercion cic:/matita/tests/coercions/pos2nat.con.
  38
  39 coercion cic:/matita/tests/coercions/nat2int.con.
  40
  41 definition fst \def \lambda x,y:int.x.
  42
  43 theorem a: fst O one = fst (positive O) (next one).
  44 reflexivity.
  45 qed.
  46
  47 definition double:
  48   \forall f:int \to int. pos \to int
  49 \def
  50   \lambda f:int \to int. \lambda x : pos .f (nat2int x).
  51
  52 definition double1:
  53   \forall f:int \to int. pos \to int
  54 \def
  55   \lambda f:int \to int. \lambda x : pos .f (pos2nat x).
  56
  57 definition double2:
  58   \forall f:int \to int. pos \to int
  59 \def
  60   \lambda f:int \to int. \lambda x : pos .f (nat2int (pos2nat x)).
  61
  62 theorem coercion_svelta : \forall T,S:Type.\forall f:T \to S.\forall x,y:T.x=y \to f y = f x.
  63   intros.
  64   apply ((\lambda h:f y = f x.h) H).
  65 qed.
  66
  67 variant pos2nat' : ? \def pos2nat.
  68
  69 inductive initial: Set \def iii : initial.
  70
  71 definition i2pos: ? \def \lambda x:initial.one.
  72
  73 coercion cic:/matita/tests/coercions/i2pos.con.
  74
  75 coercion cic:/matita/tests/coercions/pos2nat'.con.
  76
  77 inductive listn (A:Type) : nat \to Type \def
  78  | Nil : listn A O
  79  | Next : \forall n.\forall l:listn A n.\forall a:A.listn A (S n).
  80
  81 definition if : \forall A:Type.\forall b:bool.\forall a,c:A.A \def
  82   \lambda A,b,a,c.
  83   match b with
  84   [ true \Rightarrow a
  85   | false \Rightarrow c].
  86
  87 let rec ith (A:Type) (n,m:nat) (dummy:A) (l:listn A n) on l \def
  88   match l with
  89   [ Nil \Rightarrow dummy
  90   | (Next w l x) \Rightarrow if A (eqb w m) x (ith A w m dummy l)].
  91
  92 definition listn2function:
  93   \forall A:Type.\forall dummy:A.\forall n.listn A n \to nat \to A
  94 \def
  95   \lambda A,dummy,n,l,m.ith A n m dummy l.
  96
  97 definition natlist2map: ? \def listn2function nat O.
  98
  99 coercion cic:/matita/tests/coercions/natlist2map.con 1.
 100 definition map:  \forall n:nat.\forall l:listn nat n. nat \to nat \def
 101   \lambda n:nat.\lambda l:listn nat n.\lambda m:nat.l m.
 102
 103 definition church: nat \to nat \to nat \def times.
 104
 105 coercion cic:/matita/tests/coercions/church.con 1.
 106
 107 definition mapmult:  \forall n:nat.\forall l:listn nat n. nat \to nat \to nat \def
 108   \lambda n:nat.\lambda l:listn nat n.\lambda m,o:nat.l m o.
 109
 110
 111
 112