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 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
  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 (*CSC: the URI must disappear: there is a bug now *)
  62 interpretation "integer 'less than'" 'lt x y = (cic:/matita/Z/orders/Zlt.con x y).
  63
  64 theorem irreflexive_Zlt: irreflexive Z Zlt.
  65 change with \forall x:Z. x < x \to False.
  66 intro.elim x.exact H.
  67 cut neg n < neg n \to False.
  68 apply Hcut.apply H.simplify.apply not_le_Sn_n.
  69 cut pos n < pos n \to False.
  70 apply Hcut.apply H.simplify.apply not_le_Sn_n.
  71 qed.
  72
  73 theorem irrefl_Zlt: irreflexive Z Zlt
  74 \def irreflexive_Zlt.
  75
  76 (*CSC: qui uso lt perche' ho due istanze diverse di < *)
  77 theorem Zlt_neg_neg_to_lt:
  78 \forall n,m:nat. neg n < neg m \to lt m n.
  79 intros.apply H.
  80 qed.
  81
  82 (*CSC: qui uso lt perche' ho due istanze diverse di < *)
  83 theorem lt_to_Zlt_neg_neg: \forall n,m:nat.lt m n \to neg n < neg m.
  84 intros.
  85 simplify.apply H.
  86 qed.
  87
  88 (*CSC: qui uso lt perche' ho due istanze diverse di < *)
  89 theorem Zlt_pos_pos_to_lt:
  90 \forall n,m:nat. pos n < pos m \to lt n m.
  91 intros.apply H.
  92 qed.
  93
  94 (*CSC: qui uso lt perche' ho due istanze diverse di < *)
  95 theorem lt_to_Zlt_pos_pos: \forall n,m:nat.lt n m \to pos n < pos m.
  96 intros.
  97 simplify.apply H.
  98 qed.
  99
 100 theorem Zlt_to_Zle: \forall x,y:Z. x < y \to Zsucc x \leq y.
 101 intros 2.elim x.
 102 cut OZ < y \to Zsucc OZ \leq y.
 103 apply Hcut. assumption.simplify.elim y.
 104 simplify.exact H1.
 105 simplify.exact H1.
 106 simplify.apply le_O_n.
 107 cut neg n < y \to Zsucc (neg n) \leq y.
 108 apply Hcut. assumption.elim n.
 109 cut neg O < y \to Zsucc (neg O) \leq y.
 110 apply Hcut. assumption.simplify.elim y.
 111 simplify.exact I.simplify.apply not_le_Sn_O n1 H2.
 112 simplify.exact I.
 113 cut neg (S n1) < y \to (Zsucc (neg (S n1))) \leq y.
 114 apply Hcut. assumption.simplify.
 115 elim y.
 116 simplify.exact I.
 117 simplify.apply le_S_S_to_le n2 n1 H3.
 118 simplify.exact I.
 119 exact H.
 120 qed.