X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2FZ%2Ftimes.ma;h=e5e1cdb452fa38ce33a8ba73f95b6ca4a5d5f27d;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=688957e57396cecb7fd0143c60f171640024b743;hpb=03fcee16d9c262aad38a47d0a409b684a965cc3f;p=helm.git

diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma
index 688957e57..e5e1cdb45 100644
--- a/helm/matita/library/Z/times.ma
+++ b/helm/matita/library/Z/times.ma
@@ -16,7 +16,6 @@ set "baseuri" "cic:/matita/Z/times".
 
 include "nat/lt_arith.ma".
 include "Z/plus.ma".
-include "higher_order_defs/functions.ma".
 
 definition Ztimes :Z \to Z \to Z \def
 \lambda x,y.
@@ -25,13 +24,13 @@ definition Ztimes :Z \to Z \to Z \def
     | (pos m) \Rightarrow
         match y with
          [ OZ \Rightarrow OZ
-         | (pos n) \Rightarrow (pos (pred (times (S m) (S n))))
-         | (neg n) \Rightarrow (neg (pred (times (S m) (S n))))]
+         | (pos n) \Rightarrow (pos (pred ((S m) * (S n))))
+         | (neg n) \Rightarrow (neg (pred ((S m) * (S n))))]
     | (neg m) \Rightarrow
         match y with
          [ OZ \Rightarrow OZ
-         | (pos n) \Rightarrow (neg (pred (times (S m) (S n))))
-         | (neg n) \Rightarrow (pos (pred (times (S m) (S n))))]].
+         | (pos n) \Rightarrow (neg (pred ((S m) * (S n))))
+         | (neg n) \Rightarrow (pos (pred ((S m) * (S n))))]].
          
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "integer times" 'times x y = (cic:/matita/Z/times/Ztimes.con x y).
@@ -43,104 +42,105 @@ simplify.reflexivity.
 simplify.reflexivity.
 qed.
 
-theorem Ztimes_neg_Zopp: \forall n:nat.\forall x:Z. 
-eq Z (Ztimes (neg n) x) (Zopp (Ztimes (pos n) x)).
+theorem Ztimes_neg_Zopp: \forall n:nat.\forall x:Z.
+neg n * x = - (pos n * x).
 intros.elim x.
 simplify.reflexivity.
 simplify.reflexivity.
 simplify.reflexivity.
 qed.
 theorem symmetric_Ztimes : symmetric Z Ztimes.
-change with \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x).
+change with (\forall x,y:Z. x*y = y*x).
 intros.elim x.rewrite > Ztimes_z_OZ.reflexivity.
 elim y.simplify.reflexivity. 
-change with eq Z (pos (pred (times (S n) (S n1)))) (pos (pred (times (S n1) (S n)))).
+change with (pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n)))).
 rewrite < sym_times.reflexivity.
-change with eq Z (neg (pred (times (S n) (S n1)))) (neg (pred (times (S n1) (S n)))).
+change with (neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n)))).
 rewrite < sym_times.reflexivity.
 elim y.simplify.reflexivity.
-change with eq Z (neg (pred (times (S n) (S n1)))) (neg (pred (times (S n1) (S n)))).
+change with (neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n)))).
 rewrite < sym_times.reflexivity.
-change with eq Z (pos (pred (times (S n) (S n1)))) (pos (pred (times (S n1) (S n)))).
+change with (pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n)))).
 rewrite < sym_times.reflexivity.
 qed.
 
-variant sym_Ztimes : \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x)
+variant sym_Ztimes : \forall x,y:Z. x*y = y*x
 \def symmetric_Ztimes.
 
 theorem associative_Ztimes: associative Z Ztimes.
