helm/software/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
  16
  17 include "nat/compare.ma".
  18 include "nat/times.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 (* This used to test eq_f as a coercion. However, posing both eq_f and sym_eq
  63    as coercions made the qed time of some TPTP problems reach infty.
  64    Thus eq_f is no longer a coercion (nor is sym_eq).
  65 theorem coercion_svelta : \forall T,S:Type.\forall f:T \to S.\forall x,y:T.x=y \to f y = f x.
  66   intros.
  67   apply ((\lambda h:f y = f x.h) H).
  68 qed.
  69 *)
  70
  71 variant pos2nat' : ? \def pos2nat.
  72
  73 inductive initial: Set \def iii : initial.
  74
  75 definition i2pos: ? \def \lambda x:initial.one.
  76
  77 coercion cic:/matita/tests/coercions/i2pos.con.
  78
  79 coercion cic:/matita/tests/coercions/pos2nat'.con.
  80
  81 inductive listn (A:Type) : nat \to Type \def
  82  | Nil : listn A O
  83  | Next : \forall n.\forall l:listn A n.\forall a:A.listn A (S n).
  84
  85 definition if : \forall A:Type.\forall b:bool.\forall a,c:A.A \def
  86   \lambda A,b,a,c.
  87   match b with
  88   [ true \Rightarrow a
  89   | false \Rightarrow c].
  90
  91 let rec ith (A:Type) (n,m:nat) (dummy:A) (l:listn A n) on l \def
  92   match l with
  93   [ Nil \Rightarrow dummy
  94   | (Next w l x) \Rightarrow if A (eqb w m) x (ith A w m dummy l)].
  95
  96 definition listn2function:
  97   \forall A:Type.\forall dummy:A.\forall n.listn A n \to nat \to A
  98 \def
  99   \lambda A,dummy,n,l,m.ith A n m dummy l.
 100
 101 definition natlist2map: ? \def listn2function nat O.
 102
 103 coercion cic:/matita/tests/coercions/natlist2map.con 1.
 104 definition map:  \forall n:nat.\forall l:listn nat n. nat \to nat \def
 105   \lambda n:nat.\lambda l:listn nat n.\lambda m:nat.l m.
 106
 107 definition church: nat \to nat \to nat \def times.
 108
 109 coercion cic:/matita/tests/coercions/church.con 1.
 110 lemma foo0 : ∀n:nat. n n = n * n.
 111 intros; reflexivity;
 112 qed.
 113 lemma foo01 : ∀n:nat. n n n = n * n * n.
 114 intros; reflexivity;
 115 qed.
 116
 117 definition mapmult:  \forall n:nat.\forall l:listn nat n. nat \to nat \to nat \def
 118   \lambda n:nat.\lambda l:listn nat n.\lambda m,o:nat.
 119   l (m m) o (o o o).
 120
 121 lemma foo : ∀n:nat. n n n n n n = n * n * n * n * n * n.
 122 intros; reflexivity;
 123 qed.
 124
 125 axiom f : nat → nat.
 126
 127 lemma foo1 : ∀n:nat. f n n = f n * n.
 128
 129 axiom T0 : Type.
 130 axiom T1 : Type.
 131 axiom T2 : Type.
 132 axiom T3 : Type.
 133
 134 axiom c1 : T0 -> T1.
 135 axiom c2 : T1 -> T2.
 136 axiom c3 : T2 -> T3.
 137 axiom c4 : T2 -> T1.
 138
 139 coercion cic:/matita/tests/coercions/c1.con.
 140 coercion cic:/matita/tests/coercions/c2.con.
 141 coercion cic:/matita/tests/coercions/c3.con.
 142 coercion cic:/matita/tests/coercions/c4.con.
 143
 144
 145
 146
 147
 148