More notation here and there.

diff --git a/helm/matita/core_notation.moo b/helm/matita/core_notation.moo
index c528fc111d2041cb83761efa02697a33300b337f..9af57e4fe90b25c71a152c6b0db611a060d98a35 100644 (file)
--- a/helm/matita/core_notation.moo
+++ b/helm/matita/core_notation.moo
@@ -74,6 +74,14 @@ notation "- a"
   right associative with precedence 60
 for @{ 'uminus $a }.
 
+notation "a !"
+  left associative with precedence 65
+for @{ 'fact $a }.
+
+notation "(a \sup b)"
+  right associative with precedence 65
+for @{ 'exp $a $b}.
+
 notation "\sqrt a" 
   non associative with precedence 60
 for @{ 'sqrt $a }.

diff --git a/helm/matita/library/Q/q.ma b/helm/matita/library/Q/q.ma
index 1ff2adcd8dfa0bf99462486ce3641519849e0df7..f04603f15f0b129423e8bd5a0fe289f2495b7cbc 100644 (file)
--- a/helm/matita/library/Q/q.ma
+++ b/helm/matita/library/Q/q.ma
@@ -154,23 +154,23 @@ qed.
 theorem decidable_eq_fraction: \forall f,g:fraction.
 decidable (f = g).
 intros.simplify.
-apply fraction_elim2 (\lambda f,g. Or (f=g) (f=g \to False)).
+apply fraction_elim2 (\lambda f,g. f=g \lor (f=g \to False)).
   intros.elim g1.
-    elim ((decidable_eq_nat n n1) : Or (n=n1) (n=n1 \to False)).
+    elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)).
       left.apply eq_f. assumption.
       right.intro.apply H.apply injective_pp.assumption.
     right.apply not_eq_pp_nn.
     right.apply not_eq_pp_cons.
   intros. elim g1.
       right.intro.apply not_eq_pp_nn n1 n.apply sym_eq. assumption.
-      elim ((decidable_eq_nat n n1) : Or (n=n1) (n=n1 \to False)).
+      elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)).
         left. apply eq_f. assumption.
         right.intro.apply H.apply injective_nn.assumption.
       right.apply not_eq_nn_cons.
   intros.right.intro.apply not_eq_pp_cons m x f1.apply sym_eq.assumption.
   intros.right.intro.apply not_eq_nn_cons m x f1.apply sym_eq.assumption.
   intros.elim H.
-    elim ((decidable_eq_Z x y) : Or (x=y) (x=y \to False)).
+    elim ((decidable_eq_Z x y) : x=y \lor (x=y \to False)).
       left.apply eq_f2.assumption.
       assumption.
     right.intro.apply H2.apply eq_cons_to_eq1 f1 g1.assumption.
@@ -225,65 +225,65 @@ let rec ftimes f g \def
   match f with
   [ (pp n) \Rightarrow 
     match g with
-    [(pp m) \Rightarrow Z_to_ratio (Zplus (pos n) (pos m))
-    | (nn m) \Rightarrow Z_to_ratio (Zplus (pos n) (neg m))
-    | (cons y g1) \Rightarrow frac (cons (Zplus (pos n) y) g1)]
+    [(pp m) \Rightarrow Z_to_ratio (pos n + pos m)
+    | (nn m) \Rightarrow Z_to_ratio (pos n + neg m)
+    | (cons y g1) \Rightarrow frac (cons (pos n + y) g1)]
   | (nn n) \Rightarrow 
     match g with
-    [(pp m) \Rightarrow Z_to_ratio (Zplus (neg n) (pos m))
-    | (nn m) \Rightarrow Z_to_ratio (Zplus (neg n) (neg m))
-    | (cons y g1) \Rightarrow frac (cons (Zplus (neg n) y) g1)]
+    [(pp m) \Rightarrow Z_to_ratio (neg n + pos m)
+    | (nn m) \Rightarrow Z_to_ratio (neg n + neg m)
+    | (cons y g1) \Rightarrow frac (cons (neg n + y) g1)]
   | (cons x f1) \Rightarrow
     match g with
-    [ (pp m) \Rightarrow frac (cons (Zplus x (pos m)) f1)
-    | (nn m) \Rightarrow frac (cons (Zplus x (neg m)) f1)
+    [ (pp m) \Rightarrow frac (cons (x + pos m) f1)
+    | (nn m) \Rightarrow frac (cons (x + neg m) f1)
     | (cons y g1) \Rightarrow 
       match ftimes f1 g1 with
-        [ one \Rightarrow Z_to_ratio (Zplus x y)
-        | (frac h) \Rightarrow frac (cons (Zplus x y) h)]]].
+        [ one \Rightarrow Z_to_ratio (x + y)
+        | (frac h) \Rightarrow frac (cons (x + y) h)]]].
         
 theorem symmetric2_ftimes: symmetric2 fraction ratio ftimes.
 simplify. intros.apply fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f).
   intros.elim g.
-    change with Z_to_ratio (Zplus (pos n) (pos n1)) = Z_to_ratio (Zplus (pos n1) (pos n)).
+    change with Z_to_ratio (pos n + pos n1) = Z_to_ratio (pos n1 + pos n).
      apply eq_f.apply sym_Zplus.
-    change with Z_to_ratio (Zplus (pos n) (neg n1)) = Z_to_ratio (Zplus (neg n1) (pos n)).
+    change with Z_to_ratio (pos n + neg n1) = Z_to_ratio (neg n1 + pos n).
      apply eq_f.apply sym_Zplus.
-    change with frac (cons (Zplus (pos n) z) f) = frac (cons (Zplus z (pos n)) f).
+    change with frac (cons (pos n + z) f) = frac (cons (z + pos n) f).
      rewrite < sym_Zplus.reflexivity.
   intros.elim g.
-    change with Z_to_ratio (Zplus (neg n) (pos n1)) = Z_to_ratio (Zplus (pos n1) (neg n)).
+    change with Z_to_ratio (neg n + pos n1) = Z_to_ratio (pos n1 + neg n).
      apply eq_f.apply sym_Zplus.
-    change with Z_to_ratio (Zplus (neg n) (neg n1)) = Z_to_ratio (Zplus (neg n1) (neg n)).
+    change with Z_to_ratio (neg n + neg n1) = Z_to_ratio (neg n1 + neg n).
      apply eq_f.apply sym_Zplus.
-    change with frac (cons (Zplus (neg n) z) f) = frac (cons (Zplus z (neg n)) f).
+    change with frac (cons (neg n + z) f) = frac (cons (z + neg n) f).
      rewrite < sym_Zplus.reflexivity.
