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) ]].
39 definition Zlt : Z \to Z \to Prop \def
44 [ OZ \Rightarrow False
45 | (pos m) \Rightarrow True
46 | (neg m) \Rightarrow False ]
49 [ OZ \Rightarrow False
50 | (pos m) \Rightarrow (lt n m)
51 | (neg m) \Rightarrow False ]
55 | (pos m) \Rightarrow True
56 | (neg m) \Rightarrow (lt m n) ]].
58 theorem irreflexive_Zlt: irreflexive Z Zlt.
59 change with \forall x:Z. Zlt x x \to False.
61 cut (Zlt (neg n) (neg n)) \to False.
62 apply Hcut.apply H.simplify.apply not_le_Sn_n.
63 cut (Zlt (pos n) (pos n)) \to False.
64 apply Hcut.apply H.simplify.apply not_le_Sn_n.
67 theorem irrefl_Zlt: irreflexive Z Zlt
70 definition Z_compare : Z \to Z \to compare \def
76 | (pos m) \Rightarrow LT
77 | (neg m) \Rightarrow GT ]
81 | (pos m) \Rightarrow (nat_compare n m)
82 | (neg m) \Rightarrow GT]
86 | (pos m) \Rightarrow LT
87 | (neg m) \Rightarrow nat_compare m n ]].
89 theorem Zlt_neg_neg_to_lt:
90 \forall n,m:nat. Zlt (neg n) (neg m) \to lt m n.
94 theorem lt_to_Zlt_neg_neg: \forall n,m:nat.lt m n \to Zlt (neg n) (neg m).
99 theorem Zlt_pos_pos_to_lt:
100 \forall n,m:nat. Zlt (pos n) (pos m) \to lt n m.
104 theorem lt_to_Zlt_pos_pos: \forall n,m:nat.lt n m \to Zlt (pos n) (pos m).
109 theorem Z_compare_to_Prop :
110 \forall x,y:Z. match (Z_compare x y) with
111 [ LT \Rightarrow (Zlt x y)
112 | EQ \Rightarrow (eq Z x y)
113 | GT \Rightarrow (Zlt y x)].
116 simplify.apply refl_eq.
119 elim y. simplify.exact I.
121 cut match (nat_compare n1 n) with
122 [ LT \Rightarrow (lt n1 n)
123 | EQ \Rightarrow (eq nat n1 n)
124 | GT \Rightarrow (lt n n1)] \to
125 match (nat_compare n1 n) with
126 [ LT \Rightarrow (le (S n1) n)
127 | EQ \Rightarrow (eq Z (neg n) (neg n1))
128 | GT \Rightarrow (le (S n) n1)].
129 apply Hcut. apply nat_compare_to_Prop.
130 elim (nat_compare n1 n).
133 simplify.apply eq_f.apply sym_eq.exact H.
135 elim y.simplify.exact I.
138 cut match (nat_compare n n1) with
139 [ LT \Rightarrow (lt n n1)
140 | EQ \Rightarrow (eq nat n n1)
141 | GT \Rightarrow (lt n1 n)] \to
142 match (nat_compare n n1) with
143 [ LT \Rightarrow (le (S n) n1)
144 | EQ \Rightarrow (eq Z (pos n) (pos n1))
145 | GT \Rightarrow (le (S n1) n)].
146 apply Hcut. apply nat_compare_to_Prop.
147 elim (nat_compare n n1).
150 simplify.apply eq_f.exact H.
153 theorem Zlt_to_Zle: \forall x,y:Z. Zlt x y \to Zle (Zsucc x) y.
155 cut (Zlt OZ y) \to (Zle (Zsucc OZ) y).
156 apply Hcut. assumption.simplify.elim y.
159 simplify.apply le_O_n.
160 cut (Zlt (neg n) y) \to (Zle (Zsucc (neg n)) y).
161 apply Hcut. assumption.elim n.
162 cut (Zlt (neg O) y) \to (Zle (Zsucc (neg O)) y).
163 apply Hcut. assumption.simplify.elim y.
164 simplify.exact I.simplify.apply not_le_Sn_O n1 H2.
166 cut (Zlt (neg (S n1)) y) \to (Zle (Zsucc (neg (S n1))) y).
167 apply Hcut. assumption.simplify.
170 simplify.apply le_S_S_to_le n2 n1 H3.