From: Claudio Sacerdoti Coen Date: Mon, 19 Sep 2005 09:41:19 +0000 (+0000) Subject: Removed final question marks from {apply|elim|rewrite}s. X-Git-Tag: LAST_BEFORE_NEW~105 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b8c6dd0220fba9ebed2d51d5808790b5949177ea;p=helm.git Removed final question marks from {apply|elim|rewrite}s. (This used to change the goals order, but it has now been fixed by Gares) --- diff --git a/helm/matita/library/Q/q.ma b/helm/matita/library/Q/q.ma index 4878078fc..1ff2adcd8 100644 --- a/helm/matita/library/Q/q.ma +++ b/helm/matita/library/Q/q.ma @@ -162,13 +162,13 @@ apply fraction_elim2 (\lambda f,g. Or (f=g) (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) : Or (n=n1) (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) : Or (x=y) (x=y \to False)). left.apply eq_f2.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)). @@ -317,4 +317,4 @@ theorem rtimes_rinv: \forall r:ratio. rtimes r (rinv r) = one. intro.elim r. reflexivity. simplify.apply ftimes_finv. -qed. \ No newline at end of file +qed. diff --git a/helm/matita/library/Z/plus.ma b/helm/matita/library/Z/plus.ma index dc743e60b..b89f291fb 100644 --- a/helm/matita/library/Z/plus.ma +++ b/helm/matita/library/Z/plus.ma @@ -59,12 +59,12 @@ simplify. rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity. simplify. rewrite > nat_compare_n_m_m_n. -simplify.elim nat_compare ? ?.simplify.reflexivity. +simplify.elim nat_compare.simplify.reflexivity. simplify. reflexivity. simplify. reflexivity. elim y.simplify.reflexivity. simplify.rewrite > nat_compare_n_m_m_n. -simplify.elim nat_compare ? ?.simplify.reflexivity. +simplify.elim nat_compare.simplify.reflexivity. simplify. reflexivity. simplify. reflexivity. simplify.rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity. diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma index c4e965fbf..a36bd078c 100644 --- a/helm/matita/library/Z/times.ma +++ b/helm/matita/library/Z/times.ma @@ -78,24 +78,24 @@ intros.elim x. change with eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2)))) (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))). - rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity. + rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity. apply lt_O_times_S_S.apply lt_O_times_S_S. change with eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2)))) (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))). - rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity. + rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity. apply lt_O_times_S_S.apply lt_O_times_S_S. elim z. simplify.reflexivity. change with eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2)))) (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))). - rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity. + rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity. apply lt_O_times_S_S.apply lt_O_times_S_S. change with eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2)))) (pos(pred (times (S n) (S (pred (times (S n1) (S n2))))))). - rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity. + rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity. apply lt_O_times_S_S.apply lt_O_times_S_S. elim y. simplify.reflexivity. @@ -104,24 +104,24 @@ intros.elim x. change with eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2)))) (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))). - rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity. + rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity. apply lt_O_times_S_S.apply lt_O_times_S_S. change with eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2)))) (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))). - rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity. + rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity. apply lt_O_times_S_S.apply lt_O_times_S_S. elim z. simplify.reflexivity. change with eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2)))) (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))). - rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity. + rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity. apply lt_O_times_S_S.apply lt_O_times_S_S. change with eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2)))) (neg(pred (times (S n) (S (pred (times (S n1) (S n2))))))). - rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity. + rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity. apply lt_O_times_S_S.apply lt_O_times_S_S. qed. @@ -134,8 +134,8 @@ eq nat (times (S n) (S (pred (minus (S p) (S q))))) (minus (pred (times (S n) (S p))) (pred (times (S n) (S q)))). intros. -rewrite < S_pred ? ?. -rewrite > minus_pred_pred ? ? ? ?. +rewrite < S_pred. +rewrite > minus_pred_pred. rewrite < distr_times_minus. reflexivity. (* we now close all positivity conditions *) @@ -151,7 +151,7 @@ intros. simplify. change in match (plus p (times n (S p))) with (pred (times (S n) (S p))). change in match (plus q (times n (S q))) with (pred (times (S n) (S q))). -rewrite < nat_compare_pred_pred ? ? ? ?. +rewrite < nat_compare_pred_pred. rewrite < nat_compare_times_l. rewrite < nat_compare_S_S. apply nat_compare_elim p q. @@ -236,4 +236,4 @@ qed. variant distr_Ztimes_Zplus: \forall x,y,z. eq Z (Ztimes x (Zplus y z)) (Zplus (Ztimes x y) (Ztimes x z)) \def -distributive_Ztimes_Zplus. \ No newline at end of file +distributive_Ztimes_Zplus. diff --git a/helm/matita/library/nat/compare.ma b/helm/matita/library/nat/compare.ma index 443c6657f..22c8b25a7 100644 --- a/helm/matita/library/nat/compare.ma +++ b/helm/matita/library/nat/compare.ma @@ -43,7 +43,7 @@ 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). diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma index ede15596a..ad74a324d 100644 --- a/helm/matita/library/nat/div_and_mod.ma +++ b/helm/matita/library/nat/div_and_mod.ma @@ -126,7 +126,7 @@ 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. @@ -134,7 +134,7 @@ apply le_plus_n. rewrite < sym_times. rewrite > distr_times_minus. (* ATTENZIONE ALL' ORDINAMENTO DEI GOALS *) -rewrite > plus_minus ? ? ? ?. +rewrite > plus_minus. rewrite > sym_times. rewrite < H5. rewrite < sym_times. @@ -154,14 +154,14 @@ 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. apply le_plus_n. rewrite < sym_times. rewrite > distr_times_minus. -rewrite > plus_minus ? ? ? ?. +rewrite > plus_minus. rewrite > sym_times. rewrite < H3. rewrite < sym_times. @@ -275,4 +275,4 @@ 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 -\def lt_O_to_injective_times_l. \ No newline at end of file +\def lt_O_to_injective_times_l. diff --git a/helm/matita/library/nat/factorization.ma b/helm/matita/library/nat/factorization.ma index a3a715228..4628eca13 100644 --- a/helm/matita/library/nat/factorization.ma +++ b/helm/matita/library/nat/factorization.ma @@ -216,7 +216,7 @@ 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 ?. +apply not_le_Sn_O O. rewrite > Hcut3 in \vdash (? ? %). assumption.rewrite > Hcut. rewrite < H6.reflexivity. @@ -273,7 +273,7 @@ cut (S(S m1)) = r. rewrite > Hcut3 in \vdash (? (? ? %)). change with divides (nth_prime p) r \to False. intro. -apply plog_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r ? ? ? ?. +apply plog_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. @@ -301,7 +301,7 @@ 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 not_lt_to_le.assumption. @@ -400,7 +400,7 @@ 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 H i (S j). apply trans_lt ? j.assumption.simplify.apply le_n. assumption. apply divides_times_to_divides. @@ -470,7 +470,7 @@ simplify in H4. rewrite > plus_n_O. rewrite > plus_n_O (defactorize_aux n3 (S i)).assumption. apply False_ind. -apply not_divides_defactorize_aux n1 i (S i) ?. +apply not_divides_defactorize_aux n1 i (S i). simplify. apply le_n. simplify in H5. rewrite > plus_n_O (defactorize_aux n1 (S i)). @@ -480,7 +480,7 @@ apply witness ? ? ((exp (nth_prime i) n5)*(defactorize_aux n3 (S i))). reflexivity. intros. apply False_ind. -apply not_divides_defactorize_aux n3 i (S i) ?. +apply not_divides_defactorize_aux n3 i (S i). simplify. apply le_n. simplify in H4. rewrite > plus_n_O (defactorize_aux n3 (S i)). diff --git a/helm/matita/library/nat/log.ma b/helm/matita/library/nat/log.ma index 301c0be8e..3babb5c75 100644 --- a/helm/matita/library/nat/log.ma +++ b/helm/matita/library/nat/log.ma @@ -178,7 +178,7 @@ rewrite > H4. (* 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/minimization.ma b/helm/matita/library/nat/minimization.ma index 748399fbc..4dfda0ba6 100644 --- a/helm/matita/library/nat/minimization.ma +++ b/helm/matita/library/nat/minimization.ma @@ -86,7 +86,7 @@ simplify. 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. @@ -94,7 +94,7 @@ apply le_n_Sm_elim a n1 H4. intros. apply ex_intro nat ? a. split.apply le_S_S_to_le.assumption.assumption. -intros.apply False_ind.apply not_eq_true_false ?. +intros.apply False_ind.apply not_eq_true_false. rewrite < H2.rewrite < H7.rewrite > H6. reflexivity. reflexivity. qed. @@ -163,7 +163,7 @@ simplify. 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. @@ -204,7 +204,7 @@ 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 3acce20af..079e902ad 100644 --- a/helm/matita/library/nat/minus.ma +++ b/helm/matita/library/nat/minus.ma @@ -82,7 +82,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. @@ -220,7 +220,7 @@ apply (leb_elim z y). 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 ? ? ?. + rewrite < plus_minus_m_m. reflexivity. apply le_times_r.assumption. intro.rewrite > eq_minus_n_m_O. diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma index 100cb0f03..aae6434e7 100644 --- a/helm/matita/library/nat/nat.ma +++ b/helm/matita/library/nat/nat.ma @@ -97,7 +97,7 @@ 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 37c60b405..0b8f2bbe2 100644 --- a/helm/matita/library/nat/nth_prime.ma +++ b/helm/matita/library/nat/nth_prime.ma @@ -43,7 +43,7 @@ n < smallest_factor (S (fact n)). intros. apply not_le_to_lt. change with smallest_factor (S (fact n)) \le n \to False.intro. -apply not_divides_S_fact n (smallest_factor(S (fact n))) ? ?. +apply not_divides_S_fact n (smallest_factor(S (fact n))). apply lt_SO_smallest_factor. simplify.apply le_S_S.apply le_SO_fact. assumption.