Trivialities about sets

Stream: mathlib4

[Martin Dvořák]

Is there any tauto-like tactics that could solve trivialities about sets? I would like to use something similar to the former example to the latter example:

import Mathlib

example (A B C : Prop) :
    (B ∨ C) ∧ A ↔ (A ∧ C) ∨ (A ∧ B) := by
  tauto

example (α : Type) (A B C : Set α) :
    (B ∪ C) ∩ A = (A ∩ C) ∪ (A ∩ B) := by
  ext
  simp
  tauto

Chaining these three tactics works well, but I'd rather use a single tactic. In this case, I could use aesop for a one-line proof of the latter statement, but there are cases where I want to avoid aesop because the sets have some inner structure that misleads aesop but would be irrelevant for a tauto-like tactic.

[Patrick Massot]

This question comes periodically and I think we still don’t have a good answer.

[Damiano Testa]

In your cases, aesop solves both.

[Kyle Miller]

Maybe there could be a set_ext simp set (not sure about the name) loaded with simp lemmas that turn equalities of sets and subset relations into booleans?

Here are a few lemmas that could go into that simp set:

example (α : Type) (A B C : Set α) :
    (B ∪ C) ∩ A = (A ∩ C) ∪ (A ∩ B) := by
  simp only [Set.ext_iff, Set.mem_inter_iff, Set.mem_union]
  tauto

With the simp set, it could look like simp only [set_ext]; tauto

[Damiano Testa]

If there wasn't already a tactic called set, then set would be a good name for this one!

[Martin Dvořák]

This is my attempt at implementing it (and a few tests):

import Mathlib.Tactic.Tauto
import Mathlib.Data.Set.Basic

