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

diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma
index 6e7a59d16..7e4b10e00 100644
--- a/helm/matita/library/Z/times.ma
+++ b/helm/matita/library/Z/times.ma
@@ -1,5 +1,5 @@
 (**************************************************************************)
-(*       ___	                                                            *)
+(*       __                                                               *)
 (*      ||M||                                                             *)
 (*      ||A||       A project by Andrea Asperti                           *)
 (*      ||T||                                                             *)
@@ -14,6 +14,7 @@
 
 set "baseuri" "cic:/matita/Z/times".
 
+include "nat/lt_arith.ma".
 include "Z/z.ma".
 
 definition Ztimes :Z \to Z \to Z \def
@@ -31,32 +32,28 @@ definition Ztimes :Z \to Z \to Z \def
          | (pos n) \Rightarrow (neg (pred (times (S m) (S n))))
          | (neg n) \Rightarrow (pos (pred (times (S m) (S n))))]].
          
-theorem Ztimes_z_OZ:  \forall z:Z. eq Z (Ztimes z OZ) OZ.
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "integer times" 'times x y = (cic:/matita/Z/times/Ztimes.con x y).
+
+theorem Ztimes_z_OZ:  \forall z:Z. z*OZ = OZ.
 intro.elim z.
 simplify.reflexivity.
 simplify.reflexivity.
 simplify.reflexivity.
 qed.
 
-(* da spostare in nat/order *)
-theorem S_pred: \forall n:nat.lt O n \to eq nat n (S (pred n)).
-intro.elim n.apply False_ind.exact not_le_Sn_O O H.
-apply eq_f.apply pred_Sn.
-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.
 elim y.simplify.reflexivity. 
-change with eq Z (pos (pred (times (S e1) (S e)))) (pos (pred (times (S e) (S e1)))).
+change with eq Z (pos (pred (times (S n) (S n1)))) (pos (pred (times (S n1) (S n)))).
 rewrite < sym_times.reflexivity.
-change with eq Z (neg (pred (times (S e1) (S e2)))) (neg (pred (times (S e2) (S e1)))).
+change with eq Z (neg (pred (times (S n) (S n1)))) (neg (pred (times (S n1) (S n)))).
 rewrite < sym_times.reflexivity.
 elim y.simplify.reflexivity.
-change with eq Z (neg (pred (times (S e2) (S e1)))) (neg (pred (times (S e1) (S e2)))).
+change with eq Z (neg (pred (times (S n) (S n1)))) (neg (pred (times (S n1) (S n)))).
 rewrite < sym_times.reflexivity.
-change with eq Z (pos (pred (times (S e2) (S e)))) (pos (pred (times (S e) (S e2)))).
+change with eq Z (pos (pred (times (S n) (S n1)))) (pos (pred (times (S n1) (S n)))).
 rewrite < sym_times.reflexivity.
 qed.
 
@@ -70,207 +67,161 @@ elim x.simplify.reflexivity.
 elim y.simplify.reflexivity.
 elim z.simplify.reflexivity.
 change with 
-eq Z (neg (pred (times (S (pred (times (S e1) (S e)))) (S e2))))
-     (neg (pred (times (S e1) (S (pred (times (S e) (S e2))))))).
-rewrite < S_pred_S.
-
-theorem Zpred_Zplus_neg_O : \forall z:Z. eq Z (Zpred z) (Zplus (neg O) z).
-intros.elim z.
-simplify.reflexivity.
-simplify.reflexivity.
-elim e2.simplify.reflexivity.
-simplify.reflexivity.
-qed.
-
-theorem Zsucc_Zplus_pos_O : \forall z:Z. eq Z (Zsucc z) (Zplus (pos O) z).
-intros.elim z.
-simplify.reflexivity.
-elim e1.simplify.reflexivity.
-simplify.reflexivity.
-simplify.reflexivity.
-qed.
-
-theorem Zplus_pos_pos:
-\forall n,m. eq Z (Zplus (pos n) (pos m)) (Zplus (Zsucc (pos n)) (Zpred (pos m))).
-intros.
-elim n.elim m.
-simplify.reflexivity.
-simplify.reflexivity.
-elim m.
+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.
+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.
-rewrite < plus_n_O.reflexivity.
+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 ? ? ? ?.
+rewrite < distr_times_minus. 
+reflexivity. 
+(* we start closing stupid positivity conditions *)
+apply lt_O_times_S_S.                    
+apply lt_O_times_S_S.
 simplify.
