naming arguments to recursors

Stream: mathlib4

[Aaron Liu]

In #mathlib4 > Induction argument order @ 💬 it was decided that the "motive" argument should be called motive. But what about the other arguments? What should they be called?

Here's a random sample of some declarations that I would consider to be "recursors":

• docs#mabs_by_cases
• docs#Polynomial.induction_with_natDegree_le
• docs#CategoryTheory.Paths.induction_fixed_target
• docs#Nat.recOnMul
• docs#RingTheory.Sequence.IsWeaklyRegular.ndrecIterModByRegular
• docs#Function.Iterate.rec
• docs#Surreal.lift

[Eric Wieser]

I think the rough guideline is "pretend this was the recursor generated by an inductive type, and so name the arguments in the recursor as you would the constructors in the inductive type"

[Edward van de Meent]

the names you choose matter: they get used for naming new goals, and they are also the labels for with branches to cases and induction

[Edward van de Meent]

So that's something to keep in mind

[Aaron Liu]

Eric Wieser said:

I think the rough guideline is "pretend this was the recursor generated by an inductive type, and so name the arguments in the recursor as you would the constructors in the inductive type"

What do this mean for docs#Surreal.lift, which is a "quotient recursor"?

[Edward van de Meent]

ah, but that's not really a recursor

[Edward van de Meent]

in the sense that there is no motive

[Edward van de Meent]

or at least, it seems to me like there isn't any?

[Eric Wieser]

Yeah, that's more (half of) a universal property than a recursor

[Aaron Liu]

Edward van de Meent said:

in the sense that there is no motive

I analyzed this as a non-dependent recursor in which the motive {α : Sort*} is not allowed to depend on the major premise (_ : Surreal)

[Aaron Liu]

Eric Wieser said:

Yeah, that's more (half of) a universal property than a recursor

That's what a recursor is, right? It's (half of) a universal property

[Aaron Liu]

Anyways, even if you don't think Surreal.lift counts as a recursor, there are plenty more that follow this pattern. What about docs#Multiset.rec, then? Surely that's a recursor.

[Chris Bailey]

I think using "major" and some variation of "minor<constructor>" would make sense when applicable. The minor premises are usually anonymous in the type, but last I checked the iota rules just use the constructor name which is a little bit of a hit to readability (even though they're sort of hidden).

[Aaron Liu]

Chris Bailey said:

I think using "major" and some variation of "minor<constructor>" would make sense when applicable. The minor premises are usually anonymous in the type, but last I checked the iota rules just use the constructor name which is a little bit of a hit to readability (even though they're sort of hidden).

When you do induction x using Foo.rec with, the alternatives are named according to the minor premises.

[Aaron Liu]

Here's an example of this pattern, which is why they need to have names that make sense.

[Aaron Liu]

Also, sometimes there can be more than one major premise, for example in docs#Nat.recDiag both m and n are major premises.

[Aaron Liu]

Chris Bailey said:

I think using "major" and some variation of "minor<constructor>" would make sense when applicable.

This also doesn't answer what I should name the C_cons_heq argument of docs#Multiset.rec.

[Eric Wieser]

C_0 and C_cons should be called zero and cons

[Eric Wieser]

C_cons_heq I guess is emulating a quotient-inductive type, so maybe sound (referring to docs#Quotient.sound) or cons_sound is appropriate?

[Aaron Liu]

Sure! This seems like the correct naming if I'm thinking of Multiset as a higher inductive type. What other quotient-inductive recursors, like docs#Quotient.hrecOn₂? Should φ be replaced with motive, f be replaced with mk, and c be replaced with sound?

[Aaron Liu]

Also, what should the major premises be named?

[Aaron Liu]

Eric Wieser said:

C_cons_heq I guess is emulating a quotient-inductive type, so maybe sound (referring to docs#Quotient.sound) or cons_sound is appropriate?

The theorem is called docs#Multiset.cons_swap, so maybe cons_swap?

[Robin Arnez]

In my opinion you really only need to care about the minor premises and the motive specifically (naming them like constructors and well, motive). For major premises just use whatever name is typical for the type or whatever or just go with a single letter (recursors for inductive types use the name t by default iirc). Side conditions, such as the C_cons_heq can just be called as if they were just regular proofs, e.g. h is probably fine. Regarding Quotient.hrecOn and variants: using the names motive and mk would probably be better here, c can be h or whatever (although I may note that this function is not really usable with induction / cases so it's less relevant to change things).