helm/software/matita/contribs/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_autobatch/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 interpretation "integer 'less or equal to'" 'leq x y = (Zle x y).
  40 interpretation "integer 'neither less nor equal to'" 'nleq x y = (Not (Zle x y)).
  41
  42 definition Zlt : Z \to Z \to Prop \def
  43 \lambda x,y:Z.
  44   match x with
  45   [ OZ \Rightarrow
  46     match y with
  47     [ OZ \Rightarrow False
  48     | (pos m) \Rightarrow True
  49     | (neg m) \Rightarrow False ]
  50   | (pos n) \Rightarrow
  51     match y with
  52     [ OZ \Rightarrow False
  53     | (pos m) \Rightarrow n<m
  54     | (neg m) \Rightarrow False ]
  55   | (neg n) \Rightarrow
  56     match y with
  57     [ OZ \Rightarrow True
  58     | (pos m) \Rightarrow True
  59     | (neg m) \Rightarrow m<n ]].
  60
  61 interpretation "integer 'less than'" 'lt x y = (Zlt x y).
  62 interpretation "integer 'not less than'" 'nless x y = (Not (Zlt x y)).
  63
  64 theorem irreflexive_Zlt: irreflexive Z Zlt.
  65 unfold irreflexive.
  66 unfold Not.
  67 intro.
  68 elim x
  69 [ (*qui autobatch non chiude il goal*)
  70   exact H
  71 | cut (neg n < neg n \to False)
  72   [ apply Hcut.
  73     (*qui autobatch non chiude il goal*)
  74     apply H
  75   | autobatch
  76     (*simplify.
  77     unfold lt.
  78     apply not_le_Sn_n*)
  79   ]
  80 | cut (pos n < pos n \to False)
  81   [ apply Hcut.
  82     (*qui autobatch non chiude il goal*)
  83     apply H
  84   | autobatch
  85     (*simplify.
  86     unfold lt.
  87     apply not_le_Sn_n*)
  88   ]
  89 ]
  90 qed.
  91
  92 theorem irrefl_Zlt: irreflexive Z Zlt
  93 \def irreflexive_Zlt.
  94
  95 theorem Zlt_neg_neg_to_lt:
  96 \forall n,m:nat. neg n < neg m \to m < n.
  97 intros.
  98 (*qui autobatch non chiude il goal*)
  99 apply H.
 100 qed.
 101
 102 theorem lt_to_Zlt_neg_neg: \forall n,m:nat.m < n \to neg n < neg m.
 103 intros.
 104 simplify.
 105 apply H.
 106 qed.
 107
 108 theorem Zlt_pos_pos_to_lt:
 109 \forall n,m:nat. pos n < pos m \to n < m.
 110 intros.
 111 (*qui autobatch non chiude il goal*)
 112 apply H.
 113 qed.
 114
 115 theorem lt_to_Zlt_pos_pos: \forall n,m:nat.n < m \to pos n < pos m.
 116 intros.
 117 simplify.
 118 apply H.
 119 qed.
 120
 121 theorem Zlt_to_Zle: \forall x,y:Z. x < y \to Zsucc x \leq y.
 122 intros 2.
 123 elim x
 124 [ (* goal: x=OZ *)
 125   cut (OZ < y \to Zsucc OZ \leq y)
 126   [ autobatch
 127     (*apply Hcut.
 128     assumption*)
 129   | simplify.
 130     elim y
 131     [ simplify.
 132       (*qui autobatch non chiude il goal*)
 133       exact H1
 134     | simplify.
 135       apply le_O_n
 136     | simplify.
 137       (*qui autobatch non chiude il goal*)
 138       exact H1
 139     ]
 140   ]
 141 | (* goal: x=pos *)
 142   exact H
 143 | (* goal: x=neg *)
 144   cut (neg n < y \to Zsucc (neg n) \leq y)
 145   [ autobatch
 146     (*apply Hcut.
 147     assumption*)
 148   | elim n
 149     [ cut (neg O < y \to Zsucc (neg O) \leq y)
 150       [ autobatch
 151         (*apply Hcut.
 152         assumption*)
 153       | simplify.
 154         elim y
 155         [ simplify.
 156           exact I
 157         | simplify.
 158           exact I
 159         | simplify.
 160           (*qui autobatch non chiude il goal*)
 161           apply (not_le_Sn_O n1 H2)
 162         ]
 163       ]
 164     | cut (neg (S n1) < y \to (Zsucc (neg (S n1))) \leq y)
 165       [ autobatch
 166         (*apply Hcut.
 167         assumption*)
 168       | simplify.
 169         elim y
 170         [ simplify.
 171           exact I
 172         | simplify.
 173           exact I
 174         | simplify.
 175           (*qui autobatch non chiude il goal*)
 176           apply (le_S_S_to_le n2 n1 H3)
 177         ]
 178       ]
 179     ]
 180   ]
 181 ]
 182 qed.