From: Andrea Asperti <andrea.asperti@unibo.it>
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<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.
diff --git a/helm/matita/library/Z/plus.ma b/helm/matita/library/Z/plus.ma
new file mode 100644
index 000000000..b1942d209
--- /dev/null
+++ b/helm/matita/library/Z/plus.ma
@@ -0,0 +1,305 @@
+(**************************************************************************)
+(*       ___	                                                            *)
+(*      ||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/plus".
+
+include "Z/z.ma".
+include "nat/compare.ma".
+include "nat/minus.ma".
+
+definition Zplus :Z \to Z \to Z \def
+\lambda x,y.
+  match x with
+    [ OZ \Rightarrow y
+    | (pos m) \Rightarrow
+        match y with
+         [ OZ \Rightarrow x
+         | (pos n) \Rightarrow (pos (pred ((S m)+(S n))))
+         | (neg n) \Rightarrow 
+              match nat_compare m n with
+                [ LT \Rightarrow (neg (pred (n-m)))
+                | EQ \Rightarrow OZ
+                | GT \Rightarrow (pos (pred (m-n)))]]
+    | (neg m) \Rightarrow
+        match y with
+         [ OZ \Rightarrow x
+         | (pos n) \Rightarrow 
+              match nat_compare m n with
+                [ LT \Rightarrow (pos (pred (n-m)))
+                | EQ \Rightarrow OZ
+                | GT \Rightarrow (neg (pred (m-n)))]     
+         | (neg n) \Rightarrow (neg (pred ((S m)+(S n))))]].
+
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "integer plus" 'plus x y = (cic:/matita/Z/plus/Zplus.con x y).
+         
+theorem Zplus_z_OZ:  \forall z:Z. z+OZ = z.
+intro.elim z.
+simplify.reflexivity.
+simplify.reflexivity.
+simplify.reflexivity.
+qed.
+
+(* theorem symmetric_Zplus: symmetric Z Zplus. *)
+
+theorem sym_Zplus : \forall x,y:Z. x+y = y+x.
+intros.elim x.rewrite > 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.
+