Zulip Chat Archive

Stream: general

Topic: acc.rec


view this post on Zulip Chris Hughes (Mar 19 2018 at 18:54):

I've been trying to prove things using acc.rec, and I'm finding it difficult to deal with. Of these three lemmas, only the first compiled. Definitional equality doesn't always seem to work. I'm particularly surprised that the third lemma doesn't reduce, given that the two terms differ only by a proof with the same type.

lemma acc.rec_1 {α : Sort u} {r : α  α  Prop} {C : α  Sort v}
(f : Π x, ( y, r y x  acc r y)  (Π y, r y x  C y)  C x) {a : α}
(b : α) (h :  y, r y b  acc r y) :
@acc.rec α r C f b (acc.intro b h) =
f b h (λ y hyb, @acc.rec α r C f y (h y hyb)) := rfl

lemma acc.rec_2 {α : Sort u} {r : α  α  Prop} {C : α  Sort v}
(f : Π x, ( y, r y x  acc r y)  (Π y, r y x  C y)  C x) {a : α}
(b : α) (h :  y, r y b  acc r y) (h₁ : acc r b) :
@acc.rec α r C f b h₁ =
f b h (λ y hyb, @acc.rec α r C f y (h y hyb)) := rfl

lemma acc.rec_3 {α : Sort u} {r : α  α  Prop} {C : α  Sort v}
(f : Π x, ( y, r y x  acc r y)  (Π y, r y x  C y)  C x) {a : α}
(b : α) (h :  y, r y b  acc r y) (h₁ : acc r b) :
@acc.rec α r C f b h₁ =
@acc.rec α r C f b (acc.intro b h) := rfl

view this post on Zulip Mario Carneiro (Mar 19 2018 at 19:00):

heh, I was just discussing how acc.rec is the root of all evil...

view this post on Zulip Chris Hughes (Mar 19 2018 at 19:01):

(show acc.intro b h = h₁, from rfl) ▸ rfl works for the second two proofs

view this post on Zulip Mario Carneiro (Mar 19 2018 at 19:02):

suffice it to say, yes this happens. Probably congr rfl rfl will also work

view this post on Zulip Chris Hughes (Mar 19 2018 at 19:08):

Might be worth putting this in docs, since it is very weird behaviour.

view this post on Zulip Kevin Buzzard (Mar 19 2018 at 22:07):

See end of section 3.7 in the reference manual: https://leanprover.github.io/reference/expressions.html#computation

view this post on Zulip Kevin Buzzard (Mar 19 2018 at 22:07):

There is a problem with definitional equality, in that there is provably no algorithm which checks to see that two things are definitionally equal!

view this post on Zulip Kevin Buzzard (Mar 19 2018 at 22:08):

Lean's algorithm is an algorithm :-) so it can't be doing definitional equality correctly.

view this post on Zulip Kevin Buzzard (Mar 19 2018 at 22:11):

See Mario's Masters thesis https://github.com/digama0/lean-type-theory/releases/download/v0.1/main.pdf for some more info -- section 3.1.


Last updated: May 10 2021 at 18:22 UTC