Stream: Beginner Questions

Topic: How to break down these conjuncts directly?


view this post on Zulip Jiahong Lee (Dec 18 2022 at 13:55):

Hi, in my structured proof, I have "P /\ Q" as my intermediate state, but I'd like to have "P" and "Q" directly. E.g.

theorem "(A ∪ B) - B ⊆ A"
proof (rule subsetI)
  fix x assume 1: "x ∈ (A ∪ B) - B"
  hence "x ∈ A ∪ B ∧ x ∉ B" by(rule Diff_iff[THEN iffD1]) (* <=== This line is redundant *)
  hence 2: "x ∈ A ∪ B" and 3: "x ∉ B" by(rule conjunct1, rule conjunct2)
  oops

I want to simplify it into:

theorem "(A ∪ B) - B ⊆ A"
proof (rule subsetI)
  fix x assume 1: "x ∈ (A ∪ B) - B"
  hence 2: "x ∈ A ∪ B" and 3: "x ∉ B" by(rule Diff_iff[THEN iffD1[THEN (conjunct1,conjunct2)]]) (* Error, doesn't work! *)
  oops

What is the correct proof method composition for my case?

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

the hence only threads the fact to the first rule, not the second:

  hence 2: "x ∈ A ∪ B" and 3: "x ∉ B"
    by (rule Diff_iff[THEN iffD1[THEN conjunct1]])
     (use 1 in ‹rule Diff_iff[THEN iffD1[THEN conjunct2]]›)

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

and THEN (conjunct1,conjunct2) does not exist

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

but you could go for

  hence 2: "x ∈ A ∪ B" and 3: "x ∉ B"
    by (rule Diff_iff[THEN iffD1[THEN conjunct1]] Diff_iff[THEN iffD1[THEN conjunct2]])+

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

(rule applies one of the theorems that matches)

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

that being said, you should not do that and use auto instead


Last updated: Feb 27 2024 at 08:17 UTC