Email Gateway (Aug 18 2022 at 13:44): Email Gateway (Aug 18 2022 at 13:44):From: Andrei Popescu <uuomul@yahoo.com>
Hello,
In the scripts below, why does lemma "try" succeed whilst lemma "try2" fails? ("try2" fails not only with force, but also with auto and blast, not to mention simp).
Thank you in advance,
Andrei Popescu
consts P::"'a => bool"
definition Q :: "'a => bool"
where "Q = P"
lemma try:
"P x ==> Q x"
proof-
assume "P x"
thus "Q x" by (simp add: Q_def)
qed
lemma try2:
"P x ==> Q x"
proof-
assume "P x"
thus "Q x" using Q_def by force (* THIS FAILS *)
qed
Email Gateway (Aug 18 2022 at 13:45):From: Makarius <makarius@sketis.net>
On Tue, 7 Jul 2009, Andrei Popescu wrote:
consts P::"'a => bool"
definition Q :: "'a => bool"
where "Q = P"lemma try:
"P x ==> Q x"
proof-
assume "P x"
thus "Q x" by (simp add: Q_def)
qed
This works, because the polymorphic definition Q_def is locally added to
the Simplifier context (via "add") and the Simplifier will match it
against any goal states, instantiating an arbitrary ?'a by a fixed 'a as
expected.
lemma try2:
"P x ==> Q x"
proof-
assume "P x"
thus "Q x" using Q_def by force (* THIS FAILS *)
qed
This fails because Q_def is merely inserted straight into the goal, before
regular "force" operation. The unspecified ?'a on the left of the
implication that is part of the goal will never be instantiated by the
proof tool -- all automated proof tools work like that (simp, auto, fast).
Better be more specific about "unfolding Q_def" before finishing by force
etc. Alternatively, you can include it via "simp add: Q_def" into the
method context as for simp above.
Makarius
Email Gateway (Aug 18 2022 at 13:46):From: Tobias Nipkow <nipkow@in.tum.de>
This is a tricky one to do with types. If you write "using <thms>" then
these thms become part of the proof state, namely new assumptions. But
the simplifier does not instantiate ?-Variables in the proof state -
this is not equivalence preserving. This includes type variables. In
your example one of your assumptions is now "(Q::?'a => bool) = (P::?'a
=> bool)" and this ?'a does not get instantiated with 'a to allow
rewriting the conclusion "Q(x::'a)". If you write "(simp add:thms)"
instead, the simplifier is perfectly happy to instantiate the ?-type
variables as required because they are no longer part of the proof state.
The only time I add simplification rules via "using" is if they need to
be simplified themselves. Otherwise "simp add:" is preferable.
Best
Tobias
Andrei Popescu wrote:
Last updated: May 03 2024 at 04:19 UTC