macro "setauto" : tactic =>
  `(tactic|
    try simp only [
      Set.ext_iff,
      Set.subset_def,
      Set.mem_inter_iff,
      Set.mem_union,
      Set.mem_compl_iff,
    ] at *
    <;>
    try tauto)

example (α : Type) (A : Set α) :
    A ⊆ Set.univ := by
  setauto

example (α : Type) (A : Set α) :
    ∅ ⊆ A := by
  setauto

example (α : Type) (A : Set α) (hA : A ⊆ ∅) :
    A = ∅ := by
  setauto

example (α : Type) (A : Set α) :
    Aᶜᶜ = A := by
  setauto

example (α : Type) (A : Set α) (hA : Aᶜ ⊆ ∅) :
    A = Set.univ := by
  sorry -- setauto -- fails

example (α : Type) (A B C : Set α) (hAB : A ⊆ B) (hBC : B ⊆ C) :
    A ⊆ C := by
  setauto

example (α : Type) (A B C : Set α) :
    (B ∪ C) ∩ A = (A ∩ C) ∪ (A ∩ B) := by
  setauto

example (α : Type) (A B C : Set α) :
    (Aᶜ ∪ B ∪ C)ᶜ = Cᶜ ∩ Bᶜ ∩ A := by
  setauto

example (α : Type) (A B C : Set α) :
    (Aᶜ ∩ B ∩ Cᶜᶜ)ᶜᶜᶜᶜᶜ = Cᶜ ∪ Bᶜ ∪ ∅ ∪ A ∪ ∅ := by
  setauto

example (α : Type) (A B C D : Set α) :
    D ∩ (B ∪ Cᶜ) ∩ A = (Aᶜᶜ ∩ Cᶜᶜᶜ ∩ D) ∪ (A ∩ Dᶜᶜ ∩ B)ᶜᶜ := by
  setauto

It was brought to my attention that docs#Mathlib.Tactic.Tauto.tauto doesn't work for universal quantifiers. Therefore, I cannot use tauto in this way probably. And I want a tactic that does not work with the internal structure of given sets, so aesop is not an option either.

[Martin Dvořák]

Can somebody make a Mathlib-ready tactic out of the setauto above?

[Jireh Loreaux]

Martin, I think you should specify precisely the scope of this tactic. What problems are in scope, and which are out of scope? After you have that list, try to make the above succeed on a collection of tests determined by your scope.

After you get that working, realize that it's likely the case that you don't want to transform your entire local context (with simp only ... at *) permanently when calling this tactic. So then learn a bit more to make it so it doesn't suffer from that problem. At that point, I think you can make the PR. Even if it's not Mathlib-ready, you can at least hope that people will suggest improvements.

[Lenny Taelman]

Has there been any follow-up work on this?

When working on this project I frequently wished for a single tactic that proved inclusions/equalities between iterated unions, intersections, and complements.

To add to the examples of @Martin Dvořák above, here are some typical test cases that I have in mind:

import Mathlib.Data.Set.Basic

variable {α : Type} (A B C D E : Set α)


example : A ∩ ∅ = ∅ := by sorry

example : A ∪ Set.univ = Set.univ := by sorry

example (h1 : A ⊆ B) (h2: B ⊆ A) : A = B := by sorry

example : A ∪ (B ∩ C) = (A ∪ B) ∩ (A ∪ C) := by sorry

example : A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C) := by sorry

example : A ⊆ (A ∪ B) ∪ C := by sorry

example : A ∩ (B ∪ C) ⊆ (A ∩ B) ∪ (A ∩ C) := by sorry

example : A ∩ B ⊆ A := by sorry

example : A ⊆ A ∪ B := by sorry

example (h1 : A ∩ B = Set.univ) : A = Set.univ := by sorry

example (h1 : Set.univ ⊆ A) : A = Set.univ :=by sorry

example (h1 : B ⊆ A) (h2 : Set.univ ⊆ B): Set.univ = A := by sorry

example (h1 : Aᶜ ⊆ ∅) : A = Set.univ := by sorry

example (h1 : A ⊆ B \ C) : A ⊆ B := by sorry

example (h1 : A ⊆ B) (h2 : C ⊆ D) : C \ B ⊆ D \ A := by sorry

example (h : A ⊆ B ∧ C ⊆ D) : C \ B ⊆ D \ A := by sorry

example (h1 : Disjoint A B) (h2 : C ⊆ A) : Disjoint C (B \ D) := by sorry

Some of these are exact statements of mathlib lemmas, and many of them can be handled by aesop or by Martin's tactic macro above. But I feel that a single tactic should be able to settle all of them (and in fact by reduction to an invocation of tauto).

If nobody has worked on this, I'd be excited to try to do this myself; but it would be even better if someone else with more experience wants to join or help out!

[Damiano Testa]

If you define

macro "set_tac" : tactic => `(tactic| first | (intro x; try simp; tauto) | aesop)

then all are solved with by set_tac, except

example (h1 : A ∩ B = Set.univ) : A = Set.univ := by sorry

example (h1 : A ⊆ B \ C) : A ⊆ B := by sorry

example (h1 : Disjoint A B) (h2 : C ⊆ A) : Disjoint C (B \ D) := by sorry

[Damiano Testa]

I also think that this should maybe be a lemma:

@[simp]
lemma inter_eq_univ : A ∩ B = Set.univ ↔ (A = Set.univ ∧ B = Set.univ) := by sorry

[Yaël Dillies]

Why is this in #lean4 ?

[Notification Bot]

This topic was moved here from #lean4 > Trivialities about sets by Kevin Buzzard.

[Martin Dvořák]

Yaël Dillies said:

Why is this in #lean4 ?

My bad, thanks for the move!

[Lenny Taelman]

I now have a version that passes all tests I could come up with. See here: https://github.com/LennyTaelman/setauto/blob/master/Setauto/Setauto.lean

Comments are very welcome! And examples that break this even more ;-)

One thing that kept causing trouble was the simp lemma univ_subset_iff (and its counterpart subset_empty_iff). Everything seemed to work much more easily when reversing the direction of simplification in these. Is there any deeper reason for these lemmas to work the way they currently do?

[Lenny Taelman]

Ok, chasing boundary cases trying to break the tactic, it seems I broke something more. Here is a minimal case:

import Mathlib.Tactic.Tauto

