Documentation

Mathlib.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 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 : Prop} {b : Prop} {c : Prop} :
((a b) c) (a (b c))
theorem iff_left_comm {a : Prop} {b : Prop} {c : Prop} :
(a (b c)) (b (a c))
theorem iff_right_comm {a : Prop} {b : Prop} {c : Prop} :
((a b) c) ((a c) b)
theorem Eq.heq :
∀ {α : Sort u_1} {a b : α}, a = bHEq a b

Alias of the reverse direction of heq_iff_eq.

theorem HEq.eq :
∀ {α : Sort u_1} {a b : α}, HEq a ba = b

Alias of the forward direction of heq_iff_eq.

theorem dite_dite_distrib_left {α : Sort u_1} {p : Prop} {q : Prop} [Decidable p] [Decidable q] {a : pα} {b : ¬pqα} {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 : Prop} {q : Prop} [Decidable p] [Decidable q] {a : pqα} {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 : Prop} {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 : Prop} {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 : Prop} {q : Prop} [Decidable p] [Decidable q] {a : pα} {b : ¬pα} {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 : Prop} {q : Prop} [Decidable p] [Decidable q] {a : pα} {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 : Prop} {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 : Prop} {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 : PropProp} :
(∀ (p : Prop), f p) f True f False
theorem Prop.exists {f : PropProp} :
(∃ (p : Prop), f p) f True f False