-  intros.change with frac (cons (Zplus x1 (pos m)) f) = frac (cons (Zplus (pos m) x1) f).
+  intros.change with frac (cons (x1 + pos m) f) = frac (cons (pos m + x1) f).
    rewrite < sym_Zplus.reflexivity.
-  intros.change with frac (cons (Zplus x1 (neg m)) f) = frac (cons (Zplus (neg m) x1) f).
+  intros.change with frac (cons (x1 + neg m) f) = frac (cons (neg m + x1) f).
    rewrite < sym_Zplus.reflexivity.
   intros.
    change with 
    match ftimes f g with
-   [ one \Rightarrow Z_to_ratio (Zplus x1 y1)
-   | (frac h) \Rightarrow frac (cons (Zplus x1 y1) h)] =
+   [ one \Rightarrow Z_to_ratio (x1 + y1)
+   | (frac h) \Rightarrow frac (cons (x1 + y1) h)] =
    match ftimes g f with
-   [ one \Rightarrow Z_to_ratio (Zplus y1 x1)
-   | (frac h) \Rightarrow frac (cons (Zplus y1 x1) h)].
+   [ one \Rightarrow Z_to_ratio (y1 + x1)
+   | (frac h) \Rightarrow frac (cons (y1 + x1) h)].
     rewrite < H.rewrite < sym_Zplus.reflexivity.
 qed.
 
 theorem ftimes_finv : \forall f:fraction. ftimes f (finv f) = one.
 intro.elim f.
-  change with Z_to_ratio (Zplus (pos n) (Zopp (pos n))) = one.
+  change with Z_to_ratio (pos n + - (pos n)) = one.
    rewrite > Zplus_Zopp.reflexivity.
-  change with Z_to_ratio (Zplus (neg n) (Zopp (neg n))) = one.
+  change with Z_to_ratio (neg n + - (neg n)) = one.
    rewrite > Zplus_Zopp.reflexivity.
 (* again: we would need something to help finding the right change *)
   change with 
   match ftimes f1 (finv f1) with
-  [ one \Rightarrow Z_to_ratio (Zplus z (Zopp z))
-  | (frac h) \Rightarrow frac (cons (Zplus z (Zopp z)) h)] = one.
+  [ one \Rightarrow Z_to_ratio (z + - z)
+  | (frac h) \Rightarrow frac (cons (z + - z) h)] = one.
   rewrite > H.rewrite > Zplus_Zopp.reflexivity.
 qed.
 

diff --git a/helm/matita/library/Z/plus.ma b/helm/matita/library/Z/plus.ma
index b89f291fbb918684cb595dbd54b5d423259e7e23..0456ca0b31533f5aed0ccc9fd7561d67b2b3b2bd 100644 (file)
--- a/helm/matita/library/Z/plus.ma
+++ b/helm/matita/library/Z/plus.ma
@@ -169,10 +169,10 @@ elim H.reflexivity.
 qed.
 
 theorem Zplus_Zsucc_neg_neg : 
-\forall n,m. (Zsucc (neg n))+(neg m) = Zsucc ((neg n)+(neg m)).
+\forall n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m).
 intros.
 apply nat_elim2
-(\lambda n,m. ((Zsucc (neg n))+(neg m)) = Zsucc ((neg n)+(neg m))).intro.
+(\lambda n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m)).intro.
 intros.elim n1.
 simplify. reflexivity.
 elim n2.simplify. reflexivity.
@@ -189,7 +189,7 @@ theorem Zplus_Zsucc_neg_pos:
 \forall n,m. Zsucc (neg n)+(pos m) = Zsucc ((neg n)+(pos m)).
 intros.
 apply nat_elim2
-(\lambda n,m. (Zsucc (neg n))+(pos m) = Zsucc ((neg n)+(pos m))).
+(\lambda n,m. Zsucc (neg n) + (pos m) = Zsucc (neg n + pos m)).
 intros.elim n1.
 simplify. reflexivity.
 elim n2.simplify. reflexivity.

diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma
index a36bd078c01877187072ee6fb804fd44beaacdaa..e356c4357b65e636944dfb05d4189b36bb6141b6 100644 (file)
--- a/helm/matita/library/Z/times.ma
+++ b/helm/matita/library/Z/times.ma
@@ -24,13 +24,13 @@ definition Ztimes :Z \to Z \to Z \def
     | (pos m) \Rightarrow
         match y with
          [ OZ \Rightarrow OZ
-         | (pos n) \Rightarrow (pos (pred (times (S m) (S n))))
-         | (neg n) \Rightarrow (neg (pred (times (S m) (S n))))]
+         | (pos n) \Rightarrow (pos (pred ((S m) * (S n))))
+         | (neg n) \Rightarrow (neg (pred ((S m) * (S n))))]
     | (neg m) \Rightarrow
         match y with
          [ OZ \Rightarrow OZ
-         | (pos n) \Rightarrow (neg (pred (times (S m) (S n))))
-         | (neg n) \Rightarrow (pos (pred (times (S m) (S n))))]].
+         | (pos n) \Rightarrow (neg (pred ((S m) * (S n))))
+         | (neg n) \Rightarrow (pos (pred ((S m) * (S n))))]].
          
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "integer times" 'times x y = (cic:/matita/Z/times/Ztimes.con x y).
@@ -42,33 +42,33 @@ 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)).
+theorem Ztimes_neg_Zopp: \forall n:nat.\forall x:Z.
+neg n * x = - (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).
+change with \forall x,y:Z. x*y = y*x.
 intros.elim x.rewrite > Ztimes_z_OZ.reflexivity.
 elim y.simplify.reflexivity. 
-change with eq Z (pos (pred (times (S n) (S n1)))) (pos (pred (times (S n1) (S n)))).
+change with pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n))).
 rewrite < sym_times.reflexivity.
-change with eq Z (neg (pred (times (S n) (S n1)))) (neg (pred (times (S n1) (S n)))).
+change with neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n))).
 rewrite < sym_times.reflexivity.
 elim y.simplify.reflexivity.
-change with eq Z (neg (pred (times (S n) (S n1)))) (neg (pred (times (S n1) (S n)))).
+change with neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n))).
 rewrite < sym_times.reflexivity.
-change with eq Z (pos (pred (times (S n) (S n1)))) (pos (pred (times (S n1) (S n)))).
+change with pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n))).
 rewrite < sym_times.reflexivity.
 qed.
 
-variant sym_Ztimes : \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x)
+variant sym_Ztimes : \forall x,y:Z. x*y = y*x
 \def symmetric_Ztimes.
 
 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)).
+change with \forall x,y,z:Z. (x*y)*z = x*(y*z).
 intros.elim x.
   simplify.reflexivity. 
   elim y.
@@ -76,25 +76,25 @@ intros.elim x.
     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))))))).
