Email Gateway (Aug 19 2022 at 08:06): Email Gateway (Aug 19 2022 at 08:06):From: Gergely Buday <gbuday@gmail.com>
Hi,
I have written
theory Let
imports Main
begin
lemma "(2 :: nat) + 2 = 4"
proof
Now, 'proof' results in
"empty result sequence -- proof command failed"
Otherwise, i.e. without Isar,
apply (auto)
finishes the proof, so the lemma itself is well-written. What else could fail?
Email Gateway (Aug 19 2022 at 08:06):From: Lawrence Paulson <lp15@cam.ac.uk>
If you write “proof", then some default proof method (depending on the form of your goal) will be attempted. I'm not sure what it is in this case, but it obviously failing. Write
proof -
to open a proof without attempting a proof method.
Similarly, if you try to develop a structured proof by experimenting with lines of the form “apply <method>", you may find that everything fails for no apparent reason. It is the same reason as before, and can be fixed by ensuring that your first line is “apply -". This is particularly important if you have chained facts.
Larry Paulson
Email Gateway (Aug 19 2022 at 08:06):From: John Wickerson <jpw48@cam.ac.uk>
So maybe the following will work...
lemma "(2 :: nat) + 2 = 4"
proof(auto)
Email Gateway (Aug 19 2022 at 08:06):From: Lars Noschinski <noschinl@in.tum.de>
It would; but as a rule of thumb, auto should never be the argument of
proof command: The result of auto is very much unpredictable and
unstable across versions, so chances that your proof will break some not
so far time in the future are pretty high.
-- Lars
Last updated: Apr 25 2024 at 20:15 UTC