Stream: Beginner Questions

Topic: Make use of bracketed premises in Isar

Chengsong Tan (Nov 20 2023 at 22:37):

When proving a lemma like [| P ; Q |] ==> S in Isar, it seems
the premises got forgotten in the middle.
A mwe:

lemma mix: shows "⟦ x + y = 2; x ≥1; y ≥1 ⟧ ⟹ x = 1"
proof -
  have "x ≤ 1"
    sorry

It seems that you just can't prove "x<=1".

Thanks a lot,
Chengsong

Wolfgang Jeltsch (Nov 20 2023 at 23:18):

You say that you want to prove x ≤ 1 from no assumptions. This can’t work. In Isar, you have to be explicit where you use which assumptions, which is on purpose (in particular, it results in more readable proofs). Have you looked at some introduction to Isar, like the one in prog-prove?

Better use Isar also for phrasing implications. Then you can access the premises as local facts. Like in this code:

lemma mix:
  assumes "x + y = 2" and "x ≥ 1" and "y ≥ 1"
  shows "x = 1"
proof -
  from ‹x + y = 2› and ‹y ≥ 1› have "x ≤ 1"
    sorry

Chengsong Tan (Nov 22 2023 at 12:23):

Wolfgang Jeltsch said:

You say that you want to prove x ≤ 1 from no assumptions. This can’t work. In Isar, you have to be explicit where you use which assumptions, which is on purpose (in particular, it results in more readable proofs). Have you looked at some introduction to Isar, like the one in prog-prove?

Better use Isar also for phrasing implications. Then you can access the premises as local facts. Like in this code:

lemma mix:
  assumes "x + y = 2" and "x ≥ 1" and "y ≥ 1"
  shows "x = 1"
proof -
  from ‹x + y = 2› and ‹y ≥ 1› have "x ≤ 1"
    sorry

Thank you, Wolfgang!
It's good to know that bracketed premises are not compatible with Isar proofs. It would be really nice if we can mix Isar styles and apply styles together (right now Isar seems very invasive in the sense that once you want to use a snippet of Isar (which sledgehammer sometimes generates) in your apply scripts, everything has to be totally changed to accommodate Isar-style reasoning).

Wolfgang Jeltsch (Nov 22 2023 at 12:50):

Why not use Isar all the time? It allows you to write human-friendly proofs, as opposed to apply style. I use apply style only for exploration: when I’m looking for a single proof method invocation or a combination of a few of them that I can put after a by. For the final code, I exclusively use Isar.

Mathias Fleury (Nov 22 2023 at 12:56):

I always the use the assumes version. Then you can have a using assms apply - and use normal apply-scripts…

Yong Kiam (Nov 22 2023 at 13:59):

I agree with the others about using Isar, but I'm not sure what you mean by "everything has to be totally changed to Isar-style"

in principle, you could still have a mostly apply-style script like this:

proof -
have ... by (huge apply script)
have ... by (huge apply script)
show foo by
  (huge apply script)
qed

Fabian Huch (Nov 22 2023 at 14:01):

You can write a proof like that, but it will be pretty much incomprehensible.

Mathias Fleury (Nov 22 2023 at 15:02):

I still think that this would be better than huge apply-style proofs… At least there are intermediate steps

Chengsong Tan (Nov 23 2023 at 09:32):

Yong Kiam said:

I agree with the others about using Isar, but I'm not sure what you mean by "everything has to be totally changed to Isar-style"

in principle, you could still have a mostly apply-style script like this:

proof -
have ... by (huge apply script)
have ... by (huge apply script)
show foo by
  (huge apply script)
qed

Hi Yong Kiam,
To clarify what I meant, you cannot have something like this:

lemma "[| .... |] ==> P"
apply .... (apply style scripts)
(isar bit starts with n+1 subgoals)
proof -
....
proof ends
(isar bit ends, leaving you n subgoals)
apply.... (apply scripts continue)

Here the Isar bit just acts as if it is a normal 1-liner proof solving a particular goal, which blends in with other apply scripts.
But as far as my experience on Isar, once you start proof ..., you are not able to leave the Isar mode and every other goal has to be finished until you qed with the entire lemma. Yes you can still use apply scripts for certain bits in the Isar proof (when it is in "proof" mode?) but you can no longer go back to the full-on apply style now (for example bracketed premises are not usable now, of course you can still change the phrasing of the lemma but that's what I meant by "invasive").

Last updated: Apr 28 2024 at 12:28 UTC