helm/matita/library/Z/compare.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 set "baseuri" "cic:/matita/Z/compare".
  16
  17 include "datatypes/bool.ma".
  18 include "datatypes/compare.ma".
  19 include "Z/orders.ma".
  20 include "nat/compare.ma".
  21
  22 (* boolean equality *)
  23 definition eqZb : Z \to Z \to bool \def
  24 \lambda x,y:Z.
  25   match x with
  26   [ OZ \Rightarrow
  27       match y with
  28         [ OZ \Rightarrow true
  29         | (pos q) \Rightarrow false
  30         | (neg q) \Rightarrow false]
  31   | (pos p) \Rightarrow
  32       match y with
  33         [ OZ \Rightarrow false
  34         | (pos q) \Rightarrow eqb p q
  35         | (neg q) \Rightarrow false]
  36   | (neg p) \Rightarrow
  37       match y with
  38         [ OZ \Rightarrow false
  39         | (pos q) \Rightarrow false
  40         | (neg q) \Rightarrow eqb p q]].
  41
  42 theorem eqZb_to_Prop:
  43 \forall x,y:Z.
  44 match eqZb x y with
  45 [ true \Rightarrow x=y
  46 | false \Rightarrow \lnot x=y].
  47 intros.
  48 elim x.
  49   elim y.
  50     simplify.reflexivity.
  51     simplify.apply not_eq_OZ_pos.
  52     simplify.apply not_eq_OZ_neg.
  53   elim y.
  54     simplify.intro.apply not_eq_OZ_pos n.apply sym_eq.assumption.
  55     simplify.apply eqb_elim.
  56       intro.simplify.apply eq_f.assumption.
  57       intro.simplify.intro.apply H.apply inj_pos.assumption.
  58     simplify.apply not_eq_pos_neg.
  59   elim y.
  60     simplify.intro.apply not_eq_OZ_neg n.apply sym_eq.assumption.
  61     simplify.intro.apply not_eq_pos_neg n1 n.apply sym_eq.assumption.
  62     simplify.apply eqb_elim.
  63       intro.simplify.apply eq_f.assumption.
  64       intro.simplify.intro.apply H.apply inj_neg.assumption.
  65 qed.
  66
  67 theorem eqZb_elim: \forall x,y:Z.\forall P:bool \to Prop.
  68 (x=y \to (P true)) \to (\lnot x=y \to (P false)) \to P (eqZb x y).
  69 intros.
  70 cut
  71 match (eqZb x y) with
  72 [ true \Rightarrow x=y
  73 | false \Rightarrow \lnot x=y] \to P (eqZb x y).
  74 apply Hcut.
  75 apply eqZb_to_Prop.
  76 elim (eqZb).
  77 apply H H2.
  78 apply H1 H2.
  79 qed.
  80
  81 definition Z_compare : Z \to Z \to compare \def
  82 \lambda x,y:Z.
  83   match x with
  84   [ OZ \Rightarrow
  85     match y with
  86     [ OZ \Rightarrow EQ
  87     | (pos m) \Rightarrow LT
  88     | (neg m) \Rightarrow GT ]
  89   | (pos n) \Rightarrow
  90     match y with
  91     [ OZ \Rightarrow GT
  92     | (pos m) \Rightarrow (nat_compare n m)
  93     | (neg m) \Rightarrow GT]
  94   | (neg n) \Rightarrow
  95     match y with
  96     [ OZ \Rightarrow LT
  97     | (pos m) \Rightarrow LT
  98     | (neg m) \Rightarrow nat_compare m n ]].
  99
 100 theorem Z_compare_to_Prop :
 101 \forall x,y:Z. match (Z_compare x y) with
 102 [ LT \Rightarrow x < y
 103 | EQ \Rightarrow x=y
 104 | GT \Rightarrow y < x].
 105 intros.
 106 elim x.
 107   elim y.
 108     simplify.apply refl_eq.
 109     simplify.exact I.
 110     simplify.exact I.
 111   elim y.
 112     simplify.exact I.
 113     simplify.
 114       cut match (nat_compare n n1) with
 115       [ LT \Rightarrow n<n1
 116       | EQ \Rightarrow n=n1
 117       | GT \Rightarrow n1<n] \to
 118       match (nat_compare n n1) with
 119       [ LT \Rightarrow (S n) \leq n1
 120       | EQ \Rightarrow pos n = pos n1
 121       | GT \Rightarrow (S n1) \leq n].
 122         apply Hcut.apply nat_compare_to_Prop.
 123         elim (nat_compare n n1).
 124           simplify.exact H.
 125           simplify.apply eq_f.exact H.
 126           simplify.exact H.
 127     simplify.exact I.
 128   elim y.
 129     simplify.exact I.
 130     simplify.exact I.
 131     simplify.
 132       cut match (nat_compare n1 n) with
 133       [ LT \Rightarrow n1<n
 134       | EQ \Rightarrow n1=n
 135       | GT \Rightarrow n<n1] \to
 136       match (nat_compare n1 n) with
 137       [ LT \Rightarrow (S n1) \leq n
 138       | EQ \Rightarrow neg n = neg n1
 139       | GT \Rightarrow (S n) \leq n1].
 140         apply Hcut. apply nat_compare_to_Prop.
 141         elim (nat_compare n1 n).
 142           simplify.exact H.
 143           simplify.apply eq_f.apply sym_eq.exact H.
 144           simplify.exact H.
 145 qed.