helm/matita/library/Z/orders.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/orders".
  16
  17 include "Z/z.ma".
  18
  19 definition Zle : Z \to Z \to Prop \def
  20 \lambda x,y:Z.
  21   match x with
  22   [ OZ \Rightarrow
  23     match y with
  24     [ OZ \Rightarrow True
  25     | (pos m) \Rightarrow True
  26     | (neg m) \Rightarrow False ]
  27   | (pos n) \Rightarrow
  28     match y with
  29     [ OZ \Rightarrow False
  30     | (pos m) \Rightarrow (le n m)
  31     | (neg m) \Rightarrow False ]
  32   | (neg n) \Rightarrow
  33     match y with
  34     [ OZ \Rightarrow True
  35     | (pos m) \Rightarrow True
  36     | (neg m) \Rightarrow (le m n) ]].
  37
  38
  39 definition Zlt : Z \to Z \to Prop \def
  40 \lambda x,y:Z.
  41   match x with
  42   [ OZ \Rightarrow
  43     match y with
  44     [ OZ \Rightarrow False
  45     | (pos m) \Rightarrow True
  46     | (neg m) \Rightarrow False ]
  47   | (pos n) \Rightarrow
  48     match y with
  49     [ OZ \Rightarrow False
  50     | (pos m) \Rightarrow (lt n m)
  51     | (neg m) \Rightarrow False ]
  52   | (neg n) \Rightarrow
  53     match y with
  54     [ OZ \Rightarrow True
  55     | (pos m) \Rightarrow True
  56     | (neg m) \Rightarrow (lt m n) ]].
  57
  58 theorem irreflexive_Zlt: irreflexive Z Zlt.
  59 change with \forall x:Z. Zlt x x \to False.
  60 intro.elim x.exact H.
  61 cut (Zlt (neg n) (neg n)) \to False.
  62 apply Hcut.apply H.simplify.apply not_le_Sn_n.
  63 cut (Zlt (pos n) (pos n)) \to False.
  64 apply Hcut.apply H.simplify.apply not_le_Sn_n.
  65 qed.
  66
  67 theorem irrefl_Zlt: irreflexive Z Zlt
  68 \def irreflexive_Zlt.
  69
  70 definition Z_compare : Z \to Z \to compare \def
  71 \lambda x,y:Z.
  72   match x with
  73   [ OZ \Rightarrow
  74     match y with
  75     [ OZ \Rightarrow EQ
  76     | (pos m) \Rightarrow LT
  77     | (neg m) \Rightarrow GT ]
  78   | (pos n) \Rightarrow
  79     match y with
  80     [ OZ \Rightarrow GT
  81     | (pos m) \Rightarrow (nat_compare n m)
  82     | (neg m) \Rightarrow GT]
  83   | (neg n) \Rightarrow
  84     match y with
  85     [ OZ \Rightarrow LT
  86     | (pos m) \Rightarrow LT
  87     | (neg m) \Rightarrow nat_compare m n ]].
  88
  89 theorem Zlt_neg_neg_to_lt:
  90 \forall n,m:nat. Zlt (neg n) (neg m) \to lt m n.
  91 intros.apply H.
  92 qed.
  93
  94 theorem lt_to_Zlt_neg_neg: \forall n,m:nat.lt m n \to Zlt (neg n) (neg m).
  95 intros.
  96 simplify.apply H.
  97 qed.
  98
  99 theorem Zlt_pos_pos_to_lt:
 100 \forall n,m:nat. Zlt (pos n) (pos m) \to lt n m.
 101 intros.apply H.
 102 qed.
 103
 104 theorem lt_to_Zlt_pos_pos: \forall n,m:nat.lt n m \to Zlt (pos n) (pos m).
 105 intros.
 106 simplify.apply H.
 107 qed.
 108
 109 theorem Z_compare_to_Prop :
 110 \forall x,y:Z. match (Z_compare x y) with
 111 [ LT \Rightarrow (Zlt x y)
 112 | EQ \Rightarrow (eq Z x y)
 113 | GT \Rightarrow (Zlt y x)].
 114 intros.
 115 elim x. elim y.
 116 simplify.apply refl_eq.
 117 simplify.exact I.
 118 simplify.exact I.
 119 elim y. simplify.exact I.
 120 simplify.
 121 cut match (nat_compare n1 n) with
 122 [ LT \Rightarrow (lt n1 n)
 123 | EQ \Rightarrow (eq nat n1 n)
 124 | GT \Rightarrow (lt n n1)] \to
 125 match (nat_compare n1 n) with
 126 [ LT \Rightarrow (le (S n1) n)
 127 | EQ \Rightarrow (eq Z (neg n) (neg n1))
 128 | GT \Rightarrow (le (S n) n1)].
 129 apply Hcut. apply nat_compare_to_Prop.
 130 elim (nat_compare n1 n).
 131 simplify.exact H.
 132 simplify.exact H.
 133 simplify.apply eq_f.apply sym_eq.exact H.
 134 simplify.exact I.
 135 elim y.simplify.exact I.
 136 simplify.exact I.
 137 simplify.
 138 cut match (nat_compare n n1) with
 139 [ LT \Rightarrow (lt n n1)
 140 | EQ \Rightarrow (eq nat n n1)
 141 | GT \Rightarrow (lt n1 n)] \to
 142 match (nat_compare n n1) with
 143 [ LT \Rightarrow (le (S n) n1)
 144 | EQ \Rightarrow (eq Z (pos n) (pos n1))
 145 | GT \Rightarrow (le (S n1) n)].
 146 apply Hcut. apply nat_compare_to_Prop.
 147 elim (nat_compare n n1).
 148 simplify.exact H.
 149 simplify.exact H.
 150 simplify.apply eq_f.exact H.
 151 qed.
 152
 153 theorem Zlt_to_Zle: \forall x,y:Z. Zlt x y \to Zle (Zsucc x) y.
 154 intros 2.elim x.
 155 cut (Zlt OZ y) \to (Zle (Zsucc OZ) y).
 156 apply Hcut. assumption.simplify.elim y.
 157 simplify.exact H1.
 158 simplify.exact H1.
 159 simplify.apply le_O_n.
 160 cut (Zlt (neg n) y) \to (Zle (Zsucc (neg n)) y).
 161 apply Hcut. assumption.elim n.
 162 cut (Zlt (neg O) y) \to (Zle (Zsucc (neg O)) y).
 163 apply Hcut. assumption.simplify.elim y.
 164 simplify.exact I.simplify.apply not_le_Sn_O n1 H2.
 165 simplify.exact I.
 166 cut (Zlt (neg (S n1)) y) \to (Zle (Zsucc (neg (S n1))) y).
 167 apply Hcut. assumption.simplify.
 168 elim y.
 169 simplify.exact I.
 170 simplify.apply le_S_S_to_le n2 n1 H3.
 171 simplify.exact I.
 172 exact H.
 173 qed.