Simon Wimmer (Nov 25 2021 at 12:36): Simon Wimmer (Nov 25 2021 at 12:36):As you might have heard, Makarius is phasing out guess for Isabelle 2021-1. It now resides in Pure-ex.Guess.
While I agree that guess should not show up in Isar proofs, I think it has some use for "exploration" in an Isar proof.
In that spirit, I made a modified version that outputs a completion hint at 'qed' such that one can more easily turn the whole thing into a proper obtain statement.
Example:
One types
from foo[of z] guess x y .
Now, at the output of . one can click the completion hint and gets:
from foo[of z] guess x y where
"z = x + y"
"P x y"
This is not exactly what I would imagine it to be like. Ideally one would get
from foo[of z] obtain x y where
"z = x + y"
"P x y"
.
but I do not know how to achieve this.
Nevertheless, I find this useful for converting old proofs and "exploration" as mentioned.
Is anyone else still using guess?
Manuel Eberl (Nov 25 2021 at 12:44):I used it a lot in the past. I've forced myself to stop doing it. But I think it is extremely useful when you have an elimination rule that gives you a lot of long facts all at once. Something like your version of guess seems really useful. I think you ought to replace the one in HOL-Library with yours. And perhaps ask Makarius if something can be done to replace the guess with obtain by clicking on active markup.
Lukas Stevens (Nov 25 2021 at 12:58):It would also be possible to implement this as a lint (use obtain instead of guess) in the linter that Yecine (and we) are developing.
Lukas Stevens (Nov 25 2021 at 13:13):However, the direct route within the guess command would be better. In principle it should not be hard to get the right active markup using the functions in The functionality in Isabelle/ML for replacing stuff in the buffer with active markup does not exist yet. But maybe we can put it in permanently when we pull the linter into the distribution.~/src/Pure/PIDE/active.ML.
Lukas Stevens (Nov 25 2021 at 13:17):You can do this with Isabelle/Scale. See here: https://github.com/isabelle-prover/isabelle-linter/blob/master/jedit_linter/src/jedit_extension.scala
Lukas Stevens (Nov 25 2021 at 13:17):The relevant function is in the Handler.
Manuel Eberl (Nov 25 2021 at 13:40):Is something like this possible in e.g. VSCode as well?
Lukas Stevens (Nov 25 2021 at 13:59):In principle that is of course possible; however, the current state is that the markup (basically an XML tree) isn't even transmitted to VSCode. So the information gets lost and we can't implement a handler for active markup in VSCode.
Simon Wimmer (Nov 25 2021 at 14:16):Ah ok, thanks for the pointers, Lukas.
I will tinker with it a bit more and contact Makarius eventually (after the current release).
Simon Wimmer (Nov 25 2021 at 14:26):(and keep please keep me in the loop when things from the linter are moved to the distribution)
Lukas Stevens (Nov 25 2021 at 14:33):Simon Wimmer said:
(and keep please keep me in the loop when things from the linter are moved to the distribution)
We will certainly announce it on the mailing list :smile:
Fabian Huch (Nov 25 2021 at 18:35):Simon Wimmer said:
Ah ok, thanks for the pointers, Lukas.
I will tinker with it a bit more and contact Makarius eventually (after the current release).
I did already send Makarius a patch to enable sendback markup for ranges, but he did not want to put it in as nothing uses that yet. So if you have a use-case with guess then you could probably just ask him to put my changes in.
Simon Wimmer (Nov 25 2021 at 22:21):Ah nice! I'll ask him about it.
Last updated: Dec 21 2024 at 16:20 UTC