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)`

).

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