# Zulip Chat Archive

## 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