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.

[Jeremy Tan]

This seems to be a related problem.

import Mathlib.Order.Partition.Equipartition
import Mathlib.Data.Nat.Interval

open Finset

namespace Finpartition

variable {α : Type*} [DecidableEq α] {s : Finset α} {P : Finpartition s} {a : α}

noncomputable def IsEquipartition.partsEquiv (hP : P.IsEquipartition) :
    { x // x ∈ P.parts } ≃ { x // x ∈ Ico 0 P.parts.card } := sorry

noncomputable def IsEquipartition.equivProduct2 (hP : P.IsEquipartition) :
    { t : Finset α × ℕ // t.1 ∈ P.parts ∧ t.2 < t.1.card } ≃
    { t : ℕ × ℕ // t.1 < P.parts.card ∧ t.1 + P.parts.card * t.2 < s.card } where
  toFun t := by
    obtain ⟨⟨p, q⟩, ⟨m, l⟩⟩ := t
    exact ⟨⟨(hP.partsEquiv ⟨p, m⟩).1, q⟩, sorry⟩
  invFun t := by
    obtain ⟨⟨r, q⟩, ⟨l, b⟩⟩ := t
    exact ⟨⟨hP.partsEquiv.symm ⟨r, sorry⟩, q⟩, sorry⟩
  left_inv t := by
    obtain ⟨⟨p, q⟩, ⟨m, l⟩⟩ := t
    simp only [Subtype.coe_eta, Equiv.symm_apply_apply]
    -- And.rec (fun left right ↦ { val := (p, q), property := _ }) _ = { val := (p, q), property := _ }
    with_unfolding_all exact rfl -- works
  right_inv t := by
    obtain ⟨⟨r, q⟩, ⟨l, b⟩⟩ := t
    simp only [Subtype.coe_eta, Equiv.apply_symm_apply]
    -- And.rec (fun left right ↦ { val := (r, q), property := _ }) _ = { val := (r, q), property := _ }
    with_unfolding_all exact rfl -- DOESN'T WORK

Why does the last line in left_inv work but not the last line in right_inv, and how can I prove right_inv?