Email Gateway (Aug 18 2022 at 15:21): Email Gateway (Aug 18 2022 at 15:21):From: Marcin Zalewski <marcin.zalewski@gmail.com>
Dear Isabelle experts,
This question might have been answered before, but it is rather
difficult to search for a possible answer. I want to prove the
following lemma:
lemma silly: "(1::nat) + 1 = 2"
I know that I can do "by auto" (or some other automatic tactic), but
the catch is that I want to perform the proof explicitly for
pedagogical reasons. It seems to be more difficult than I have
expected. I am able to see the proof term generated by auto, but the
proof starts with equal_elim, which I have no idea how to apply. I
would be extremely grateful for some direction on how to proceed with
an explicit proof of the above lemma. Is it even practical?
Thank you,
Marcin
Email Gateway (Aug 18 2022 at 15:22):From: Lawrence Paulson <lp15@cam.ac.uk>
I wonder what you mean by pedagogical reasons. If you want to teach the basics of Peano arithmetic, just do it on paper. You don't need Isabelle to carry out a two step proof. If you imagine that this would be a way to teach the use of Isabelle, I would disagree. The way to prove this sort of trivial fact is indeed using auto. There are plenty of other examples that you could use to demonstrate basic Isabelle skills.
Even so, if you would like to step through the basics of this proof, I first suggest that you state the theorem explicitly using the successor function:
lemma silly: "(Suc 0) + (Suc 0) = (Suc (Suc 0))"
Then perform a couple of substitutions using the theorems add_0 and add_Suc.
Larry Paulson
Email Gateway (Aug 18 2022 at 15:22):From: Lawrence Paulson <lp15@cam.ac.uk>
I'm glad you were able to work things out.
It's important to recognise that a proof generated by an automated procedure will seldom look natural or simple. Uniform proof procedures usually produce many unnecessary steps.
Larry Paulson
Email Gateway (Aug 18 2022 at 15:22):From: Marcin Zalewski <marcin.zalewski@gmail.com>
Thanks.
I actually figured out what I wanted soon after I have sent my
message. I used the two substitutions as you suggest (on the restated
lemma since I soon figured out that dealing with literals makes the
proof term too complex), followed by reflection, and interleaved this
with full_prf between each step. That helped me to finally understand
exactly (I think) how Isabelle works under the hood. :) Seeing a full
proof term for this simple theorem, looking at thm.ML in Pure, and
going back to the current and the old manuals (the old one to
understand that prf %% prf corresponds to ==>) helped me to get the
"pedagogical" effect of understanding Isabelle much better. Now I
understand that the foundations are not that complicated, but it
helped to see things in action.
--Marcin
Last updated: Nov 21 2024 at 12:39 UTC