list.mem_diff_iff?

Stream: general

[Henning Dieterichs]

There seems to be list.mem_diff_of_mem, but I cannot find a mem-based iff characterization of list.diff (which would be great as simp lemma). Is that lemma just missing?
I'm looking for this:

theorem mem_diff_iff {α: Type} [decidable_eq α] {a : α} : ∀ {l₁ l₂ : list α}, a ∈ l₁.diff l₂ ↔ a ∈ l₁ ∧ a ∉ l₂ := by sorry

library search fails.

[Alex J. Best]

There is docs#list.mem_diff_iff_of_nodup which has the right side condition, otherwise

#eval to_bool $ 1 ∈ [1,1].diff [1] ↔ 1 ∈ [1,1] ∧ 1 ∉ [1]

[Henning Dieterichs]

Oh, I thought diff would remove all elements! I only looked through all lemmas in the diff section here. Thanks for the counterexample!

[Bryan Gin-ge Chen]

slim_check is able to generate counterexamples too:

import tactic.slim_check

example (a : ℕ) : ∀ {l₁ l₂ : list ℕ}, a ∈ l₁.diff l₂ → a ∈ l₁ ∧ a ∉ l₂ :=
by slim_check
/-
===================
Found problems!

a := 0
l₁ := [4, 4, 11, 178, 7, 5, 0, 0]
l₂ := [511, 0, 2, 8, 3]
(0 shrinks)
-------------------
-/

It's missing a tactic doc entry, but there's info in the tactic.slim_check module doc.

[Henning Dieterichs]

Wow, slim_check is nice. It would be so cool if slim_check, library_search, and finish were run in the background for every unclosed goal!

[Kevin Buzzard]

Ha ha! If I'm working on discrete valuation rings then these things have 0 chance of doing anything unless I'm on the last line of a proof, and all that would happen would be that my PC would start heating the room!

[Kevin Buzzard]

We could also add that gpt command which @Jesse Michael Han was showing off to me on the Discord yesterday ;-) I saw it proving a few lemmas of the natural number game!

[Kevin Buzzard]

But I think that's a story for later on this week at the conference...