Stream: Beginner Questions

Topic: Isar proof by 3 disjunctive cases

Bob Rubbens (May 02 2023 at 07:49):

Hey everyone, I have an isar question. Is a structure as follows possible?

have "P \/ Q \/ R" sorry
then show ?thesis
proof
  assume "P" then show ?case sorry
next
  assume "Q" then show ?case sorry
next
  assume "R" then show ?case sorry
qed

When I tried it it only allowed two disjunctive cases, so after proving P I had to split Q \/ R apart again using assume Q \/ R then show ?case proof .... Works fine but I'd like to avoid the extra nesting.

Bob Rubbens (May 02 2023 at 08:12):

I did not google hard enough, the answer is yes, this is possible. Discussed here: https://stackoverflow.com/questions/15901570/proof-rule-disje-for-nested-disjunction

Yosuke Ito (May 02 2023 at 09:17):

I agree to using consider command.

Bob Rubbens (May 02 2023 at 11:41):

Besides syntax preference, what factors are there to choose "consider" over the other options in the SO post?

Yosuke Ito (May 02 2023 at 12:30):

Maybe it's just my preference, but consider is especially used for case analysis, so the proof by exhaustion would be easy to read.

Wolfgang Jeltsch (May 03 2023 at 17:19):

Well, with just disjunctions, it is trivial to relate the three parts of the proof to the subformulas; so you might want to not use consider here.

I haven’t checked the StackOverflow thread, but I just want to remark that the problem with the original example is that the automatically invoked standard method, which should perform rule disjE here, is only applied once. Something like proof standard+ or proof (elim disjE) might do the trick.

Yosuke Ito (May 03 2023 at 23:30):

Thanks, Wolfgang. Let me confirm your opinion.
When you use consider, you are to prove that the cases exhaust all the patterns. In this case however, the hypothesis is already written in disjunction, so consider requires the extra task to prove the completness. That makes the proof less efficient.
Is that what you are saying?

Mathias Fleury (May 04 2023 at 05:03):

have "P ∨ Q ∨ R" sorry
then have G
proof (elim disjE)
  assume "P" then show G sorry
next
  assume "Q" then show G sorry
next
  assume "R" then show G sorry
qed

Wolfgang Jeltsch (May 05 2023 at 14:10):

Yosuke Ito said:

Thanks, Wolfgang. Let me confirm your opinion.
When you use consider, you are to prove that the cases exhaust all the patterns. In this case however, the hypothesis is already written in disjunction, so consider requires the extra task to prove the completness. That makes the proof less efficient.
Is that what you are saying?

Yes, that’s basically what I wanted to say, although I might not use the term “efficiency”. I always strive to write Isar proofs that are close to ordinary pen-and-paper proofs. It’s all about being intelligible for the reader. When making a non-trivial case distinction, you want to state what your cases actually are, but when distinguishing three cases already explicitly stated via a disjunction it would produce unnecessary boilerplate to essentially restate these three cases.

Wolfgang Jeltsch (May 05 2023 at 14:12):

Looking at the example code @Mathias Fleury posted, I realize that with this style you even do restate the cases as assumptions; so there is really no need to be even more explicit and restate them via consider here.

Yosuke Ito (May 05 2023 at 22:02):

@Wolfgang Jeltsch I definitely agree with you. I appreciate your detail explanation.
@Bob Rubbens Please follow Wolfgang's advice. Sorry for confusing you, but I learned a lot from your question.

Bob Rubbens (May 06 2023 at 09:13):

No problem, I also learned a lot :)

Last updated: Apr 28 2024 at 12:28 UTC