prop valued ifs

Stream: mathlib4

[Jakob von Raumer]

Shouldn't these be simpable?

example {p : Prop} [Decidable p] : (if p then True else False) = p := by aesop

example {p : Prop} [Decidable p] : (if p then False else True) = ¬ p := by aesop

[Jakob von Raumer]

The lhs is something where simp often gets stuck

[Jakob von Raumer]

bump

[Jakob von Raumer]

Guess I'll just add it as a simp lemma and see if anything breaks.

[Yaël Dillies]

Yeah I think those are reasonable simp lemmas

[Alex J. Best]

How about the more general

example {p q r : Prop} [Decidable p] : (if p then q else r) = ((p → q) ∧ (¬ p → r)) := by
  aesop

[Jakob von Raumer]

That or (if P then Q else R) ↔ (P ∧ Q ∨ ¬ P ∧ R)?

[Junyan Xu]

In practice I find docs#ite_eq_iff' much easier to use than docs#ite_eq_iff ...

[Kyle Miller]

Having implications like in Alex's formulation means you have access to p and Not p in q and r for example you do simp (config := {contextual := true})

[Eric Wieser]

Isn't the actual version we want:

theorem dite_prop {P : Prop} {Q : P → Prop} {R : ¬P → Prop} [Decidable P] :
    dite P Q R ↔ (∀ h, Q h) ∧ (∀ h, R h) := by
  by_cases h : P <;> simp [h, forall_prop_of_false, forall_prop_of_true]

[Kyle Miller]

docs#ite and docs#dite are both semireducible, so you'd want that in addition, not instead of