Floating matches/ifs out of function applications

Stream: Is there code for X?

[Joachim Breitner]

Idle weekend thought, without much behind, but I just wondered if we have a tactic, or should have a tactic, that floats eliminators (match, if…) to the top, duplicating the context into each alternative, e.g.

|- foo (if x then a else b) = if x then foo a else foo b

(where foo could be a more complex context, and if could be a matcher).

I guess this could even be a simpproc. I think I ran into proofs where this would allow me to solve a goal with just simplification, no need for split.

Of course it can only float it out as far as the condition (or the scrutinee of a matcher) ’s local variables allow.

(There is some similarity to Isabelle’s _splitter_ feature in the Simplifier, only that it's simpler and nicer in our case because we can put propositions into the branches.)

[Vincent Beffara]

docs#apply_ite ?

[Joachim Breitner]

Right, that’s the lemma that one could use when doing this to ite, but for arbitrary match expressions, you’d have to generate that on the fly, and I am not sure how well just using this as a simp lemma would work, with the higher-order f pattern variable.

[Yaël Dillies]

Yes it would be great to have that because apply_ite/apply_dite is really hard to use without passing the motive explicitly

[Joachim Breitner]

So you have encountered the need for that transformation before?

[Yaël Dillies]

A handful of times, yes.

[Kyle Miller]

At least for ifs, it might be good to think about this as if normalization (like in this challenge), with the floating step corresponding to turning a more functional programming style into a procedural one.

[Joachim Breitner]

For anyone finding this old thread: This is now taking shape at lean4#5923