option.elim

Stream: general

[Yaël Dillies]

Should the arguments of docs#option.elim be swapped so that it behaves like docs#sum.elim? Mario in number_theory.dioph defined docs#option.cons, which is just option.elim with the arguments swapped.

[Eric Wieser]

What side do docs#and.elim and docs#or.elim fall on?

[Yaël Dillies]

Seem like they agree with option

[Eric Wieser]

docs#iff.elim goes the other way though

[Eric Wieser]

As does docs#nat.elim

[Eric Wieser]

My feeling is that the option.cons order is the right one, and the rule should be "elim is just non-dependent rec"

[Eric Wieser]

As opposed to the current meaning "as decided by a possibly biased coin toss, elim is the non-dependent version of either rec or rec_on"

[Eric Wieser]

What does lean 4 do?

[Mario Carneiro]

Eric Wieser said:

What does lean 4 do?

Same as lean 3: it's not autogenerated so when it is created manually it's a coin toss what you get

[Eric Wieser]

Does lean 4 still generate both rec and rec_on?

[Mario Carneiro]

yes, although they are a lot less useful since they aren't @[elab_as_elminator]

[Mario Carneiro]

you can't really use them directly anymore

[Eric Wieser]

Why even bother having both then?

[Kyle Miller]

Idle question: how feasible is it to have some syntax where you can do eliminator foo.rec a b c and have elaborate like elab_as_eliminator? (Maybe it could be like an expression version of the induction tactic?)

[Kyle Miller]

@Eric Wieser They seemed to be used at least by the induction tactic. (edit: oh, why both)

[Eric Wieser]

I'm surprised rec alone isn't enough and that rec_on is worth leaving around

[Eric Wieser]

Maybe there's a mutual case where only one exists, like in lean 3

[Yaël Dillies]

#13403 for moving option.cons. I didn't make the notation global.

[Mario Carneiro]

Yeah, I would be on board with a term mode syntax for @[elab_as_eliminator]. That can be implemented in user space too

[Yaël Dillies]

#14681