1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/Z/orders".
19 definition Zle : Z \to Z \to Prop \def
25 | (pos m) \Rightarrow True
26 | (neg m) \Rightarrow False ]
29 [ OZ \Rightarrow False
30 | (pos m) \Rightarrow (le n m)
31 | (neg m) \Rightarrow False ]
35 | (pos m) \Rightarrow True
36 | (neg m) \Rightarrow (le m n) ]].
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 (*CSC: this alias must disappear: there is a bug in the generation of the .moos *)
41 alias symbol "leq" (instance 0) = "integer 'less or equal to'".
43 definition Zlt : Z \to Z \to Prop \def
48 [ OZ \Rightarrow False
49 | (pos m) \Rightarrow True
50 | (neg m) \Rightarrow False ]
53 [ OZ \Rightarrow False
54 | (pos m) \Rightarrow (lt n m)
55 | (neg m) \Rightarrow False ]
59 | (pos m) \Rightarrow True
60 | (neg m) \Rightarrow (lt m n) ]].
62 (*CSC: the URI must disappear: there is a bug now *)
63 interpretation "integer 'less than'" 'lt x y = (cic:/matita/Z/orders/Zlt.con x y).
64 (*CSC: this alias must disappear: there is a bug in the generation of the .moos *)
65 alias symbol "lt" (instance 0) = "integer 'less than'".
67 theorem irreflexive_Zlt: irreflexive Z Zlt.
68 change with \forall x:Z. x < x \to False.
70 cut neg n < neg n \to False.
71 apply Hcut.apply H.simplify.apply not_le_Sn_n.
72 cut pos n < pos n \to False.
73 apply Hcut.apply H.simplify.apply not_le_Sn_n.
76 theorem irrefl_Zlt: irreflexive Z Zlt
79 definition Z_compare : Z \to Z \to compare \def
85 | (pos m) \Rightarrow LT
86 | (neg m) \Rightarrow GT ]
90 | (pos m) \Rightarrow (nat_compare n m)
91 | (neg m) \Rightarrow GT]
95 | (pos m) \Rightarrow LT
96 | (neg m) \Rightarrow nat_compare m n ]].
98 theorem Zlt_neg_neg_to_lt:
99 \forall n,m:nat. neg n < neg m \to lt m n.
103 theorem lt_to_Zlt_neg_neg: \forall n,m:nat.lt m n \to neg n < neg m.
108 theorem Zlt_pos_pos_to_lt:
109 \forall n,m:nat. pos n < pos m \to lt n m.
113 theorem lt_to_Zlt_pos_pos: \forall n,m:nat.lt n m \to pos n < pos m.
118 theorem Z_compare_to_Prop :
119 \forall x,y:Z. match (Z_compare x y) with
120 [ LT \Rightarrow x < y
122 | GT \Rightarrow y < x].
125 simplify.apply refl_eq.
128 elim y. simplify.exact I.
130 cut match (nat_compare n1 n) with
131 [ LT \Rightarrow (lt n1 n)
132 | EQ \Rightarrow (eq nat n1 n)
133 | GT \Rightarrow (lt n n1)] \to
134 match (nat_compare n1 n) with
135 [ LT \Rightarrow (le (S n1) n)
136 | EQ \Rightarrow (eq Z (neg n) (neg n1))
137 | GT \Rightarrow (le (S n) n1)].
138 apply Hcut. apply nat_compare_to_Prop.
139 elim (nat_compare n1 n).
142 simplify.apply eq_f.apply sym_eq.exact H.
144 elim y.simplify.exact I.
147 cut match (nat_compare n n1) with
148 [ LT \Rightarrow (lt n n1)
149 | EQ \Rightarrow (eq nat n n1)
150 | GT \Rightarrow (lt n1 n)] \to
151 match (nat_compare n n1) with
152 [ LT \Rightarrow (le (S n) n1)
153 | EQ \Rightarrow (eq Z (pos n) (pos n1))
154 | GT \Rightarrow (le (S n1) n)].
155 apply Hcut. apply nat_compare_to_Prop.
156 elim (nat_compare n n1).
159 simplify.apply eq_f.exact H.
162 theorem Zlt_to_Zle: \forall x,y:Z. x < y \to Zsucc x \leq y.
164 cut OZ < y \to Zsucc OZ \leq y.
165 apply Hcut. assumption.simplify.elim y.
168 simplify.apply le_O_n.
169 cut neg n < y \to Zsucc (neg n) \leq y.
170 apply Hcut. assumption.elim n.
171 cut neg O < y \to Zsucc (neg O) \leq y.
172 apply Hcut. assumption.simplify.elim y.
173 simplify.exact I.simplify.apply not_le_Sn_O n1 H2.
175 cut neg (S n1) < y \to (Zsucc (neg (S n1))) \leq y.
176 apply Hcut. assumption.simplify.
179 simplify.apply le_S_S_to_le n2 n1 H3.