Induction argument order

Stream: mathlib4

[Violeta Hernández]

Do we have some sort of convention for the argument order in induction principles?

[Violeta Hernández]

I notice in some induction principles proving P a, the argument a is at the end of the argument list, like in docs#Nat.recOnMul, while in others like docs#Ordinal.induction it goes at the beginning, before any of the hypotheses.

[Violeta Hernández]

Is either form preferred?

[Yaël Dillies]

The rule is that if you have On in the name, then a is at the start, else it's at the end. Looks like both your examples are going against that rule...

[Edward van de Meent]

Is this a rule (i.e. explicitly stated somewhere) or merely unspoken convention?

[Edward van de Meent]

If it is the latter, but should be the former, perhaps the place to write this down is the style guide?

[Yaël Dillies]

Probably #naming is the right place for such information

[Kyle Miller]

I'm not sure there's any hard-and-fast rule for induction, but On definitely signifies the major premise comes first. (A rule that major premises come last if there's no On makes sense to me though.)

[Edward van de Meent]

let me see if i can make a PR adding this to the naming guide...

[Edward van de Meent]

while i am writing this, would i be correct in saying that if the declaration is for Prop-typed motives, it should be called like induction (i.e. inductionOn rather than recOn)?

[Yaël Dillies]

and induction_on rather than inductionOn

[Edward van de Meent]

Quot.inductionOn
ZFSet.inductionOn
:face_with_peeking_eye:

[Edward van de Meent]

for now, i've made a preliminary PR. Please do suggest improvements to phrasing, i'm not quite sure about it yet. Also, i'd apreciate it if a maintainer could comment on this. (seeing the current state of mathlib, the proposed convention is not quite as commonplace as i expected it to be...)

[Edward van de Meent]

Edward van de Meent said:

(seeing the current state of mathlib, the proposed convention is not quite as commonplace as i expected it to be...)

as evidenced by searching the docs for .ind and inductionOn, as well as the earlier-mentioned counterexamples mentioned by Violeta...

[Kevin Buzzard]

Don't forget recOn ;-)

[Edward van de Meent]

recOn is an allowed name according to the naming convention though?

[Kevin Buzzard]

Sure! I just meant "make sure that you check that the order of the variables is OK in this case too :-)"

[Edward van de Meent]

My point was that they are both bad names: inductionOn is bad because the case suggests it can be Type-valued, which would mean it is rather a recursion principle, while ind is an unnecessary shortening of induction, decreasing readability.

[Yuyang Zhao]

I think the .rec .recOn rule comes from the names of automatically generated recursors of inductive types.

[Eric Wieser]

Do we have buy-in from core here? There seem to be Sort-valued recursors that use the Induction name.

#check Nat.div2Induction
#check Nat.strongInductionOn
#check Nat.strongRecOn -- identical to the above

[Eric Wieser]

cc @Kim Morrison, would a PR to rename / deprecate those names be accepted?

[Mario Carneiro]

IIRC there was a very similar case that was deprecated in lean 4, so I think the answer is yes

[Mario Carneiro]

lean4#5179 <- by "very similar" I mean "identical"

[Edward van de Meent]

there is another question from the discussion of this PR (which is about adding a naming convention for inductive/recursive principles) about what to name the "motive" argument, and it was rightly suggested by @Eric Wieser that this should be discussed on zulip. I argued that we should try to give these more understandable names, because an undergrad might not have heard of the term, which can make using an inductive or recursive principle daunting. As an alternative in the case of induction principles, i suggested calling the motive argument simply P for proposition. as such, are some polls:

[Edward van de Meent]

/poll What should Prop-eliminating motives be called
P
motive
decide on a case-by-case basis

[Edward van de Meent]

/poll What should Sort-eliminating motives be called
P
motive

[Edward van de Meent]

/poll What should Type-eliminating motives be called
P
motive

[Eric Wieser]

(for some history, in Lean 3 the nat.rec_on auto-generated recursors used C for the motive name)

[Mario Carneiro]

isn't the point of calling it motive instead of C exactly to "give it a more understandable name"?

[Eric Wieser]

Yes, I guess the question is whether "more understandable" applies to P too

[Edward van de Meent]

(and there are still some recursors with that as motive name, see for example WellFounded.induction)

[Mario Carneiro]

single letter names don't really convey anything

[Eric Wieser]

Eric Wieser said:

cc Kim Morrison, would a PR to rename / deprecate those names be accepted?

docs#Quot.inductionOn also has the Sort-capitalized name.

[Edward van de Meent]

Mario Carneiro said:

single letter names don't really convey anything

indeed, but they are less intimidating than [insert term you've never heard of] when looking at a function/lemma which should do something simple

[Mario Carneiro]

it is true that we don't have def Nat.sub (minuend subtrahend : Nat) : Nat

[Violeta Hernández]

It took me quite a while to understand what motive was doing, I initially thought it was some sort of reserved keyword.

[Violeta Hernández]

P and C are what I've most often come across with custom induction/recursion principles

[Edward van de Meent]

i suppose i'll call it now and note that there is a majority for using motive in all cases.

[Edward van de Meent]

the PR to the website adding this as naming convention has been merged, see here

[Edward van de Meent]

this may mean there is some tech debt to clean up

[Kyle Miller]

Why is it induction_on and not inductionOn? Wouldn't this be like insisting that in theorems we should see strict_mono rather than strictMono? To me, inductionOn is the name of the principle; the on isn't separate.

[Eric Wieser]

I think this is the congrArg vs congr_arg discussion again, which I don't remember if we resolved.

[Eric Wieser]

A weak argument in favor of _on is that it is a bit like _of

[Kyle Miller]

_on being like _of_nameOfThisType seems reasonable

[Kyle Miller]

I think that one's a bit different from congr though. I think congr_position makes sense in general as a naming convention, and it's just like the _left/_right naming convention. For function application, there just happen to be better names than Function.congr_left and Function.congr_right, namely referring to fun and arg. (We shouldn't expect core to change on this, but I do think congr_fun and congr_arg are more principled names.)

[Eric Wieser]

But also, this is me making up a justification for something that we inherited without thought from lean 3.

[Kyle Miller]

There's a big proviso with that _on justification, which is that specifically it's saying what the first explicit argument is, vs _of which doesn't have that restriction.

[Edward van de Meent]

according to the docs, terms of prop are in snake_case.

[Edward van de Meent]

and since inductionOn isn't a word...

[Edward van de Meent]

other than that, i'd like to point out that the added naming convention doesn't specify that it should be induction_on. it merely says that the name has to contain both induction and on when it eliminates only into prop and has the value argument before the constructions.

[Kyle Miller]

strictMono isn't a word either though, right?

[Edward van de Meent]

right

[Edward van de Meent]

in that case, it's the lowercase-ing of StrictMono, which produces a term of type Prop. However, there is no Prop (or Type) named InductionOn...

[Kyle Miller]

I'm just saying that "the docs say terms of prop are snake_case" doesn't imply inductionOn shouldn't be inductionOn

[Mario Carneiro]

My understanding of the rule here is what Edward says: strictMono is named that because there is actually a definition called StrictMono which is involved in the statement. If it was just about monotonicity as a general concept it would be spelled strict_mono in theorems

[Mario Carneiro]

(and yes, this is the congr_arg discussion again)

[Mario Carneiro]

which was never really resolved; core and mathlib simply have different conventions on this point