Zulip Chat Archive

Stream: general

Topic: recursor_of "list" is none


Cyril Cohen (Jul 23 2019 at 12:38):

Dear all, could someone tell me why the result of

run_cmd do env  get_env, let r := env.recursor_of "list", trace r

is none?

Chris Hughes (Jul 23 2019 at 12:48):

#eval do env  get_env, let r := env.recursor_of `list.rec, trace r --(some list)

Looks like it returns a type given a recursor.

Kenny Lau (Jul 23 2019 at 12:59):

from my experiments it looks like that if it returns none, then the recursor is X.rec

Chris Hughes (Jul 23 2019 at 13:05):

Is there an inductive type whose recursor is not X.rec?

Kenny Lau (Jul 23 2019 at 13:08):

I don't think so

Wojciech Nawrocki (Jul 23 2019 at 13:17):

C++ doc says: "If n is the name of an elimination rule in env, then return the name of the inductive datatype D
s.t. n is an elimination rule of D. Otherwise, return none."

Cyril Cohen (Jul 24 2019 at 08:15):

C++ doc says: "If n is the name of an elimination rule in env, then return the name of the inductive datatype D
s.t. n is an elimination rule of D. Otherwise, return none."

Thanks! Looks like the lean doc is wrong (Return the recursor of the given inductive datatype). Where can I find the C++ doc?

Cyril Cohen (Jul 24 2019 at 08:19):

Is there an inductive type whose recursor is not X.rec?

Since recursor_of did not work, I am indeed using X.rec, but name-based meta-programming is not a very good practice in my experience.

Mario Carneiro (Jul 24 2019 at 08:51):

It's not always rec :/

Mario Carneiro (Jul 24 2019 at 08:52):

Sometimes it's drec

Mario Carneiro (Jul 24 2019 at 08:52):

Or rather, I think X.rec always exists but it may not be primitive

Mario Carneiro (Jul 24 2019 at 08:56):

I don't see any docs, but from https://github.com/leanprover-community/lean/blob/master/src/library/vm/vm_environment.cpp#L183-L188 it looks like Wojciech's description is correct

Mario Carneiro (Jul 24 2019 at 09:01):

Looks like the code actually does that "name based meta-programming" https://github.com/leanprover-community/lean/blob/master/src/kernel/inductive/inductive.cpp#L183-L186

Cyril Cohen (Jul 24 2019 at 09:03):

Or rather, I think X.rec always exists but it may not be primitive

Oww,... I'd say it's always a primitive but not always the most general one (e.g. eq.rec is primitive but not as general as eq.drec). What is the general rule about rec vs drec?

Cyril Cohen (Jul 24 2019 at 09:05):

I am wrong it looks like eq.drec is actually programmed using eq.rec... so I did not yet find a case where drec is primitive and rec isn't...

Mario Carneiro (Jul 24 2019 at 09:13):

I got it confused. rec is always primitive, but it is dependent only if it doesn't eliminate to Prop. If it does eliminate to Prop then drec is the dependent one

Cyril Cohen (Jul 24 2019 at 09:18):

I got it confused. rec is always primitive, but it is dependent only if it doesn't eliminate to Prop. If it does eliminate to Prop then drec is the dependent one

ok.... could you tell me the rationale?

Mario Carneiro (Jul 24 2019 at 09:20):

No, this is me griping

Cyril Cohen (Jul 24 2019 at 09:20):

I got it confused. rec is always primitive, but it is dependent only if it doesn't eliminate to Prop. If it does eliminate to Prop then drec is the dependent one

I'm not sure I understood the rule... do you mean if it admits strong elimination? (i.e. elimination to Type of an inductive in Prop ?)

Mario Carneiro (Jul 24 2019 at 09:21):

Ah, actually it's not strong elimination that is the deciding factor, it is whether the inductive itself is a prop

Mario Carneiro (Jul 24 2019 at 09:21):

for example or and eq both have a drec

Mario Carneiro (Jul 24 2019 at 09:21):

but nat doesn't

Cyril Cohen (Jul 24 2019 at 09:22):

ok, is it using proof irrelevance for prop to derive drec from rec? (because otherwise I do not see how it is possible)

Mario Carneiro (Jul 24 2019 at 09:22):

yes

Mario Carneiro (Jul 24 2019 at 09:23):

If I were king of lean I would make the dependent version always be called rec and always be primitive

Cyril Cohen (Jul 24 2019 at 09:23):

yes

ok, this will not make my life easy ^^'

Mario Carneiro (Jul 24 2019 at 09:23):

The fact that you can derive it from the non-dependent version is a cute fact but not worth breaking the pattern

Cyril Cohen (Jul 24 2019 at 09:23):

If I were king of lean I would make the dependent version always be called rec and always be primitive

Now you make me wish you were the king of lean

Cyril Cohen (Jul 24 2019 at 09:25):

Writing parametricity translation of inductive families is already difficult without having to take into account discrepancies in the patterns of primitives... :'(

Sebastian Ullrich (Jul 24 2019 at 10:34):

If I were king of lean I would make the dependent version always be called rec and always be primitive

Like this? https://github.com/leanprover/lean4/commit/a7d08d2f3dd608a70d41c92ca5559c2528e21ee5


Last updated: Dec 20 2023 at 11:08 UTC