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 n \leq 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 m \leq 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
  41 definition Zlt : Z \to Z \to Prop \def
  42 \lambda x,y:Z.
  43   match x with
  44   [ OZ \Rightarrow
  45     match y with
  46     [ OZ \Rightarrow False
  47     | (pos m) \Rightarrow True
  48     | (neg m) \Rightarrow False ]
  49   | (pos n) \Rightarrow
  50     match y with
  51     [ OZ \Rightarrow False
  52     | (pos m) \Rightarrow n<m
  53     | (neg m) \Rightarrow False ]
  54   | (neg n) \Rightarrow
  55     match y with
  56     [ OZ \Rightarrow True
  57     | (pos m) \Rightarrow True
  58     | (neg m) \Rightarrow m<n ]].
  59
  60 (*CSC: the URI must disappear: there is a bug now *)
  61 interpretation "integer 'less than'" 'lt x y = (cic:/matita/Z/orders/Zlt.con x y).
  62
  63 theorem irreflexive_Zlt: irreflexive Z Zlt.
  64 change with \forall x:Z. x < x \to False.
  65 intro.elim x.exact H.
  66 cut neg n < neg n \to False.
  67 apply Hcut.apply H.simplify.apply not_le_Sn_n.
  68 cut pos n < pos n \to False.
  69 apply Hcut.apply H.simplify.apply not_le_Sn_n.
  70 qed.
  71
  72 theorem irrefl_Zlt: irreflexive Z Zlt
  73 \def irreflexive_Zlt.
  74
  75 definition Z_compare : Z \to Z \to compare \def
  76 \lambda x,y:Z.
  77   match x with
  78   [ OZ \Rightarrow
  79     match y with
  80     [ OZ \Rightarrow EQ
  81     | (pos m) \Rightarrow LT
  82     | (neg m) \Rightarrow GT ]
  83   | (pos n) \Rightarrow
  84     match y with
  85     [ OZ \Rightarrow GT
  86     | (pos m) \Rightarrow (nat_compare n m)
  87     | (neg m) \Rightarrow GT]
  88   | (neg n) \Rightarrow
  89     match y with
  90     [ OZ \Rightarrow LT
  91     | (pos m) \Rightarrow LT
  92     | (neg m) \Rightarrow nat_compare m n ]].
  93
  94 (*CSC: qui uso lt perche' ho due istanze diverse di < *)
  95 theorem Zlt_neg_neg_to_lt:
  96 \forall n,m:nat. neg n < neg m \to lt m n.
  97 intros.apply H.
  98 qed.
  99
 100 (*CSC: qui uso lt perche' ho due istanze diverse di < *)
 101 theorem lt_to_Zlt_neg_neg: \forall n,m:nat.lt m n \to neg n < neg m.
 102 intros.
 103 simplify.apply H.
 104 qed.
 105
 106 (*CSC: qui uso lt perche' ho due istanze diverse di < *)
 107 theorem Zlt_pos_pos_to_lt:
 108 \forall n,m:nat. pos n < pos m \to lt n m.
 109 intros.apply H.
 110 qed.
 111
 112 (*CSC: qui uso lt perche' ho due istanze diverse di < *)
 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 (*CSC: qui uso le perche' altrimenti ci sono troppe scelte
 131   per via delle coercions! *)
 132 cut match (nat_compare n1 n) with
 133 [ LT \Rightarrow n1<n
 134 | EQ \Rightarrow n1=n
 135 | GT \Rightarrow n<n1] \to
 136 match (nat_compare n1 n) with
 137 [ LT \Rightarrow (le (S n1) n)
 138 | EQ \Rightarrow neg n = neg n1
 139 | GT \Rightarrow (le (S n) n1)].
 140 apply Hcut. apply nat_compare_to_Prop.
 141 elim (nat_compare n1 n).
 142 simplify.exact H.
 143 simplify.exact H.
 144 simplify.apply eq_f.apply sym_eq.exact H.
 145 simplify.exact I.
 146 elim y.simplify.exact I.
 147 simplify.exact I.
 148 simplify.
 149 (*CSC: qui uso le perche' altrimenti ci sono troppe scelte
 150   per via delle coercions! *)
 151 cut match (nat_compare n n1) with
 152 [ LT \Rightarrow n<n1
 153 | EQ \Rightarrow n=n1
 154 | GT \Rightarrow n1<n] \to
 155 match (nat_compare n n1) with
 156 [ LT \Rightarrow (le (S n) n1)
 157 | EQ \Rightarrow pos n = pos n1
 158 | GT \Rightarrow (le (S n1) n)].
 159 apply Hcut. apply nat_compare_to_Prop.
 160 elim (nat_compare n n1).
 161 simplify.exact H.
 162 simplify.exact H.
 163 simplify.apply eq_f.exact H.
 164 qed.
 165
 166 theorem Zlt_to_Zle: \forall x,y:Z. x < y \to Zsucc x \leq y.
 167 intros 2.elim x.
 168 cut OZ < y \to Zsucc OZ \leq y.
 169 apply Hcut. assumption.simplify.elim y.
 170 simplify.exact H1.
 171 simplify.exact H1.
 172 simplify.apply le_O_n.
 173 cut neg n < y \to Zsucc (neg n) \leq y.
 174 apply Hcut. assumption.elim n.
 175 cut neg O < y \to Zsucc (neg O) \leq y.
 176 apply Hcut. assumption.simplify.elim y.
 177 simplify.exact I.simplify.apply not_le_Sn_O n1 H2.
 178 simplify.exact I.
 179 cut neg (S n1) < y \to (Zsucc (neg (S n1))) \leq y.
 180 apply Hcut. assumption.simplify.
 181 elim y.
 182 simplify.exact I.
 183 simplify.apply le_S_S_to_le n2 n1 H3.
 184 simplify.exact I.
 185 exact H.
 186 qed.