helm/software/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 include "Z/z.ma".
  16 include "nat/orders.ma".
  17
  18 definition Zle : Z \to Z \to Prop \def
  19 \lambda x,y:Z.
  20   match x with
  21   [ OZ \Rightarrow
  22     match y with
  23     [ OZ \Rightarrow True
  24     | (pos m) \Rightarrow True
  25     | (neg m) \Rightarrow False ]
  26   | (pos n) \Rightarrow
  27     match y with
  28     [ OZ \Rightarrow False
  29     | (pos m) \Rightarrow n \leq m
  30     | (neg m) \Rightarrow False ]
  31   | (neg n) \Rightarrow
  32     match y with
  33     [ OZ \Rightarrow True
  34     | (pos m) \Rightarrow True
  35     | (neg m) \Rightarrow m \leq n ]].
  36
  37 interpretation "integer 'less or equal to'" 'leq x y = (Zle x y).
  38 interpretation "integer 'neither less nor equal to'" 'nleq x y = (Not (Zle x y)).
  39
  40 definition Zlt : Z \to Z \to Prop \def
  41 \lambda x,y:Z.
  42   match x with
  43   [ OZ \Rightarrow
  44     match y with
  45     [ OZ \Rightarrow False
  46     | (pos m) \Rightarrow True
  47     | (neg m) \Rightarrow False ]
  48   | (pos n) \Rightarrow
  49     match y with
  50     [ OZ \Rightarrow False
  51     | (pos m) \Rightarrow n<m
  52     | (neg m) \Rightarrow False ]
  53   | (neg n) \Rightarrow
  54     match y with
  55     [ OZ \Rightarrow True
  56     | (pos m) \Rightarrow True
  57     | (neg m) \Rightarrow m<n ]].
  58
  59 interpretation "integer 'less than'" 'lt x y = (Zlt x y).
  60 interpretation "integer 'not less than'" 'nless x y = (Not (Zlt x y)).
  61
  62 theorem irreflexive_Zlt: irreflexive Z Zlt.
  63 unfold irreflexive.unfold Not.
  64 intro.elim x.exact H.
  65 cut (neg n < neg n \to False).
  66 apply Hcut.apply H.simplify.unfold lt.apply not_le_Sn_n.
  67 cut (pos n < pos n \to False).
  68 apply Hcut.apply H.simplify.unfold lt.apply not_le_Sn_n.
  69 qed.
  70
  71 (* transitivity *)
  72 theorem transitive_Zle : transitive Z Zle.
  73 unfold transitive.
  74 intros 3.
  75 elim x 0
  76 [ (* x = OZ *)
  77   elim y 0
  78   [ intros. assumption
  79   | intro.
  80     elim z
  81     [ simplify. apply I
  82     | simplify. apply I
  83     | simplify. simplify in H1. assumption
  84     ]
  85   | intro.
  86     elim z
  87     [ simplify. apply I
  88     | simplify. apply I
  89     | simplify. simplify in H. assumption
  90     ]
  91   ]
  92 | (* x = (pos n) *)
  93   intro.
  94   elim y 0
  95   [ intros. apply False_ind. apply H
  96   | intros 2.
  97     elim z 0
  98     [ simplify. intro. assumption
  99     | intro. generalize in match H. simplify. apply trans_le
 100     | intro. simplify. intro. assumption
 101     ]
 102   | intros 2. apply False_ind. apply H
 103   ]
 104 | (* x = (neg n) *)
 105   intro.
 106   elim y 0
 107   [ elim z 0
 108     [ simplify. intros. assumption
 109     | intro. simplify. intros. assumption
 110     | intro. simplify. intros. apply False_ind. apply H1
 111     ]
 112   | intros 2.
 113     elim z
 114     [ apply False_ind. apply H1
 115     | simplify. apply I
 116     | apply False_ind. apply H1
 117     ]
 118   | intros 2.
 119     elim z 0
 120     [ simplify. intro. assumption
 121     | intro. simplify. intro. assumption
 122     | intros. simplify. simplify in H. simplify in H1.
 123       generalize in match H. generalize in match H1. apply trans_le
 124     ]
 125   ]
 126 ]
 127 qed.
 128
 129 variant trans_Zle: transitive Z Zle
 130 \def transitive_Zle.
 131
 132 theorem transitive_Zlt: transitive Z Zlt.
 133 unfold.
 134 intros 3.
 135 elim x 0
 136 [ (* x = OZ *)
 137   elim y 0
 138   [ intros. apply False_ind. apply H
 139   | intro.
 140     elim z
 141     [ simplify. apply H1
 142     | simplify. apply I
 143     | simplify. apply H1
 144     ]
 145   | intros 2. apply False_ind. apply H
 146   ]
 147 | (* x = (pos n) *)
 148   intro.
 149   elim y 0
 150   [ intros. apply False_ind. apply H
 151   | intros 2.
 152     elim z 0
 153     [ simplify. intro. assumption
 154     | intro. generalize in match H. simplify. apply trans_lt
 155     | intro. simplify. intro. assumption
 156     ]
 157   | intros 2. apply False_ind. apply H
 158   ]
 159 | (* x = (neg n) *)
 160   intro.
 161   elim y 0
 162   [ elim z 0
 163     [ intros. simplify. apply I
 164     | intro. simplify. intros. assumption
 165     | intro. simplify. intros. apply False_ind. apply H1
 166     ]
 167   | intros 2.
 168     elim z
 169     [ apply False_ind. apply H1
 170     | simplify. apply I
 171     | apply False_ind. apply H1
 172     ]
 173   | intros 2.
 174     elim z 0
 175     [ simplify. intro. assumption
 176     | intro. simplify. intro. assumption
 177     | intros. simplify. simplify in H. simplify in H1.
 178       generalize in match H. generalize in match H1. apply trans_lt
 179     ]
 180   ]
 181 ]
 182 qed.
 183
 184 variant trans_Zlt: transitive Z Zlt
 185 \def transitive_Zlt.
 186 theorem irrefl_Zlt: irreflexive Z Zlt
 187 \def irreflexive_Zlt.
 188
 189 theorem Zlt_neg_neg_to_lt:
 190 \forall n,m:nat. neg n < neg m \to m < n.
 191 intros.apply H.
 192 qed.
 193
 194 theorem lt_to_Zlt_neg_neg: \forall n,m:nat.m < n \to neg n < neg m.
 195 intros.
 196 simplify.apply H.
 197 qed.
 198
 199 theorem Zlt_pos_pos_to_lt:
 200 \forall n,m:nat. pos n < pos m \to n < m.
 201 intros.apply H.
 202 qed.
 203
 204 theorem lt_to_Zlt_pos_pos: \forall n,m:nat.n < m \to pos n < pos m.
 205 intros.
 206 simplify.apply H.
 207 qed.
 208
 209 theorem Zlt_to_Zle: \forall x,y:Z. x < y \to Zsucc x \leq y.
 210 intros 2.
 211 elim x.
 212 (* goal: x=OZ *)
 213   cut (OZ < y \to Zsucc OZ \leq y).
 214     apply Hcut. assumption.
 215     simplify.elim y.
 216       simplify.exact H1.
 217       simplify.apply le_O_n.
 218       simplify.exact H1.
 219 (* goal: x=pos *)
 220   exact H.
 221 (* goal: x=neg *)
 222   cut (neg n < y \to Zsucc (neg n) \leq y).
 223     apply Hcut. assumption.
 224     elim n.
 225       cut (neg O < y \to Zsucc (neg O) \leq y).
 226         apply Hcut. assumption.
 227         simplify.elim y.
 228           simplify.exact I.
 229           simplify.exact I.
 230           simplify.apply (not_le_Sn_O n1 H2).
 231       cut (neg (S n1) < y \to (Zsucc (neg (S n1))) \leq y).
 232         apply Hcut. assumption.simplify.
 233         elim y.
 234           simplify.exact I.
 235           simplify.exact I.
 236           simplify.apply (le_S_S_to_le n2 n1 H3).
 237 qed.