Zulip Chat Archive

Stream: new members

Topic: involution and ite


view this post on Zulip Yakov Pechersky (Sep 08 2020 at 20:29):

What would be the most mathlib-friendly way to state this? Is this too specific? What file would it go in?

import logic.function.basic

lemma inv_ite {α : Type*} (P : Prop) [decidable P] {f : α  α} (hinv : function.involutive f) (x : α) :
  ite P x (f x) = f (ite (¬ P) x (f x)) :=
begin
  rw apply_ite f,
  by_cases h : P,
  { rw [if_pos h, if_neg (not_not.mpr h), hinv x] },
  { rw [if_pos h, if_neg h] },
end

view this post on Zulip Alex J. Best (Sep 08 2020 at 20:41):

adding a lemma ite_neg seems useful:

lemma ite_neg {c : Prop} {X : Type*} (a b : X) [decidable c] : ite (¬ c) a b = ite c b a :=
by split_ifs; refl

lemma inv_ite {α : Type*} (P : Prop) [decidable P] {f : α  α} (hinv : function.involutive f) (x : α) :
  ite P x (f x) = f (ite (¬ P) x (f x)) :=
by rw [apply_ite f, hinv, ite_neg]

view this post on Zulip Kenny Lau (Sep 08 2020 at 20:50):

always generalize

view this post on Zulip Yakov Pechersky (Sep 08 2020 at 20:54):

So, PR this?

lemma ite_neg {c : Prop} {X : Type*} (a b : X) [decidable c] : ite (¬ c) a b = ite c b a :=
by split_ifs; refl

lemma inv_ite {α : Type*} (P : Prop) [decidable P] {f : α  α} (hinv : function.involutive f) (x : α) :
  f (ite P x (f x)) = ite (¬ P) x (f x) :=
by rw [apply_ite f, hinv, ite_neg]

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 21:42):

Sure!

view this post on Zulip Yakov Pechersky (Sep 08 2020 at 22:11):

#4074


Last updated: May 13 2021 at 22:15 UTC