Question about List.Mem

Stream: new members

[Kevin Cheung]

The documentation for List.Mem has the following:

inductive List.Mem {α : u} (a : α) : List α → Prop

a ∈ l is a predicate which asserts that a is in the list l. Unlike elem, this uses = instead of == and is suited for mathematical reasoning.a ∈ [x, y, z] ↔ a = x ∨ a = y ∨ a = z.

Now, for the following:

example (d : ℕ): d ∈ Nat.divisors 6 ↔ d = 1 ∨ d = 2 ∨ d = 3 ∨ d = 6 := by
  reduce

the info view after reducehas

d : ℕ
⊢ List.Mem d [1, 2, 3, 6] ↔ d = 1 ∨ d = 2 ∨ d = 3 ∨ d = 6

At this point simp doesn't close the goal even though the line a ∈ [x, y, z] ↔ a = x ∨ a = y ∨ a = z in the documentation quoted above seems to suggest that it does. A

Right now, I'm proving the example like this:

example (d : ℕ): d ∈ Nat.divisors 6 ↔ d = 1 ∨ d = 2 ∨ d = 3 ∨ d = 6 := by
  have : d ∈ Nat.divisors 6 ↔ d ∈ ({1, 2, 3, 6} : Finset ℕ) := by exact Eq.to_iff rfl
  rw [this]
  simp

I have a feeling that there should be a very simple proof. Am I missing something very obvious here? Pointers greatly appreciated.

[James Sundstrom]

example (d : ℕ): d ∈ Nat.divisors 6 ↔ d = 1 ∨ d = 2 ∨ d = 3 ∨ d = 6 := by
  change d ∈ [1, 2, 3, 6] ↔ _
  simp

[Ruben Van de Velde]

I'd never heard of reduce, but it seems like a terrible idea

[Kyle Miller]

Note: reduce is generally not a tactic that you should expect to be useful for making progress; rather it's useful for understanding the innards of terms. It's unsurprising that simp can't close a goal after reduce — the issue is that simp lemmas expect things to be in particular forms, and reduce does indiscriminate reduction. In particular, List.Mem isn't "simp normal form". (That said, possibly we're missing a simp lemma that rewrites List.Mem back to element notation.)

[Ruben Van de Velde]

import Mathlib
example (d : ℕ): d ∈ Nat.divisors 6 ↔ d = 1 ∨ d = 2 ∨ d = 3 ∨ d = 6 := by
  have : Nat.divisors 6 = {1, 2, 3, 6} := by decide
  simp [this]

[Ruben Van de Velde]

Though it would be nice if norm_num could solve the first step

[Kyle Miller]

Here's a proof that doesn't mention elements:

example (d : ℕ): d ∈ Nat.divisors 6 ↔ d = 1 ∨ d = 2 ∨ d = 3 ∨ d = 6 := by
  constructor
  · rw [← Nat.filter_dvd_eq_divisors (by simp), Finset.mem_filter, Finset.mem_range, and_imp]
    decide +revert
  · intro
    casesm* _ ∨ _ <;> subst_vars <;> decide

[Kyle Miller]

That whole second case can be replaced with simp +contextual [or_imp]

[Kyle Miller]

@Ruben Van de Velde That by decide is probably a slower version of rfl

[Aaron Liu]

With quotients they are not always equivalent

[Aaron Liu]

But in this case rfl works

[Kevin Cheung]

Thank you. I did want a way to do this without mentioning the elements. If a lemma that does the expansion is added, that'll be wonderful.

[Kyle Miller]

Aaron Liu said:

With quotients they are not always equivalent

But in this case rfl works

Certainly, though I wasn't making a general claim about decide.

[Kevin Cheung]

I have not seen casesm* before. Is this something quite new?

[Kyle Miller]

I think Lean 3 had it, and the Lean 4 version was written by Mario in 2022 https://github.com/leanprover-community/mathlib4/commits/master/Mathlib/Tactic/CasesM.lean

[Kevin Cheung]

Kyle Miller said:

Here's a proof that doesn't mention elements:

example (d : ℕ): d ∈ Nat.divisors 6 ↔ d = 1 ∨ d = 2 ∨ d = 3 ∨ d = 6 := by
  constructor
  · rw [← Nat.filter_dvd_eq_divisors (by simp), Finset.mem_filter, Finset.mem_range, and_imp]
    decide +revert
  · intro
    casesm* _ ∨ _ <;> subst_vars <;> decide

Is there a way to avoid "decide +revert"? It seems that it only works with recent versions of Lean.

EDIT: I figured out. revert d then decide works.