Mathlib.Logic.Lemmas

iff_assoc theorem

{a b c : Prop} : ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))

Full source

theorem iff_assoc {a b c : Prop} : ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c)) := by tauto

Associativity of Logical Equivalence

Informal description

For any propositions $a$, $b$, and $c$, the equivalence $((a \leftrightarrow b) \leftrightarrow c)$ holds if and only if $(a \leftrightarrow (b \leftrightarrow c))$ holds.

iff_left_comm theorem

{a b c : Prop} : (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))

Full source

theorem iff_left_comm {a b c : Prop} : (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c)) := by tauto

Left Commutativity of Biconditional

Informal description

For any propositions $a$, $b$, and $c$, the equivalence $a \leftrightarrow (b \leftrightarrow c)$ holds if and only if $b \leftrightarrow (a \leftrightarrow c)$ holds.

iff_right_comm theorem

{a b c : Prop} : ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)

Full source

theorem iff_right_comm {a b c : Prop} : ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b) := by tauto

Right Commutativity of Biconditional

Informal description

For any propositions $a$, $b$, and $c$, the equivalence $((a \leftrightarrow b) \leftrightarrow c)$ holds if and only if $((a \leftrightarrow c) \leftrightarrow b)$ holds.

dite_dite_distrib_left theorem

 {a : p → α} {b : ¬p → q → α} {c : ¬p → ¬q → α} :
  (dite p a fun hp ↦ dite q (b hp) (c hp)) =
    dite q (fun hq ↦ (dite p a) fun hp ↦ b hp hq) fun hq ↦ (dite p a) fun hp ↦ c hp hq

Full source

theorem dite_dite_distrib_left {a : p → α} {b : ¬p → q → α} {c : ¬p → ¬q → α} :
    (dite p a fun hp ↦ dite q (b hp) (c hp)) =
      dite q (fun hq ↦ (dite p a) fun hp ↦ b hp hq) fun hq ↦ (dite p a) fun hp ↦ c hp hq := by
  split_ifs <;> rfl

Left Distributivity of Dependent If-Then-Else Statements

Informal description

For any propositions $p$ and $q$, and for any functions $a : p \to \alpha$, $b : \lnot p \to q \to \alpha$, and $c : \lnot p \to \lnot q \to \alpha$, the following equality holds: \[ \text{dite } p \, a \, (\lambda hp, \text{dite } q \, (b \, hp) \, (c \, hp)) = \text{dite } q \, (\lambda hq, \text{dite } p \, a \, (\lambda hp, b \, hp \, hq)) \, (\lambda hq, \text{dite } p \, a \, (\lambda hp, c \, hp \, hq)) \] where $\text{dite}$ is the dependent if-then-else construct.

dite_dite_distrib_right theorem

 {a : p → q → α} {b : p → ¬q → α} {c : ¬p → α} :
  dite p (fun hp ↦ dite q (a hp) (b hp)) c =
    dite q (fun hq ↦ dite p (fun hp ↦ a hp hq) c) fun hq ↦ dite p (fun hp ↦ b hp hq) c

Full source

theorem dite_dite_distrib_right {a : p → q → α} {b : p → ¬q → α} {c : ¬p → α} :
    dite p (fun hp ↦ dite q (a hp) (b hp)) c =
      dite q (fun hq ↦ dite p (fun hp ↦ a hp hq) c) fun hq ↦ dite p (fun hp ↦ b hp hq) c := by
  split_ifs <;> rfl

Distributivity of Dependent If-Then-Else Over Conditions

Informal description

For any propositions $p$ and $q$, and for any functions $a : p \to q \to \alpha$, $b : p \to \neg q \to \alpha$, and $c : \neg p \to \alpha$, the following equality holds: \[ \text{if } p \text{ then } (\text{if } q \text{ then } a \text{ else } b) \text{ else } c = \text{if } q \text{ then } (\text{if } p \text{ then } a \text{ else } c) \text{ else } (\text{if } p \text{ then } b \text{ else } c) \] where the "if-then-else" expressions are interpreted as dependent if-then-else (`dite`) constructs.

ite_dite_distrib_left theorem

 {a : α} {b : q → α} {c : ¬q → α} : ite p a (dite q b c) = dite q (fun hq ↦ ite p a <| b hq) fun hq ↦ ite p a <| c hq

Full source

theorem ite_dite_distrib_left {a : α} {b : q → α} {c : ¬q → α} :
    ite p a (dite q b c) = dite q (fun hq ↦ ite p a <| b hq) fun hq ↦ ite p a <| c hq :=
  dite_dite_distrib_left

Left Distributivity of If-Then-Else Over Dependent If-Then-Else

Informal description

For any type $\alpha$, any propositions $p$ and $q$, any element $a : \alpha$, and any functions $b : q \to \alpha$ and $c : \neg q \to \alpha$, the following equality holds: \[ \text{if } p \text{ then } a \text{ else } (\text{if } q \text{ then } b \text{ else } c) = \text{if } q \text{ then } (\text{if } p \text{ then } a \text{ else } b) \text{ else } (\text{if } p \text{ then } a \text{ else } c) \] where the first "if-then-else" is non-dependent (`ite`) and the second is dependent (`dite`).

ite_dite_distrib_right theorem

 {a : q → α} {b : ¬q → α} {c : α} : ite p (dite q a b) c = dite q (fun hq ↦ ite p (a hq) c) fun hq ↦ ite p (b hq) c

Full source

theorem ite_dite_distrib_right {a : q → α} {b : ¬q → α} {c : α} :
    ite p (dite q a b) c = dite q (fun hq ↦ ite p (a hq) c) fun hq ↦ ite p (b hq) c :=
  dite_dite_distrib_right

Right Distributivity of If-Then-Else Over Dependent If-Then-Else

