helm/software/matita/tests/Ztest.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "arithmetics/nat.ma".
  16
  17 ninductive Z : Type ≝
  18   OZ : Z
  19 | pos : nat → Z
  20 | neg : nat → Z.
  21
  22 interpretation "Integers" 'Z = Z.
  23
  24 (* TODO: move the following two to datatypes/compare.ma *)
  25 ninductive compare : Type[0] ≝
  26 | LT : compare
  27 | EQ : compare
  28 | GT : compare.
  29
  30 nlet rec nat_compare n m: compare ≝
  31 match n with
  32 [ O ⇒ match m with
  33       [ O ⇒ EQ
  34       | (S q) ⇒ LT ]
  35 | S p ⇒ match m with
  36       [ O ⇒ GT
  37       | S q ⇒ nat_compare p q]].
  38
  39 ndefinition Zplus : Z → Z → Z ≝
  40   λx,y. match x with
  41     [ OZ ⇒ y
  42     | pos m ⇒
  43         match y with
  44          [ OZ ⇒ x
  45          | pos n ⇒ (pos (pred ((S m)+(S n))))
  46          | neg n ⇒
  47               match nat_compare m n with
  48                 [ LT ⇒ (neg (pred (n-m)))
  49                 | EQ ⇒ OZ
  50                 | GT ⇒ (pos (pred (m-n)))] ]
  51     | neg m ⇒
  52         match y with
  53          [ OZ ⇒ x
  54          | pos n ⇒
  55               match nat_compare m n with
  56                 [ LT ⇒ (pos (pred (n-m)))
  57                 | EQ ⇒ OZ
  58                 | GT ⇒ (neg (pred (m-n)))]
  59          | neg n ⇒ (neg (pred ((S m)+(S n))))] ].
  60
  61 interpretation "integer plus" 'plus x y = (Zplus x y).
  62
  63 ndefinition Z_of_nat ≝
  64 λn. match n with
  65 [ O ⇒ OZ
  66 | S n ⇒ pos n].
  67
  68 nlemma fails : ∀p. p + Z_of_nat 1 = Z_of_nat 1 + p.
  69 #p;nnormalize;