X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2FZ%2Ftimes.ma;h=688957e57396cecb7fd0143c60f171640024b743;hb=91a095f0686ee569ba035e4e30c7d071588cb8e7;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..688957e57 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,7 +14,9 @@
 
 set "baseuri" "cic:/matita/Z/times".
 
-include "Z/z.ma".
+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.
@@ -31,32 +33,35 @@ 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.
+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.
 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 +75,163 @@ 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.
-simplify.
-rewrite < plus_n_O.reflexivity.
-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.
+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.
-apply Zplus_pos_neg.
-apply Zplus_pos_pos.
+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.
 
-theorem Zplus_Zsucc_pos_pos : 
-\forall n,m. eq Z (Zplus (Zsucc (pos n)) (pos m)) (Zsucc (Zplus (pos n) (pos m))).
-intros.reflexivity.
-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 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.
+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 < (Zplus_pos_neg ? m1).
-elim H.reflexivity.
+rewrite < S_pred ? ?.  
+rewrite > minus_pred_pred ? ? ? ?.
+rewrite < distr_times_minus. 
+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.
 qed.
 
-theorem Zplus_Zsucc_neg_neg : 
-\forall n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m))).
+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.
-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.
+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 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.
+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.                                 
+(* two more positivity conditions from nat_compare_pred_pred *)   
+apply lt_O_times_S_S.  
+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 < (Zplus_neg_neg ? m1).
-reflexivity.
+rewrite < sym_Zplus.
+rewrite > Ztimes_Zplus_pos_neg_pos.
+apply sym_Zplus.
 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.
+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.
-rewrite < H.
-rewrite < (Zplus_neg_pos ? (S m1)).
+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.
 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.
+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.
 
-theorem Zplus_Zpred: \forall x,y:Z. eq Z (Zplus (Zpred x) y) (Zpred (Zplus x y)).
+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.
-cut eq Z (Zpred (Zplus x y)) (Zpred (Zplus (Zsucc (Zpred x)) y)).
-rewrite > Hcut.
-rewrite > Zplus_Zsucc.
-rewrite > Zpred_Zsucc.
-reflexivity.
-rewrite > Zsucc_Zpred.
+rewrite > Ztimes_neg_Zopp. 
+rewrite > distr_Ztimes_Zplus_pos.
+rewrite > Zopp_Zplus.
+rewrite < Ztimes_neg_Zopp. rewrite < Ztimes_neg_Zopp.
 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
+distributive2_Ztimes_neg_Zplus.
 
-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.
+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 = neg n *)
+apply distr_Ztimes_Zplus_neg.
+(* case x = pos n *)
+apply distr_Ztimes_Zplus_pos.
 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.
-simplify.
-rewrite > nat_compare_n_n.
-simplify.apply refl_eq.
-simplify.
-rewrite > nat_compare_n_n.
-simplify.apply refl_eq.
-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