Stream: Beginner Questions

Topic: proving set equality in Isabelle/HOL?

Jason Hu (Aug 12 2022 at 21:49):

Hi, I have some trouble proving set equalities. Currently I am using auto to simplify goals for me but I suppose this is not a good style. I think I should apply Lifting_Set.rel_set_eq, but this requires rewriting from the opposite direction. what am I missing here? how should I get started to prove two sets are equal?

Wenda Li (Aug 13 2022 at 08:00):

Hi Jason, proving set equalities is usually not an easy goal. Depending on the situations, we can manually choose some introduction rules to make progress. For example, the following rules could be quite handy:

  Set.subset_antisym: ?A ⊆ ?B ⟹ ?B ⊆ ?A ⟹ ?A = ?B
  Set.set_eqI: (⋀x. (x ∈ ?A) = (x ∈ ?B)) ⟹ ?A = ?B
  Finite_Set.card_subset_eq: finite ?B ⟹ ?A ⊆ ?B ⟹ card ?A = card ?B ⟹ ?A = ?B
  Finite_Set.card_seteq: finite ?B ⟹ ?A ⊆ ?B ⟹ card ?B ≤ card ?A ⟹ ?A = ?B

We can apply those introduction rules using the rule tactic (e.g., apply (rule Set.subset_antisym)).

As for Lifting_Set.rel_set_eq, it is not meant to be used in this situation -- it is mainly for the lift and transfer framework in Isabelle (i.e., a way to exploit relational parametricity).

Last updated: Oct 13 2024 at 01:36 UTC