From 400b07e007cfbb0b4ce5ed77cfc50f227c491310 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 8 Nov 2005 15:43:07 +0000 Subject: [PATCH] Yet another semantics for simplify. --- helm/matita/library/Q/q.ma | 28 ++++---- helm/matita/library/Z/compare.ma | 10 +-- helm/matita/library/Z/orders.ma | 4 +- helm/matita/library/Z/times.ma | 2 +- helm/matita/library/Z/z.ma | 28 ++++---- helm/matita/library/datatypes/bool.ma | 2 +- helm/matita/library/list/sort.ma | 24 ++++--- helm/matita/library/logic/equality.ma | 4 +- helm/matita/library/nat/chinese_reminder.ma | 8 +-- helm/matita/library/nat/compare.ma | 14 ++-- helm/matita/library/nat/count.ma | 46 ++++++------- helm/matita/library/nat/div_and_mod.ma | 8 +-- helm/matita/library/nat/exp.ma | 10 +-- helm/matita/library/nat/factorial.ma | 4 +- helm/matita/library/nat/factorization.ma | 38 +++++------ .../library/nat/fermat_little_theorem.ma | 66 +++++++++---------- helm/matita/library/nat/gcd.ma | 36 +++++----- helm/matita/library/nat/lt_arith.ma | 14 ++-- helm/matita/library/nat/minus.ma | 6 +- helm/matita/library/nat/nat.ma | 8 +-- helm/matita/library/nat/nth_prime.ma | 12 ++-- helm/matita/library/nat/ord.ma | 6 +- helm/matita/library/nat/orders.ma | 42 ++++++------ helm/matita/library/nat/permutation.ma | 54 +++++++-------- helm/matita/library/nat/plus.ma | 2 +- helm/matita/library/nat/primes.ma | 32 ++++----- helm/matita/library/nat/times.ma | 6 +- helm/matita/library/nat/totient.ma | 20 +++--- helm/matita/tests/simpl.ma | 2 +- 29 files changed, 269 insertions(+), 267 deletions(-) diff --git a/helm/matita/library/Q/q.ma b/helm/matita/library/Q/q.ma index d69e459ac..340154979 100644 --- a/helm/matita/library/Q/q.ma +++ b/helm/matita/library/Q/q.ma @@ -92,13 +92,13 @@ definition ftl \def | (cons x f) \Rightarrow f]. theorem injective_pp : injective nat fraction pp. -simplify.intros. +unfold injective.intros. change with ((aux (pp x)) = (aux (pp y))). apply eq_f.assumption. qed. theorem injective_nn : injective nat fraction nn. -simplify.intros. +unfold injective.intros. change with ((aux (nn x)) = (aux (nn y))). apply eq_f.assumption. qed. @@ -118,7 +118,7 @@ apply eq_f.assumption. qed. theorem not_eq_pp_nn: \forall n,m:nat. pp n \neq nn m. -intros.simplify. intro. +intros.unfold Not. intro. change with match (pp n) with [ (pp n) \Rightarrow False | (nn n) \Rightarrow True @@ -130,7 +130,7 @@ qed. theorem not_eq_pp_cons: \forall n:nat.\forall x:Z. \forall f:fraction. pp n \neq cons x f. -intros.simplify. intro. +intros.unfold Not. intro. change with match (pp n) with [ (pp n) \Rightarrow False | (nn n) \Rightarrow True @@ -142,7 +142,7 @@ qed. theorem not_eq_nn_cons: \forall n:nat.\forall x:Z. \forall f:fraction. nn n \neq cons x f. -intros.simplify. intro. +intros.unfold Not. intro. change with match (nn n) with [ (pp n) \Rightarrow True | (nn n) \Rightarrow False @@ -153,7 +153,7 @@ qed. theorem decidable_eq_fraction: \forall f,g:fraction. decidable (f = g). -intros.simplify. +intros.unfold decidable. 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)). @@ -188,16 +188,16 @@ intros.apply (fraction_elim2 intros.elim g1. simplify.apply eqb_elim. intro.simplify.apply eq_f.assumption. - intro.simplify.intro.apply H.apply injective_pp.assumption. + intro.simplify.unfold Not.intro.apply H.apply injective_pp.assumption. 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.unfold Not.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. + intro.simplify.unfold Not.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.unfold Not.intro.apply (not_eq_pp_cons m x f1).apply sym_eq. assumption. + intros.simplify.unfold Not.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.unfold Not.intro.apply H2.apply (eq_cons_to_eq2 x y).assumption. + intro.simplify.unfold Not.intro.apply H1.apply (eq_cons_to_eq1 f1 g1).assumption. qed. let rec finv f \def @@ -243,7 +243,7 @@ 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)). +unfold symmetric2. 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)). apply eq_f.apply sym_Zplus. diff --git a/helm/matita/library/Z/compare.ma b/helm/matita/library/Z/compare.ma index a59100885..4a5025975 100644 --- a/helm/matita/library/Z/compare.ma +++ b/helm/matita/library/Z/compare.ma @@ -49,17 +49,17 @@ 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.unfold Not.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. + intro.simplify.unfold Not.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.unfold Not.intro.apply (not_eq_OZ_neg n).apply sym_eq.assumption. + simplify.unfold Not.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. + intro.simplify.unfold Not.intro.apply H.apply inj_neg.assumption. qed. theorem eqZb_elim: \forall x,y:Z.\forall P:bool \to Prop. diff --git a/helm/matita/library/Z/orders.ma b/helm/matita/library/Z/orders.ma index 186533ea0..c39f69308 100644 --- a/helm/matita/library/Z/orders.ma +++ b/helm/matita/library/Z/orders.ma @@ -71,9 +71,9 @@ theorem irreflexive_Zlt: irreflexive Z Zlt. change with (\forall x:Z. x < x \to False). intro.elim x.exact H. cut (neg n < neg n \to False). -apply Hcut.apply H.simplify.apply not_le_Sn_n. +apply Hcut.apply H.simplify.unfold lt.apply not_le_Sn_n. cut (pos n < pos n \to False). -apply Hcut.apply H.simplify.apply not_le_Sn_n. +apply Hcut.apply H.simplify.unfold lt.apply not_le_Sn_n. qed. theorem irrefl_Zlt: irreflexive Z Zlt diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma index 27266bf39..e5e1cdb45 100644 --- a/helm/matita/library/Z/times.ma +++ b/helm/matita/library/Z/times.ma @@ -140,7 +140,7 @@ reflexivity. (* we now close all positivity conditions *) apply lt_O_times_S_S. apply lt_O_times_S_S. -simplify. +simplify.unfold lt. apply le_SO_minus. exact H. qed. diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma index d1a846da4..d18c80b23 100644 --- a/helm/matita/library/Z/z.ma +++ b/helm/matita/library/Z/z.ma @@ -54,15 +54,15 @@ match OZ_test z with |false \Rightarrow z \neq OZ]. intros.elim z. simplify.reflexivity. -simplify.intros (H). +simplify. unfold Not. intros (H). discriminate H. -simplify.intros (H). +simplify. unfold Not. intros (H). discriminate H. qed. (* discrimination *) theorem injective_pos: injective nat Z pos. -simplify. +unfold injective. intros. change with (abs (pos x) = abs (pos y)). apply eq_f.assumption. @@ -72,7 +72,7 @@ variant inj_pos : \forall n,m:nat. pos n = pos m \to n = m \def injective_pos. theorem injective_neg: injective nat Z neg. -simplify. +unfold injective. intros. change with (abs (neg x) = abs (neg y)). apply eq_f.assumption. @@ -82,22 +82,22 @@ 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). +unfold Not.intros (n H). discriminate H. qed. theorem not_eq_OZ_neg :\forall n:nat. OZ \neq neg n. -simplify.intros (n H). +unfold Not.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). +unfold Not.intros (n m H). discriminate H. qed. theorem decidable_eq_Z : \forall x,y:Z. decidable (x=y). -intros.simplify. +intros.unfold decidable. elim x. (* goal: x=OZ *) elim y. @@ -110,25 +110,25 @@ elim x. (* goal: x=pos *) elim y. (* goal: x=pos y=OZ *) - right.intro. + right.unfold Not.intro. 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.unfold Not.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.unfold Not.intro.apply (not_eq_pos_neg n n1). assumption. (* goal: x=neg *) elim y. (* goal: x=neg y=OZ *) - right.intro. + right.unfold Not.intro. 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. unfold Not.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. - right.intro.apply H.apply injective_neg.assumption. + right.unfold Not.intro.apply H.apply injective_neg.assumption. qed. (* end discrimination *) diff --git a/helm/matita/library/datatypes/bool.ma b/helm/matita/library/datatypes/bool.ma index 11f1d7a8c..f4aec8167 100644 --- a/helm/matita/library/datatypes/bool.ma +++ b/helm/matita/library/datatypes/bool.ma @@ -32,7 +32,7 @@ theorem bool_elim: \forall P:bool \to Prop. \forall b:bool. qed. theorem not_eq_true_false : true \neq false. -simplify.intro. +unfold Not.intro. change with match true with [ true \Rightarrow False diff --git a/helm/matita/library/list/sort.ma b/helm/matita/library/list/sort.ma index 2d60662a4..1cc127759 100644 --- a/helm/matita/library/list/sort.ma +++ b/helm/matita/library/list/sort.ma @@ -74,7 +74,8 @@ lemma ordered_injective: [ generalize in match Hcut; apply andb_elim; elim (le s s1); - [ change with (ordered A le (s1::l2) = true \to ordered A le (s1::l2) = true). + [ simplify; + fold simplify (ordered ? le (s1::l2)); intros; assumption; | simplify; intros (Habsurd); @@ -96,11 +97,11 @@ lemma insert_sorted: ordered A le l = true \to ordered A le (insert A le x l) = true. intros 5 (A le H l x). elim l; - [ 2: change with (ordered A le (match le x s with - [ true ⇒ x::(s::l1) | false ⇒ s::(insert A le x l1) ]) = true). + [ 2: simplify; apply (bool_elim ? (le x s)); [ intros; - change with ((le x s \land ordered A le (s::l1)) = true); + simplify; + fold simplify (ordered ? le (s::l1)); apply andb_elim; rewrite > H3; assumption; @@ -112,22 +113,25 @@ lemma insert_sorted: [ simplify; rewrite > (H x a H2); reflexivity; - | change with ((ordered A le (a::match le x s with - [ true ⇒ x::s::l2 | false ⇒ s::(insert A le x l2) ])) = true). + | simplify in \vdash (? ? (? ? ? %) ?); apply (bool_elim ? (le x s)); [ intros; - change with ((le a x \land (le x s \land ordered A le (s::l2))) = true). + simplify; + fold simplify (ordered A le (s::l2)); apply andb_elim; rewrite > (H x a H3); - change with ((le x s \land ordered A le (s::l2)) = true). + simplify; + fold simplify (ordered A le (s::l2)); apply andb_elim; rewrite > H4; apply (ordered_injective A le (a::s::l2)); assumption; | intros; - change with ((le a s \land ordered A le (s::(insert A le x l2))) = true); + simplify; + fold simplify (ordered A le (s::(insert A le x l2))); apply andb_elim; - change in H2 with ((le a s \land ordered A le (s::l2)) = true); + simplify in H2; + fold simplify (ordered A le (s::l2)) in H2; generalize in match H2; apply (andb_elim (le a s)); elim (le a s); diff --git a/helm/matita/library/logic/equality.ma b/helm/matita/library/logic/equality.ma index 40157d849..b87dc6c95 100644 --- a/helm/matita/library/logic/equality.ma +++ b/helm/matita/library/logic/equality.ma @@ -41,14 +41,14 @@ simplify.intros.apply refl_eq. qed. theorem symmetric_eq: \forall A:Type. symmetric A (eq A). -simplify.intros.elim H. apply refl_eq. +unfold symmetric.intros.elim H. apply refl_eq. qed. theorem sym_eq : \forall A:Type.\forall x,y:A. x=y \to y=x \def symmetric_eq. theorem transitive_eq : \forall A:Type. transitive A (eq A). -simplify.intros.elim H1.assumption. +unfold transitive.intros.elim H1.assumption. qed. theorem trans_eq : \forall A:Type.\forall x,y,z:A. x=y \to y=z \to x=z diff --git a/helm/matita/library/nat/chinese_reminder.ma b/helm/matita/library/nat/chinese_reminder.ma index f14f16d27..30cc7440f 100644 --- a/helm/matita/library/nat/chinese_reminder.ma +++ b/helm/matita/library/nat/chinese_reminder.ma @@ -53,7 +53,7 @@ apply minus_to_plus. apply lt_to_le. change with (O + a2*m < a1*n). apply lt_minus_to_plus. -rewrite > H5.simplify.apply le_n. +rewrite > H5.unfold lt.apply le_n. assumption. (* congruent to b *) cut (a2*m = a1*n - (S O)). @@ -84,7 +84,7 @@ apply minus_to_plus. apply lt_to_le. change with (O + a2*m < a1*n). apply lt_minus_to_plus. -rewrite > H5.simplify.apply le_n. +rewrite > H5.unfold lt.apply le_n. assumption. (* and now the symmetric case; the price to pay for working in nat instead than Z *) @@ -119,7 +119,7 @@ apply minus_to_plus. apply lt_to_le. change with (O + a1*n < a2*m). apply lt_minus_to_plus. -rewrite > H5.simplify.apply le_n. +rewrite > H5.unfold lt.apply le_n. assumption. (* congruent to a *) cut (a2*m = a1*n + (S O)). @@ -149,7 +149,7 @@ apply minus_to_plus. apply lt_to_le. change with (O + a1*n < a2*m). apply lt_minus_to_plus. -rewrite > H5.simplify.apply le_n. +rewrite > H5.unfold lt.apply le_n. assumption. (* proof of the cut *) rewrite < H2. diff --git a/helm/matita/library/nat/compare.ma b/helm/matita/library/nat/compare.ma index e85a80265..264731580 100644 --- a/helm/matita/library/nat/compare.ma +++ b/helm/matita/library/nat/compare.ma @@ -42,13 +42,13 @@ intro.elim n1. simplify.reflexivity. simplify.apply not_eq_O_S. intro. -simplify. +simplify.unfold Not. intro. apply (not_eq_O_S n1).apply sym_eq.assumption. intros.simplify. generalize in match H. elim ((eqb n1 m1)). simplify.apply eq_f.apply H1. -simplify.intro.apply H1.apply inj_S.assumption. +simplify.unfold Not.intro.apply H1.apply inj_S.assumption. qed. theorem eqb_elim : \forall n,m:nat.\forall P:bool \to Prop. @@ -126,7 +126,7 @@ simplify.exact le_O_n. simplify.exact not_le_Sn_O. 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. +simplify.unfold Not.intros.apply H.apply le_S_S_to_le.assumption. qed. theorem leb_elim: \forall n,m:nat. \forall P:bool \to Prop. @@ -191,12 +191,12 @@ apply (nat_elim2 (\lambda n,m.match (nat_compare n m) with | EQ \Rightarrow n=m | 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. +simplify.unfold lt.apply le_S_S.apply le_O_n. +intro.simplify.unfold lt.apply le_S_S. apply le_O_n. intros 2.simplify.elim ((nat_compare n1 m1)). -simplify. apply le_S_S.apply H. +simplify. unfold lt. apply le_S_S.apply H. simplify. apply eq_f. apply H. -simplify. apply le_S_S.apply H. +simplify. unfold lt.apply le_S_S.apply H. qed. theorem nat_compare_n_m_m_n: \forall n,m:nat. diff --git a/helm/matita/library/nat/count.ma b/helm/matita/library/nat/count.ma index 60bdbadc4..20913fa60 100644 --- a/helm/matita/library/nat/count.ma +++ b/helm/matita/library/nat/count.ma @@ -78,7 +78,7 @@ rewrite < plus_n_O. rewrite < H. rewrite > (S_pred ((S n1)*(S m))). apply sigma_plus1. -simplify.apply le_S_S.apply le_O_n. +simplify.unfold lt.apply le_S_S.apply le_O_n. qed. theorem eq_sigma_sigma1 : \forall n,m:nat.\forall f:nat \to nat. @@ -138,15 +138,15 @@ rewrite > (div_mod_spec_to_eq2 (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n)) ((i1*(S n) + i) \mod (S n)) i1 i). rewrite > H3. apply bool_to_nat_andb. -simplify.apply le_S_S.assumption. -simplify.apply le_S_S.assumption. +unfold lt.apply le_S_S.assumption. +unfold lt.apply le_S_S.assumption. apply div_mod_spec_div_mod. -simplify.apply le_S_S.apply le_O_n. -constructor 1.simplify.apply le_S_S.assumption. +unfold lt.apply le_S_S.apply le_O_n. +constructor 1.unfold lt.apply le_S_S.assumption. reflexivity. apply div_mod_spec_div_mod. -simplify.apply le_S_S.apply le_O_n. -constructor 1.simplify.apply le_S_S.assumption. +unfold lt.apply le_S_S.apply le_O_n. +constructor 1.unfold lt.apply le_S_S.assumption. reflexivity. apply (trans_eq ? ? (sigma n (\lambda n.((bool_to_nat (f1 n)) * @@ -170,13 +170,13 @@ rewrite < S_pred in \vdash (? ? %). change with ((g (i/(S n)) (i \mod (S n))) \lt (S n)*(S m)). apply H. apply lt_mod_m_m. -simplify. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. apply (lt_times_to_lt_l n). apply (le_to_lt_to_lt ? i). rewrite > (div_mod i (S n)) in \vdash (? ? %). rewrite > sym_plus. apply le_plus_n. -simplify. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. unfold lt. rewrite > S_pred in \vdash (? ? %). apply le_S_S. @@ -184,12 +184,12 @@ rewrite > plus_n_O in \vdash (? ? %). rewrite > sym_times. assumption. rewrite > (times_n_O O). apply lt_times. -simplify. apply le_S_S.apply le_O_n. -simplify. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. rewrite > (times_n_O O). apply lt_times. -simplify. apply le_S_S.apply le_O_n. -simplify. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. rewrite < plus_n_O. unfold injn. intros. @@ -206,40 +206,40 @@ rewrite < (H2 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3) in \vdash (? ? (? % ?) ?). rewrite < (H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5). rewrite < (H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5) in \vdash (? ? ? (? % ?)). rewrite > H6.reflexivity. -simplify. apply le_S_S.apply le_O_n. -simplify. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. apply (lt_times_to_lt_l n). apply (le_to_lt_to_lt ? j). rewrite > (div_mod j (S n)) in \vdash (? ? %). rewrite > sym_plus. apply le_plus_n. -simplify. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. rewrite < sym_times. assumption. apply lt_mod_m_m. -simplify. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. apply (lt_times_to_lt_l n). apply (le_to_lt_to_lt ? i). rewrite > (div_mod i (S n)) in \vdash (? ? %). rewrite > sym_plus. apply le_plus_n. -simplify. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. rewrite < sym_times. assumption. apply lt_mod_m_m. -simplify. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. unfold lt. rewrite > S_pred in \vdash (? ? %). apply le_S_S.assumption. rewrite > (times_n_O O). apply lt_times. -simplify. apply le_S_S.apply le_O_n. -simplify. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. unfold lt. rewrite > S_pred in \vdash (? ? %). apply le_S_S.assumption. rewrite > (times_n_O O). apply lt_times. -simplify. apply le_S_S.apply le_O_n. -simplify. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. intros. apply False_ind. apply (not_le_Sn_O m1 H4). diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma index 9995830a9..e9831f82a 100644 --- a/helm/matita/library/nat/div_and_mod.ma +++ b/helm/matita/library/nat/div_and_mod.ma @@ -70,7 +70,7 @@ 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). -simplify.apply le_S_S.apply le_mod_aux_m_m. +simplify.unfold lt.apply le_S_S.apply le_mod_aux_m_m. apply le_n. qed. @@ -108,7 +108,7 @@ 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.unfold Not.intros.elim H.absurd (le (S r) O). rewrite < H1.assumption. exact (not_le_Sn_O r). qed. @@ -188,7 +188,7 @@ qed. theorem div_mod_spec_times : \forall n,m:nat.div_mod_spec ((S n)*m) (S n) m O. intros.constructor 1. -simplify.apply le_S_S.apply le_O_n. +unfold lt.apply le_S_S.apply le_O_n. rewrite < plus_n_O.rewrite < sym_times.reflexivity. qed. @@ -198,7 +198,7 @@ intros. 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. +unfold lt.apply le_S_S.apply le_O_n. apply div_mod_spec_times. qed. diff --git a/helm/matita/library/nat/exp.ma b/helm/matita/library/nat/exp.ma index 49e3bbd70..11d84f74c 100644 --- a/helm/matita/library/nat/exp.ma +++ b/helm/matita/library/nat/exp.ma @@ -48,14 +48,14 @@ rewrite < times_n_Sm.reflexivity. qed. theorem lt_O_exp: \forall n,m:nat. O < n \to O < n \sup m. -intros.elim m.simplify.apply le_n. -simplify.rewrite > times_n_SO. +intros.elim m.simplify.unfold lt.apply le_n. +simplify.unfold lt.rewrite > times_n_SO. apply le_times.assumption.assumption. qed. theorem lt_m_exp_nm: \forall n,m:nat. (S O) < n \to m < n \sup m. -intros.elim m.simplify.reflexivity. -simplify. +intros.elim m.simplify.unfold lt.reflexivity. +simplify.unfold lt. apply (trans_le ? ((S(S O))*(S n1))). simplify. rewrite < plus_n_Sm.apply le_S_S.apply le_S_S. @@ -83,7 +83,7 @@ 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). -apply Hcut.simplify. apply le_S_S_to_le. apply le_S. assumption. +apply Hcut.simplify.unfold lt.apply le_S_S_to_le. apply le_S. assumption. assumption. intros 2. apply (nat_case n). diff --git a/helm/matita/library/nat/factorial.ma b/helm/matita/library/nat/factorial.ma index 22a799d07..14217bbcb 100644 --- a/helm/matita/library/nat/factorial.ma +++ b/helm/matita/library/nat/factorial.ma @@ -52,10 +52,10 @@ 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. +simplify.unfold lt. apply le_S_S.rewrite < plus_n_O. apply le_plus_n. apply le_times_r.apply le_SSO_fact. -simplify.apply le_S_S_to_le.exact H. +simplify.unfold lt.apply le_S_S_to_le.exact H. qed. diff --git a/helm/matita/library/nat/factorization.ma b/helm/matita/library/nat/factorization.ma index b64e3733b..6a3094303 100644 --- a/helm/matita/library/nat/factorization.ma +++ b/helm/matita/library/nat/factorization.ma @@ -40,10 +40,10 @@ rewrite > H1. apply le_smallest_factor_n. rewrite > H1. 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)).unfold lt. 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)). unfold lt. apply le_n. assumption. apply prime_to_nth_prime. apply prime_smallest_factor_n.assumption. qed. @@ -167,7 +167,7 @@ match f with theorem lt_O_defactorize_aux: \forall f:nat_fact.\forall i:nat. O < defactorize_aux f i. -intro.elim f.simplify. +intro.elim f.simplify.unfold lt. rewrite > times_n_SO. apply le_times. change with (O < nth_prime i). @@ -175,7 +175,7 @@ apply lt_O_nth_prime_n. change with (O < exp (nth_prime i) n). apply lt_O_exp. apply lt_O_nth_prime_n. -simplify. +simplify.unfold lt. rewrite > times_n_SO. apply le_times. change with (O < exp (nth_prime i) n). @@ -187,7 +187,7 @@ qed. theorem lt_SO_defactorize_aux: \forall f:nat_fact.\forall i:nat. S O < defactorize_aux f i. -intro.elim f.simplify. +intro.elim f.simplify.unfold lt. rewrite > times_n_SO. apply le_times. change with (S O < nth_prime i). @@ -195,7 +195,7 @@ apply lt_SO_nth_prime_n. change with (O < exp (nth_prime i) n). apply lt_O_exp. apply lt_O_nth_prime_n. -simplify. +simplify.unfold lt. rewrite > times_n_SO. rewrite > sym_times. apply le_times. @@ -233,7 +233,7 @@ rewrite < Hcut.reflexivity. 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). +unfold Not. 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). @@ -251,11 +251,11 @@ 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. +simplify.unfold lt.apply le_S_S.apply le_O_n. 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. +unfold Not.intro. cut (O=n1). apply (not_le_Sn_O O). rewrite > Hcut3 in \vdash (? ? %). @@ -309,14 +309,14 @@ 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))). -simplify.apply le_S_S.apply le_S_S. apply le_O_n. +unfold lt.apply le_S_S.apply le_S_S. apply le_O_n. cut ((S(S m1)) = r). rewrite > Hcut3 in \vdash (? (? ? %)). 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 lt_SO_nth_prime_n. -simplify.apply le_S_S.apply le_O_n.apply le_n. +unfold lt.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 (? ? ? %). @@ -330,18 +330,18 @@ 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). -simplify.apply le_S_S. apply le_O_n. +unfold lt.apply le_S_S. apply le_O_n. apply le_n. assumption.assumption. 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. +simplify.unfold lt.apply le_S_S.apply le_O_n. 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. +unfold Not.intro. apply (not_le_Sn_O O). rewrite > H3 in \vdash (? ? %).assumption.assumption. apply (le_to_or_lt_eq r (S O)). @@ -406,11 +406,11 @@ theorem divides_exp_to_eq: \forall p,q,m:nat. prime p \to prime q \to p \divides q \sup m \to p = q. intros. -simplify in H1. +unfold prime in H1. elim H1.apply H4. apply (divides_exp_to_divides p q m). assumption.assumption. -simplify in H.elim H.assumption. +unfold prime in H.elim H.assumption. qed. theorem not_divides_defactorize_aux: \forall f:nat_fact. \forall i,j:nat. @@ -442,7 +442,7 @@ 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. +apply (trans_lt ? j).assumption.unfold lt.apply le_n. assumption. apply divides_times_to_divides. apply prime_nth_prime.assumption. @@ -473,10 +473,10 @@ qed. lemma not_eq_nf_cons_O_nf_cons: \forall f,g:nat_fact.\forall n,i:nat. \lnot (defactorize_aux (nf_cons O f) i= defactorize_aux (nf_cons (S n) g) i). intros. -simplify.rewrite < plus_n_O. +simplify.unfold Not.rewrite < plus_n_O. intro. apply (not_divides_defactorize_aux f i (S i) ?). -simplify.apply le_n. +unfold lt.apply le_n. rewrite > H. rewrite > assoc_times. apply (witness ? ? ((exp (nth_prime i) n)*(defactorize_aux g (S i)))). diff --git a/helm/matita/library/nat/fermat_little_theorem.ma b/helm/matita/library/nat/fermat_little_theorem.ma index bbd5e359a..cc18a8bb9 100644 --- a/helm/matita/library/nat/fermat_little_theorem.ma +++ b/helm/matita/library/nat/fermat_little_theorem.ma @@ -25,7 +25,7 @@ unfold S_mod. apply le_S_S_to_le. change with ((S i) \mod (S n) < S n). apply lt_mod_m_m. -simplify.apply le_S_S.apply le_O_n. +unfold lt.apply le_S_S.apply le_O_n. unfold injn.intros. apply inj_S. rewrite < (lt_to_eq_mod i (S n)). @@ -37,14 +37,14 @@ elim Hcut1. (* i < n, j< n *) rewrite < mod_S. rewrite < mod_S. -apply H2.simplify.apply le_S_S.apply le_O_n. +apply H2.unfold lt.apply le_S_S.apply le_O_n. rewrite > lt_to_eq_mod. -simplify.apply le_S_S.assumption. -simplify.apply le_S_S.assumption. -simplify.apply le_S_S.apply le_O_n. +unfold lt.apply le_S_S.assumption. +unfold lt.apply le_S_S.assumption. +unfold lt.apply le_S_S.apply le_O_n. rewrite > lt_to_eq_mod. -simplify.apply le_S_S.assumption. -simplify.apply le_S_S.assumption. +unfold lt.apply le_S_S.assumption. +unfold lt.apply le_S_S.assumption. (* i < n, j=n *) unfold S_mod in H2. simplify. @@ -54,11 +54,11 @@ apply sym_eq. rewrite < (mod_n_n (S n)). rewrite < H4 in \vdash (? ? ? (? %?)). rewrite < mod_S.assumption. -simplify.apply le_S_S.apply le_O_n. +unfold lt.apply le_S_S.apply le_O_n. rewrite > lt_to_eq_mod. -simplify.apply le_S_S.assumption. -simplify.apply le_S_S.assumption. -simplify.apply le_S_S.apply le_O_n. +unfold lt.apply le_S_S.assumption. +unfold lt.apply le_S_S.assumption. +unfold lt.apply le_S_S.apply le_O_n. (* i = n, j < n *) elim Hcut1. apply False_ind. @@ -66,19 +66,19 @@ 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. +unfold lt.apply le_S_S.apply le_O_n. rewrite > lt_to_eq_mod. -simplify.apply le_S_S.assumption. -simplify.apply le_S_S.assumption. -simplify.apply le_S_S.apply le_O_n. +unfold lt.apply le_S_S.assumption. +unfold lt.apply le_S_S.assumption. +unfold lt.apply le_S_S.apply le_O_n. (* i = n, j= n*) rewrite > H3. rewrite > H4. reflexivity. apply le_to_or_lt_eq.assumption. apply le_to_or_lt_eq.assumption. -simplify.apply le_S_S.assumption. -simplify.apply le_S_S.assumption. +unfold lt.apply le_S_S.assumption. +unfold lt.apply le_S_S.assumption. qed. (* @@ -95,19 +95,19 @@ 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. +intros 3.elim n.unfold Not.intros. apply (lt_to_not_le (S O) p). unfold prime in H.elim H. -assumption.apply divides_to_le.simplify.apply le_n. +assumption.apply divides_to_le.unfold lt.apply le_n. assumption. 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). assumption. -apply divides_to_le.simplify.apply le_S_S.apply le_O_n. +apply divides_to_le.unfold lt.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)).unfold lt. apply le_n. assumption.assumption. apply divides_times_to_divides. assumption.assumption. @@ -120,19 +120,19 @@ split.intros.apply le_S_S_to_le. 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))). +unfold prime in H.elim H. +unfold lt.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)).unfold lt.apply le_n.assumption. unfold injn.intros. apply (nat_compare_elim i j). (* i < j *) intro. absurd (j-i \lt p). -simplify. +unfold lt. rewrite > (S_pred p). apply le_S_S. apply le_plus_to_minus. @@ -141,9 +141,9 @@ rewrite > sym_plus. apply le_plus_n. unfold prime in H. elim H. -apply (trans_lt ? (S O)).simplify.apply le_n.assumption. +apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption. apply (le_to_not_lt p (j-i)). -apply divides_to_le.simplify. +apply divides_to_le.unfold lt. apply le_SO_minus.assumption. cut (divides p a \lor divides p (j-i)). elim Hcut.apply False_ind.apply H1.assumption.assumption. @@ -152,7 +152,7 @@ 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)).unfold lt.apply le_n.assumption. apply sym_eq. apply H4. (* i = j *) @@ -160,7 +160,7 @@ intro. assumption. (* j < i *) intro. absurd (i-j \lt p). -simplify. +unfold lt. rewrite > (S_pred p). apply le_S_S. apply le_plus_to_minus. @@ -169,9 +169,9 @@ rewrite > sym_plus. apply le_plus_n. unfold prime in H. elim H. -apply (trans_lt ? (S O)).simplify.apply le_n.assumption. +apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption. apply (le_to_not_lt p (i-j)). -apply divides_to_le.simplify. +apply divides_to_le.unfold lt. apply le_SO_minus.assumption. cut (divides p a \lor divides p (i-j)). elim Hcut.apply False_ind.apply H1.assumption.assumption. @@ -180,7 +180,7 @@ 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)).unfold lt.apply le_n.assumption. apply H4. qed. @@ -238,7 +238,7 @@ 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)). -simplify.apply le_n.assumption. +unfold lt.apply le_n.assumption. cut (O < a \lor O = a). elim Hcut.assumption. apply False_ind.apply H1. diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma index d42a57e8e..65f61b581 100644 --- a/helm/matita/library/nat/gcd.ma +++ b/helm/matita/library/nat/gcd.ma @@ -136,7 +136,7 @@ intros.change with \land gcd_aux (S m1) m (S m1) \divides (S m1)). apply divides_gcd_aux_mn. -simplify.apply le_S_S.apply le_O_n. +unfold lt.apply le_S_S.apply le_O_n. assumption.apply le_n. simplify.intro. apply (nat_case1 m). @@ -152,8 +152,8 @@ cut (gcd_aux (S m1) n (S m1) \divides n 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. +unfold lt.apply le_S_S.apply le_O_n. +apply not_lt_to_le.unfold Not. unfold lt.intro.apply H. rewrite > H1.apply (trans_le ? (S n)). apply le_n_Sn.assumption.apply le_n. qed. @@ -221,13 +221,13 @@ apply (nat_case1 n).simplify.intros.assumption. intros. 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. +unfold lt.apply le_S_S.apply le_O_n.assumption.apply le_n.assumption. rewrite < H2.assumption. apply (nat_case1 m).simplify.intros.assumption. intros. change with (d \divides gcd_aux (S m1) n (S m1)). apply divides_gcd_aux. -simplify.apply le_S_S.apply le_O_n. +unfold lt.apply le_S_S.apply le_O_n. apply lt_to_le.apply not_le_to_lt.assumption.apply le_n.assumption. rewrite < H2.assumption. qed. @@ -343,7 +343,7 @@ change with 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))). apply eq_minus_gcd_aux. -simplify. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. assumption.apply le_n. apply (nat_case1 m). simplify.intros. @@ -370,7 +370,7 @@ apply (ex_intro ? ? a1). apply (ex_intro ? ? a). left.assumption. apply eq_minus_gcd_aux. -simplify. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. apply lt_to_le.apply not_le_to_lt.assumption. apply le_n. qed. @@ -397,7 +397,7 @@ intros. generalize in match (gcd_O_to_eq_O m n H1). intros.elim H2. rewrite < H4 in \vdash (? ? %).assumption. -intros.simplify.apply le_S_S.apply le_O_n. +intros.unfold lt.apply le_S_S.apply le_O_n. qed. theorem symmetric_gcd: symmetric nat gcd. @@ -435,7 +435,7 @@ intro. apply divides_to_le. apply lt_O_gcd. rewrite > (times_n_O O). -apply lt_times.simplify.apply le_S_S.apply le_O_n.assumption. +apply lt_times.unfold lt.apply le_S_S.apply le_O_n.assumption. apply divides_d_gcd. apply (transitive_divides ? (S m1)). apply divides_gcd_m. @@ -457,7 +457,7 @@ qed. 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 antisym_le.apply divides_to_le.unfold lt.apply le_n. apply divides_gcd_n. cut (O < gcd (S O) n \lor O = gcd (S O) n). elim Hcut.assumption. @@ -502,7 +502,7 @@ 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.unfold prime in H.change with (gcd n m = (S O)). elim H. apply antisym_le. apply not_lt_to_le. @@ -557,8 +557,8 @@ 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. -simplify in H.elim H. assumption. +apply (trans_lt ? (S O)).unfold lt.apply le_n. +unfold prime in H.elim H. assumption. qed. theorem eq_gcd_times_SO: \forall m,n,p:nat. O < n \to O < p \to @@ -576,11 +576,11 @@ rewrite < H2 in \vdash (? ? %). apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))). apply lt_SO_smallest_factor.assumption. apply divides_to_le. -rewrite > H2.simplify.apply le_n. +rewrite > H2.unfold lt.apply le_n. apply divides_d_gcd.assumption. apply (transitive_divides ? (gcd m (n*p))). apply divides_smallest_factor_n. -apply (trans_lt ? (S O)). simplify. apply le_n. assumption. +apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption. apply divides_gcd_n. apply (not_le_Sn_n (S O)). change with ((S O) < (S O)). @@ -588,18 +588,18 @@ rewrite < H3 in \vdash (? ? %). apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))). apply lt_SO_smallest_factor.assumption. apply divides_to_le. -rewrite > H3.simplify.apply le_n. +rewrite > H3.unfold lt.apply le_n. apply divides_d_gcd.assumption. apply (transitive_divides ? (gcd m (n*p))). apply divides_smallest_factor_n. -apply (trans_lt ? (S O)). simplify. apply le_n. assumption. +apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption. apply divides_gcd_n. apply divides_times_to_divides. apply prime_smallest_factor_n. assumption. apply (transitive_divides ? (gcd m (n*p))). apply divides_smallest_factor_n. -apply (trans_lt ? (S O)). simplify. apply le_n. assumption. +apply (trans_lt ? (S O)).unfold lt. apply le_n. assumption. apply divides_gcd_m. change with (O < gcd m (n*p)). apply lt_O_gcd. diff --git a/helm/matita/library/nat/lt_arith.ma b/helm/matita/library/nat/lt_arith.ma index 4897fb598..b8339f374 100644 --- a/helm/matita/library/nat/lt_arith.ma +++ b/helm/matita/library/nat/lt_arith.ma @@ -21,7 +21,7 @@ theorem monotonic_lt_plus_r: \forall n:nat.monotonic nat lt (\lambda m.n+m). simplify.intros. elim n.simplify.assumption. -simplify. +simplify.unfold lt. apply le_S_S.assumption. qed. @@ -51,7 +51,7 @@ intro.elim n. rewrite > plus_n_O. rewrite > (plus_n_O q).assumption. apply H. -simplify.apply le_S_S_to_le. +unfold lt.apply le_S_S_to_le. rewrite > plus_n_Sm. rewrite > (plus_n_Sm q). exact H1. @@ -65,7 +65,7 @@ qed. (* times and zero *) theorem lt_O_times_S_S: \forall n,m:nat.O < (S n)*(S m). -intros.simplify.apply le_S_S.apply le_O_n. +intros.simplify.unfold lt.apply le_S_S.apply le_O_n. qed. (* times *) @@ -172,7 +172,7 @@ rewrite < sym_times. rewrite < div_mod. rewrite > H2. assumption. -simplify.apply le_S_S.apply le_O_n. +unfold lt.apply le_S_S.apply le_O_n. qed. theorem lt_div_n_m_n: \forall n,m:nat. (S O) < m \to O < n \to n / m \lt n. @@ -184,7 +184,7 @@ 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. +simplify.unfold lt. rewrite < plus_n_O. rewrite < plus_n_Sm. apply le_S_S. @@ -195,13 +195,13 @@ assumption. rewrite < sym_plus. apply le_plus_n. apply (trans_lt ? (S O)). -simplify. apply le_n.assumption. +unfold lt. apply le_n.assumption. qed. (* general properties of functions *) theorem monotonic_to_injective: \forall f:nat\to nat. monotonic nat lt f \to injective nat nat f. -simplify.intros. +unfold injective.intros. 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. diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma index 00a90acd8..710418d72 100644 --- a/helm/matita/library/nat/minus.ma +++ b/helm/matita/library/nat/minus.ma @@ -170,7 +170,7 @@ 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. -simplify.apply le_S_S.apply le_minus_m. +simplify.unfold lt.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. @@ -230,14 +230,14 @@ theorem lt_minus_to_plus: \forall n,m,p. (lt n (p-m)) \to (lt (n+m) p). intros 3.apply (nat_elim2 (\lambda m,p.(lt n (p-m)) \to (lt (n+m) p))). intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption. simplify.intros.apply False_ind.apply (not_le_Sn_O n H). -simplify.intros. +simplify.intros.unfold lt. apply le_S_S. rewrite < plus_n_Sm. apply H.apply H1. qed. theorem distributive_times_minus: distributive nat times minus. -simplify. +unfold distributive. intros. apply ((leb_elim z y)). intro.cut (x*(y-z)+x*z = (x*y-x*z)+x*z). diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma index fb7d1686e..a75032d71 100644 --- a/helm/matita/library/nat/nat.ma +++ b/helm/matita/library/nat/nat.ma @@ -30,7 +30,7 @@ intros. reflexivity. qed. theorem injective_S : injective nat nat S. -simplify. +unfold injective. intros. rewrite > pred_Sn. rewrite > (pred_Sn y). @@ -42,7 +42,7 @@ theorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m theorem not_eq_S : \forall n,m:nat. \lnot n=m \to S n \neq S m. -intros. simplify. intros. +intros. unfold Not. intros. apply H. apply injective_S. assumption. qed. @@ -53,7 +53,7 @@ definition not_zero : nat \to Prop \def | (S p) \Rightarrow True ]. theorem not_eq_O_S : \forall n:nat. O \neq S n. -intros. simplify. intros. +intros. unfold Not. intros. cut (not_zero O). exact Hcut. rewrite > H.exact I. @@ -91,7 +91,7 @@ intros.apply H2. apply H3. qed. theorem decidable_eq_nat : \forall n,m:nat.decidable (n=m). -intros.simplify. +intros.unfold decidable. apply (nat_elim2 (\lambda n,m.(Or (n=m) ((n=m) \to False)))). intro.elim n1. left.reflexivity. diff --git a/helm/matita/library/nat/nth_prime.ma b/helm/matita/library/nat/nth_prime.ma index 5fa636301..5330f52ad 100644 --- a/helm/matita/library/nat/nth_prime.ma +++ b/helm/matita/library/nat/nth_prime.ma @@ -45,10 +45,10 @@ 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!))). apply lt_SO_smallest_factor. -simplify.apply le_S_S.apply le_SO_fact. +unfold lt.apply le_S_S.apply le_SO_fact. assumption. apply divides_smallest_factor_n. -simplify.apply le_S_S.apply le_O_n. +unfold lt.apply le_S_S.apply le_O_n. qed. theorem ex_prime: \forall n. (S O) \le n \to \exists m. @@ -66,7 +66,7 @@ apply le_smallest_factor_n. apply prime_smallest_factor_n. change with ((S(S O)) \le S (S n1)!). apply le_S.apply le_SSO_fact. -simplify.apply le_S_S.assumption. +unfold lt.apply le_S_S.assumption. qed. let rec nth_prime n \def @@ -147,14 +147,14 @@ apply increasing_nth_prime. qed. theorem lt_SO_nth_prime_n : \forall n:nat. (S O) \lt nth_prime n. -intros. elim n.simplify.apply le_n. +intros. elim n.unfold lt.apply le_n. 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)). -simplify. apply le_n.apply lt_SO_nth_prime_n. +unfold lt. apply le_n.apply lt_SO_nth_prime_n. qed. theorem ex_m_le_n_nth_prime_m: @@ -195,6 +195,6 @@ 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. +simplify.unfold prime in H.elim H.assumption. qed. diff --git a/helm/matita/library/nat/ord.ma b/helm/matita/library/nat/ord.ma index b982accb3..24874c08a 100644 --- a/helm/matita/library/nat/ord.ma +++ b/helm/matita/library/nat/ord.ma @@ -167,7 +167,7 @@ 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)).unfold lt.apply le_n. assumption.assumption.assumption. apply le_S_S_to_le. apply (trans_le ? n1).change with (n1 / m < n1). @@ -175,9 +175,7 @@ apply lt_div_n_m_n.assumption.assumption.assumption. intros. change with (n1 \mod m \neq O). rewrite > H4. -(* Andrea: META NOT FOUND !!! -rewrite > sym_eq. *) -simplify.intro. +unfold Not.intro. 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 0ddd4b5c5..6ec0c9992 100644 --- a/helm/matita/library/nat/orders.ma +++ b/helm/matita/library/nat/orders.ma @@ -54,7 +54,7 @@ interpretation "natural 'not greater than'" 'ngtr x y = (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/orders/gt.con x y)). theorem transitive_le : transitive nat le. -simplify.intros.elim H1. +unfold transitive.intros.elim H1. assumption. apply le_S.assumption. qed. @@ -63,7 +63,7 @@ theorem trans_le: \forall n,m,p:nat. n \leq m \to m \leq p \to n \leq p \def transitive_le. theorem transitive_lt: transitive nat lt. -simplify.intros.elim H1. +unfold transitive.unfold lt.intros.elim H1. apply le_S. assumption. apply le_S.assumption. 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.unfold Not.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.unfold Not.simplify.intros.cut (S n1 \leq n1). apply H.assumption. apply le_S_S_to_le.assumption. qed. @@ -119,19 +119,19 @@ theorem le_to_or_lt_eq : \forall n,m:nat. n \leq m \to n < m \lor n = m. intros.elim H. right.reflexivity. -left.simplify.apply le_S_S.assumption. +left.unfold lt.apply le_S_S.assumption. qed. (* not eq *) theorem lt_to_not_eq : \forall n,m:nat. n (not_eq_to_eqb_false k i). rewrite > (eqb_n_n k). simplify.reflexivity. -simplify.intro.apply H1.apply sym_eq.assumption. +unfold Not.intro.apply H1.apply sym_eq.assumption. assumption. -simplify.intro.apply H2.apply (trans_eq ? ? n). +unfold Not.intro.apply H2.apply (trans_eq ? ? n). apply sym_eq.assumption.assumption. intro.apply (eqb_elim n k).intro. simplify. @@ -210,7 +210,7 @@ rewrite > (not_eq_to_eqb_false i j). simplify. rewrite > (eqb_n_n i). simplify.assumption. -simplify.intro.apply H.apply sym_eq.assumption. +unfold Not.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). @@ -225,7 +225,7 @@ theorem permut_S_to_permut_transpose: \forall f:nat \to nat. (f n)) m. unfold permut.intros. elim H. -split.intros.simplify. +split.intros.simplify.unfold transpose. apply (eqb_elim (f i) (f (S m))). intro.apply False_ind. cut (i = (S m)). @@ -310,7 +310,7 @@ qed. theorem bijn_transpose : \forall n,i,j. i \le n \to j \le n \to bijn (transpose i j) n. -intros.simplify.intros. +intros.unfold bijn.unfold transpose.intros. cut (m = i \lor \lnot m = i). elim Hcut. apply (ex_intro ? ? j). @@ -354,7 +354,7 @@ 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. +elim n.unfold bijn.intros. apply (ex_intro ? ? m). split.assumption. apply (le_n_O_elim m ? (\lambda p. f p = p)). @@ -370,7 +370,7 @@ elim H1.apply H2.apply le_n.apply le_n. apply bijn_n_Sn. apply H. apply permut_S_to_permut_transpose. -assumption.simplify. +assumption.unfold transpose. rewrite > (eqb_n_n (f (S n1))).simplify.reflexivity. qed. @@ -395,9 +395,9 @@ simplify. 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). +unfold Not.intro.absurd (m = S n1). apply H3.apply le_S.assumption.apply le_n.assumption. -simplify.intro. +unfold Not.intro. apply (not_le_Sn_n n1).rewrite < H5.assumption. qed. @@ -552,15 +552,15 @@ rewrite < H. rewrite < (H1 (g (S m + n))). apply eq_f. apply eq_map_iter_i. -intros.unfold transpose. +intros.simplify.unfold transpose. 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)). -simplify.apply le_S_S.apply le_S.assumption. +apply (lt_to_not_eq m1 (S ((S m)+n))). +unfold lt.apply le_S_S.change with (m1 \leq S (m+n)).apply le_S.assumption. apply (lt_to_not_eq m1 (S m+n)). -simplify.apply le_S_S.assumption. +simplify.unfold lt.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 @@ -579,11 +579,11 @@ 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)). simplify.reflexivity. -simplify.intro. +simplify.unfold Not.intro. 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. +simplify.unfold Not.intro. +apply (lt_to_not_eq i (S (S n1+n))).simplify.unfold lt. apply le_S_S.assumption. apply sym_eq. assumption. apply H2.assumption.apply le_S_S_to_le. @@ -608,13 +608,13 @@ 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 H2. -simplify. apply le_n.assumption. +unfold lt. apply le_n.assumption. 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))). -simplify.apply le_S_S.apply le_O_n. +unfold lt.apply le_S_S.apply le_O_n. apply (trans_le ? i).assumption. change with (i \le (S m1)+i).apply le_plus_n. exact H4. @@ -623,23 +623,23 @@ apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g (transpose (S(m1 + i)) (S(S(m1 + i))) (transpose i (S(m1 + i)) m)))) f n)). apply (H2 m1). -simplify. apply le_n.assumption. +unfold lt. apply le_n.assumption. 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. +unfold Not. intro. apply (not_le_Sn_n i). rewrite < H7 in \vdash (? ? %). apply le_S_S.apply le_S. apply le_plus_n. -simplify. intro. +unfold Not. intro. apply (not_le_Sn_n i). rewrite > H7 in \vdash (? ? %). apply le_S_S. apply le_plus_n. -simplify. intro. +unfold Not. intro. apply (not_eq_n_Sn (S m1+i)). apply sym_eq.assumption. qed. @@ -726,11 +726,11 @@ 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. -simplify.apply le_S_S.apply le_plus_n.assumption. +simplify.unfold lt.apply le_S_S.apply le_plus_n.assumption. unfold permut in H3.elim H3. -simplify.intro. +simplify.unfold Not.intro. apply (lt_to_not_eq m (S n+n1)).apply (trans_lt ? n1).assumption. -simplify.apply le_S_S.apply le_plus_n. +simplify.unfold lt.apply le_S_S.apply le_plus_n. unfold injn in H7. apply (H7 m (S n+n1)).apply (trans_le ? n1). apply lt_to_le.assumption.apply le_plus_n.apply le_n. diff --git a/helm/matita/library/nat/plus.ma b/helm/matita/library/nat/plus.ma index 8043d9a52..d595dad19 100644 --- a/helm/matita/library/nat/plus.ma +++ b/helm/matita/library/nat/plus.ma @@ -43,7 +43,7 @@ simplify.rewrite > H.apply plus_n_Sm. qed. theorem associative_plus : associative nat plus. -simplify.intros.elim x. +unfold associative.intros.elim x. simplify.reflexivity. simplify.apply eq_f.assumption. qed. diff --git a/helm/matita/library/nat/primes.ma b/helm/matita/library/nat/primes.ma index 452adc89c..50b7d1221 100644 --- a/helm/matita/library/nat/primes.ma +++ b/helm/matita/library/nat/primes.ma @@ -27,7 +27,7 @@ interpretation "not divides" 'ndivides n m = (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/primes/divides.ind#xpointer(1/1) n m)). theorem reflexive_divides : reflexive nat divides. -simplify. +unfold reflexive. intros. exact (witness x x (S O) (times_n_SO x)). qed. @@ -151,7 +151,7 @@ apply (decidable_le n m). qed. theorem antisymmetric_divides: antisymmetric nat divides. -simplify.intros.elim H. elim H1. +unfold antisymmetric.intros.elim H. elim H1. apply (nat_case1 n2).intro. rewrite > H3.rewrite > H2.rewrite > H4. rewrite < times_n_O.reflexivity. @@ -206,7 +206,7 @@ match eqb (m \mod n) O with | false \Rightarrow n \ndivides m]. apply eqb_elim. intro.simplify.apply mod_O_to_divides.assumption.assumption. -intro.simplify.intro.apply H1.apply divides_to_mod_O.assumption.assumption. +intro.simplify.unfold Not.intro.apply H1.apply divides_to_mod_O.assumption.assumption. qed. theorem divides_b_true_to_divides : @@ -339,11 +339,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). +unfold Not.unfold prime.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). +unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_n (S O) H1). qed. (* smallest factor *) @@ -390,10 +390,10 @@ 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. -simplify.apply le_n. +simplify.unfold lt.apply le_n. intros.apply (trans_lt ? (S O)). -simplify. apply le_n. -apply lt_SO_smallest_factor.simplify. apply le_S_S. +unfold lt.apply le_n. +apply lt_SO_smallest_factor.unfold lt. apply le_S_S. apply le_S_S.apply le_O_n. qed. @@ -414,7 +414,7 @@ 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)).unfold lt. apply le_S_S.apply le_S_S.apply le_O_n. qed. @@ -423,9 +423,9 @@ theorem le_smallest_factor_n : 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. +unfold lt.apply le_S_S.apply le_O_n. apply divides_smallest_factor_n. -simplify.apply le_S_S.apply le_O_n. +unfold lt.apply le_S_S.apply le_O_n. qed. theorem lt_smallest_factor_to_not_divides: \forall n,i:nat. @@ -459,7 +459,7 @@ 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)). unfold lt. apply le_n. exact H. apply lt_smallest_factor_to_not_divides. exact H.assumption.assumption.assumption. apply divides_to_le. @@ -481,7 +481,7 @@ change with 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)).unfold lt. apply le_n.assumption. apply lt_SO_smallest_factor. assumption. qed. @@ -517,8 +517,8 @@ 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.unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_O (S O) H1). +intro.apply (nat_case m).simplify.unfold Not.unfold prime.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 @@ -528,7 +528,7 @@ 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. +unfold lt.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.apply H. diff --git a/helm/matita/library/nat/times.ma b/helm/matita/library/nat/times.ma index 70a4fd76e..2ae5ffd74 100644 --- a/helm/matita/library/nat/times.ma +++ b/helm/matita/library/nat/times.ma @@ -52,7 +52,7 @@ reflexivity. qed. theorem symmetric_times : symmetric nat times. -simplify. +unfold symmetric. intros.elim x. simplify.apply times_n_O. simplify.rewrite > H.apply times_n_Sm. @@ -62,7 +62,7 @@ variant sym_times : \forall n,m:nat. n*m = m*n \def symmetric_times. theorem distributive_times_plus : distributive nat times plus. -simplify. +unfold distributive. intros.elim x. simplify.reflexivity. simplify.rewrite > H. rewrite > assoc_plus.rewrite > assoc_plus. @@ -74,7 +74,7 @@ variant distr_times_plus: \forall n,m,p:nat. n*(m+p) = n*m + n*p \def distributive_times_plus. theorem associative_times: associative nat times. -simplify.intros. +unfold associative.intros. elim x.simplify.apply refl_eq. simplify.rewrite < sym_times. rewrite > distr_times_plus. diff --git a/helm/matita/library/nat/totient.ma b/helm/matita/library/nat/totient.ma index ff425772c..24c3920ed 100644 --- a/helm/matita/library/nat/totient.ma +++ b/helm/matita/library/nat/totient.ma @@ -68,35 +68,35 @@ rewrite < H4. rewrite > sym_gcd. rewrite > gcd_mod. apply (gcd_times_SO_to_gcd_SO ? ? (S m2)). -simplify.apply le_S_S.apply le_O_n. -simplify.apply le_S_S.apply le_O_n. +unfold lt.apply le_S_S.apply le_O_n. +unfold lt.apply le_S_S.apply le_O_n. assumption. -simplify.apply le_S_S.apply le_O_n. +unfold lt.apply le_S_S.apply le_O_n. rewrite < H5. rewrite > sym_gcd. rewrite > gcd_mod. apply (gcd_times_SO_to_gcd_SO ? ? (S m)). -simplify.apply le_S_S.apply le_O_n. -simplify.apply le_S_S.apply le_O_n. +unfold lt.apply le_S_S.apply le_O_n. +unfold lt.apply le_S_S.apply le_O_n. rewrite > sym_times. assumption. -simplify.apply le_S_S.apply le_O_n. +unfold lt.apply le_S_S.apply le_O_n. intro. apply eqb_elim. intro.apply eqb_elim. intro.apply False_ind. apply H6. apply eq_gcd_times_SO. -simplify.apply le_S_S.apply le_O_n. -simplify.apply le_S_S.apply le_O_n. +unfold lt.apply le_S_S.apply le_O_n. +unfold lt.apply le_S_S.apply le_O_n. rewrite < gcd_mod. rewrite > H4. rewrite > sym_gcd.assumption. -simplify.apply le_S_S.apply le_O_n. +unfold lt.apply le_S_S.apply le_O_n. rewrite < gcd_mod. rewrite > H5. rewrite > sym_gcd.assumption. -simplify.apply le_S_S.apply le_O_n. +unfold lt.apply le_S_S.apply le_O_n. intro.reflexivity. intro.reflexivity. qed. \ No newline at end of file diff --git a/helm/matita/tests/simpl.ma b/helm/matita/tests/simpl.ma index 75a1693f4..1001d2351 100644 --- a/helm/matita/tests/simpl.ma +++ b/helm/matita/tests/simpl.ma @@ -28,7 +28,7 @@ theorem a : \forall x,y : A. not (x = y) \to not(y = x). intros. -simplify. +unfold not. (* simplify. *) intro. apply H. symmetry. exact H1. -- 2.39.2