involution and ite

Stream: new members

[Yakov Pechersky]

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

[Alex J. Best]

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]

[Kenny Lau]

always generalize

[Yakov Pechersky]

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]

[Kevin Buzzard]

Sure!

[Yakov Pechersky]

#4074