Option matches as eliminators

fun_prop cannot see through a match: its auxiliary matcher is a constant of the defining function, and it does not reduce on a stuck discriminant. Rules are therefore stated for Option.elim. The tactic option_match_to_elim rewrites every non-dependent two-way match on an option in the goal, under binders and nested, to Option.elim, so that a definition written with match needs no separate statement in terms of tests and defaults.

Option.map and Option.any unfold to such a match, so unfold Option.map reaches them. Option.bind unfolds to a match on two discriminants, so the tactic rewrites Option.bind itself. An alternative that takes a pattern apart, such as some (a, b), is left unchanged, since Option.elim has a single argument.

def Cslib.Tactic.optionMatchToElim : Lean.ParserDescr

Rewrite every Option.bind and non-dependent two-way match on an option in the goal to Option.elim.