From: Stefano Zacchiroli Date: Tue, 25 Oct 2005 13:48:39 +0000 (+0000) Subject: ported to new syntactic requirement about terms being surrounded by parens X-Git-Tag: V_0_7_2_3~193 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fb94e5a71be508516514dfe50528ccfb3cd2da91;p=helm.git ported to new syntactic requirement about terms being surrounded by parens --- diff --git a/helm/matita/library/Q/q.ma b/helm/matita/library/Q/q.ma index 6e3639f6e..d69e459ac 100644 --- a/helm/matita/library/Q/q.ma +++ b/helm/matita/library/Q/q.ma @@ -93,27 +93,27 @@ definition ftl \def theorem injective_pp : injective nat fraction pp. simplify.intros. -change with (aux (pp x)) = (aux (pp y)). +change with ((aux (pp x)) = (aux (pp y))). apply eq_f.assumption. qed. theorem injective_nn : injective nat fraction nn. simplify.intros. -change with (aux (nn x)) = (aux (nn y)). +change with ((aux (nn x)) = (aux (nn y))). apply eq_f.assumption. qed. theorem eq_cons_to_eq1: \forall f,g:fraction.\forall x,y:Z. (cons x f) = (cons y g) \to x = y. intros. -change with (fhd (cons x f)) = (fhd (cons y g)). +change with ((fhd (cons x f)) = (fhd (cons y g))). apply eq_f.assumption. qed. theorem eq_cons_to_eq2: \forall x,y:Z.\forall f,g:fraction. (cons x f) = (cons y g) \to f = g. intros. -change with (ftl (cons x f)) = (ftl (cons y g)). +change with ((ftl (cons x f)) = (ftl (cons y g))). apply eq_f.assumption. qed. @@ -154,7 +154,7 @@ qed. theorem decidable_eq_fraction: \forall f,g:fraction. decidable (f = g). intros.simplify. -apply fraction_elim2 (\lambda f,g. f=g \lor (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) : n=n1 \lor (n=n1 \to False)). left.apply eq_f. assumption. @@ -162,29 +162,29 @@ apply fraction_elim2 (\lambda f,g. f=g \lor (f=g \to False)). 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. + right.intro.apply (not_eq_pp_nn n1 n).apply sym_eq. assumption. 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.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) : 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. - right.intro.apply H1.apply eq_cons_to_eq2 x y f1 g1.assumption. + right.intro.apply H2.apply (eq_cons_to_eq1 f1 g1).assumption. + right.intro.apply H1.apply (eq_cons_to_eq2 x y f1 g1).assumption. qed. theorem eqfb_to_Prop: \forall f,g:fraction. match (eqfb f g) with [true \Rightarrow f=g |false \Rightarrow f \neq g]. -intros.apply fraction_elim2 +intros.apply (fraction_elim2 (\lambda f,g.match (eqfb f g) with [true \Rightarrow f=g -|false \Rightarrow f \neq g]). +|false \Rightarrow f \neq g])). intros.elim g1. simplify.apply eqb_elim. intro.simplify.apply eq_f.assumption. @@ -192,12 +192,12 @@ intros.apply fraction_elim2 simplify.apply not_eq_pp_nn. simplify.apply not_eq_pp_cons. intros.elim g1. - simplify.intro.apply not_eq_pp_nn n1 n.apply sym_eq. assumption. + simplify.intro.apply (not_eq_pp_nn n1 n).apply sym_eq. assumption. simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption. intro.simplify.intro.apply H.apply injective_nn.assumption. simplify.apply not_eq_nn_cons. - intros.simplify.intro.apply not_eq_pp_cons m x f1.apply sym_eq. assumption. - intros.simplify.intro.apply not_eq_nn_cons m x f1.apply sym_eq. assumption. + intros.simplify.intro.apply (not_eq_pp_cons m x f1).apply sym_eq. assumption. + intros.simplify.intro.apply (not_eq_nn_cons m x f1).apply sym_eq. assumption. intros. change in match (eqfb (cons x f1) (cons y g1)) with (andb (eqZb x y) (eqfb f1 g1)). @@ -205,8 +205,8 @@ intros.apply fraction_elim2 intro.generalize in match H.elim (eqfb f1 g1). simplify.apply eq_f2.assumption. apply H2. - simplify.intro.apply H2.apply eq_cons_to_eq2 x y.assumption. - intro.simplify.intro.apply H1.apply eq_cons_to_eq1 f1 g1.assumption. + simplify.intro.apply H2.apply (eq_cons_to_eq2 x y).assumption. + intro.simplify.intro.apply H1.apply (eq_cons_to_eq1 f1 g1).assumption. qed. let rec finv f \def @@ -243,47 +243,47 @@ let rec ftimes f g \def | (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). +simplify. intros.apply (fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f)). intros.elim g. - change with Z_to_ratio (pos n + pos n1) = Z_to_ratio (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 (pos n + neg n1) = Z_to_ratio (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 (pos n + z) f) = frac (cons (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 (neg n + pos n1) = Z_to_ratio (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 (neg n + neg n1) = Z_to_ratio (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 (neg n + z) f) = frac (cons (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 (x1 + pos m) f) = frac (cons (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 (x1 + neg m) f) = frac (cons (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 + (match ftimes f g with [ 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 (y1 + x1) - | (frac h) \Rightarrow frac (cons (y1 + x1) h)]. + | (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 (pos n + - (pos n)) = one. + change with (Z_to_ratio (pos n + - (pos n)) = one). rewrite > Zplus_Zopp.reflexivity. - change with Z_to_ratio (neg n + - (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 + (match ftimes f1 (finv f1) with [ one \Rightarrow Z_to_ratio (z + - z) - | (frac h) \Rightarrow frac (cons (z + - z) h)] = one. + | (frac h) \Rightarrow frac (cons (z + - z) h)] = one). rewrite > H.rewrite > Zplus_Zopp.reflexivity. qed. @@ -297,7 +297,7 @@ definition rtimes : ratio \to ratio \to ratio \def | (frac g) \Rightarrow ftimes f g]]. theorem symmetric_rtimes : symmetric ratio rtimes. -change with \forall r,s:ratio. rtimes r s = rtimes s r. +change with (\forall r,s:ratio. rtimes r s = rtimes s r). intros. elim r. elim s. reflexivity. diff --git a/helm/matita/library/Z/compare.ma b/helm/matita/library/Z/compare.ma index 1bf4f066a..a59100885 100644 --- a/helm/matita/library/Z/compare.ma +++ b/helm/matita/library/Z/compare.ma @@ -49,14 +49,14 @@ elim x. simplify.apply not_eq_OZ_pos. simplify.apply not_eq_OZ_neg. elim y. - simplify.intro.apply not_eq_OZ_pos n.apply sym_eq.assumption. + simplify.intro.apply (not_eq_OZ_pos n).apply sym_eq.assumption. simplify.apply eqb_elim. intro.simplify.apply eq_f.assumption. intro.simplify.intro.apply H.apply inj_pos.assumption. simplify.apply not_eq_pos_neg. elim y. - simplify.intro.apply not_eq_OZ_neg n.apply sym_eq.assumption. - simplify.intro.apply not_eq_pos_neg n1 n.apply sym_eq.assumption. + simplify.intro.apply (not_eq_OZ_neg n).apply sym_eq.assumption. + simplify.intro.apply (not_eq_pos_neg n1 n).apply sym_eq.assumption. simplify.apply eqb_elim. intro.simplify.apply eq_f.assumption. intro.simplify.intro.apply H.apply inj_neg.assumption. @@ -66,14 +66,14 @@ theorem eqZb_elim: \forall x,y:Z.\forall P:bool \to Prop. (x=y \to (P true)) \to (x \neq y \to (P false)) \to P (eqZb x y). intros. cut -match (eqZb x y) with +(match (eqZb x y) with [ true \Rightarrow x=y -| false \Rightarrow x \neq y] \to P (eqZb x y). +| false \Rightarrow x \neq y] \to P (eqZb x y)). apply Hcut. apply eqZb_to_Prop. elim (eqZb). -apply H H2. -apply H1 H2. +apply (H H2). +apply (H1 H2). qed. definition Z_compare : Z \to Z \to compare \def @@ -109,14 +109,14 @@ elim x. elim y. simplify.exact I. simplify. - cut match (nat_compare n n1) with + cut (match (nat_compare n n1) with [ LT \Rightarrow n Zpred_Zsucc.simplify.reflexivity. apply Zplus_neg_pos. rewrite < Zplus_neg_neg.reflexivity. @@ -154,8 +154,8 @@ qed. theorem Zplus_Zsucc_pos_neg: \forall n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))). intros. -apply nat_elim2 -(\lambda n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m)))).intro. +apply (nat_elim2 +(\lambda n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))))).intro. intros.elim n1. simplify. reflexivity. elim n2.simplify. reflexivity. @@ -171,8 +171,8 @@ qed. theorem Zplus_Zsucc_neg_neg : \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. +apply (nat_elim2 +(\lambda n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m))).intro. intros.elim n1. simplify. reflexivity. elim n2.simplify. reflexivity. @@ -188,8 +188,8 @@ qed. 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)). +apply (nat_elim2 +(\lambda n,m. Zsucc (neg n) + (pos m) = Zsucc (neg n + pos m))). intros.elim n1. simplify. reflexivity. elim n2.simplify. reflexivity. @@ -210,18 +210,18 @@ intros.elim x. simplify.reflexivity. rewrite < Zsucc_Zplus_pos_O.reflexivity. elim y. - rewrite < sym_Zplus OZ.reflexivity. + rewrite < (sym_Zplus OZ).reflexivity. apply Zplus_Zsucc_pos_pos. apply Zplus_Zsucc_pos_neg. elim y. - rewrite < sym_Zplus.rewrite < sym_Zplus OZ.simplify.reflexivity. + rewrite < sym_Zplus.rewrite < (sym_Zplus OZ).simplify.reflexivity. apply Zplus_Zsucc_neg_pos. apply Zplus_Zsucc_neg_neg. qed. theorem Zplus_Zpred: \forall x,y:Z. (Zpred x)+y = Zpred (x+y). intros. -cut Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y). +cut (Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y)). rewrite > Hcut. rewrite > Zplus_Zsucc. rewrite > Zpred_Zsucc. @@ -232,20 +232,20 @@ qed. theorem associative_Zplus: associative Z Zplus. -change with \forall x,y,z:Z. (x + y) + z = x + (y + z). +change with (\forall x,y,z:Z. (x + y) + z = x + (y + z)). (* simplify. *) intros.elim x. simplify.reflexivity. elim n. rewrite < Zsucc_Zplus_pos_O.rewrite < Zsucc_Zplus_pos_O. rewrite > Zplus_Zsucc.reflexivity. - rewrite > Zplus_Zsucc (pos n1).rewrite > Zplus_Zsucc (pos n1). - rewrite > Zplus_Zsucc ((pos n1)+y).apply eq_f.assumption. + rewrite > (Zplus_Zsucc (pos n1)).rewrite > (Zplus_Zsucc (pos n1)). + rewrite > (Zplus_Zsucc ((pos n1)+y)).apply eq_f.assumption. elim n. rewrite < (Zpred_Zplus_neg_O (y+z)).rewrite < (Zpred_Zplus_neg_O y). rewrite < Zplus_Zpred.reflexivity. - rewrite > Zplus_Zpred (neg n1).rewrite > Zplus_Zpred (neg n1). - rewrite > Zplus_Zpred ((neg n1)+y).apply eq_f.assumption. + rewrite > (Zplus_Zpred (neg n1)).rewrite > (Zplus_Zpred (neg n1)). + rewrite > (Zplus_Zpred ((neg n1)+y)).apply eq_f.assumption. qed. variant assoc_Zplus : \forall x,y,z:Z. (x+y)+z = x+(y+z) diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma index e356c4357..19158e300 100644 --- a/helm/matita/library/Z/times.ma +++ b/helm/matita/library/Z/times.ma @@ -50,17 +50,17 @@ simplify.reflexivity. simplify.reflexivity. qed. theorem symmetric_Ztimes : symmetric Z Ztimes. -change with \forall x,y:Z. x*y = 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 pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n))). +change with (pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n)))). rewrite < sym_times.reflexivity. -change with neg (pred ((S n) * (S n1))) = neg (pred ((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 neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n))). +change with (neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n)))). rewrite < sym_times.reflexivity. -change with pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n))). +change with (pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n)))). rewrite < sym_times.reflexivity. qed. @@ -68,7 +68,7 @@ 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. (x*y)*z = x*(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 - pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) = - pos (pred ((S n) * (S (pred ((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 - neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) = - neg (pred ((S n) * (S (pred ((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 - neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) = - neg (pred ((S n) * (S (pred ((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 - pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) = - pos(pred ((S n) * (S (pred ((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,25 +102,25 @@ intros.elim x. elim z. simplify.reflexivity. change with - neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) = - neg (pred ((S n) * (S (pred ((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 - pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) = - pos (pred ((S n) * (S (pred ((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 - pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) = - pos (pred ((S n) * (S (pred ((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 - neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) = - neg(pred ((S n) * (S (pred ((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. @@ -148,22 +148,22 @@ 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 p + n * (S p) with pred ((S n) * (S p)). -change in match q + n * (S q) with pred ((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. +apply (nat_compare_elim p q). intro. (* uff *) -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. +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 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. +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. apply lt_O_times_S_S. @@ -179,23 +179,23 @@ qed. lemma distributive2_Ztimes_pos_Zplus: distributive2 nat Z (\lambda n,z. (pos n) * z) Zplus. -change with \forall n,y,z. -(pos n) * (y + z) = (pos n) * y + (pos n) * z. +change with (\forall n,y,z. +(pos n) * (y + z) = (pos n) * y + (pos n) * z). intros.elim y. reflexivity. elim z. reflexivity. change with - pos (pred ((S n) * ((S n1) + (S n2)))) = - pos (pred ((S n) * (S n1) + (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 - neg (pred ((S n) * ((S n1) + (S n2)))) = - neg (pred ((S n) * (S n1) + (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. @@ -205,8 +205,8 @@ distributive2_Ztimes_pos_Zplus. lemma distributive2_Ztimes_neg_Zplus : distributive2 nat Z (\lambda n,z. (neg n) * z) Zplus. -change with \forall n,y,z. -(neg n) * (y + z) = (neg n) * y + (neg n) * z. +change with (\forall n,y,z. +(neg n) * (y + z) = (neg n) * y + (neg n) * z). intros. rewrite > Ztimes_neg_Zopp. rewrite > distr_Ztimes_Zplus_pos. @@ -220,7 +220,7 @@ variant distr_Ztimes_Zplus_neg: \forall n,y,z. distributive2_Ztimes_neg_Zplus. theorem distributive_Ztimes_Zplus: distributive Z Ztimes Zplus. -change with \forall x,y,z:Z. x * (y + z) = x*y + x*z. +change with (\forall x,y,z:Z. x * (y + z) = x*y + x*z). intros.elim x. (* case x = OZ *) simplify.reflexivity. diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma index 8ce0047e1..d1a846da4 100644 --- a/helm/matita/library/Z/z.ma +++ b/helm/matita/library/Z/z.ma @@ -54,9 +54,9 @@ match OZ_test z with |false \Rightarrow z \neq OZ]. intros.elim z. simplify.reflexivity. -simplify.intros [H]. +simplify.intros (H). discriminate H. -simplify.intros [H]. +simplify.intros (H). discriminate H. qed. @@ -64,7 +64,7 @@ qed. theorem injective_pos: injective nat Z pos. simplify. intros. -change with abs (pos x) = abs (pos y). +change with (abs (pos x) = abs (pos y)). apply eq_f.assumption. qed. @@ -74,7 +74,7 @@ variant inj_pos : \forall n,m:nat. pos n = pos m \to n = m theorem injective_neg: injective nat Z neg. simplify. intros. -change with abs (neg x) = abs (neg y). +change with (abs (neg x) = abs (neg y)). apply eq_f.assumption. qed. @@ -82,17 +82,17 @@ variant inj_neg : \forall n,m:nat. neg n = neg m \to n = m \def injective_neg. theorem not_eq_OZ_pos: \forall n:nat. OZ \neq pos n. -simplify.intros [n; H]. +simplify.intros (n H). discriminate H. qed. theorem not_eq_OZ_neg :\forall n:nat. OZ \neq neg n. -simplify.intros [n; H]. +simplify.intros (n H). discriminate H. qed. theorem not_eq_pos_neg :\forall n,m:nat. pos n \neq neg m. -simplify.intros [n; m; H]. +simplify.intros (n m H). discriminate H. qed. @@ -111,20 +111,20 @@ elim x. elim y. (* goal: x=pos y=OZ *) right.intro. - apply not_eq_OZ_pos n. symmetry. assumption. + apply (not_eq_OZ_pos n). symmetry. assumption. (* goal: x=pos y=pos *) 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. + right.intros (H_inj).apply H. injection H_inj. assumption. (* goal: x=pos y=neg *) - right.intro.apply not_eq_pos_neg n n1. assumption. + right.intro.apply (not_eq_pos_neg n n1). assumption. (* goal: x=neg *) elim y. (* goal: x=neg y=OZ *) right.intro. - apply not_eq_OZ_neg n. symmetry. assumption. + apply (not_eq_OZ_neg n). symmetry. assumption. (* goal: x=neg y=pos *) - right. intro. apply not_eq_pos_neg n1 n. symmetry. assumption. + right. intro. apply (not_eq_pos_neg n1 n). symmetry. assumption. (* goal: x=neg y=neg *) elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False))). left.apply eq_f.assumption. diff --git a/helm/matita/library/logic/equality.ma b/helm/matita/library/logic/equality.ma index a5d2f0d1e..ed257afa4 100644 --- a/helm/matita/library/logic/equality.ma +++ b/helm/matita/library/logic/equality.ma @@ -48,7 +48,7 @@ theorem trans_eq : \forall A:Type.\forall x,y,z:A. x=y \to y=z \to x=z theorem eq_elim_r: \forall A:Type.\forall x:A. \forall P: A \to Prop. P x \to \forall y:A. y=x \to P y. -intros. elim sym_eq ? ? ? H1.assumption. +intros. elim (sym_eq ? ? ? H1).assumption. qed. default "equality" @@ -68,3 +68,20 @@ theorem eq_f2: \forall A,B,C:Type.\forall f:A\to B \to C. x1=x2 \to y1=y2 \to f x1 y1 = f x2 y2. intros.elim H1.elim H.reflexivity. qed. + +(* +theorem a:\forall x.x=x\land True. +[ +2:intros; + split; + [ + exact (refl_eq Prop x); + | + exact I; + ] +1: + skip +] +qed. +*) + diff --git a/helm/matita/library/nat/compare.ma b/helm/matita/library/nat/compare.ma index 55e526c8f..6431f5f29 100644 --- a/helm/matita/library/nat/compare.ma +++ b/helm/matita/library/nat/compare.ma @@ -34,19 +34,19 @@ match (eqb n m) with [ true \Rightarrow n = m | false \Rightarrow n \neq m]. intros. -apply nat_elim2 +apply (nat_elim2 (\lambda n,m:nat.match (eqb n m) with [ true \Rightarrow n = m -| false \Rightarrow n \neq m]). +| false \Rightarrow n \neq m])). intro.elim n1. simplify.reflexivity. simplify.apply not_eq_O_S. intro. simplify. -intro. apply not_eq_O_S n1.apply sym_eq.assumption. +intro. apply (not_eq_O_S n1).apply sym_eq.assumption. intros.simplify. generalize in match H. -elim (eqb n1 m1). +elim ((eqb n1 m1)). simplify.apply eq_f.apply H1. simplify.intro.apply H1.apply inj_S.assumption. qed. @@ -55,13 +55,13 @@ theorem eqb_elim : \forall n,m:nat.\forall P:bool \to Prop. (n=m \to (P true)) \to (n \neq m \to (P false)) \to (P (eqb n m)). intros. cut -match (eqb n m) with +(match (eqb n m) with [ true \Rightarrow n = m -| false \Rightarrow n \neq m] \to (P (eqb n m)). +| false \Rightarrow n \neq m] \to (P (eqb n m))). apply Hcut.apply eqb_to_Prop. -elim eqb n m. -apply (H H2). -apply (H1 H2). +elim (eqb n m). +apply ((H H2)). +apply ((H1 H2)). qed. theorem eqb_n_n: \forall n. eqb n n = true. @@ -71,15 +71,15 @@ qed. theorem eq_to_eqb_true: \forall n,m:nat. n = m \to eqb n m = true. -intros.apply eqb_elim n m. +intros.apply (eqb_elim n m). intros. reflexivity. -intros.apply False_ind.apply H1 H. +intros.apply False_ind.apply (H1 H). qed. theorem not_eq_to_eqb_false: \forall n,m:nat. \lnot (n = m) \to eqb n m = false. -intros.apply eqb_elim n m. -intros. apply False_ind.apply H H1. +intros.apply (eqb_elim n m). +intros. apply False_ind.apply (H H1). intros.reflexivity. qed. @@ -96,13 +96,13 @@ match (leb n m) with [ true \Rightarrow n \leq m | false \Rightarrow n \nleq m]. intros. -apply nat_elim2 +apply (nat_elim2 (\lambda n,m:nat.match (leb n m) with [ true \Rightarrow n \leq m -| false \Rightarrow n \nleq m]). +| false \Rightarrow n \nleq m])). simplify.exact le_O_n. simplify.exact not_le_Sn_O. -intros 2.simplify.elim (leb n1 m1). +intros 2.simplify.elim ((leb n1 m1)). simplify.apply le_S_S.apply H. simplify.intros.apply H.apply le_S_S_to_le.assumption. qed. @@ -112,13 +112,13 @@ theorem leb_elim: \forall n,m:nat. \forall P:bool \to Prop. P (leb n m). intros. cut -match (leb n m) with +(match (leb n m) with [ true \Rightarrow n \leq m -| false \Rightarrow n \nleq m] \to (P (leb n m)). +| false \Rightarrow n \nleq m] \to (P (leb n m))). apply Hcut.apply leb_to_Prop. -elim leb n m. -apply (H H2). -apply (H1 H2). +elim (leb n m). +apply ((H H2)). +apply ((H1 H2)). qed. let rec nat_compare n m: compare \def @@ -144,7 +144,7 @@ intros.simplify.reflexivity. qed. theorem S_pred: \forall n:nat.lt O n \to eq nat n (S (pred n)). -intro.elim n.apply False_ind.exact not_le_Sn_O O H. +intro.elim n.apply False_ind.exact (not_le_Sn_O O H). apply eq_f.apply pred_Sn. qed. @@ -152,8 +152,8 @@ theorem nat_compare_pred_pred: \forall n,m:nat.lt O n \to lt O m \to eq compare (nat_compare n m) (nat_compare (pred n) (pred m)). intros. -apply lt_O_n_elim n H. -apply lt_O_n_elim m H1. +apply (lt_O_n_elim n H). +apply (lt_O_n_elim m H1). intros. simplify.reflexivity. qed. @@ -164,14 +164,14 @@ match (nat_compare n m) with | EQ \Rightarrow n=m | GT \Rightarrow m < n ]. intros. -apply nat_elim2 (\lambda n,m.match (nat_compare n m) with +apply (nat_elim2 (\lambda n,m.match (nat_compare n m) with [ LT \Rightarrow n < m | EQ \Rightarrow n=m - | GT \Rightarrow m < n ]). + | GT \Rightarrow m < n ])). intro.elim n1.simplify.reflexivity. simplify.apply le_S_S.apply le_O_n. intro.simplify.apply le_S_S. apply le_O_n. -intros 2.simplify.elim (nat_compare n1 m1). +intros 2.simplify.elim ((nat_compare n1 m1)). simplify. apply le_S_S.apply H. simplify. apply eq_f. apply H. simplify. apply le_S_S.apply H. @@ -180,7 +180,7 @@ qed. theorem nat_compare_n_m_m_n: \forall n,m:nat. nat_compare n m = compare_invert (nat_compare m n). intros. -apply nat_elim2 (\lambda n,m. nat_compare n m = compare_invert (nat_compare m n)). +apply (nat_elim2 (\lambda n,m. nat_compare n m = compare_invert (nat_compare m n))). intros.elim n1.simplify.reflexivity. simplify.reflexivity. intro.elim n1.simplify.reflexivity. @@ -192,14 +192,14 @@ theorem nat_compare_elim : \forall n,m:nat. \forall P:compare \to Prop. (n < m \to P LT) \to (n=m \to P EQ) \to (m < n \to P GT) \to (P (nat_compare n m)). intros. -cut match (nat_compare n m) with +cut (match (nat_compare n m) with [ LT \Rightarrow n < m | EQ \Rightarrow n=m | GT \Rightarrow m < n] \to -(P (nat_compare n m)). +(P (nat_compare n m))). apply Hcut.apply nat_compare_to_Prop. -elim (nat_compare n m). -apply (H H3). -apply (H1 H3). -apply (H2 H3). +elim ((nat_compare n m)). +apply ((H H3)). +apply ((H1 H3)). +apply ((H2 H3)). qed. diff --git a/helm/matita/library/nat/congruence.ma b/helm/matita/library/nat/congruence.ma index 20c73b3d1..7681f191f 100644 --- a/helm/matita/library/nat/congruence.ma +++ b/helm/matita/library/nat/congruence.ma @@ -30,22 +30,22 @@ qed. theorem transitive_congruent: \forall p:nat. transitive nat (\lambda n,m. congruent n m p). intros.unfold transitive.unfold congruent.intros. -whd.apply trans_eq ? ? (y \mod p). +whd.apply (trans_eq ? ? (y \mod p)). apply H.apply H1. qed. theorem le_to_mod: \forall n,m:nat. n \lt m \to n = n \mod m. intros. -apply div_mod_spec_to_eq2 n m O n (n/m) (n \mod m). +apply (div_mod_spec_to_eq2 n m O n (n/m) (n \mod m)). constructor 1.assumption.simplify.reflexivity. apply div_mod_spec_div_mod. -apply le_to_lt_to_lt O n m.apply le_O_n.assumption. +apply (le_to_lt_to_lt O n m).apply le_O_n.assumption. qed. theorem mod_mod : \forall n,p:nat. O

div_mod (n \mod p) p in \vdash (? ? % ?). -rewrite > eq_div_O ? p.reflexivity. +rewrite > (div_mod (n \mod p) p) in \vdash (? ? % ?). +rewrite > (eq_div_O ? p).reflexivity. (* uffa: hint non lo trova lt vs. le*) apply lt_mod_m_m. assumption. @@ -61,14 +61,14 @@ qed. theorem eq_times_plus_to_congruent: \forall n,m,p,r:nat. O< p \to n = r*p+m \to congruent n m p. intros.unfold congruent. -apply div_mod_spec_to_eq2 n p (div n p) (mod n p) (r +(div m p)) (mod m p). +apply (div_mod_spec_to_eq2 n p (div n p) (mod n p) (r +(div m p)) (mod m p)). apply div_mod_spec_div_mod.assumption. constructor 1. apply lt_mod_m_m.assumption. rewrite > sym_times. rewrite > distr_times_plus. rewrite > sym_times. -rewrite > sym_times p. +rewrite > (sym_times p). rewrite > assoc_plus. rewrite < div_mod. assumption.assumption. @@ -77,7 +77,7 @@ qed. theorem divides_to_congruent: \forall n,m,p:nat. O < p \to m \le n \to divides p (n - m) \to congruent n m p. intros.elim H2. -apply eq_times_plus_to_congruent n m p n2. +apply (eq_times_plus_to_congruent n m p n2). assumption. rewrite < sym_plus. apply minus_to_plus.assumption. @@ -87,13 +87,13 @@ qed. theorem congruent_to_divides: \forall n,m,p:nat. O < p \to congruent n m p \to divides p (n - m). intros.unfold congruent in H1. -apply witness ? ? ((n / p)-(m / p)). +apply (witness ? ? ((n / p)-(m / p))). rewrite > sym_times. -rewrite > div_mod n p in \vdash (? ? % ?). -rewrite > div_mod m p in \vdash (? ? % ?). -rewrite < sym_plus (m \mod p). +rewrite > (div_mod n p) in \vdash (? ? % ?). +rewrite > (div_mod m p) in \vdash (? ? % ?). +rewrite < (sym_plus (m \mod p)). rewrite < H1. -rewrite < eq_minus_minus_minus_plus ? (n \mod p). +rewrite < (eq_minus_minus_minus_plus ? (n \mod p)). rewrite < minus_plus_m_m. apply sym_eq. apply times_minus_l. @@ -103,24 +103,24 @@ qed. theorem mod_times: \forall n,m,p:nat. O < p \to mod (n*m) p = mod ((mod n p)*(mod m p)) p. intros. -change with congruent (n*m) ((mod n p)*(mod m p)) p. -apply eq_times_plus_to_congruent ? ? p -((n / p)*p*(m / p) + (n / p)*(m \mod p) + (n \mod p)*(m / p)). +change with (congruent (n*m) ((mod n p)*(mod m p)) p). +apply (eq_times_plus_to_congruent ? ? p +((n / p)*p*(m / p) + (n / p)*(m \mod p) + (n \mod p)*(m / p))). assumption. -apply trans_eq ? ? (((n/p)*p+(n \mod p))*((m/p)*p+(m \mod p))). +apply (trans_eq ? ? (((n/p)*p+(n \mod p))*((m/p)*p+(m \mod p)))). apply eq_f2. apply div_mod.assumption. apply div_mod.assumption. -apply trans_eq ? ? (((n/p)*p)*((m/p)*p) + (n/p)*p*(m \mod p) + -(n \mod p)*((m / p)*p) + (n \mod p)*(m \mod p)). +apply (trans_eq ? ? (((n/p)*p)*((m/p)*p) + (n/p)*p*(m \mod p) + +(n \mod p)*((m / p)*p) + (n \mod p)*(m \mod p))). apply times_plus_plus. apply eq_f2. rewrite < assoc_times. -rewrite > assoc_times (n/p) p (m \mod p). -rewrite > sym_times p (m \mod p). -rewrite < assoc_times (n/p) (m \mod p) p. +rewrite > (assoc_times (n/p) p (m \mod p)). +rewrite > (sym_times p (m \mod p)). +rewrite < (assoc_times (n/p) (m \mod p) p). rewrite < times_plus_l. -rewrite < assoc_times (n \mod p). +rewrite < (assoc_times (n \mod p)). rewrite < times_plus_l. apply eq_f2. apply eq_f2.reflexivity. @@ -132,7 +132,7 @@ theorem congruent_times: \forall n,m,n1,m1,p. O < p \to congruent n n1 p \to congruent m m1 p \to congruent (n*m) (n1*m1) p. unfold congruent. intros. -rewrite > mod_times n m p H. +rewrite > (mod_times n m p H). rewrite > H1. rewrite > H2. apply sym_eq. @@ -142,12 +142,12 @@ qed. theorem congruent_pi: \forall f:nat \to nat. \forall n,m,p:nat.O < p \to congruent (pi n f m) (pi n (\lambda m. mod (f m) p) m) p. intros. -elim n.change with congruent (f m) (f m \mod p) p. +elim n.change with (congruent (f m) (f m \mod p) p). apply congruent_n_mod_n.assumption. -change with congruent ((f (S n1+m))*(pi n1 f m)) -(((f (S n1+m))\mod p)*(pi n1 (\lambda m.(f m) \mod p) m)) p. +change with (congruent ((f (S n1+m))*(pi n1 f m)) +(((f (S n1+m))\mod p)*(pi n1 (\lambda m.(f m) \mod p) m)) p). apply congruent_times. assumption. apply congruent_n_mod_n.assumption. assumption. -qed. \ No newline at end of file +qed. diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma index f79891b48..9995830a9 100644 --- a/helm/matita/library/nat/div_and_mod.ma +++ b/helm/matita/library/nat/div_and_mod.ma @@ -53,23 +53,23 @@ interpretation "natural divide" 'divide x y = theorem le_mod_aux_m_m: \forall p,n,m. n \leq p \to (mod_aux p n m) \leq m. intro.elim p. -apply le_n_O_elim n H (\lambda n.(mod_aux O n m) \leq m). +apply (le_n_O_elim n H (\lambda n.(mod_aux O n m) \leq m)). simplify.apply le_O_n. simplify. -apply leb_elim n1 m. +apply (leb_elim n1 m). simplify.intro.assumption. simplify.intro.apply H. -cut n1 \leq (S n) \to n1-(S m) \leq n. +cut (n1 \leq (S n) \to n1-(S m) \leq n). apply Hcut.assumption. elim n1. simplify.apply le_O_n. -simplify.apply trans_le ? n2 n. +simplify.apply (trans_le ? n2 n). apply le_minus_m.apply le_S_S_to_le.assumption. qed. theorem lt_mod_m_m: \forall n,m. O < m \to (n \mod m) < m. intros 2.elim m.apply False_ind. -apply not_le_Sn_O O H. +apply (not_le_Sn_O O H). simplify.apply le_S_S.apply le_mod_aux_m_m. apply le_n. qed. @@ -77,11 +77,11 @@ qed. theorem div_aux_mod_aux: \forall p,n,m:nat. (n=(div_aux p n m)*(S m) + (mod_aux p n m)). intro.elim p. -simplify.elim leb n m. +simplify.elim (leb n m). simplify.apply refl_eq. simplify.apply refl_eq. simplify. -apply leb_elim n1 m. +apply (leb_elim n1 m). simplify.intro.apply refl_eq. simplify.intro. rewrite > assoc_plus. @@ -89,7 +89,7 @@ elim (H (n1-(S m)) m). change with (n1=(S m)+(n1-(S m))). rewrite < sym_plus. apply plus_minus_m_m. -change with m < n1. +change with (m < n1). apply not_le_to_lt.exact H1. qed. @@ -108,9 +108,9 @@ definition div_mod_spec : nat \to nat \to nat \to nat \to Prop \def *) theorem div_mod_spec_to_not_eq_O: \forall n,m,q,r.(div_mod_spec n m q r) \to m \neq O. -intros 4.simplify.intros.elim H.absurd le (S r) O. +intros 4.simplify.intros.elim H.absurd (le (S r) O). rewrite < H1.assumption. -exact not_le_Sn_O r. +exact (not_le_Sn_O r). qed. theorem div_mod_spec_div_mod: @@ -125,14 +125,14 @@ theorem div_mod_spec_to_eq :\forall a,b,q,r,q1,r1. (div_mod_spec a b q r) \to (div_mod_spec a b q1 r1) \to (eq nat q q1). intros.elim H.elim H1. -apply nat_compare_elim q q1.intro. +apply (nat_compare_elim q q1).intro. apply False_ind. -cut eq nat ((q1-q)*b+r1) r. -cut b \leq (q1-q)*b+r1. -cut b \leq r. -apply lt_to_not_le r b H2 Hcut2. +cut (eq nat ((q1-q)*b+r1) r). +cut (b \leq (q1-q)*b+r1). +cut (b \leq r). +apply (lt_to_not_le r b H2 Hcut2). elim Hcut.assumption. -apply trans_le ? ((q1-q)*b). +apply (trans_le ? ((q1-q)*b)). apply le_times_n. apply le_SO_minus.exact H6. rewrite < sym_plus. @@ -153,12 +153,12 @@ intros.assumption. (* the following case is symmetric *) intro. apply False_ind. -cut eq nat ((q-q1)*b+r) r1. -cut b \leq (q-q1)*b+r. -cut b \leq r1. -apply lt_to_not_le r1 b H4 Hcut2. +cut (eq nat ((q-q1)*b+r) r1). +cut (b \leq (q-q1)*b+r). +cut (b \leq r1). +apply (lt_to_not_le r1 b H4 Hcut2). elim Hcut.assumption. -apply trans_le ? ((q-q1)*b). +apply (trans_le ? ((q-q1)*b)). apply le_times_n. apply le_SO_minus.exact H6. rewrite < sym_plus. @@ -180,9 +180,9 @@ theorem div_mod_spec_to_eq2 :\forall a,b,q,r,q1,r1. (div_mod_spec a b q r) \to (div_mod_spec a b q1 r1) \to (eq nat r r1). intros.elim H.elim H1. -apply inj_plus_r (q*b). +apply (inj_plus_r (q*b)). rewrite < H3. -rewrite > div_mod_spec_to_eq a b q r q1 r1 H H1. +rewrite > (div_mod_spec_to_eq a b q r q1 r1 H H1). assumption. qed. @@ -195,7 +195,7 @@ qed. (* some properties of div and mod *) theorem div_times: \forall n,m:nat. ((S n)*m) / (S n) = m. intros. -apply div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O. +apply (div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O). goal 15. (* ?11 is closed with the following tactics *) apply div_mod_spec_div_mod. simplify.apply le_S_S.apply le_O_n. @@ -204,7 +204,7 @@ qed. theorem div_n_n: \forall n:nat. O < n \to n / n = S O. intros. -apply div_mod_spec_to_eq n n (n / n) (n \mod n) (S O) O. +apply (div_mod_spec_to_eq n n (n / n) (n \mod n) (S O) O). apply div_mod_spec_div_mod.assumption. constructor 1.assumption. rewrite < plus_n_O.simplify.rewrite < plus_n_O.reflexivity. @@ -212,16 +212,16 @@ qed. theorem eq_div_O: \forall n,m. n < m \to n / m = O. intros. -apply div_mod_spec_to_eq n m (n/m) (n \mod m) O n. +apply (div_mod_spec_to_eq n m (n/m) (n \mod m) O n). apply div_mod_spec_div_mod. -apply le_to_lt_to_lt O n m. +apply (le_to_lt_to_lt O n m). apply le_O_n.assumption. constructor 1.assumption.reflexivity. qed. theorem mod_n_n: \forall n:nat. O < n \to n \mod n = O. intros. -apply div_mod_spec_to_eq2 n n (n / n) (n \mod n) (S O) O. +apply (div_mod_spec_to_eq2 n n (n / n) (n \mod n) (S O) O). apply div_mod_spec_div_mod.assumption. constructor 1.assumption. rewrite < plus_n_O.simplify.rewrite < plus_n_O.reflexivity. @@ -230,7 +230,7 @@ qed. theorem mod_S: \forall n,m:nat. O < m \to S (n \mod m) < m \to ((S n) \mod m) = S (n \mod m). intros. -apply div_mod_spec_to_eq2 (S n) m ((S n) / m) ((S n) \mod m) (n / m) (S (n \mod m)). +apply (div_mod_spec_to_eq2 (S n) m ((S n) / m) ((S n) \mod m) (n / m) (S (n \mod m))). apply div_mod_spec_div_mod.assumption. constructor 1.assumption.rewrite < plus_n_Sm. apply eq_f. @@ -245,19 +245,19 @@ qed. theorem lt_to_eq_mod:\forall n,m:nat. n < m \to n \mod m = n. intros. -apply div_mod_spec_to_eq2 n m (n/m) (n \mod m) O n. +apply (div_mod_spec_to_eq2 n m (n/m) (n \mod m) O n). apply div_mod_spec_div_mod. -apply le_to_lt_to_lt O n m.apply le_O_n.assumption. +apply (le_to_lt_to_lt O n m).apply le_O_n.assumption. constructor 1. assumption.reflexivity. qed. (* injectivity *) theorem injective_times_r: \forall n:nat.injective nat nat (\lambda m:nat.(S n)*m). -change with \forall n,p,q:nat.(S n)*p = (S n)*q \to p=q. +change with (\forall n,p,q:nat.(S n)*p = (S n)*q \to p=q). intros. -rewrite < div_times n. -rewrite < div_times n q. +rewrite < (div_times n). +rewrite < (div_times n q). apply eq_f2.assumption. reflexivity. qed. @@ -266,21 +266,21 @@ variant inj_times_r : \forall n,p,q:nat.(S n)*p = (S n)*q \to p=q \def injective_times_r. theorem lt_O_to_injective_times_r: \forall n:nat. O < n \to injective nat nat (\lambda m:nat.n*m). -change with \forall n. O < n \to \forall p,q:nat.n*p = n*q \to p=q. +change with (\forall n. O < n \to \forall p,q:nat.n*p = n*q \to p=q). intros 4. -apply lt_O_n_elim n H.intros. -apply inj_times_r m.assumption. +apply (lt_O_n_elim n H).intros. +apply (inj_times_r m).assumption. qed. variant inj_times_r1:\forall n. O < n \to \forall p,q:nat.n*p = n*q \to p=q \def lt_O_to_injective_times_r. theorem injective_times_l: \forall n:nat.injective nat nat (\lambda m:nat.m*(S n)). -change with \forall n,p,q:nat.p*(S n) = q*(S n) \to p=q. +change with (\forall n,p,q:nat.p*(S n) = q*(S n) \to p=q). intros. -apply inj_times_r n p q. +apply (inj_times_r n p q). rewrite < sym_times. -rewrite < sym_times q. +rewrite < (sym_times q). assumption. qed. @@ -288,10 +288,10 @@ variant inj_times_l : \forall n,p,q:nat. p*(S n) = q*(S n) \to p=q \def injective_times_l. theorem lt_O_to_injective_times_l: \forall n:nat. O < n \to injective nat nat (\lambda m:nat.m*n). -change with \forall n. O < n \to \forall p,q:nat.p*n = q*n \to p=q. +change with (\forall n. O < n \to \forall p,q:nat.p*n = q*n \to p=q). intros 4. -apply lt_O_n_elim n H.intros. -apply inj_times_l m.assumption. +apply (lt_O_n_elim n H).intros. +apply (inj_times_l m).assumption. qed. variant inj_times_l1:\forall n. O < n \to \forall p,q:nat.p*n = q*n \to p=q diff --git a/helm/matita/library/nat/exp.ma b/helm/matita/library/nat/exp.ma index 19c09e27c..49e3bbd70 100644 --- a/helm/matita/library/nat/exp.ma +++ b/helm/matita/library/nat/exp.ma @@ -56,7 +56,7 @@ qed. 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)). +apply (trans_le ? ((S(S O))*(S n1))). simplify. rewrite < plus_n_Sm.apply le_S_S.apply le_S_S. rewrite < sym_plus. @@ -67,7 +67,7 @@ qed. theorem exp_to_eq_O: \forall n,m:nat. (S O) < n \to n \sup m = (S O) \to m = O. intros.apply antisym_le.apply le_S_S_to_le. -rewrite < H1.change with m < n \sup m. +rewrite < H1.change with (m < n \sup m). apply lt_m_exp_nm.assumption. apply le_O_n. qed. @@ -75,21 +75,21 @@ qed. theorem injective_exp_r: \forall n:nat. (S O) < n \to injective nat nat (\lambda m:nat. n \sup m). simplify.intros 4. -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. +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. +intros.apply (exp_to_eq_O n).assumption.assumption. intros.apply eq_f. apply H1. (* esprimere inj_times senza S *) -cut \forall a,b:nat.O < n \to n*a=n*b \to a=b. +cut (\forall a,b:nat.O < n \to n*a=n*b \to a=b). apply Hcut.simplify. apply le_S_S_to_le. apply le_S. assumption. assumption. intros 2. -apply nat_case n. -intros.apply False_ind.apply not_le_Sn_O O H3. +apply (nat_case n). +intros.apply False_ind.apply (not_le_Sn_O O H3). intros. -apply inj_times_r m1.assumption. +apply (inj_times_r m1).assumption. qed. variant inj_exp_r: \forall p:nat. (S O) < p \to \forall n,m:nat. diff --git a/helm/matita/library/nat/factorial.ma b/helm/matita/library/nat/factorial.ma index d792574e3..22a799d07 100644 --- a/helm/matita/library/nat/factorial.ma +++ b/helm/matita/library/nat/factorial.ma @@ -25,32 +25,32 @@ 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)*n1!. -apply trans_le ? ((S n1)*(S O)).simplify. +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 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)*m!. -apply trans_le ? ((S(S O))*(S O)).apply 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)*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 n!. intro. elim n.apply le_O_n. -change with S n1 \le (S n1)*n1!. -apply trans_le ? ((S n1)*(S O)). +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 < 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)*m!. -apply lt_to_le_to_lt ? ((S m)*(S (S O))). +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)*m!). +apply (lt_to_le_to_lt ? ((S m)*(S (S O)))). rewrite < sym_times. simplify. apply le_S_S.rewrite < plus_n_O. diff --git a/helm/matita/library/nat/factorization.ma b/helm/matita/library/nat/factorization.ma index fc51b32ff..b64e3733b 100644 --- a/helm/matita/library/nat/factorization.ma +++ b/helm/matita/library/nat/factorization.ma @@ -28,22 +28,22 @@ theorem divides_max_prime_factor_n: \forall n:nat. (S O) < n \to nth_prime (max_prime_factor n) \divides n. intros.apply divides_b_true_to_divides. apply lt_O_nth_prime_n. -apply f_max_true (\lambda p:nat.eqb (n \mod (nth_prime p)) O) n. -cut \exists i. nth_prime i = smallest_factor n. +apply (f_max_true (\lambda p:nat.eqb (n \mod (nth_prime p)) O) n). +cut (\exists i. nth_prime i = smallest_factor n). elim Hcut. -apply ex_intro nat ? a. +apply (ex_intro nat ? a). split. -apply trans_le a (nth_prime a). +apply (trans_le a (nth_prime a)). apply le_n_fn. exact lt_nth_prime_n_nth_prime_Sn. rewrite > H1. apply le_smallest_factor_n. rewrite > H1. -change with divides_b (smallest_factor n) n = true. +change with (divides_b (smallest_factor n) n = true). apply divides_to_divides_b_true. -apply trans_lt ? (S O).simplify. apply le_n. +apply (trans_lt ? (S O)).simplify. apply le_n. apply lt_SO_smallest_factor.assumption. apply divides_smallest_factor_n. -apply trans_lt ? (S O). simplify. apply le_n. assumption. +apply (trans_lt ? (S O)). simplify. apply le_n. assumption. apply prime_to_nth_prime. apply prime_smallest_factor_n.assumption. qed. @@ -51,17 +51,17 @@ qed. theorem divides_to_max_prime_factor : \forall n,m. (S O) < n \to O < m \to n \divides m \to max_prime_factor n \le max_prime_factor m. intros.change with -(max n (\lambda p:nat.eqb (n \mod (nth_prime p)) O)) \le -(max m (\lambda p:nat.eqb (m \mod (nth_prime p)) O)). +((max n (\lambda p:nat.eqb (n \mod (nth_prime p)) O)) \le +(max m (\lambda p:nat.eqb (m \mod (nth_prime p)) O))). apply f_m_to_le_max. -apply trans_le ? n. +apply (trans_le ? n). apply le_max_n.apply divides_to_le.assumption.assumption. -change with divides_b (nth_prime (max_prime_factor n)) m = true. +change with (divides_b (nth_prime (max_prime_factor n)) m = true). apply divides_to_divides_b_true. -cut prime (nth_prime (max_prime_factor n)). +cut (prime (nth_prime (max_prime_factor n))). apply lt_O_nth_prime_n.apply prime_nth_prime. -cut nth_prime (max_prime_factor n) \divides n. -apply transitive_divides ? n. +cut (nth_prime (max_prime_factor n) \divides n). +apply (transitive_divides ? n). apply divides_max_prime_factor_n. assumption.assumption. apply divides_b_true_to_divides. @@ -78,28 +78,28 @@ p = max_prime_factor n \to (S O) < r \to max_prime_factor r < p. intros. rewrite > H1. -cut max_prime_factor r \lt max_prime_factor n \lor - max_prime_factor r = max_prime_factor n. +cut (max_prime_factor r \lt max_prime_factor n \lor + max_prime_factor r = max_prime_factor n). elim Hcut.assumption. -absurd nth_prime (max_prime_factor n) \divides r. +absurd (nth_prime (max_prime_factor n) \divides r). rewrite < H4. apply divides_max_prime_factor_n. assumption. -change with nth_prime (max_prime_factor n) \divides r \to False. +change with (nth_prime (max_prime_factor n) \divides r \to False). intro. -cut r \mod (nth_prime (max_prime_factor n)) \neq O. +cut (r \mod (nth_prime (max_prime_factor n)) \neq O). apply Hcut1.apply divides_to_mod_O. apply lt_O_nth_prime_n.assumption. -apply p_ord_aux_to_not_mod_O n n ? q r. +apply (p_ord_aux_to_not_mod_O n n ? q r). apply lt_SO_nth_prime_n.assumption. apply le_n. rewrite < H1.assumption. -apply le_to_or_lt_eq (max_prime_factor r) (max_prime_factor n). +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 ((nth_prime p) \sup q). +apply (witness r n ((nth_prime p) \sup q)). rewrite < sym_times. -apply p_ord_aux_to_exp n n ? q r. +apply (p_ord_aux_to_exp n n ? q r). apply lt_O_nth_prime_n.assumption. qed. @@ -108,17 +108,17 @@ max_prime_factor n \le p \to (pair nat nat q r) = p_ord n (nth_prime p) \to (S O) < r \to max_prime_factor r < p. 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). +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 ((nth_prime p) \sup q). +apply (witness r n ((nth_prime p) \sup q)). rewrite > sym_times. -apply p_ord_aux_to_exp n n. +apply (p_ord_aux_to_exp n n). apply lt_O_nth_prime_n. assumption.assumption. -apply p_ord_to_lt_max_prime_factor n ? q. +apply (p_ord_to_lt_max_prime_factor n ? q). assumption.apply sym_eq.assumption.assumption.assumption. -apply le_to_or_lt_eq ? p H1. +apply (le_to_or_lt_eq ? p H1). qed. (* datatypes and functions *) @@ -170,18 +170,18 @@ O < defactorize_aux f i. intro.elim f.simplify. rewrite > times_n_SO. apply le_times. -change with O < nth_prime i. +change with (O < nth_prime i). apply lt_O_nth_prime_n. -change with O < exp (nth_prime i) n. +change with (O < exp (nth_prime i) n). apply lt_O_exp. apply lt_O_nth_prime_n. simplify. rewrite > times_n_SO. apply le_times. -change with O < exp (nth_prime i) n. +change with (O < exp (nth_prime i) n). apply lt_O_exp. apply lt_O_nth_prime_n. -change with O < defactorize_aux n1 (S i). +change with (O < defactorize_aux n1 (S i)). apply H. qed. @@ -190,19 +190,19 @@ S O < defactorize_aux f i. intro.elim f.simplify. rewrite > times_n_SO. apply le_times. -change with S O < nth_prime i. +change with (S O < nth_prime i). apply lt_SO_nth_prime_n. -change with O < exp (nth_prime i) n. +change with (O < exp (nth_prime i) n). apply lt_O_exp. apply lt_O_nth_prime_n. simplify. rewrite > times_n_SO. rewrite > sym_times. apply le_times. -change with O < exp (nth_prime i) n. +change with (O < exp (nth_prime i) n). apply lt_O_exp. apply lt_O_nth_prime_n. -change with S O < defactorize_aux n1 (S i). +change with (S O < defactorize_aux n1 (S i)). apply H. qed. @@ -213,150 +213,150 @@ defactorize_aux (factorize_aux p n acc) O = n*(defactorize_aux acc p). intro.elim p.simplify. elim H1.elim H2.rewrite > H3. rewrite > sym_times. apply times_n_SO. -apply False_ind.apply not_le_Sn_O (max_prime_factor n) H2. +apply False_ind.apply (not_le_Sn_O (max_prime_factor n) H2). simplify. (* generalizing the goal: I guess there exists a better way *) -cut \forall q,r.(pair nat nat q r) = (p_ord_aux n1 n1 (nth_prime n)) \to +cut (\forall q,r.(pair nat nat q r) = (p_ord_aux n1 n1 (nth_prime n)) \to defactorize_aux match (p_ord_aux n1 n1 (nth_prime n)) with [(pair q r) \Rightarrow (factorize_aux n r (nf_cons q acc))] O = -n1*defactorize_aux acc (S n). -apply Hcut (fst ? ? (p_ord_aux n1 n1 (nth_prime n))) -(snd ? ? (p_ord_aux n1 n1 (nth_prime n))). +n1*defactorize_aux acc (S n)). +apply (Hcut (fst ? ? (p_ord_aux n1 n1 (nth_prime n))) +(snd ? ? (p_ord_aux n1 n1 (nth_prime n)))). apply sym_eq.apply eq_pair_fst_snd. intros. rewrite < H3. simplify. -cut n1 = r * (nth_prime n) \sup q. +cut (n1 = r * (nth_prime n) \sup q). rewrite > H. simplify.rewrite < assoc_times. rewrite < Hcut.reflexivity. -cut O < r \lor O = r. -elim Hcut1.assumption.absurd n1 = O. +cut (O < r \lor O = r). +elim Hcut1.assumption.absurd (n1 = O). rewrite > Hcut.rewrite < H4.reflexivity. -simplify. intro.apply not_le_Sn_O O. +simplify. intro.apply (not_le_Sn_O O). rewrite < H5 in \vdash (? ? %).assumption. apply le_to_or_lt_eq.apply le_O_n. -cut (S O) < r \lor (S O) \nlt r. +cut ((S O) < r \lor (S O) \nlt r). elim Hcut1. right. -apply p_ord_to_lt_max_prime_factor1 n1 ? q r. +apply (p_ord_to_lt_max_prime_factor1 n1 ? q r). assumption.elim H2. elim H5. apply False_ind. -apply not_eq_O_S n.apply sym_eq.assumption. +apply (not_eq_O_S n).apply sym_eq.assumption. apply le_S_S_to_le. exact H5. assumption.assumption. -cut r=(S O). -apply nat_case n. +cut (r=(S O)). +apply (nat_case n). left.split.assumption.reflexivity. intro.right.rewrite > Hcut2. simplify.apply le_S_S.apply le_O_n. -cut r \lt (S O) \or r=(S O). -elim Hcut2.absurd O=r. +cut (r \lt (S O) \or r=(S O)). +elim Hcut2.absurd (O=r). apply le_n_O_to_eq.apply le_S_S_to_le.exact H5. simplify.intro. -cut O=n1. -apply not_le_Sn_O O. +cut (O=n1). +apply (not_le_Sn_O O). rewrite > Hcut3 in \vdash (? ? %). assumption.rewrite > Hcut. rewrite < H6.reflexivity. assumption. -apply le_to_or_lt_eq r (S O). +apply (le_to_or_lt_eq r (S O)). apply not_lt_to_le.assumption. -apply decidable_lt (S O) r. +apply (decidable_lt (S O) r). rewrite > sym_times. -apply p_ord_aux_to_exp n1 n1. +apply (p_ord_aux_to_exp n1 n1). apply lt_O_nth_prime_n.assumption. qed. theorem defactorize_factorize: \forall n:nat.defactorize (factorize n) = n. intro. -apply nat_case n.reflexivity. -intro.apply nat_case m.reflexivity. +apply (nat_case n).reflexivity. +intro.apply (nat_case m).reflexivity. intro.change with -let p \def (max (S(S m1)) (\lambda p:nat.eqb ((S(S m1)) \mod (nth_prime p)) O)) in +(let p \def (max (S(S m1)) (\lambda p:nat.eqb ((S(S m1)) \mod (nth_prime p)) O)) in defactorize (match p_ord (S(S m1)) (nth_prime p) with [ (pair q r) \Rightarrow - nfa_proper (factorize_aux p r (nf_last (pred q)))])=(S(S m1)). + nfa_proper (factorize_aux p r (nf_last (pred q)))])=(S(S m1))). intro. (* generalizing the goal; find a better way *) -cut \forall q,r.(pair nat nat q r) = (p_ord (S(S m1)) (nth_prime p)) \to +cut (\forall q,r.(pair nat nat q r) = (p_ord (S(S m1)) (nth_prime p)) \to defactorize (match p_ord (S(S m1)) (nth_prime p) with [ (pair q r) \Rightarrow - nfa_proper (factorize_aux p r (nf_last (pred q)))])=(S(S m1)). -apply Hcut (fst ? ? (p_ord (S(S m1)) (nth_prime p))) -(snd ? ? (p_ord (S(S m1)) (nth_prime p))). + nfa_proper (factorize_aux p r (nf_last (pred q)))])=(S(S m1))). +apply (Hcut (fst ? ? (p_ord (S(S m1)) (nth_prime p))) +(snd ? ? (p_ord (S(S m1)) (nth_prime p)))). apply sym_eq.apply eq_pair_fst_snd. intros. rewrite < H. change with -defactorize_aux (factorize_aux p r (nf_last (pred q))) O = (S(S m1)). -cut (S(S m1)) = (nth_prime p) \sup q *r. -cut O defactorize_aux_factorize_aux. -change with r*(nth_prime p) \sup (S (pred q)) = (S(S m1)). -cut (S (pred q)) = q. +change with (r*(nth_prime p) \sup (S (pred q)) = (S(S m1))). +cut ((S (pred q)) = q). rewrite > Hcut2. rewrite > sym_times. apply sym_eq. -apply p_ord_aux_to_exp (S(S m1)). +apply (p_ord_aux_to_exp (S(S m1))). apply lt_O_nth_prime_n. assumption. (* O < q *) apply sym_eq. apply S_pred. -cut O < q \lor O = q. +cut (O < q \lor O = q). elim Hcut2.assumption. -absurd nth_prime p \divides S (S m1). -apply divides_max_prime_factor_n (S (S m1)). +absurd (nth_prime p \divides S (S m1)). +apply (divides_max_prime_factor_n (S (S m1))). simplify.apply le_S_S.apply le_S_S. apply le_O_n. -cut (S(S m1)) = r. +cut ((S(S m1)) = r). rewrite > Hcut3 in \vdash (? (? ? %)). -change with nth_prime p \divides r \to False. +change with (nth_prime p \divides r \to False). intro. -apply p_ord_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r. +apply (p_ord_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r). apply lt_SO_nth_prime_n. simplify.apply le_S_S.apply le_O_n.apply le_n. assumption. apply divides_to_mod_O.apply lt_O_nth_prime_n.assumption. rewrite > times_n_SO in \vdash (? ? ? %). rewrite < sym_times. -rewrite > exp_n_O (nth_prime p). +rewrite > (exp_n_O (nth_prime p)). rewrite > H1 in \vdash (? ? ? (? (? ? %) ?)). assumption. apply le_to_or_lt_eq.apply le_O_n.assumption. (* e adesso l'ultimo goal. TASSI: che ora non e' piu' l'ultimo :P *) -cut (S O) < r \lor S O \nlt r. +cut ((S O) < r \lor S O \nlt r). elim Hcut2. right. -apply p_ord_to_lt_max_prime_factor1 (S(S m1)) ? q r. +apply (p_ord_to_lt_max_prime_factor1 (S(S m1)) ? q r). simplify.apply le_S_S. apply le_O_n. apply le_n. assumption.assumption. -cut r=(S O). -apply nat_case p. +cut (r=(S O)). +apply (nat_case p). left.split.assumption.reflexivity. intro.right.rewrite > Hcut3. simplify.apply le_S_S.apply le_O_n. -cut r \lt (S O) \or r=(S O). -elim Hcut3.absurd O=r. +cut (r \lt (S O) \or r=(S O)). +elim Hcut3.absurd (O=r). apply le_n_O_to_eq.apply le_S_S_to_le.exact H2. simplify.intro. -apply not_le_Sn_O O. +apply (not_le_Sn_O O). rewrite > H3 in \vdash (? ? %).assumption.assumption. -apply le_to_or_lt_eq r (S O). +apply (le_to_or_lt_eq r (S O)). apply not_lt_to_le.assumption. -apply decidable_lt (S O) r. +apply (decidable_lt (S O) r). (* O < r *) -cut O < r \lor O = r. +cut (O < r \lor O = r). elim Hcut1.assumption. apply False_ind. -apply not_eq_O_S (S m1). +apply (not_eq_O_S (S m1)). rewrite > Hcut.rewrite < H1.rewrite < times_n_O.reflexivity. apply le_to_or_lt_eq.apply le_O_n. (* prova del cut *) goal 20. -apply p_ord_aux_to_exp (S(S m1)). +apply (p_ord_aux_to_exp (S(S m1))). apply lt_O_nth_prime_n. assumption. (* fine prova cut *) @@ -375,17 +375,17 @@ match f with theorem divides_max_p_defactorize: \forall f:nat_fact.\forall i:nat. nth_prime ((max_p f)+i) \divides defactorize_aux f i. intro. -elim f.simplify.apply witness ? ? ((nth_prime i) \sup n). +elim f.simplify.apply (witness ? ? ((nth_prime i) \sup n)). reflexivity. change with -nth_prime (S(max_p n1)+i) \divides -(nth_prime i) \sup n *(defactorize_aux n1 (S i)). -elim H (S i). +(nth_prime (S(max_p n1)+i) \divides +(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* (nth_prime i) \sup n). +apply (witness ? ? (n2* (nth_prime i) \sup n)). reflexivity. qed. @@ -393,9 +393,9 @@ theorem divides_exp_to_divides: \forall p,n,m:nat. prime p \to p \divides n \sup m \to p \divides n. intros 3.elim m.simplify in H1. -apply transitive_divides p (S O).assumption. +apply (transitive_divides p (S O)).assumption. apply divides_SO_n. -cut p \divides n \lor p \divides n \sup n1. +cut (p \divides n \lor p \divides n \sup n1). elim Hcut.assumption. apply H.assumption.assumption. apply divides_times_to_divides.assumption. @@ -408,7 +408,7 @@ p \divides q \sup m \to p = q. intros. simplify in H1. elim H1.apply H4. -apply divides_exp_to_divides p q m. +apply (divides_exp_to_divides p q m). assumption.assumption. simplify in H.elim H.assumption. qed. @@ -417,32 +417,32 @@ theorem not_divides_defactorize_aux: \forall f:nat_fact. \forall i,j:nat. i < j \to nth_prime i \ndivides defactorize_aux f j. intro.elim f. change with -nth_prime i \divides (nth_prime j) \sup (S n) \to False. -intro.absurd (nth_prime i) = (nth_prime j). -apply divides_exp_to_eq ? ? (S n). +(nth_prime i \divides (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. assumption. -change with (nth_prime i) = (nth_prime j) \to False. -intro.cut i = j. -apply not_le_Sn_n i.rewrite > Hcut in \vdash (? ? %).assumption. -apply injective_nth_prime ? ? H2. +change with ((nth_prime i) = (nth_prime j) \to False). +intro.cut (i = j). +apply (not_le_Sn_n i).rewrite > Hcut in \vdash (? ? %).assumption. +apply (injective_nth_prime ? ? H2). change with -nth_prime i \divides (nth_prime j) \sup n *(defactorize_aux n1 (S j)) \to False. +(nth_prime i \divides (nth_prime j) \sup n *(defactorize_aux n1 (S j)) \to False). intro. -cut nth_prime i \divides (nth_prime j) \sup n -\lor nth_prime i \divides defactorize_aux n1 (S j). +cut (nth_prime i \divides (nth_prime j) \sup n +\lor nth_prime i \divides defactorize_aux n1 (S j)). elim Hcut. -absurd (nth_prime i) = (nth_prime j). -apply divides_exp_to_eq ? ? n. +absurd ((nth_prime i) = (nth_prime j)). +apply (divides_exp_to_eq ? ? n). apply prime_nth_prime.apply prime_nth_prime. assumption. -change with (nth_prime i) = (nth_prime j) \to False. +change with ((nth_prime i) = (nth_prime j) \to False). intro. -cut i = j. -apply not_le_Sn_n i.rewrite > Hcut1 in \vdash (? ? %).assumption. -apply injective_nth_prime ? ? H4. -apply H i (S j). -apply trans_lt ? j.assumption.simplify.apply le_n. +cut (i = j). +apply (not_le_Sn_n i).rewrite > Hcut1 in \vdash (? ? %).assumption. +apply (injective_nth_prime ? ? H4). +apply (H i (S j)). +apply (trans_lt ? j).assumption.simplify.apply le_n. assumption. apply divides_times_to_divides. apply prime_nth_prime.assumption. @@ -452,21 +452,21 @@ lemma not_eq_nf_last_nf_cons: \forall g:nat_fact.\forall n,m,i:nat. \lnot (defactorize_aux (nf_last n) i= defactorize_aux (nf_cons m g) i). intros. change with -exp (nth_prime i) (S n) = defactorize_aux (nf_cons m g) i \to False. +(exp (nth_prime i) (S n) = defactorize_aux (nf_cons m g) i \to False). intro. -cut S(max_p g)+i= i. -apply not_le_Sn_n i. +cut (S(max_p g)+i= i). +apply (not_le_Sn_n i). rewrite < Hcut in \vdash (? ? %). simplify.apply le_S_S. apply le_plus_n. apply injective_nth_prime. (* uffa, perche' semplifica ? *) -change with nth_prime (S(max_p g)+i)= nth_prime i. -apply divides_exp_to_eq ? ? (S n). +change with (nth_prime (S(max_p g)+i)= nth_prime i). +apply (divides_exp_to_eq ? ? (S n)). apply prime_nth_prime.apply prime_nth_prime. rewrite > H. -change with divides (nth_prime ((max_p (nf_cons m g))+i)) -(defactorize_aux (nf_cons m g) i). +change with (divides (nth_prime ((max_p (nf_cons m g))+i)) +(defactorize_aux (nf_cons m g) i)). apply divides_max_p_defactorize. qed. @@ -475,11 +475,11 @@ lemma not_eq_nf_cons_O_nf_cons: \forall f,g:nat_fact.\forall n,i:nat. intros. simplify.rewrite < plus_n_O. intro. -apply not_divides_defactorize_aux f i (S i) ?. +apply (not_divides_defactorize_aux f i (S i) ?). simplify.apply le_n. rewrite > H. rewrite > assoc_times. -apply witness ? ? ((exp (nth_prime i) n)*(defactorize_aux g (S i))). +apply (witness ? ? ((exp (nth_prime i) n)*(defactorize_aux g (S i)))). reflexivity. qed. @@ -490,67 +490,67 @@ elim f. generalize in match H. elim g. apply eq_f. -apply inj_S. apply inj_exp_r (nth_prime i). +apply inj_S. apply (inj_exp_r (nth_prime i)). apply lt_SO_nth_prime_n. assumption. apply False_ind. -apply not_eq_nf_last_nf_cons n2 n n1 i H2. +apply (not_eq_nf_last_nf_cons n2 n n1 i H2). generalize in match H1. elim g. apply False_ind. -apply not_eq_nf_last_nf_cons n1 n2 n i. +apply (not_eq_nf_last_nf_cons n1 n2 n i). apply sym_eq. assumption. simplify in H3. generalize in match H3. -apply nat_elim2 (\lambda n,n2. +apply (nat_elim2 (\lambda n,n2. ((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). +nf_cons n n1 = nf_cons n2 n3)). intro. elim n4. apply eq_f. -apply H n3 (S i). +apply (H n3 (S i)). simplify in H4. rewrite > plus_n_O. -rewrite > plus_n_O (defactorize_aux n3 (S i)).assumption. +rewrite > (plus_n_O (defactorize_aux n3 (S i))).assumption. apply False_ind. -apply not_eq_nf_cons_O_nf_cons n1 n3 n5 i.assumption. +apply (not_eq_nf_cons_O_nf_cons n1 n3 n5 i).assumption. intros. apply False_ind. -apply not_eq_nf_cons_O_nf_cons n3 n1 n4 i. +apply (not_eq_nf_cons_O_nf_cons n3 n1 n4 i). apply sym_eq.assumption. intros. -cut nf_cons n4 n1 = nf_cons m n3. -cut n4=m. -cut n1=n3. +cut (nf_cons n4 n1 = nf_cons m n3). +cut (n4=m). +cut (n1=n3). rewrite > Hcut1.rewrite > Hcut2.reflexivity. change with -match nf_cons n4 n1 with +(match nf_cons n4 n1 with [ (nf_last m) \Rightarrow n1 -| (nf_cons m g) \Rightarrow g ] = n3. +| (nf_cons m g) \Rightarrow g ] = n3). rewrite > Hcut.simplify.reflexivity. change with -match nf_cons n4 n1 with +(match nf_cons n4 n1 with [ (nf_last m) \Rightarrow m -| (nf_cons m g) \Rightarrow m ] = m. +| (nf_cons m g) \Rightarrow m ] = m). rewrite > Hcut.simplify.reflexivity. apply H4.simplify in H5. -apply inj_times_r1 (nth_prime i). +apply (inj_times_r1 (nth_prime i)). apply lt_O_nth_prime_n. rewrite < assoc_times.rewrite < assoc_times.assumption. qed. theorem injective_defactorize_aux: \forall i:nat. injective nat_fact nat (\lambda f.defactorize_aux f i). -change with \forall i:nat.\forall f,g:nat_fact. -defactorize_aux f i = defactorize_aux g i \to f = g. +change with (\forall i:nat.\forall f,g:nat_fact. +defactorize_aux f i = defactorize_aux g i \to f = g). intros. -apply eq_defactorize_aux_to_eq f g i H. +apply (eq_defactorize_aux_to_eq f g i H). qed. theorem injective_defactorize: injective nat_fact_all nat defactorize. -change with \forall f,g:nat_fact_all. -defactorize f = defactorize g \to f = g. +change with (\forall f,g:nat_fact_all. +defactorize f = defactorize g \to f = g). intro.elim f. generalize in match H.elim g. (* zero - zero *) @@ -558,47 +558,47 @@ reflexivity. (* zero - one *) simplify in H1. apply False_ind. -apply not_eq_O_S O H1. +apply (not_eq_O_S O H1). (* zero - proper *) simplify in H1. apply False_ind. -apply not_le_Sn_n O. +apply (not_le_Sn_n O). rewrite > H1 in \vdash (? ? %). -change with O < defactorize_aux n O. +change with (O < defactorize_aux n O). apply lt_O_defactorize_aux. generalize in match H. elim g. (* one - zero *) simplify in H1. apply False_ind. -apply not_eq_O_S O.apply sym_eq. assumption. +apply (not_eq_O_S O).apply sym_eq. assumption. (* one - one *) reflexivity. (* one - proper *) simplify in H1. apply False_ind. -apply not_le_Sn_n (S O). +apply (not_le_Sn_n (S O)). rewrite > H1 in \vdash (? ? %). -change with (S O) < defactorize_aux n O. +change with ((S O) < defactorize_aux n O). apply lt_SO_defactorize_aux. generalize in match H.elim g. (* proper - zero *) simplify in H1. apply False_ind. -apply not_le_Sn_n O. +apply (not_le_Sn_n O). rewrite < H1 in \vdash (? ? %). -change with O < defactorize_aux n O. +change with (O < defactorize_aux n O). apply lt_O_defactorize_aux. (* proper - one *) simplify in H1. apply False_ind. -apply not_le_Sn_n (S O). +apply (not_le_Sn_n (S O)). rewrite < H1 in \vdash (? ? %). -change with (S O) < defactorize_aux n O. +change with ((S O) < defactorize_aux n O). apply lt_SO_defactorize_aux. (* proper - proper *) apply eq_f. -apply injective_defactorize_aux O. +apply (injective_defactorize_aux O). exact H1. qed. @@ -607,7 +607,7 @@ theorem factorize_defactorize: intros. apply injective_defactorize. (* uffa: perche' semplifica ??? *) -change with defactorize(factorize (defactorize f)) = (defactorize f). +change with (defactorize(factorize (defactorize f)) = (defactorize f)). apply defactorize_factorize. qed. diff --git a/helm/matita/library/nat/fermat_little_theorem.ma b/helm/matita/library/nat/fermat_little_theorem.ma index b8ccac291..bbd5e359a 100644 --- a/helm/matita/library/nat/fermat_little_theorem.ma +++ b/helm/matita/library/nat/fermat_little_theorem.ma @@ -23,15 +23,15 @@ theorem permut_S_mod: \forall n:nat. permut (S_mod (S n)) n. intro.unfold permut.split.intros. unfold S_mod. apply le_S_S_to_le. -change with (S i) \mod (S n) < S n. +change with ((S i) \mod (S n) < S n). apply lt_mod_m_m. simplify.apply le_S_S.apply le_O_n. unfold injn.intros. apply inj_S. -rewrite < lt_to_eq_mod i (S n). -rewrite < lt_to_eq_mod j (S n). -cut i < n \lor i = n. -cut j < n \lor j = n. +rewrite < (lt_to_eq_mod i (S n)). +rewrite < (lt_to_eq_mod j (S n)). +cut (i < n \lor i = n). +cut (j < n \lor j = n). elim Hcut. elim Hcut1. (* i < n, j< n *) @@ -49,9 +49,9 @@ simplify.apply le_S_S.assumption. unfold S_mod in H2. simplify. apply False_ind. -apply not_eq_O_S (i \mod (S n)). +apply (not_eq_O_S (i \mod (S n))). apply sym_eq. -rewrite < mod_n_n (S n). +rewrite < (mod_n_n (S n)). rewrite < H4 in \vdash (? ? ? (? %?)). rewrite < mod_S.assumption. simplify.apply le_S_S.apply le_O_n. @@ -62,8 +62,8 @@ simplify.apply le_S_S.apply le_O_n. (* i = n, j < n *) elim Hcut1. apply False_ind. -apply not_eq_O_S (j \mod (S n)). -rewrite < mod_n_n (S n). +apply (not_eq_O_S (j \mod (S n))). +rewrite < (mod_n_n (S n)). rewrite < H3 in \vdash (? ? (? %?) ?). rewrite < mod_S.assumption. simplify.apply le_S_S.apply le_O_n. @@ -88,7 +88,7 @@ simplify.reflexivity. change with (S n1)*n1!=(S_mod m n1)*(pi n1 (S_mod m)). unfold S_mod in \vdash (? ? ? (? % ?)). rewrite > lt_to_eq_mod. -apply eq_f.apply H.apply trans_lt ? (S n1). +apply eq_f.apply H.apply (trans_lt ? (S n1)). simplify. apply le_n.assumption.assumption. qed. *) @@ -96,18 +96,18 @@ qed. theorem prime_to_not_divides_fact: \forall p:nat. prime p \to \forall n:nat. n \lt p \to \not divides p n!. intros 3.elim n.simplify.intros. -apply lt_to_not_le (S O) p. +apply (lt_to_not_le (S O) p). unfold prime in H.elim H. assumption.apply divides_to_le.simplify.apply le_n. assumption. -change with (divides p ((S n1)*n1!)) \to False. +change with (divides p ((S n1)*n1!) \to False). intro. -cut divides p (S n1) \lor divides p n1!. -elim Hcut.apply lt_to_not_le (S n1) p. +cut (divides p (S n1) \lor divides p n1!). +elim Hcut.apply (lt_to_not_le (S n1) p). assumption. apply divides_to_le.simplify.apply le_S_S.apply le_O_n. assumption.apply H1. -apply trans_lt ? (S n1).simplify. apply le_n. +apply (trans_lt ? (S n1)).simplify. apply le_n. assumption.assumption. apply divides_times_to_divides. assumption.assumption. @@ -117,108 +117,108 @@ theorem permut_mod: \forall p,a:nat. prime p \to \lnot divides p a\to permut (\lambda n.(mod (a*n) p)) (pred p). unfold permut.intros. split.intros.apply le_S_S_to_le. -apply trans_le ? p. -change with mod (a*i) p < p. +apply (trans_le ? p). +change with (mod (a*i) p < p). apply lt_mod_m_m. simplify in H.elim H. -simplify.apply trans_le ? (S (S O)). +simplify.apply (trans_le ? (S (S O))). apply le_n_Sn.assumption. rewrite < S_pred.apply le_n. unfold prime in H. elim H. -apply trans_lt ? (S O).simplify.apply le_n.assumption. +apply (trans_lt ? (S O)).simplify.apply le_n.assumption. unfold injn.intros. -apply nat_compare_elim i j. +apply (nat_compare_elim i j). (* i < j *) intro. -absurd j-i \lt p. +absurd (j-i \lt p). simplify. -rewrite > S_pred p. +rewrite > (S_pred p). apply le_S_S. apply le_plus_to_minus. -apply trans_le ? (pred p).assumption. +apply (trans_le ? (pred p)).assumption. rewrite > sym_plus. apply le_plus_n. unfold prime in H. elim H. -apply trans_lt ? (S O).simplify.apply le_n.assumption. -apply le_to_not_lt p (j-i). +apply (trans_lt ? (S O)).simplify.apply le_n.assumption. +apply (le_to_not_lt p (j-i)). apply divides_to_le.simplify. apply le_SO_minus.assumption. -cut divides p a \lor divides p (j-i). +cut (divides p a \lor divides p (j-i)). elim Hcut.apply False_ind.apply H1.assumption.assumption. apply divides_times_to_divides.assumption. rewrite > distr_times_minus. apply eq_mod_to_divides. unfold prime in H. elim H. -apply trans_lt ? (S O).simplify.apply le_n.assumption. +apply (trans_lt ? (S O)).simplify.apply le_n.assumption. apply sym_eq. apply H4. (* i = j *) intro. assumption. (* j < i *) intro. -absurd i-j \lt p. +absurd (i-j \lt p). simplify. -rewrite > S_pred p. +rewrite > (S_pred p). apply le_S_S. apply le_plus_to_minus. -apply trans_le ? (pred p).assumption. +apply (trans_le ? (pred p)).assumption. rewrite > sym_plus. apply le_plus_n. unfold prime in H. elim H. -apply trans_lt ? (S O).simplify.apply le_n.assumption. -apply le_to_not_lt p (i-j). +apply (trans_lt ? (S O)).simplify.apply le_n.assumption. +apply (le_to_not_lt p (i-j)). apply divides_to_le.simplify. apply le_SO_minus.assumption. -cut divides p a \lor divides p (i-j). +cut (divides p a \lor divides p (i-j)). elim Hcut.apply False_ind.apply H1.assumption.assumption. apply divides_times_to_divides.assumption. rewrite > distr_times_minus. apply eq_mod_to_divides. unfold prime in H. elim H. -apply trans_lt ? (S O).simplify.apply le_n.assumption. +apply (trans_lt ? (S O)).simplify.apply le_n.assumption. apply H4. qed. theorem congruent_exp_pred_SO: \forall p,a:nat. prime p \to \lnot divides p a \to congruent (exp a (pred p)) (S O) p. intros. -cut O < a. -cut O < p. -cut O < pred p. +cut (O < a). +cut (O < p). +cut (O < pred p). apply divides_to_congruent. assumption. -change with O < exp a (pred p). +change with (O < exp a (pred p)). apply lt_O_exp.assumption. -cut divides p (exp a (pred p)-(S O)) \lor divides p (pred p)!. +cut (divides p (exp a (pred p)-(S O)) \lor divides p (pred p)!). elim Hcut3. assumption. apply False_ind. -apply prime_to_not_divides_fact p H (pred p). -change with S (pred p) \le p. +apply (prime_to_not_divides_fact p H (pred p)). +change with (S (pred p) \le p). rewrite < S_pred.apply le_n. assumption.assumption. apply divides_times_to_divides. assumption. rewrite > times_minus_l. -rewrite > sym_times (S O). +rewrite > (sym_times (S O)). rewrite < times_n_SO. -rewrite > S_pred (pred p). +rewrite > (S_pred (pred p)). rewrite > eq_fact_pi. (* in \vdash (? ? (? % ?)). *) rewrite > exp_pi_l. apply congruent_to_divides. assumption. -apply transitive_congruent p ? -(pi (pred (pred p)) (\lambda m. a*m \mod p) (S O)). -apply congruent_pi (\lambda m. a*m). +apply (transitive_congruent p ? +(pi (pred (pred p)) (\lambda m. a*m \mod p) (S O))). +apply (congruent_pi (\lambda m. a*m)). assumption. -cut pi (pred(pred p)) (\lambda m.m) (S O) -= pi (pred(pred p)) (\lambda m.a*m \mod p) (S O). +cut (pi (pred(pred p)) (\lambda m.m) (S O) += pi (pred(pred p)) (\lambda m.a*m \mod p) (S O)). rewrite > Hcut3.apply congruent_n_n. rewrite < eq_map_iter_i_pi. rewrite < eq_map_iter_i_pi. @@ -229,21 +229,21 @@ rewrite < plus_n_Sm.rewrite < plus_n_O. rewrite < S_pred. apply permut_mod.assumption. assumption.assumption. -intros.cut m=O. +intros.cut (m=O). rewrite > Hcut3.rewrite < times_n_O. apply mod_O_n.apply sym_eq.apply le_n_O_to_eq. apply le_S_S_to_le.assumption. assumption. -change with (S O) \le pred p. +change with ((S O) \le pred p). apply le_S_S_to_le.rewrite < S_pred. unfold prime in H.elim H.assumption.assumption. -unfold prime in H.elim H.apply trans_lt ? (S O). +unfold prime in H.elim H.apply (trans_lt ? (S O)). simplify.apply le_n.assumption. -cut O < a \lor O = a. +cut (O < a \lor O = a). elim Hcut.assumption. apply False_ind.apply H1. rewrite < H2. -apply witness ? ? O.apply times_n_O. +apply (witness ? ? O).apply times_n_O. apply le_to_or_lt_eq. apply le_O_n. qed. diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma index 90de2013a..8cb4867ff 100644 --- a/helm/matita/library/nat/gcd.ma +++ b/helm/matita/library/nat/gcd.ma @@ -39,7 +39,7 @@ definition gcd : nat \to nat \to nat \def theorem divides_mod: \forall p,m,n:nat. O < n \to p \divides m \to p \divides n \to p \divides (m \mod n). intros.elim H1.elim H2. -apply witness ? ? (n2 - n1*(m / n)). +apply (witness ? ? (n2 - n1*(m / n))). rewrite > distr_times_minus. rewrite < H3. rewrite < assoc_times. @@ -54,7 +54,7 @@ qed. theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to p \divides (m \mod n) \to p \divides n \to p \divides m. intros.elim H1.elim H2. -apply witness p m ((n1*(m / n))+n2). +apply (witness p m ((n1*(m / n))+n2)). rewrite > distr_times_plus. rewrite < H3. rewrite < assoc_times. @@ -65,30 +65,30 @@ qed. theorem divides_gcd_aux_mn: \forall p,m,n. O < n \to n \le m \to n \le p \to gcd_aux p m n \divides m \land gcd_aux p m n \divides n. intro.elim p. -absurd O < n.assumption.apply le_to_not_lt.assumption. -cut (n1 \divides m) \lor (n1 \ndivides m). +absurd (O < n).assumption.apply le_to_not_lt.assumption. +cut ((n1 \divides m) \lor (n1 \ndivides m)). change with -(match divides_b n1 m with +((match divides_b n1 m with [ true \Rightarrow n1 | false \Rightarrow gcd_aux n n1 (m \mod n1)]) \divides m \land (match divides_b n1 m with [ true \Rightarrow n1 -| false \Rightarrow gcd_aux n n1 (m \mod n1)]) \divides n1. +| false \Rightarrow gcd_aux n n1 (m \mod n1)]) \divides n1). elim Hcut.rewrite > divides_to_divides_b_true. simplify. -split.assumption.apply witness n1 n1 (S O).apply times_n_SO. +split.assumption.apply (witness n1 n1 (S O)).apply times_n_SO. assumption.assumption. rewrite > not_divides_to_divides_b_false. change with -gcd_aux n n1 (m \mod n1) \divides m \land -gcd_aux n n1 (m \mod n1) \divides n1. -cut gcd_aux n n1 (m \mod n1) \divides n1 \land -gcd_aux n n1 (m \mod n1) \divides mod m n1. +(gcd_aux n n1 (m \mod n1) \divides m \land +gcd_aux n n1 (m \mod n1) \divides n1). +cut (gcd_aux n n1 (m \mod n1) \divides n1 \land +gcd_aux n n1 (m \mod n1) \divides mod m n1). elim Hcut1. -split.apply divides_mod_to_divides ? ? n1. +split.apply (divides_mod_to_divides ? ? n1). assumption.assumption.assumption.assumption. apply H. -cut O \lt m \mod n1 \lor O = mod m n1. +cut (O \lt m \mod n1 \lor O = mod m n1). elim Hcut1.assumption. apply False_ind.apply H4.apply mod_O_to_divides. assumption.apply sym_eq.assumption. @@ -96,18 +96,18 @@ apply le_to_or_lt_eq.apply le_O_n. apply lt_to_le. apply lt_mod_m_m.assumption. apply le_S_S_to_le. -apply trans_le ? n1. -change with m \mod n1 < n1. +apply (trans_le ? n1). +change with (m \mod n1 < n1). apply lt_mod_m_m.assumption.assumption. assumption.assumption. -apply decidable_divides n1 m.assumption. +apply (decidable_divides n1 m).assumption. qed. theorem divides_gcd_nm: \forall n,m. gcd n m \divides m \land gcd n m \divides n. intros. change with -match leb n m with +(match leb n m with [ true \Rightarrow match n with [ O \Rightarrow m @@ -125,88 +125,88 @@ match leb n m with | false \Rightarrow match m with [ O \Rightarrow n - | (S p) \Rightarrow gcd_aux (S p) n (S p) ] ] \divides n. -apply leb_elim n m. -apply nat_case1 n. + | (S p) \Rightarrow gcd_aux (S p) n (S p) ] ] \divides n). +apply (leb_elim n m). +apply (nat_case1 n). simplify.intros.split. -apply witness m m (S O).apply times_n_SO. -apply witness m O O.apply times_n_O. +apply (witness m m (S O)).apply times_n_SO. +apply (witness m O O).apply times_n_O. intros.change with -gcd_aux (S m1) m (S m1) \divides m +(gcd_aux (S m1) m (S m1) \divides m \land -gcd_aux (S m1) m (S m1) \divides (S m1). +gcd_aux (S m1) m (S m1) \divides (S m1)). apply divides_gcd_aux_mn. simplify.apply le_S_S.apply le_O_n. assumption.apply le_n. simplify.intro. -apply nat_case1 m. +apply (nat_case1 m). simplify.intros.split. -apply witness n O O.apply times_n_O. -apply witness n n (S O).apply times_n_SO. +apply (witness n O O).apply times_n_O. +apply (witness n n (S O)).apply times_n_SO. intros.change with -gcd_aux (S m1) n (S m1) \divides (S m1) +(gcd_aux (S m1) n (S m1) \divides (S m1) \land -gcd_aux (S m1) n (S m1) \divides n. -cut gcd_aux (S m1) n (S m1) \divides n +gcd_aux (S m1) n (S m1) \divides n). +cut (gcd_aux (S m1) n (S m1) \divides n \land -gcd_aux (S m1) n (S m1) \divides S m1. +gcd_aux (S m1) n (S m1) \divides S m1). elim Hcut.split.assumption.assumption. apply divides_gcd_aux_mn. simplify.apply le_S_S.apply le_O_n. apply not_lt_to_le.simplify.intro.apply H. -rewrite > H1.apply trans_le ? (S n). +rewrite > H1.apply (trans_le ? (S n)). apply le_n_Sn.assumption.apply le_n. qed. theorem divides_gcd_n: \forall n,m. gcd n m \divides n. intros. -exact proj2 ? ? (divides_gcd_nm n m). +exact (proj2 ? ? (divides_gcd_nm n m)). qed. theorem divides_gcd_m: \forall n,m. gcd n m \divides m. intros. -exact proj1 ? ? (divides_gcd_nm n m). +exact (proj1 ? ? (divides_gcd_nm n m)). qed. theorem divides_gcd_aux: \forall p,m,n,d. O < n \to n \le m \to n \le p \to d \divides m \to d \divides n \to d \divides gcd_aux p m n. intro.elim p. -absurd O < n.assumption.apply le_to_not_lt.assumption. +absurd (O < n).assumption.apply le_to_not_lt.assumption. change with -d \divides +(d \divides (match divides_b n1 m with [ true \Rightarrow n1 -| false \Rightarrow gcd_aux n n1 (m \mod n1)]). -cut n1 \divides m \lor n1 \ndivides m. +| false \Rightarrow gcd_aux n n1 (m \mod n1)])). +cut (n1 \divides m \lor n1 \ndivides m). elim Hcut. rewrite > divides_to_divides_b_true. simplify.assumption. assumption.assumption. rewrite > not_divides_to_divides_b_false. -change with d \divides gcd_aux n n1 (m \mod n1). +change with (d \divides gcd_aux n n1 (m \mod n1)). apply H. -cut O \lt m \mod n1 \lor O = m \mod n1. +cut (O \lt m \mod n1 \lor O = m \mod n1). elim Hcut1.assumption. -absurd n1 \divides m.apply mod_O_to_divides. +absurd (n1 \divides m).apply mod_O_to_divides. assumption.apply sym_eq.assumption.assumption. apply le_to_or_lt_eq.apply le_O_n. apply lt_to_le. apply lt_mod_m_m.assumption. apply le_S_S_to_le. -apply trans_le ? n1. -change with m \mod n1 < n1. +apply (trans_le ? n1). +change with (m \mod n1 < n1). apply lt_mod_m_m.assumption.assumption. assumption. apply divides_mod.assumption.assumption.assumption. assumption.assumption. -apply decidable_divides n1 m.assumption. +apply (decidable_divides n1 m).assumption. qed. theorem divides_d_gcd: \forall m,n,d. d \divides m \to d \divides n \to d \divides gcd n m. intros. change with -d \divides +(d \divides match leb n m with [ true \Rightarrow match n with @@ -215,17 +215,17 @@ match leb n m with | false \Rightarrow match m with [ O \Rightarrow n - | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]. -apply leb_elim n m. -apply nat_case1 n.simplify.intros.assumption. + | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]). +apply (leb_elim n m). +apply (nat_case1 n).simplify.intros.assumption. intros. -change with d \divides gcd_aux (S m1) m (S m1). +change with (d \divides gcd_aux (S m1) m (S m1)). apply divides_gcd_aux. simplify.apply le_S_S.apply le_O_n.assumption.apply le_n.assumption. rewrite < H2.assumption. -apply nat_case1 m.simplify.intros.assumption. +apply (nat_case1 m).simplify.intros.assumption. intros. -change with d \divides gcd_aux (S m1) n (S m1). +change with (d \divides gcd_aux (S m1) n (S m1)). apply divides_gcd_aux. simplify.apply le_S_S.apply le_O_n. apply lt_to_le.apply not_le_to_lt.assumption.apply le_n.assumption. @@ -236,49 +236,49 @@ theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to \exists a,b. a*n - b*m = gcd_aux p m n \lor b*m - a*n = gcd_aux p m n. intro. elim p. -absurd O < n.assumption.apply le_to_not_lt.assumption. -cut O < m. -cut n1 \divides m \lor n1 \ndivides m. +absurd (O < n).assumption.apply le_to_not_lt.assumption. +cut (O < m). +cut (n1 \divides m \lor n1 \ndivides m). change with -\exists a,b. +(\exists a,b. a*n1 - b*m = match divides_b n1 m with [ true \Rightarrow n1 | false \Rightarrow gcd_aux n n1 (m \mod n1)] \lor b*m - a*n1 = match divides_b n1 m with [ true \Rightarrow n1 -| false \Rightarrow gcd_aux n n1 (m \mod n1)]. +| false \Rightarrow gcd_aux n n1 (m \mod n1)]). elim Hcut1. rewrite > divides_to_divides_b_true. simplify. -apply ex_intro ? ? (S O). -apply ex_intro ? ? O. +apply (ex_intro ? ? (S O)). +apply (ex_intro ? ? O). left.simplify.rewrite < plus_n_O. apply sym_eq.apply minus_n_O. assumption.assumption. rewrite > not_divides_to_divides_b_false. change with -\exists a,b. +(\exists a,b. a*n1 - b*m = gcd_aux n n1 (m \mod n1) \lor -b*m - a*n1 = gcd_aux n n1 (m \mod n1). +b*m - a*n1 = gcd_aux n n1 (m \mod n1)). cut -\exists a,b. +(\exists a,b. a*(m \mod n1) - b*n1= gcd_aux n n1 (m \mod n1) \lor -b*n1 - a*(m \mod n1) = gcd_aux n n1 (m \mod n1). +b*n1 - a*(m \mod n1) = gcd_aux n n1 (m \mod n1)). elim Hcut2.elim H5.elim H6. (* first case *) rewrite < H7. -apply ex_intro ? ? (a1+a*(m / n1)). -apply ex_intro ? ? a. +apply (ex_intro ? ? (a1+a*(m / n1))). +apply (ex_intro ? ? a). right. rewrite < sym_plus. -rewrite < sym_times n1. +rewrite < (sym_times n1). rewrite > distr_times_plus. -rewrite > sym_times n1. -rewrite > sym_times n1. -rewrite > div_mod m n1 in \vdash (? ? (? % ?) ?). +rewrite > (sym_times n1). +rewrite > (sym_times n1). +rewrite > (div_mod m n1) in \vdash (? ? (? % ?) ?). rewrite > assoc_times. rewrite < sym_plus. rewrite > distr_times_plus. @@ -290,15 +290,15 @@ apply le_n. assumption. (* second case *) rewrite < H7. -apply ex_intro ? ? (a1+a*(m / n1)). -apply ex_intro ? ? a. +apply (ex_intro ? ? (a1+a*(m / n1))). +apply (ex_intro ? ? a). left. (* clear Hcut2.clear H5.clear H6.clear H. *) rewrite > sym_times. rewrite > distr_times_plus. rewrite > sym_times. -rewrite > sym_times n1. -rewrite > div_mod m n1 in \vdash (? ? (? ? %) ?). +rewrite > (sym_times n1). +rewrite > (div_mod m n1) in \vdash (? ? (? ? %) ?). rewrite > distr_times_plus. rewrite > assoc_times. rewrite < eq_minus_minus_minus_plus. @@ -307,67 +307,67 @@ rewrite < plus_minus. rewrite < minus_n_n.reflexivity. apply le_n. assumption. -apply H n1 (m \mod n1). -cut O \lt m \mod n1 \lor O = m \mod n1. +apply (H n1 (m \mod n1)). +cut (O \lt m \mod n1 \lor O = m \mod n1). elim Hcut2.assumption. -absurd n1 \divides m.apply mod_O_to_divides. +absurd (n1 \divides m).apply mod_O_to_divides. assumption. symmetry.assumption.assumption. apply le_to_or_lt_eq.apply le_O_n. apply lt_to_le. apply lt_mod_m_m.assumption. apply le_S_S_to_le. -apply trans_le ? n1. -change with m \mod n1 < n1. +apply (trans_le ? n1). +change with (m \mod n1 < n1). apply lt_mod_m_m. assumption.assumption.assumption.assumption. -apply decidable_divides n1 m.assumption. -apply lt_to_le_to_lt ? n1.assumption.assumption. +apply (decidable_divides n1 m).assumption. +apply (lt_to_le_to_lt ? n1).assumption.assumption. qed. theorem eq_minus_gcd: \forall m,n.\exists a,b.a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m). intros. unfold gcd. -apply leb_elim n m. -apply nat_case1 n. +apply (leb_elim n m). +apply (nat_case1 n). simplify.intros. -apply ex_intro ? ? O. -apply ex_intro ? ? (S O). +apply (ex_intro ? ? O). +apply (ex_intro ? ? (S O)). right.simplify. rewrite < plus_n_O. apply sym_eq.apply minus_n_O. intros. change with -\exists a,b. +(\exists a,b. a*(S m1) - b*m = (gcd_aux (S m1) m (S m1)) -\lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1)). +\lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1))). apply eq_minus_gcd_aux. simplify. apply le_S_S.apply le_O_n. assumption.apply le_n. -apply nat_case1 m. +apply (nat_case1 m). simplify.intros. -apply ex_intro ? ? (S O). -apply ex_intro ? ? O. +apply (ex_intro ? ? (S O)). +apply (ex_intro ? ? O). left.simplify. rewrite < plus_n_O. apply sym_eq.apply minus_n_O. intros. change with -\exists a,b. +(\exists a,b. a*n - b*(S m1) = (gcd_aux (S m1) n (S m1)) -\lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1)). +\lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1))). cut -\exists a,b. +(\exists a,b. a*(S m1) - b*n = (gcd_aux (S m1) n (S m1)) \lor -b*n - a*(S m1) = (gcd_aux (S m1) n (S m1)). +b*n - a*(S m1) = (gcd_aux (S m1) n (S m1))). elim Hcut.elim H2.elim H3. -apply ex_intro ? ? a1. -apply ex_intro ? ? a. +apply (ex_intro ? ? a1). +apply (ex_intro ? ? a). right.assumption. -apply ex_intro ? ? a1. -apply ex_intro ? ? a. +apply (ex_intro ? ? a1). +apply (ex_intro ? ? a). left.assumption. apply eq_minus_gcd_aux. simplify. apply le_S_S.apply le_O_n. @@ -383,7 +383,7 @@ qed. theorem gcd_O_to_eq_O:\forall m,n:nat. (gcd m n) = O \to m = O \land n = O. -intros.cut O \divides n \land O \divides m. +intros.cut (O \divides n \land O \divides m). elim Hcut.elim H2.split. assumption.elim H1.assumption. rewrite < H. @@ -392,11 +392,11 @@ qed. theorem symmetric_gcd: symmetric nat gcd. change with -\forall n,m:nat. gcd n m = gcd m n. +(\forall n,m:nat. gcd n m = gcd m n). intros. -cut O < (gcd n m) \lor O = (gcd n m). +cut (O < (gcd n m) \lor O = (gcd n m)). elim Hcut. -cut O < (gcd m n) \lor O = (gcd m n). +cut (O < (gcd m n) \lor O = (gcd m n)). elim Hcut1. apply antisym_le. apply divides_to_le.assumption. @@ -404,12 +404,12 @@ apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m. apply divides_to_le.assumption. apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m. rewrite < H1. -cut m=O \land n=O. +cut (m=O \land n=O). elim Hcut2.rewrite > H2.rewrite > H3.reflexivity. apply gcd_O_to_eq_O.apply sym_eq.assumption. apply le_to_or_lt_eq.apply le_O_n. rewrite < H. -cut n=O \land m=O. +cut (n=O \land m=O). elim Hcut1.rewrite > H1.rewrite > H2.reflexivity. apply gcd_O_to_eq_O.apply sym_eq.assumption. apply le_to_or_lt_eq.apply le_O_n. @@ -422,11 +422,11 @@ theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O). intro. apply antisym_le.apply divides_to_le.simplify.apply le_n. apply divides_gcd_n. -cut O < gcd (S O) n \lor O = gcd (S O) n. +cut (O < gcd (S O) n \lor O = gcd (S O) n). elim Hcut.assumption. apply False_ind. -apply not_eq_O_S O. -cut (S O)=O \land n=O. +apply (not_eq_O_S O). +cut ((S O)=O \land n=O). elim Hcut1.apply sym_eq.assumption. apply gcd_O_to_eq_O.apply sym_eq.assumption. apply le_to_or_lt_eq.apply le_O_n. @@ -434,19 +434,19 @@ qed. theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to gcd n m = (S O). -intros.simplify in H.change with gcd n m = (S O). +intros.simplify in H.change with (gcd n m = (S O)). elim H. apply antisym_le. apply not_lt_to_le. -change with (S (S O)) \le gcd n m \to False.intro. -apply H1.rewrite < H3 (gcd n m). +change with ((S (S O)) \le gcd n m \to False).intro. +apply H1.rewrite < (H3 (gcd n m)). apply divides_gcd_m. apply divides_gcd_n.assumption. -cut O < gcd n m \lor O = gcd n m. +cut (O < gcd n m \lor O = gcd n m). elim Hcut.assumption. apply False_ind. -apply not_le_Sn_O (S O). -cut n=O \land m=O. +apply (not_le_Sn_O (S O)). +cut (n=O \land m=O). elim Hcut1.rewrite < H5 in \vdash (? ? %).assumption. apply gcd_O_to_eq_O.apply sym_eq.assumption. apply le_to_or_lt_eq.apply le_O_n. @@ -455,40 +455,40 @@ qed. theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to n \divides p*q \to n \divides p \lor n \divides q. intros. -cut n \divides p \lor n \ndivides p. +cut (n \divides p \lor n \ndivides p). elim Hcut. left.assumption. right. -cut \exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O). +cut (\exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O)). elim Hcut1.elim H3.elim H4. (* first case *) -rewrite > times_n_SO q.rewrite < H5. +rewrite > (times_n_SO q).rewrite < H5. rewrite > distr_times_minus. -rewrite > sym_times q (a1*p). -rewrite > assoc_times a1. +rewrite > (sym_times q (a1*p)). +rewrite > (assoc_times a1). elim H1.rewrite > H6. -rewrite < sym_times n.rewrite < assoc_times. -rewrite > sym_times q.rewrite > assoc_times. -rewrite < assoc_times a1.rewrite < sym_times n. -rewrite > assoc_times n. +rewrite < (sym_times n).rewrite < assoc_times. +rewrite > (sym_times q).rewrite > assoc_times. +rewrite < (assoc_times a1).rewrite < (sym_times n). +rewrite > (assoc_times n). rewrite < distr_times_minus. -apply witness ? ? (q*a-a1*n2).reflexivity. +apply (witness ? ? (q*a-a1*n2)).reflexivity. (* second case *) -rewrite > times_n_SO q.rewrite < H5. +rewrite > (times_n_SO q).rewrite < H5. rewrite > distr_times_minus. -rewrite > sym_times q (a1*p). -rewrite > assoc_times a1. +rewrite > (sym_times q (a1*p)). +rewrite > (assoc_times a1). elim H1.rewrite > H6. rewrite < sym_times.rewrite > assoc_times. -rewrite < assoc_times q. -rewrite < sym_times n. +rewrite < (assoc_times q). +rewrite < (sym_times n). rewrite < distr_times_minus. -apply witness ? ? (n2*a1-q*a).reflexivity. +apply (witness ? ? (n2*a1-q*a)).reflexivity. (* end second case *) -rewrite < prime_to_gcd_SO n p. +rewrite < (prime_to_gcd_SO n p). apply eq_minus_gcd. assumption.assumption. -apply decidable_divides n p. -apply trans_lt ? (S O).simplify.apply le_n. +apply (decidable_divides n p). +apply (trans_lt ? (S O)).simplify.apply le_n. simplify in H.elim H. assumption. qed. diff --git a/helm/matita/library/nat/le_arith.ma b/helm/matita/library/nat/le_arith.ma index 7ece3fdc7..a76183063 100644 --- a/helm/matita/library/nat/le_arith.ma +++ b/helm/matita/library/nat/le_arith.ma @@ -31,7 +31,7 @@ theorem le_plus_r: \forall p,n,m:nat. n \le m \to p + n \le p + m theorem monotonic_le_plus_l: \forall m:nat.monotonic nat le (\lambda n.n + m). simplify.intros. -rewrite < sym_plus.rewrite < sym_plus m. +rewrite < sym_plus.rewrite < (sym_plus m). apply le_plus_r.assumption. qed. @@ -41,13 +41,13 @@ theorem le_plus_l: \forall p,n,m:nat. n \le m \to n + p \le m + p 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 ? (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. m \le n + m. -intros.change with O+m \le n+m. +intros.change with (O+m \le n+m). apply le_plus_l.apply le_O_n. qed. @@ -73,7 +73,7 @@ theorem le_times_r: \forall p,n,m:nat. n \le m \to p*n \le p*m theorem monotonic_le_times_l: \forall m:nat.monotonic nat le (\lambda n.n*m). simplify.intros. -rewrite < sym_times.rewrite < sym_times m. +rewrite < sym_times.rewrite < (sym_times m). apply le_times_r.assumption. qed. @@ -83,7 +83,7 @@ theorem le_times_l: \forall p,n,m:nat. n \le m \to n*p \le m*p 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 ? (n2*m1). +apply (trans_le ? (n2*m1)). apply le_times_l.assumption. apply le_times_r.assumption. qed. @@ -93,4 +93,3 @@ intros.elim H.simplify. elim (plus_n_O ?).apply le_n. simplify.rewrite < sym_plus.apply le_plus_n. qed. - diff --git a/helm/matita/library/nat/lt_arith.ma b/helm/matita/library/nat/lt_arith.ma index ce66decaa..4897fb598 100644 --- a/helm/matita/library/nat/lt_arith.ma +++ b/helm/matita/library/nat/lt_arith.ma @@ -30,9 +30,9 @@ monotonic_lt_plus_r. theorem monotonic_lt_plus_l: \forall n:nat.monotonic nat lt (\lambda m.m+n). -change with \forall n,p,q:nat. p < q \to p + n < q + n. +change with (\forall n,p,q:nat. p < q \to p + n < q + n). intros. -rewrite < sym_plus. rewrite < sym_plus n. +rewrite < sym_plus. rewrite < (sym_plus n). apply lt_plus_r.assumption. qed. @@ -41,7 +41,7 @@ monotonic_lt_plus_l. theorem lt_plus: \forall n,m,p,q:nat. n < m \to p < q \to n + p < m + q. intros. -apply trans_lt ? (n + q). +apply (trans_lt ? (n + q)). apply lt_plus_r.assumption. apply lt_plus_l.assumption. qed. @@ -49,18 +49,18 @@ qed. 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. +rewrite > (plus_n_O q).assumption. apply H. simplify.apply le_S_S_to_le. rewrite > plus_n_Sm. -rewrite > plus_n_Sm q. +rewrite > (plus_n_Sm q). exact H1. qed. theorem lt_plus_to_lt_r :\forall n,p,q:nat. n+p < n+q \to p sym_plus. -rewrite > sym_plus q.assumption. +rewrite > (sym_plus q).assumption. qed. (* times and zero *) @@ -71,10 +71,10 @@ qed. (* times *) theorem monotonic_lt_times_r: \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. +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 p + (S n1) * p < q + (S n1) * q. +change with (p + (S n1) * p < q + (S n1) * q). apply lt_plus.assumption.assumption. qed. @@ -84,9 +84,9 @@ theorem lt_times_r: \forall n,p,q:nat. p < q \to (S n) * p < (S n) * q theorem monotonic_lt_times_l: \forall m:nat.monotonic nat lt (\lambda n.n * (S m)). change with -\forall n,p,q:nat. p < q \to p*(S n) < 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). +rewrite < sym_times.rewrite < (sym_times (S n)). apply lt_times_r.assumption. qed. @@ -96,44 +96,44 @@ variant lt_times_l: \forall n,p,q:nat. p nat_compare_n_n.reflexivity. intro.apply nat_compare_elim.intro. -absurd p plus_n_O ((S m1)*(n / (S m1))). +rewrite > (plus_n_O ((S m1)*(n / (S m1)))). rewrite < H2. rewrite < sym_times. rewrite < div_mod. @@ -177,11 +177,11 @@ qed. theorem lt_div_n_m_n: \forall n,m:nat. (S O) < m \to O < n \to n / m \lt n. intros. -apply nat_case1 (n / m).intro. +apply (nat_case1 (n / m)).intro. assumption.intros.rewrite < H2. rewrite > (div_mod n m) in \vdash (? ? %). -apply lt_to_le_to_lt ? ((n / m)*m). -apply lt_to_le_to_lt ? ((n / m)*(S (S O))). +apply (lt_to_le_to_lt ? ((n / m)*m)). +apply (lt_to_le_to_lt ? ((n / m)*(S (S O)))). rewrite < sym_times. rewrite > H2. simplify. @@ -194,7 +194,7 @@ apply le_times_r. assumption. rewrite < sym_plus. apply le_plus_n. -apply trans_lt ? (S O). +apply (trans_lt ? (S O)). simplify. apply le_n.assumption. qed. @@ -202,11 +202,11 @@ qed. theorem monotonic_to_injective: \forall f:nat\to nat. monotonic nat lt f \to injective nat nat f. simplify.intros. -apply nat_compare_elim x y. -intro.apply False_ind.apply not_le_Sn_n (f x). +apply (nat_compare_elim x y). +intro.apply False_ind.apply (not_le_Sn_n (f x)). rewrite > H1 in \vdash (? ? %).apply H.apply H2. intros.assumption. -intro.apply False_ind.apply not_le_Sn_n (f y). +intro.apply False_ind.apply (not_le_Sn_n (f y)). rewrite < H1 in \vdash (? ? %).apply H.apply H2. qed. diff --git a/helm/matita/library/nat/minimization.ma b/helm/matita/library/nat/minimization.ma index 72812cb65..bc60b50ac 100644 --- a/helm/matita/library/nat/minimization.ma +++ b/helm/matita/library/nat/minimization.ma @@ -26,7 +26,7 @@ let rec max i f \def theorem max_O_f : \forall f: nat \to bool. max O f = O. intro. simplify. -elim f O. +elim (f O). simplify.reflexivity. simplify.reflexivity. qed. @@ -50,9 +50,9 @@ theorem le_to_le_max : \forall f: nat \to bool. \forall n,m:nat. n\le m \to max n f \le max m f. intros.elim H. apply le_n. -apply trans_le ? (max n1 f).apply H2. -cut (f (S n1) = true \land max (S n1) f = (S n1)) \lor -(f (S n1) = false \land max (S n1) f = max n1 f). +apply (trans_le ? (max n1 f)).apply H2. +cut ((f (S n1) = true \land max (S n1) f = (S n1)) \lor +(f (S n1) = false \land max (S n1) f = max n1 f)). elim Hcut.elim H3. rewrite > H5. apply le_S.apply le_max_n. @@ -62,10 +62,10 @@ qed. theorem f_m_to_le_max: \forall f: nat \to bool. \forall n,m:nat. m\le n \to f m = true \to m \le max n f. -intros 3.elim n.apply le_n_O_elim m H. +intros 3.elim n.apply (le_n_O_elim m H). apply le_O_n. -apply le_n_Sm_elim m n1 H1. -intro.apply trans_le ? (max n1 f). +apply (le_n_Sm_elim m n1 H1). +intro.apply (trans_le ? (max n1 f)). apply H.apply le_S_S_to_le.assumption.assumption. apply le_to_le_max.apply le_n_Sn. intro.simplify.rewrite < H3. @@ -81,19 +81,19 @@ theorem f_max_true : \forall f:nat \to bool. \forall n:nat. (\exists i:nat. le i n \land f i = true) \to f (max n f) = true. intros 2. elim n.elim H.elim H1.generalize in match H3. -apply le_n_O_elim a H2.intro.simplify.rewrite > H4. +apply (le_n_O_elim a H2).intro.simplify.rewrite > H4. simplify.assumption. simplify. -apply bool_ind (\lambda b:bool. +apply (bool_ind (\lambda b:bool. (f (S n1) = b) \to (f ([\lambda b:bool.nat] match b in bool with [ true \Rightarrow (S n1) -| false \Rightarrow (max n1 f)])) = true). +| false \Rightarrow (max n1 f)])) = true)). simplify.intro.assumption. simplify.intro.apply H. elim H1.elim H3.generalize in match H5. -apply le_n_Sm_elim a n1 H4. +apply (le_n_Sm_elim a n1 H4). intros. -apply ex_intro nat ? a. +apply (ex_intro nat ? a). split.apply le_S_S_to_le.assumption.assumption. intros.apply False_ind.apply not_eq_true_false. rewrite < H2.rewrite < H7.rewrite > H6. reflexivity. @@ -103,16 +103,16 @@ qed. theorem lt_max_to_false : \forall f:nat \to bool. \forall n,m:nat. (max n f) < m \to m \leq n \to f m = false. intros 2. -elim n.absurd le m O.assumption. -cut O < m.apply lt_O_n_elim m Hcut.exact not_le_Sn_O. -rewrite < max_O_f f.assumption. +elim n.absurd (le m O).assumption. +cut (O < m).apply (lt_O_n_elim m Hcut).exact not_le_Sn_O. +rewrite < (max_O_f f).assumption. generalize in match H1. -elim max_S_max f n1. +elim (max_S_max f n1). elim H3. -absurd m \le S n1.assumption. +absurd (m \le S n1).assumption. apply lt_to_not_le.rewrite < H6.assumption. elim H3. -apply le_n_Sm_elim m n1 H2. +apply (le_n_Sm_elim m n1 H2). intro. apply H.rewrite < H6.assumption. apply le_S_S_to_le.assumption. @@ -133,14 +133,13 @@ definition min : nat \to (nat \to bool) \to nat \def theorem min_aux_O_f: \forall f:nat \to bool. \forall i :nat. min_aux O i f = i. intros.simplify.rewrite < minus_n_O. -elim f i. -simplify.reflexivity. +elim (f i).reflexivity. simplify.reflexivity. qed. theorem min_O_f : \forall f:nat \to bool. min O f = O. -intro.apply min_aux_O_f f O. +intro.apply (min_aux_O_f f O). qed. theorem min_aux_S : \forall f: nat \to bool. \forall i,n:nat. @@ -156,23 +155,23 @@ theorem f_min_aux_true: \forall f:nat \to bool. \forall off,m:nat. f (min_aux off m f) = true. intros 2. elim off.elim H.elim H1.elim H2. -cut a = m. -rewrite > min_aux_O_f f.rewrite < Hcut.assumption. -apply antisym_le a m .assumption.rewrite > minus_n_O m.assumption. +cut (a = m). +rewrite > (min_aux_O_f f).rewrite < Hcut.assumption. +apply (antisym_le a m).assumption.rewrite > (minus_n_O m).assumption. simplify. -apply bool_ind (\lambda b:bool. +apply (bool_ind (\lambda b:bool. (f (m-(S n)) = b) \to (f ([\lambda b:bool.nat] match b in bool with [ true \Rightarrow m-(S n) -| false \Rightarrow (min_aux n m f)])) = true). +| false \Rightarrow (min_aux n m f)])) = true)). simplify.intro.assumption. simplify.intro.apply H. elim H1.elim H3.elim H4. elim (le_to_or_lt_eq (m-(S n)) a H6). -apply ex_intro nat ? a. +apply (ex_intro nat ? a). split.split. apply lt_minus_S_n_to_le_minus_n.assumption. assumption.assumption. -absurd f a = false.rewrite < H8.assumption. +absurd (f a = false).rewrite < H8.assumption. rewrite > H5. apply not_eq_true_false. reflexivity. @@ -181,15 +180,15 @@ qed. theorem lt_min_aux_to_false : \forall f:nat \to bool. \forall n,off,m:nat. (n-off) \leq m \to m < (min_aux off n f) \to f m = false. intros 3. -elim off.absurd le n m.rewrite > minus_n_O.assumption. -apply lt_to_not_le.rewrite < min_aux_O_f f n.assumption. +elim off.absurd (le n m).rewrite > minus_n_O.assumption. +apply lt_to_not_le.rewrite < (min_aux_O_f f n).assumption. generalize in match H1. -elim min_aux_S f n1 n. +elim (min_aux_S f n1 n). elim H3. -absurd n - S n1 \le m.assumption. +absurd (n - S n1 \le m).assumption. apply lt_to_not_le.rewrite < H6.assumption. elim H3. -elim le_to_or_lt_eq (n -(S n1)) m. +elim (le_to_or_lt_eq (n -(S n1)) m). apply H.apply lt_minus_S_n_to_le_minus_n.assumption. rewrite < H6.assumption. rewrite < H7.assumption. @@ -200,11 +199,11 @@ theorem le_min_aux : \forall f:nat \to bool. \forall n,off:nat. (n-off) \leq (min_aux off n f). intros 3. elim off.rewrite < minus_n_O. -rewrite > min_aux_O_f f n.apply le_n. -elim min_aux_S f n1 n. +rewrite > (min_aux_O_f f n).apply le_n. +elim (min_aux_S f n1 n). elim H1.rewrite > H3.apply le_n. elim H1.rewrite > H3. -apply trans_le (n-(S n1)) (n-n1). +apply (trans_le (n-(S n1)) (n-n1)). apply monotonic_le_minus_r. apply le_n_Sn. assumption. diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma index 0c8780f7e..4910f3003 100644 --- a/helm/matita/library/nat/minus.ma +++ b/helm/matita/library/nat/minus.ma @@ -48,9 +48,9 @@ qed. theorem minus_Sn_m: \forall n,m:nat. m \leq n \to (S n)-m = S (n-m). intros 2. -apply nat_elim2 -(\lambda n,m.m \leq n \to (S n)-m = S (n-m)). -intros.apply le_n_O_elim n1 H. +apply (nat_elim2 +(\lambda n,m.m \leq n \to (S n)-m = S (n-m))). +intros.apply (le_n_O_elim n1 H). simplify.reflexivity. intros.simplify.reflexivity. intros.rewrite < H.reflexivity. @@ -60,9 +60,9 @@ qed. theorem plus_minus: \forall n,m,p:nat. m \leq n \to (n-m)+p = (n+p)-m. intros 2. -apply nat_elim2 -(\lambda n,m.\forall p:nat.m \leq n \to (n-m)+p = (n+p)-m). -intros.apply le_n_O_elim ? H. +apply (nat_elim2 +(\lambda n,m.\forall p:nat.m \leq n \to (n-m)+p = (n+p)-m)). +intros.apply (le_n_O_elim ? H). simplify.rewrite < minus_n_O.reflexivity. intros.simplify.reflexivity. intros.simplify.apply H.apply le_S_S_to_le.assumption. @@ -76,15 +76,15 @@ rewrite < minus_n_O.apply plus_n_O. elim n2.simplify. apply minus_n_n. rewrite < plus_n_Sm. -change with S n3 = (S n3 + n1)-n1. +change with (S n3 = (S n3 + n1)-n1). apply H. qed. theorem plus_minus_m_m: \forall n,m:nat. m \leq n \to n = (n-m)+m. intros 2. -apply nat_elim2 (\lambda n,m.m \leq n \to n = (n-m)+m). -intros.apply le_n_O_elim n1 H. +apply (nat_elim2 (\lambda n,m.m \leq n \to n = (n-m)+m)). +intros.apply (le_n_O_elim n1 H). reflexivity. intros.simplify.rewrite < plus_n_O.reflexivity. intros.simplify.rewrite < sym_plus.simplify. @@ -94,7 +94,7 @@ qed. theorem minus_to_plus :\forall n,m,p:nat.m \leq n \to n-m = p \to n = m+p. -intros.apply trans_eq ? ? ((n-m)+m). +intros.apply (trans_eq ? ? ((n-m)+m)). apply plus_minus_m_m. apply H.elim H1. apply sym_plus. @@ -103,7 +103,7 @@ qed. theorem plus_to_minus :\forall n,m,p:nat. n = m+p \to n-m = p. intros. -apply inj_plus_r m. +apply (inj_plus_r m). rewrite < H. rewrite < sym_plus. symmetry. @@ -121,15 +121,15 @@ qed. theorem minus_pred_pred : \forall n,m:nat. lt O n \to lt O m \to eq nat (minus (pred n) (pred m)) (minus n m). intros. -apply lt_O_n_elim n H.intro. -apply lt_O_n_elim m H1.intro. +apply (lt_O_n_elim n H).intro. +apply (lt_O_n_elim m H1).intro. simplify.reflexivity. qed. theorem eq_minus_n_m_O: \forall n,m:nat. n \leq m \to n-m = O. intros 2. -apply nat_elim2 (\lambda n,m.n \leq m \to n-m = O). +apply (nat_elim2 (\lambda n,m.n \leq m \to n-m = O)). intros.simplify.reflexivity. intros.apply False_ind. apply not_le_Sn_O. @@ -139,14 +139,14 @@ simplify.apply H.apply le_S_S_to_le. apply H1. qed. theorem le_SO_minus: \forall n,m:nat.S n \leq m \to S O \leq m-n. -intros.elim H.elim minus_Sn_n n.apply le_n. +intros.elim H.elim (minus_Sn_n n).apply le_n. rewrite > minus_Sn_m. apply le_S.assumption. apply lt_to_le.assumption. qed. theorem minus_le_S_minus_S: \forall n,m:nat. m-n \leq S (m-(S n)). -intros.apply nat_elim2 (\lambda n,m.m-n \leq S (m-(S n))). +intros.apply (nat_elim2 (\lambda n,m.m-n \leq S (m-(S n)))). intro.elim n1.simplify.apply le_n_Sn. simplify.rewrite < minus_n_O.apply le_n. intros.simplify.apply le_n_Sn. @@ -155,27 +155,27 @@ qed. theorem lt_minus_S_n_to_le_minus_n : \forall n,m,p:nat. m-(S n) < p \to m-n \leq p. intros 3.simplify.intro. -apply trans_le (m-n) (S (m-(S n))) p. +apply (trans_le (m-n) (S (m-(S n))) p). apply minus_le_S_minus_S. assumption. qed. theorem le_minus_m: \forall n,m:nat. n-m \leq n. -intros.apply nat_elim2 (\lambda m,n. n-m \leq n). +intros.apply (nat_elim2 (\lambda m,n. n-m \leq n)). intros.rewrite < minus_n_O.apply le_n. intros.simplify.apply le_n. intros.simplify.apply le_S.assumption. qed. theorem lt_minus_m: \forall n,m:nat. O < n \to O < m \to n-m \lt n. -intros.apply lt_O_n_elim n H.intro. -apply lt_O_n_elim m H1.intro. +intros.apply (lt_O_n_elim n H).intro. +apply (lt_O_n_elim m H1).intro. simplify.apply le_S_S.apply le_minus_m. qed. theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m. intros 2. -apply nat_elim2 (\lambda n,m:nat.n-m \leq O \to n \leq m). +apply (nat_elim2 (\lambda n,m:nat.n-m \leq O \to n \leq m)). intros.apply le_O_n. simplify.intros. assumption. simplify.intros.apply le_S_S.apply H.assumption. @@ -184,9 +184,9 @@ qed. (* galois *) theorem monotonic_le_minus_r: \forall p,q,n:nat. q \leq p \to n-p \le n-q. -simplify.intros 2.apply nat_elim2 -(\lambda p,q.\forall a.q \leq p \to a-p \leq a-q). -intros.apply le_n_O_elim n H.apply le_n. +simplify.intros 2.apply (nat_elim2 +(\lambda p,q.\forall a.q \leq p \to a-p \leq a-q)). +intros.apply (le_n_O_elim n H).apply le_n. intros.rewrite < minus_n_O. apply le_minus_m. intros.elim a.simplify.apply le_n. @@ -194,7 +194,7 @@ simplify.apply H.apply le_S_S_to_le.assumption. qed. theorem le_minus_to_plus: \forall n,m,p. (le (n-m) p) \to (le n (p+m)). -intros 2.apply nat_elim2 (\lambda n,m.\forall p.(le (n-m) p) \to (le n (p+m))). +intros 2.apply (nat_elim2 (\lambda n,m.\forall p.(le (n-m) p) \to (le n (p+m)))). intros.apply le_O_n. simplify.intros.rewrite < plus_n_O.assumption. intros. @@ -204,7 +204,7 @@ exact H1. qed. theorem le_plus_to_minus: \forall n,m,p. (le n (p+m)) \to (le (n-m) p). -intros 2.apply nat_elim2 (\lambda n,m.\forall p.(le n (p+m)) \to (le (n-m) p)). +intros 2.apply (nat_elim2 (\lambda n,m.\forall p.(le n (p+m)) \to (le (n-m) p))). intros.simplify.apply le_O_n. intros 2.rewrite < plus_n_O.intro.simplify.assumption. intros.simplify.apply H. @@ -213,11 +213,11 @@ qed. (* the converse of le_plus_to_minus does not hold *) theorem le_plus_to_minus_r: \forall n,m,p. (le (n+m) p) \to (le n (p-m)). -intros 3.apply nat_elim2 (\lambda m,p.(le (n+m) p) \to (le n (p-m))). +intros 3.apply (nat_elim2 (\lambda m,p.(le (n+m) p) \to (le n (p-m)))). intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption. -intro.intro.cut n=O.rewrite > Hcut.apply le_O_n. +intro.intro.cut (n=O).rewrite > Hcut.apply le_O_n. apply sym_eq. apply le_n_O_to_eq. -apply trans_le ? (n+(S n1)). +apply (trans_le ? (n+(S n1))). rewrite < sym_plus. apply le_plus_n.assumption. intros.simplify. @@ -229,16 +229,16 @@ qed. theorem distributive_times_minus: distributive nat times minus. simplify. intros. -apply (leb_elim z y). - intro.cut x*(y-z)+x*z = (x*y-x*z)+x*z. - apply inj_plus_l (x*z).assumption. - apply trans_eq nat ? (x*y). - rewrite < distr_times_plus.rewrite < plus_minus_m_m ? ? H.reflexivity. +apply ((leb_elim z y)). + intro.cut (x*(y-z)+x*z = (x*y-x*z)+x*z). + apply (inj_plus_l (x*z)).assumption. + apply (trans_eq nat ? (x*y)). + rewrite < distr_times_plus.rewrite < (plus_minus_m_m ? ? H).reflexivity. rewrite < plus_minus_m_m. reflexivity. apply le_times_r.assumption. intro.rewrite > eq_minus_n_m_O. - rewrite > eq_minus_n_m_O (x*y). + rewrite > (eq_minus_n_m_O (x*y)). rewrite < sym_times.simplify.reflexivity. apply le_times_r.apply lt_to_le.apply not_le_to_lt.assumption. apply lt_to_le.apply not_le_to_lt.assumption. @@ -249,23 +249,23 @@ theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p). intros. -cut m+p \le n \or m+p \nleq n. +cut (m+p \le n \or m+p \nleq n). elim Hcut. symmetry.apply plus_to_minus. - rewrite > assoc_plus.rewrite > sym_plus p.rewrite < plus_minus_m_m. + rewrite > assoc_plus.rewrite > (sym_plus p).rewrite < plus_minus_m_m. rewrite > sym_plus.rewrite < plus_minus_m_m. reflexivity. - apply trans_le ? (m+p). + apply (trans_le ? (m+p)). rewrite < sym_plus.apply le_plus_n. assumption. apply le_plus_to_minus_r.rewrite > sym_plus.assumption. - rewrite > eq_minus_n_m_O n (m+p). - rewrite > eq_minus_n_m_O (n-m) p. + rewrite > (eq_minus_n_m_O n (m+p)). + rewrite > (eq_minus_n_m_O (n-m) p). reflexivity. apply le_plus_to_minus.apply lt_to_le. rewrite < sym_plus. apply not_le_to_lt. assumption. apply lt_to_le.apply not_le_to_lt.assumption. - apply decidable_le (m+p) n. + apply (decidable_le (m+p) n). qed. theorem eq_plus_minus_minus_minus: \forall n,m,p:nat. p \le m \to m \le n \to diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma index e36c1beaa..fb7d1686e 100644 --- a/helm/matita/library/nat/nat.ma +++ b/helm/matita/library/nat/nat.ma @@ -33,7 +33,7 @@ theorem injective_S : injective nat nat S. simplify. intros. rewrite > pred_Sn. -rewrite > pred_Sn y. +rewrite > (pred_Sn y). apply eq_f. assumption. qed. @@ -86,18 +86,18 @@ theorem nat_elim2 : (\forall n,m:nat. R n m \to R (S n) (S m)) \to \forall n,m:nat. R n m. intros 5.elim n. apply H. -apply nat_case m.apply H1. +apply (nat_case m).apply H1. intros.apply H2. apply H3. qed. theorem decidable_eq_nat : \forall n,m:nat.decidable (n=m). intros.simplify. -apply nat_elim2 (\lambda n,m.(Or (n=m) ((n=m) \to False))). +apply (nat_elim2 (\lambda n,m.(Or (n=m) ((n=m) \to False)))). intro.elim n1. left.reflexivity. right.apply not_eq_O_S. intro.right.intro. -apply not_eq_O_S n1. +apply (not_eq_O_S n1). apply sym_eq.assumption. intros.elim H. left.apply eq_f. assumption. diff --git a/helm/matita/library/nat/nth_prime.ma b/helm/matita/library/nat/nth_prime.ma index 84407538d..5fa636301 100644 --- a/helm/matita/library/nat/nth_prime.ma +++ b/helm/matita/library/nat/nth_prime.ma @@ -42,8 +42,8 @@ theorem smallest_factor_fact: \forall n:nat. n < smallest_factor (S n!). intros. apply not_le_to_lt. -change with smallest_factor (S n!) \le n \to False.intro. -apply not_divides_S_fact n (smallest_factor(S 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. @@ -55,16 +55,16 @@ theorem ex_prime: \forall n. (S O) \le n \to \exists 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 (S n1)!)). +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 (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 (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. @@ -94,20 +94,20 @@ normalize.reflexivity. theorem prime_nth_prime : \forall n:nat.prime (nth_prime n). intro. -apply nat_case n. -change with prime (S(S O)). -apply primeb_to_Prop (S(S O)). +apply (nat_case n). +change with (prime (S(S O))). +apply (primeb_to_Prop (S(S O))). intro. change with -let previous_prime \def (nth_prime m) in +(let previous_prime \def (nth_prime m) in let upper_bound \def S previous_prime! in -prime (min_aux (upper_bound - (S previous_prime)) upper_bound primeb). +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 (nth_prime m)!)). +apply (ex_intro nat ? (smallest_factor (S (nth_prime m)!))). split.split. -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). +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. apply plus_minus_m_m. @@ -116,20 +116,20 @@ 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 (nth_prime m)!. +change with ((S(S O)) \le S (nth_prime m)!). apply le_S_S.apply le_SO_fact. qed. (* properties of nth_prime *) theorem increasing_nth_prime: increasing nth_prime. -change with \forall n:nat. (nth_prime n) < (nth_prime (S n)). +change with (\forall n:nat. (nth_prime n) < (nth_prime (S n))). intros. change with -let previous_prime \def (nth_prime n) in +(let previous_prime \def (nth_prime n) in let upper_bound \def S previous_prime! in -(S previous_prime) \le min_aux (upper_bound - (S previous_prime)) upper_bound primeb. +(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). +cut (upper_bound - (upper_bound -(S previous_prime)) = (S previous_prime)). rewrite < Hcut in \vdash (? % ?). apply le_min_aux. apply plus_to_minus. @@ -148,12 +148,12 @@ qed. theorem lt_SO_nth_prime_n : \forall n:nat. (S O) \lt nth_prime n. intros. elim n.simplify.apply le_n. -apply trans_lt ? (nth_prime n1). +apply (trans_lt ? (nth_prime n1)). assumption.apply lt_nth_prime_n_nth_prime_Sn. qed. theorem lt_O_nth_prime_n : \forall n:nat. O \lt nth_prime n. -intros.apply trans_lt O (S O). +intros.apply (trans_lt O (S O)). simplify. apply le_n.apply lt_SO_nth_prime_n. qed. @@ -169,10 +169,10 @@ theorem lt_nth_prime_to_not_prime: \forall n,m. nth_prime n < m \to m < nth_prim \to \lnot (prime m). intros. apply primeb_false_to_not_prime. -letin previous_prime \def nth_prime n. -letin upper_bound \def S previous_prime!. -apply lt_min_aux_to_false primeb upper_bound (upper_bound - (S previous_prime)) m. -cut S (nth_prime n)!-(S (nth_prime n)! - (S (nth_prime n))) = (S (nth_prime n)). +letin previous_prime \def (nth_prime n). +letin upper_bound \def (S previous_prime!). +apply (lt_min_aux_to_false primeb upper_bound (upper_bound - (S previous_prime)) m). +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 plus_minus_m_m. @@ -185,14 +185,14 @@ qed. theorem prime_to_nth_prime : \forall p:nat. prime p \to \exists i. nth_prime i = p. intros. -cut \exists m. nth_prime m \le p \land p < nth_prime (S m). +cut (\exists m. nth_prime m \le p \land p < nth_prime (S m)). elim Hcut.elim H1. -cut nth_prime a < p \lor nth_prime a = p. +cut (nth_prime a < p \lor nth_prime a = p). elim Hcut1. absurd (prime p). assumption. -apply lt_nth_prime_to_not_prime a.assumption.assumption. -apply ex_intro nat ? a.assumption. +apply (lt_nth_prime_to_not_prime a).assumption.assumption. +apply (ex_intro nat ? a).assumption. apply le_to_or_lt_eq.assumption. apply ex_m_le_n_nth_prime_m. simplify.simplify in H.elim H.assumption. diff --git a/helm/matita/library/nat/ord.ma b/helm/matita/library/nat/ord.ma index 1992121b6..b982accb3 100644 --- a/helm/matita/library/nat/ord.ma +++ b/helm/matita/library/nat/ord.ma @@ -46,7 +46,7 @@ match n \mod m with | (S a) \Rightarrow pair nat nat O n] ) with [ (pair q r) \Rightarrow n = m \sup q * r ]. -apply nat_case (n \mod m). +apply (nat_case (n \mod m)). simplify.apply plus_n_O. intros. simplify.apply plus_n_O. @@ -59,7 +59,7 @@ match n1 \mod m with | (S a) \Rightarrow pair nat nat O n1] ) with [ (pair q r) \Rightarrow n1 = m \sup q * r]. -apply nat_case1 (n1 \mod m).intro. +apply (nat_case1 (n1 \mod m)).intro. change with match ( match (p_ord_aux n (n1 / m) m) with @@ -67,10 +67,10 @@ match ( with [ (pair q r) \Rightarrow n1 = m \sup q * r]. generalize in match (H (n1 / m) m). -elim p_ord_aux n (n1 / m) m. +elim (p_ord_aux n (n1 / m) m). simplify. rewrite > assoc_times. -rewrite < H3.rewrite > plus_n_O (m*(n1 / m)). +rewrite < H3.rewrite > (plus_n_O (m*(n1 / m))). rewrite < H2. rewrite > sym_times. rewrite < div_mod.reflexivity. @@ -95,63 +95,63 @@ intros 5. elim i. simplify. rewrite < plus_n_O. -apply nat_case p. +apply (nat_case p). change with - match n \mod m with + (match n \mod m with [ O \Rightarrow pair nat nat O n | (S a) \Rightarrow pair nat nat O n] - = pair nat nat O n. + = pair nat nat O n). elim (n \mod m).simplify.reflexivity.simplify.reflexivity. intro. change with - match n \mod m with + (match n \mod m with [ O \Rightarrow match (p_ord_aux m1 (n / m) m) with [ (pair q r) \Rightarrow pair nat nat (S q) r] | (S a) \Rightarrow pair nat nat O n] - = pair nat nat O n. -cut O < n \mod m \lor O = n \mod m. -elim Hcut.apply lt_O_n_elim (n \mod m) H3. + = pair nat nat O n). +cut (O < n \mod m \lor O = n \mod m). +elim Hcut.apply (lt_O_n_elim (n \mod m) H3). intros. simplify.reflexivity. apply False_ind. apply H1.apply sym_eq.assumption. apply le_to_or_lt_eq.apply le_O_n. generalize in match H3. -apply nat_case p.intro.apply False_ind.apply not_le_Sn_O n1 H4. +apply (nat_case p).intro.apply False_ind.apply (not_le_Sn_O n1 H4). intros. change with - match ((m \sup (S n1) *n) \mod m) with + (match ((m \sup (S n1) *n) \mod m) with [ O \Rightarrow match (p_ord_aux m1 ((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 (m \sup (S n1) *n)] - = pair nat nat (S n1) n. -cut ((m \sup (S n1)*n) \mod m) = O. + = pair nat nat (S n1) n). +cut (((m \sup (S n1)*n) \mod m) = O). rewrite > Hcut. change with -match (p_ord_aux m1 ((m \sup (S n1)*n) / m) m) with +(match (p_ord_aux m1 ((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 (m \sup (S n1) *n) / m = m \sup n1 *n. + = pair nat nat (S n1) n). +cut ((m \sup (S n1) *n) / m = m \sup n1 *n). rewrite > Hcut1. -rewrite > H2 m1. simplify.reflexivity. +rewrite > (H2 m1). simplify.reflexivity. apply le_S_S_to_le.assumption. (* div_exp *) -change with (m* m \sup n1 *n) / m = m \sup n1 * n. +change with ((m* m \sup n1 *n) / m = m \sup n1 * n). rewrite > assoc_times. -apply lt_O_n_elim m H. +apply (lt_O_n_elim m H). intro.apply div_times. (* mod_exp = O *) apply divides_to_mod_O. assumption. simplify.rewrite > assoc_times. -apply witness ? ? (m \sup n1 *n).reflexivity. +apply (witness ? ? (m \sup n1 *n)).reflexivity. qed. theorem p_ord_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to match p_ord_aux p n m with [ (pair q r) \Rightarrow r \mod m \neq O]. -intro.elim p.absurd O < n.assumption. +intro.elim p.absurd (O < n).assumption. apply le_to_not_lt.assumption. change with match @@ -162,23 +162,23 @@ match | (S a) \Rightarrow pair nat nat O n1]) with [ (pair q r) \Rightarrow r \mod m \neq O]. -apply nat_case1 (n1 \mod m).intro. +apply (nat_case1 (n1 \mod m)).intro. generalize in match (H (n1 / m) m). elim (p_ord_aux n (n1 / m) m). apply H5.assumption. apply eq_mod_O_to_lt_O_div. -apply trans_lt ? (S O).simplify.apply le_n. +apply (trans_lt ? (S O)).simplify.apply le_n. assumption.assumption.assumption. apply le_S_S_to_le. -apply trans_le ? n1.change with n1 / m < n1. +apply (trans_le ? n1).change with (n1 / m < n1). apply lt_div_n_m_n.assumption.assumption.assumption. intros. -change with n1 \mod m \neq O. +change with (n1 \mod m \neq O). rewrite > H4. (* Andrea: META NOT FOUND !!! rewrite > sym_eq. *) simplify.intro. -apply not_eq_O_S m1. +apply (not_eq_O_S m1). rewrite > H5.reflexivity. qed. diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma index 796567fa5..0ddd4b5c5 100644 --- a/helm/matita/library/nat/orders.ma +++ b/helm/matita/library/nat/orders.ma @@ -94,8 +94,8 @@ simplify.apply le_n_Sn. qed. theorem le_S_S_to_le : \forall n,m:nat. S n \leq S m \to n \leq m. -intros.change with pred (S n) \leq pred (S m). -elim H.apply le_n.apply trans_le ? (pred n1).assumption. +intros.change with (pred (S n) \leq pred (S m)). +elim H.apply le_n.apply (trans_le ? (pred n1)).assumption. apply le_pred_n. qed. @@ -105,11 +105,11 @@ qed. (* not le *) theorem not_le_Sn_O: \forall n:nat. S n \nleq O. -intros.simplify.intros.apply leS_to_not_zero ? ? H. +intros.simplify.intros.apply (leS_to_not_zero ? ? H). qed. theorem not_le_Sn_n: \forall n:nat. S n \nleq n. -intros.elim n.apply not_le_Sn_O.simplify.intros.cut S n1 \leq n1. +intros.elim n.apply not_le_Sn_O.simplify.intros.cut (S n1 \leq n1). apply H.assumption. apply le_S_S_to_le.assumption. qed. @@ -124,7 +124,7 @@ qed. (* not eq *) theorem lt_to_not_eq : \forall n,m:nat. n H7. apply H. diff --git a/helm/matita/library/nat/permutation.ma b/helm/matita/library/nat/permutation.ma index 5d99f657b..cc0f41027 100644 --- a/helm/matita/library/nat/permutation.ma +++ b/helm/matita/library/nat/permutation.ma @@ -50,17 +50,17 @@ permut f (S m) \to f (S m) = (S m) \to permut f m. unfold permut.intros. elim H. split.intros. -cut f i < S m \lor f i = S m. +cut (f i < S m \lor f i = S m). elim Hcut. apply le_S_S_to_le.assumption. apply False_ind. -apply not_le_Sn_n m. -cut (S m) = i. +apply (not_le_Sn_n m). +cut ((S m) = i). rewrite > Hcut1.assumption. apply H3.apply le_n.apply le_S.assumption. rewrite > H5.assumption. apply le_to_or_lt_eq.apply H2.apply le_S.assumption. -apply injn_Sn_n f m H3. +apply (injn_Sn_n f m H3). qed. (* transpositions *) @@ -76,19 +76,19 @@ match eqb n i with lemma transpose_i_j_i: \forall i,j:nat. transpose i j i = j. intros.unfold transpose. -rewrite > eqb_n_n i.simplify. reflexivity. +rewrite > (eqb_n_n i).simplify. reflexivity. qed. lemma transpose_i_j_j: \forall i,j:nat. transpose i j j = i. intros.unfold transpose. -apply eqb_elim j i.simplify.intro.assumption. -rewrite > eqb_n_n j.simplify. +apply (eqb_elim j i).simplify.intro.assumption. +rewrite > (eqb_n_n j).simplify. intros. reflexivity. qed. theorem transpose_i_i: \forall i,n:nat. (transpose i i n) = n. intros.unfold transpose. -apply eqb_elim n i. +apply (eqb_elim n i). intro.simplify.apply sym_eq. assumption. intro.simplify.reflexivity. qed. @@ -96,12 +96,12 @@ qed. theorem transpose_i_j_j_i: \forall i,j,n:nat. transpose i j n = transpose j i n. intros.unfold transpose. -apply eqb_elim n i. -apply eqb_elim n j. +apply (eqb_elim n i). +apply (eqb_elim n j). intros. simplify.rewrite < H. rewrite < H1. reflexivity. intros.simplify.reflexivity. -apply eqb_elim n j. +apply (eqb_elim n j). intros.simplify.reflexivity. intros.simplify.reflexivity. qed. @@ -109,19 +109,19 @@ qed. theorem transpose_transpose: \forall i,j,n:nat. (transpose i j (transpose i j n)) = n. intros.unfold transpose. unfold transpose. -apply eqb_elim n i.simplify. +apply (eqb_elim n i).simplify. intro. -apply eqb_elim j i. +apply (eqb_elim j i). simplify.intros.rewrite > H. rewrite > H1.reflexivity. -rewrite > eqb_n_n j.simplify.intros. +rewrite > (eqb_n_n j).simplify.intros. apply sym_eq. assumption. -apply eqb_elim n j.simplify. -rewrite > eqb_n_n i.intros.simplify. +apply (eqb_elim n j).simplify. +rewrite > (eqb_n_n i).intros.simplify. apply sym_eq. assumption. simplify.intros. -rewrite > not_eq_to_eqb_false n i H1. -rewrite > not_eq_to_eqb_false n j H. +rewrite > (not_eq_to_eqb_false n i H1). +rewrite > (not_eq_to_eqb_false n j H). simplify.reflexivity. qed. @@ -129,8 +129,8 @@ theorem injective_transpose : \forall i,j:nat. injective nat nat (transpose i j). unfold injective. intros. -rewrite < transpose_transpose i j x. -rewrite < transpose_transpose i j y. +rewrite < (transpose_transpose i j x). +rewrite < (transpose_transpose i j y). apply eq_f.assumption. qed. @@ -143,10 +143,10 @@ permut (transpose i j) n. unfold permut.intros. split.unfold transpose. intros. -elim eqb i1 i.simplify.assumption. -elim eqb i1 j.simplify.assumption. +elim (eqb i1 i).simplify.assumption. +elim (eqb i1 j).simplify.assumption. simplify.assumption. -apply injective_to_injn (transpose i j) n. +apply (injective_to_injn (transpose i j) n). apply injective_transpose. qed. @@ -165,7 +165,7 @@ qed. theorem permut_transpose_l: \forall f:nat \to nat. \forall m,i,j:nat. i \le m \to j \le m \to permut f m \to permut (\lambda n.transpose i j (f n)) m. -intros.apply permut_fg (transpose i j) f m ? ?. +intros.apply (permut_fg (transpose i j) f m ? ?). apply permut_transpose.assumption.assumption. assumption. qed. @@ -173,7 +173,7 @@ qed. theorem permut_transpose_r: \forall f:nat \to nat. \forall m,i,j:nat. i \le m \to j \le m \to permut f m \to permut (\lambda n.f (transpose i j n)) m. -intros.apply permut_fg f (transpose i j) m ? ?. +intros.apply (permut_fg f (transpose i j) m ? ?). assumption.apply permut_transpose.assumption.assumption. qed. @@ -182,41 +182,41 @@ theorem eq_transpose : \forall i,j,k,n:nat. \lnot j=i \to transpose i j n = transpose i k (transpose k j (transpose i k n)). (* uffa: triplo unfold? *) intros.unfold transpose.unfold transpose.unfold transpose. -apply eqb_elim n i.intro. -simplify.rewrite > eqb_n_n k. -simplify.rewrite > not_eq_to_eqb_false j i H. -rewrite > not_eq_to_eqb_false j k H2. +apply (eqb_elim n i).intro. +simplify.rewrite > (eqb_n_n k). +simplify.rewrite > (not_eq_to_eqb_false j i H). +rewrite > (not_eq_to_eqb_false j k H2). reflexivity. -intro.apply eqb_elim n j. +intro.apply (eqb_elim n j). intro. -cut \lnot n = k. -cut \lnot n = i. -rewrite > not_eq_to_eqb_false n k Hcut. +cut (\lnot n = k). +cut (\lnot n = i). +rewrite > (not_eq_to_eqb_false n k Hcut). simplify. -rewrite > not_eq_to_eqb_false n k Hcut. -rewrite > eq_to_eqb_true n j H4. +rewrite > (not_eq_to_eqb_false n k Hcut). +rewrite > (eq_to_eqb_true n j H4). simplify. -rewrite > not_eq_to_eqb_false k i. -rewrite > eqb_n_n k. +rewrite > (not_eq_to_eqb_false k i). +rewrite > (eqb_n_n k). simplify.reflexivity. simplify.intro.apply H1.apply sym_eq.assumption. assumption. -simplify.intro.apply H2.apply trans_eq ? ? n. +simplify.intro.apply H2.apply (trans_eq ? ? n). apply sym_eq.assumption.assumption. -intro.apply eqb_elim n k.intro. +intro.apply (eqb_elim n k).intro. simplify. -rewrite > not_eq_to_eqb_false i k H1. -rewrite > not_eq_to_eqb_false i j. +rewrite > (not_eq_to_eqb_false i k H1). +rewrite > (not_eq_to_eqb_false i j). simplify. -rewrite > eqb_n_n i. +rewrite > (eqb_n_n i). simplify.assumption. simplify.intro.apply H.apply sym_eq.assumption. intro.simplify. -rewrite > not_eq_to_eqb_false n k H5. -rewrite > not_eq_to_eqb_false n j H4. +rewrite > (not_eq_to_eqb_false n k H5). +rewrite > (not_eq_to_eqb_false n j H4). simplify. -rewrite > not_eq_to_eqb_false n i H3. -rewrite > not_eq_to_eqb_false n k H5. +rewrite > (not_eq_to_eqb_false n i H3). +rewrite > (not_eq_to_eqb_false n k H5). simplify.reflexivity. qed. @@ -226,27 +226,27 @@ theorem permut_S_to_permut_transpose: \forall f:nat \to nat. unfold permut.intros. elim H. split.intros.simplify. -apply eqb_elim (f i) (f (S m)).simplify. +apply (eqb_elim (f i) (f (S m))). intro.apply False_ind. -cut i = (S m). -apply not_le_Sn_n m. +cut (i = (S m)). +apply (not_le_Sn_n m). rewrite < Hcut.assumption. apply H2.apply le_S.assumption.apply le_n.assumption. intro.simplify. -apply eqb_elim (f i) (S m).simplify. +apply (eqb_elim (f i) (S m)). intro. -cut f (S m) \lt (S m) \lor f (S m) = (S m). +cut (f (S m) \lt (S m) \lor f (S m) = (S m)). elim Hcut.apply le_S_S_to_le.assumption. apply False_ind.apply H4.rewrite > H6.assumption. apply le_to_or_lt_eq.apply H1.apply le_n. intro.simplify. -cut f i \lt (S m) \lor f i = (S m). +cut (f i \lt (S m) \lor f i = (S m)). elim Hcut.apply le_S_S_to_le.assumption. apply False_ind.apply H5.assumption. apply le_to_or_lt_eq.apply H1.apply le_S.assumption. unfold injn.intros. apply H2.apply le_S.assumption.apply le_S.assumption. -apply inj_transpose (f (S m)) (S m). +apply (inj_transpose (f (S m)) (S m)). apply H5. qed. @@ -260,21 +260,21 @@ theorem eq_to_bijn: \forall f,g:nat\to nat. \forall n:nat. (\forall i:nat. i \le n \to (f i) = (g i)) \to bijn f n \to bijn g n. intros 4.unfold bijn. -intros.elim H1 m. -apply ex_intro ? ? a. -rewrite < H a.assumption. +intros.elim (H1 m). +apply (ex_intro ? ? a). +rewrite < (H a).assumption. elim H3.assumption.assumption. qed. theorem bijn_Sn_n: \forall f:nat \to nat. \forall n:nat. bijn f (S n) \to f (S n) = (S n) \to bijn f n. -unfold bijn.intros.elim H m. +unfold bijn.intros.elim (H m). elim H3. -apply ex_intro ? ? a.split. -cut a < S n \lor a = S n. +apply (ex_intro ? ? a).split. +cut (a < S n \lor a = S n). elim Hcut.apply le_S_S_to_le.assumption. apply False_ind. -apply not_le_Sn_n n. +apply (not_le_Sn_n n). rewrite < H1.rewrite < H6.rewrite > H5.assumption. apply le_to_or_lt_eq.assumption.assumption. apply le_S.assumption. @@ -283,14 +283,14 @@ qed. theorem bijn_n_Sn: \forall f:nat \to nat. \forall n:nat. bijn f n \to f (S n) = (S n) \to bijn f (S n). unfold bijn.intros. -cut m < S n \lor m = S n. +cut (m < S n \lor m = S n). elim Hcut. -elim H m. +elim (H m). elim H4. -apply ex_intro ? ? a.split. +apply (ex_intro ? ? a).split. apply le_S.assumption.assumption. apply le_S_S_to_le.assumption. -apply ex_intro ? ? (S n). +apply (ex_intro ? ? (S n)). split.apply le_n. rewrite > H3.assumption. apply le_to_or_lt_eq.assumption. @@ -300,9 +300,9 @@ theorem bijn_fg: \forall f,g:nat\to nat. \forall n:nat. bijn f n \to bijn g n \to bijn (\lambda p.f(g p)) n. unfold bijn. intros.simplify. -elim H m.elim H3. -elim H1 a.elim H6. -apply ex_intro ? ? a1. +elim (H m).elim H3. +elim (H1 a).elim H6. +apply (ex_intro ? ? a1). split.assumption. rewrite > H8.assumption. assumption.assumption. @@ -311,60 +311,59 @@ qed. theorem bijn_transpose : \forall n,i,j. i \le n \to j \le n \to bijn (transpose i j) n. intros.simplify.intros. -cut m = i \lor \lnot m = i. +cut (m = i \lor \lnot m = i). elim Hcut. -apply ex_intro ? ? j. +apply (ex_intro ? ? j). split.assumption. -apply eqb_elim j i. +apply (eqb_elim j i). intro.simplify.rewrite > H3.rewrite > H4.reflexivity. -rewrite > eqb_n_n j.simplify. +rewrite > (eqb_n_n j).simplify. intros. apply sym_eq.assumption. -cut m = j \lor \lnot m = j. +cut (m = j \lor \lnot m = j). elim Hcut1. -apply ex_intro ? ? i. +apply (ex_intro ? ? i). split.assumption. -rewrite > eqb_n_n i.simplify. +rewrite > (eqb_n_n i).simplify. apply sym_eq. assumption. -apply ex_intro ? ? m. +apply (ex_intro ? ? m). split.assumption. -rewrite > not_eq_to_eqb_false m i. -rewrite > not_eq_to_eqb_false m j. +rewrite > (not_eq_to_eqb_false m i). +rewrite > (not_eq_to_eqb_false m j). simplify. reflexivity. assumption. assumption. -apply decidable_eq_nat m j. -apply decidable_eq_nat m i. +apply (decidable_eq_nat m j). +apply (decidable_eq_nat m i). qed. theorem bijn_transpose_r: \forall f:nat\to nat.\forall n,i,j. i \le n \to j \le n \to bijn f n \to bijn (\lambda p.f (transpose i j p)) n. intros. -apply bijn_fg f ?.assumption. -apply bijn_transpose n i j.assumption.assumption. +apply (bijn_fg f ?).assumption. +apply (bijn_transpose n i j).assumption.assumption. qed. theorem bijn_transpose_l: \forall f:nat\to nat.\forall n,i,j. i \le n \to j \le n \to bijn f n \to bijn (\lambda p.transpose i j (f p)) n. intros. -apply bijn_fg ? f. -apply bijn_transpose n i j.assumption.assumption. +apply (bijn_fg ? f). +apply (bijn_transpose n i j).assumption.assumption. assumption. qed. - theorem permut_to_bijn: \forall n:nat.\forall f:nat\to nat. permut f n \to bijn f n. intro. elim n.simplify.intros. -apply ex_intro ? ? m. +apply (ex_intro ? ? m). split.assumption. -apply le_n_O_elim m ? (\lambda p. f p = p). +apply (le_n_O_elim m ? (\lambda p. f p = p)). assumption.unfold permut in H. elim H.apply sym_eq. apply le_n_O_to_eq.apply H2.apply le_n. -apply eq_to_bijn (\lambda p. -(transpose (f (S n1)) (S n1)) (transpose (f (S n1)) (S n1) (f p))) f. +apply (eq_to_bijn (\lambda p. +(transpose (f (S n1)) (S n1)) (transpose (f (S n1)) (S n1) (f p))) f). intros.apply transpose_transpose. -apply bijn_fg (transpose (f (S n1)) (S n1)). +apply (bijn_fg (transpose (f (S n1)) (S n1))). apply bijn_transpose. unfold permut in H1. elim H1.apply H2.apply le_n.apply le_n. @@ -372,7 +371,7 @@ apply bijn_n_Sn. apply H. apply permut_S_to_permut_transpose. assumption.simplify. -rewrite > eqb_n_n (f (S n1)).simplify.reflexivity. +rewrite > (eqb_n_n (f (S n1))).simplify.reflexivity. qed. let rec invert_permut n f m \def @@ -387,36 +386,36 @@ theorem invert_permut_f: \forall f:nat \to nat. \forall n,m:nat. m \le n \to injn f n\to invert_permut n f (f m) = m. intros 4. elim H. -apply nat_case1 m. +apply (nat_case1 m). intro.simplify. -rewrite > eqb_n_n (f O).simplify.reflexivity. +rewrite > (eqb_n_n (f O)).simplify.reflexivity. intros.simplify. -rewrite > eqb_n_n (f (S m1)).simplify.reflexivity. +rewrite > (eqb_n_n (f (S m1))).simplify.reflexivity. simplify. -rewrite > not_eq_to_eqb_false (f m) (f (S n1)). +rewrite > (not_eq_to_eqb_false (f m) (f (S n1))). simplify.apply H2. apply injn_Sn_n. assumption. -simplify.intro.absurd m = S n1. +simplify.intro.absurd (m = S n1). apply H3.apply le_S.assumption.apply le_n.assumption. simplify.intro. -apply not_le_Sn_n n1.rewrite < H5.assumption. +apply (not_le_Sn_n n1).rewrite < H5.assumption. qed. theorem injective_invert_permut: \forall f:nat \to nat. \forall n:nat. permut f n \to injn (invert_permut n f) n. intros. unfold injn.intros. -cut bijn f n. +cut (bijn f n). unfold bijn in Hcut. -generalize in match Hcut i H1.intro. -generalize in match Hcut j H2.intro. +generalize in match (Hcut i H1).intro. +generalize in match (Hcut j H2).intro. elim H4.elim H6. elim H5.elim H9. rewrite < H8. rewrite < H11. apply eq_f. -rewrite < invert_permut_f f n a. -rewrite < invert_permut_f f n a1. +rewrite < (invert_permut_f f n a). +rewrite < (invert_permut_f f n a1). rewrite > H8. rewrite > H11. assumption.assumption. @@ -430,8 +429,8 @@ theorem permut_invert_permut: \forall f:nat \to nat. \forall n:nat. permut f n \to permut (invert_permut n f) n. intros.unfold permut.split. intros.simplify.elim n. -simplify.elim eqb i (f O).simplify.apply le_n.simplify.apply le_n. -simplify.elim eqb i (f (S n1)).simplify.apply le_n. +simplify.elim (eqb i (f O)).simplify.apply le_n.simplify.apply le_n. +simplify.elim (eqb i (f (S n1))).simplify.apply le_n. simplify.apply le_S. assumption. apply injective_invert_permut.assumption. qed. @@ -439,16 +438,16 @@ qed. theorem f_invert_permut: \forall f:nat \to nat. \forall n,m:nat. m \le n \to permut f n\to f (invert_permut n f m) = m. intros. -apply injective_invert_permut f n H1. +apply (injective_invert_permut f n H1). unfold permut in H1.elim H1. apply H2. -cut permut (invert_permut n f) n.unfold permut in Hcut. +cut (permut (invert_permut n f) n).unfold permut in Hcut. elim Hcut.apply H4.assumption. apply permut_invert_permut.assumption.assumption. (* uffa: lo ha espanso troppo *) -change with invert_permut n f (f (invert_permut n f m)) = invert_permut n f m. +change with (invert_permut n f (f (invert_permut n f m)) = invert_permut n f m). apply invert_permut_f. -cut permut (invert_permut n f) n.unfold permut in Hcut. +cut (permut (invert_permut n f) n).unfold permut in Hcut. elim Hcut.apply H2.assumption. apply permut_invert_permut.assumption. unfold permut in H1.elim H1.assumption. @@ -457,16 +456,16 @@ qed. theorem permut_n_to_eq_n: \forall h:nat \to nat.\forall n:nat. permut h n \to (\forall m:nat. m < n \to h m = m) \to h n = n. intros.unfold permut in H.elim H. -cut invert_permut n h n < n \lor invert_permut n h n = n. +cut (invert_permut n h n < n \lor invert_permut n h n = n). elim Hcut. -rewrite < f_invert_permut h n n in \vdash (? ? ? %). +rewrite < (f_invert_permut h n n) in \vdash (? ? ? %). apply eq_f. -rewrite < f_invert_permut h n n in \vdash (? ? % ?). +rewrite < (f_invert_permut h n n) in \vdash (? ? % ?). apply H1.assumption.apply le_n.assumption.apply le_n.assumption. rewrite < H4 in \vdash (? ? % ?). -apply f_invert_permut h.apply le_n.assumption. +apply (f_invert_permut h).apply le_n.assumption. apply le_to_or_lt_eq. -cut permut (invert_permut n h) n. +cut (permut (invert_permut n h) n). unfold permut in Hcut.elim Hcut. apply H4.apply le_n. apply permut_invert_permut.assumption. @@ -476,14 +475,14 @@ theorem permut_n_to_le: \forall h:nat \to nat.\forall k,n:nat. k \le n \to permut h n \to (\forall m:nat. m < k \to h m = m) \to \forall j. k \le j \to j \le n \to k \le h j. intros.unfold permut in H1.elim H1. -cut h j < k \lor \not(h j < k). -elim Hcut.absurd k \le j.assumption. +cut (h j < k \lor \not(h j < k)). +elim Hcut.absurd (k \le j).assumption. apply lt_to_not_le. -cut h j = j.rewrite < Hcut1.assumption. +cut (h j = j).rewrite < Hcut1.assumption. apply H6.apply H5.assumption.assumption. apply H2.assumption. apply not_lt_to_le.assumption. -apply decidable_lt (h j) k. +apply (decidable_lt (h j) k). qed. (* applications *) @@ -524,7 +523,7 @@ map_iter_i n (\lambda m.m) times (S O) = (S n)!. intros.elim n. simplify.reflexivity. change with -((S n1)+(S O))*(map_iter_i n1 (\lambda m.m) times (S O)) = (S(S n1))*(S n1)!. +(((S n1)+(S O))*(map_iter_i n1 (\lambda m.m) times (S O)) = (S(S n1))*(S n1)!). rewrite < plus_n_Sm.rewrite < plus_n_O. apply eq_f.assumption. qed. @@ -532,65 +531,65 @@ qed. theorem eq_map_iter_i_transpose_l : \forall f:nat\to nat \to nat.associative nat f \to symmetric2 nat nat f \to \forall g:nat \to nat. \forall n,k:nat. map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose (k+n) (S k+n) m)) f n. -intros.apply nat_case1 k. +intros.apply (nat_case1 k). intros.simplify. change with -f (g (S n)) (g n) = -f (g (transpose n (S n) (S n))) (g (transpose n (S n) n)). +(f (g (S n)) (g n) = +f (g (transpose n (S n) (S n))) (g (transpose n (S n) n))). rewrite > transpose_i_j_i. rewrite > transpose_i_j_j. apply H1. intros. change with -f (g (S (S (m+n)))) (f (g (S (m+n))) (map_iter_i m g f n)) = +(f (g (S (S (m+n)))) (f (g (S (m+n))) (map_iter_i m g f n)) = f (g (transpose (S m + n) (S (S m) + n) (S (S m)+n))) (f (g (transpose (S m + n) (S (S m) + n) (S m+n))) -(map_iter_i m (\lambda m1. g (transpose (S m+n) (S (S m)+n) m1)) f n)). +(map_iter_i m (\lambda m1. g (transpose (S m+n) (S (S m)+n) m1)) f n))). rewrite > transpose_i_j_i. rewrite > transpose_i_j_j. rewrite < H. rewrite < H. -rewrite < H1 (g (S m + n)). +rewrite < (H1 (g (S m + n))). apply eq_f. apply eq_map_iter_i. intros.unfold transpose. -rewrite > not_eq_to_eqb_false m1 (S m+n). -rewrite > not_eq_to_eqb_false m1 (S (S m)+n). +rewrite > (not_eq_to_eqb_false m1 (S m+n)). +rewrite > (not_eq_to_eqb_false m1 (S (S m)+n)). simplify. reflexivity. -apply lt_to_not_eq m1 (S (S m)+n). +apply (lt_to_not_eq m1 (S (S m)+n)). simplify.apply le_S_S.apply le_S.assumption. -apply lt_to_not_eq m1 (S m+n). +apply (lt_to_not_eq m1 (S m+n)). simplify.apply le_S_S.assumption. qed. theorem eq_map_iter_i_transpose_i_Si : \forall f:nat\to nat \to nat.associative nat f \to symmetric2 nat nat f \to \forall g:nat \to nat. \forall n,k,i:nat. n \le i \to i \le k+n \to map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i (S i) m)) f n. -intros 6.elim k.cut i=n. +intros 6.elim k.cut (i=n). rewrite > Hcut. -apply eq_map_iter_i_transpose_l f H H1 g n O. +apply (eq_map_iter_i_transpose_l f H H1 g n O). apply antisymmetric_le.assumption.assumption. -cut i < S n1 + n \lor i = S n1 + n. +cut (i < S n1 + n \lor i = S n1 + n). elim Hcut. change with -f (g (S (S n1)+n)) (map_iter_i (S n1) g f n) = -f (g (transpose i (S i) (S (S n1)+n))) (map_iter_i (S n1) (\lambda m. g (transpose i (S i) m)) f n). +(f (g (S (S n1)+n)) (map_iter_i (S n1) g f n) = +f (g (transpose i (S i) (S (S n1)+n))) (map_iter_i (S n1) (\lambda m. g (transpose i (S i) m)) f n)). apply eq_f2.unfold transpose. -rewrite > not_eq_to_eqb_false (S (S n1)+n) i. -rewrite > not_eq_to_eqb_false (S (S n1)+n) (S i). +rewrite > (not_eq_to_eqb_false (S (S n1)+n) i). +rewrite > (not_eq_to_eqb_false (S (S n1)+n) (S i)). simplify.reflexivity. simplify.intro. -apply lt_to_not_eq i (S n1+n).assumption. +apply (lt_to_not_eq i (S n1+n)).assumption. apply inj_S.apply sym_eq. assumption. simplify.intro. -apply lt_to_not_eq i (S (S n1+n)).simplify. +apply (lt_to_not_eq i (S (S n1+n))).simplify. apply le_S_S.assumption. apply sym_eq. assumption. apply H2.assumption.apply le_S_S_to_le. assumption. rewrite > H5. -apply eq_map_iter_i_transpose_l f H H1 g n (S n1). +apply (eq_map_iter_i_transpose_l f H H1 g n (S n1)). apply le_to_or_lt_eq.assumption. qed. @@ -600,48 +599,48 @@ associative nat f \to symmetric2 nat nat f \to \forall n,k,o:nat. \forall g:nat \to nat. \forall i:nat. n \le i \to S (o + i) \le S k+n \to map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i (S(o + i)) m)) f n. intros 6. -apply nat_elim1 o. +apply (nat_elim1 o). intro. -apply nat_case m ?. +apply (nat_case m ?). intros. -apply eq_map_iter_i_transpose_i_Si ? H H1. +apply (eq_map_iter_i_transpose_i_Si ? H H1). exact H3.apply le_S_S_to_le.assumption. intros. -apply trans_eq ? ? (map_iter_i (S k) (\lambda m. g (transpose i (S(m1 + i)) m)) f n). +apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g (transpose i (S(m1 + i)) m)) f n)). apply H2. simplify. apply le_n.assumption. -apply trans_le ? (S(S (m1+i))). +apply (trans_le ? (S(S (m1+i)))). apply le_S.apply le_n.assumption. -apply trans_eq ? ? (map_iter_i (S k) (\lambda m. g -(transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m))) f n). -apply H2 O ? ? (S(m1+i)). +apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g +(transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m))) f n)). +apply (H2 O ? ? (S(m1+i))). simplify.apply le_S_S.apply le_O_n. -apply trans_le ? i.assumption. -change with i \le (S m1)+i.apply le_plus_n. +apply (trans_le ? i).assumption. +change with (i \le (S m1)+i).apply le_plus_n. exact H4. -apply trans_eq ? ? (map_iter_i (S k) (\lambda m. g +apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g (transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) -(transpose i (S(m1 + i)) m)))) f n). -apply H2 m1. +(transpose i (S(m1 + i)) m)))) f n)). +apply (H2 m1). simplify. apply le_n.assumption. -apply trans_le ? (S(S (m1+i))). +apply (trans_le ? (S(S (m1+i)))). apply le_S.apply le_n.assumption. apply eq_map_iter_i. intros.apply eq_f. apply sym_eq. apply eq_transpose. simplify. intro. -apply not_le_Sn_n i. +apply (not_le_Sn_n i). rewrite < H7 in \vdash (? ? %). apply le_S_S.apply le_S. apply le_plus_n. simplify. intro. -apply not_le_Sn_n i. +apply (not_le_Sn_n i). rewrite > H7 in \vdash (? ? %). apply le_S_S. apply le_plus_n. simplify. intro. -apply not_eq_n_Sn (S m1+i). +apply (not_eq_n_Sn (S m1+i)). apply sym_eq.assumption. qed. @@ -651,20 +650,20 @@ symmetric2 nat nat f \to \forall n,k,i,j:nat. map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i j m)) f n. intros. simplify in H3. -cut (S i) < j \lor (S i) = j. +cut ((S i) < j \lor (S i) = j). elim Hcut. -cut j = S ((j - (S i)) + i). +cut (j = S ((j - (S i)) + i)). rewrite > Hcut1. -apply eq_map_iter_i_transpose f H H1 n k (j - (S i)) g i. +apply (eq_map_iter_i_transpose f H H1 n k (j - (S i)) g i). assumption. rewrite < Hcut1.assumption. rewrite > plus_n_Sm. apply plus_minus_m_m.apply lt_to_le.assumption. rewrite < H5. -apply eq_map_iter_i_transpose_i_Si f H H1 g. +apply (eq_map_iter_i_transpose_i_Si f H H1 g). simplify. assumption.apply le_S_S_to_le. -apply trans_le ? j.assumption.assumption. +apply (trans_le ? j).assumption.assumption. apply le_to_or_lt_eq.assumption. qed. @@ -673,14 +672,14 @@ symmetric2 nat nat f \to \forall n,k,i,j:nat. \forall g:nat \to nat. n \le i \to i \le (S k+n) \to n \le j \to j \le (S k+n) \to map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i j m)) f n. intros. -apply nat_compare_elim i j. -intro.apply eq_map_iter_i_transpose1 f H H1 n k i j g H2 H6 H5. +apply (nat_compare_elim i j). +intro.apply (eq_map_iter_i_transpose1 f H H1 n k i j g H2 H6 H5). intro.rewrite > H6. apply eq_map_iter_i.intros. -rewrite > transpose_i_i j.reflexivity. +rewrite > (transpose_i_i j).reflexivity. intro. -apply trans_eq ? ? (map_iter_i (S k) (\lambda m:nat.g (transpose j i m)) f n). -apply eq_map_iter_i_transpose1 f H H1 n k j i g H4 H6 H3. +apply (trans_eq ? ? (map_iter_i (S k) (\lambda m:nat.g (transpose j i m)) f n)). +apply (eq_map_iter_i_transpose1 f H H1 n k j i g H4 H6 H3). apply eq_map_iter_i. intros.apply eq_f.apply transpose_i_j_j_i. qed. @@ -690,19 +689,19 @@ symmetric2 nat nat f \to \forall k,n:nat.\forall g,h:nat \to nat. permut h (k+n) \to (\forall m:nat. m \lt n \to h m = m) \to map_iter_i k g f n = map_iter_i k (\lambda m.g(h m)) f n. intros 4.elim k. -simplify.rewrite > permut_n_to_eq_n h.reflexivity.assumption.assumption. -apply trans_eq ? ? (map_iter_i (S n) (\lambda m.g ((transpose (h (S n+n1)) (S n+n1)) m)) f n1). +simplify.rewrite > (permut_n_to_eq_n h).reflexivity.assumption.assumption. +apply (trans_eq ? ? (map_iter_i (S n) (\lambda m.g ((transpose (h (S n+n1)) (S n+n1)) m)) f n1)). unfold permut in H3. elim H3. -apply eq_map_iter_i_transpose2 f H H1 n1 n ? ? g. -apply permut_n_to_le h n1 (S n+n1). +apply (eq_map_iter_i_transpose2 f H H1 n1 n ? ? g). +apply (permut_n_to_le h n1 (S n+n1)). apply le_plus_n.assumption.assumption.apply le_plus_n.apply le_n. apply H5.apply le_n.apply le_plus_n.apply le_n. -apply trans_eq ? ? (map_iter_i (S n) (\lambda m. +apply (trans_eq ? ? (map_iter_i (S n) (\lambda m. (g(transpose (h (S n+n1)) (S n+n1) -(transpose (h (S n+n1)) (S n+n1) (h m)))) )f n1). +(transpose (h (S n+n1)) (S n+n1) (h m)))) )f n1)). change with -f (g (transpose (h (S n+n1)) (S n+n1) (S n+n1))) +(f (g (transpose (h (S n+n1)) (S n+n1) (S n+n1))) (map_iter_i n (\lambda m. g (transpose (h (S n+n1)) (S n+n1) m)) f n1) = @@ -712,31 +711,30 @@ f (map_iter_i n (\lambda m. (g(transpose (h (S n+n1)) (S n+n1) -(transpose (h (S n+n1)) (S n+n1) (h m))))) f n1). +(transpose (h (S n+n1)) (S n+n1) (h m))))) f n1)). apply eq_f2.apply eq_f. rewrite > transpose_i_j_j. rewrite > transpose_i_j_i. rewrite > transpose_i_j_j.reflexivity. -apply H2 n1 (\lambda m.(g(transpose (h (S n+n1)) (S n+n1) m))). +apply (H2 n1 (\lambda m.(g(transpose (h (S n+n1)) (S n+n1) m)))). apply permut_S_to_permut_transpose. assumption. intros. unfold transpose. -rewrite > not_eq_to_eqb_false (h m) (h (S n+n1)). -rewrite > not_eq_to_eqb_false (h m) (S n+n1). +rewrite > (not_eq_to_eqb_false (h m) (h (S n+n1))). +rewrite > (not_eq_to_eqb_false (h m) (S n+n1)). simplify.apply H4.assumption. rewrite > H4. -apply lt_to_not_eq.apply trans_lt ? n1.assumption. +apply lt_to_not_eq.apply (trans_lt ? n1).assumption. simplify.apply le_S_S.apply le_plus_n.assumption. unfold permut in H3.elim H3. simplify.intro. -apply lt_to_not_eq m (S n+n1).apply trans_lt ? n1.assumption. +apply (lt_to_not_eq m (S n+n1)).apply (trans_lt ? n1).assumption. simplify.apply le_S_S.apply le_plus_n. unfold injn in H7. -apply H7 m (S n+n1).apply trans_le ? n1. +apply (H7 m (S n+n1)).apply (trans_le ? n1). apply lt_to_le.assumption.apply le_plus_n.apply le_n. assumption. apply eq_map_iter_i.intros. rewrite > transpose_transpose.reflexivity. -qed. - +qed. \ No newline at end of file diff --git a/helm/matita/library/nat/plus.ma b/helm/matita/library/nat/plus.ma index 79640b136..8043d9a52 100644 --- a/helm/matita/library/nat/plus.ma +++ b/helm/matita/library/nat/plus.ma @@ -62,9 +62,9 @@ theorem inj_plus_r: \forall p,n,m:nat. p+n = p+m \to n=m theorem injective_plus_l: \forall m:nat.injective nat nat (\lambda n.n+m). intro.simplify.intros. -apply injective_plus_r m. +apply (injective_plus_r m). rewrite < sym_plus. -rewrite < sym_plus y. +rewrite < (sym_plus y). assumption. qed. diff --git a/helm/matita/library/nat/primes.ma b/helm/matita/library/nat/primes.ma index 691356243..74fd74e74 100644 --- a/helm/matita/library/nat/primes.ma +++ b/helm/matita/library/nat/primes.ma @@ -29,14 +29,14 @@ interpretation "not divides" 'ndivides n m = theorem reflexive_divides : reflexive nat divides. simplify. intros. -exact witness x x (S O) (times_n_SO x). +exact (witness x x (S O) (times_n_SO x)). qed. theorem divides_to_div_mod_spec : \forall n,m. O < n \to n \divides m \to div_mod_spec m n (m / n) O. intros.elim H1.rewrite > H2. constructor 1.assumption. -apply lt_O_n_elim n H.intros. +apply (lt_O_n_elim n H).intros. rewrite < plus_n_O. rewrite > div_times.apply sym_times. qed. @@ -44,14 +44,14 @@ qed. theorem div_mod_spec_to_divides : \forall n,m,p. div_mod_spec m n p O \to n \divides m. intros.elim H. -apply witness n m p. +apply (witness n m p). rewrite < sym_times. -rewrite > plus_n_O (p*n).assumption. +rewrite > (plus_n_O (p*n)).assumption. qed. theorem divides_to_mod_O: \forall n,m. O < n \to n \divides m \to (m \mod n) = O. -intros.apply div_mod_spec_to_eq2 m n (m / n) (m \mod n) (m / n) O. +intros.apply (div_mod_spec_to_eq2 m n (m / n) (m \mod n) (m / n) O). apply div_mod_spec_div_mod.assumption. apply divides_to_div_mod_spec.assumption.assumption. qed. @@ -59,8 +59,8 @@ qed. theorem mod_O_to_divides: \forall n,m. O< n \to (m \mod n) = O \to n \divides m. intros. -apply witness n m (m / n). -rewrite > plus_n_O (n * (m / n)). +apply (witness n m (m / n)). +rewrite > (plus_n_O (n * (m / n))). rewrite < H1. rewrite < sym_times. (* Andrea: perche' hint non lo trova ?*) @@ -69,50 +69,50 @@ assumption. qed. theorem divides_n_O: \forall n:nat. n \divides O. -intro. apply witness n O O.apply times_n_O. +intro. apply (witness n O O).apply times_n_O. qed. theorem divides_n_n: \forall n:nat. n \divides n. -intro. apply witness n n (S O).apply times_n_SO. +intro. apply (witness n n (S O)).apply times_n_SO. qed. theorem divides_SO_n: \forall n:nat. (S O) \divides n. -intro. apply witness (S O) n n. simplify.apply plus_n_O. +intro. apply (witness (S O) n n). simplify.apply plus_n_O. qed. theorem divides_plus: \forall n,p,q:nat. n \divides p \to n \divides q \to n \divides p+q. intros. -elim H.elim H1. apply witness n (p+q) (n2+n1). +elim H.elim H1. apply (witness n (p+q) (n2+n1)). rewrite > H2.rewrite > H3.apply sym_eq.apply distr_times_plus. qed. theorem divides_minus: \forall n,p,q:nat. divides n p \to divides n q \to divides n (p-q). intros. -elim H.elim H1. apply witness n (p-q) (n2-n1). +elim H.elim H1. apply (witness n (p-q) (n2-n1)). rewrite > H2.rewrite > H3.apply sym_eq.apply distr_times_minus. qed. theorem divides_times: \forall n,m,p,q:nat. n \divides p \to m \divides q \to n*m \divides p*q. intros. -elim H.elim H1. apply witness (n*m) (p*q) (n2*n1). +elim H.elim H1. apply (witness (n*m) (p*q) (n2*n1)). rewrite > H2.rewrite > H3. -apply trans_eq nat ? (n*(m*(n2*n1))). -apply trans_eq nat ? (n*(n2*(m*n1))). +apply (trans_eq nat ? (n*(m*(n2*n1)))). +apply (trans_eq nat ? (n*(n2*(m*n1)))). apply assoc_times. apply eq_f. -apply trans_eq nat ? ((n2*m)*n1). +apply (trans_eq nat ? ((n2*m)*n1)). apply sym_eq. apply assoc_times. -rewrite > sym_times n2 m.apply assoc_times. +rewrite > (sym_times n2 m).apply assoc_times. apply sym_eq. apply assoc_times. qed. theorem transitive_divides: transitive ? divides. unfold. intros. -elim H.elim H1. apply witness x z (n2*n). +elim H.elim H1. apply (witness x z (n2*n)). rewrite > H3.rewrite > H2. apply assoc_times. qed. @@ -123,19 +123,19 @@ variant trans_divides: \forall n,m,p. theorem eq_mod_to_divides:\forall n,m,p. O< p \to mod n p = mod m p \to divides p (n-m). intros. -cut n \le m \or \not n \le m. +cut (n \le m \or \not n \le m). elim Hcut. -cut n-m=O. +cut (n-m=O). rewrite > Hcut1. -apply witness p O O. +apply (witness p O O). apply times_n_O. apply eq_minus_n_m_O. assumption. -apply witness p (n-m) ((div n p)-(div m p)). +apply (witness p (n-m) ((div n p)-(div m p))). rewrite > distr_times_minus. rewrite > sym_times. -rewrite > sym_times p. -cut (div n p)*p = n - (mod n p). +rewrite > (sym_times p). +cut ((div n p)*p = n - (mod n p)). rewrite > Hcut1. rewrite > eq_minus_minus_minus_plus. rewrite > sym_plus. @@ -147,30 +147,30 @@ apply plus_to_minus. rewrite > sym_plus. apply div_mod. assumption. -apply decidable_le n m. +apply (decidable_le n m). qed. (* divides le *) theorem divides_to_le : \forall n,m. O < m \to n \divides m \to n \le m. -intros. elim H1.rewrite > H2.cut O < n2. -apply lt_O_n_elim n2 Hcut.intro.rewrite < sym_times. +intros. elim H1.rewrite > H2.cut (O < n2). +apply (lt_O_n_elim n2 Hcut).intro.rewrite < sym_times. simplify.rewrite < sym_plus. apply le_plus_n. -elim le_to_or_lt_eq O n2. +elim (le_to_or_lt_eq O n2). assumption. -absurd O H2.rewrite < H3.rewrite < times_n_O. -apply not_le_Sn_n O. +apply (not_le_Sn_n O). apply le_O_n. qed. theorem divides_to_lt_O : \forall n,m. O < m \to n \divides m \to O < n. intros.elim H1. -elim le_to_or_lt_eq O n (le_O_n n). +elim (le_to_or_lt_eq O n (le_O_n n)). assumption. -rewrite < H3.absurd O < m.assumption. +rewrite < H3.absurd (O < m).assumption. rewrite > H2.rewrite < H3. -simplify.exact not_le_Sn_n O. +simplify.exact (not_le_Sn_n O). qed. (* boolean divides *) @@ -218,11 +218,11 @@ qed. theorem decidable_divides: \forall n,m:nat.O < n \to decidable (n \divides m). -intros.change with (n \divides m) \lor n \ndivides m. +intros.change with ((n \divides m) \lor n \ndivides m). cut -match divides_b n m with +(match divides_b n m with [ true \Rightarrow n \divides m -| false \Rightarrow n \ndivides m] \to n \divides m \lor n \ndivides m. +| false \Rightarrow n \ndivides m] \to n \divides m \lor n \ndivides m). apply Hcut.apply divides_b_to_Prop.assumption. elim (divides_b n m).left.apply H1.right.apply H1. qed. @@ -230,22 +230,22 @@ qed. theorem divides_to_divides_b_true : \forall n,m:nat. O < n \to n \divides m \to divides_b n m = true. intros. -cut match (divides_b n m) with +cut (match (divides_b n m) with [ true \Rightarrow n \divides m -| false \Rightarrow n \ndivides m] \to ((divides_b n m) = true). +| false \Rightarrow n \ndivides m] \to ((divides_b n m) = true)). apply Hcut.apply divides_b_to_Prop.assumption. -elim divides_b n m.reflexivity. +elim (divides_b n m).reflexivity. absurd (n \divides m).assumption.assumption. qed. theorem not_divides_to_divides_b_false: \forall n,m:nat. O < n \to \lnot(n \divides m) \to (divides_b n m) = false. intros. -cut match (divides_b n m) with +cut (match (divides_b n m) with [ true \Rightarrow n \divides m -| false \Rightarrow n \ndivides m] \to ((divides_b n m) = false). +| false \Rightarrow n \ndivides m] \to ((divides_b n m) = false)). apply Hcut.apply divides_b_to_Prop.assumption. -elim divides_b n m. +elim (divides_b n m). absurd (n \divides m).assumption.assumption. reflexivity. qed. @@ -254,16 +254,16 @@ qed. theorem divides_f_pi_f : \forall f:nat \to nat.\forall n,m,i:nat. m \le i \to i \le n+m \to f i \divides pi n f m. intros 5.elim n.simplify. -cut i = m.rewrite < Hcut.apply divides_n_n. +cut (i = m).rewrite < Hcut.apply divides_n_n. apply antisymmetric_le.assumption.assumption. simplify. -cut i < S n1+m \lor i = S n1 + m. +cut (i < S n1+m \lor i = S n1 + m). elim Hcut. -apply transitive_divides ? (pi n1 f m). +apply (transitive_divides ? (pi n1 f m)). apply H1.apply le_S_S_to_le. assumption. -apply witness ? ? (f (S n1+m)).apply sym_times. +apply (witness ? ? (f (S n1+m))).apply sym_times. rewrite > H3. -apply witness ? ? (pi n1 f m).reflexivity. +apply (witness ? ? (pi n1 f m)).reflexivity. apply le_to_or_lt_eq.assumption. qed. @@ -282,27 +282,27 @@ qed. (* divides and fact *) theorem divides_fact : \forall n,i:nat. O < i \to i \le n \to i \divides n!. -intros 3.elim n.absurd O H3. -apply witness ? ? n1!.reflexivity. +apply (witness ? ? n1!).reflexivity. qed. theorem mod_S_fact: \forall n,i:nat. (S O) < i \to i \le n \to (S n!) \mod i = (S O). -intros.cut n! \mod i = O. +intros.cut (n! \mod i = O). rewrite < Hcut. -apply mod_S.apply trans_lt O (S O).apply le_n (S O).assumption. +apply mod_S.apply (trans_lt O (S O)).apply (le_n (S O)).assumption. rewrite > Hcut.assumption. -apply divides_to_mod_O.apply trans_lt O (S O).apply le_n (S O).assumption. -apply divides_fact.apply trans_lt O (S O).apply le_n (S O).assumption. +apply divides_to_mod_O.apply (trans_lt O (S O)).apply (le_n (S O)).assumption. +apply divides_fact.apply (trans_lt O (S O)).apply (le_n (S O)).assumption. assumption. qed. @@ -310,8 +310,8 @@ theorem not_divides_S_fact: \forall n,i:nat. (S O) < i \to i \le n \to i \ndivides 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 ((S n!) \mod i) O) = false. +apply (trans_lt O (S O)).apply (le_n (S O)).assumption. +change with ((eqb ((S n!) \mod i) O) = false). rewrite > mod_S_fact.simplify.reflexivity. assumption.assumption. qed. @@ -322,11 +322,11 @@ definition prime : nat \to Prop \def (\forall m:nat. m \divides n \to (S O) < m \to m = n). theorem not_prime_O: \lnot (prime O). -simplify.intro.elim H.apply not_le_Sn_O (S O) H1. +simplify.intro.elim H.apply (not_le_Sn_O (S O) H1). qed. theorem not_prime_SO: \lnot (prime (S O)). -simplify.intro.elim H.apply not_le_Sn_n (S O) H1. +simplify.intro.elim H.apply (not_le_Sn_n (S O) H1). qed. (* smallest factor *) @@ -355,14 +355,14 @@ qed. *) theorem lt_SO_smallest_factor: \forall n:nat. (S O) < n \to (S O) < (smallest_factor n). intro. -apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S O) H. -intro.apply nat_case m.intro. apply False_ind.apply not_le_Sn_n (S O) H. +apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O (S O) H). +intro.apply (nat_case m).intro. apply False_ind.apply (not_le_Sn_n (S O) H). intros. change with -S O < min_aux m1 (S(S m1)) (\lambda m.(eqb ((S(S m1)) \mod m) O)). -apply lt_to_le_to_lt ? (S (S O)). -apply le_n (S(S O)). -cut (S(S O)) = (S(S m1)) - m1. +(S O < min_aux m1 (S(S m1)) (\lambda m.(eqb ((S(S m1)) \mod m) O))). +apply (lt_to_le_to_lt ? (S (S O))). +apply (le_n (S(S O))). +cut ((S(S O)) = (S(S m1)) - m1). rewrite > Hcut. apply le_min_aux. apply sym_eq.apply plus_to_minus. @@ -371,10 +371,10 @@ qed. theorem lt_O_smallest_factor: \forall n:nat. O < n \to O < (smallest_factor n). intro. -apply nat_case n.intro.apply False_ind.apply not_le_Sn_n O H. -intro.apply nat_case m.intro. +apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_n O H). +intro.apply (nat_case m).intro. simplify.apply le_n. -intros.apply trans_lt ? (S O). +intros.apply (trans_lt ? (S O)). simplify. apply le_n. apply lt_SO_smallest_factor.simplify. apply le_S_S. apply le_S_S.apply le_O_n. @@ -383,28 +383,28 @@ qed. theorem divides_smallest_factor_n : \forall n:nat. O < n \to smallest_factor n \divides n. intro. -apply nat_case n.intro.apply False_ind.apply not_le_Sn_O O H. -intro.apply nat_case m.intro. simplify. -apply witness ? ? (S O). simplify.reflexivity. +apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O O H). +intro.apply (nat_case m).intro. simplify. +apply (witness ? ? (S O)). simplify.reflexivity. intros. apply divides_b_true_to_divides. -apply lt_O_smallest_factor ? H. +apply (lt_O_smallest_factor ? H). change with -eqb ((S(S m1)) \mod (min_aux m1 (S(S m1)) - (\lambda m.(eqb ((S(S m1)) \mod m) O)))) O = true. +(eqb ((S(S m1)) \mod (min_aux m1 (S(S m1)) + (\lambda m.(eqb ((S(S m1)) \mod m) O)))) O = true). apply f_min_aux_true. -apply ex_intro nat ? (S(S m1)). +apply (ex_intro nat ? (S(S m1))). split.split. apply le_minus_m.apply le_n. rewrite > mod_n_n.reflexivity. -apply trans_lt ? (S O).apply le_n (S O).simplify. +apply (trans_lt ? (S O)).apply (le_n (S O)).simplify. apply le_S_S.apply le_S_S.apply le_O_n. qed. theorem le_smallest_factor_n : \forall n:nat. smallest_factor n \le n. -intro.apply nat_case n.simplify.reflexivity. -intro.apply nat_case m.simplify.reflexivity. +intro.apply (nat_case n).simplify.reflexivity. +intro.apply (nat_case m).simplify.reflexivity. intro.apply divides_to_le. simplify.apply le_S_S.apply le_O_n. apply divides_smallest_factor_n. @@ -414,15 +414,15 @@ qed. theorem lt_smallest_factor_to_not_divides: \forall n,i:nat. (S O) < n \to (S O) < i \to i < (smallest_factor n) \to i \ndivides n. intros 2. -apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S O) H. -intro.apply nat_case m.intro. apply False_ind.apply not_le_Sn_n (S O) H. +apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O (S O) H). +intro.apply (nat_case m).intro. apply False_ind.apply (not_le_Sn_n (S O) H). intros. apply divides_b_false_to_not_divides. -apply trans_lt O (S O).apply le_n (S O).assumption. -change with (eqb ((S(S m1)) \mod i) O) = false. -apply lt_min_aux_to_false -(\lambda i:nat.eqb ((S(S m1)) \mod i) O) (S(S m1)) m1 i. -cut (S(S O)) = (S(S m1)-m1). +apply (trans_lt O (S O)).apply (le_n (S O)).assumption. +change with ((eqb ((S(S m1)) \mod i) O) = false). +apply (lt_min_aux_to_false +(\lambda i:nat.eqb ((S(S m1)) \mod i) O) (S(S m1)) m1 i). +cut ((S(S O)) = (S(S m1)-m1)). rewrite < Hcut.exact H1. apply sym_eq. apply plus_to_minus. rewrite < sym_plus.simplify.reflexivity. @@ -431,23 +431,23 @@ qed. theorem prime_smallest_factor_n : \forall n:nat. (S O) < n \to prime (smallest_factor n). -intro. change with (S(S O)) \le n \to (S O) < (smallest_factor n) \land -(\forall m:nat. m \divides smallest_factor n \to (S O) < m \to m = (smallest_factor n)). +intro. change with ((S(S O)) \le n \to (S O) < (smallest_factor n) \land +(\forall m:nat. m \divides smallest_factor n \to (S O) < m \to m = (smallest_factor n))). intro.split. apply lt_SO_smallest_factor.assumption. intros. -cut le m (smallest_factor n). -elim le_to_or_lt_eq m (smallest_factor n) Hcut. -absurd m \divides n. -apply transitive_divides m (smallest_factor n). +cut (le m (smallest_factor n)). +elim (le_to_or_lt_eq m (smallest_factor n) Hcut). +absurd (m \divides n). +apply (transitive_divides m (smallest_factor n)). assumption. apply divides_smallest_factor_n. -apply trans_lt ? (S O). simplify. apply le_n. exact H. +apply (trans_lt ? (S O)). simplify. apply le_n. exact H. apply lt_smallest_factor_to_not_divides. exact H.assumption.assumption.assumption. apply divides_to_le. -apply trans_lt O (S O). -apply le_n (S O). +apply (trans_lt O (S O)). +apply (le_n (S O)). apply lt_SO_smallest_factor. exact H. assumption. @@ -455,16 +455,16 @@ qed. theorem prime_to_smallest_factor: \forall n. prime n \to smallest_factor n = n. -intro.apply nat_case n.intro.apply False_ind.apply not_prime_O H. -intro.apply nat_case m.intro.apply False_ind.apply not_prime_SO H. +intro.apply (nat_case n).intro.apply False_ind.apply (not_prime_O H). +intro.apply (nat_case m).intro.apply False_ind.apply (not_prime_SO H). intro. change with -(S O) < (S(S m1)) \land +((S O) < (S(S m1)) \land (\forall m:nat. m \divides S(S m1) \to (S O) < m \to m = (S(S m1))) \to -smallest_factor (S(S m1)) = (S(S m1)). +smallest_factor (S(S m1)) = (S(S m1))). intro.elim H.apply H2. apply divides_smallest_factor_n. -apply trans_lt ? (S O).simplify. apply le_n.assumption. +apply (trans_lt ? (S O)).simplify. apply le_n.assumption. apply lt_SO_smallest_factor. assumption. qed. @@ -500,20 +500,20 @@ match primeb n with [ true \Rightarrow prime n | false \Rightarrow \lnot (prime n)]. intro. -apply nat_case n.simplify.intro.elim H.apply not_le_Sn_O (S O) H1. -intro.apply nat_case m.simplify.intro.elim H.apply not_le_Sn_n (S O) H1. +apply (nat_case n).simplify.intro.elim H.apply (not_le_Sn_O (S O) H1). +intro.apply (nat_case m).simplify.intro.elim H.apply (not_le_Sn_n (S O) H1). intro. change with match eqb (smallest_factor (S(S m1))) (S(S m1)) with [ true \Rightarrow prime (S(S m1)) | false \Rightarrow \lnot (prime (S(S m1)))]. -apply eqb_elim (smallest_factor (S(S m1))) (S(S m1)). -intro.change with prime (S(S m1)). +apply (eqb_elim (smallest_factor (S(S m1))) (S(S m1))). +intro.change with (prime (S(S m1))). rewrite < H. apply prime_smallest_factor_n. simplify.apply le_S_S.apply le_S_S.apply le_O_n. -intro.change with \lnot (prime (S(S m1))). -change with prime (S(S m1)) \to False. +intro.change with (\lnot (prime (S(S m1)))). +change with (prime (S(S m1)) \to False). intro.apply H. apply prime_to_smallest_factor. assumption. @@ -540,11 +540,11 @@ apply primeb_to_Prop. qed. theorem decidable_prime : \forall n:nat.decidable (prime n). -intro.change with (prime n) \lor \lnot (prime n). +intro.change with ((prime n) \lor \lnot (prime n)). cut -match primeb n with +(match primeb n with [ true \Rightarrow prime n -| false \Rightarrow \lnot (prime n)] \to (prime n) \lor \lnot (prime n). +| false \Rightarrow \lnot (prime n)] \to (prime n) \lor \lnot (prime n)). apply Hcut.apply primeb_to_Prop. elim (primeb n).left.apply H.right.apply H. qed. @@ -552,22 +552,22 @@ qed. theorem prime_to_primeb_true: \forall n:nat. prime n \to primeb n = true. intros. -cut match (primeb n) with +cut (match (primeb n) with [ true \Rightarrow prime n -| false \Rightarrow \lnot (prime n)] \to ((primeb n) = true). +| false \Rightarrow \lnot (prime n)] \to ((primeb n) = true)). apply Hcut.apply primeb_to_Prop. -elim primeb n.reflexivity. +elim (primeb n).reflexivity. absurd (prime n).assumption.assumption. qed. theorem not_prime_to_primeb_false: \forall n:nat. \lnot(prime n) \to primeb n = false. intros. -cut match (primeb n) with +cut (match (primeb n) with [ true \Rightarrow prime n -| false \Rightarrow \lnot (prime n)] \to ((primeb n) = false). +| false \Rightarrow \lnot (prime n)] \to ((primeb n) = false)). apply Hcut.apply primeb_to_Prop. -elim primeb n. +elim (primeb n). absurd (prime n).assumption.assumption. reflexivity. qed. diff --git a/helm/matita/library/nat/relevant_equations.ma b/helm/matita/library/nat/relevant_equations.ma index 1c0f25f57..f4cf43775 100644 --- a/helm/matita/library/nat/relevant_equations.ma +++ b/helm/matita/library/nat/relevant_equations.ma @@ -19,9 +19,9 @@ include "nat/minus.ma". theorem times_plus_l: \forall n,m,p:nat. (n+m)*p = n*p + m*p. intros. -apply trans_eq ? ? (p*(n+m)). +apply (trans_eq ? ? (p*(n+m))). apply sym_times. -apply trans_eq ? ? (p*n+p*m). +apply (trans_eq ? ? (p*n+p*m)). apply distr_times_plus. apply eq_f2. apply sym_times. @@ -30,9 +30,9 @@ qed. theorem times_minus_l: \forall n,m,p:nat. (n-m)*p = n*p - m*p. intros. -apply trans_eq ? ? (p*(n-m)). +apply (trans_eq ? ? (p*(n-m))). apply sym_times. -apply trans_eq ? ? (p*n-p*m). +apply (trans_eq ? ? (p*n-p*m)). apply distr_times_minus. apply eq_f2. apply sym_times. @@ -42,7 +42,7 @@ qed. theorem times_plus_plus: \forall n,m,p,q:nat. (n + m)*(p + q) = n*p + n*q + m*p + m*q. intros. -apply trans_eq nat ? ((n*(p+q) + m*(p+q))). +apply (trans_eq nat ? ((n*(p+q) + m*(p+q)))). apply times_plus_l. rewrite > distr_times_plus. rewrite > distr_times_plus. diff --git a/helm/matita/library/nat/sigma_and_pi.ma b/helm/matita/library/nat/sigma_and_pi.ma index 331df8fb3..4f5f6cba0 100644 --- a/helm/matita/library/nat/sigma_and_pi.ma +++ b/helm/matita/library/nat/sigma_and_pi.ma @@ -36,8 +36,8 @@ intros 3.elim n. simplify.apply H.apply le_n.rewrite < plus_n_O.apply le_n. simplify. apply eq_f2.apply H1. -change with m \le (S n1)+m.apply le_plus_n. -rewrite > sym_plus m.apply le_n. +change with (m \le (S n1)+m).apply le_plus_n. +rewrite > (sym_plus m).apply le_n. apply H.intros.apply H1.assumption. rewrite < plus_n_Sm. apply le_S.assumption. @@ -51,8 +51,8 @@ intros 3.elim n. simplify.apply H.apply le_n.rewrite < plus_n_O.apply le_n. simplify. apply eq_f2.apply H1. -change with m \le (S n1)+m.apply le_plus_n. -rewrite > sym_plus m.apply le_n. +change with (m \le (S n1)+m).apply le_plus_n. +rewrite > (sym_plus m).apply le_n. apply H.intros.apply H1.assumption. rewrite < plus_n_Sm. apply le_S.assumption. @@ -61,7 +61,7 @@ qed. theorem eq_fact_pi: \forall n. (S n)! = pi n (\lambda m.m) (S O). intro.elim n. simplify.reflexivity. -change with (S(S n1))*(S n1)! = ((S n1)+(S O))*(pi n1 (\lambda m.m) (S O)). +change with ((S(S n1))*(S n1)! = ((S n1)+(S O))*(pi n1 (\lambda m.m) (S O))). rewrite < plus_n_Sm.rewrite < plus_n_O. apply eq_f.assumption. qed. diff --git a/helm/matita/library/nat/times.ma b/helm/matita/library/nat/times.ma index 8c53a56c8..70a4fd76e 100644 --- a/helm/matita/library/nat/times.ma +++ b/helm/matita/library/nat/times.ma @@ -66,7 +66,7 @@ simplify. intros.elim x. simplify.reflexivity. simplify.rewrite > H. rewrite > assoc_plus.rewrite > assoc_plus. -apply eq_f.rewrite < assoc_plus. rewrite < sym_plus ? z. +apply eq_f.rewrite < assoc_plus. rewrite < (sym_plus ? z). rewrite > assoc_plus.reflexivity. qed. @@ -79,7 +79,7 @@ elim x.simplify.apply refl_eq. simplify.rewrite < sym_times. rewrite > distr_times_plus. rewrite < sym_times. -rewrite < sym_times (times n y) z. +rewrite < (sym_times (times n y) z). rewrite < H.apply refl_eq. qed. diff --git a/helm/matita/tests/change.ma b/helm/matita/tests/change.ma index 4e26d4439..511754d27 100644 --- a/helm/matita/tests/change.ma +++ b/helm/matita/tests/change.ma @@ -33,7 +33,7 @@ qed. alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)". theorem t: (\forall x:nat. x=x) \to True. intro H. - change in match x in H : \forall _.% with 0+x. + change in match x in H : \forall _.% with (0+x). change in H: \forall _.(? ? ? (? % ?)) with 0. constructor 1. qed. diff --git a/helm/matita/tests/clear.ma b/helm/matita/tests/clear.ma index 71457ae2c..9f1655b59 100644 --- a/helm/matita/tests/clear.ma +++ b/helm/matita/tests/clear.ma @@ -22,9 +22,9 @@ theorem stupid: \forall a: True. \forall b: 0 = 0. 0 = 0. -intros 1 [H] . +intros 1 (H). clear H. -intros 1 [H]. +intros 1 (H). exact H. qed. diff --git a/helm/matita/tests/continuationals.ma b/helm/matita/tests/continuationals.ma new file mode 100644 index 000000000..b2f906084 --- /dev/null +++ b/helm/matita/tests/continuationals.ma @@ -0,0 +1,80 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/test/continuationals/". +include "coq.ma". + +alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". +alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)". +alias id "trans_equal" = "cic:/Coq/Init/Logic/trans_equal.con". +alias id "refl_equal" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)". +alias id "Z" = "cic:/Coq/ZArith/BinInt/Z.ind#xpointer(1/1)". + +theorem semicolon: \forall p:Prop.p\to p\land p. +intros (p); split; assumption. +qed. + +theorem branch:\forall x:nat.x=x. +intros (n); +elim n +[ reflexivity; +| reflexivity ]. +qed. + +theorem pos:\forall x:Z.x=x. +intros (n); +elim n; +[ 3: reflexivity; +| 2: reflexivity; +| reflexivity ] +qed. + +theorem dot:\forall x:Z.x=x. +intros (x). +elim x. +reflexivity. reflexivity. reflexivity. +qed. + +theorem dot_slice:\forall x:Z.x=x. +intros (x). +elim x; +[ elim x. reflexivity. reflexivity. reflexivity; +| reflexivity +| reflexivity ]; +qed. + +theorem focus:\forall x:Z.x=x. +intros (x); elim x. +focus 16 17; + reflexivity; +unfocus. +reflexivity. +qed. + +theorem skip:\forall x:nat.x=x. +intros (x). +apply trans_equal; +[ 2: apply (refl_equal nat x); +| skip +| reflexivity +] +qed. + +theorem skip_focus:\forall x:nat.x=x. +intros (x). +apply trans_equal; +[ focus 18; apply (refl_equal nat x); unfocus; +| skip +| reflexivity ] +qed. diff --git a/helm/matita/tests/cut.ma b/helm/matita/tests/cut.ma index e20db6f5d..3e5605a10 100644 --- a/helm/matita/tests/cut.ma +++ b/helm/matita/tests/cut.ma @@ -18,8 +18,8 @@ alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". theorem stupid: 3 = 3. - cut 3 = 3. + cut (3 = 3). assumption. reflexivity. - qed. +qed. diff --git a/helm/matita/tests/inversion.ma b/helm/matita/tests/inversion.ma index 4f8c4c6d4..f717cd1df 100644 --- a/helm/matita/tests/inversion.ma +++ b/helm/matita/tests/inversion.ma @@ -28,21 +28,15 @@ alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". theorem test_inversion: \forall n. le n O \to n=O. intros. (* inversion begins *) - cut O=O. - (* goal 2: 0 = 0 *) - goal 7. reflexivity. - (* goal 1 *) - generalize in match Hcut. - apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H). - (* first goal (left open) *) - intro. rewrite < H1. - clear Hcut. - (* second goal (closed) *) - goal 14. - simplify. intros. - discriminate H3. - (* inversion ends *) + cut (O=O); + [ 2: reflexivity; + | generalize in match Hcut. + apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H); + [ intro. rewrite < H1. clear Hcut. + | simplify. intros. discriminate H3. + ] reflexivity. + ] qed. (* Piu' semplice e non lascia l'ipotesi inutile Hcut *) @@ -51,13 +45,9 @@ theorem test_inversion2: \forall n. le n O \to n=O. intros. (* inversion begins *) generalize in match (refl_equal nat O). - apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H). - (* first goal (left open) *) - intro. rewrite < H1. - (* second goal (closed) *) - goal 13. - simplify. intros. - discriminate H3. - (* inversion ends *) + apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H); + [ intro. rewrite < H1. + | simplify. intros. discriminate H3. + ] reflexivity. qed. diff --git a/helm/matita/tests/metasenv_ordering.ma b/helm/matita/tests/metasenv_ordering.ma index 98b3ff0fe..25c66594b 100644 --- a/helm/matita/tests/metasenv_ordering.ma +++ b/helm/matita/tests/metasenv_ordering.ma @@ -25,11 +25,11 @@ theorem th1 : \forall P:Prop. \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 1 = 1 \land 1 = 0 \land 2 = 2. - intros. split. split. - goal 13. - rewrite > H; [reflexivity | exact nat | exact 0=0 | exact Type]. - reflexivity. - reflexivity. + intros. split; split; + [ reflexivity + | rewrite > H; + [ reflexivity | exact nat | exact (0=0) | exact Type ] + ] qed. theorem th2 : @@ -37,8 +37,9 @@ theorem th2 : \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 1 = 1 \land 1 = 0 \land 3 = 3. intros. split. split. - goal 13. - rewrite > H ?; [reflexivity | exact nat | exact 0=0 | exact Type]. + focus 13. + rewrite > (H ?); [reflexivity | exact nat | exact (0=0) | exact Type]. + unfocus. reflexivity. reflexivity. qed. @@ -48,8 +49,9 @@ theorem th3 : \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 1 = 1 \land 1 = 0 \land 4 = 4. intros. split. split. - goal 13. - rewrite > H ? ?; [reflexivity | exact nat | exact 0=0 | exact Type]. + focus 13. + rewrite > (H ? ?); [reflexivity | exact nat | exact (0=0) | exact Type]. + unfocus. reflexivity. reflexivity. qed. @@ -59,8 +61,9 @@ theorem th4 : \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 1 = 1 \land 1 = 0 \land 5 = 5. intros. split. split. - goal 13. - rewrite > H ? ? ?; [reflexivity | exact nat | exact 0=0 | exact Type]. + focus 13. + rewrite > (H ? ? ?); [reflexivity | exact nat | exact (0=0) | exact Type]. + unfocus. reflexivity. reflexivity. qed. @@ -72,8 +75,9 @@ theorem th5 : \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 1 = 1 \land 1 = 0 \land 6 = 6. intros. split. split. - goal 13. - apply H; [exact nat | exact 0=0 | exact Type]. + focus 13. + apply H; [exact nat | exact (0=0) | exact Type]. + unfocus. reflexivity. reflexivity. qed. @@ -83,8 +87,9 @@ theorem th6 : \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 1 = 1 \land 1 = 0 \land 7 = 7. intros. split. split. - goal 13. - apply H ?; [exact nat | exact 0=0 | exact Type]. + focus 13. + apply (H ?); [exact nat | exact (0=0) | exact Type]. + unfocus. reflexivity. reflexivity. qed. @@ -94,8 +99,9 @@ theorem th7 : \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 1 = 1 \land 1 = 0 \land 8 = 8. intros. split. split. - goal 13. - apply H ? ?; [exact nat | exact 0=0 | exact Type]. + focus 13. + apply (H ? ?); [exact nat | exact (0=0) | exact Type]. + unfocus. reflexivity. reflexivity. qed. @@ -105,8 +111,9 @@ theorem th8 : \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 1 = 1 \land 1 = 0 \land 9 = 9. intros. split. split. - goal 13. - apply H ? ? ?; [exact nat | exact 0=0 | exact Type]. + focus 13. + apply (H ? ? ?); [exact nat | exact (0=0) | exact Type]. + unfocus. reflexivity. reflexivity. qed. @@ -115,28 +122,18 @@ qed. theorem th9: \forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q. - intros [P; Q; R; S; r; s; H]. - elim H ? ?; [split; assumption | exact r | exact s]. + intros (P Q R S r s H). + elim (H ? ?); [split; assumption | exact r | exact s]. qed. theorem th10: \forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q. - intros [P; Q; R; S; r; s; H]. - elim H ?; [split; assumption | exact r | exact s]. + intros (P Q R S r s H). + elim (H ?); [split; assumption | exact r | exact s]. qed. theorem th11: \forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q. - intros [P; Q; R; S; r; s; H]. + intros (P Q R S r s H). elim H; [split; assumption | exact r | exact s]. qed. - - - - - - - - - - \ No newline at end of file diff --git a/helm/matita/tests/replace.ma b/helm/matita/tests/replace.ma index 6d62e41d1..8504b6c16 100644 --- a/helm/matita/tests/replace.ma +++ b/helm/matita/tests/replace.ma @@ -26,8 +26,8 @@ theorem t: \forall x:nat. x * (x + 0) = (0 + x) * (x + x * 0). intro. replace in \vdash (? ? (? ? %) (? % %)) with x. reflexivity. - rewrite < mult_n_O x. - rewrite < plus_n_O x. + rewrite < (mult_n_O x). + rewrite < (plus_n_O x). reflexivity. reflexivity. auto. @@ -35,5 +35,5 @@ qed. (* This test tests "replace in match t" where t contains some metavariables *) theorem t2: 2 + (3 * 4) = (5 + 5) + 2 * 2. - replace in match 5+? with 6 + 4; [reflexivity | reflexivity]. + replace in match 5+? with (6 + 4); [reflexivity | reflexivity]. qed. diff --git a/helm/matita/tests/simpl.ma b/helm/matita/tests/simpl.ma index 2a860e190..75a1693f4 100644 --- a/helm/matita/tests/simpl.ma +++ b/helm/matita/tests/simpl.ma @@ -20,7 +20,8 @@ alias id "plus" = "cic:/Coq/Init/Peano/plus.con". alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)". alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)". alias id "not" = "cic:/Coq/Init/Logic/not.con". - +alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". +alias id "plus_comm" = "cic:/Coq/Arith/Plus/plus_comm.con". theorem a : \forall A:Set. @@ -37,12 +38,14 @@ theorem t: let f \def \lambda x,y. x y in f (\lambda x.S x) O = S O. intros. simplify. change in \vdash (? ? (? %) ?) with O. reflexivity. qed. + theorem X: \forall x:nat. let myplus \def plus x in myplus (S O) = S x. - intros. simplify. change in \vdash (? ? (% ?) ?) with plus x. - rewrite > plus_comm. reflexivity. qed. + intros. simplify. change in \vdash (? ? (% ?) ?) with (plus x). + +rewrite > plus_comm. reflexivity. qed. theorem R: \forall x:nat. let uno \def x + O in S O + uno = 1 + x. intros. simplify. - change in \vdash (? ? (? %) ?) with x + O. + change in \vdash (? ? (? %) ?) with (x + O). rewrite > plus_comm. reflexivity. qed. diff --git a/helm/matita/tests/test3.ma b/helm/matita/tests/test3.ma index 6b05351e6..98dc65c95 100644 --- a/helm/matita/tests/test3.ma +++ b/helm/matita/tests/test3.ma @@ -18,9 +18,9 @@ include "coq.ma". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". theorem a:\forall x.x=x. alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". -exact nat. -intro. -reflexivity. +[ exact nat. +| intro. reflexivity. +] qed. alias num (instance 0) = "natural number". alias symbol "times" (instance 0) = "Coq's natural times".