-change with \forall x,y,z:Z.eq Z (Ztimes (Ztimes x y) z) (Ztimes x (Ztimes y z)).
-intros.
-elim x.simplify.reflexivity.
-elim y.simplify.reflexivity.
-elim z.simplify.reflexivity.
-change with 
-eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
-     (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
-apply lt_O_times_S_S.
-apply lt_O_times_S_S.
-change with 
-eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
-     (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
-apply lt_O_times_S_S.apply lt_O_times_S_S.
-elim z.simplify.reflexivity.
-change with 
-eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
-     (pos(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
-apply lt_O_times_S_S.apply lt_O_times_S_S.
-change with 
-eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
-     (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
-apply lt_O_times_S_S.
-apply lt_O_times_S_S.
-elim y.simplify.reflexivity.
-elim z.simplify.reflexivity.
-change with 
-eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
-     (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
-apply lt_O_times_S_S.
-apply lt_O_times_S_S.
-change with 
-eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
-     (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
-apply lt_O_times_S_S.apply lt_O_times_S_S.
-elim z.simplify.reflexivity.
-change with 
-eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
-     (neg(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
-apply lt_O_times_S_S.apply lt_O_times_S_S.
-change with 
-eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
-     (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
-apply lt_O_times_S_S.
-apply lt_O_times_S_S.
+change with (\forall x,y,z:Z. (x*y)*z = x*(y*z)).
+intros.elim x.
+  simplify.reflexivity. 
+  elim y.
+    simplify.reflexivity.
+    elim z.
+      simplify.reflexivity.
+      change with 
+       (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+       pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
+         apply lt_O_times_S_S.apply lt_O_times_S_S.
+      change with 
+       (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+       neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
+         apply lt_O_times_S_S.apply lt_O_times_S_S.
+    elim z.
+      simplify.reflexivity.
+      change with 
+       (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+       neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
+         apply lt_O_times_S_S.apply lt_O_times_S_S.
+      change with 
+       (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+       pos(pred ((S n) * (S (pred ((S n1) * (S n2))))))).
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
+        apply lt_O_times_S_S.apply lt_O_times_S_S.
+  elim y.
+    simplify.reflexivity.
+    elim z.
+      simplify.reflexivity.
+      change with 
+       (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+       neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
+         apply lt_O_times_S_S.apply lt_O_times_S_S.
+      change with 
+       (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+       pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
+         apply lt_O_times_S_S.apply lt_O_times_S_S.
+    elim z.
+      simplify.reflexivity.
+      change with 
+       (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+       pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
+         apply lt_O_times_S_S.apply lt_O_times_S_S.
+      change with 
+       (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+       neg(pred ((S n) * (S (pred ((S n1) * (S n2))))))).
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
+         apply lt_O_times_S_S.apply lt_O_times_S_S.
 qed.
 
 variant assoc_Ztimes : \forall x,y,z:Z. 
-eq Z (Ztimes (Ztimes x y) z) (Ztimes x (Ztimes y z)) \def 
+(x * y) * z = x * (y * z) \def 
 associative_Ztimes.
 
 lemma times_minus1: \forall n,p,q:nat. lt q p \to
-eq nat (times (S n) (S (pred (minus (S p) (S q)))))
-       (minus (pred (times (S n) (S p))) 
-              (pred (times (S n) (S q)))).
+(S n) * (S (pred ((S p) - (S q)))) =
+pred ((S n) * (S p)) - pred ((S n) * (S q)).
 intros.
-rewrite < S_pred ? ?.  
-rewrite > minus_pred_pred ? ? ? ?.
+rewrite < S_pred.  
+rewrite > minus_pred_pred.
 rewrite < distr_times_minus. 
-reflexivity.  
+reflexivity.
 (* we now close all positivity conditions *)
 apply lt_O_times_S_S.                    
 apply lt_O_times_S_S.
-simplify.
+simplify.unfold lt.
 apply le_SO_minus.  exact H.
 qed.
 
@@ -148,24 +148,22 @@ lemma Ztimes_Zplus_pos_neg_pos: \forall n,p,q:nat.
 (pos n)*((neg p)+(pos q)) = (pos n)*(neg p)+ (pos n)*(pos q). 
 intros.
 simplify. 
-change in match (plus p (times n (S p))) with (pred (times (S n) (S p))).
-change in match (plus q (times n (S q))) with (pred (times (S n) (S q))).
-rewrite < nat_compare_pred_pred ? ? ? ?.
+change in match (p + n * (S p)) with (pred ((S n) * (S p))).
+change in match (q + n * (S q)) with (pred ((S n) * (S q))).
+rewrite < nat_compare_pred_pred.
 rewrite < nat_compare_times_l.
 rewrite < nat_compare_S_S.
-apply nat_compare_elim p q.
+apply (nat_compare_elim p q).
 intro.
 (* uff *)
-change with (eq Z (pos (pred (times (S n) (S (pred (minus (S q) (S p)))))))
-           (pos (pred (minus (pred (times (S n) (S q)))
-                             (pred (times (S n) (S p))))))).
-rewrite < times_minus1 n q p H.reflexivity.
+change with (pos (pred ((S n) * (S (pred ((S q) - (S p)))))) =
+            pos (pred ((pred ((S n) * (S q))) - (pred ((S n) * (S p)))))).
+rewrite < (times_minus1 n q p H).reflexivity.
 intro.rewrite < H.simplify.reflexivity.
 intro.
-change with (eq Z (neg (pred (times (S n) (S (pred (minus (S p) (S q)))))))
-           (neg (pred (minus (pred (times (S n) (S p)))
-                             (pred (times (S n) (S q))))))). 
-rewrite < times_minus1 n p q H.reflexivity.                                 
+change with (neg (pred ((S n) * (S (pred ((S p) - (S q)))))) =
+            neg (pred ((pred ((S n) * (S p))) - (pred ((S n) * (S q)))))). 
+rewrite < (times_minus1 n p q H).reflexivity.                                 
 (* two more positivity conditions from nat_compare_pred_pred *)   
 apply lt_O_times_S_S.  
 apply lt_O_times_S_S. 
@@ -180,34 +178,35 @@ apply sym_Zplus.
 qed.
 
 lemma distributive2_Ztimes_pos_Zplus: 
-distributive2 nat Z (\lambda n,z. Ztimes (pos n) z) Zplus.
-change with \forall n,y,z.
-eq Z (Ztimes (pos n) (Zplus y z)) (Zplus (Ztimes (pos n) y) (Ztimes (pos n) z)).  
-intros.
-elim y.reflexivity.
-elim z.reflexivity.
-change with
-eq Z (neg (pred (times (S n) (plus (S n1) (S n2)))))
-     (neg (pred (plus (times (S n) (S n1))(times (S n) (S n2))))).
-rewrite < distr_times_plus.reflexivity.
-apply Ztimes_Zplus_pos_neg_pos.
-elim z.reflexivity.
-apply Ztimes_Zplus_pos_pos_neg.
-change with
-eq Z (pos (pred (times (S n) (plus (S n1) (S n2)))))
-     (pos (pred (plus (times (S n) (S n1))(times (S n) (S n2))))).
-rewrite < distr_times_plus. 
-reflexivity.
+distributive2 nat Z (\lambda n,z. (pos n) * z) Zplus.
+change with (\forall n,y,z.
+(pos n) * (y + z) = (pos n) * y + (pos n) * z).  
+intros.elim y.
+  reflexivity.
+  elim z.
+    reflexivity.
+    change with
+     (pos (pred ((S n) * ((S n1) + (S n2)))) =
+     pos (pred ((S n) * (S n1) + (S n) * (S n2)))).
+      rewrite < distr_times_plus.reflexivity.
+    apply Ztimes_Zplus_pos_pos_neg.
+  elim z.
+    reflexivity.
+    apply Ztimes_Zplus_pos_neg_pos.
+    change with
+     (neg (pred ((S n) * ((S n1) + (S n2)))) =
+     neg (pred ((S n) * (S n1) + (S n) * (S n2)))).
+    rewrite < distr_times_plus.reflexivity.
 qed.
 
 variant distr_Ztimes_Zplus_pos: \forall n,y,z.
-eq Z (Ztimes (pos n) (Zplus y z)) (Zplus (Ztimes (pos n) y) (Ztimes (pos n) z)) \def
+(pos n) * (y + z) = ((pos n) * y + (pos n) * z) \def
 distributive2_Ztimes_pos_Zplus.
 
 lemma distributive2_Ztimes_neg_Zplus : 
-distributive2 nat Z (\lambda n,z. Ztimes (neg n) z) Zplus.
-change with \forall n,y,z.
-eq Z (Ztimes (neg n) (Zplus y z)) (Zplus (Ztimes (neg n) y) (Ztimes (neg n) z)).  
+distributive2 nat Z (\lambda n,z. (neg n) * z) Zplus.
+change with (\forall n,y,z.
+(neg n) * (y + z) = (neg n) * y + (neg n) * z).  
 intros.
 rewrite > Ztimes_neg_Zopp. 
 rewrite > distr_Ztimes_Zplus_pos.
@@ -217,21 +216,20 @@ reflexivity.
 qed.
 
 variant distr_Ztimes_Zplus_neg: \forall n,y,z.
-eq Z (Ztimes (neg n) (Zplus y z)) (Zplus (Ztimes (neg n) y) (Ztimes (neg n) z)) \def
+(neg n) * (y + z) = (neg n) * y + (neg n) * z \def
 distributive2_Ztimes_neg_Zplus.
 
 theorem distributive_Ztimes_Zplus: distributive Z Ztimes Zplus.
-change with \forall x,y,z:Z.
-eq Z (Ztimes x (Zplus y z)) (Zplus (Ztimes x y) (Ztimes x z)).
+change with (\forall x,y,z:Z. x * (y + z) = x*y + x*z).
 intros.elim x.
 (* case x = OZ *)
 simplify.reflexivity.
-(* case x = neg n *)
-apply distr_Ztimes_Zplus_neg.
 (* case x = pos n *)
 apply distr_Ztimes_Zplus_pos.
+(* case x = neg n *)
+apply distr_Ztimes_Zplus_neg.
 qed.
 
 variant distr_Ztimes_Zplus: \forall x,y,z.
-eq Z (Ztimes x (Zplus y z)) (Zplus (Ztimes x y) (Ztimes x z)) \def
-distributive_Ztimes_Zplus.
\ No newline at end of file
+x * (y + z) = x*y + x*z \def
+distributive_Ztimes_Zplus.