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/compare".
17 include "Z/orders.ma".
18 include "nat/compare.ma".
19 include "datatypes/bool.ma".
20 include "datatypes/compare.ma".
22 (* boolean equality *)
23 definition eqZb : Z \to Z \to bool \def
29 | (pos q) \Rightarrow false
30 | (neg q) \Rightarrow false]
33 [ OZ \Rightarrow false
34 | (pos q) \Rightarrow eqb p q
35 | (neg q) \Rightarrow false]
38 [ OZ \Rightarrow false
39 | (pos q) \Rightarrow false
40 | (neg q) \Rightarrow eqb p q]].
45 [ true \Rightarrow x=y
46 | false \Rightarrow \lnot x=y].
50 simplify.apply not_eq_OZ_neg.
51 simplify.apply not_eq_OZ_pos.
53 simplify.intro.apply not_eq_OZ_neg n ?.apply sym_eq.assumption.
54 simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption.
55 intro.simplify.intro.apply H.apply inj_neg.assumption.
56 simplify.intro.apply not_eq_pos_neg n1 n ?.apply sym_eq.assumption.
58 simplify.intro.apply not_eq_OZ_pos n ?.apply sym_eq.assumption.
59 simplify.apply not_eq_pos_neg.
60 simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption.
61 intro.simplify.intro.apply H.apply inj_pos.assumption.
64 theorem eqZb_elim: \forall x,y:Z.\forall P:bool \to Prop.
65 (x=y \to (P true)) \to (\lnot x=y \to (P false)) \to P (eqZb x y).
69 [ true \Rightarrow x=y
70 | false \Rightarrow \lnot x=y] \to P (eqZb x y).
78 definition Z_compare : Z \to Z \to compare \def
84 | (pos m) \Rightarrow LT
85 | (neg m) \Rightarrow GT ]
89 | (pos m) \Rightarrow (nat_compare n m)
90 | (neg m) \Rightarrow GT]
94 | (pos m) \Rightarrow LT
95 | (neg m) \Rightarrow nat_compare m n ]].
97 theorem Z_compare_to_Prop :
98 \forall x,y:Z. match (Z_compare x y) with
99 [ LT \Rightarrow x < y
101 | GT \Rightarrow y < x].
104 simplify.apply refl_eq.
107 elim y. simplify.exact I.
109 (*CSC: qui uso le perche' altrimenti ci sono troppe scelte
110 per via delle coercions! *)
111 cut match (nat_compare n1 n) with
112 [ LT \Rightarrow n1<n
113 | EQ \Rightarrow n1=n
114 | GT \Rightarrow n<n1] \to
115 match (nat_compare n1 n) with
116 [ LT \Rightarrow (le (S n1) n)
117 | EQ \Rightarrow neg n = neg n1
118 | GT \Rightarrow (le (S n) n1)].
119 apply Hcut. apply nat_compare_to_Prop.
120 elim (nat_compare n1 n).
123 simplify.apply eq_f.apply sym_eq.exact H.
125 elim y.simplify.exact I.
128 (*CSC: qui uso le perche' altrimenti ci sono troppe scelte
129 per via delle coercions! *)
130 cut match (nat_compare n n1) with
131 [ LT \Rightarrow n<n1
132 | EQ \Rightarrow n=n1
133 | GT \Rightarrow n1<n] \to
134 match (nat_compare n n1) with
135 [ LT \Rightarrow (le (S n) n1)
136 | EQ \Rightarrow pos n = pos n1
137 | GT \Rightarrow (le (S n1) n)].
138 apply Hcut. apply nat_compare_to_Prop.
139 elim (nat_compare n n1).
142 simplify.apply eq_f.exact H.