Email Gateway (Aug 19 2022 at 09:19): Email Gateway (Aug 19 2022 at 09:19):From: Julian Brunner <julianbrunner@gmail.com>
Hello,
While using Isabelle, I keep running into the problem of not being able to
prove existentially quantified statements using a witness with the show
statement telling me that the "Local statement will fail to refine any
pending goal".
For instance:
theorem "EX x. x = (0 :: nat)"
proof
obtain x where x_def: "x = (0 :: nat)" by simp
show "x = 0" using x_def by simp
qed
This example results in "Local statement will fail to refine any pending
goal" in line 4 of the proof. Furthermore, replacing line 3 with
def x == "0 :: nat"
makes everything work just fine. This is a minimal example built from a
bigger proof where the witness used for proving the existential statement
was an expression containing variables that originated in an obtain
statement. From what I've observed so far, it appears that whenever
variables from an obtain statement are part of the witness, the show
statement fails. I've used [[show_types]] to confirm that the types aren't
part of the issue, both x and 0 are of type nat. Also, the output doesn't
give me the usual "Failed attempt to solve goal by exported rule" line
stating why the show statement failed, as is the case with assume
statements that don't match any assumption in the goal.
Of course I can work around this by invoking proof with the '-' method and
using automation to prove the existentially quantified statement using the
witness, but it'd be nicer if it'd work like this, I feel like this is just
a minor technical issue, but I couldn't figure out what's going on.
I think I've also run into a similar problem that didn't involve obtain
statements but I can't find the theory where that happened right now, maybe
I'll post again if I run into that issue once more. For now, I'd be happy
with figuring this one out.
Cheers,
Julian
Email Gateway (Aug 19 2022 at 09:19):From: Lars Noschinski <noschinl@in.tum.de>
On 12.11.2012 20:21, Julian Brunner wrote:
Hello,
While using Isabelle, I keep running into the problem of not being able to
prove existentially quantified statements using a witness with the show
statement telling me that the "Local statement will fail to refine any
pending goal".
This error message is not very helpful (and I seem to remember there
once was a more useful one, mentioning obtained variables?). There is a
more useful error message when the last theorem of a {-}-block contains
an obtained variable
{ obtain x where "x = Suc 0" by auto
then have "x > 0" by auto }
results in:
Result contains obtained parameters: x
This is due to the same reason. When you use "fix" or "def" to define a
variable, they either get just generalized (i.e. turned into schematics)
(fix) or replaced by their right hand side (definitions)
when a block is closed / a show is performed.
This cannot be done for obtained variables.
Of course I can work around this by invoking proof with the '-' method and
using automation to prove the existentially quantified statement using the
witness, but it'd be nicer if it'd work like this, I feel like this is just
a minor technical issue, but I couldn't figure out what's going on.
A good scheme for proving such things is
lemma "EX x. P x"
proof -
obtain x where <...>
<...>
have "P x" <...>
show ?thesis ..
qed
where .. is a shorthand for "by rule".
-- Lars
Email Gateway (Aug 19 2022 at 09:20):From: Tobias Nipkow <nipkow@in.tum.de>
The reason for this failure is consistency: when proving P(?x), you delay the
point at which you give the actual witness t for ?x. But that is just an
operational rearrangement of the proof. Logically it must be possible to
construct that t right away. Hence t must not depend on anything that only came
into existence while proving P(?x). Otherwise you could prove EX x. ALL y. x=y:
apply(rule exI)
apply(rule allI)
apply(rule refl)
fails because you would need to instantiate ?x with the local y, which Isabelle
prevents. (Contrast this with a proof of ALL x. EX y. x=y)
Your failed proof attempt was morally correct, but you need to convince the
system that the witness could have been constructed up front, usually by
rearranging your proof text, eg as Lars suggested.
Best
Tobias
Email Gateway (Aug 19 2022 at 09:21):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Julian,
a further comment:
theorem "EX x. x = (0 :: nat)"
proof
the statement to prove here contains a schematic variable ?x or such.
This is something better to be avoided except for good reason.
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 09:26):From: Makarius <makarius@sketis.net>
On Tue, 13 Nov 2012, Lars Noschinski wrote:
On 12.11.2012 20:21, Julian Brunner wrote:
While using Isabelle, I keep running into the problem of not being able
to prove existentially quantified statements using a witness with the
show statement telling me that the "Local statement will fail to refine
any pending goal".This error message is not very helpful (and I seem to remember there
once was a more useful one, mentioning obtained variables?).
It seems that I've destroyed that error messahe by accident in Jan-2009,
but it is likely to work again in the coming release.
For instance:
theorem "EX x. x = (0 :: nat)"
proof
obtain x where x_def: "x = (0 :: nat)" by simp
show "x = 0" using x_def by simp
qed
BTW, a more compact way to write that wrong proof is this:
theorem "EX x. x = (0 :: nat)"
proof
obtain x where "x = (0 :: nat)" by simp
then show ?this .
qed
But that does not work for logical reasons, as has been pointed out
before. You cannot apply an obtained result with parameters to the
enclosing goal. This is also the deeper reason why there is 'have' for
local results, and 'show' for local results that get exported into the
enclosing goal context, but only 'obtain' and not 'obtain_show'.
(And you don't need to obtain local definitions in the first place, has
has been said already.)
Makarius
Email Gateway (Aug 19 2022 at 09:26):From: Makarius <makarius@sketis.net>
Just for fun some further vacuous 'obtain' proofs:
notepad
begin
obtain x where "x = (0 :: nat)" by (rule that) (rule refl)
next
obtain x where "x == (0 :: nat)" by (rule that) (rule reflexive)
next
obtain x where "x == (0 :: nat)" ..
end
The last form works, because "that" is declared as Pure.intro, and Pure
"reflexive" implicit (like assumption).
The better form is this:
def x == "0 :: nat"
Here the system does the reflexicity step for you, and it bypasses the
full "may-assume-that-holds" mechanism of 'obtain', that involves the
restriction on variable occurrences (as seen in the exE rule).
Makarius
Last updated: Nov 21 2024 at 12:39 UTC