Email Gateway (Aug 22 2022 at 10:15): Email Gateway (Aug 22 2022 at 10:15):From: noam neer <noamneer@gmail.com>
hi.
again I'm nitpicking with simplifier details.
in the following the first proof works while the second doesn't,
and I don't understand why.
theory tmp
imports Complex_Main
begin
lemma "(4::nat) = 1+1+1+1"
by (simp only : algebra_simps)
lemma "(x::real) ^ (4::nat) = x ^ (1+1+1+(1::nat))"
by (simp only : algebra_simps)
end
the second proof fails even if I replace 'only' with 'add'.
I know that the second lemma can be proved with
by (simp add:eval_nat_numeral)
but I'm trying to use the simplifier with as little simp rules as possible.
the reason is that applying it to expressions that contain something like
"2^(2^100)" might get the computer stuck, and the 'only' seems to protect
from it.
if u have a different solution to this problem I'd be happy to hear as well.
thnx
Email Gateway (Aug 22 2022 at 10:16):From: Lars Noschinski <noschinl@in.tum.de>
On 20.06.2015 01:19, noam neer wrote:
lemma "(4::nat) = 1+1+1+1"
by (simp only : algebra_simps)
This is not solved by the simplifier itself but by one of the arithmetic
solvers employed by the simplifier, I guess "linarith" in this instance.
The algebra_simps are not necessary, the goal is also solved by "simp
only:".
lemma "(x::real) ^ (4::nat) = x ^ (1+1+1+(1::nat))"
by (simp only : algebra_simps)
The arithmetic solvers cannot deal with powers, so they cannot solve
this goal.
One solution would be to prove "4 = 1+1+1+1" first and feed this fact
into the second equation. If you have longer chains of such reasoning,
have a look into calculational reasoning (chapter 1.2 of the Isar
reference manual). You could also use the rule "arg_cong" to remove the
"x ^ _" on both sides, but this is a rather low-level style of proof.
-- Lars
Email Gateway (Aug 22 2022 at 10:16):From: noam neer <noamneer@gmail.com>
arithmetic
in a sub expression. everything here happens inside the exponent.
there are cases where they are able to do that, for example in
lemma "(2(x::real)+2y)^(2x+2y) = (2*(x+y))^(2*(x+y))"
by (simp only:algebra_simps)
so I was surprised they didn't succeed here.
Email Gateway (Aug 22 2022 at 10:17):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
"(2(x::real)+2y)^(2x+2y) = (2*(x+y))^(2*(x+y))"
gets rewritten with algebra_simps (which contains, among other things, distributivity) to
"(real x * 2 + real y * 2) ^ (x * 2 + y * 2) =
(real x * 2 + real y * 2) ^ (x * 2 + y * 2)"
which is trivially true. The decision procedure for linear arithmetic has nothing to do with this. You can see that when you write
lemma "(2(x::real)+2y)^(2x+2y) = (2*(x+y))^(2*(x+y))"
unfolding algebra_simps
The linear arithmetic simproc handles equations and inequalities involving linear arithmetic, i.e. it applies to something of the form "2x = x + x", never to something like "2x" alone.
An equation like "(x::real) ^ (4::nat) = x ^ (1+1+1+(1::nat))" is not in the supported fragment because, clearly, the power operation is not linear. This particular problem can be reduced to the (trivially) linear problem "(4::nat) = 1+1+1+1", but the simplifier does not ‘know’ that. For the simproc to apply, the simplifier would first have to set up the goal "(4::nat) = 1+1+1+1", and it does not do that, because that is just not how the simplifier works.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 10:46):From: noam neer <noamneer@gmail.com>
this reply is just for clarification :
I didn't want to use the linear arithmetic part at all.
for example, here it seems the simplifier performs arithmetic rewrites
without it -
lemma "sin(4) = sin(1+1+1+1)"
by simp
so I wondered why when the sin() was replaced by x^() it didn't.
today I found that the following works -
lemma "(x::real)^(4) = x^(1+1+1+1)"
by (simp del: One_nat_def)
if the rule 'One_nat_def' isn't deleted the simplifier rewrites
x^(1+1+1+1) --> xxx*x
after which it gets stuck. so this seems to solve my problem.
(and if one wants to prevent the simplifier from overworking on terms
like "2^(2^100)", one can add "del: power_numeral".)
Last updated: Apr 20 2024 at 12:26 UTC