+++ /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".
-
-(* 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 x \neq y].
-intros.
-elim x.
- elim y.
- simplify.reflexivity.
- simplify.apply not_eq_OZ_pos.
- simplify.apply not_eq_OZ_neg.
- elim y.
- simplify.unfold Not.intro.apply (not_eq_OZ_pos n).apply sym_eq.assumption.
- simplify.apply eqb_elim.
- intro.simplify.apply eq_f.assumption.
- intro.simplify.unfold Not.intro.apply H.apply inj_pos.assumption.
- simplify.apply not_eq_pos_neg.
- elim y.
- simplify.unfold Not.intro.apply (not_eq_OZ_neg n).apply sym_eq.assumption.
- simplify.unfold Not.intro.apply (not_eq_pos_neg n1 n).apply sym_eq.assumption.
- simplify.apply eqb_elim.
- intro.simplify.apply eq_f.assumption.
- intro.simplify.unfold Not.intro.apply H.apply inj_neg.assumption.
-qed.
-
-theorem eqZb_elim: \forall x,y:Z.\forall P:bool \to Prop.
-(x=y \to (P true)) \to (x \neq y \to (P false)) \to P (eqZb x y).
-intros.
-cut
-(match (eqZb x y) with
-[ true \Rightarrow x=y
-| false \Rightarrow x \neq 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.
- 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 (S n) \leq n1
- | EQ \Rightarrow pos n = pos n1
- | GT \Rightarrow (S n1) \leq n]).
- apply Hcut.apply nat_compare_to_Prop.
- elim (nat_compare n n1).
- simplify.exact H.
- simplify.apply eq_f.exact H.
- simplify.exact H.
- simplify.exact I.
- elim y.
- simplify.exact I.
- simplify.exact I.
- simplify.
- 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 (S n1) \leq n
- | EQ \Rightarrow neg n = neg n1
- | GT \Rightarrow (S n) \leq n1]).
- apply Hcut. apply nat_compare_to_Prop.
- elim (nat_compare n1 n).
- simplify.exact H.
- simplify.apply eq_f.apply sym_eq.exact H.
- simplify.exact H.
-qed.