Stream: Beginner Questions

Topic: What about a 'suffices to show' Isar keyword?

Moritz R (Dec 15 2024 at 17:35):

I find myself repeatedly longing for a nice way to write

Instead of the current goal, it is enough to instead show bla (since [easy justification])

Is there a suffices keyword or similar (that would change the goal)?

I see that there exists the 'presume' keyword, but that does the wrong thing.

Moritz R (Dec 15 2024 at 17:37):

Sure, one can just write
have bla by [easy justification] right at the end of the proof, but i find that often leaves a ready confused to what will be happening for the earlier part of the proof - it doesnt communicate what i want to communicate.

Mathias Fleury (Dec 15 2024 at 18:16):

I am not aware of any keyword to do that. How about starting the proof with

  fix A B C :: bool
  have H: thesis  if A and B and C
    sorry (*easy justification*)

(*then either application of the theorem to have the shows*)
  have thesis
  proof (rule H)
    show A
      sorry
    show B
      sorry
    show C
      sorry
  qed

(*or you go for*)
  have A
    sorry
  moreover have B
    sorry
  moreover have C
    sorry
  ultimately show thesis
    using H by blast

Moritz R (Dec 15 2024 at 22:28):

For this one still has to write A multiple times :/ but already better than quietly appending it at the end and pretending we only did forward reasoning the whole time :D

Mathias Fleury (Dec 16 2024 at 05:54):

Why not use is? (and give a better name than goal1 obviously, but it is easier on real examples to come up with names)

  fix A B C :: bool
  have H: thesis  if A (is ?goal1) and B (is ?goal2) and C (is ?goal3)
    sorry
  have thesis
  proof (rule H)
    show ?goal1
      sorry
    show ?goal2
      sorry
    show ?goal3
      sorry
  qed

Manuel Eberl (Dec 19 2024 at 19:15):

Moritz R said:

I find myself repeatedly longing for a nice way to write

Instead of the current goal, it is enough to instead show bla (since [easy justification])

Is there a suffices keyword or similar (that would change the goal)?

I see that there exists the 'presume' keyword, but that does the wrong thing.

One of the problems with that is that Isar does not have a concept of ‘the current goal’. At any given point there may be more than one goal and you can solve them in whatever order you want. So if you wanted to have a keyword like that, you would have to specify both the new goal and the old goal that you want to replace with it.

I don't know enough about the internals of Isar to say if something like that would be possible, but I would imagine so. Not sure how useful it would be in that form though.

Manuel Eberl (Dec 19 2024 at 19:17):

In some cases you can also do something like that with an induction rule; consider e.g. the rule linorder_wlog, which allows you to prove P x y where x and y are of type 'a :: linorder by additionally assuming x ≤ y and showing that P is symmetric.

Last updated: Dec 21 2024 at 16:20 UTC