+       pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+       pos (pred ((S n) * (S (pred ((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))))))).
+       neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+       neg (pred ((S n) * (S (pred ((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))))))).
+       neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+       neg (pred ((S n) * (S (pred ((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))))))).
+       pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+       pos(pred ((S n) * (S (pred ((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.
@@ -102,42 +102,41 @@ intros.elim x.
     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))))))).
+       neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+       neg (pred ((S n) * (S (pred ((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))))))).
+       pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+       pos (pred ((S n) * (S (pred ((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))))))).
+       pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+       pos (pred ((S n) * (S (pred ((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))))))).
+       neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+       neg(pred ((S n) * (S (pred ((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 
+(x * y) * z = x * (y * z) \def 
 associative_Ztimes.
 
 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)))).
+(S n) * (S (pred ((S p) - (S q)))) =
+pred ((S n) * (S p)) - pred ((S n) * (S q)).
 intros.
 rewrite < S_pred.  
 rewrite > minus_pred_pred.
 rewrite < distr_times_minus. 
-reflexivity.  
+reflexivity.
 (* we now close all positivity conditions *)
 apply lt_O_times_S_S.                    
 apply lt_O_times_S_S.
@@ -149,23 +148,21 @@ 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))).
+change in match p + n * (S p) with pred ((S n) * (S p)).
+change in match q + n * (S q) with pred ((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))))))).
+change with pos (pred ((S n) * (S (pred ((S q) - (S p)))))) =
+            pos (pred ((pred ((S n) * (S q))) - (pred ((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))))))). 
+change with neg (pred ((S n) * (S (pred ((S p) - (S q)))))) =
+            neg (pred ((pred ((S n) * (S p))) - (pred ((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.  
@@ -181,35 +178,35 @@ apply sym_Zplus.
 qed.
 
 lemma distributive2_Ztimes_pos_Zplus: 
-distributive2 nat Z (\lambda n,z. Ztimes (pos n) z) Zplus.
+distributive2 nat Z (\lambda n,z. (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)).  
+(pos n) * (y + z) = (pos n) * y + (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))))).
+     pos (pred ((S n) * ((S n1) + (S n2)))) =
+     pos (pred ((S n) * (S n1) + (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 ((S n) * ((S n1) + (S n2)))) =
+     neg (pred ((S n) * (S n1) + (S n) * (S n2))).
     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
+(pos n) * (y + z) = ((pos n) * y + (pos n) * z) \def
 distributive2_Ztimes_pos_Zplus.
 
 lemma distributive2_Ztimes_neg_Zplus : 
-distributive2 nat Z (\lambda n,z. Ztimes (neg n) z) Zplus.
+distributive2 nat Z (\lambda n,z. (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)).  
+(neg n) * (y + z) = (neg n) * y + (neg n) * z.  
 intros.
 rewrite > Ztimes_neg_Zopp. 
 rewrite > distr_Ztimes_Zplus_pos.
@@ -219,12 +216,11 @@ 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
+(neg n) * (y + z) = (neg n) * y + (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)).
+change with \forall x,y,z:Z. x * (y + z) = x*y + x*z.
 intros.elim x.
 (* case x = OZ *)
 simplify.reflexivity.
@@ -235,5 +231,5 @@ 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
+x * (y + z) = x*y + x*z \def
 distributive_Ztimes_Zplus.

diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma
index 997229763f5fc77f4a62790ffe009bd1d65cd0f0..423399ff2c85449324be1f97ee243930182e0114 100644 (file)
--- a/helm/matita/library/Z/z.ma
+++ b/helm/matita/library/Z/z.ma
@@ -113,7 +113,7 @@ elim x.
     right.intro.
     apply not_eq_OZ_pos n. symmetry. assumption.
   (* goal: x=pos y=pos *)
-    elim (decidable_eq_nat n n1:(Or (n=n1) ((n=n1) \to False))).
+    elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False))).
     left.apply eq_f.assumption.
     right.intros [H_inj].apply H. injection H_inj. assumption.
   (* goal: x=pos y=neg *)
@@ -126,7 +126,7 @@ elim x.
   (* goal: x=neg y=pos *)
     right. intro. apply not_eq_pos_neg n1 n. symmetry. assumption.
   (* goal: x=neg y=neg *)
-    elim (decidable_eq_nat n n1:(Or (n=n1) ((n=n1) \to False))).
+    elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False))).
     left.apply eq_f.assumption.
     right.intro.apply H.apply injective_neg.assumption.
 qed.

diff --git a/helm/matita/library/nat/exp.ma b/helm/matita/library/nat/exp.ma
index a80a0cee362fc3fd4024dd565faec8df6d6f4373..19c09e27ccb6ae27633fa7809ced27cd71c73cbc 100644 (file)
--- a/helm/matita/library/nat/exp.ma
+++ b/helm/matita/library/nat/exp.ma
@@ -21,37 +21,39 @@ let rec exp n m on m\def
  [ O \Rightarrow (S O)
  | (S p) \Rightarrow (times n (exp n p)) ].
 
+interpretation "natural exponent" 'exp a b = (cic:/matita/nat/exp/exp.con a b).
+
 theorem exp_plus_times : \forall n,p,q:nat. 
-eq nat (exp n (plus p q)) (times (exp n p) (exp n q)).
+n \sup (p + q) = (n \sup p) * (n \sup 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).
+theorem exp_n_O : \forall n:nat. S O = n \sup O.
 intro.simplify.reflexivity.
 qed.
 
-theorem exp_n_SO : \forall n:nat. eq nat n (exp n (S O)).
+theorem exp_n_SO : \forall n:nat. n = n \sup (S O).
 intro.simplify.rewrite < times_n_SO.reflexivity.
 qed.
 
 theorem exp_exp_times : \forall n,p,q:nat. 
