c.f. Terence's talk and pairwise disjoint {1}, {2}, {3, 4}

Stream: Big Proof 2025

[Emilio Jesús Gallego Arias]

Hi folks, I'm curious about the problem @Terence Tao mention in his talk, in particular about a hard proof of "pairwise-disjoint { {1}, {2}, {3,4} }" IIRC.

Do we have more details? TIA!

[Terence Tao]

See the discussion around #Polynomial Freiman-Ruzsa conjecture > Balog-Szemerédi-Gowers @ 💬

[Kevin Buzzard]

The person sitting next to me during the talk assured me that grind will do this.

[Terence Tao]

import Mathlib

abbrev S1 : Fin 3 → Finset (Fin 4)
  | 0 => {0}
  | 1 => {1}
  | 2 => {2, 3}

example: Pairwise (Function.onFun Disjoint fun x ↦ S1 x) := by grind --`grind` failed

It doesn't one-shot the problem, but perhaps there is another way to use it?

[Emilio Jesús Gallego Arias]

Thanks a lot! I had tried some different versions and by simp did solve them! :eyes:

[Emilio Jesús Gallego Arias]

In particular this works

import Mathlib

def s0 : Finset (Fin 4) := {0}
def s1 : Finset (Fin 4) := {1}
def s23 : Finset (Fin 4) := {2,3}

lemma ex1 : Disjoint s0 s1 /\ Disjoint s0 s23 /\ Disjoint s1 s23 :=
  by simp [s0, s1, s23]

[Kim Morrison]

Kevin Buzzard said:

The person sitting next to me during the talk assured me that grind will do this.

@Terence Tao, grind will do this, but as with many many things grind will do, we need annotations set up first.

I'm working hard on this for the Lean standard library, but others are going to have to learn how to do this for Mathlib starting in a few weeks when we make the first release of grind.

I think all the following attributes would be reasonable library additions, and indeed grind then succeeds:

import Mathlib

attribute [grind _=_] LawfulSingleton.insert_emptyc_eq

attribute [grind =] Finset.mem_singleton

attribute [grind =] Finset.disjoint_insert_left
attribute [grind =] Finset.disjoint_insert_right
attribute [grind] Finset.disjoint_empty_left
attribute [grind] Finset.disjoint_empty_right

attribute [grind] Pairwise

abbrev S1 : Fin 3 → Finset (Fin 4)
  | 0 => {0}
  | 1 => {1}
  | 2 => {2, 3}

example: Pairwise (Function.onFun Disjoint fun x ↦ S1 x) := by
  grind

But it is slightly premature to declare success here. :-)

[Kim Morrison]

(This works on the nightly-testing branch, no guarantees on master!)

[Kim Morrison]

(Probably it will be better to annotate more generic versions of these lemmas rather than the Finset versions.)

[Peiran Wu]

Where can I read about grind? I checked the docs under Init/Grind but didn't find anything other than explanation of the config.

[Johan Commelin]

@Peiran Wu grind isn't officially released yet. It will be in the near future. The manual is being written right now (-;

[Peiran Wu]

Great. I found the PR for the manual.

I also found a discussion from March that contains some information.