Why isn't this inductive function defeq to its value?

Stream: mathlib4

[Daniel Weber]

I'm trying to update #12750, and I encountered something quite strange. In this code:

def grayCodeInv : Nat → Nat
  | 0 => 0
  | n+1 => grayCodeInv (n / 2)
  decreasing_by sorry

example : grayCodeInv 0 = 0 := rfl -- doesn't work

example : grayCodeInv 0 = 0 := by rfl -- works

example : grayCodeInv 0 = 0 := show_term by rfl -- Eq.refl (grayCodeInv 0)

example : grayCodeInv 0 = 0 := Eq.refl (grayCodeInv 0) -- doesn't work

What's going on?

[Daniel Weber]

I see it's not mathlib related, could someone move it to #lean4 ?

[Edward van de Meent]

it might be something to do with inductive definitions typically being irreducable?

[Daniel Weber]

Does tactic mode affect the reducibility settings?

[Daniel Weber]

No, but even example : grayCodeInv 0 = 0 := by exact Eq.refl (grayCodeInv 0) doesn't work.

[Jannis Limperg]

Functions defined by well-founded recursion (the decreasing_by) have recently become irreducible by default. You can use @[semireducible] def grayCodeInv ... to make this one reducible again, or you can use unseal to locally make it reducible. The fact that by rfl works is apparently a bug.

[Daniel Weber]

What is considered better style?

[Jannis Limperg]

Don't know whether there is a Mathlib convention. My personal take is that this irreducibility business is a performance optimisation, so if the performance is good enough, I see no reason not to go for @[semireducible].

[Kevin Buzzard]

I thought we were supposed to be doing

example : grayCodeInv 0 = 0 := by simp [grayCodeInv]

[Kevin Buzzard]

Jannis Limperg said:

The fact that by rfl works is apparently a bug.

I wonder how many of the 287 occurrences of by rfl in mathlib will break when this bug is fixed...

[Jannis Limperg]

Kevin Buzzard said:

I thought we were supposed to be doing

example : grayCodeInv 0 = 0 := by simp [grayCodeInv]

Right, that's definitely more idiomatic. Sorry.