-eq nat (exp (exp n p) q) (exp n (times p q)).
+(n \sup p) \sup q = n \sup (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.
 
-theorem lt_O_exp: \forall n,m:nat. O < n \to O < exp n m. 
+theorem lt_O_exp: \forall n,m:nat. O < n \to O < n \sup m. 
 intros.elim m.simplify.apply le_n.
 simplify.rewrite > times_n_SO.
 apply le_times.assumption.assumption.
 qed.
 
-theorem lt_m_exp_nm: \forall n,m:nat. (S O) < n \to m < exp n m.
+theorem lt_m_exp_nm: \forall n,m:nat. (S O) < n \to m < n \sup m.
 intros.elim m.simplify.reflexivity.
 simplify.
 apply trans_le ? ((S(S O))*(S n1)).
@@ -63,17 +65,17 @@ apply le_times.assumption.assumption.
 qed.
 
 theorem exp_to_eq_O: \forall n,m:nat. (S O) < n 
-\to exp n m = (S O) \to m = O.
+\to n \sup m = (S O) \to m = O.
 intros.apply antisym_le.apply le_S_S_to_le.
-rewrite < H1.change with m < exp n m.
+rewrite < H1.change with m < n \sup m.
 apply lt_m_exp_nm.assumption.
 apply le_O_n.
 qed.
 
 theorem injective_exp_r: \forall n:nat. (S O) < n \to 
-injective nat nat (\lambda m:nat. exp n m).
+injective nat nat (\lambda m:nat. n \sup m).
 simplify.intros 4.
-apply nat_elim2 (\lambda x,y.exp n x = exp n y \to x = y).
+apply nat_elim2 (\lambda x,y.n \sup x = n \sup y \to x = y).
 intros.apply sym_eq.apply exp_to_eq_O n.assumption.
 rewrite < H1.reflexivity.
 intros.apply exp_to_eq_O n.assumption.assumption.
@@ -91,5 +93,5 @@ apply inj_times_r m1.assumption.
 qed.
 
 variant inj_exp_r: \forall p:nat. (S O) < p \to \forall n,m:nat.
-(exp p n) = (exp p m) \to n = m \def
-injective_exp_r.
\ No newline at end of file
+p \sup n = p \sup m \to n = m \def
+injective_exp_r.

diff --git a/helm/matita/library/nat/factorial.ma b/helm/matita/library/nat/factorial.ma
index 50345ee121e62aca628e4e82b9811e040199d08b..159559f092b271a4131fdab1b834f84ce600bf40 100644 (file)
--- a/helm/matita/library/nat/factorial.ma
+++ b/helm/matita/library/nat/factorial.ma
@@ -21,33 +21,35 @@ let rec fact n \def
   [ O \Rightarrow (S O)
   | (S m) \Rightarrow (S m)*(fact m)].
 
-theorem le_SO_fact : \forall n. (S O) \le (fact n).
+interpretation "factorial" 'fact n = (cic:/matita/nat/factorial/fact.con n).
+
+theorem le_SO_fact : \forall n. (S O) \le n !.
 intro.elim n.simplify.apply le_n.
-change with (S O) \le (S n1)*(fact n1).
+change with (S O) \le (S n1)*n1 !.
 apply trans_le ? ((S n1)*(S O)).simplify.
 apply le_S_S.apply le_O_n.
 apply le_times_r.assumption.
 qed.
 
-theorem le_SSO_fact : \forall n. (S O) < n \to (S(S O)) \le (fact n).
+theorem le_SSO_fact : \forall n. (S O) < n \to (S(S O)) \le n !.
 intro.apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S O) H.
-intros.change with (S (S O)) \le (S m)*(fact m).
+intros.change with (S (S O)) \le (S m)*m !.
 apply trans_le ? ((S(S O))*(S O)).apply le_n.
 apply le_times.exact H.apply le_SO_fact.
 qed.
 
-theorem le_n_fact_n: \forall n. n \le (fact n).
+theorem le_n_fact_n: \forall n. n \le n !.
 intro. elim n.apply le_O_n.
-change with S n1 \le (S n1)*(fact n1).
+change with S n1 \le (S n1)*n1 !.
 apply trans_le ? ((S n1)*(S O)).
 rewrite < times_n_SO.apply le_n.
 apply le_times.apply le_n.
 apply le_SO_fact.
 qed.
 
-theorem lt_n_fact_n: \forall n. (S(S O)) < n \to n < (fact n).
+theorem lt_n_fact_n: \forall n. (S(S O)) < n \to n < n !.
 intro.apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S(S O)) H.
-intros.change with (S m) < (S m)*(fact m).
+intros.change with (S m) < (S m)*m !.
 apply lt_to_le_to_lt ? ((S m)*(S (S O))).
 rewrite < sym_times.
 simplify.

diff --git a/helm/matita/library/nat/factorization.ma b/helm/matita/library/nat/factorization.ma
index c8127a1fa8cde6467be67ca32b6549466b56a566..43b942a5b828ea0305d7d3442e9f1db824c3ca8e 100644 (file)
--- a/helm/matita/library/nat/factorization.ma
+++ b/helm/matita/library/nat/factorization.ma
@@ -97,7 +97,7 @@ rewrite < H1.assumption.
 apply le_to_or_lt_eq (max_prime_factor r)  (max_prime_factor n).
 apply divides_to_max_prime_factor.
 assumption.assumption.
-apply witness r n (exp (nth_prime p) q).
+apply witness r n ((nth_prime p) \sup q).
 rewrite < sym_times.
 apply plog_aux_to_exp n n ? q r.
 apply lt_O_nth_prime_n.assumption.
@@ -111,7 +111,7 @@ intros.
 cut max_prime_factor n < p \lor max_prime_factor n = p.
 elim Hcut.apply le_to_lt_to_lt ? (max_prime_factor n).
 apply divides_to_max_prime_factor.assumption.assumption.
-apply witness r n (exp (nth_prime p) q).
+apply witness r n ((nth_prime p) \sup q).
 rewrite > sym_times.
 apply plog_aux_to_exp n n.
 apply lt_O_nth_prime_n.
@@ -154,9 +154,9 @@ definition factorize : nat \to nat_fact_all \def \lambda n:nat.
            
 let rec defactorize_aux f i \def
   match f with
-  [ (nf_last n) \Rightarrow exp (nth_prime i) (S n)
+  [ (nf_last n) \Rightarrow (nth_prime i) \sup (S n)
   | (nf_cons n g) \Rightarrow 
-      (exp (nth_prime i) n)*(defactorize_aux g (S i))].
+      (nth_prime i) \sup n *(defactorize_aux g (S i))].
       
 definition defactorize : nat_fact_all \to nat \def
 \lambda f : nat_fact_all. 
@@ -185,7 +185,7 @@ apply sym_eq.apply eq_pair_fst_snd.
 intros.
 rewrite < H3.
 simplify.
-cut n1 = r*(exp (nth_prime n) q).
+cut n1 = r * (nth_prime n) \sup q.
 rewrite > H.
 simplify.rewrite < assoc_times.
 rewrite < Hcut.reflexivity.
@@ -251,10 +251,10 @@ intros.
 rewrite < H.
 change with 
 defactorize_aux (factorize_aux p r (nf_last (pred q))) O = (S(S m1)).
-cut (S(S m1)) = (exp (nth_prime p) q)*r.
+cut (S(S m1)) = (nth_prime p) \sup q *r.
 cut O <r.
 rewrite > defactorize_aux_factorize_aux.
-change with r*(exp (nth_prime p) (S (pred q))) = (S(S m1)).
+change with r*(nth_prime p) \sup (S (pred q)) = (S(S m1)).
 cut (S (pred q)) = q.
 rewrite > Hcut2.
 rewrite > sym_times.
