Getting unification info from lean

Stream: new members

[Chris B]

If I try to define nat.succ_add as it is in core for some arbitrary type with the same shape as nat (or using anything with the congr_arg succ _ pattern), Lean isn't able to unify the successor case as it is with nat. Is there any way to get Lean to say what it's using behind the scenes to solve the unification problem? None of the definitions in core or init that are tagged with attributes jumped out as an obvious culprit.

[Floris van Doorn]

I think this attribute is the culprit: https://github.com/leanprover-community/lean/blob/master/library/init/core.lean#L417

[Floris van Doorn]

This works for me:

inductive mynat
| zero : mynat
| succ (n : mynat) : mynat

namespace mynat

protected def add : mynat → mynat → mynat
| a zero     := a
| a (succ b) := succ (add a b)

instance : has_zero mynat := ⟨mynat.zero⟩
instance : has_one mynat := ⟨mynat.succ mynat.zero⟩
instance : has_add mynat := ⟨mynat.add⟩

attribute [pattern] mynat.add mynat.add._main

lemma succ_add : ∀ n m : mynat, (succ n) + m = succ (n + m)
| n 0     := rfl
| n (m+1) := congr_arg succ (succ_add n m)

end mynat

[Floris van Doorn]

Oh, actually, when I remove the [pattern] attribute this example still works...

[Chris B]

Thank you, you're a hundred percent right and I am every bad adjective in the book.I made a completely stupid mistake and defined add as add ((succ a) b) and proceeded to totally ignore it while putting everything else under the microscope. My apologies.

[Floris van Doorn]

No problem! If you make a mistake it is very hard to figure out where exactly the mistake is.