# 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.

source
theorem iff_assoc {a b c : Prop} :
((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))
source
theorem iff_left_comm {a b c : Prop} :
(a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))
source
theorem iff_right_comm {a b c : Prop} :
((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
source
theorem HEq.eq {α : Sort u_1} {a b : α} :
a ≍ b → a = b

Alias of the forward direction of `heq_iff_eq`.

source
theorem Eq.heq {α : Sort u_1} {a b : α} :
a = b → a ≍ b

Alias of the reverse direction of `heq_iff_eq`.

source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
theorem Prop.forall {f : Prop → Prop} :
(∀ (p : Prop), f p) ↔ f True ∧ f False
source
theorem Prop.exists {f : Prop → Prop} :
(∃ (p : Prop), f p) ↔ f True ∨ f False