@@ -334,27 +334,27 @@ match f with
 theorem divides_max_p_defactorize: \forall f:nat_fact.\forall i:nat. 
 divides (nth_prime ((max_p f)+i)) (defactorize_aux f i).
 intro.
-elim f.simplify.apply witness ? ? (exp (nth_prime i) n).
+elim f.simplify.apply witness ? ? ((nth_prime i) \sup n).
 reflexivity.
 change with 
 divides (nth_prime (S(max_p n1)+i)) 
-((exp (nth_prime i) n)*(defactorize_aux n1 (S i))).
+((nth_prime i) \sup n *(defactorize_aux n1 (S i))).
 elim H (S i).
 rewrite > H1.
 rewrite < sym_times.
 rewrite > assoc_times.
 rewrite < plus_n_Sm.
-apply witness ? ? (n2*(exp (nth_prime i) n)).
+apply witness ? ? (n2* (nth_prime i) \sup n).
 reflexivity.
 qed.
 
 theorem divides_exp_to_divides: 
 \forall p,n,m:nat. prime p \to 
-divides p (exp n m) \to divides p n.
+divides p (n \sup m) \to divides p n.
 intros 3.elim m.simplify in H1.
 apply transitive_divides p (S O).assumption.
 apply divides_SO_n.
-cut divides p n \lor divides p (exp n n1).
+cut divides p n \lor divides p (n \sup n1).
 elim Hcut.assumption.
 apply H.assumption.assumption.
 apply divides_times_to_divides.assumption.
@@ -363,7 +363,7 @@ qed.
 
 theorem divides_exp_to_eq: 
 \forall p,q,m:nat. prime p \to prime q \to
-divides p (exp q m) \to p = q.
+divides p (q \sup m) \to p = q.
 intros.
 simplify in H1.
 elim H1.apply H4.
@@ -376,7 +376,7 @@ theorem  not_divides_defactorize_aux: \forall f:nat_fact. \forall i,j:nat.
 i < j \to \not divides (nth_prime i) (defactorize_aux f j).
 intro.elim f.
 change with
-divides (nth_prime i) (exp (nth_prime j) (S n)) \to False.
+divides (nth_prime i) ((nth_prime j) \sup (S n)) \to False.
 intro.absurd (nth_prime i) = (nth_prime j).
 apply divides_exp_to_eq ? ? (S n).
 apply prime_nth_prime.apply prime_nth_prime.
@@ -386,9 +386,9 @@ intro.cut i = j.
 apply not_le_Sn_n i.rewrite > Hcut in \vdash (? ? %).assumption.
 apply injective_nth_prime ? ? H2.
 change with 
-divides (nth_prime i) ((exp (nth_prime j) n)*(defactorize_aux n1 (S j))) \to False.
+divides (nth_prime i) ((nth_prime j) \sup n *(defactorize_aux n1 (S j))) \to False.
 intro.
-cut divides (nth_prime i) (exp (nth_prime j) n)
+cut divides (nth_prime i) ((nth_prime j) \sup n)
 \lor divides (nth_prime i) (defactorize_aux n1 (S j)).
 elim Hcut.
 absurd (nth_prime i) = (nth_prime j).
@@ -424,7 +424,7 @@ absurd divides (nth_prime (S(max_p n2)+i)) (defactorize_aux (nf_cons n1 n2) i).
 apply divides_max_p_defactorize.
 rewrite < H2.
 change with 
-(divides (nth_prime (S(max_p n2)+i)) (exp (nth_prime i) (S n))) \to False.
+(divides (nth_prime (S(max_p n2)+i)) ((nth_prime i) \sup (S n))) \to False.
 intro.
 absurd nth_prime (S (max_p n2) + i) = nth_prime i.
 apply divides_exp_to_eq ? ? (S n).
@@ -445,7 +445,7 @@ absurd divides (nth_prime (S(max_p n1)+i)) (defactorize_aux (nf_cons n n1) i).
 apply divides_max_p_defactorize.
 rewrite > H2.
 change with 
-(divides (nth_prime (S(max_p n1)+i)) (exp (nth_prime i) (S n2))) \to False.
+(divides (nth_prime (S(max_p n1)+i)) ((nth_prime i) \sup (S n2))) \to False.
 intro.
 absurd nth_prime (S (max_p n1) + i) = nth_prime i.
 apply divides_exp_to_eq ? ? (S n2).
@@ -460,8 +460,8 @@ apply injective_nth_prime ? ? H4.
 simplify in H3.
 generalize in match H3.
 apply nat_elim2 (\lambda n,n2.
-(exp (nth_prime i) n)*(defactorize_aux n1 (S i)) =
-(exp (nth_prime i) n2)*(defactorize_aux n3 (S i)) \to
+((nth_prime i) \sup n)*(defactorize_aux n1 (S i)) =
+((nth_prime i) \sup n2)*(defactorize_aux n3 (S i)) \to
 nf_cons n n1 = nf_cons n2 n3).
 intro.
 elim n4. apply eq_f.
@@ -476,7 +476,7 @@ simplify in H5.
 rewrite > plus_n_O (defactorize_aux n1 (S i)).
 rewrite > H5.
 rewrite > assoc_times.
-apply witness ? ? ((exp (nth_prime i) n5)*(defactorize_aux n3 (S i))).
+apply witness ? ? (((nth_prime i) \sup n5)*(defactorize_aux n3 (S i))).
 reflexivity.
 intros.
 apply False_ind.
@@ -486,7 +486,7 @@ simplify in H4.
 rewrite > plus_n_O (defactorize_aux n3 (S i)).
 rewrite < H4.
 rewrite > assoc_times.
-apply witness ? ? ((exp (nth_prime i) n4)*(defactorize_aux n1 (S i))).
+apply witness ? ? (((nth_prime i) \sup n4)*(defactorize_aux n1 (S i))).
 reflexivity.
 intros.
 cut nf_cons n4 n1 = nf_cons m n3.

diff --git a/helm/matita/library/nat/le_arith.ma b/helm/matita/library/nat/le_arith.ma
index dbf7b1c4298ca340b14791da95e44f1bfab3e988..7ece3fdc75b7053e1413bc30f963264d086cbf3b 100644 (file)
--- a/helm/matita/library/nat/le_arith.ma
+++ b/helm/matita/library/nat/le_arith.ma
@@ -19,40 +19,39 @@ include "nat/orders.ma".
 
 (* plus *)
 theorem monotonic_le_plus_r: 
