Zulip Chat Archive

Stream: general

Topic: I don't understand rfl


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Jul 10 2020 at 05:16):

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

view this post on Zulip Kenny Lau (Jul 10 2020 at 05:16):

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

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Jul 10 2020 at 10:46):

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

view this post on Zulip 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: May 06 2021 at 21:09 UTC