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 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 HEq.eq :
∀ {α : Sort u_1} {a b : α}, HEq a ba = b

Alias of the forward direction of heq_iff_eq.

theorem Eq.heq :
∀ {α : Sort u_1} {a b : α}, a = bHEq a b

Alias of the reverse direction of heq_iff_eq.

theorem dite_dite_distrib_left {α : Sort u_1} {p : Prop} {q : Prop} [inst : Decidable p] [inst : Decidable q] {a : pα} {b : ¬pqα} {c : ¬p¬qα} :
(dite p a fun hp => dite q (b hp) (c hp)) = if hq : q then dite p a fun hp => b hp hq else dite p a fun hp => c hp hq
theorem dite_dite_distrib_right {α : Sort u_1} {p : Prop} {q : Prop} [inst : Decidable p] [inst : Decidable q] {a : pqα} {b : p¬qα} {c : ¬pα} :
dite p (fun hp => dite q (a hp) (b hp)) c = if hq : q then dite p (fun hp => a hp hq) c else dite p (fun hp => b hp hq) c
theorem ite_dite_distrib_left {α : Sort u_1} {p : Prop} {q : Prop} [inst : Decidable p] [inst : 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} [inst : Decidable p] [inst : 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} [inst : Decidable p] [inst : Decidable q] {a : pα} {b : ¬pα} {c : ¬pα} :
(dite p a fun hp => 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} [inst : Decidable p] [inst : Decidable q] {a : pα} {b : pα} {c : ¬pα} :
dite p (fun hp => 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} [inst : Decidable p] [inst : 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} [inst : Decidable p] [inst : 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, f p) f True f False