--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
+(* ||A|| E.Tassi, S.Zacchiroli *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU Lesser General Public License Version 2.1 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/Z/compare".
+
+include "Z/orders.ma".
+include "nat/compare.ma".
+include "datatypes/bool.ma".
+include "datatypes/compare.ma".
+
+(* boolean equality *)
+definition eqZb : Z \to Z \to bool \def
+\lambda x,y:Z.
+ match x with
+ [ OZ \Rightarrow
+ match y with
+ [ OZ \Rightarrow true
+ | (pos q) \Rightarrow false
+ | (neg q) \Rightarrow false]
+ | (pos p) \Rightarrow
+ match y with
+ [ OZ \Rightarrow false
+ | (pos q) \Rightarrow eqb p q
+ | (neg q) \Rightarrow false]
+ | (neg p) \Rightarrow
+ match y with
+ [ OZ \Rightarrow false
+ | (pos q) \Rightarrow false
+ | (neg q) \Rightarrow eqb p q]].
+
+theorem eqZb_to_Prop:
+\forall x,y:Z.
+match eqZb x y with
+[ true \Rightarrow x=y
+| false \Rightarrow \lnot x=y].
+intros.elim x.
+elim y.
+simplify.reflexivity.
+simplify.apply not_eq_OZ_neg.
+simplify.apply not_eq_OZ_pos.
+elim y.
+simplify.intro.apply not_eq_OZ_neg n ?.apply sym_eq.assumption.
+simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption.
+intro.simplify.intro.apply H.apply inj_neg.assumption.
+simplify.intro.apply not_eq_pos_neg n1 n ?.apply sym_eq.assumption.
+elim y.
+simplify.intro.apply not_eq_OZ_pos n ?.apply sym_eq.assumption.
+simplify.apply not_eq_pos_neg.
+simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption.
+intro.simplify.intro.apply H.apply inj_pos.assumption.
+qed.
+
+theorem eqZb_elim: \forall x,y:Z.\forall P:bool \to Prop.
+(x=y \to (P true)) \to (\lnot x=y \to (P false)) \to P (eqZb x y).
+intros.
+cut
+match (eqZb x y) with
+[ true \Rightarrow x=y
+| false \Rightarrow \lnot x=y] \to P (eqZb x y).
+apply Hcut.
+apply eqZb_to_Prop.
+elim (eqZb).
+apply H H2.
+apply H1 H2.
+qed.
+
+definition Z_compare : Z \to Z \to compare \def
+\lambda x,y:Z.
+ match x with
+ [ OZ \Rightarrow
+ match y with
+ [ OZ \Rightarrow EQ
+ | (pos m) \Rightarrow LT
+ | (neg m) \Rightarrow GT ]
+ | (pos n) \Rightarrow
+ match y with
+ [ OZ \Rightarrow GT
+ | (pos m) \Rightarrow (nat_compare n m)
+ | (neg m) \Rightarrow GT]
+ | (neg n) \Rightarrow
+ match y with
+ [ OZ \Rightarrow LT
+ | (pos m) \Rightarrow LT
+ | (neg m) \Rightarrow nat_compare m n ]].
+
+theorem Z_compare_to_Prop :
+\forall x,y:Z. match (Z_compare x y) with
+[ LT \Rightarrow x < y
+| EQ \Rightarrow x=y
+| GT \Rightarrow y < x].
+intros.
+elim x. elim y.
+simplify.apply refl_eq.
+simplify.exact I.
+simplify.exact I.
+elim y. simplify.exact I.
+simplify.
+(*CSC: qui uso le perche' altrimenti ci sono troppe scelte
+ per via delle coercions! *)
+cut match (nat_compare n1 n) with
+[ LT \Rightarrow n1<n
+| EQ \Rightarrow n1=n
+| GT \Rightarrow n<n1] \to
+match (nat_compare n1 n) with
+[ LT \Rightarrow (le (S n1) n)
+| EQ \Rightarrow neg n = neg n1
+| GT \Rightarrow (le (S n) n1)].
+apply Hcut. apply nat_compare_to_Prop.
+elim (nat_compare n1 n).
+simplify.exact H.
+simplify.exact H.
+simplify.apply eq_f.apply sym_eq.exact H.
+simplify.exact I.
+elim y.simplify.exact I.
+simplify.exact I.
+simplify.
+(*CSC: qui uso le perche' altrimenti ci sono troppe scelte
+ per via delle coercions! *)
+cut match (nat_compare n n1) with
+[ LT \Rightarrow n<n1
+| EQ \Rightarrow n=n1
+| GT \Rightarrow n1<n] \to
+match (nat_compare n n1) with
+[ LT \Rightarrow (le (S n) n1)
+| EQ \Rightarrow pos n = pos n1
+| GT \Rightarrow (le (S n1) n)].
+apply Hcut. apply nat_compare_to_Prop.
+elim (nat_compare n n1).
+simplify.exact H.
+simplify.exact H.
+simplify.apply eq_f.exact H.
+qed.