- bugfix: eta abstractions ignores attributed node while counting lambdas

[helm.git] / helm / matita / library / Z / times.ma

diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma
index 7e4b10e0028428b64f7809329eb430f9123ac37e..a36bd078c01877187072ee6fb804fd44beaacdaa 100644 (file)
--- 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".
 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.
 
 definition Ztimes :Z \to Z \to Z \def
 \lambda x,y.


@@ -42,6 +42,13 @@ simplify.reflexivity.
 simplify.reflexivity.
 qed.
 
 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.
 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)).
 
 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.
 
 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. 
 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.
 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.
 rewrite < nat_compare_times_l.
 rewrite < nat_compare_S_S.

-apply nat_compare_elim n1 n2.
+apply nat_compare_elim p q.

 intro.
 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.
 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.  
 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))))).
      (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.
 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.