Committing all the recent development of Andrea after the merge between his

commits and my recent commits (that added notation here and there).

diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma
index 1352988df32cd32d2dcf77699db265a8c4f4c523..7e4b10e0028428b64f7809329eb430f9123ac37e 100644 (file)
--- 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
@@ -41,20 +42,18 @@ simplify.reflexivity.
 simplify.reflexivity.
 qed.
 
-(*CSC: da qui in avanti niente notazione *)
-(*
 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.
 
@@ -68,190 +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.
+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.
+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.
+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.
-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.
-*)
+(* and now the case x = pos n *)

diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma
index d3bc2ee2584529c00802746e4e5e792ea0c4242e..cdc0e44d7c28f29fb01681a6d2b52a139a2955d0 100644 (file)
--- a/helm/matita/library/Z/z.ma
+++ b/helm/matita/library/Z/z.ma
@@ -108,7 +108,7 @@ definition Zplus :Z \to Z \to Z \def
     | (pos m) \Rightarrow
         match y with
          [ OZ \Rightarrow x
-         | (pos n) \Rightarrow (pos (S (m+n)))
+         | (pos n) \Rightarrow (pos (pred ((S m)+(S n))))
          | (neg n) \Rightarrow 
               match nat_compare m n with
                 [ LT \Rightarrow (neg (pred (n-m)))
@@ -122,7 +122,7 @@ definition Zplus :Z \to Z \to Z \def
                 [ LT \Rightarrow (pos (pred (n-m)))
                 | EQ \Rightarrow OZ
                 | GT \Rightarrow (neg (pred (m-n)))]     
-         | (neg n) \Rightarrow (neg (S (m+n)))]].
+         | (neg n) \Rightarrow (neg (pred ((S m)+(S n))))]].
 
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "integer plus" 'plus x y = (cic:/matita/Z/z/Zplus.con x y).
@@ -140,7 +140,7 @@ theorem sym_Zplus : \forall x,y:Z. x+y = y+x.
 intros.elim x.rewrite > Zplus_z_OZ.reflexivity.
 elim y.simplify.reflexivity.
 simplify.
-rewrite < sym_plus.reflexivity.
+rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity.
 simplify.
 rewrite > nat_compare_n_m_m_n.
 simplify.elim nat_compare ? ?.simplify.reflexivity.
@@ -151,7 +151,7 @@ simplify.rewrite > nat_compare_n_m_m_n.
 simplify.elim nat_compare ? ?.simplify.reflexivity.
 simplify. reflexivity.
 simplify. reflexivity.
-simplify.rewrite < sym_plus.reflexivity.
+simplify.rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity.
 qed.
 
 theorem Zpred_Zplus_neg_O : \forall z:Z. Zpred z = (neg O)+z.
@@ -177,9 +177,9 @@ elim n.elim m.
 simplify.reflexivity.
 simplify.reflexivity.
 elim m.
-simplify.
+simplify.rewrite < plus_n_Sm.
 rewrite < plus_n_O.reflexivity.
-simplify.
+simplify.rewrite < plus_n_Sm.
 rewrite < plus_n_Sm.reflexivity.
 qed.
 
@@ -206,7 +206,7 @@ elim n.elim m.
 simplify.reflexivity.
 simplify.reflexivity.
 elim m.
-simplify.rewrite < plus_n_Sm.reflexivity.
+simplify.rewrite > plus_n_Sm.reflexivity.
 simplify.rewrite > plus_n_Sm.reflexivity.
 qed.
 

diff --git a/helm/matita/library/nat/compare.ma b/helm/matita/library/nat/compare.ma
index 60a9d4194c2dc5b3dbf47936260f9763d4bf577d..3a8e4a87ca50a7416e2df5f72920ea151977f41c 100644 (file)
--- a/helm/matita/library/nat/compare.ma
+++ b/helm/matita/library/nat/compare.ma
@@ -78,6 +78,21 @@ nat_compare n m = nat_compare (S n) (S m).
 intros.simplify.reflexivity.
 qed.
 
