Option mess

Stream: general

[Yaël Dillies]

We have docs#Option.elim, docs#Option.elim', docs#Option.casesOn' which are all basically the same function. My understanding of the naming convention around recursors was that

• ∀ o : Option α, motive none → (∀ a : α, motive (some a)) → motive o is Option.rec (correct :check:)
• motive none → (∀ a : α, motive (some a)) → ∀ o : Option α, motive o is Option.recOn (correct :check:)
• Option α → β → (α → β) → β is Option.casesOn (wrong :cross_mark:, currently it's called Option.casesOn' and also Option.elim)
• β → (α → β) → Option α → β is Option.elim (wrong :cross_mark:, currently it's called Option.elim')

[Yaël Dillies]

.. the general pattern being that

• the suffix On indicates that the inductive type argument comes first
• rec indicates a dependent recursor
• elim/cases indicate a non-dependent recursor

[Yaël Dillies]

Is there any opposition to cleaning up the current mess? @Mario Carneiro, I will need your approval since docs#Option.elim is now in Std (but not the other two, somehow)

[Yaël Dillies]

Also, why is docs#Option.elim simp?

[Mario Carneiro]

As far as I know, T.elim has always been used conventionally for the non-dependent version of T.recOn. There is no T.elimOn

[Eric Wieser]

docs#Sum.elim and docs3#option.elim contradict that claim

[Eric Wieser]

docs#Option.elim matches docs#Sum.elim, so I think Option.elim' should probably go (which is a porting artefact)

[Mario Carneiro]

No I think your first claim was correct and existing functions are inconsistent:

• Option.elim is nondependent Option.recOn
• Option.elim' is nondependent Option.rec
• Sum.elim is nondependent Sum.rec

[Mario Carneiro]

Can someone do a census of all T.elim functions?

[Eric Wieser]

My claim is that Sum.elim is pretty heavily used as a definition for building vectors, where the argument order has to be this way around, and so must be the "right" one

[Eric Wieser]

Option.elim' is what option.elim got renamed to in the port

[Eric Wieser]

We discussed this all before

[Mario Carneiro]

The example with option.cons from that thread shows that similar reasoning also applies to Option

[Mario Carneiro]

I definitely agree that when you want to partially apply the function putting the major premise last is always the right answer

[Mario Carneiro]

and moreover that nondependent eliminators are particularly good for partial application

[Mario Carneiro]

the main reason to want the major premise to come first is when using it as a poor-man's match statement you want to specify the scrutinee before the branches

[Mario Carneiro]

You can avoid this issue when using dot-notation since in that case it doesn't matter, but if you want to specify the full name of the function or use @ then dot-notation is not available

[Mario Carneiro]

Using named arguments also allows you to manually reorder arguments (I do this so much for Array.foldl, I want the init argument first), but it means we should probably also be sure to name the major premise and name it consistently (currently neither Option.elim nor Sum.elim names the major premise)

[Mario Carneiro]

you also want to name the minor premises if you want it to be usable with induction/cases, although TBH I've never tried this with nondependent recursors and I'm not sure if it works

[Yaël Dillies]

I have now opened lean#5096