proof pattern for set equality · Beginner Questions

Stream: Beginner Questions

Topic: proof pattern for set equality

Sophie Tourret (Aug 18 2021 at 19:14):

Hello,

In the theory I am currently working on, I find myself frequently having to prove $A = B$ where $A$ and $B$ are sets. Here is how I did it

lemma what_i_do: "(A::'a set) = B"
proof
  show "A ⊆ B"
  proof
    fix x
    assume "x ∈ A"
    show "x ∈ B" sorry
  qed
next
  show "B ⊆ A"
  proof
    fix x
    assume "x ∈ B"
    show "x ∈ A" sorry
  qed
qed

I find this approach really heavy but I need the two sides decomposition, so I added the following:

lemma shortcut:
  assumes "⋀x. x∈A ⟹ x∈B" and
    "⋀x. x∈B ⟹ x∈A"
  shows "A = B"
  using assms by fastforce

This allows me to write instead:

lemma what_i_want_to_do: "(A::'a set) = B"
proof (rule shortcut)
  fix x
  assume "x ∈ A"
  show "x ∈ B" sorry
next
  fix x
  assume "x ∈ B"
  show "x ∈ A" sorry
qed

My question is: can I achieve the same thing using existing rules instead of my ad-hoc "shortcut"?

Last updated: Jul 15 2022 at 23:21 UTC