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)