Informal description

For any propositions $p$ and $q$, and for any functions $a : q \to \alpha$, $b : \neg q \to \alpha$, and an element $c : \alpha$, the following equality holds: \[ \text{if } p \text{ then } (\text{if } q \text{ then } a \text{ else } b) \text{ else } c = \text{if } q \text{ then } (\text{if } p \text{ then } a \text{ else } c) \text{ else } (\text{if } p \text{ then } b \text{ else } c) \] where the "if-then-else" expressions are interpreted as non-dependent (`ite`) and dependent (`dite`) if-then-else constructs.

dite_ite_distrib_left theorem

 {a : p → α} {b : ¬p → α} {c : ¬p → α} : (dite p a fun hp ↦ ite q (b hp) (c hp)) = ite q (dite p a b) (dite p a c)

Full source

theorem dite_ite_distrib_left {a : p → α} {b : ¬p → α} {c : ¬p → α} :
    (dite p a fun hp ↦ ite q (b hp) (c hp)) = ite q (dite p a b) (dite p a c) :=
  dite_dite_distrib_left

Left Distributivity of Dependent If-Then-Else over Regular If-Then-Else

Informal description

For any proposition $p$ and any type $\alpha$, given functions $a : p \to \alpha$, $b : \lnot p \to \alpha$, and $c : \lnot p \to \alpha$, the following equality holds: \[ \text{dite } p \, a \, (\lambda hp, \text{ite } q \, (b \, hp) \, (c \, hp)) = \text{ite } q \, (\text{dite } p \, a \, b) \, (\text{dite } p \, a \, c) \] where $\text{dite}$ is the dependent if-then-else construct and $\text{ite}$ is the regular if-then-else construct.

dite_ite_distrib_right theorem

 {a : p → α} {b : p → α} {c : ¬p → α} : dite p (fun hp ↦ ite q (a hp) (b hp)) c = ite q (dite p a c) (dite p b c)

Full source

theorem dite_ite_distrib_right {a : p → α} {b : p → α} {c : ¬p → α} :
    dite p (fun hp ↦ ite q (a hp) (b hp)) c = ite q (dite p a c) (dite p b c) :=
  dite_dite_distrib_right

Distributivity of Dependent If-Then-Else Over Regular If-Then-Else (Right)

Informal description

For any propositions $p$ and $q$, and for any functions $a, b : p \to \alpha$ and $c : \neg p \to \alpha$, the following equality holds: \[ \text{if } p \text{ then } (\text{if } q \text{ then } a \text{ else } b) \text{ else } c = \text{if } q \text{ then } (\text{if } p \text{ then } a \text{ else } c) \text{ else } (\text{if } p \text{ then } b \text{ else } c) \] where the outer "if-then-else" is a dependent if-then-else (`dite`) and the inner one is a regular if-then-else (`ite`).

ite_ite_distrib_left theorem

: ite p a (ite q b c) = ite q (ite p a b) (ite p a c)

Full source

theorem ite_ite_distrib_left : ite p a (ite q b c) = ite q (ite p a b) (ite p a c) :=
  dite_dite_distrib_left

Left Distributivity of If-Then-Else Statements

Informal description

For any propositions $p$ and $q$, and for any elements $a$, $b$, and $c$ of type $\alpha$, the following equality holds: \[ \text{if } p \text{ then } a \text{ else } (\text{if } q \text{ then } b \text{ else } c) = \text{if } q \text{ then } (\text{if } p \text{ then } a \text{ else } b) \text{ else } (\text{if } p \text{ then } a \text{ else } c) \]

ite_ite_distrib_right theorem

: ite p (ite q a b) c = ite q (ite p a c) (ite p b c)

Full source

theorem ite_ite_distrib_right : ite p (ite q a b) c = ite q (ite p a c) (ite p b c) :=
  dite_dite_distrib_right

Right Distributivity of Nested If-Then-Else Statements

Informal description

For any propositions $p$ and $q$, and for any elements $a$, $b$, and $c$ of type $\alpha$, the following equality holds: \[ \text{if } p \text{ then } (\text{if } q \text{ then } a \text{ else } b) \text{ else } c = \text{if } q \text{ then } (\text{if } p \text{ then } a \text{ else } c) \text{ else } (\text{if } p \text{ then } b \text{ else } c) \] where the "if-then-else" expressions are interpreted as non-dependent if-then-else (`ite`) constructs.

Prop.forall theorem

{f : Prop → Prop} : (∀ p, f p) ↔ f True ∧ f False

Full source

lemma Prop.forall {f : Prop → Prop} : (∀ p, f p) ↔ f True ∧ f False :=
  ⟨fun h ↦ ⟨h _, h _⟩, by rintro ⟨h₁, h₀⟩ p; by_cases hp : p <;> simp only [hp] <;> assumption⟩

Universal Quantification over Propositions is Equivalent to Conjunction at True and False

Informal description

For any predicate $f$ on propositions, the universal quantification $\forall p, f(p)$ holds if and only if both $f(\text{True})$ and $f(\text{False})$ hold.

Prop.exists theorem

{f : Prop → Prop} : (∃ p, f p) ↔ f True ∨ f False

Full source

lemma Prop.exists {f : Prop → Prop} : (∃ p, f p) ↔ f True ∨ f False :=
  ⟨fun ⟨p, h⟩ ↦ by refine (em p).imp ?_ ?_ <;> intro H <;> convert h <;> simp [H],
    by rintro (h | h) <;> exact ⟨_, h⟩⟩

Existential Quantification over Propositions is Equivalent to Disjunction at True and False

Informal description

For any predicate $f$ on propositions, the existential quantification $\exists p, f(p)$ holds if and only if either $f(\text{True})$ or $f(\text{False})$ holds.

Implementation notes