turn subgoal into Isar style statement · General

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?

Manuel Eberl (Apr 19 2021 at 15:08):

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

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.

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

Lukas Stevens (Apr 19 2021 at 16:39):

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

Lukas Stevens (Apr 19 2021 at 16:39):

(without seeing the output panel)

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.

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:

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.

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.

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)

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:

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

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?

Simon Wimmer (Apr 20 2021 at 16:39):

Please feel free to include them!

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.

Mathias Fleury (Apr 20 2021 at 17:17):

Hmmm good question.

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.

Mathias Fleury (Apr 20 2021 at 17:18):

But this is definitely a good point. Thanks!

Last updated: Dec 21 2024 at 12:33 UTC