-\forall n:nat.monotonic nat le (\lambda m.plus n m).
+\forall n:nat.monotonic nat le (\lambda m.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)
+theorem le_plus_r: \forall p,n,m:nat. n \le m \to p + n \le p + m
 \def monotonic_le_plus_r.
 
 theorem monotonic_le_plus_l: 
-\forall m:nat.monotonic nat le (\lambda n.plus n m).
+\forall m:nat.monotonic nat le (\lambda n.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)
+theorem le_plus_l: \forall p,n,m:nat. n \le m \to n + p \le 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).
+theorem le_plus: \forall n1,n2,m1,m2:nat. n1 \le n2  \to m1 \le m2 
+\to n1 + m1 \le n2 + m2.
 intros.
-apply trans_le ? (plus n2 m1).
+apply trans_le ? (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).
+theorem le_plus_n :\forall n,m:nat. m \le n + m.
+intros.change with O+m \le 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.
+theorem eq_plus_to_le: \forall n,m,p:nat.n=m+p \to m \le n.
 intros.rewrite > H.
 rewrite < sym_plus.
 apply le_plus_n.
@@ -60,7 +59,7 @@ qed.
 
 (* times *)
 theorem monotonic_le_times_r: 
-\forall n:nat.monotonic nat le (\lambda m.times n m).
+\forall n:nat.monotonic nat le (\lambda m. n * m).
 simplify.intros.elim n.
 simplify.apply le_O_n.
 simplify.apply le_plus.
@@ -68,28 +67,28 @@ assumption.
 assumption.
 qed.
 
-theorem le_times_r: \forall p,n,m:nat. le n m \to le (times p n) (times p m)
+theorem le_times_r: \forall p,n,m:nat. n \le m \to p*n \le p*m
 \def monotonic_le_times_r.
 
 theorem monotonic_le_times_l: 
-\forall m:nat.monotonic nat le (\lambda n.times n m).
+\forall m:nat.monotonic nat le (\lambda n.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)
+theorem le_times_l: \forall p,n,m:nat. n \le m \to n*p \le 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).
+theorem le_times: \forall n1,n2,m1,m2:nat. n1 \le n2  \to m1 \le m2 
+\to n1*m1 \le n2*m2.
 intros.
-apply trans_le ? (times n2 m1).
+apply trans_le ? (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).
+theorem le_times_n: \forall n,m:nat.(S O) \le n \to m \le n*m.
 intros.elim H.simplify.
 elim (plus_n_O ?).apply le_n.
 simplify.rewrite < sym_plus.apply le_plus_n.

diff --git a/helm/matita/library/nat/log.ma b/helm/matita/library/nat/log.ma
index 51d0108d97d89d937a488c68d6fbb7bc1e0a5323..e7fd12f15836693f941cfcd3696b2ff598cbb81e 100644 (file)
--- a/helm/matita/library/nat/log.ma
+++ b/helm/matita/library/nat/log.ma
@@ -36,7 +36,7 @@ definition plog \def \lambda n,m:nat.plog_aux n n m.
 
 theorem plog_aux_to_Prop: \forall p,n,m. O < m \to
   match plog_aux p n m with
-  [ (pair q r) \Rightarrow n = (exp m q)*r ].
+  [ (pair q r) \Rightarrow n = m \sup q *r ].
 intro.
 elim p.
 change with 
@@ -45,7 +45,7 @@ match (mod n m) with
   [ O \Rightarrow pair nat nat O n
   | (S a) \Rightarrow pair nat nat O n] )
 with
-  [ (pair q r) \Rightarrow n = (exp m q)*r ].
+  [ (pair q r) \Rightarrow n = m \sup q * r ].
 apply nat_case (mod n m).
 simplify.apply plus_n_O.
 intros.
@@ -58,14 +58,14 @@ match (mod n1 m) with
        [ (pair q r) \Rightarrow pair nat nat (S q) r]
   | (S a) \Rightarrow pair nat nat O n1] )
 with
-  [ (pair q r) \Rightarrow n1 = (exp m q)*r].
+  [ (pair q r) \Rightarrow n1 = m \sup q * r].
 apply nat_case1 (mod n1 m).intro.
 change with 
 match (
  match (plog_aux n (div n1 m) m) with
    [ (pair q r) \Rightarrow pair nat nat (S q) r])
 with
-  [ (pair q r) \Rightarrow n1 = (exp m q)*r].
+  [ (pair q r) \Rightarrow n1 = m \sup q * r].
 generalize in match (H (div n1 m) m).
 elim plog_aux n (div n1 m) m.
 simplify.
@@ -79,18 +79,18 @@ intros.simplify.apply plus_n_O.
 qed.
 
 theorem plog_aux_to_exp: \forall p,n,m,q,r. O < m \to
-  (pair nat nat q r) = plog_aux p n m \to n = (exp m q)*r.
+  (pair nat nat q r) = plog_aux p n m \to n = m \sup q * r.
 intros.
 change with 
 match (pair nat nat q r) with
-  [ (pair q r) \Rightarrow n = (exp m q)*r ].
+  [ (pair q r) \Rightarrow n = m \sup q * r ].
 rewrite > H1.
 apply plog_aux_to_Prop.
 assumption.
 qed.
 (* questo va spostato in primes1.ma *)
 theorem plog_exp: \forall n,m,i. O < m \to \not (mod n m = O) \to
-\forall p. i \le p \to plog_aux p ((exp m i)*n) m = pair nat nat i n.
+\forall p. i \le p \to plog_aux p (m \sup i * n) m = pair nat nat i n.
 intros 5.
 elim i.
 simplify.
@@ -120,24 +120,24 @@ generalize in match H3.
 apply nat_case p.intro.apply False_ind.apply not_le_Sn_O n1 H4.
 intros.
 change with
- match (mod ((exp m (S n1))*n) m) with
+ match (mod (m \sup (S n1) *n) m) with
   [ O \Rightarrow 
-       match (plog_aux m1 (div ((exp m (S n1))*n) m) m) with
+       match (plog_aux m1 (div (m \sup (S n1) *n) m) m) with
        [ (pair q r) \Rightarrow pair nat nat (S q) r]
-  | (S a) \Rightarrow pair nat nat O ((exp m (S n1))*n)]
+  | (S a) \Rightarrow pair nat nat O (m \sup (S n1) *n)]
   = pair nat nat (S n1) n.
-cut (mod ((exp m (S n1))*n) m) = O.
+cut (mod (m \sup (S n1)*n) m) = O.
 rewrite > Hcut.
 change with
-match (plog_aux m1 (div ((exp m (S n1))*n) m) m) with
+match (plog_aux m1 (div (m \sup (S n1)*n) m) m) with
        [ (pair q r) \Rightarrow pair nat nat (S q) r] 
   = pair nat nat (S n1) n. 
