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 found 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"?

Manuel Eberl (Aug 18 2021 at 19:18):

proof (intro equalityI subsetI)

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

Thanks! How did you find it? Is there a way to see what is applied by the default "proof" (or is it just experience)?

Notification Bot (Aug 18 2021 at 19:48):

Sophie Tourret has marked this topic as resolved.

Manuel Eberl (Aug 18 2021 at 19:55):

I think it's just experience. You can use find_theorems to search for theorems that you think ought to be there.

Manuel Eberl (Aug 18 2021 at 19:57):

I don't remember the exact rule for what proof does; I think it uses the standard method, which does a bunch of things. In particular, it can apply any one rule that is marked as an intro rule, which is the case for equalityI.

Manuel Eberl (Aug 18 2021 at 19:59):

You can also do proof safe. The method safe applies any introduction rule marked as safe (i.e. that supposedly does not turn provable goal states into unprovable ones). This includes, in particular, things like introduction rules for $\wedge \forall \subseteq$ and implication. But sometimes it does a bit too much for my taste, that's why I often prefer the intro method with explicit introduction rules.

Manuel Eberl (Aug 18 2021 at 20:00):

Basically, every logical connective (and many other predicates) has one or more introduction rule that you can use to prove it, and applying these is often a good way to start off a proof.

Manuel Eberl (Aug 18 2021 at 20:00):

These are usually called <name of the predicate>I, e.g. conjI, allI, impI.

Last updated: Apr 19 2024 at 04:17 UTC