I don't understand rfl

Stream: general

[Kenny Lau]

import data.nat.digits

theorem test (b n : ℕ) : digits (b+2) (n+1) = (n+1)%(b+2) :: digits (b+2) ((n+1)/(b+2)) := rfl -- works
theorem test' : digits (0+2) (1+1) = (1+1)%(0+2) :: digits (0+2) ((1+1)/(0+2)) := rfl          -- fails

[Chris Hughes]

There's an acc.rec in the definition of digits_aux which is the main source of funny things like this.

[Kenny Lau]

and what's wrong with acc.rec? isn't everything computable?

[Kenny Lau]

meta-theorem: if it's computable and everything is explicit then it can be unfolded

[Scott Morrison]

I would love to understand this, too. I know in my work on combinatorial games, nothing was every "actually" computable if I used well-founded recursion, and I always had to rewrite everything in terms recursion over nat before proofs by rfl or dec_trivial would start working.

[Chris Hughes]

I fixed it here by writing an axiom free well foundedness proof.

[Gabriel Ebner]

The best move is to avoid definitional reduction of acc.rec. It is one of the few places in Lean where the actual proof term matters. Namely the acc.rec application is reduced as many times as there are acc.intro in the well-foundedness proof. This is also one of the earliest known failures of transitivity of definitional equality in Lean.