-cut div ((exp m (S n1))*n) m = (exp m n1)*n.
+cut div (m \sup (S n1) *n) m = m \sup n1 *n.
 rewrite > Hcut1.
 rewrite > H2 m1. simplify.reflexivity.
 apply le_S_S_to_le.assumption.
 (* div_exp *)
-change with div (m*(exp m n1)*n) m = (exp m n1)*n.
+change with div (m* m \sup n1 *n) m = m \sup n1 * n.
 rewrite > assoc_times.
 apply lt_O_n_elim m H.
 intro.apply div_times.
@@ -145,7 +145,7 @@ intro.apply div_times.
 apply divides_to_mod_O.
 assumption.
 simplify.rewrite > assoc_times.
-apply witness ? ? ((exp m n1)*n).reflexivity.
+apply witness ? ? (m \sup n1 *n).reflexivity.
 qed.
 
 theorem plog_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to

diff --git a/helm/matita/library/nat/lt_arith.ma b/helm/matita/library/nat/lt_arith.ma
index f8df1c6be9f171b1987ba7a493f344ce9e0c4521..19f25a967c0376dd2045007c67145c175ad94ed7 100644 (file)
--- a/helm/matita/library/nat/lt_arith.ma
+++ b/helm/matita/library/nat/lt_arith.ma
@@ -18,35 +18,35 @@ include "nat/div_and_mod.ma".
 
 (* plus *)
 theorem monotonic_lt_plus_r: 
-\forall n:nat.monotonic nat lt (\lambda m.plus n m).
+\forall n:nat.monotonic nat lt (\lambda m.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
+variant lt_plus_r: \forall n,p,q:nat. p < q \to n + p < 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).
+\forall n:nat.monotonic nat lt (\lambda m.m+n).
+change with \forall n,p,q:nat. p < q \to p + n < 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
+variant lt_plus_l: \forall n,p,q:nat. p < q \to p + n < 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).
+theorem lt_plus: \forall n,m,p,q:nat. n < m \to p < q \to n + p < m + q.
 intros.
-apply trans_lt ? (plus n q).
+apply trans_lt ? (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.
+theorem lt_plus_to_lt_l :\forall n,p,q:nat. p+n < q+n \to p<q.
 intro.elim n.
 rewrite > plus_n_O.
 rewrite > plus_n_O q.assumption.
@@ -57,53 +57,53 @@ 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.
+theorem lt_plus_to_lt_r :\forall n,p,q:nat. n+p < n+q \to 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)).
+theorem lt_O_times_S_S: \forall n,m:nat.O < (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).
+\forall n:nat.monotonic nat lt (\lambda m.(S n)*m).
+change with \forall n,p,q:nat. p < q \to (S n) * p < (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)).
+change with p + (S n1) * p < q + (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)
+theorem lt_times_r: \forall n,p,q:nat. p < q \to (S n) * p < (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)).
+\forall m:nat.monotonic nat lt (\lambda n.n * (S m)).
 change with 
-\forall n,p,q:nat. lt p q \to lt (times p (S n)) (times q (S n)).
+\forall n,p,q:nat. p < q \to p*(S n) < 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))
+variant lt_times_l: \forall n,p,q:nat. p<q \to p*(S n) < 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).
+theorem lt_times:\forall n,m,p,q:nat. n<m \to p<q \to n*p < 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)).
+intro.change with O < (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 trans_lt ? ((S n1)*q).
 apply lt_times_r.assumption.
 cut lt O q.
 apply lt_O_n_elim q Hcut.
@@ -114,12 +114,12 @@ 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.
+\forall n,p,q:nat. p*(S n) < q*(S n) \to p < q.
 intros.
-cut Or (lt p q) (Not (lt p q)).
+cut p < q \lor \lnot (p < q).
 elim Hcut.
 assumption.
-absurd lt (times p (S n)) (times q (S n)).
+absurd p * (S n) < q * (S n).
 assumption.
 apply le_to_not_lt.
 apply le_times_l.
@@ -129,7 +129,7 @@ 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.
+\forall n,p,q:nat. (S n)*p < (S n)*q \to lt p q.
 intros.
 apply lt_times_to_lt_l n.
 rewrite < sym_times.
@@ -138,22 +138,22 @@ 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)).
+nat_compare p q = nat_compare ((S n) * p) ((S n) * q).
 intros.apply nat_compare_elim.intro.
 apply nat_compare_elim.
 intro.reflexivity.
-intro.absurd eq nat p q.
+intro.absurd p=q.
 apply inj_times_r n.assumption.
 apply lt_to_not_eq. assumption.
-intro.absurd lt q p.
+intro.absurd 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).
+absurd 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.
+intro.absurd q=p.
 symmetry.
 apply inj_times_r n.assumption.
 apply lt_to_not_eq.assumption.
@@ -214,4 +214,4 @@ theorem increasing_to_injective: \forall f:nat\to nat.
 increasing f \to injective nat nat f.
 intros.apply monotonic_to_injective.
 apply increasing_to_monotonic.assumption.
-qed.
\ No newline at end of file
+qed.

diff --git a/helm/matita/library/nat/nth_prime.ma b/helm/matita/library/nat/nth_prime.ma
index 200ccba5a9086b0ca2a940c7f19ae0964bb8402c..f165705ac42e04a6a88168149ad0bfd580af239b 100644 (file)
--- a/helm/matita/library/nat/nth_prime.ma
+++ b/helm/matita/library/nat/nth_prime.ma
@@ -39,11 +39,11 @@ normalize.reflexivity.
 qed. *)
 
 theorem smallest_factor_fact: \forall n:nat.
-n < smallest_factor (S (fact n)).
+n < smallest_factor (S (n !)).
 intros.
 apply not_le_to_lt.
-change with smallest_factor (S (fact n)) \le n \to False.intro.
-apply not_divides_S_fact n (smallest_factor(S (fact n))).
+change with smallest_factor (S (n !)) \le n \to False.intro.
+apply not_divides_S_fact n (smallest_factor(S (n !))).
 apply lt_SO_smallest_factor.
 simplify.apply le_S_S.apply le_SO_fact.
 assumption.
@@ -52,19 +52,19 @@ simplify.apply le_S_S.apply le_O_n.
 qed.
 
 theorem ex_prime: \forall n. (S O) \le n \to \exists m.
-n < m \land m \le (S (fact n)) \land (prime m).
+n < m \land m \le (S (n !)) \land (prime m).
 intros.
 elim H.
 apply ex_intro nat ? (S(S O)).
 split.split.apply le_n (S(S O)).
 apply le_n (S(S O)).apply primeb_to_Prop (S(S O)).