lemma weird (α : Type) (h : α → False) (x : α) : False := by
  tauto -- No goals, yet lean gives "application type mismatch"

#check weird -- unknown identifier 'weird'

The tactic tauto seems to work, yet lean does not infer a term `weird'. Is this supposed to be possible? Is it a bug in tauto? Or in some part of lean? Or in the infoview?

[Kevin Buzzard]

I get an error on the weird in lemma weird and I don't trust any Lean output (e.g. "no goals") after the first error in my code.

[Christian Merten]

This seems to be fixed on latest mathlib according to the live server.

[Johan Commelin]

docs#Set.univ_subset_iff and docs#Set.subset_empty_iff

[Johan Commelin]

I agree that it would make sense to flip the simp direction of those.
We should just try that, and see if Mathlib still builds (-;

[Christian Merten]

docs#Set.univ_subset_iff matches docs#top_le_iff though (same for docs#Set.subset_empty_iff and docs#le_bot_iff).

[Johan Commelin]

I would be inclined to flip those as well, and see what happens

[Lenny Taelman]

Here is a simpler new version that seems to tackle the boundary cases as well: https://github.com/LennyTaelman/setauto/blob/master/Setauto/Setauto.lean

The main point is a custom tactic 'specialize_all' that attempts to specialize all hypotheses in the local context at a common term.

The actual setauto tactic then becomes:

macro "setauto" : tactic => `(tactic|(
  simp_all only [
    Set.diff_eq, Set.disjoint_iff,
    Set.ext_iff, Set.subset_def,
    Set.mem_union, Set.mem_compl_iff, Set.mem_empty_iff_false,
    Set.mem_inter_iff,
  ];
  try intro x
  try specialize_all x
  tauto
))

Feedback is very welcome!

[Lenny Taelman]

One remaining issue: how do I make this into a tactic that either succeeds or raises an error? The tauto tactic will raise an error if it fails (as desired), but it will also raise an error if the simp already closes the goal.

[Lenny Taelman]

And here is the specialize_all tactic code:

syntax (name := specialize_all) "specialize_all" term : tactic

@[tactic specialize_all] def evalSpecializeAll : Tactic :=
    fun stx => withMainContext do
  match stx with
  | `(tactic| specialize_all $x:term) =>
    -- loop over all hypotheses h
    let ctx ← Lean.MonadLCtx.getLCtx
    ctx.forM fun h: Lean.LocalDecl => do
      let s ← saveState
      try
        -- run `specialize h x`
        evalTactic (← `(tactic|specialize $(mkIdent h.userName) $x))
      catch _ =>
        restoreState s
  | _ => throwError "unexpected input"

[Damiano Testa]

If you use <;> tauto, tauto will not run if the previous tactics close all goal.

[Damiano Testa]

Ending with done will raise an error if there are open goals.

[Damiano Testa]

It is probably safer to add a focus at the very start of the tactic calls.

[Damiano Testa]

(Sorry that I'm so brief: I'm on mobile!)

[Lenny Taelman]

ah, never seen this focus thing. Let me see if I can dig up an example/doc...

[Damiano Testa]

Basically it makes the tactic act on the current goal, it's subgoals, but will not leak into a second goal.

[Damiano Testa]

So, if you had two goal and simp closes the first, you do not want tauto tackling the second one.

[Lenny Taelman]

makes sense!

[Damiano Testa]

Of course, it is already dubious form to have two accessible goals, but that is no reason to avoid building more robust tactics!

[Lenny Taelman]

/poll What would be a good name for this tactic? (Alas "set" is already taken...)
setauto
set_tauto
tauto_set

[Kevin Buzzard]

(I voted for tauto_set because of aesop_cat)

[Lenny Taelman]

That convinced me!

[Martin Dvořák]

Good point!

[Martin Dvořák]

Lenny Taelman said:

Comments are very welcome! And examples that break this even more ;-)

Can you please test the following examples?
https://github.com/Ivan-Sergeyev/seymour/blob/d8fcfa23336efe50b09fa0939e8a4ec3a5601ae9/Seymour/ForMathlib/SetTheory.lean
I would like your tactic to solve most of them.

