Email Gateway (Aug 19 2022 at 14:09): Email Gateway (Aug 19 2022 at 14:09):From: noam neer <noamneer@gmail.com>
this question is about the behaviour of 'auto' in problems that
require rewriting.
in both examples below the lemma states that "expr1^2 = expr2^2", which is true
since "expr1=expr2". in the first case the proof is short -
lemma tt1 :
fixes a b :: real
shows "(cos(a+b))^2 =
(cos(a)cos(b) - sin(a)sin(b))^2"
proof -
from cos_add
show ?thesis
by auto
qed
in the second case the equality of the expressions is slightly more
complicated so it is
proved in a sub lemma. but using the result in an analogous way FAILS :
lemma tt2 :
fixes a b :: real
shows "(1 + 2*cos(a+b))^2 =
(1 + cos(a+b) + cos(a)cos(b) - sin(a)sin(b))^2"
proof -
{
fix c d::real
from cos_add
have "1 + 2*cos(c+d) =
1 + cos(c+d) + cos(c)cos(d) - sin(c)sin(d)"
by auto
}
from this
show ?thesis
by auto
(* DOESN'T TERMINATE*)
qed
I was able to fix the code s.t. the proof terminates successfully,
by adding an appropriate lemma to the 'from' part :
from this
Power.idom_class.power2_eq_iff
[of "1 + 2*cos(a+b)"
"1 + cos(a+b) + cos(a)cos(b) - sin(a)sin(b)"]
show ?thesis
by auto
the added lemma states the obvious
lemma power2_eq_iff: "x\<^sup>2 = y\<^sup>2 \<longleftrightarrow>
x = y \<or> x = - y"
but since the first example must have used this lemma (or something
very similar,)
I'd like to understand why I had to add it explicitly and also to
instantiate it myself
(otherwise it refused to work,)
while in the first example this wasn't necessary.
thanx, Noam
Email Gateway (Aug 19 2022 at 14:10):From: Lawrence Paulson <lp15@cam.ac.uk>
auto, blast, force all do logical reasoning. If you need just pure rewriting, try simp, or even just subst.
Larry Paulson
Last updated: Apr 26 2024 at 08:19 UTC