recursor_of "list" is none

Stream: general

[Cyril Cohen]

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]

#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]

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

[Chris Hughes]

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

[Kenny Lau]

I don't think so

[Wojciech Nawrocki]

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]

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]

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]

It's not always rec :/

[Mario Carneiro]

Sometimes it's drec

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

No, this is me griping

[Cyril Cohen]

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]

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

[Mario Carneiro]

for example or and eq both have a drec

[Mario Carneiro]

but nat doesn't

[Cyril Cohen]

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]

yes

[Mario Carneiro]

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

[Cyril Cohen]

yes

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

[Mario Carneiro]

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

[Cyril Cohen]

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]

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

[Sebastian Ullrich]

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