From 373b88228a8f9a6b4b4dcf781bc166865f89f43d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 22 Sep 2005 11:59:54 +0000 Subject: [PATCH] More notation here and there. --- helm/matita/core_notation.moo | 8 ++ helm/matita/library/Q/q.ma | 60 ++++++------- helm/matita/library/Z/plus.ma | 6 +- helm/matita/library/Z/times.ma | 106 +++++++++++------------ helm/matita/library/Z/z.ma | 4 +- helm/matita/library/nat/exp.ma | 26 +++--- helm/matita/library/nat/factorial.ma | 18 ++-- helm/matita/library/nat/factorization.ma | 44 +++++----- helm/matita/library/nat/le_arith.ma | 37 ++++---- helm/matita/library/nat/log.ma | 30 +++---- helm/matita/library/nat/lt_arith.ma | 60 ++++++------- helm/matita/library/nat/nth_prime.ma | 28 +++--- helm/matita/library/nat/primes.ma | 16 ++-- helm/matita/library/nat/primes1.ma | 2 +- 14 files changed, 226 insertions(+), 219 deletions(-) diff --git a/helm/matita/core_notation.moo b/helm/matita/core_notation.moo index c528fc111..9af57e4fe 100644 --- 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 1ff2adcd8..f04603f15 100644 --- 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 b89f291fb..0456ca0b3 100644 --- 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 a36bd078c..e356c4357 100644 --- 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 997229763..423399ff2 100644 --- 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 a80a0cee3..19c09e27c 100644 --- 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 50345ee12..159559f09 100644 --- 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 c8127a1fa..43b942a5b 100644 --- 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 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 dbf7b1c42..7ece3fdc7 100644 --- 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 51d0108d9..e7fd12f15 100644 --- 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 f8df1c6be..19f25a967 100644 --- 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 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 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 nat_compare_n_n.reflexivity. intro.apply nat_compare_elim.intro. -absurd (lt p q). +absurd p 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 dc5f627e4..505d3de49 100644 --- 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 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 3df3922a4..37fcbd21f 100644 --- 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). *) -- 2.39.2