Finset.choose

Stream: mathlib4

[Heather Macbeth]

@Jeremy Avigad and I just distilled the following strange behaviour of Finset.choose:

import Mathlib.Data.Finset.Basic

lemma foo : ∃! x, x ∈ ({0,3} : Finset (Fin 5)) ∧ x = 3 := by
  use 3
  simp

example : Finset.choose _ _ foo = 3 := by rfl -- works
example : Finset.choose _ _ foo = 3 := rfl -- fails
example : Finset.choose _ _ foo = 3 := by eq_refl -- works
example : Finset.choose _ _ foo = 3 := by exact rfl -- fails
example : Finset.choose _ _ foo = 3 := by decide -- fails

Among the strange points here are that, if you hover over eq_refl you get the docstring

eq_refl is equivalent to exact rfl, but has a few optimizations

which, it seems, is not true in this case!

[Heather Macbeth]

Is something wrong with the implementation of Finset.choose? We tried to make examples not using it, and failed.

[Eric Wieser]

(docs#Finset.choose)

[Eric Wieser]

A slightly simpler test using docs#List.choose with analogous behavior:

import Mathlib.Data.Finset.Basic

lemma foo : ∃ x, x ∈ ([0,3] : List (Fin 5)) ∧ x = 3 := by
  use 3
  simp

example : List.choose _ _ foo = 3 := by rfl -- works
example : List.choose _ _ foo = 3 := rfl -- fails
example : List.choose _ _ foo = 3 := by eq_refl -- works
example : List.choose _ _ foo = 3 := by exact rfl -- fails
example : List.choose _ _ foo = 3 := by decide -- fails

[Kyle Miller]

It seems to be a reducibility thing. This works:

example : Finset.choose _ _ foo = 3 := by with_unfolding_all exact rfl

[Eric Wieser]

I think this is due to a non-structural recursion

[Eric Wieser]

The let pattern match in chooseX is to blame

[Eric Wieser]

Patch incoming

[Eric Wieser]

#8753

[Eric Wieser]

I'm afraid this doesn't answer your question about eq_refl, nor do I know why the pattern match is problematic here.

[Eric Wieser]

This is "no eta for propositions" striking again

[Eric Wieser]

def ohno (h : True ∧ True) : Nat :=
  let ⟨_a, _b⟩ := h
  1

example : ohno sorry = 1 := rfl -- fails

def anyway (h : Unit × Unit) : Nat :=
  let ⟨_a, _b⟩ := h
  1

example : anyway sorry = 1 := rfl -- succeeds

[Kyle Miller]

Eric Wieser said:

I'm afraid this doesn't answer your question about eq_refl, nor do I know why the pattern match is problematic here.

One thing I noticed when digging into this earlier was that eq_refl uses the kernel to check that rfl works rather than using the elaborator's isDefEq check(*). I suspect isDefEq is more restrictive than the kernel here -- the kernel doesn't know about reducibility for example.

(*) This is conditional in the code. It uses the kernel if there are no metavariables or fvars.