Difference of Finset.induction and Finset. induction_on

Stream: new members

[Michael Rothgang]

Reading the API docs, docs#Finset.induction and docs#Finset.induction_on look exactly the same, except for a different order of arguments. Is there a point in having both versions? The latter has a Finset as argument first, so enables dot notation; this makes sense. What is the purpose of the former version?

(This same question also exists for Finset.cons_induction{_on}, and probably in more places.)

[Michael Rothgang]

Looking at the source, I see that the latter is indeed defined in terms of the former.

Okay: why do we have both? Can somebody explain Chesterton's fence to me?

[Kevin Buzzard]

docs#Nat.rec docs#Nat.rec_on they're everywhere :-)(I didn't expect Nat.rec not to exist!) Yeah, this is a standard idiom for induction hypotheses; one is useful if you already have the s you want to prove P s for at hand, and the other is useful if you don't. e.g. docs#PNat.recOn eats the positive natural first

[Eric Wieser]

Nat.rec does exist, just not in the docs

[Floris van Doorn]

I'm not sure if both are needed in the current day and age. If you only use induction principles using the induction ... using ... tactic, then it doesn't matter which you use.
The *.induction version is the usual way recursors are written in type theory papers. They also sometimes have nice properties. E.g. Sigma.rec is an equivalence (the backwards direction on docs#Equiv.piCurry).
*.induction_on is sometimes useful when applying induction principles. In term mode, you might first want to specify the induction variable, and only then the induction steps. In Lean 2 you could write apply Nat.rec_on n and Lean would figure out the motive (I don't think that generally works anymore).

[Mario Carneiro]

I think it does work, that's what elab_as_elim is for

[Mario Carneiro]

oh no it doesn't work, at least not with apply. You can use refine though if you pass enough ?_

[Eric Wieser]

Of course if you pass enough ?_, the order doesn't matter anyway