acc.rec

Stream: general

[Chris Hughes]

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

[Mario Carneiro]

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

[Chris Hughes]

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

[Mario Carneiro]

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

[Chris Hughes]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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.