logic.lemmas

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

## 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 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 (λ (hp : ¬p), dite q (b hp) (c hp)) = dite q (λ (hq : q), dite p a (λ (hp : ¬p), b hp hq)) (λ (hq : ¬q), dite p a (λ (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 (λ (hp : p), dite q (a hp) (b hp)) c = dite q (λ (hq : q), dite p (λ (hp : p), a hp hq) c) (λ (hq : ¬q), dite p (λ (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 → α} :
ite p a (dite q b c) = dite q (λ (hq : q), ite p a (b hq)) (λ (hq : ¬q), ite p a (c hq))
theorem ite_dite_distrib_right {α : Sort u_1} {p q : Prop} [decidable p] [decidable q] {a : q → α} {b : ¬q → α} {c : α} :
ite p (dite q a b) c = dite q (λ (hq : q), ite p (a hq) c) (λ (hq : ¬q), ite p (b hq) c)
theorem dite_ite_distrib_left {α : Sort u_1} {p q : Prop} [decidable p] [decidable q] {a : p → α} {b c : ¬p → α} :
dite p a (λ (hp : ¬p), ite q (b hp) (c hp)) = ite q (dite p a b) (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 (λ (hp : p), ite q (a hp) (b hp)) c = ite q (dite p a c) (dite p b c)
theorem ite_ite_distrib_left {α : Sort u_1} {p q : Prop} [decidable p] [decidable q] {a b c : α} :
ite p a (ite q b c) = ite q (ite p a b) (ite p a c)
theorem ite_ite_distrib_right {α : Sort u_1} {p q : Prop} [decidable p] [decidable q] {a b c : α} :
ite p (ite q a b) c = ite q (ite p a c) (ite p b c)