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