From: Enrico Tassi Date: Fri, 16 Sep 2005 16:15:02 +0000 (+0000) Subject: added a function to reorder the metasenv. X-Git-Tag: LAST_BEFORE_NEW~111 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=78044035b4419e569df0d7f6a7f96fa32d21a19d;p=helm.git added a function to reorder the metasenv. --- diff --git a/helm/matita/library/Makefile b/helm/matita/library/Makefile index 4e85bcccc..8375a61b6 100644 --- a/helm/matita/library/Makefile +++ b/helm/matita/library/Makefile @@ -44,4 +44,5 @@ depend: $(DEPEND_NAME): $(SRC) $(H)$(MATITADEP) $(SRC) > $@ || rm -f $@ -include $(DEPEND_NAME) +#include $(DEPEND_NAME) +include .depend diff --git a/helm/matita/library/Q/q.ma b/helm/matita/library/Q/q.ma index 0e6678dc9..d7c2816a1 100644 --- a/helm/matita/library/Q/q.ma +++ b/helm/matita/library/Q/q.ma @@ -45,11 +45,13 @@ theorem fraction_elim2: (\forall x:Z.\forall f:fraction.\forall m:nat.R (cons x f) (nn m)) \to (\forall x,y:Z.\forall f,g:fraction.R f g \to R (cons x f) (cons y g)) \to \forall f,g:fraction. R f g. -intros 7.elim f.apply H. -elim g.apply H2. -apply H4.apply H5. -apply H3. -apply H1. +intros 7.elim f. + apply H. + apply H1. + elim g. + apply H2. + apply H3. + apply H4.apply H5. qed. (* boolean equality *) @@ -154,27 +156,26 @@ theorem decidable_eq_fraction: \forall f,g:fraction. decidable (f = g). intros.simplify. apply fraction_elim2 (\lambda f,g. Or (f=g) (f=g \to False)). -intros.elim g1. -elim ((decidable_eq_nat n n1) : Or (n=n1) (n=n1 \to False)). -left.apply eq_f. assumption. -right.intro.apply H.apply injective_pp.assumption. -right.apply not_eq_pp_cons. -right.apply not_eq_pp_nn. -intros. elim g1. -right.intro.apply not_eq_pp_nn n1 n ?.apply sym_eq. assumption. -right.apply not_eq_nn_cons. -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. -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. 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. + intros.elim g1. + elim ((decidable_eq_nat n n1) : Or (n=n1) (n=n1 \to False)). + left.apply eq_f. assumption. + right.intro.apply H.apply injective_pp.assumption. + right.apply not_eq_pp_nn. + right.apply not_eq_pp_cons. + intros. elim g1. + right.intro.apply not_eq_pp_nn n1 n ?.apply sym_eq. assumption. + elim ((decidable_eq_nat n n1) : Or (n=n1) (n=n1 \to False)). + left. apply eq_f. assumption. + right.intro.apply H.apply injective_nn.assumption. + right.apply not_eq_nn_cons. + intros.right.intro.apply not_eq_pp_cons m x f1 ?.apply sym_eq.assumption. + intros.right.intro.apply not_eq_nn_cons m x f1 ?.apply sym_eq.assumption. + intros.elim H. + elim ((decidable_eq_Z x y) : Or (x=y) (x=y \to False)). + 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. qed. theorem eqfb_to_Prop: \forall f,g:fraction. @@ -185,33 +186,28 @@ intros.apply fraction_elim2 (\lambda f,g.match (eqfb f g) with [true \Rightarrow f=g |false \Rightarrow \lnot f=g]). -intros.elim g1. -simplify. -apply eqb_elim. -intro.simplify.apply eq_f.assumption. -intro.simplify.intro.apply H.apply injective_pp.assumption. -simplify.apply not_eq_pp_cons. -simplify.apply not_eq_pp_nn. -intros. -elim g1.simplify. -intro.apply not_eq_pp_nn n1 n ?.apply sym_eq. assumption. -simplify.apply not_eq_nn_cons. -simplify.apply eqb_elim. -intro.simplify.apply eq_f.assumption. -intro.simplify.intro.apply H.apply injective_nn.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)). -apply eqZb_elim. -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. + intros.elim g1. + simplify.apply eqb_elim. + intro.simplify.apply eq_f.assumption. + intro.simplify.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.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. + change in match (eqfb (cons x f1) (cons y g1)) + with (andb (eqZb x y) (eqfb f1 g1)). + apply eqZb_elim. + 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. qed. let rec finv f \def @@ -248,54 +244,48 @@ let rec ftimes f g \def | (frac h) \Rightarrow frac (cons (Zplus x y) h)]]]. theorem symmetric2_ftimes: symmetric2 fraction ratio ftimes. -simplify. intros. -apply fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f). -intros.elim g. -change with Z_to_ratio (Zplus (pos n) (pos n1)) = Z_to_ratio (Zplus (pos n1) (pos n)). -apply eq_f.apply sym_Zplus. -change with frac (cons (Zplus (pos n) z) f) = frac (cons (Zplus z (pos n)) f). -rewrite < sym_Zplus.reflexivity. -change with Z_to_ratio (Zplus (pos n) (neg n1)) = Z_to_ratio (Zplus (neg n1) (pos n)). -apply eq_f.apply sym_Zplus. -intros.elim g. -change with Z_to_ratio (Zplus (neg n) (pos n1)) = Z_to_ratio (Zplus (pos n1) (neg n)). -apply eq_f.apply sym_Zplus. -change with frac (cons (Zplus (neg n) z) f) = frac (cons (Zplus z (neg n)) f). -rewrite < sym_Zplus.reflexivity. -change with Z_to_ratio (Zplus (neg n) (neg n1)) = Z_to_ratio (Zplus (neg n1) (neg n)). -apply eq_f.apply sym_Zplus. -intros. -change with frac (cons (Zplus x1 (pos m)) f) = frac (cons (Zplus (pos m) x1) f). -rewrite < sym_Zplus.reflexivity. -intros. -change with frac (cons (Zplus x1 (neg m)) f) = frac (cons (Zplus (neg m) x1) f). -rewrite < sym_Zplus.reflexivity. -intros. -change with - match ftimes f g with - [ one \Rightarrow Z_to_ratio (Zplus x1 y1) - | (frac h) \Rightarrow frac (cons (Zplus x1 y1) h)] = - match ftimes g f with - [ one \Rightarrow Z_to_ratio (Zplus y1 x1) - | (frac h) \Rightarrow frac (cons (Zplus y1 x1) h)]. -rewrite < H.rewrite < sym_Zplus. -reflexivity. +simplify. intros.apply fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f). + intros.elim g. + change with Z_to_ratio (Zplus (pos n) (pos n1)) = Z_to_ratio (Zplus (pos n1) (pos n)). + apply eq_f.apply sym_Zplus. + change with Z_to_ratio (Zplus (pos n) (neg n1)) = Z_to_ratio (Zplus (neg n1) (pos n)). + apply eq_f.apply sym_Zplus. + change with frac (cons (Zplus (pos n) z) f) = frac (cons (Zplus z (pos n)) f). + rewrite < sym_Zplus.reflexivity. + intros.elim g. + change with Z_to_ratio (Zplus (neg n) (pos n1)) = Z_to_ratio (Zplus (pos n1) (neg n)). + apply eq_f.apply sym_Zplus. + change with Z_to_ratio (Zplus (neg n) (neg n1)) = Z_to_ratio (Zplus (neg n1) (neg n)). + apply eq_f.apply sym_Zplus. + change with frac (cons (Zplus (neg n) z) f) = frac (cons (Zplus z (neg n)) f). + rewrite < sym_Zplus.reflexivity. + intros.change with frac (cons (Zplus x1 (pos m)) f) = frac (cons (Zplus (pos m) x1) f). + rewrite < sym_Zplus.reflexivity. + intros.change with frac (cons (Zplus x1 (neg m)) f) = frac (cons (Zplus (neg m) x1) f). + rewrite < sym_Zplus.reflexivity. + intros. + change with + match ftimes f g with + [ one \Rightarrow Z_to_ratio (Zplus x1 y1) + | (frac h) \Rightarrow frac (cons (Zplus x1 y1) h)] = + match ftimes g f with + [ one \Rightarrow Z_to_ratio (Zplus y1 x1) + | (frac h) \Rightarrow frac (cons (Zplus y1 x1) h)]. + rewrite < H.rewrite < sym_Zplus.reflexivity. qed. theorem ftimes_finv : \forall f:fraction. ftimes f (finv f) = one. -intro. -elim f. -change with Z_to_ratio (Zplus (pos n) (Zopp (pos n))) = one. -rewrite > Zplus_Zopp.reflexivity. +intro.elim f. + change with Z_to_ratio (Zplus (pos n) (Zopp (pos n))) = one. + rewrite > Zplus_Zopp.reflexivity. + change with Z_to_ratio (Zplus (neg n) (Zopp (neg n))) = one. + rewrite > Zplus_Zopp.reflexivity. (* again: we would need something to help finding the right change *) -change with -match ftimes f1 (finv f1) with - [ one \Rightarrow Z_to_ratio (Zplus z (Zopp z)) - | (frac h) \Rightarrow frac (cons (Zplus z (Zopp z)) h)] = one. -rewrite > H. -rewrite > Zplus_Zopp.reflexivity. -change with Z_to_ratio (Zplus (neg n) (Zopp (neg n))) = one. -rewrite > Zplus_Zopp.reflexivity. + change with + match ftimes f1 (finv f1) with + [ one \Rightarrow Z_to_ratio (Zplus z (Zopp z)) + | (frac h) \Rightarrow frac (cons (Zplus z (Zopp z)) h)] = one. + rewrite > H.rewrite > Zplus_Zopp.reflexivity. qed. definition rtimes : ratio \to ratio \to ratio \def diff --git a/helm/matita/library/Z/compare.ma b/helm/matita/library/Z/compare.ma index 4ae6dd2c4..a8f8aca39 100644 --- a/helm/matita/library/Z/compare.ma +++ b/helm/matita/library/Z/compare.ma @@ -44,21 +44,24 @@ theorem eqZb_to_Prop: match eqZb x y with [ true \Rightarrow x=y | false \Rightarrow \lnot x=y]. -intros.elim x. -elim y. -simplify.reflexivity. -simplify.apply not_eq_OZ_neg. -simplify.apply not_eq_OZ_pos. -elim y. -simplify.intro.apply not_eq_OZ_neg n ?.apply sym_eq.assumption. -simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption. -intro.simplify.intro.apply H.apply inj_neg.assumption. -simplify.intro.apply not_eq_pos_neg n1 n ?.apply sym_eq.assumption. -elim y. -simplify.intro.apply not_eq_OZ_pos n ?.apply sym_eq.assumption. -simplify.apply not_eq_pos_neg. -simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption. -intro.simplify.intro.apply H.apply inj_pos.assumption. +intros. +elim x. + elim y. + simplify.reflexivity. + 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.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.apply eqb_elim. + intro.simplify.apply eq_f.assumption. + intro.simplify.intro.apply H.apply inj_neg.assumption. qed. theorem eqZb_elim: \forall x,y:Z.\forall P:bool \to Prop. @@ -100,40 +103,43 @@ theorem Z_compare_to_Prop : | EQ \Rightarrow x=y | GT \Rightarrow y < x]. intros. -elim x. elim y. -simplify.apply refl_eq. -simplify.exact I. -simplify.exact I. -elim y. simplify.exact I. -simplify. -cut match (nat_compare n1 n) with -[ LT \Rightarrow n1 Zsucc_Zpred.reflexivity. -elim y.rewrite < sym_Zplus.rewrite < sym_Zplus (Zpred OZ). -rewrite < Zpred_Zplus_neg_O. -rewrite > Zpred_Zsucc. -simplify.reflexivity. -rewrite < Zplus_neg_neg.reflexivity. -apply Zplus_neg_pos. -elim y.simplify.reflexivity. -apply Zplus_pos_neg. -apply Zplus_pos_pos. +intros.elim x. + elim y. + simplify.reflexivity. + rewrite < Zsucc_Zplus_pos_O.rewrite > Zsucc_Zpred.reflexivity. + simplify.reflexivity. + elim y. + simplify.reflexivity. + apply Zplus_pos_pos. + apply Zplus_pos_neg. + elim y. + rewrite < sym_Zplus.rewrite < sym_Zplus (Zpred OZ). + rewrite < Zpred_Zplus_neg_O.rewrite > Zpred_Zsucc.simplify.reflexivity. + apply Zplus_neg_pos. + rewrite < Zplus_neg_neg.reflexivity. qed. theorem Zplus_Zsucc_pos_pos : @@ -204,17 +205,19 @@ reflexivity. qed. theorem Zplus_Zsucc : \forall x,y:Z. (Zsucc x)+y = Zsucc (x+y). -intros.elim x.elim y. -simplify. reflexivity. -rewrite < Zsucc_Zplus_pos_O.reflexivity. -simplify.reflexivity. -elim y.rewrite < sym_Zplus.rewrite < sym_Zplus OZ.simplify.reflexivity. -apply Zplus_Zsucc_neg_neg. -apply Zplus_Zsucc_neg_pos. -elim y. -rewrite < sym_Zplus OZ.reflexivity. -apply Zplus_Zsucc_pos_neg. -apply Zplus_Zsucc_pos_pos. +intros.elim x. + elim y. + simplify. reflexivity. + simplify.reflexivity. + rewrite < Zsucc_Zplus_pos_O.reflexivity. + elim y. + 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. + apply Zplus_Zsucc_neg_pos. + apply Zplus_Zsucc_neg_neg. qed. theorem Zplus_Zpred: \forall x,y:Z. (Zpred x)+y = Zpred (x+y). @@ -232,23 +235,18 @@ qed. theorem associative_Zplus: associative Z Zplus. change with \forall x,y,z:Z. (x + y) + z = x + (y + z). (* simplify. *) -intros.elim x.simplify.reflexivity. -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. -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. +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. + 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. 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 688957e57..72e8177b8 100644 --- a/helm/matita/library/Z/times.ma +++ b/helm/matita/library/Z/times.ma @@ -70,58 +70,60 @@ variant sym_Ztimes : \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x) theorem associative_Ztimes: associative Z Ztimes. change with \forall x,y,z:Z.eq Z (Ztimes (Ztimes x y) z) (Ztimes x (Ztimes y z)). -intros. -elim x.simplify.reflexivity. -elim y.simplify.reflexivity. -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. -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. -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. -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. -apply lt_O_times_S_S. -apply lt_O_times_S_S. -elim y.simplify.reflexivity. -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. -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. -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. -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. -apply lt_O_times_S_S. -apply lt_O_times_S_S. +intros.elim x. + simplify.reflexivity. + elim y. + simplify.reflexivity. + 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. + 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. + 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. + 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. + apply lt_O_times_S_S.apply lt_O_times_S_S. + elim y. + simplify.reflexivity. + 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. + 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. + 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. + 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. + apply lt_O_times_S_S.apply lt_O_times_S_S. qed. variant assoc_Ztimes : \forall x,y,z:Z. @@ -183,21 +185,22 @@ lemma distributive2_Ztimes_pos_Zplus: distributive2 nat Z (\lambda n,z. Ztimes (pos n) z) Zplus. change with \forall n,y,z. eq Z (Ztimes (pos n) (Zplus y z)) (Zplus (Ztimes (pos n) y) (Ztimes (pos n) z)). -intros. -elim y.reflexivity. -elim z.reflexivity. -change with -eq Z (neg (pred (times (S n) (plus (S n1) (S n2))))) +intros.elim y. + reflexivity. + elim z. + reflexivity. + change with + eq Z (pos (pred (times (S n) (plus (S n1) (S n2))))) + (pos (pred (plus (times (S n) (S n1))(times (S n) (S n2))))). + rewrite < distr_times_plus.reflexivity. + apply Ztimes_Zplus_pos_pos_neg. + elim z. + reflexivity. + apply Ztimes_Zplus_pos_neg_pos. + change with + eq Z (neg (pred (times (S n) (plus (S n1) (S n2))))) (neg (pred (plus (times (S n) (S n1))(times (S n) (S n2))))). -rewrite < distr_times_plus.reflexivity. -apply Ztimes_Zplus_pos_neg_pos. -elim z.reflexivity. -apply Ztimes_Zplus_pos_pos_neg. -change with -eq Z (pos (pred (times (S n) (plus (S n1) (S n2))))) - (pos (pred (plus (times (S n) (S n1))(times (S n) (S n2))))). -rewrite < distr_times_plus. -reflexivity. + rewrite < distr_times_plus.reflexivity. qed. variant distr_Ztimes_Zplus_pos: \forall n,y,z. @@ -226,10 +229,10 @@ eq Z (Ztimes x (Zplus y z)) (Zplus (Ztimes x y) (Ztimes x z)). intros.elim x. (* case x = OZ *) simplify.reflexivity. -(* case x = neg n *) -apply distr_Ztimes_Zplus_neg. (* case x = pos n *) apply distr_Ztimes_Zplus_pos. +(* case x = neg n *) +apply distr_Ztimes_Zplus_neg. qed. variant distr_Ztimes_Zplus: \forall x,y,z. diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma index a5e0fba8f..207457a91 100644 --- a/helm/matita/library/Z/z.ma +++ b/helm/matita/library/Z/z.ma @@ -54,18 +54,10 @@ match OZ_test z with |false \Rightarrow \lnot (z=OZ)]. intros.elim z. simplify.reflexivity. -simplify.intros. -cut match neg n with -[ OZ \Rightarrow True -| (pos n) \Rightarrow False -| (neg n) \Rightarrow False]. -apply Hcut.rewrite > H.simplify.exact I. -simplify.intros. -cut match pos n with -[ OZ \Rightarrow True -| (pos n) \Rightarrow False -| (neg n) \Rightarrow False]. -apply Hcut. rewrite > H.simplify.exact I. +simplify.intros [H]. +discriminate H. +simplify.intros [H]. +discriminate H. qed. (* discrimination *) @@ -90,56 +82,53 @@ 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. \lnot (OZ = (pos n)). -simplify.intros. -change with - match pos n with - [ OZ \Rightarrow True - | (pos n) \Rightarrow False - | (neg n) \Rightarrow False]. -rewrite < H. -simplify.exact I. +simplify.intros [n; H]. +discriminate H. qed. theorem not_eq_OZ_neg :\forall n:nat. \lnot (OZ = (neg n)). -simplify.intros. -change with - match neg n with - [ OZ \Rightarrow True - | (pos n) \Rightarrow False - | (neg n) \Rightarrow False]. -rewrite < H. -simplify.exact I. +simplify.intros [n; H]. +discriminate H. qed. theorem not_eq_pos_neg :\forall n,m:nat. \lnot ((pos n) = (neg m)). -simplify.intros. -change with - match neg m with - [ OZ \Rightarrow False - | (pos n) \Rightarrow True - | (neg n) \Rightarrow False]. -rewrite < H. -simplify.exact I. +simplify.intros [n; m; H]. +discriminate H. qed. theorem decidable_eq_Z : \forall x,y:Z. decidable (x=y). intros.simplify. -elim x.elim y. -left.reflexivity. -right.apply not_eq_OZ_neg. -right.apply not_eq_OZ_pos. -elim y.right.intro. -apply not_eq_OZ_neg 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_neg.assumption. -right.intro.apply not_eq_pos_neg n1 n ?.apply sym_eq.assumption. -elim y.right.intro. -apply not_eq_OZ_pos n ?.apply sym_eq.assumption. -right.apply not_eq_pos_neg. -elim (decidable_eq_nat n n1:(Or (n=n1) ((n=n1) \to False))). -left.apply eq_f.assumption. -right.intro.apply H.apply injective_pos.assumption. +elim x. +(* goal: x=OZ *) + elim y. + (* goal: x=OZ y=OZ *) + left.reflexivity. + (* goal: x=OZ 2=2 *) + right.apply not_eq_OZ_pos. + (* goal: x=OZ 2=3 *) + right.apply not_eq_OZ_neg. +(* goal: x=pos *) + elim y. + (* goal: x=pos y=OZ *) + right.intro. + apply not_eq_OZ_pos n. symmetry. assumption. + (* goal: x=pos y=pos *) + elim (decidable_eq_nat n n1:(Or (n=n1) ((n=n1) \to False))). + left.apply eq_f.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. +(* goal: x=neg *) + elim y. + (* goal: x=neg y=OZ *) + right.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. + (* goal: x=neg y=neg *) + elim (decidable_eq_nat n n1:(Or (n=n1) ((n=n1) \to False))). + left.apply eq_f.assumption. + right.intro.apply H.apply injective_neg.assumption. qed. (* end discrimination *) @@ -163,16 +152,22 @@ definition Zpred \def | (neg n) \Rightarrow neg (S n)]. theorem Zpred_Zsucc: \forall z:Z. Zpred (Zsucc z) = z. -intros.elim z.reflexivity. -elim n.reflexivity. -reflexivity. -reflexivity. +intros. +elim z. + reflexivity. + reflexivity. + elim n. + reflexivity. + reflexivity. qed. theorem Zsucc_Zpred: \forall z:Z. Zsucc (Zpred z) = z. -intros.elim z.reflexivity. -reflexivity. -elim n.reflexivity. -reflexivity. +intros. +elim z. + reflexivity. + elim n. + reflexivity. + reflexivity. + reflexivity. qed. diff --git a/helm/matita/library/nat/compare.ma b/helm/matita/library/nat/compare.ma index 852cd7b65..443c6657f 100644 --- a/helm/matita/library/nat/compare.ma +++ b/helm/matita/library/nat/compare.ma @@ -154,8 +154,8 @@ 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). simplify. apply le_S_S.apply H. -simplify. apply le_S_S.apply H. simplify. apply eq_f. apply H. +simplify. apply le_S_S.apply H. qed. theorem nat_compare_n_m_m_n: \forall n,m:nat. @@ -181,6 +181,6 @@ cut match (nat_compare n m) with apply Hcut.apply nat_compare_to_Prop. elim (nat_compare n m). apply (H H3). -apply (H2 H3). apply (H1 H3). +apply (H2 H3). qed. diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma index e4645c307..73f90e553 100644 --- a/helm/matita/library/nat/div_and_mod.ma +++ b/helm/matita/library/nat/div_and_mod.ma @@ -195,6 +195,7 @@ qed. theorem div_times: \forall n,m:nat. div ((S n)*m) (S n) = m. 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. apply div_mod_spec_times. diff --git a/helm/matita/library/nat/factorization.ma b/helm/matita/library/nat/factorization.ma index 30174d770..a3a715228 100644 --- a/helm/matita/library/nat/factorization.ma +++ b/helm/matita/library/nat/factorization.ma @@ -189,9 +189,6 @@ cut n1 = r*(exp (nth_prime n) q). rewrite > H. simplify.rewrite < assoc_times. rewrite < Hcut.reflexivity. -rewrite > sym_times. -apply plog_aux_to_exp n1 n1. -apply lt_O_nth_prime_n.assumption. cut O < r \lor O = r. elim Hcut1.assumption.absurd n1 = O. rewrite > Hcut.rewrite < H4.reflexivity. @@ -227,6 +224,9 @@ assumption. apply le_to_or_lt_eq r (S O). apply not_lt_to_le.assumption. apply decidable_lt (S O) r. +rewrite > sym_times. +apply plog_aux_to_exp n1 n1. +apply lt_O_nth_prime_n.assumption. qed. theorem defactorize_factorize: \forall n:nat.defactorize (factorize n) = n. @@ -274,35 +274,20 @@ 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 divides_to_mod_O. -apply lt_O_nth_prime_n. -assumption. apply lt_SO_nth_prime_n. -simplify.apply le_S_S.apply le_O_n. -apply le_n. -assumption.rewrite > times_n_SO in \vdash (? ? ? %). +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 > H1 in \vdash (? ? ? (? (? ? %) ?)). assumption. -apply le_to_or_lt_eq.apply le_O_n. -(* O < r *) -cut O < r \lor O = r. -elim Hcut1.assumption. -apply False_ind. -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 *) -apply plog_aux_to_exp (S(S m1)). -apply lt_O_nth_prime_n. -assumption. -(* fine prova cut *) -assumption. -(* e adesso l'ultimo goal *) +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 \lnot (S O) < r. elim Hcut2. -right. +right. apply plog_to_lt_max_prime_factor1 (S(S m1)) ? q r. simplify.apply le_S_S. apply le_O_n. apply le_n. @@ -321,6 +306,19 @@ rewrite > H3 in \vdash (? ? %).assumption.assumption. apply le_to_or_lt_eq r (S O). apply not_lt_to_le.assumption. apply decidable_lt (S O) r. +(* O < r *) +cut O < r \lor O = r. +elim Hcut1.assumption. +apply False_ind. +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 plog_aux_to_exp (S(S m1)). +apply lt_O_nth_prime_n. +assumption. +(* fine prova cut *) qed. let rec max_p f \def @@ -403,7 +401,8 @@ cut i = j. apply not_le_Sn_n i.rewrite > Hcut1 in \vdash (? ? %).assumption. apply injective_nth_prime ? ? H4. apply H i (S j) ?. -assumption.apply trans_lt ? j.assumption.simplify.apply le_n. +apply trans_lt ? j.assumption.simplify.apply le_n. +assumption. apply divides_times_to_divides. apply prime_nth_prime.assumption. qed. @@ -472,23 +471,23 @@ 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) ?. +simplify. apply le_n. simplify in H5. rewrite > plus_n_O (defactorize_aux n1 (S i)). rewrite > H5. rewrite > assoc_times. apply witness ? ? ((exp (nth_prime i) n5)*(defactorize_aux n3 (S i))). reflexivity. -simplify. apply le_n. intros. apply False_ind. 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)). rewrite < H4. rewrite > assoc_times. apply witness ? ? ((exp (nth_prime i) n4)*(defactorize_aux n1 (S i))). reflexivity. -simplify. apply le_n. intros. cut nf_cons n4 n1 = nf_cons m n3. cut n4=m. diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma index 5a2fd4647..921d8853e 100644 --- a/helm/matita/library/nat/gcd.ma +++ b/helm/matita/library/nat/gcd.ma @@ -51,8 +51,9 @@ rewrite > div_mod m n in \vdash (? ? %). rewrite > sym_times. apply eq_plus_to_le ? ? (mod m n). reflexivity. +assumption. rewrite > sym_times. -apply div_mod.assumption. assumption. +apply div_mod.assumption. qed. theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to @@ -83,6 +84,7 @@ change with elim Hcut.rewrite > divides_to_divides_b_true. simplify. split.assumption.apply witness n1 n1 (S O).apply times_n_SO. +assumption.assumption. rewrite > not_divides_to_divides_b_false. change with (divides (gcd_aux n n1 (mod m n1)) m) \land @@ -104,10 +106,8 @@ apply le_S_S_to_le. apply trans_le ? n1. change with mod m n1 < n1. apply lt_mod_m_m.assumption.assumption. -apply decidable_divides n1 m.assumption. -apply lt_to_le_to_lt ? n1.assumption.reflexivity. -assumption. assumption.assumption. +apply decidable_divides n1 m.assumption. qed. theorem divides_gcd_nm: \forall n,m. @@ -192,6 +192,7 @@ cut divides n1 m \lor \not (divides n1 m). elim Hcut. rewrite > divides_to_divides_b_true. simplify.assumption. +assumption.assumption. rewrite > not_divides_to_divides_b_false. change with divides d (gcd_aux n n1 (mod m n1)). apply H. @@ -208,9 +209,8 @@ change with mod m 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 lt_to_le_to_lt ? n1.assumption.reflexivity. -assumption.assumption.assumption. qed. theorem divides_d_gcd: \forall m,n,d. @@ -267,6 +267,7 @@ 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 ex nat (\lambda a. ex nat (\lambda b. @@ -297,6 +298,8 @@ rewrite < eq_minus_minus_minus_plus. rewrite < sym_plus. rewrite < plus_minus. rewrite < minus_n_n.reflexivity. +apply le_n. +assumption. (* second case *) rewrite < H7. apply ex_intro ? ? (a1+a*(div m n1)). @@ -313,25 +316,24 @@ rewrite < eq_minus_minus_minus_plus. rewrite < sym_plus. rewrite < plus_minus. rewrite < minus_n_n.reflexivity. -(* end second case *) +apply le_n. +assumption. apply H n1 (mod m n1). -(* a lot of trivialities left *) cut O \lt mod m n1 \lor O = mod m n1. -elim Hcut2.assumption. +elim Hcut2.assumption. absurd divides n1 m.apply mod_O_to_divides. -assumption.apply sym_eq.assumption.assumption. +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 mod m n1 < n1. -apply lt_mod_m_m.assumption.assumption. +apply lt_mod_m_m. +assumption.assumption.assumption.assumption. apply decidable_divides n1 m.assumption. apply lt_to_le_to_lt ? n1.assumption.assumption. -assumption.assumption.assumption.assumption.assumption. -apply le_n.assumption. -apply le_n. qed. theorem eq_minus_gcd: \forall m,n. @@ -473,6 +475,7 @@ apply not_lt_to_le. 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. elim Hcut.assumption. apply False_ind. @@ -481,7 +484,6 @@ 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. -apply divides_gcd_n.assumption. qed. (* esempio di sfarfallalmento !!! *) @@ -532,8 +534,8 @@ apply witness ? ? (n2*a1-q*a).reflexivity. (* end second case *) 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. -assumption.assumption. qed. diff --git a/helm/matita/library/nat/log.ma b/helm/matita/library/nat/log.ma index 9f32777b3..e24c3031f 100644 --- a/helm/matita/library/nat/log.ma +++ b/helm/matita/library/nat/log.ma @@ -73,8 +73,8 @@ rewrite < H3.rewrite > plus_n_O (m*(div n1 m)). rewrite < H2. rewrite > sym_times. rewrite < div_mod.reflexivity. -intros.simplify.apply plus_n_O. assumption.assumption. +intros.simplify.apply plus_n_O. qed. theorem plog_aux_to_exp: \forall p,n,m,q,r. O < m \to @@ -134,6 +134,7 @@ match (plog_aux m1 (div ((exp m (S n1))*n) m) m) with cut div ((exp m (S n1))*n) m = (exp m n1)*n. rewrite > Hcut1. rewrite > H2 m1. simplify.reflexivity. +apply le_S_S_to_le.assumption. (* div_exp *) change with div (m*(exp m n1)*n) m = (exp m n1)*n. rewrite > assoc_times. @@ -144,7 +145,6 @@ apply divides_to_mod_O. assumption. simplify.rewrite > assoc_times. apply witness ? ? ((exp m n1)*n).reflexivity. -apply le_S_S_to_le.assumption. qed. theorem plog_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to @@ -174,7 +174,7 @@ apply lt_div_n_m_n.assumption.assumption.assumption. intros. change with (\lnot (mod n1 m = O)). rewrite > H4. -(* META NOT FOUND !!! +(* META NOT FOUND !!! rewrite > sym_eq. *) simplify.intro. apply not_eq_O_S m1 ?. diff --git a/helm/matita/library/nat/minimization.ma b/helm/matita/library/nat/minimization.ma index bb3475150..748399fbc 100644 --- a/helm/matita/library/nat/minimization.ma +++ b/helm/matita/library/nat/minimization.ma @@ -87,7 +87,6 @@ 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) ? ? ?. -reflexivity. simplify.intro.assumption. simplify.intro.apply H. elim H1.elim H3.generalize in match H5. @@ -97,6 +96,7 @@ 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. +reflexivity. qed. theorem lt_max_to_false : \forall f:nat \to bool. @@ -164,7 +164,6 @@ 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) ? ? ?. -reflexivity. simplify.intro.assumption. simplify.intro.apply H. elim H1.elim H3.elim H4. @@ -176,6 +175,7 @@ assumption.assumption. absurd f a = false.rewrite < H8.assumption. rewrite > H5. apply not_eq_true_false. +reflexivity. qed. theorem lt_min_aux_to_false : \forall f:nat \to bool. @@ -191,8 +191,9 @@ apply lt_to_not_le.rewrite < H6.assumption. elim H3. 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.assumption. +rewrite < H6.assumption. rewrite < H7.assumption. +assumption. qed. theorem le_min_aux : \forall f:nat \to bool. diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma index 6ff744dcb..3acce20af 100644 --- a/helm/matita/library/nat/minus.ma +++ b/helm/matita/library/nat/minus.ma @@ -215,24 +215,19 @@ 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. -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 < sym_times.simplify.reflexivity. -apply lt_to_le. -apply not_le_to_lt.assumption. -apply le_times_r.apply lt_to_le. -apply not_le_to_lt.assumption. +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 < 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. qed. theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p @@ -241,26 +236,22 @@ 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 \not m+p \le n. -elim Hcut. -apply sym_eq. -apply plus_to_minus.assumption. -rewrite > assoc_plus. -rewrite > sym_plus p. -rewrite < plus_minus_m_m. -rewrite > sym_plus. -rewrite < plus_minus_m_m.reflexivity. -rewrite > eq_minus_n_m_O n (m+p). -rewrite > eq_minus_n_m_O (n-m) p.reflexivity. -apply decidable_le (m+p) n. -apply le_plus_to_minus_r. -rewrite > sym_plus.assumption. -apply trans_le ? (m+p). -rewrite < sym_plus. -apply le_plus_n.assumption. -apply lt_to_le.apply not_le_to_lt.assumption. -apply le_plus_to_minus. -apply lt_to_le.apply not_le_to_lt. -rewrite < sym_plus.assumption. + elim Hcut. + symmetry.apply plus_to_minus.assumption. + 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). + 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. + 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. 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/nth_prime.ma b/helm/matita/library/nat/nth_prime.ma index 5ff937e42..ee21195dc 100644 --- a/helm/matita/library/nat/nth_prime.ma +++ b/helm/matita/library/nat/nth_prime.ma @@ -43,11 +43,11 @@ 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 divides_smallest_factor_n. -simplify.apply le_S_S.apply le_O_n. apply lt_SO_smallest_factor. simplify.apply le_S_S.apply le_SO_fact. assumption. +apply divides_smallest_factor_n. +simplify.apply le_S_S.apply le_O_n. qed. (* mi sembra che il problem sia ex *) diff --git a/helm/matita/library/nat/primes.ma b/helm/matita/library/nat/primes.ma index d7ee89d4e..644cae978 100644 --- a/helm/matita/library/nat/primes.ma +++ b/helm/matita/library/nat/primes.ma @@ -116,10 +116,11 @@ 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. -assumption.apply le_O_n. +assumption. absurd O H2.rewrite < H3.rewrite < times_n_O. apply not_le_Sn_n O. +apply le_O_n. qed. theorem divides_to_lt_O : \forall n,m. O < m \to divides n m \to O < n. diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index a627086c2..a94dcf152 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -103,6 +103,7 @@ TODO matitamake /x/y/z/foo/a.ma - notazione -> Luca e Zack - non chiudere transitivamente i moo ?? + - matitaclean all (non troglie i moo?) DEMONI E ALTRO diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 577e243a6..4bb407975 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -329,12 +329,142 @@ let disambiguate_tactic status tactic = in status_ref, tactic +let reorder_metasenv start refine tactic goals current_goal always_opens_a_goal= + let module PEH = ProofEngineHelpers in + (* phase one calculates: + * new_goals_from_refine: goals added by refine + * head_goal: the first goal opened by ythe tactic + * other_goals: other goals opened by the tactic + *) + let new_goals_from_refine = PEH.compare_metasenvs start refine in + let new_goals_from_tactic = PEH.compare_metasenvs refine tactic in + let head_goal, other_goals, goals = + match goals with + | [] -> None,[],goals + | hd::tl -> + (* assert (List.mem hd new_goals_from_tactic); + * invalidato dalla goal_tac + * *) + Some hd, List.filter ((<>) hd) new_goals_from_tactic, List.filter ((<>) + hd) goals + in + let produced_goals = + match head_goal with + | None -> new_goals_from_refine @ other_goals + | Some x -> x :: new_goals_from_refine @ other_goals + in + (* extract the metas generated by refine and tactic *) + let metas_for_tactic_head = + match head_goal with + | None -> [] + | Some head_goal -> List.filter (fun (n,_,_) -> n = head_goal) tactic in + let metas_for_tactic_goals = + List.map + (fun x -> List.find (fun (metano,_,_) -> metano = x) tactic) + goals + in + let metas_for_refine_goals = + List.filter (fun (n,_,_) -> List.mem n new_goals_from_refine) tactic in + let produced_metas, goals = + let produced_metas = + if always_opens_a_goal then + metas_for_tactic_head @ metas_for_refine_goals @ + metas_for_tactic_goals + else + metas_for_refine_goals @ metas_for_tactic_head @ + metas_for_tactic_goals + in + let goals = List.map (fun (metano, _, _) -> metano) produced_metas in + produced_metas, goals + in + (* residual metas, preserving the original order *) + let before, after = + let rec split e = + function + | [] -> [],[] + | (metano, _, _) :: tl when metano = e -> + [], List.map (fun (x,_,_) -> x) tl + | (metano, _, _) :: tl -> let b, a = split e tl in metano :: b, a + in + let find n metasenv = + try + Some (List.find (fun (metano, _, _) -> metano = n) metasenv) + with Not_found -> None + in + let extract l = + List.fold_right + (fun n acc -> + match find n tactic with + | Some x -> x::acc + | None -> acc + ) l [] in + let before_l, after_l = split current_goal start in + let before_l = + List.filter (fun x -> not (List.mem x produced_goals)) before_l in + let after_l = + List.filter (fun x -> not (List.mem x produced_goals)) after_l in + let before = extract before_l in + let after = extract after_l in + before, after + in + (* DEBUG CODE + let print_m name metasenv = + prerr_endline (">>>>> " ^ name); + prerr_endline (CicMetaSubst.ppmetasenv metasenv []) + in + print_m "BEGIN" start; + prerr_endline ("goal was: " ^ string_of_int current_goal); + prerr_endline ("and metas from refine are:"); + List.iter + (fun t -> prerr_string (" " ^ string_of_int t)) + new_goals_from_refine; + prerr_endline ""; + print_m "before" before; + print_m "metas_for_tactic_head" metas_for_tactic_head; + print_m "metas_for_refine_goals" metas_for_refine_goals; + print_m "metas_for_tactic_goals" metas_for_tactic_goals; + print_m "after" after; + FINE DEBUG CODE *) + before @ produced_metas @ after, goals + +(* maybe we only need special cases for apply and goal *) +let classify_tactic tactic = + match tactic with + (* tactics that can't close the goal (return a goal we want to "select") *) + | GrafiteAst.Rewrite _ + | GrafiteAst.Split _ + | GrafiteAst.Replace _ + | GrafiteAst.Reduce _ + | GrafiteAst.Injection _ + | GrafiteAst.IdTac _ + | GrafiteAst.Generalize _ + | GrafiteAst.Elim _ + | GrafiteAst.Decompose _ -> true, true + (* tactics we don't want to reorder goals. I think only Goal needs this. *) + | GrafiteAst.Goal _ -> false, true + (* tactics like apply *) + | _ -> true, false + let apply_tactic tactic status = + let starting_metasenv = MatitaMisc.get_proof_metasenv status in let status_ref, tactic = disambiguate_tactic status tactic in + let metasenv_after_refinement = MatitaMisc.get_proof_metasenv !status_ref in let proof_status = MatitaMisc.get_proof_status !status_ref in + let needs_reordering, always_opens_a_goal = classify_tactic tactic in let tactic = tactic_of_ast tactic in (* apply tactic will change the status pointed by status_ref ... *) + let current_goal = let _, g = proof_status in g in let (proof, goals) = ProofEngineTypes.apply_tactic tactic proof_status in + let proof, goals = + if needs_reordering then + let uri, metasenv_after_tactic, t, ty = proof in + let reordered_metasenv, goals = + reorder_metasenv starting_metasenv metasenv_after_refinement + metasenv_after_tactic goals current_goal always_opens_a_goal in + (uri, reordered_metasenv, t, ty), goals + else + proof, goals + in let dummy = -1 in { !status_ref with proof_status = MatitaTypes.Incomplete_proof (proof,dummy) }, diff --git a/helm/matita/tests/metasenv_ordering.ma b/helm/matita/tests/metasenv_ordering.ma new file mode 100644 index 000000000..98b3ff0fe --- /dev/null +++ b/helm/matita/tests/metasenv_ordering.ma @@ -0,0 +1,142 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tests/metasenv_ordering". + +include "coq.ma". + +alias num (instance 0) = "natural number". +alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". + +(* REWRITE *) + +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. +qed. + +theorem th2 : + \forall P:Prop. + \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]. + reflexivity. + reflexivity. +qed. + +theorem th3 : + \forall P:Prop. + \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]. + reflexivity. + reflexivity. +qed. + +theorem th4 : + \forall P:Prop. + \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]. + reflexivity. + reflexivity. +qed. + +(* APPLY *) + +theorem th5 : + \forall P:Prop. + \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]. + reflexivity. + reflexivity. +qed. + +theorem th6 : + \forall P:Prop. + \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]. + reflexivity. + reflexivity. +qed. + +theorem th7 : + \forall P:Prop. + \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]. + reflexivity. + reflexivity. +qed. + +theorem th8 : + \forall P:Prop. + \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]. + reflexivity. + reflexivity. +qed. + +(* ELIM *) + +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]. + 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]. + 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]. + elim H; [split; assumption | exact r | exact s]. + qed. + + + + + + + + + + \ No newline at end of file