## Stream: general

### Topic: I don't understand rfl

#### Kenny Lau (Jul 10 2020 at 04:54):

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 (Jul 10 2020 at 05:05):

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

#### Kenny Lau (Jul 10 2020 at 05:16):

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

#### Kenny Lau (Jul 10 2020 at 05:16):

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

#### Scott Morrison (Jul 10 2020 at 05:25):

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 (Jul 10 2020 at 10:46):

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

#### Gabriel Ebner (Jul 10 2020 at 10:55):

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.

Last updated: Dec 20 2023 at 11:08 UTC