From: Claudio Sacerdoti Coen Date: Sun, 18 May 2008 19:04:18 +0000 (+0000) Subject: Dummy dependent types are no longer cleaned in inductive type arities. X-Git-Tag: make_still_working~5160 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f11316bd6cda8e0eb519bbced0a09de23dacc252;p=helm.git Dummy dependent types are no longer cleaned in inductive type arities. --- diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma index f5847033a..8e70ab958 100644 --- a/helm/software/matita/library/nat/neper.ma +++ b/helm/software/matita/library/nat/neper.ma @@ -727,10 +727,10 @@ elim k |(*già usata 2 volte: fattorizzare*) elim n [simplify;apply le_n - |apply (bool_elim ? (p n1));intro + |apply (bool_elim ? (p n2));intro [rewrite > true_to_pi_p_Sn [rewrite > (times_n_O O);apply lt_times - [elim (H n1);assumption + [elim (H n2);assumption |assumption] |assumption] |rewrite > false_to_pi_p_Sn;assumption]]] @@ -777,7 +777,7 @@ intros;apply eq_sigma_p;intros; [rewrite > exp_plus_times; unfold bc; elim (bc2 n x) - [rewrite > H3;cut (x!*n2 = pi_p x (\lambda i.true) (\lambda i.(n - i))) + [rewrite > H3;cut (x!*n1 = pi_p x (\lambda i.true) (\lambda i.(n - i))) [rewrite > sym_times in ⊢ (? ? (? (? (? (? % ?) ?) ?) ?) ?); rewrite > assoc_times; rewrite < sym_times in ⊢ (? ? (? (? (? % ?) ?) ?) ?); @@ -878,25 +878,25 @@ intros;apply eq_sigma_p;intros; [apply divides_SO_n |elim x [simplify;apply divides_SO_n - |change in \vdash (? % ?) with (n*(exp n n1)); + |change in \vdash (? % ?) with (n*(exp n n2)); rewrite > true_to_pi_p_Sn [apply divides_times;assumption |reflexivity]]] |apply lt_O_fact - |apply (witness ? ? n2);symmetry;assumption]] + |apply (witness ? ? n1);symmetry;assumption]] |rewrite > divides_times_to_eq; [apply eq_f2 [reflexivity |elim x [simplify;reflexivity - |change in \vdash (? ? % ?) with (a*(exp a n1)); + |change in \vdash (? ? % ?) with (a*(exp a n2)); rewrite > true_to_pi_p_Sn [apply eq_f2 [reflexivity |assumption] |reflexivity]]] |apply lt_O_fact - |apply (witness ? ? n2);symmetry;assumption]] + |apply (witness ? ? n1);symmetry;assumption]] |apply lt_O_fact |apply lt_O_fact] |apply (inj_times_r (pred ((n-x)!))); @@ -964,15 +964,15 @@ intros;transitivity ((exp a n)*(exp (S n) n)/(exp n n)/(exp a n)) [elim H2;rewrite > H3;rewrite < times_exp;rewrite > sym_times in ⊢ (? ? (? (? ? ? (λ_:?.? ? %)) ?) ?); rewrite > sym_times in ⊢ (? ? ? (? ? ? (λ_:?.? (? (? ? %) ?) ?))); transitivity (sigma_p (S n) (λx:nat.true) -(λk:nat.(exp n n)*(bc n k*(n)\sup(n-k)*(n2)\sup(n)))/exp n n) +(λk:nat.(exp n n)*(bc n k*(n)\sup(n-k)*(n1)\sup(n)))/exp n n) [apply eq_f2 [apply eq_sigma_p;intros; [reflexivity |rewrite < assoc_times;rewrite > sym_times;reflexivity] |reflexivity] - |rewrite < (distributive_times_plus_sigma_p ? ? ? (\lambda k.bc n k*(exp n (n-k))*(exp n2 n))); + |rewrite < (distributive_times_plus_sigma_p ? ? ? (\lambda k.bc n k*(exp n (n-k))*(exp n1 n))); transitivity (sigma_p (S n) (λx:nat.true) - (λk:nat.bc n k*(n2)\sup(n)*(n)\sup(n-k))) + (λk:nat.bc n k*(n1)\sup(n)*(n)\sup(n-k))) [rewrite > (S_pred (exp n n)) [rewrite > div_times;apply eq_sigma_p;intros [reflexivity @@ -1042,7 +1042,7 @@ intros;rewrite > (neper_sigma_p3 (n*S n) n) rewrite > sym_times;apply divides_times [apply divides_SO_n |elim (bc2 n i); - [apply (witness ? ? n2); + [apply (witness ? ? n1); cut (pi_p i (\lambda y.true) (\lambda i.n-i) = (n!/(n-i)!)) [rewrite > Hcut1;rewrite > H3;rewrite > sym_times in ⊢ (? ? (? (? % ?) ?) ?); rewrite > (S_pred ((n-i)!)) @@ -1086,7 +1086,7 @@ intros;rewrite > (neper_sigma_p3 (n*S n) n) apply divides_times [apply divides_SO_n |elim (bc2 (S n) i); - [apply (witness ? ? n2); + [apply (witness ? ? n1); cut (pi_p i (\lambda y.true) (\lambda i.S n-i) = ((S n)!/(S n-i)!)) [rewrite > Hcut1;rewrite > H3;rewrite > sym_times in ⊢ (? ? (? (? % ?) ?) ?); rewrite > (S_pred ((S n-i)!))