## Stream: new members

### Topic: dite of function application

#### Eric Wieser (Jul 02 2020 at 10:51):

Is there a builtin proof that function application is commutative withdite?

example (A : Type) (B : Type) (f : A → B) (a1 a2 : A) (h : Prop) [decidable h] :
dite h (λ h, f a1) (λ h, f a2) = f (dite h (λ h, a1) (λ h, a2))
:= begin
library_search,
end


finds nothing

#### Eric Wieser (Jul 02 2020 at 11:00):

  example (A : Type) (B : Type) (f : A → B) (a1 a2 : A) (h : Prop) [decidable h] :
dite h (λ h, f a1) (λ h, f a2) = f (dite h (λ h, a1) (λ h, a2)) := begin
cases decidable.em h,
repeat {rw dif_pos h_1},
repeat {rw dif_neg h_1},
end


seems to do the trick. Should this be called dif_comm or somthing?

#### Mario Carneiro (Jul 02 2020 at 11:02):

example (A : Type) (B : Type) (f : A → B) (a1 a2 : A) (h : Prop) [decidable h] :
dite h (λ h, f a1) (λ h, f a2) = f (dite h (λ h, a1) (λ h, a2)) :=
by split_ifs; simp


I think a lemma like this can't really be used more easily than the general tactics

#### Mario Carneiro (Jul 02 2020 at 11:03):

plus, your dite isn't actually dependent

#### Eric Wieser (Jul 02 2020 at 11:03):

  lemma dif_apply {A : Type} {B : Type} (f : A → B) {h : Prop} {a1 : h -> A} {a2 : ¬h -> A} [decidable h] :
dite h (λ h, f (a1 h)) (λ h, f (a2 h)) = f (dite h a1 a2) := begin
cases decidable.em h,
repeat {rw dif_pos h_1},
repeat {rw dif_neg h_1},
end


#### Mario Carneiro (Jul 02 2020 at 11:03):

probably it's easier to use in the other direction

#### Kevin Buzzard (Jul 02 2020 at 11:04):

@Mario Carneiro what is this lemma called? Is it a congr lemma? I never understood congr properly

#### Mario Carneiro (Jul 02 2020 at 11:04):

not a congr lemma

#### Mario Carneiro (Jul 02 2020 at 11:05):

apply_dif might be an appropriate name?

#### Eric Wieser (Jul 02 2020 at 11:05):

You're right that split_ifs solved my problem too

#### Kenny Lau (Jul 02 2020 at 11:06):

Kevin Buzzard said:

Mario Carneiro what is this lemma called? Is it a congr lemma? I never understood congr properly

this is an apply lemma right

#### Scott Morrison (Jul 02 2020 at 12:44):

I think I just added this lemma ...

#### Scott Morrison (Jul 02 2020 at 13:43):

They are in logic/basic.lean, at the bottom.

#### Scott Morrison (Jul 02 2020 at 13:44):

and library_search finds them for me... :-) a reminder to obsessively upgrade mathlib, I guess!

#### Eric Wieser (Jul 02 2020 at 13:58):

What's the new lemma called?

#### Scott Morrison (Jul 02 2020 at 14:45):

lemma apply_dite {α β : Type*} (f : α → β) (P : Prop) [decidable P] (x : P → α) (y : ¬P → α) :
f (dite P x y) = dite P (λ h, f (x h)) (λ h, f (y h)) :=
by { by_cases h : P; simp [h], }

lemma apply_ite {α β : Type*} (f : α → β) (P : Prop) [decidable P] (x y : α) :
f (ite P x y) = ite P (f x) (f y) :=
apply_dite f P (λ _, x) (λ _, y)

lemma dite_apply {α : Type*} {β : α → Type*} (P : Prop) [decidable P]
(f : P → Π a, β a) (g : ¬ P → Π a, β a) (x : α) :
(dite P f g) x = dite P (λ h, f h x) (λ h, g h x) :=
by { by_cases h : P; simp [h], }

lemma ite_apply {α : Type*} {β : α → Type*} (P : Prop) [decidable P]
(f g : Π a, β a) (x : α) :
(ite P f g) x = ite P (f x) (g x) :=
dite_apply P (λ _, f) (λ _, g) x


Last updated: May 13 2021 at 22:15 UTC