From: Andrea Asperti Date: Mon, 22 Aug 2005 08:09:37 +0000 (+0000) Subject: Added Z/plus.ma e Z/compare.ma. X-Git-Tag: working_equations_only~25 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=15753bd130b39be9854894898154163ba036d4b0;p=helm.git Added Z/plus.ma e Z/compare.ma. --- diff --git a/helm/matita/library/Z/compare.ma b/helm/matita/library/Z/compare.ma new file mode 100644 index 000000000..d2e075d26 --- /dev/null +++ b/helm/matita/library/Z/compare.ma @@ -0,0 +1,143 @@ +(**************************************************************************) +(* ___ *) +(* ||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 Zplus_z_OZ.reflexivity. +elim y.simplify.reflexivity. +simplify. +rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity. +simplify. +rewrite > nat_compare_n_m_m_n. +simplify.elim nat_compare ? ?.simplify.reflexivity. +simplify. reflexivity. +simplify. reflexivity. +elim y.simplify.reflexivity. +simplify.rewrite > nat_compare_n_m_m_n. +simplify.elim nat_compare ? ?.simplify.reflexivity. +simplify. reflexivity. +simplify. reflexivity. +simplify.rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity. +qed. + +theorem Zpred_Zplus_neg_O : \forall z:Z. Zpred z = (neg O)+z. +intros.elim z. +simplify.reflexivity. +simplify.reflexivity. +elim n.simplify.reflexivity. +simplify.reflexivity. +qed. + +theorem Zsucc_Zplus_pos_O : \forall z:Z. Zsucc z = (pos O)+z. +intros.elim z. +simplify.reflexivity. +elim n.simplify.reflexivity. +simplify.reflexivity. +simplify.reflexivity. +qed. + +theorem Zplus_pos_pos: +\forall n,m. (pos n)+(pos m) = (Zsucc (pos n))+(Zpred (pos m)). +intros. +elim n.elim m. +simplify.reflexivity. +simplify.reflexivity. +elim m. +simplify.rewrite < plus_n_Sm. +rewrite < plus_n_O.reflexivity. +simplify.rewrite < plus_n_Sm. +rewrite < plus_n_Sm.reflexivity. +qed. + +theorem Zplus_pos_neg: +\forall n,m. (pos n)+(neg m) = (Zsucc (pos n))+(Zpred (neg m)). +intros.reflexivity. +qed. + +theorem Zplus_neg_pos : +\forall n,m. (neg n)+(pos m) = (Zsucc (neg n))+(Zpred (pos m)). +intros. +elim n.elim m. +simplify.reflexivity. +simplify.reflexivity. +elim m. +simplify.reflexivity. +simplify.reflexivity. +qed. + +theorem Zplus_neg_neg: +\forall n,m. (neg n)+(neg m) = (Zsucc (neg n))+(Zpred (neg m)). +intros. +elim n.elim m. +simplify.reflexivity. +simplify.reflexivity. +elim m. +simplify.rewrite > plus_n_Sm.reflexivity. +simplify.rewrite > plus_n_Sm.reflexivity. +qed. + +theorem Zplus_Zsucc_Zpred: +\forall x,y. x+y = (Zsucc x)+(Zpred y). +intros. +elim x. elim y. +simplify.reflexivity. +simplify.reflexivity. +rewrite < Zsucc_Zplus_pos_O. +rewrite > Zsucc_Zpred.reflexivity. +elim y.rewrite < sym_Zplus.rewrite < sym_Zplus (Zpred OZ). +rewrite < Zpred_Zplus_neg_O. +rewrite > Zpred_Zsucc. +simplify.reflexivity. +rewrite < Zplus_neg_neg.reflexivity. +apply Zplus_neg_pos. +elim y.simplify.reflexivity. +apply Zplus_pos_neg. +apply Zplus_pos_pos. +qed. + +theorem Zplus_Zsucc_pos_pos : +\forall n,m. (Zsucc (pos n))+(pos m) = Zsucc ((pos n)+(pos m)). +intros.reflexivity. +qed. + +theorem Zplus_Zsucc_pos_neg: +\forall n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))). +intros. +apply nat_elim2 +(\lambda n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m)))).intro. +intros.elim n1. +simplify. reflexivity. +elim n2.simplify. reflexivity. +simplify. reflexivity. +intros. elim n1. +simplify. reflexivity. +simplify.reflexivity. +intros. +rewrite < (Zplus_pos_neg ? m1). +elim H.reflexivity. +qed. + +theorem Zplus_Zsucc_neg_neg : +\forall n,m. (Zsucc (neg n))+(neg m) = Zsucc ((neg n)+(neg m)). +intros. +apply nat_elim2 +(\lambda n,m. ((Zsucc (neg n))+(neg m)) = Zsucc ((neg n)+(neg m))).intro. +intros.elim n1. +simplify. reflexivity. +elim n2.simplify. reflexivity. +simplify. reflexivity. +intros. elim n1. +simplify. reflexivity. +simplify.reflexivity. +intros. +rewrite < (Zplus_neg_neg ? m1). +reflexivity. +qed. + +theorem Zplus_Zsucc_neg_pos: +\forall n,m. Zsucc (neg n)+(pos m) = Zsucc ((neg n)+(pos m)). +intros. +apply nat_elim2 +(\lambda n,m. (Zsucc (neg n))+(pos m) = Zsucc ((neg n)+(pos m))). +intros.elim n1. +simplify. reflexivity. +elim n2.simplify. reflexivity. +simplify. reflexivity. +intros. elim n1. +simplify. reflexivity. +simplify.reflexivity. +intros. +rewrite < H. +rewrite < (Zplus_neg_pos ? (S m1)). +reflexivity. +qed. + +theorem Zplus_Zsucc : \forall x,y:Z. (Zsucc x)+y = Zsucc (x+y). +intros.elim x.elim y. +simplify. reflexivity. +rewrite < Zsucc_Zplus_pos_O.reflexivity. +simplify.reflexivity. +elim y.rewrite < sym_Zplus.rewrite < sym_Zplus OZ.simplify.reflexivity. +apply Zplus_Zsucc_neg_neg. +apply Zplus_Zsucc_neg_pos. +elim y. +rewrite < sym_Zplus OZ.reflexivity. +apply Zplus_Zsucc_pos_neg. +apply Zplus_Zsucc_pos_pos. +qed. + +theorem Zplus_Zpred: \forall x,y:Z. (Zpred x)+y = Zpred (x+y). +intros. +cut Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y). +rewrite > Hcut. +rewrite > Zplus_Zsucc. +rewrite > Zpred_Zsucc. +reflexivity. +rewrite > Zsucc_Zpred. +reflexivity. +qed. + + +theorem associative_Zplus: associative Z Zplus. +change with \forall x,y,z:Z. (x + y) + z = x + (y + z). +(* simplify. *) +intros.elim x.simplify.reflexivity. +elim n.rewrite < (Zpred_Zplus_neg_O (y+z)). +rewrite < (Zpred_Zplus_neg_O y). +rewrite < Zplus_Zpred. +reflexivity. +rewrite > Zplus_Zpred (neg n1). +rewrite > Zplus_Zpred (neg n1). +rewrite > Zplus_Zpred ((neg n1)+y). +apply eq_f.assumption. +elim n.rewrite < Zsucc_Zplus_pos_O. +rewrite < Zsucc_Zplus_pos_O. +rewrite > Zplus_Zsucc. +reflexivity. +rewrite > Zplus_Zsucc (pos n1). +rewrite > Zplus_Zsucc (pos n1). +rewrite > Zplus_Zsucc ((pos n1)+y). +apply eq_f.assumption. +qed. + +variant assoc_Zplus : \forall x,y,z:Z. (x+y)+z = x+(y+z) +\def associative_Zplus. + +(* Zopp *) +definition Zopp : Z \to Z \def +\lambda x:Z. match x with +[ OZ \Rightarrow OZ +| (pos n) \Rightarrow (neg n) +| (neg n) \Rightarrow (pos n) ]. + +(*CSC: the URI must disappear: there is a bug now *) +interpretation "integer unary minus" 'uminus x = (cic:/matita/Z/plus/Zopp.con x). + +theorem Zopp_Zplus: \forall x,y:Z. -(x+y) = -x + -y. +intros. +elim x.elim y. +simplify. reflexivity. +simplify. reflexivity. +simplify. reflexivity. +elim y. +simplify. reflexivity. +simplify. reflexivity. +simplify. apply nat_compare_elim. +intro.simplify.reflexivity. +intro.simplify.reflexivity. +intro.simplify.reflexivity. +elim y. +simplify. reflexivity. +simplify. apply nat_compare_elim. +intro.simplify.reflexivity. +intro.simplify.reflexivity. +intro.simplify.reflexivity. +simplify.reflexivity. +qed. + +(* --x non gli piace, ma lo stampa *) +theorem Zopp_Zopp: \forall x:Z. -(-x) = x. +intro. elim x. +reflexivity.reflexivity.reflexivity. +qed. + +theorem Zplus_Zopp: \forall x:Z. x+ -x = OZ. +intro.elim x. +apply refl_eq. +simplify. +rewrite > nat_compare_n_n. +simplify.apply refl_eq. +simplify. +rewrite > nat_compare_n_n. +simplify.apply refl_eq. +qed. +