Email Gateway (Aug 22 2022 at 09:56): Email Gateway (Aug 22 2022 at 09:56):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
I definitely agree that it is still unclear how IDE support for proof
construction should look like, and this for me seems the main reason why
numerous people (including me) prefer a output-buffer-centric working
style here.
What I would appreciate is better support to materialize pending proof
obligations in the source proper – what, by the way, is one of my main
applications of the output buffer: copying open goals to the source and
turning them into proper Isar.
Some time (years?) ago I did a small sketch of a command which takes a
method, applies and it writes back the resulting goal state as Isar
skeleton. In the presence of the rich infrastructure (including
sledgehammer's facilities to print pretty Isar proofs) it should not be
that difficult to get something running and useful here, with rich
potential for research. I would appreciate if somebody would seriously
take up this enterprise.
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 09:56):From: Peter Lammich <lammich@in.tum.de>
What I would appreciate is better support to materialize pending proof
obligations in the source proper – what, by the way, is one of my main
applications of the output buffer: copying open goals to the source and
turning them into proper Isar.
(At least for me) another main application of the output buffer is
backward-style proof exploration. I throw apply-style tactics onto my
goal until it is solved, including old-fashioned things like
rule_tac x="..." in exI
(For me) this is a very efficient method to find proofs. Once the proof
is found, I usually clean it up (a bit). Thus, even if apply-style and
xxx_tac methods are considered bad style for camera-ready proof text,
they are very important for proof exploration, and should not be
abandoned without viable alternatives.
Some time (years?) ago I did a small sketch of a command which takes a
method, applies and it writes back the resulting goal state as Isar
skeleton.
Sounds like a good idea that may save lot's of tedious copy-and-paste if
you already have the detailed proof in mind, and want to document the
steps at a very fine-grained level in Isar.
I am unsure whether it would work as a replacement for proof-exploration
as described above, because it would produce lots of text in the main
buffer, which may obfuscate the whole proof, in particular for big
subgoals. (I regularly have ~20 subgoals, each of which is ~20 lines
long)
Email Gateway (Aug 22 2022 at 09:57):From: Larry Paulson <lp15@cam.ac.uk>
I also work in the way you describe. I imagine that this is the normal approach, as opposed to trying to generate structured proofs directly out of nothing.
It would be great to have a command that could take the current subgoal and generate the corresponding text of a nested block. At the same time, I hope that users would take the trouble to clean this up, deleting unused assumptions and possibly generalising the result proved.
Larry Paulson
Email Gateway (Aug 22 2022 at 10:26):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Some time (years?) ago I did a small sketch of a command which takes a
method, applies and it writes back the resulting goal state as Isar
skeleton.Sounds like a good idea that may save lot's of tedious copy-and-paste if
you already have the detailed proof in mind, and want to document the
steps at a very fine-grained level in Isar.
I really had proof exploration in mind.
I am unsure whether it would work as a replacement for proof-exploration
as described above, because it would produce lots of text in the main
buffer, which may obfuscate the whole proof, in particular for big
subgoals. (I regularly have ~20 subgoals, each of which is ~20 lines
long)
Deleting big experimental sections should not be a big problem.
When doing proof development nowadays, I often make the experience that,
when I am actually finishing the proof, I have to delete draft lines
more than an editor page (!) which has accumulated over time.
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 10:28):From: Peter Lammich <lammich@in.tum.de>
The same for me.
My fear was, if these draft lines now also contain tons of subgoals,
they may be dozens of editor pages, and obfuscate the essential proof
steps that have been worked out. But, maybe I've not correctly
understood the idea.
Last updated: Apr 26 2024 at 08:19 UTC