Zulip Chat Archive

Stream: new members

Topic: dite of function application


view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 02 2020 at 11:03):

plus, your dite isn't actually dependent

view this post on Zulip Eric Wieser (Jul 02 2020 at 11:03):

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

view this post on Zulip Mario Carneiro (Jul 02 2020 at 11:03):

probably it's easier to use in the other direction

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 02 2020 at 11:04):

not a congr lemma

view this post on Zulip Mario Carneiro (Jul 02 2020 at 11:05):

apply_dif might be an appropriate name?

view this post on Zulip Eric Wieser (Jul 02 2020 at 11:05):

You're right that split_ifs solved my problem too

view this post on Zulip 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

view this post on Zulip Scott Morrison (Jul 02 2020 at 12:44):

I think I just added this lemma ...

view this post on Zulip Scott Morrison (Jul 02 2020 at 13:43):

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

view this post on Zulip Scott Morrison (Jul 02 2020 at 13:44):

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

view this post on Zulip Eric Wieser (Jul 02 2020 at 13:58):

What's the new lemma called?

view this post on Zulip 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