X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2FZ%2Ftimes.ma;h=a36bd078c01877187072ee6fb804fd44beaacdaa;hb=2ecd65dbcc1388bb2dfe6425e6ef1b2e3f45c4ac;hp=7e4b10e0028428b64f7809329eb430f9123ac37e;hpb=7bbce6bc163892cfd99cfcda65db42001b86789f;p=helm.git

diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma
index 7e4b10e00..a36bd078c 100644
--- a/helm/matita/library/Z/times.ma
+++ b/helm/matita/library/Z/times.ma
@@ -15,7 +15,7 @@
 set "baseuri" "cic:/matita/Z/times".
 
 include "nat/lt_arith.ma".
-include "Z/z.ma".
+include "Z/plus.ma".
 
 definition Ztimes :Z \to Z \to Z \def
 \lambda x,y.
@@ -42,6 +42,13 @@ 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)).
+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).
 intros.elim x.rewrite > Ztimes_z_OZ.reflexivity.
@@ -62,166 +69,171 @@ variant sym_Ztimes : \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x)
 
 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.
+intros.elim x.
+  simplify.reflexivity. 
+  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.
+  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.
 qed.
 
 variant assoc_Ztimes : \forall x,y,z:Z. 
 eq Z (Ztimes (Ztimes x y) z) (Ztimes x (Ztimes y z)) \def 
 associative_Ztimes.
 
-
-theorem distributive_Ztimes: 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)).
-intros.elim x.
-simplify.reflexivity.
-(* case x = neg n *)
-elim y.reflexivity.
-elim z.reflexivity.
-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 < times_plus_distr.reflexivity.
-simplify. (* problemi di naming su n *)
-(* sintassi della change ??? *)
-cut \forall n,m:nat.eq nat (plus m (times n (S m))) (pred (times (S n) (S m))).
-rewrite > Hcut.
-rewrite > Hcut.
-rewrite < nat_compare_pred_pred ? ? ? ?.
-rewrite < nat_compare_times_l.
-rewrite < nat_compare_S_S.
-apply nat_compare_elim n1 n2.
-intro.
-(* per ricavare questo change ci ho messo un'ora; 
-LA GESTIONE DELLA RIDUZIONE NON VA *)
-change with (eq Z (neg (pred (times (S n) (S (pred (minus (S n2) (S n1)))))))
-           (neg (pred (minus (pred (times (S n) (S n2)))
-                             (pred (times (S n) (S n1))))))).
-rewrite < S_pred ? ?.  
-rewrite > minus_pred_pred ? ? ? ?.
-rewrite < distr_times_minus. 
-reflexivity. 
-(* we start closing stupid positivity conditions *)
-apply lt_O_times_S_S.                    
-apply lt_O_times_S_S.
-simplify.
-apply le_SO_minus.  exact H.    
-intro.rewrite < H.simplify.reflexivity.
-intro.
-change with (eq Z (pos (pred (times (S n) (S (pred (minus (S n1) (S n2)))))))
-           (pos (pred (minus (pred (times (S n) (S n1)))
-                             (pred (times (S n) (S n2))))))).       
-rewrite < S_pred ? ?.  
-rewrite > minus_pred_pred ? ? ? ?.
+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)))).
+intros.
+rewrite < S_pred.  
+rewrite > minus_pred_pred.
 rewrite < distr_times_minus. 
-reflexivity. 
-(* we start closing stupid positivity conditions *)
+reflexivity.  
+(* we now close all positivity conditions *)
 apply lt_O_times_S_S.                    
 apply lt_O_times_S_S.
 simplify.
 apply le_SO_minus.  exact H.
-(* questi non so neppure da dove vengano *)   
-apply lt_O_times_S_S.  
-apply lt_O_times_S_S.  
-(* adesso chiudo il cut stupido *)
-intros.reflexivity.
-elim z.reflexivity.
-simplify.
-cut \forall n,m:nat.eq nat (plus m (times n (S m))) (pred (times (S n) (S m))).
-rewrite > Hcut.
-rewrite > Hcut.
-rewrite < nat_compare_pred_pred ? ? ? ?.
+qed.
+
+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.
 rewrite < nat_compare_times_l.
 rewrite < nat_compare_S_S.
-apply nat_compare_elim n1 n2.
+apply nat_compare_elim p q.
 intro.
-(* per ricavare questo change ci ho messo un'ora; 
-LA GESTIONE DELLA RIDUZIONE NON VA *)
-change with (eq Z (pos (pred (times (S n) (S (pred (minus (S n2) (S n1)))))))
-           (pos (pred (minus (pred (times (S n) (S n2)))
-                             (pred (times (S n) (S n1))))))).
-rewrite < S_pred ? ?.  
-rewrite > minus_pred_pred ? ? ? ?.
-rewrite < distr_times_minus. 
-reflexivity. 
-(* we start closing stupid positivity conditions *)
-apply lt_O_times_S_S.                    
-apply lt_O_times_S_S.
-simplify.
-apply le_SO_minus.  exact H.    
+(* 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.
 intro.rewrite < H.simplify.reflexivity.
 intro.
-change with (eq Z (neg (pred (times (S n) (S (pred (minus (S n1) (S n2)))))))
-           (neg (pred (minus (pred (times (S n) (S n1)))
-                             (pred (times (S n) (S n2))))))).       
-rewrite < S_pred ? ?.  
-rewrite > minus_pred_pred ? ? ? ?.
-rewrite < distr_times_minus. 
-reflexivity. 
-(* we start closing stupid positivity conditions *)
-apply lt_O_times_S_S.                    
-apply lt_O_times_S_S.
-simplify.
-apply le_SO_minus.  exact H.
-(* questi non so neppure da dove vengano *)   
-apply lt_O_times_S_S.  
+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.                                 
+(* two more positivity conditions from nat_compare_pred_pred *)   
 apply lt_O_times_S_S.  
-(* adesso chiudo il cut stupido *)
-intros.reflexivity.
-change with
-eq Z (neg (pred (times (S n) (plus (S n1) (S n2)))))
+apply lt_O_times_S_S. 
+qed. 
+
+lemma Ztimes_Zplus_pos_pos_neg: \forall n,p,q:nat.
+(pos n)*((pos p)+(neg q)) = (pos n)*(pos p)+ (pos n)*(neg q).
+intros.
+rewrite < sym_Zplus.
+rewrite > Ztimes_Zplus_pos_neg_pos.
+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 (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.
+    apply Ztimes_Zplus_pos_pos_neg.
+  elim z.
+    reflexivity.
+    apply Ztimes_Zplus_pos_neg_pos.
+    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 < times_plus_distr. 
+    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
+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)).  
+intros.
+rewrite > Ztimes_neg_Zopp. 
+rewrite > distr_Ztimes_Zplus_pos.
+rewrite > Zopp_Zplus.
+rewrite < Ztimes_neg_Zopp. rewrite < Ztimes_neg_Zopp.
 reflexivity.
-(* and now the case x = pos n *)
+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
+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)).
+intros.elim x.
+(* case x = OZ *)
+simplify.reflexivity.
+(* 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.