Stream: general

Topic: acc.rec

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


Mario Carneiro (Mar 19 2018 at 19:00):

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

Chris Hughes (Mar 19 2018 at 19:01):

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

Mario Carneiro (Mar 19 2018 at 19:02):

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

Chris Hughes (Mar 19 2018 at 19:08):

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

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

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!

Kevin Buzzard (Mar 19 2018 at 22:08):

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