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 (*CSC: the URI must disappear: there is a bug now *)
  39 interpretation "integer 'less or equal to'" 'leq x y = (cic:/matita/Z/orders/Zle.con x y).
  40 (*CSC: this alias must disappear: there is a bug in the generation of the .moos *)
  41 alias symbol "leq" (instance 0) = "integer 'less or equal to'".
  42
  43 definition Zlt : Z \to Z \to Prop \def
  44 \lambda x,y:Z.
  45   match x with
  46   [ OZ \Rightarrow
  47     match y with
  48     [ OZ \Rightarrow False
  49     | (pos m) \Rightarrow True
  50     | (neg m) \Rightarrow False ]
  51   | (pos n) \Rightarrow
  52     match y with
  53     [ OZ \Rightarrow False
  54     | (pos m) \Rightarrow (lt n m)
  55     | (neg m) \Rightarrow False ]
  56   | (neg n) \Rightarrow
  57     match y with
  58     [ OZ \Rightarrow True
  59     | (pos m) \Rightarrow True
  60     | (neg m) \Rightarrow (lt m n) ]].
  61
  62 (*CSC: the URI must disappear: there is a bug now *)
  63 interpretation "integer 'less than'" 'lt x y = (cic:/matita/Z/orders/Zlt.con x y).
  64 (*CSC: this alias must disappear: there is a bug in the generation of the .moos *)
  65 alias symbol "lt" (instance 0) = "integer 'less than'".
  66
  67 theorem irreflexive_Zlt: irreflexive Z Zlt.
  68 change with \forall x:Z. x < x \to False.
  69 intro.elim x.exact H.
  70 cut neg n < neg n \to False.
  71 apply Hcut.apply H.simplify.apply not_le_Sn_n.
  72 cut pos n < pos n \to False.
  73 apply Hcut.apply H.simplify.apply not_le_Sn_n.
  74 qed.
  75
  76 theorem irrefl_Zlt: irreflexive Z Zlt
  77 \def irreflexive_Zlt.
  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 Zlt_neg_neg_to_lt:
  99 \forall n,m:nat. neg n < neg m \to lt m n.
 100 intros.apply H.
 101 qed.
 102
 103 theorem lt_to_Zlt_neg_neg: \forall n,m:nat.lt m n \to neg n < neg m.
 104 intros.
 105 simplify.apply H.
 106 qed.
 107
 108 theorem Zlt_pos_pos_to_lt:
 109 \forall n,m:nat. pos n < pos m \to lt n m.
 110 intros.apply H.
 111 qed.
 112
 113 theorem lt_to_Zlt_pos_pos: \forall n,m:nat.lt n m \to pos n < pos m.
 114 intros.
 115 simplify.apply H.
 116 qed.
 117
 118 theorem Z_compare_to_Prop :
 119 \forall x,y:Z. match (Z_compare x y) with
 120 [ LT \Rightarrow x < y
 121 | EQ \Rightarrow x=y
 122 | GT \Rightarrow y < x].
 123 intros.
 124 elim x. elim y.
 125 simplify.apply refl_eq.
 126 simplify.exact I.
 127 simplify.exact I.
 128 elim y. simplify.exact I.
 129 simplify.
 130 cut match (nat_compare n1 n) with
 131 [ LT \Rightarrow (lt n1 n)
 132 | EQ \Rightarrow (eq nat n1 n)
 133 | GT \Rightarrow (lt n n1)] \to
 134 match (nat_compare n1 n) with
 135 [ LT \Rightarrow (le (S n1) n)
 136 | EQ \Rightarrow (eq Z (neg n) (neg n1))
 137 | GT \Rightarrow (le (S n) n1)].
 138 apply Hcut. apply nat_compare_to_Prop.
 139 elim (nat_compare n1 n).
 140 simplify.exact H.
 141 simplify.exact H.
 142 simplify.apply eq_f.apply sym_eq.exact H.
 143 simplify.exact I.
 144 elim y.simplify.exact I.
 145 simplify.exact I.
 146 simplify.
 147 cut match (nat_compare n n1) with
 148 [ LT \Rightarrow (lt n n1)
 149 | EQ \Rightarrow (eq nat n n1)
 150 | GT \Rightarrow (lt n1 n)] \to
 151 match (nat_compare n n1) with
 152 [ LT \Rightarrow (le (S n) n1)
 153 | EQ \Rightarrow (eq Z (pos n) (pos n1))
 154 | GT \Rightarrow (le (S n1) n)].
 155 apply Hcut. apply nat_compare_to_Prop.
 156 elim (nat_compare n n1).
 157 simplify.exact H.
 158 simplify.exact H.
 159 simplify.apply eq_f.exact H.
 160 qed.
 161
 162 theorem Zlt_to_Zle: \forall x,y:Z. x < y \to Zsucc x \leq y.
 163 intros 2.elim x.
 164 cut OZ < y \to Zsucc OZ \leq y.
 165 apply Hcut. assumption.simplify.elim y.
 166 simplify.exact H1.
 167 simplify.exact H1.
 168 simplify.apply le_O_n.
 169 cut neg n < y \to Zsucc (neg n) \leq y.
 170 apply Hcut. assumption.elim n.
 171 cut neg O < y \to Zsucc (neg O) \leq y.
 172 apply Hcut. assumption.simplify.elim y.
 173 simplify.exact I.simplify.apply not_le_Sn_O n1 H2.
 174 simplify.exact I.
 175 cut neg (S n1) < y \to (Zsucc (neg (S n1))) \leq y.
 176 apply Hcut. assumption.simplify.
 177 elim y.
 178 simplify.exact I.
 179 simplify.apply le_S_S_to_le n2 n1 H3.
 180 simplify.exact I.
 181 exact H.
 182 qed.