Proving set-related theorems using `aesop`

Stream: new members

[Pranav cs22b015]

I wish to prove the following theorem as part of a larger proof involving concurrent sets.

theorem my_theorem: ∀ (s : Set (ℕ × ℕ)) (fst: ℕ) (e1: ℕ), {x | (x = (fst, e1) ∨ x ∈ s) ∧ ¬x.2 = e1} = insert (fst, e1) {x | x ∈ s ∧ ¬x.2 = e1} → False

The LHS of the theorem cannot contain an element of the form (fst, e1) for any natural number fst. However, the RHS does. Therefore, we should be able to prove a contradiction.
I wish to use automated proving using aesop predominantly, although proving it with tactics would also be a start. As an aside, is there a nice way to reason about sets built using the set builder format?

[Notification Bot]

A message was moved here from #lean4 > Proving set-related theorems using `aesop` by Kevin Buzzard.

[Anthony Wang]

Here's a golfed version of the proof that was sent in the wrong channel:

import Mathlib

theorem my_theorem (s : Set (ℕ × ℕ)) fst e1
    (h : {x | (x = (fst, e1) ∨ x ∈ s) ∧ ¬x.2 = e1} = insert (fst, e1) {x | x ∈ s ∧ ¬x.2 = e1}) : False := by
  have : (fst, e1) ∉ {x | (x = (fst, e1) ∨ x ∈ s) ∧ ¬ x.2 = e1} := by simp
  aesop

[Anthony Wang]

For dealing with the set builder notation, you can convert a ∈ {x | f x} to f a using a simp:

example {α} (f : α → Prop) (a : α) (ha : a ∈ {x | f x}) : f a := by
  simp at ha
  exact ha

[Pranav cs22b015]

Thank you for your responses! I'm more curious to know if there is a standard library of sorts of theorems involving sets to give as hints to the simp / aesop tactic so that I don't have to prove these simple theorems each time? Most of the theorems I'm interested in can be proved by using lemmas involving just construction. For example,

1. lemma1 : forall (l: Set t) (x: t), l ∩ insert x l = l
2. lemma2: forall (l: Set t) (x: t), insert x (insert x l) = insert x l
3. lemma3: forall (l: Set t) (x: t), insert x l = { y | y ∈ l ∨ y = x }

I am looking for a single tactic which applies all basic set operations and simplifies my goal

[Anthony Wang]

There's Mathlib/Data/Set/Insert.lean which contains some useful theorems about set insertion but many of them are already tagged with @[simp] so they should be automatically used by simp.

[Anthony Wang]

You could also try using grind. (For the differences between grind and aesop see #mathlib4 > grind vs aesop @ 💬 )

[Pranav cs22b015]

Is there a way to add all theorems in the standard library related to sets to the results usable by grind ?

[Anthony Wang]

It looks like some of the set-related theorems in mathlib are already tagged with @[grind], but you can use grind [theorem1, theorem2] to use additional theorems when you use grind in a proof.