Email Gateway (Aug 22 2022 at 10:12): Email Gateway (Aug 22 2022 at 10:12):From: Lars Noschinski <noschinl@in.tum.de>
On 13.06.2015 15:59, noam neer wrote:
sounds reasonable. however, when I give it to Isabelle I don't get an
error message saying it can't match power_add to the goal,
You wouldn't get an error message about this -- an equation not matching
the goal is the rule, not the exception ;)
I get some
complaint about type unknowns :lemma ?a ^ 6 = ?a ^ 3 * ?a ^ 3
[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
(⋀a m n. a ^ (m + n) = a ^ m * a ^ n) ⟹ a ^ 6 = a ^ 3 * a ^ 3
[1]Cannot add premise as rewrite rule because it contains (type) unknowns:
⋀a m n. a ^ (m + n) = a ^ m * a ^ n
Failed to apply initial proof method⌂:
using this:
?a ^ (?m + ?n) = ?a ^ ?m * ?a ^ ?n
goal (1 subgoal):
1. a ^ 6 = a ^ 3 * a ^ 3what does it mean ?
This means that that the simplifier falls over even earlier than I
thought: Isabelle/HOL cannot quantify over types, so polymorphic rules
(like power_add) are expressed by schematic type variables. If you do
lemma
fixes a::real
shows "a^6 = a^3 * a^3"
using power_add
apply -
you see that the schematic variables in power_add have been replaced by
universally quantified variables. However, if you Ctrl+Hover over the
bound variable "a", you see that it still has a schematic type. To use
it for rewriting, these variables must be instantiated. The simplifier
does not instantiate type variables (except in a few circumstances), so
it rejects this rule.
For your experiments, you can instantiate the type variables in the
lemma by writing
using power_add[where 'a=real]
instead.
-- Lars
Email Gateway (Aug 22 2022 at 10:32):From: noam neer <noamneer@gmail.com>
hi.
I have another simplifier question, possibly partly related to the previous
one.
again I have a proof that works-
theory tmp
imports Complex_Main
begin
lemma
fixes a::real
shows "a^6 = a^3 * a^3"
using [[simp_trace=true]]
using power_add [of a 3 3]
by simp
end
and two that don't. the first failed proof is
theory tmp
imports Complex_Main
begin
lemma
fixes a::real
shows "a^6 = a^3 * a^3"
using [[simp_trace=true]]
using power_add
by simp
end
where it seems strange that the smiplifier couldn't find by itself such a
simple substitution. the second failed proof is
theory tmp
imports Complex_Main
begin
lemma
fixes a::real
shows "a^6 = a^3 * a^3"
using [[simp_trace=true]]
by (simp add:power_add [of a 3 3])
end
is the explanation here the same as before, that in this way
"power_add [of a 3 3]" is not available to the linear arith component?
it seems that the simplifier could have done it by itself if it only knew
that "6=3+3". isn't there a way to inform it of this? it seems very
rudimentary.
thanx
Email Gateway (Aug 22 2022 at 10:32):From: Lars Noschinski <noschinl@in.tum.de>
On 07.06.2015 01:30, noam neer wrote:
[simplifier questions]
The simplifier performs (primarily) rewriting. A term t will be
rewritten with an equation s = s' if there is some substitution of the
variables σ, such that t is syntactically equal to sσ. Then t is
replaced by s'σ. The simplifier tries to do this for all subterms of the
goal.
Recall, power_add is the theorem: ?a ^ (?m + ?n) = ?a ^ ?m * ?a ^ ?n
Now, for your proof attempts:
lemma
fixes a::real
shows "a^6 = a^3 * a^3"
using [[simp_trace=true]]
using power_add [of a 3 3]
by simp
This works as the simplifier can rewrite "3 + 3" to 6 and can then solve
the goal by rewriting with "a^6 = a^3 * a^3".
using power_add
The simplifier cannot rewrite "?m + ?n" to anything. It also does not match the "6" in the goal.
apply (simp add: power_add)
Similar. "a^6" does not match "?a ^ (?m + ?n)".
In my opinion, the nicest proof is:
apply (simp add: power_add[symmetric])
The [symmetric] reverses the equation.
-- Lars
Email Gateway (Aug 22 2022 at 10:32):From: noam neer <noamneer@gmail.com>
thanx for the explanation.
however, note that in the third proof I didn't write
apply (simp add: power_add)
but
by (simp add:power_add [of a 3 3])
so I'm adding "a^(3+3)=a^3 * a^3" to the simp set.
this doesn't match directly, but why wasn't the simplifier able
to simplify it to "a^6 = a^3 * a^3" ?
On Sun, Jun 7, 2015 at 10:12 AM, Lars Noschinski <noschinl@in.tum.de> wrote:
On 07.06.2015 01:30, noam neer wrote:
[simplifier questions]
The simplifier performs (primarily) rewriting. A term t will be
rewritten with an equation s = s' if there is some substitution of the
variables σ, such that t is syntactically equal to sσ. Then t is
replaced by s'σ. The simplifier tries to do this for all subterms of the
goal.Recall, power_add is the theorem: ?a ^ (?m + ?n) = ?a ^ ?m * ?a ^ ?n
Now, for your proof attempts:
lemma
fixes a::real
shows "a^6 = a^3 * a^3"
using [[simp_trace=true]]
using power_add [of a 3 3]
by simpThis works as the simplifier can rewrite "3 + 3" to 6 and can then solve
the goal by rewriting with "a^6 = a^3 * a^3".using power_add
The simplifier cannot rewrite "?m + ?n" to anything. It also does not
match the "6" in the goal.apply (simp add: power_add)
Similar. "a^6" does not match "?a ^ (?m + ?n)".
In my opinion, the nicest proof is:
apply (simp add: power_add[symmetric])
The [symmetric] reverses the equation.
-- Lars
Email Gateway (Aug 22 2022 at 10:32):From: Manuel Eberl <eberlm@in.tum.de>
Equations added to the simp set are not simplified themselves, so the
simplifier will only rewrite "a^(3+3)", but still not "a^6". It might
not even rewrite "a^(3+3)" to "a^3 * a^3", because "3+3" might be
rewritten to "6" first.
Manuel
Email Gateway (Aug 22 2022 at 10:33):From: Lars Noschinski <noschinl@in.tum.de>
That issue is shortly touched upon in Gerwin's style guide[1] in the
section " Decide on good normal forms and use them consistently."
[1] http://proofcraft.org/blog/isabelle-style-part2.html
Email Gateway (Aug 22 2022 at 10:36):From: noam neer <noamneer@gmail.com>
hi again.your explanation for the first failed proof :
theory tmp
imports Complex_Main
begin
lemma
fixes a::real
shows "a^6 = a^3 * a^3"
using [[simp_trace=true]]
using power_add
by simp
end
sounds reasonable. however, when I give it to Isabelle I don't get an
error message saying it can't match power_add to the goal, I get some
complaint about type unknowns :
lemma ?a ^ 6 = ?a ^ 3 * ?a ^ 3
[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
(⋀a m n. a ^ (m + n) = a ^ m * a ^ n) ⟹ a ^ 6 = a ^ 3 * a ^ 3
[1]Cannot add premise as rewrite rule because it contains (type) unknowns:
⋀a m n. a ^ (m + n) = a ^ m * a ^ n
Failed to apply initial proof method⌂:
using this:
?a ^ (?m + ?n) = ?a ^ ?m * ?a ^ ?n
goal (1 subgoal):
1. a ^ 6 = a ^ 3 * a ^ 3
what does it mean ?
Last updated: Apr 23 2024 at 20:15 UTC