Stream: General

Topic: turn subgoal into Isar style statement


view this post on Zulip Max W. Haslbeck (Feb 18 2021 at 17:12):

I'm searching for an Isabelle method that turns subgoals into Isar style statements.
For example,

⋀x y. P x ⟹ Q y ⟹ U x y

gets printed as

"U x y" if "P x" "Q y" for x y

in the output panel.

I think, someone posted something like that on the mailing list. Anybody remembering that thread?

view this post on Zulip Manuel Eberl (Feb 18 2021 at 17:30):

https://mailman46.in.tum.de/pipermail/isabelle-dev/2018-September/016496.html
https://gitlab.mpi-klsb.mpg.de/mfleury/isafol-clone/-/blob/24af98ae003c41fbbb427807c7b2769b593bf0c3/lib/Explorer.thy

view this post on Zulip Manuel Eberl (Feb 18 2021 at 17:30):

Tagging @Mathias Fleury

view this post on Zulip Mathias Fleury (Feb 18 2021 at 17:53):

Florian Haftmann has one that is built-in

view this post on Zulip Mathias Fleury (Feb 18 2021 at 17:53):

https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2019-March/016796.html

view this post on Zulip Mathias Fleury (Feb 18 2021 at 17:55):

but the features are not the same. So you probably need to try both :grinning:

view this post on Zulip Mathias Fleury (Feb 18 2021 at 18:05):

I even mention the built-in one in the latest version: https://bitbucket.org/isafol/isafol/src/master/lib/Explorer.thy

view this post on Zulip Mathias Fleury (Feb 18 2021 at 18:30):

Thanks for tagging me @Manuel Eberl

view this post on Zulip Simon Wimmer (Apr 19 2021 at 14:31):

Late to the party, but I have recently thought about about these "explore" commands again.

Does anyone understand the rational behind the current "official" version of producing "show .... if .... for ..." Isar statements?
Doing "fix ... assume ... show ..." as IIRC Mathias' tactic would do seem more reasonable/standard to me.

Also, I think a much simpler command that produces "subgoal for ... premises prems using prems apply -" (or similar) would also sometimes be useful. This has not been implemented, right?

view this post on Zulip Manuel Eberl (Apr 19 2021 at 15:08):

I never use {fix … assume … show} anymore these days, almost aways these eigencontexts with if/for

view this post on Zulip Simon Wimmer (Apr 19 2021 at 16:25):

Yeah, true, so I also do not use these blocks anymore but have ... if ... for (this is what explore gives). But for starting a proof I would always do proof ... fix ... assume ... show ... qed and with Florian's tool (sketch command) I would get proof ... show ... if ... for ..., which I find awkward.

view this post on Zulip Manuel Eberl (Apr 19 2021 at 16:37):

That might make sense. But I never really understood what these tools are for to begin with when you can just do proof goal_cases

view this post on Zulip Lukas Stevens (Apr 19 2021 at 16:39):

One reason that I can imagine is that goal_cases is less readable

view this post on Zulip Lukas Stevens (Apr 19 2021 at 16:39):

(without seeing the output panel)

view this post on Zulip Lukas Stevens (Apr 19 2021 at 16:41):

If it wasn't such a pain to type everything in, then I would certainly prefer the more explicit approach. The explore command could solve that.

view this post on Zulip Simon Wimmer (Apr 19 2021 at 17:07):

It is particularly useful if you have, say, 39 proof obligations generated by a vcg. Then your proofs will break horribly with proof goal_cases when the code changes. But with explore you can get the explicit statements of all these goals quickly. I guess the refinement framework is the main reason why Mathias likes this tool :grinning_face_with_smiling_eyes:

view this post on Zulip Mathias Fleury (Apr 19 2021 at 17:34):

One advantage of the show if is that assumptionsare not shared across shows. This is only relevant if you have multiple goals.

view this post on Zulip Mathias Fleury (Apr 19 2021 at 17:42):

To give an example:

A ==> B ==> C
A ==> ~B ==> C

The corresponding Isar proof is:

  assume A
  assume B
  show C
     sorry
next
  assume A
  assume "~B"
  show C
     sorry

With the if version you could get:

  assume A
  show C if B
     sorry
  show C if  "~B"
     sorry

also making it possible to share consequences of A.

view this post on Zulip Mathias Fleury (Apr 19 2021 at 17:45):

@Simon Wimmer in extreme cases for Refinement goals, I use even context assumes ... instead of show (e.g., search for context on https://people.mpi-inf.mpg.de/~mfleury/IsaFoL/current/Weidenbach_Book/IsaSAT/IsaSAT_Lookup_Conflict.html)

view this post on Zulip Manuel Eberl (Apr 19 2021 at 19:16):

Simon Wimmer said:

It is particularly useful if you have, say, 39 proof obligations generated by a vcg. Then your proofs will break horribly with proof goal_cases when the code changes. But with explore you can get the explicit statements of all these goals quickly. I guess the refinement framework is the main reason why Mathias likes this tool :grinning_face_with_smiling_eyes:

Okay, I see. That doesn't really occur in my life. :grinning:

view this post on Zulip Simon Wimmer (Apr 20 2021 at 15:59):

Simon Wimmer said:

Also, I think a much simpler command that produces "subgoal for ... premises prems using prems apply -" (or similar) would also sometimes be useful. This has not been implemented, right?

Just in case anyone is interested, I have hacked this now: https://github.com/wimmers/explore-subgoal

view this post on Zulip Mathias Fleury (Apr 20 2021 at 16:36):

@Simon Wimmer is there a specific license for your changes or can I included them in my Explorer file?

view this post on Zulip Simon Wimmer (Apr 20 2021 at 16:39):

Please feel free to include them!

view this post on Zulip Lukas Stevens (Apr 20 2021 at 17:00):

Just a question: why didn't you use a config attribute to switch between cartouche and quotes? I think you could shorten your code with that.

view this post on Zulip Mathias Fleury (Apr 20 2021 at 17:17):

Hmmm good question.

view this post on Zulip Mathias Fleury (Apr 20 2021 at 17:17):

Either I did not know about them or I wanted type safety instead of using a string attribute. I don't remember.

view this post on Zulip Mathias Fleury (Apr 20 2021 at 17:18):

But this is definitely a good point. Thanks!


Last updated: Mar 29 2024 at 04:18 UTC