More basic logic properties

A few more logic lemmas. These are in their own file, rather than Logic.Basic, because it is convenient to be able to use the tauto or split_ifs tactics.

Implementation notes

We spell those lemmas out with dite and ite rather than the if then else notation because this would result in less delta-reduced statements.

theorem iff_assoc {a b c : Prop} : ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))

theorem iff_left_comm {a b c : Prop} : (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))

theorem iff_right_comm {a b c : Prop} : ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)

theorem Eq.heq {α✝ : Sort u_1} {a b : α✝} : a = b → HEq a b

Alias of the reverse direction of heq_iff_eq.

theorem HEq.eq {α✝ : Sort u_1} {a b : α✝} : HEq a b → a = b

Alias of the forward direction of heq_iff_eq.

theorem dite_dite_distrib_left {α : Sort u_1} {p q : Prop} [Decidable p] [Decidable q] {a : p → α} {b : ¬p → q → α} {c : ¬p → ¬q → α} : (dite p a fun (hp : ¬p) => dite q (b hp) (c hp)) = if hq : q then dite p a fun (hp : ¬p) => b hp hq else dite p a fun (hp : ¬p) => c hp hq

theorem dite_dite_distrib_right {α : Sort u_1} {p q : Prop} [Decidable p] [Decidable q] {a : p → q → α} {b : p → ¬q → α} {c : ¬p → α} : dite p (fun (hp : p) => dite q (a hp) (b hp)) c = if hq : q then dite p (fun (hp : p) => a hp hq) c else dite p (fun (hp : p) => b hp hq) c

theorem ite_dite_distrib_left {α : Sort u_1} {p q : Prop} [Decidable p] [Decidable q] {a : α} {b : q → α} {c : ¬q → α} : (if p then a else dite q b c) = if hq : q then if p then a else b hq else if p then a else c hq

theorem ite_dite_distrib_right {α : Sort u_1} {p q : Prop} [Decidable p] [Decidable q] {a : q → α} {b : ¬q → α} {c : α} : (if p then dite q a b else c) = if hq : q then if p then a hq else c else if p then b hq else c

theorem dite_ite_distrib_left {α : Sort u_1} {p q : Prop} [Decidable p] [Decidable q] {a : p → α} {b c : ¬p → α} : (dite p a fun (hp : ¬p) => if q then b hp else c hp) = if q then dite p a b else dite p a c

theorem dite_ite_distrib_right {α : Sort u_1} {p q : Prop} [Decidable p] [Decidable q] {a b : p → α} {c : ¬p → α} : dite p (fun (hp : p) => if q then a hp else b hp) c = if q then dite p a c else dite p b c

theorem ite_ite_distrib_left {α : Sort u_1} {p q : Prop} [Decidable p] [Decidable q] {a b c : α} : (if p then a else if q then b else c) = if q then if p then a else b else if p then a else c

theorem ite_ite_distrib_right {α : Sort u_1} {p q : Prop} [Decidable p] [Decidable q] {a b c : α} : (if p then if q then a else b else c) = if q then if p then a else c else if p then b else c

theorem Prop.forall {f : Prop → Prop} : (∀ (p : Prop), f p) ↔ f True ∧ f False

theorem Prop.exists {f : Prop → Prop} : (∃ (p : Prop), f p) ↔ f True ∨ f False