Zulip Chat Archive

Stream: new members

Topic: Getting unification info from lean


view this post on Zulip Chris B (Jul 31 2019 at 23:15):

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.

view this post on Zulip Floris van Doorn (Jul 31 2019 at 23:21):

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

view this post on Zulip Floris van Doorn (Jul 31 2019 at 23:21):

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

view this post on Zulip Floris van Doorn (Jul 31 2019 at 23:24):

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

view this post on Zulip Chris B (Jul 31 2019 at 23:57):

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.

view this post on Zulip Floris van Doorn (Aug 01 2019 at 00:38):

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


Last updated: May 12 2021 at 04:19 UTC