Zulip Chat Archive

Stream: general

Topic: invalid occurence of recursive args


view this post on Zulip Zesen Qian (Jun 20 2018 at 20:21):

Not sure if it's a place for routine trouble shooting, but I'm trying to do some theory inside lean, I defined a inductive family but lean is not happy with it. https://ptpb.pw/3O0a
The error is at the constructor satlem, "invalid occurence of recursive arg#5, the body of the functional type depends on it".

view this post on Zulip Mario Carneiro (Jun 20 2018 at 20:30):

I don't think lean likes that you have placed the recursive argument before the variable v

view this post on Zulip Mario Carneiro (Jun 20 2018 at 20:33):

you had:

| satlem (c : context) (cl cl' : clause) :
  proof c (type.holds cl) →
  ∀ v : string, proof ((v, type.holds cl) :: c) (type.holds cl') →
  proof c (type.holds cl')

This works:

| satlem (c : context) (cl cl' : clause) :
  ∀ v : string, proof c (type.holds cl) →
  proof ((v, type.holds cl) :: c) (type.holds cl') →
  proof c (type.holds cl')

Or maybe you got the parentheses wrong? This works too, but means something different:

| satlem (c : context) (cl cl' : clause) :
  proof c (type.holds cl) →
  (∀ v : string, proof ((v, type.holds cl) :: c) (type.holds cl')) →
  proof c (type.holds cl')

view this post on Zulip Zesen Qian (Jun 20 2018 at 20:50):

Thanks! this works. I also fixed similar issues in the code.
question tho: why is this required? intuitively I don't see how it's invalid.

view this post on Zulip Mario Carneiro (Jun 20 2018 at 20:57):

There was a restriction along the lines that recursive arguments must come after non-recursive args, mostly for convenience of implementation, but last I checked that restriction had been lifted, so I'm not sure why you are getting the error still

view this post on Zulip Zesen Qian (Jun 20 2018 at 21:03):

maybe because it's inductive family, so impl. could be harder.

view this post on Zulip Gabriel Ebner (Jun 21 2018 at 07:11):

There is still a restriction on dependent arguments, none of the arguments after the first recursive argument may occur in other arguments. In this case v comes after the first recursive argument and occurs in the second recursive argument.


Last updated: May 08 2021 at 10:12 UTC