+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 nat_compare_pred_pred: 
+\forall n,m:nat.lt O n \to lt O m \to 
+eq compare (nat_compare n m) (nat_compare (pred n) (pred m)).
+intros.
+apply lt_O_n_elim n H.
+apply lt_O_n_elim m H1.
+intros.
+simplify.reflexivity.
+qed.
+
 theorem nat_compare_to_Prop: \forall n,m:nat. 
 match (nat_compare n m) with
   [ LT \Rightarrow n < m

diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma
index ca8b6c3faaaec0cd8c89c5bce373ba0efd9a588a..619ba68151a48183109400077fc9e1d034d6919a 100644 (file)
--- a/helm/matita/library/nat/div_and_mod.ma
+++ b/helm/matita/library/nat/div_and_mod.ma
@@ -15,7 +15,7 @@
 set "baseuri" "cic:/matita/nat/div_and_mod".
 
 include "nat/minus.ma".
-include "nat/orders_op.ma".
+include "nat/le_arith.ma".
 include "nat/compare.ma".
 
 let rec mod_aux p m n: nat \def
@@ -174,3 +174,41 @@ apply le_times_r.
 apply lt_to_le.
 apply H6.
 qed.
+
+theorem div_mod_spec_times : \forall n,m:nat.div_mod_spec ((S n)*m) (S n) m O.
+intros.constructor 1.
+simplify.apply le_S_S.apply le_O_n.
+rewrite < plus_n_O.rewrite < sym_times.reflexivity.
+qed.
+
+theorem div_times: \forall n,m:nat. div ((S n)*m) (S n) = m.
+intros.
+apply div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O.
+apply div_mod_spec_div_mod.
+simplify.apply le_S_S.apply le_O_n.
+apply div_mod_spec_times.
+qed.
+
+theorem injective_times_r: \forall n:nat.injective nat nat (\lambda m:nat.(S n)*m).
+change with \forall n,p,q:nat.(S n)*p = (S n)*q \to p=q.
+intros.
+rewrite < div_times n.
+rewrite < div_times n q.
+apply eq_f2.assumption.
+reflexivity.
+qed.
+
+variant inj_times_r : \forall n,p,q:nat.(S n)*p = (S n)*q \to p=q \def
+injective_times_r.
+
+theorem injective_times_l: \forall n:nat.injective nat nat (\lambda m:nat.m*(S n)).
+change with \forall n,p,q:nat.p*(S n) = q*(S n) \to p=q.
+intros.
+apply inj_times_r n p q.
+rewrite < sym_times.
+rewrite < sym_times q.
+assumption.
+qed.
+
+variant inj_times_l : \forall n,p,q:nat. p*(S n) = q*(S n) \to p=q \def
+injective_times_l.

diff --git a/helm/matita/library/nat/exp.ma b/helm/matita/library/nat/exp.ma
new file mode 100644 (file)
index 0000000..c0d3637
--- /dev/null
+++ b/helm/matita/library/nat/exp.ma
@@ -0,0 +1,46 @@
+(**************************************************************************)
+(*       ___                                                               *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/nat/exp".
+
+include "nat/times.ma". 
+
+let rec exp n m on m\def 
+ match m with 
+ [ O \Rightarrow (S O)
+ | (S p) \Rightarrow (times n (exp n p)) ].
+
+theorem exp_plus_times : \forall n,p,q:nat. 
+eq nat (exp n (plus p q)) (times (exp n p) (exp n q)).
+intros.elim p.
+simplify.rewrite < plus_n_O.reflexivity.
+simplify.rewrite > H.symmetry.
+apply assoc_times.
+qed.
+
+theorem exp_n_O : \forall n:nat. eq nat (S O) (exp n O).
+intro.simplify.reflexivity.
+qed.
+
+theorem exp_n_SO : \forall n:nat. eq nat n (exp n (S O)).
+intro.simplify.rewrite < times_n_SO.reflexivity.
+qed.
+
+theorem bad : \forall n,p,q:nat. 
+eq nat (exp (exp n p) q) (exp n (times p q)).
+intros.
+elim q.simplify.rewrite < times_n_O.simplify.reflexivity.
+simplify.rewrite > H.rewrite < exp_plus_times.
+rewrite < times_n_Sm.reflexivity.
+qed.
\ No newline at end of file

diff --git a/helm/matita/library/nat/le_arith.ma b/helm/matita/library/nat/le_arith.ma
new file mode 100644 (file)
index 0000000..a36f96b
--- /dev/null
+++ b/helm/matita/library/nat/le_arith.ma
@@ -0,0 +1,99 @@
+(**************************************************************************)
+(*       ___                                                               *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/nat/le_arith".
+
+include "higher_order_defs/functions.ma".
+include "nat/times.ma".
+include "nat/orders.ma".
+include "nat/compare.ma".
+
+(* plus *)
+theorem monotonic_le_plus_r: 
+\forall n:nat.monotonic nat le (\lambda m.plus n m).
+simplify.intros.elim n.
+simplify.assumption.
+simplify.apply le_S_S.assumption.
+qed.
+
+theorem le_plus_r: \forall p,n,m:nat. le n m \to le (plus p n) (plus p m)
+\def monotonic_le_plus_r.
+
+theorem monotonic_le_plus_l: 
+\forall m:nat.monotonic nat le (\lambda n.plus n m).
+simplify.intros.
+rewrite < sym_plus.rewrite < sym_plus m.
+apply le_plus_r.assumption.
+qed.
+
+theorem le_plus_l: \forall p,n,m:nat. le n m \to le (plus n p) (plus m p)
+\def monotonic_le_plus_l.
+
+theorem le_plus: \forall n1,n2,m1,m2:nat. le n1 n2  \to le m1 m2 
+\to le (plus n1 m1) (plus n2 m2).
+intros.
+apply trans_le ? (plus n2 m1).
+apply le_plus_l.assumption.
+apply le_plus_r.assumption.
+qed.
+
+theorem le_plus_n :\forall n,m:nat. le m (plus n m).
+intros.change with le (plus O m) (plus n m).
+apply le_plus_l.apply le_O_n.
+qed.
+
+theorem eq_plus_to_le: \forall n,m,p:nat.eq nat n (plus m p) 
+\to le m n.
+intros.rewrite > H.
+rewrite < sym_plus.
+apply le_plus_n.
+qed.
+
+(* times *)
+theorem monotonic_le_times_r: 
+\forall n:nat.monotonic nat le (\lambda m.times n m).
+simplify.intros.elim n.
+simplify.apply le_O_n.
+simplify.apply le_plus.
+assumption.
+assumption.
+qed.
+
+theorem le_times_r: \forall p,n,m:nat. le n m \to le (times p n) (times p m)
+\def monotonic_le_times_r.
+
+theorem monotonic_le_times_l: 
+\forall m:nat.monotonic nat le (\lambda n.times n m).
+simplify.intros.
+rewrite < sym_times.rewrite < sym_times m.
+apply le_times_r.assumption.
+qed.
+
+theorem le_times_l: \forall p,n,m:nat. le n m \to le (times n p) (times m p)
+\def monotonic_le_times_l.
+
+theorem le_times: \forall n1,n2,m1,m2:nat. le n1 n2  \to le m1 m2 
+\to le (times n1 m1) (times n2 m2).
+intros.
+apply trans_le ? (times n2 m1).
+apply le_times_l.assumption.
+apply le_times_r.assumption.
+qed.
+
+theorem le_times_n: \forall n,m:nat.le (S O) n \to le m (times n m).
+intros.elim H.simplify.
+elim (plus_n_O ?).apply le_n.
+simplify.rewrite < sym_plus.apply le_plus_n.
+qed.
+

diff --git a/helm/matita/library/nat/lt_arith.ma b/helm/matita/library/nat/lt_arith.ma
new file mode 100644 (file)
index 0000000..5bef223
--- /dev/null
+++ b/helm/matita/library/nat/lt_arith.ma
@@ -0,0 +1,162 @@
+(**************************************************************************)
+(*       ___                                                               *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/nat/lt_arith".
+
+include "nat/div_and_mod.ma".
+
+(* plus *)
+theorem monotonic_lt_plus_r: 
+\forall n:nat.monotonic nat lt (\lambda m.plus n m).
+simplify.intros.
+elim n.simplify.assumption.
+simplify.
+apply le_S_S.assumption.
+qed.
+
+variant lt_plus_r: \forall n,p,q:nat. lt p q \to lt (plus n p) (plus n q) \def
+monotonic_lt_plus_r.
+
+theorem monotonic_lt_plus_l: 
+\forall n:nat.monotonic nat lt (\lambda m.plus m n).
+change with \forall n,p,q:nat. lt p q \to lt (plus p n) (plus q n).
+intros.
+rewrite < sym_plus. rewrite < sym_plus n.
+apply lt_plus_r.assumption.
+qed.
+
+variant lt_plus_l: \forall n,p,q:nat. lt p q \to lt (plus p n) (plus q n) \def
+monotonic_lt_plus_l.
+
+theorem lt_plus: \forall n,m,p,q:nat. lt n m \to lt p q \to lt (plus n p) (plus m q).
+intros.
+apply trans_lt ? (plus n q).
+apply lt_plus_r.assumption.
+apply lt_plus_l.assumption.
+qed.
+
+theorem lt_plus_to_lt_l :\forall n,p,q:nat. lt (plus p n) (plus q n) \to lt p q.
+intro.elim n.
+rewrite > plus_n_O.
+rewrite > plus_n_O q.assumption.
+apply H.
+simplify.apply le_S_S_to_le.
+rewrite > plus_n_Sm.
+rewrite > plus_n_Sm q.
+exact H1.
+qed.
+
+theorem lt_plus_to_lt_r :\forall n,p,q:nat. lt (plus n p) (plus n q) \to lt p q.
+intros.apply lt_plus_to_lt_l n. 
+rewrite > sym_plus.
+rewrite > sym_plus q.assumption.
+qed.
+
+(* times and zero *)
+theorem lt_O_times_S_S: \forall n,m:nat.lt O (times (S n) (S m)).
+intros.simplify.apply le_S_S.apply le_O_n.
+qed.
+
+(* times *)
+theorem monotonic_lt_times_r: 
+\forall n:nat.monotonic nat lt (\lambda m.times (S n) m).
+change with \forall n,p,q:nat. lt p q \to lt (times (S n) p) (times (S n) q).
+intros.elim n.
+simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption.
+change with lt (plus p (times (S n1) p)) (plus q (times (S n1) q)).
+apply lt_plus.assumption.assumption.
+qed.
+
+theorem lt_times_r: \forall n,p,q:nat. lt p q \to lt (times (S n) p) (times (S n) q)
+\def monotonic_lt_times_r.
+
+theorem monotonic_lt_times_l: 
+\forall m:nat.monotonic nat lt (\lambda n.times n (S m)).
+change with 
+\forall n,p,q:nat. lt p q \to lt (times p (S n)) (times q (S n)).
+intros.
+rewrite < sym_times.rewrite < sym_times (S n).
+apply lt_times_r.assumption.
+qed.
+
+variant lt_times_l: \forall n,p,q:nat. lt p q \to lt (times p (S n)) (times q (S n))
+\def monotonic_lt_times_l.
+
+theorem lt_times:\forall n,m,p,q:nat. lt n m \to lt p q \to lt (times n p) (times m q).
+intro.
+elim n.
+apply lt_O_n_elim m H.
+intro.
+cut lt O q.
+apply lt_O_n_elim q Hcut.
+intro.change with lt O (times (S m1) (S m2)).
+apply lt_O_times_S_S.
+apply ltn_to_ltO p q H1.
+apply trans_lt ? (times (S n1) q).
+apply lt_times_r.assumption.
+cut lt O q.
+apply lt_O_n_elim q Hcut.
+intro.
+apply lt_times_l.
+assumption.
+apply ltn_to_ltO p q H2.
+qed.
+
+theorem lt_times_to_lt_l: 
+\forall n,p,q:nat. lt (times p (S n)) (times q (S n)) \to lt p q.
+intros.
+(* convertibility problem here *)
+cut Or (lt p q) (Not (lt p q)).
+elim Hcut.
+assumption.
+absurd lt (times p (S n)) (times q (S n)).
+assumption.
+apply le_to_not_lt.
+apply le_times_l.
+apply not_lt_to_le.
+assumption.
+exact decidable_lt p q.
+qed.
+
+theorem lt_times_to_lt_r: 
+\forall n,p,q:nat. lt (times (S n) p) (times(S n) q) \to lt p q.
+intros.
+apply lt_times_to_lt_l n.
+rewrite < sym_times.
+rewrite < sym_times (S n).
+assumption.
+qed.
+
+theorem nat_compare_times_l : \forall n,p,q:nat. 
+eq compare (nat_compare p q) (nat_compare (times (S n) p) (times (S n) q)).
+intros.apply nat_compare_elim.intro.
+apply nat_compare_elim.
+intro.reflexivity.
+intro.absurd eq nat p q.
+apply inj_times_r n.assumption.
+apply lt_to_not_eq. assumption.
+intro.absurd lt q p.
+apply lt_times_to_lt_r n.assumption.
+apply le_to_not_lt.apply lt_to_le.assumption.
+intro.rewrite < H.rewrite > nat_compare_n_n.reflexivity.
+intro.apply nat_compare_elim.intro.
+absurd (lt p q).
+apply lt_times_to_lt_r n.assumption.
+apply le_to_not_lt.apply lt_to_le.assumption.
+intro.absurd eq nat q p.
+symmetry.
+apply inj_times_r n.assumption.
+apply lt_to_not_eq.assumption.
+intro.reflexivity.
+qed.

diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma
index e725185e004bfaedb6ed3dbbea63720bd91ab4ba..1b790031401c2aeb8dc04a3ad769fd9f43fa86c6 100644 (file)
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -15,7 +15,7 @@
 
 set "baseuri" "cic:/matita/nat/minus".
 
-include "nat/orders_op.ma".
+include "nat/le_arith.ma".
 include "nat/compare.ma".
 
 let rec minus n m \def 
@@ -98,6 +98,20 @@ symmetry.
 apply plus_minus_m_m.assumption.
 qed.
 
+theorem minus_S_S : \forall n,m:nat.
+eq nat (minus (S n) (S m)) (minus n m).
+intros.
+reflexivity.
+qed.
+
+theorem minus_pred_pred : \forall n,m:nat. lt O n \to lt O m \to 
+eq nat (minus (pred n) (pred m)) (minus n m).
+intros.
+apply lt_O_n_elim n H.intro.
+apply lt_O_n_elim m H1.intro.
+simplify.reflexivity.
+qed.
+
 theorem eq_minus_n_m_O: \forall n,m:nat.
 n \leq m \to n-m = O.
 intros 2.

diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma
index d269e5fe1b83485fc20203ef08c5e3e6d7c988aa..4ec4dfc5b11089876cafc3d2802a80f098c3917a 100644 (file)
--- a/helm/matita/library/nat/orders.ma
+++ b/helm/matita/library/nat/orders.ma
@@ -52,6 +52,15 @@ qed.
 theorem trans_le: \forall n,m,p:nat. n \leq m \to m \leq p \to n \leq p
 \def transitive_le.
 
+theorem transitive_lt: transitive nat lt.
+simplify.intros.elim H1.
+apply le_S. assumption.
+apply le_S.assumption.
+qed.
+
+theorem trans_lt: \forall n,m,p:nat. lt n m \to lt m p \to lt n p
+\def transitive_lt.
+
 theorem le_S_S: \forall n,m:nat. n \leq m \to S n \leq S m.
 intros.elim H.
 apply le_n.
@@ -95,10 +104,11 @@ apply H.assumption.
 apply le_S_S_to_le.assumption.
 qed.
 
-(* ??? this needs not le *)
-theorem S_pred: \forall n:nat.O<n \to n=S (pred n).
-intro.elim n.apply False_ind.exact not_le_Sn_O O H.
-apply eq_f.apply pred_Sn.
+(* not eq *)
+theorem lt_to_not_eq : \forall n,m:nat. n<m \to \lnot (n=m).
+simplify.intros.cut (le (S n) m) \to False.
+apply Hcut.assumption.rewrite < H1.
+apply not_le_Sn_n.
 qed.
 
 (* le vs. lt *)
@@ -108,6 +118,11 @@ apply le_S. apply le_n.
 apply le_S. assumption.
 qed.
 
+theorem lt_S_to_le : \forall n,m:nat. n < S m \to n \leq m.
+simplify.intros.
+apply le_S_S_to_le.assumption.
+qed.
+
 theorem not_le_to_lt: \forall n,m:nat. \lnot (n \leq m) \to m<n.
 intros 2.
 apply nat_elim2 (\lambda n,m.\lnot (n \leq m) \to m<n).
@@ -123,6 +138,19 @@ apply not_le_Sn_n n H1.
 apply H2.apply lt_to_le. apply H3.
 qed.
 
+theorem not_lt_to_le: \forall n,m:nat. Not (lt n m) \to le m n.
+simplify.intros.
+apply lt_S_to_le.
+apply not_le_to_lt.exact H.
+qed.
+
+theorem le_to_not_lt: \forall n,m:nat. le n m \to Not (lt m n).
+intros.
+change with Not (le (S m) n).
+apply lt_to_not_le.simplify.
+apply le_S_S.assumption.
+qed.
+
 (* le elimination *)
 theorem le_n_O_to_eq : \forall n:nat. n \leq O \to O=n.
 intro.elim n.reflexivity.
@@ -146,6 +174,29 @@ apply H2.reflexivity.
 apply H3. apply le_S_S. assumption.
 qed.
 
+(* lt and le trans *)
+theorem lt_to_le_to_lt: \forall n,m,p:nat. lt n m \to le m p \to lt n p.
+intros.elim H1.
+assumption.simplify.apply le_S.assumption.
+qed.
+
+theorem le_to_lt_to_lt: \forall n,m,p:nat. le n m \to lt m p \to lt n p.
+intros 4.elim H.
+assumption.apply H2.simplify.
+apply lt_to_le.assumption.
+qed.
+
+theorem ltn_to_ltO: \forall n,m:nat. lt n m \to lt O m.
+intros.apply le_to_lt_to_lt O n.
+apply le_O_n.assumption.
+qed.
+
+theorem lt_O_n_elim: \forall n:nat. lt O n \to 
+\forall P:nat\to Prop. (\forall m:nat.P (S m)) \to P n.
+intro.elim n.apply False_ind.exact not_le_Sn_O O H.
+apply H2.
+qed.
+
 (* other abstract properties *)
 theorem antisymmetric_le : antisymmetric nat le.
 simplify.intros 2.
@@ -169,3 +220,7 @@ intros 2.simplify.intro.elim H.
 left.apply le_S_S.assumption.
 right.intro.apply H1.apply le_S_S_to_le.assumption.
 qed.
+
+theorem decidable_lt: \forall n,m:nat. decidable (n < m).
+intros.exact decidable_le (S n) m.
+qed.

diff --git a/helm/matita/library/nat/times.ma b/helm/matita/library/nat/times.ma
index d2ce51bfa83dd9605bf5160e227edf3c532aeff0..2707c2ba1cdd8ff08a0404fa40de9f714390542c 100644 (file)
--- a/helm/matita/library/nat/times.ma
+++ b/helm/matita/library/nat/times.ma
@@ -1,5 +1,5 @@
 (**************************************************************************)
-(*       ___                                                               *)
+(*       __                                                               *)
 (*      ||M||                                                             *)
 (*      ||A||       A project by Andrea Asperti                           *)
 (*      ||T||                                                             *)
@@ -14,14 +14,12 @@
 
 set "baseuri" "cic:/matita/nat/times".
 
-include "logic/equality.ma".
-include "nat/nat.ma".
 include "nat/plus.ma".
 
 let rec times n m \def 
  match n with 
  [ O \Rightarrow O
- | (S p) \Rightarrow (m+(times p m)) ].
+ | (S p) \Rightarrow m+(times p m) ].
 
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural times" 'times x y = (cic:/matita/nat/times/times.con x y).
@@ -33,7 +31,7 @@ simplify.assumption.
 qed.
 
 theorem times_n_Sm : 
-\forall n,m:nat.n+n*m = n*(S m).
+\forall n,m:nat. n+(n*m) = n*(S m).
 intros.elim n.
 simplify.reflexivity.
 simplify.apply eq_f.rewrite < H.
@@ -45,16 +43,24 @@ reflexivity.
 apply assoc_plus.
 qed.
 
-(* same problem with symmetric: see plus 
-theorem symmetric_times : symmetric nat times. *)
+theorem times_n_SO : \forall n:nat. eq nat n (times n (S O)).
+intros.
+rewrite < times_n_Sm.
+rewrite < times_n_O.
+rewrite < plus_n_O.
+reflexivity.
+qed.
 
-theorem sym_times : 
-\forall n,m:nat.n*m = m*n.
-intros.elim n.
+theorem symmetric_times : symmetric nat times. 
+simplify.
+intros.elim x.
 simplify.apply times_n_O.
 simplify.rewrite > H.apply times_n_Sm.
 qed.
 
+variant sym_times : \forall n,m:nat. n*m = m*n \def
+symmetric_times.
+
 theorem distributive_times_plus : distributive nat times plus.
 simplify.
 intros.elim x.
@@ -64,6 +70,18 @@ apply eq_f.rewrite < assoc_plus. rewrite < sym_plus ? z.
 rewrite > assoc_plus.reflexivity.
 qed.
 
-variant times_plus_distr: \forall n,m,p:nat. n*(m+p)=n*m+n*p
+variant times_plus_distr: \forall n,m,p:nat. n*(m+p) = n*m + n*p
 \def distributive_times_plus.
 
+theorem associative_times: associative nat times.
+simplify.intros.
+elim x.simplify.apply refl_eq.
+simplify.rewrite < sym_times.
+rewrite > times_plus_distr.
+rewrite < sym_times.
+rewrite < sym_times (times n y) z.
+rewrite < H.apply refl_eq.
+qed.
+
+variant assoc_times: \forall n,m,p:nat. (n*m)*p = n*(m*p) \def
+associative_times.