dite of function application

Stream: new members

[Eric Wieser]

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]

  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]

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]

plus, your dite isn't actually dependent

[Eric Wieser]

How about this then:

  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]

probably it's easier to use in the other direction

[Kevin Buzzard]

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

[Mario Carneiro]

not a congr lemma

[Mario Carneiro]

apply_dif might be an appropriate name?

[Eric Wieser]

You're right that split_ifs solved my problem too

[Kenny Lau]

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]

I think I just added this lemma ...

[Scott Morrison]

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

[Scott Morrison]

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

[Eric Wieser]

What's the new lemma called?

[Scott Morrison]

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