-apply ex_intro nat ? (smallest_factor (S (fact (S n1)))).
+apply ex_intro nat ? (smallest_factor (S ((S n1) !))).
 split.split.
 apply smallest_factor_fact.
 apply le_smallest_factor_n.
 (* Andrea: ancora hint non lo trova *)
 apply prime_smallest_factor_n.
-change with (S(S O)) \le S (fact (S n1)).
+change with (S(S O)) \le S ((S n1) !).
 apply le_S.apply le_SSO_fact.
 simplify.apply le_S_S.assumption.
 qed.
@@ -74,7 +74,7 @@ match n with
   [ O \Rightarrow (S(S O))
   | (S p) \Rightarrow
     let previous_prime \def (nth_prime p) in
-    let upper_bound \def S (fact previous_prime) in
+    let upper_bound \def S (previous_prime !) in
     min_aux (upper_bound - (S previous_prime)) upper_bound primeb].
     
 (* it works, but nth_prime 4 takes already a few minutes -
@@ -100,13 +100,13 @@ apply primeb_to_Prop (S(S O)).
 intro.
 change with
 let previous_prime \def (nth_prime m) in
-let upper_bound \def S (fact previous_prime) in
+let upper_bound \def S (previous_prime !) in
 prime (min_aux (upper_bound - (S previous_prime)) upper_bound primeb).
 apply primeb_true_to_prime.
 apply f_min_aux_true.
-apply ex_intro nat ? (smallest_factor (S (fact (nth_prime m)))).
+apply ex_intro nat ? (smallest_factor (S ((nth_prime m) !))).
 split.split.
-cut S (fact (nth_prime m))-(S (fact (nth_prime m)) - (S (nth_prime m))) = (S (nth_prime m)).
+cut S ((nth_prime m) !)-(S ((nth_prime m) !) - (S (nth_prime m))) = (S (nth_prime m)).
 rewrite > Hcut.exact smallest_factor_fact (nth_prime m).
 (* maybe we could factorize this proof *)
 apply plus_to_minus.
@@ -117,7 +117,7 @@ apply le_n_fact_n.
 apply le_smallest_factor_n.
 apply prime_to_primeb_true.
 apply prime_smallest_factor_n.
-change with (S(S O)) \le S (fact (nth_prime m)).
+change with (S(S O)) \le S ((nth_prime m) !).
 apply le_S_S.apply le_SO_fact.
 qed.
 
@@ -127,7 +127,7 @@ change with \forall n:nat. (nth_prime n) < (nth_prime (S n)).
 intros.
 change with
 let previous_prime \def (nth_prime n) in
-let upper_bound \def S (fact previous_prime) in
+let upper_bound \def S (previous_prime !) in
 (S previous_prime) \le min_aux (upper_bound - (S previous_prime)) upper_bound primeb.
 intros.
 cut upper_bound - (upper_bound -(S previous_prime)) = (S previous_prime).
@@ -172,9 +172,9 @@ theorem lt_nth_prime_to_not_prime: \forall n,m. nth_prime n < m \to m < nth_prim
 intros.
 apply primeb_false_to_not_prime.
 letin previous_prime \def nth_prime n.
-letin upper_bound \def S (fact previous_prime).
+letin upper_bound \def S (previous_prime !).
 apply lt_min_aux_to_false primeb upper_bound (upper_bound - (S previous_prime)) m.
-cut S (fact (nth_prime n))-(S (fact (nth_prime n)) - (S (nth_prime n))) = (S (nth_prime n)).
+cut S ((nth_prime n) !)-(S ((nth_prime n) !) - (S (nth_prime n))) = (S (nth_prime n)).
 rewrite > Hcut.assumption.
 apply plus_to_minus.
 apply le_minus_m.

diff --git a/helm/matita/library/nat/primes.ma b/helm/matita/library/nat/primes.ma
index dc5f627e43103119199d71747a837c60b8595cf4..505d3de496053c56b8de48232387891ea19a5a1e 100644 (file)
--- a/helm/matita/library/nat/primes.ma
+++ b/helm/matita/library/nat/primes.ma
@@ -237,23 +237,23 @@ qed.
 
 (* divides and fact *)
 theorem divides_fact : \forall n,i:nat. 
-O < i \to i \le n \to divides i (fact n).
+O < i \to i \le n \to divides i (n !).
 intros 3.elim n.absurd O<i.assumption.apply le_n_O_elim i H1.
 apply not_le_Sn_O O.
-change with divides i ((S n1)*(fact n1)).
+change with divides i ((S n1)*(n1 !)).
 apply le_n_Sm_elim i n1 H2.
 intro.
-apply transitive_divides ? (fact n1).
+apply transitive_divides ? (n1 !).
 apply H1.apply le_S_S_to_le. assumption.
 apply witness ? ? (S n1).apply sym_times.
 intro.
 rewrite > H3.
-apply witness ? ? (fact n1).reflexivity.
+apply witness ? ? (n1 !).reflexivity.
 qed.
 
 theorem mod_S_fact: \forall n,i:nat. 
-(S O) < i \to i \le n \to mod (S (fact n)) i = (S O).
-intros.cut mod (fact n) i = O.
+(S O) < i \to i \le n \to mod (S (n !)) i = (S O).
+intros.cut mod (n !) i = O.
 rewrite < Hcut.
 apply mod_S.apply trans_lt O (S O).apply le_n (S O).assumption.
 rewrite > Hcut.assumption.
@@ -263,11 +263,11 @@ assumption.
 qed.
 
 theorem not_divides_S_fact: \forall n,i:nat. 
-(S O) < i \to i \le n \to \not (divides i (S (fact n))).
+(S O) < i \to i \le n \to \not (divides i (S (n !))).
 intros.
 apply divides_b_false_to_not_divides.
 apply trans_lt O (S O).apply le_n (S O).assumption.
-change with (eqb (mod (S (fact n)) i) O) = false.
+change with (eqb (mod (S (n !)) i) O) = false.
 rewrite > mod_S_fact.simplify.reflexivity.
 assumption.assumption.
 qed.

diff --git a/helm/matita/library/nat/primes1.ma b/helm/matita/library/nat/primes1.ma
index 3df3922a4887d50e19fc4ec3e0f5acfffadb2ec4..37fcbd21fe3b2762bae5f0f504cb58ff55918c62 100644 (file)
--- a/helm/matita/library/nat/primes1.ma
+++ b/helm/matita/library/nat/primes1.ma
@@ -32,7 +32,7 @@ definition n_divides \def \lambda n,m:nat.n_divides_aux n n m O.
 (*
 theorem n_divides_to_Prop: \forall n,m,p,a. 
   match n_divides_aux p n m a with
-  [ (pair q r) \Rightarrow n = (exp m a)*r].
+  [ (pair q r) \Rightarrow n = m \sup a *r].
 intros.
 apply nat_case (mod n m). *)