matita/library_auto/auto/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/library_auto/Z/orders".
  16
  17 include "auto/Z/z.ma".
  18 include "auto/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/library_auto/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/library_auto/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/library_auto/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/library_auto/Z/orders/Zlt.con x y)).
  69
  70 theorem irreflexive_Zlt: irreflexive Z Zlt.
  71 unfold irreflexive.
  72 unfold Not.
  73 intro.
  74 elim x
  75 [ (*qui auto non chiude il goal*)
  76   exact H
  77 | cut (neg n < neg n \to False)
  78   [ apply Hcut.
  79     (*qui auto non chiude il goal*)
  80     apply H
  81   | auto
  82     (*simplify.
  83     unfold lt.
  84     apply not_le_Sn_n*)
  85   ]
  86 | cut (pos n < pos n \to False)
  87   [ apply Hcut.
  88     (*qui auto non chiude il goal*)
  89     apply H
  90   | auto
  91     (*simplify.
  92     unfold lt.
  93     apply not_le_Sn_n*)
  94   ]
  95 ]
  96 qed.
  97
  98 theorem irrefl_Zlt: irreflexive Z Zlt
  99 \def irreflexive_Zlt.
 100
 101 theorem Zlt_neg_neg_to_lt:
 102 \forall n,m:nat. neg n < neg m \to m < n.
 103 intros.
 104 (*qui auto non chiude il goal*)
 105 apply H.
 106 qed.
 107
 108 theorem lt_to_Zlt_neg_neg: \forall n,m:nat.m < n \to neg n < neg m.
 109 intros.
 110 simplify.
 111 apply H.
 112 qed.
 113
 114 theorem Zlt_pos_pos_to_lt:
 115 \forall n,m:nat. pos n < pos m \to n < m.
 116 intros.
 117 (*qui auto non chiude il goal*)
 118 apply H.
 119 qed.
 120
 121 theorem lt_to_Zlt_pos_pos: \forall n,m:nat.n < m \to pos n < pos m.
 122 intros.
 123 simplify.
 124 apply H.
 125 qed.
 126
 127 theorem Zlt_to_Zle: \forall x,y:Z. x < y \to Zsucc x \leq y.
 128 intros 2.
 129 elim x
 130 [ (* goal: x=OZ *)
 131   cut (OZ < y \to Zsucc OZ \leq y)
 132   [ auto
 133     (*apply Hcut.
 134     assumption*)
 135   | simplify.
 136     elim y
 137     [ simplify.
 138       (*qui auto non chiude il goal*)
 139       exact H1
 140     | simplify.
 141       apply le_O_n
 142     | simplify.
 143       (*qui auto non chiude il goal*)
 144       exact H1
 145     ]
 146   ]
 147 | (* goal: x=pos *)
 148   exact H
 149 | (* goal: x=neg *)
 150   cut (neg n < y \to Zsucc (neg n) \leq y)
 151   [ auto
 152     (*apply Hcut.
 153     assumption*)
 154   | elim n
 155     [ cut (neg O < y \to Zsucc (neg O) \leq y)
 156       [ auto
 157         (*apply Hcut.
 158         assumption*)
 159       | simplify.
 160         elim y
 161         [ simplify.
 162           exact I
 163         | simplify.
 164           exact I
 165         | simplify.
 166           (*qui auto non chiude il goal*)
 167           apply (not_le_Sn_O n1 H2)
 168         ]
 169       ]
 170     | cut (neg (S n1) < y \to (Zsucc (neg (S n1))) \leq y)
 171       [ auto
 172         (*apply Hcut.
 173         assumption*)
 174       | simplify.
 175         elim y
 176         [ simplify.
 177           exact I
 178         | simplify.
 179           exact I
 180         | simplify.
 181           (*qui auto non chiude il goal*)
 182           apply (le_S_S_to_le n2 n1 H3)
 183         ]
 184       ]
 185     ]
 186   ]
 187 ]
 188 qed.