Stream: Beginner Questions

Topic: ✔ Rewrite term using a proven "p ==> q" theorem?


view this post on Zulip Jiahong Lee (Dec 19 2022 at 06:46):

I see, thanks! The subst proof method does the trick for me:

lemma "p ∨ q ⟹ p ∨ ¬ ¬ q"
proof -
  assume "p ∨ q"
  thus "p ∨ ¬ ¬ q" by(subst not_not)
qed

lemma "p ∨ ¬ ¬ q ⟹ p ∨ q"
proof -
  assume "p ∨ ¬ ¬ q"
  thus "p ∨ q" by(subst not_not[symmetric])
qed

Given a theorem , it substitutes terms matching its RHS by its LHS.

view this post on Zulip Jiahong Lee (Dec 19 2022 at 06:48):

However, it doesn't work in calculational reasoning:

lemma "(P ⟶ Q) ⟷ ¬ (P ∧ ¬ Q)"
proof -
  have "(P ⟶ Q) = (¬ P ∨ Q)" by(rule imp_conv_disj)
  also have "... = (¬ P ∨ ¬ ¬ Q)" by(subst not_not) (* Error! *)

view this post on Zulip Jiahong Lee (Dec 19 2022 at 06:49):

After searching around, the unfolding proof method does the trick for me:

lemma "(P ⟶ Q) ⟷ ¬ (P ∧ ¬ Q)"
proof -
  have "(P ⟶ Q) = (¬ P ∨ Q)" by(rule imp_conv_disj)
  also have "... = (¬ P ∨ ¬ ¬ Q)" unfolding not_not by(rule refl) (* Ok! *)

view this post on Zulip Notification Bot (Dec 19 2022 at 06:49):

Jiahong Lee has marked this topic as resolved.

view this post on Zulip Mathias Fleury (Dec 19 2022 at 09:06):

Jiahong Lee said:

However, it doesn't work in calculational reasoning:

lemma "(P ⟶ Q) ⟷ ¬ (P ∧ ¬ Q)"
proof -
  have "(P ⟶ Q) = (¬ P ∨ Q)" by(rule imp_conv_disj)
  also have "... = (¬ P ∨ ¬ ¬ Q)" by(subst not_not) (* Error! *)

as you noticed, subst only does the substitution, not proving that ?A = ?A, so

  also have "... = (¬ P ∨ ¬ ¬ Q)" by(subst not_not) (rule refl)

view this post on Zulip Wolfgang Jeltsch (Dec 19 2022 at 15:31):

Note that rule refl is something that the standard proof method covers, so that you can replace rule refl by ...

view this post on Zulip Wolfgang Jeltsch (Dec 19 2022 at 15:32):

By the way, it took me years of intensely working with Isabelle to discover that; actually, my colleague @Javier Diaz discovered it, and I saw him using this trick. Before, I had resorted to simp in such situations, which might often be considered overkill.

view this post on Zulip Jiahong Lee (Dec 20 2022 at 02:12):

as you noticed, subst only does the substitution, not proving that ?A = ?A,

Ah, I see, the error message didn't make sense to me previously, thanks!

view this post on Zulip Jiahong Lee (Dec 20 2022 at 02:19):

Note that rule refl is something that the standard proof method covers, so that you can replace rule refl by ...

Thanks for your info, but right now I prefer an explicit proof method for better understanding


Last updated: Feb 27 2024 at 08:17 UTC