Finset.range_two

Stream: Is there code for X?

[Terence Tao]

In my own project I recently needed a proof that Finset.range 2 = {0,1}. I initially had an embarrasingly long proof of this,

import Mathlib
import Mathlib.Tactic

example : Finset.range 2 = {0,1} := by
  ext a
  simp
  constructor
  . intro ha
    have ha' : a ≤ 1 := by linarith [ha]
    rcases a with a | a
    . norm_num
    rw [Nat.succ_eq_add_one]
    rw [Nat.succ_eq_add_one] at ha'
    have ha'' : a = 0 := by linarith
    right
    rw [ha'']
  intro ha
  rcases ha with h | h
  . norm_num [h]
  norm_num [h]

but eventually realized that due to existing tools such as Finset.range_one, it was much easier:

example : Finset.range 2 = {0,1} := by
  rw [(show 2 = Nat.succ 1 by norm_num), Finset.range_succ]
  simp

But I wonder if one should actually have a Finset.range_two simp lemma in the Mathlib for this sort of situation. What is the general philosophy regarding simp lemmas - should one stuff in as many random lemmas like this into the mathlib that would come up occasionally but not incredibly frequently, or should one be more minimalist?

[Heather Macbeth]

Not addressing your direct question, but for me, these both work:

import Mathlib

example : Finset.range 2 = {0,1} := by simp
example : Finset.range 2 = {0,1} := rfl

[Heather Macbeth]

Do they on your mathlib version?

[Terence Tao]

Okay, I'm embarrassed to say I never even tried this!

[Terence Tao]

In which case there is probably no need for an explicit Finset.range_two lemma in mathlib.

[Heather Macbeth]

There's even automation (a "linter") which is supposed to prevent mathlib from getting simp lemmas which would provide duplicate simp-ing paths to an existing path.

[Jireh Loreaux]

There's a few things to say here:

1. Just as a tip, one way you may have been able to suspect the proof was rfl easier once you got down to this code:

example : Finset.range 2 = {0,1} := by
  rw [(show 2 = Nat.succ 1 by norm_num), Finset.range_succ]
  simp

Is by calling simp? which says Try this: simp only, which means that it wasn't applying any simp lemmas. And then you might just try deleting stuff, and you'll find that you get all the way down to rfl.

2. Your question is still valid for explicit lemmas like Finset.range_two which are not provable by rfl, and the answer is that sometimes we provide convenience lemmas for special cases. Generally, I would say the rule of thumb is: if someone needed it, they probably wrote it and added it to mathlib (assuming it passes the simpNF linter Heather referred to).

The following aren't all necessarily simp lemmas, but they are the sorts of special case lemmas you were considering here:
docs#half_pos, docs#zero_lt_four, docs#Finset.card_doubleton, docs#isLUB_pair, and there are plenty more throughout the library.

[Junyan Xu]

I just found that the defeq of List.Mem changed from Lean 3 to Lean 4 and as a consequence destructing Finset membership becomes more complicated:

example : ∀ x ∈ Finset.range 2, x = 0 ∨ x = 1 := by
  rintro _ (_|⟨_,(_|⟨_,⟨⟩⟩)⟩)
  exacts [Or.inl rfl, Or.inr rfl]

in Lean3 it used to be rintro (rfl|rfl|⟨⟩) IIRC.