-rewrite < plus_n_Sm.reflexivity.
-qed.
-
-theorem Zplus_pos_neg:
-\forall n,m. eq Z (Zplus (pos n) (neg m)) (Zplus (Zsucc (pos n)) (Zpred (neg m))).
-intros.reflexivity.
-qed.
-
-theorem Zplus_neg_pos :
-\forall n,m. eq Z (Zplus (neg n) (pos m)) (Zplus (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. eq Z (Zplus (neg n) (neg m)) (Zplus (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. eq Z (Zplus x y) (Zplus (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. eq Z (Zplus (Zsucc (pos n)) (pos m)) (Zsucc (Zplus (pos n) (pos m))).
+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.
-qed.
-
-theorem Zplus_Zsucc_pos_neg: 
-\forall n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m))).
-intros.
-apply nat_elim2
-(\lambda n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m)))).intro.
-intros.elim n1.
-simplify. reflexivity.
-elim e1.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. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m))).
-intros.
-apply nat_elim2
-(\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m)))).intro.
-intros.elim n1.
-simplify. reflexivity.
-elim e1.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. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m))).
-intros.
-apply nat_elim2
-(\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m)))).
-intros.elim n1.
-simplify. reflexivity.
-elim e1.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. eq Z (Zplus (Zsucc x) y) (Zsucc (Zplus 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. eq Z (Zplus (Zpred x) y) (Zpred (Zplus x y)).
-intros.
-cut eq Z (Zpred (Zplus x y)) (Zpred (Zplus (Zsucc (Zpred x)) y)).
+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 > Zplus_Zsucc.
-rewrite > Zpred_Zsucc.
-reflexivity.
-rewrite > Zsucc_Zpred.
-reflexivity.
-qed.
-
-
-theorem associative_Zplus: associative Z Zplus.
-change with \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z)). 
-
-intros.elim x.simplify.reflexivity.
-elim e1.rewrite < (Zpred_Zplus_neg_O (Zplus y z)).
-rewrite < (Zpred_Zplus_neg_O y).
-rewrite < Zplus_Zpred.
-reflexivity.
-rewrite > Zplus_Zpred (neg e).
-rewrite > Zplus_Zpred (neg e).
-rewrite > Zplus_Zpred (Zplus (neg e) y).
-apply eq_f.assumption.
-elim e2.rewrite < Zsucc_Zplus_pos_O.
-rewrite < Zsucc_Zplus_pos_O.
-rewrite > Zplus_Zsucc.
-reflexivity.
-rewrite > Zplus_Zsucc (pos e1).
-rewrite > Zplus_Zsucc (pos e1).
-rewrite > Zplus_Zsucc (Zplus (pos e1) y).
-apply eq_f.assumption.
-qed.
-
-variant assoc_Zplus : \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z))
-\def associative_Zplus.
-
-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) ].
-
-theorem Zplus_Zopp: \forall x:Z. (eq Z (Zplus x (Zopp x)) OZ).
-intro.elim x.
-apply refl_eq.
+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 (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.
-rewrite > nat_compare_n_n.
-simplify.apply refl_eq.
+apply le_SO_minus.  exact H.    
+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.
-rewrite > nat_compare_n_n.
-simplify.apply refl_eq.
-qed.
-*)
+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.
+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. 
+reflexivity.
+(* and now the case x = pos n *)