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