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?
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)).
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: Dec 07 2023 at 20:16 UTC