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