[Lenny Taelman]

Thanks for the test cases! Some of those are outside of the scope (containing strict subsets or other forms of hidden existential quantifiers), and I don't think it would be reasonable to extend the scope (we'd quickly run into things that are meant for SAT solvers). All the ones that are within scope are solved by setauto, and some of them are quite significant compressions...

See https://github.com/LennyTaelman/setauto/blob/master/Setauto/Setauto.lean for the updated file including your test cases.

[Damiano Testa]

In case it is helpful, you can simplify your code:

diff --git a/Setauto/Setauto.lean b/Setauto/Setauto.lean
index ad8dc49..7d6c0f0 100644
--- a/Setauto/Setauto.lean
+++ b/Setauto/Setauto.lean
@@ -26,22 +26,11 @@ open Lean Elab.Tactic
   `specialize h x` for all hypotheses `h` where this tactic succeeds.
 -/

-syntax (name := specialize_all) "specialize_all" term : tactic
-
-@[tactic specialize_all] def evalSpecializeAll : Tactic :=
-    fun stx => withMainContext do
-  match stx with
-  | `(tactic| specialize_all $x:term) =>
-    -- loop over all hypotheses h
-    let ctx ← Lean.MonadLCtx.getLCtx
-    ctx.forM fun h: Lean.LocalDecl => do
-      let s ← saveState
-      try
-        -- run `specialize h x`
-        evalTactic (← `(tactic|specialize $(mkIdent h.userName) $x))
-      catch _ =>
-        restoreState s
-  | _ => throwError "unexpected input"
+elab (name := specialize_all) "specialize_all" x:term : tactic => withMainContext do
+  -- loop over all hypotheses h
+  for h in ← getLCtx do
+    -- run `specialize h x`
+    evalTactic (← `(tactic|specialize $(mkIdent h.userName) $x)) <|> pure ()


 macro "tauto_set" : tactic => `(tactic|

[Lenny Taelman]

Thanks! This seems actually more robust in my tests, with <|> catching errors that the try-catch block in the original code doesn't. I'll have to delve more into the different ways tactics can produce errors...

[Damiano Testa]

As a general rule, try ... catch to simply restore a state is often better implemented using a "backtrack".

Anyway, I am glad that this is helpful!

[Damiano Testa]

Not all monads have backtracking, though: I think that MetaM, TermElabM and TacticM do, but CommandElabM does not. (To be confirmed!)

[Lenny Taelman]

Thanks everyone for your help. I have now committed the tauto_set tactic to a branch of the mathlib4 repository, see here.

Before I make a pull request (my first), I have a few more questions:

1. Do I include the test examples? Do they go somewhere else in mathlib? Or are they just discarded? They could be useful in asserting that changes elsewhere (e.g. in a simp lemma) don't break the tactic?
2. What/where else should I document? And more generally: how do I make sure users actually know about this tactic and use it where appropriate?
3. Anything else I should pay attention to?

[Kevin Buzzard]

Yes tests definitely go with the PR. I've never PRed a tactic myself but looking at past PRs of tactics it looks like you should dump the test file in MathlibTest/tauto_set.lean. I would also be tempted to put two examples in the docstring for the tactic. Users will just come to learn about it by osmosis.

[Bryan Gin-ge Chen]

Regarding tests, they should go in a new file in the MathlibTest directory (see the other examples there).

[Damiano Testa]

Wrt 2, you could also use your tactic in a few places in mathlib, to show how it works "in the real world" to golf/uniformize a few proofs. It does not have to be exhaustive, in order to avoid creating too much extra diff. Alternatively, you could also open a dependent PR that, on top of a PR that only adds the tactic (and the tests), uses it in mathlib: in this case, you can try to be more exhaustive.

[Damiano Testa]

The possibility of viewing what kinds of proofs get simplified/are in scope for the tactic is helpful for the review process.

[Lenny Taelman]

Thanks for all your help! This is now PR #20706.

[Violeta Hernández]

Are there any easy candidates for files where this could be used to golf proofs?