Something like `linarith` or `ring` for basic set theory?

Stream: new members

[Stuart Presnell]

We have tactics like linarith and ring to automatically fill in proofs of basic equations and inequalities in arithmetic. Is there a corresponding tactic for proving basic equations and inclusions in set theory (things involving unions, intersections, sdiffs, complements etc.) ?

[Johan Commelin]

I think the group that was working on matroids had such a tactic. But I don't think it landed in mathlib...

[Yakov Pechersky]

Would tauto or itauto discharge this? Since such statements are just statements over a (generalized) boolean algebra

[Bryan Gin-ge Chen]

Johan Commelin said:

I think the group that was working on matroids had such a tactic. But I don't think it landed in mathlib...

For reference: https://github.com/apnelson1/lean-set-tactic

Zulip thread here

[Stuart Presnell]

I've just tried tauto and itauto on example {X : Type*} (S T : set X) : T ⊆ (univ \ S) ∪ (S ∩ T) and they weren't able to solve it.

[Stuart Presnell]

Thanks for the pointer Bryan, I'll take a look at that

[Kevin Buzzard]

Does intro x, finish work?

[Stuart Presnell]

Oh, it does :)

[Stuart Presnell]

Thanks!

[Stuart Presnell]

Two notes for the benefit of anyone finding this thread later:
(1) use ext x, finish to prove set-theoretic equations; use intro x, finish to prove subset inclusions.
(2) you may need to re-write or unfold some premises. For example, this approach fails with (hST: S ⊆ T) ⊢ univ \ S ∪ T = univ, but works if we first use rw subset_def at hST to change the premise to hST: ∀ (x : X), x ∈ S → x ∈ T.

[Kevin Buzzard]

Another finish tip is that it doesn't try split, so if you're proving P <-> Q then you might want to try split; finish (which sometimes works even when finish doesn't).