Stream: Beginner Questions

Topic: Default proof method creates an unprovable goal

Alexandre Soares (Sep 27 2024 at 19:02):

I'm trying to prove P ∨ (Q ∧ R) from the premises P ∨ Q and P ∨ R. When I write

lemma "(P ∨ Q) ⟹ (P ∨ R) ⟹ (P ∨ (Q ∧ R))"
proof

the goal gets simplified to P ∨ Q ⟹ P ∨ R ⟹ P. What proof method is being applied automatically and why? Clearly I can't show P from P ∨ Q and P ∨ R.

Mathias Fleury (Sep 27 2024 at 19:09):

The default proof method is called standard. If you want no proof method, you need proof - instead of proof standard or proof

Mathias Fleury (Sep 27 2024 at 19:12):

The default method seems to be applying disjI1 here (try lemma ‹P ⟹ P ∨ Q› and see what solves_direct gives you)

Alexandre Soares (Sep 27 2024 at 19:50):

Mathias Fleury said:

(try lemma ‹P ⟹ P ∨ Q› and see what solves_direct gives you)

I don't how to implement this suggestion, I'm still learning Isar and I'm trying to prove simple theorems to get more used to the language.

I tried to do it using prove - at the beginning:

  lemma "(P ∨ Q) ⟹ (P ∨ R) ⟹ (P ∨ (Q ∧ R))"
  proof -
    assume "P ∨ Q"           (* 1 *)
    then show "P ∨ Q ∧ R"
    proof                    (* 2 *)
      assume "P"
      thus "P ∨ Q ∧ R" by simp
    next
      assume "Q"
      show "P ∨ Q ∧ R"
      proof -

My intent was to split the proof in two cases with the hypothesis P ∨ Q, and then on Q split it further using the hypothesis P ∨ R. So I assumed P ∨ Q at line (* 1 *) and split the proof at line (* 2 *). The P case goes smoothly. To continue in the Q case I need to use the hypothesis P ∨ R to split again, but it's not available to me, I assume because I did not include it at line (* 1 *); if I do include it there, then it doesn't let me split with disjE at line (* 2 *) (even if I explicitly try proof (rule disjE [of "P" "R"])), so I'm stuck.

Katherine Kosaian (Oct 01 2024 at 18:55):

Try setting up your proof assuming both P v Q and P v R. E.g.

lemma "(P ∨ Q) ⟹ (P ∨ R) ⟹ (P ∨ (Q ∧ R))"
proof -
assume p_or_q: "P ∨ Q"
assume p_or_r: "P ∨ R"
show "(P ∨ (Q ∧ R))"
sorry
qed

Notice that I've labeled these facts as p_or_q and p_or_r, respectively, to make it easier to use them later on in the proof.

Then you can further split the proof to assume P and Q individually, e.g.

lemma "(P ∨ Q) ⟹ (P ∨ R) ⟹ (P ∨ (Q ∧ R))"
proof -
assume "P ∨ Q"
assume "P ∨ R"
{assume p: "P"
have "(P ∨ (Q ∧ R))"
sorry
} moreover {assume q: "Q"
have "(P ∨ (Q ∧ R))"
sorry
}
ultimately show "(P ∨ (Q ∧ R))"
sorry
qed

where again I've labeled these as "p" and "q" respectively. This should get you unstuck! The proof by cases structure is very useful, so I'd recommend investing into learning how to use it.

Alexandre Soares (Oct 01 2024 at 21:37):

@Katherine Kosaian Thanks! I actually managed to get unstuck in my original problem by removing the then at the line before line (* 2 *) and using proof (rule disjE) at line (* 2 *). Surely the method wasn't being accepted due to some conflict of assumptions. I guess I don't yet fully understand the interplay between assumptions contained in the goal and assumptions that are inside the proof context.

I will try to do it using your suggestion as well.

Mathias Fleury (Oct 02 2024 at 04:40):

Assumptions in the proof context do not exist for proof methods. You must pass them via using assms. This is why many induction proofs look like:

  using assms
proof (induction ...)

because the assumption do not exist for induction otherwise. There is nothing implicit in Isar.

Alexandre Soares (Oct 02 2024 at 14:41):

In this case it was the opposite, there were assumptions from the proof context being carried by then that I didn't think would affect the applicability of the method, but they did.

Mathias Fleury (Oct 02 2024 at 14:45):

Yeah stuff like rule X assumes that the assumptions are passed in the same order as needed for X

Last updated: Dec 21 2024 at 16:20 UTC