apply_ite

Stream: general

[Scott Morrison]

-- How is this not in mathlib?!
lemma apply_ite {α β : Type*} (f : α → β) (P : Prop) [decidable P] (x y : α) :
  f (ite P x y) = ite P (f x) (f y) :=
by split_ifs; refl

Is this already somewhere in mathlib? If not, can I put it in logic/basic.lean?

[Scott Morrison]

Surely there is some existing colloquial way to push a function inside an if...?

[Johan Commelin]

Sounds like a good idea!

[Patrick Stevens]

Naive naming question: is this really "apply"? In the "applicative functor" sense, "apply" has the signature F (A -> B) -> F A -> F B, which is the first thing I think of. My guess would have been something like "interchange".

[Kenny Lau]

in mathlib apply means applying a function to an input

[Floris van Doorn]

We probably also wants its friend:

lemma ite_apply {α} {β : α → Type*} (P : Prop) [decidable P] (f g : Π x, β x) (x : α) :
  (ite P f g) x = ite P (f x) (g x) :=
by split_ifs; refl

[Scott Morrison]

all in mathlib now, part of #3177

[Simon Hudon]

I don't think it will behave well with simp and rw because the outer function on the lhs is a variable

[Scott Morrison]

Yes. To use it you need to write simp [ite_apply _ f], etc. Maybe I should add a doc-string to that effect.

[Simon Hudon]

Could it be worth having a specialized version of rw to make it more usable?

[Scott Morrison]

Sounds interesting!

[Simon Hudon]

I'd start it with generalize h : ite _ _ _ = x

[Scott Morrison]

Could we possibly do something much more general? That is not ite specific in any way, but just tries to do rewriting even without being able to key on the head symbol (because it could be a metavariable).