Init.SimpLemmas

of_eq_true theorem

(h : p = True) : p

Full source

theorem of_eq_true (h : p = True) : p := h ▸ trivial

Implication from Equality to True

Informal description

If a proposition $p$ is equal to the true proposition $\text{True}$, then $p$ holds.

of_eq_false theorem

(h : p = False) : ¬p

Full source

theorem of_eq_false (h : p = False) : ¬ p := fun hp => False.elim (h.mp hp)

Negation from False Equality

Informal description

If a proposition $p$ is equal to `False`, then $\neg p$ holds.

implies_congr theorem

{p₁ p₂ : Sort u} {q₁ q₂ : Sort v} (h₁ : p₁ = p₂) (h₂ : q₁ = q₂) : (p₁ → q₁) = (p₂ → q₂)

Full source

theorem implies_congr {p₁ p₂ : Sort u} {q₁ q₂ : Sort v} (h₁ : p₁ = p₂) (h₂ : q₁ = q₂) : (p₁ → q₁) = (p₂ → q₂) :=
  h₁ ▸ h₂ ▸ rfl

Congruence of Function Types Under Type Equality

Informal description

For any types $p₁, p₂$ (in universe $u$) and $q₁, q₂$ (in universe $v$), if $p₁ = p₂$ and $q₁ = q₂$, then the type of functions from $p₁$ to $q₁$ is equal to the type of functions from $p₂$ to $q₂$.

iff_congr theorem

{p₁ p₂ q₁ q₂ : Prop} (h₁ : p₁ ↔ p₂) (h₂ : q₁ ↔ q₂) : (p₁ ↔ q₁) ↔ (p₂ ↔ q₂)

Full source

theorem iff_congr {p₁ p₂ q₁ q₂ : Prop} (h₁ : p₁ ↔ p₂) (h₂ : q₁ ↔ q₂) : (p₁ ↔ q₁) ↔ (p₂ ↔ q₂) :=
  Iff.of_eq (propext h₁ ▸ propext h₂ ▸ rfl)

Congruence of Biconditional Statements

Informal description

For any propositions $p₁, p₂, q₁, q₂$, if $p₁$ is equivalent to $p₂$ and $q₁$ is equivalent to $q₂$, then the equivalence $p₁ ↔ q₁$ holds if and only if $p₂ ↔ q₂$ holds.

implies_dep_congr_ctx theorem

 {p₁ p₂ q₁ : Prop} (h₁ : p₁ = p₂) {q₂ : p₂ → Prop} (h₂ : (h : p₂) → q₁ = q₂ h) : (p₁ → q₁) = ((h : p₂) → q₂ h)

Full source

theorem implies_dep_congr_ctx {p₁ p₂ q₁ : Prop} (h₁ : p₁ = p₂) {q₂ : p₂ → Prop} (h₂ : (h : p₂) → q₁ = q₂ h) : (p₁ → q₁) = ((h : p₂) → q₂ h) :=
  propext ⟨
    fun hl hp₂ => (h₂ hp₂).mp (hl (h₁.mpr hp₂)),
    fun hr hp₁ => (h₂ (h₁.mp hp₁)).mpr (hr (h₁.mp hp₁))⟩

Contextual Congruence for Dependent Implications

Informal description

Given propositions $p_1$ and $p_2$ such that $p_1 = p_2$, and a proposition $q_1$ that depends on $p_1$, and a family of propositions $q_2$ depending on $p_2$ such that for any proof $h$ of $p_2$, we have $q_1 = q_2(h)$, then the implication $p_1 \to q_1$ is equal to the dependent implication $(h : p_2) \to q_2(h)$.

implies_congr_ctx theorem

{p₁ p₂ q₁ q₂ : Prop} (h₁ : p₁ = p₂) (h₂ : p₂ → q₁ = q₂) : (p₁ → q₁) = (p₂ → q₂)

Full source

theorem implies_congr_ctx {p₁ p₂ q₁ q₂ : Prop} (h₁ : p₁ = p₂) (h₂ : p₂ → q₁ = q₂) : (p₁ → q₁) = (p₂ → q₂) :=
  implies_dep_congr_ctx h₁ h₂

Contextual Congruence for Implications

Informal description

Given propositions $p_1, p_2, q_1, q_2$ such that $p_1 = p_2$ and for any proof of $p_2$, we have $q_1 = q_2$, then the implication $p_1 \to q_1$ is equal to the implication $p_2 \to q_2$.

forall_congr theorem

{α : Sort u} {p q : α → Prop} (h : ∀ a, p a = q a) : (∀ a, p a) = (∀ a, q a)

Full source

theorem forall_congr {α : Sort u} {p q : α → Prop} (h : ∀ a, p a = q a) : (∀ a, p a) = (∀ a, q a) :=
  (funext h : p = q) ▸ rfl

Equivalence of Universal Quantifications under Pointwise Equivalence

Informal description

For any type $\alpha$ and predicates $p, q : \alpha \to \text{Prop}$, if for every element $a$ of $\alpha$ the propositions $p(a)$ and $q(a)$ are equivalent, then the universal quantifications $(\forall a, p(a))$ and $(\forall a, q(a))$ are also equivalent.

forall_prop_domain_congr theorem

 {p₁ p₂ : Prop} {q₁ : p₁ → Prop} {q₂ : p₂ → Prop} (h₁ : p₁ = p₂) (h₂ : ∀ a : p₂, q₁ (h₁.substr a) = q₂ a) :
  (∀ a : p₁, q₁ a) = (∀ a : p₂, q₂ a)

Full source

theorem forall_prop_domain_congr {p₁ p₂ : Prop} {q₁ : p₁ → Prop} {q₂ : p₂ → Prop}
    (h₁ : p₁ = p₂)
    (h₂ : ∀ a : p₂, q₁ (h₁.substr a) = q₂ a)
    : (∀ a : p₁, q₁ a) = (∀ a : p₂, q₂ a) := by
  subst h₁; simp [← h₂]

Equivalence of Universal Quantifications under Propositional Equality and Pointwise Equivalence

Informal description

For any propositions $p_1$ and $p_2$ such that $p_1 = p_2$, and for any predicates $q_1 : p_1 \to \text{Prop}$ and $q_2 : p_2 \to \text{Prop}$, if for every proof $a$ of $p_2$ we have $q_1(h_1(a)) = q_2(a)$, where $h_1$ is the substitution induced by $p_1 = p_2$, then the universal quantification $(\forall a : p_1, q_1(a))$ is equal to $(\forall a : p_2, q_2(a))$.

forall_prop_congr_dom theorem

{p₁ p₂ : Prop} (h : p₁ = p₂) (q : p₁ → Prop) : (∀ a : p₁, q a) = (∀ a : p₂, q (h.substr a))

Full source

theorem forall_prop_congr_dom {p₁ p₂ : Prop} (h : p₁ = p₂) (q : p₁ → Prop) :
    (∀ a : p₁, q a) = (∀ a : p₂, q (h.substr a)) :=
  h ▸ rfl

Equivalence of Universal Quantifications under Propositional Equality

Informal description

For any propositions $p_1$ and $p_2$ such that $p_1 = p_2$, and for any predicate $q$ on $p_1$, the universal quantification over $p_1$ of $q$ is equal to the universal quantification over $p_2$ of $q$ composed with the substitution induced by $h$.

pi_congr theorem

{α : Sort u} {β β' : α → Sort v} (h : ∀ a, β a = β' a) : (∀ a, β a) = ∀ a, β' a

Full source

theorem pi_congr {α : Sort u} {β β' : α → Sort v} (h : ∀ a, β a = β' a) : (∀ a, β a) = ∀ a, β' a :=
  (funext h : β = β') ▸ rfl

Equality of Dependent Function Types under Pointwise Equality

Informal description

For any type $\alpha$ and families of types $\beta, \beta' : \alpha \to \text{Type}$, if $\beta(a) = \beta'(a)$ for all $a : \alpha$, then the dependent function types $(\forall a, \beta a)$ and $(\forall a, \beta' a)$ are equal.

let_congr theorem

 {α : Sort u} {β : Sort v} {a a' : α} {b b' : α → β} (h₁ : a = a') (h₂ : ∀ x, b x = b' x) :
  (let x := a;
    b x) =
    (let x := a';
    b' x)

Full source

theorem let_congr {α : Sort u} {β : Sort v} {a a' : α} {b b' : α → β}
    (h₁ : a = a') (h₂ : ∀ x, b x = b' x) : (let x := a; b x) = (let x := a'; b' x) :=
  h₁ ▸ (funext h₂ : b = b') ▸ rfl

Congruence of Let Expressions with Equal Values and Functions

Informal description

Let $α$ and $β$ be types, and let $a, a'$ be elements of $α$ and $b, b'$ be functions from $α$ to $β$. If $a = a'$ and for all $x$ in $α$, $b(x) = b'(x)$, then the expressions `let x := a; b x` and `let x := a'; b' x` are equal.

let_val_congr theorem

 {α : Sort u} {β : Sort v} {a a' : α} (b : α → β) (h : a = a') :
  (let x := a;
    b x) =
    (let x := a';
    b x)

Full source

theorem let_val_congr {α : Sort u} {β : Sort v} {a a' : α}
    (b : α → β) (h : a = a') : (let x := a; b x) = (let x := a'; b x) := h ▸ rfl

Equality Preservation Under Let-Binding with Equal Values

Informal description

For any types $\alpha$ and $\beta$, given elements $a, a' \in \alpha$ and a function $b : \alpha \to \beta$, if $a = a'$, then the expressions `let x := a; b x` and `let x := a'; b x` are equal.

let_body_congr theorem

 {α : Sort u} {β : α → Sort v} {b b' : (a : α) → β a} (a : α) (h : ∀ x, b x = b' x) :
  (let x := a;
    b x) =
    (let x := a;
    b' x)

Full source

theorem let_body_congr {α : Sort u} {β : α → Sort v} {b b' : (a : α) → β a}
    (a : α) (h : ∀ x, b x = b' x) : (let x := a; b x) = (let x := a; b' x) :=
  (funext h : b = b') ▸ rfl

Congruence of Let-Body Expressions

Informal description

Let $\alpha$ and $\beta$ be types, where $\beta$ depends on $\alpha$. For any $a \in \alpha$ and functions $b, b' \colon \alpha \to \beta$ such that $b(x) = b'(x)$ for all $x \in \alpha$, the expressions `let x := a; b x` and `let x := a; b' x` are equal.

letFun_unused theorem

{α : Sort u} {β : Sort v} (a : α) {b b' : β} (h : b = b') : @letFun α (fun _ => β) a (fun _ => b) = b'

Full source

theorem letFun_unused {α : Sort u} {β : Sort v} (a : α) {b b' : β} (h : b = b') : @letFun α (fun _ => β) a (fun _ => b) = b' :=
  h

Unused `letFun` Argument Equality

Informal description

For any types $\alpha$ and $\beta$, given an element $a \in \alpha$ and elements $b, b' \in \beta$ such that $b = b'$, the expression `letFun a (fun _ => b)` is equal to $b'$.

letFun_congr theorem

 {α : Sort u} {β : Sort v} {a a' : α} {f f' : α → β} (h₁ : a = a') (h₂ : ∀ x, f x = f' x) :
  @letFun α (fun _ => β) a f = @letFun α (fun _ => β) a' f'

Full source

theorem letFun_congr {α : Sort u} {β : Sort v}  {a a' : α} {f f' : α → β} (h₁ : a = a') (h₂ : ∀ x, f x = f' x)
    : @letFun α (fun _ => β) a f = @letFun α (fun _ => β) a' f' := by
  rw [h₁, funext h₂]

Congruence of `letFun` with respect to equality of arguments and functions

Informal description

For any types $\alpha$ and $\beta$, and elements $a, a' : \alpha$ and functions $f, f' : \alpha \to \beta$, if $a = a'$ and for all $x : \alpha$, $f(x) = f'(x)$, then the expressions `letFun a f` and `letFun a' f'` are equal.

letFun_body_congr theorem

 {α : Sort u} {β : Sort v} (a : α) {f f' : α → β} (h : ∀ x, f x = f' x) :
  @letFun α (fun _ => β) a f = @letFun α (fun _ => β) a f'

Full source

theorem letFun_body_congr {α : Sort u} {β : Sort v}  (a : α) {f f' : α → β} (h : ∀ x, f x = f' x)
    : @letFun α (fun _ => β) a f = @letFun α (fun _ => β) a f' := by
  rw [funext h]

Congruence of Let-Binding Under Function Equality

Informal description

For any types $\alpha$ and $\beta$, given an element $a \in \alpha$ and functions $f, f' : \alpha \to \beta$, if $f(x) = f'(x)$ for all $x \in \alpha$, then the let-binding expressions $\texttt{letFun}(a, f)$ and $\texttt{letFun}(a, f')$ are equal.

letFun_val_congr theorem

 {α : Sort u} {β : Sort v} {a a' : α} {f : α → β} (h : a = a') :
  @letFun α (fun _ => β) a f = @letFun α (fun _ => β) a' f

Full source

theorem letFun_val_congr {α : Sort u} {β : Sort v} {a a' : α} {f : α → β} (h : a = a')
    : @letFun α (fun _ => β) a f = @letFun α (fun _ => β) a' f := by
  rw [h]

Congruence of Function Evaluation under Equality of Arguments

Informal description

For any types $\alpha$ and $\beta$, given elements $a, a' \in \alpha$ and a function $f : \alpha \to \beta$, if $a = a'$, then the evaluation of $f$ at $a$ is equal to the evaluation of $f$ at $a'$, i.e., $f(a) = f(a')$.

ite_congr theorem

 {x y u v : α} {s : Decidable b} [Decidable c] (h₁ : b = c) (h₂ : c → x = u) (h₃ : ¬c → y = v) : ite b x y = ite c u v

Full source

@[congr]
theorem ite_congr {x y u v : α} {s : Decidable b} [Decidable c]
    (h₁ : b = c) (h₂ : c → x = u) (h₃ : ¬ c → y = v) : ite b x y = ite c u v := by
  cases Decidable.em c with
  | inl h => rw [if_pos h]; subst b; rw [if_pos h]; exact h₂ h
  | inr h => rw [if_neg h]; subst b; rw [if_neg h]; exact h₃ h

Congruence of Conditional Expressions: $\text{ite}(b, x, y) = \text{ite}(c, u, v)$ under Equivalent Conditions

Informal description

For any type $\alpha$, boolean conditions $b$ and $c$, and elements $x, y, u, v \in \alpha$, if $b = c$, and whenever $c$ holds we have $x = u$, and whenever $\neg c$ holds we have $y = v$, then the conditional expression $\text{ite}(b, x, y)$ equals $\text{ite}(c, u, v)$.

Eq.mpr_prop theorem

{p q : Prop} (h₁ : p = q) (h₂ : q) : p

Full source

theorem Eq.mpr_prop {p q : Prop} (h₁ : p = q) (h₂ : q)  : p  := h₁ ▸ h₂

Implication via Equality of Propositions

Informal description

For any propositions $p$ and $q$, if $p = q$ and $q$ holds, then $p$ holds.

Eq.mpr_not theorem

{p q : Prop} (h₁ : p = q) (h₂ : ¬q) : ¬p

Full source

theorem Eq.mpr_not  {p q : Prop} (h₁ : p = q) (h₂ : ¬q) : ¬p := h₁ ▸ h₂

Implication of Negation via Equality: $\neg q \to \neg p$ when $p = q$

Informal description

For any propositions $p$ and $q$, if $p = q$ and $\neg q$ holds, then $\neg p$ holds.

dite_congr theorem

 {_ : Decidable b} [Decidable c] {x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α} (h₁ : b = c)
  (h₂ : (h : c) → x (h₁.mpr_prop h) = u h) (h₃ : (h : ¬c) → y (h₁.mpr_not h) = v h) : dite b x y = dite c u v

Full source

@[congr]
theorem dite_congr {_ : Decidable b} [Decidable c]
    {x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
    (h₁ : b = c)
    (h₂ : (h : c)  → x (h₁.mpr_prop h) = u h)
    (h₃ : (h : ¬c) → y (h₁.mpr_not h)  = v h) :
    dite b x y = dite c u v := by
  cases Decidable.em c with
  | inl h => rw [dif_pos h]; subst b; rw [dif_pos h]; exact h₂ h
  | inr h => rw [dif_neg h]; subst b; rw [dif_neg h]; exact h₃ h

Congruence of Dependent If-Then-Else Expressions under Propositional Equality

Informal description

Let $b$ and $c$ be decidable propositions, and let $\alpha$ be a type. Suppose we have functions $x : b \to \alpha$, $u : c \to \alpha$, $y : \neg b \to \alpha$, and $v : \neg c \to \alpha$. If $b = c$, and for all $h : c$ we have $x(h_1(h)) = u(h)$ (where $h_1$ is the proof that $b = c$), and for all $h : \neg c$ we have $y(h_2(h)) = v(h)$ (where $h_2$ is the proof that $\neg b$ follows from $\neg c$ via $b = c$), then the dependent if-then-else expressions $\text{dite } b \text{ } x \text{ } y$ and $\text{dite } c \text{ } u \text{ } v$ are equal.

ne_eq theorem

(a b : α) : (a ≠ b) = ¬(a = b)

Full source

@[simp] theorem ne_eq (a b : α) : (a ≠ b) = ¬(a = b) := rfl

Inequality as Negation of Equality

Informal description

For any two elements $a$ and $b$ of type $\alpha$, the inequality $a \neq b$ is equivalent to the negation of the equality $a = b$, i.e., $a \neq b = \neg (a = b)$.

ite_true theorem

(a b : α) : (if True then a else b) = a

Full source

@[simp] theorem ite_true (a b : α) : (if True then a else b) = a := rfl

Conditional Evaluation with True Condition: $\text{if True then } a \text{ else } b = a$

Informal description

For any elements $a$ and $b$ of a type $\alpha$, the conditional expression `if True then a else b` evaluates to $a$.

ite_false theorem

(a b : α) : (if False then a else b) = b

Full source

@[simp] theorem ite_false (a b : α) : (if False then a else b) = b := rfl

Conditional Evaluation for False Case: `if False then a else b = b`

Informal description

For any elements $a$ and $b$ of a type $\alpha$, the expression `if False then a else b` evaluates to $b$.

dite_true theorem

{α : Sort u} {t : True → α} {e : ¬True → α} : (dite True t e) = t True.intro

Full source

@[simp] theorem dite_true {α : Sort u} {t : True → α} {e : ¬ True → α} : (dite True t e) = t True.intro := rfl

Dependent If-True Evaluation

Informal description

For any type `α` and functions `t : True → α` and `e : ¬True → α`, the dependent if-then-else expression `dite True t e` evaluates to `t True.intro`.

dite_false theorem

{α : Sort u} {t : False → α} {e : ¬False → α} : (dite False t e) = e not_false

Full source

@[simp] theorem dite_false {α : Sort u} {t : False → α} {e : ¬ False → α} : (dite False t e) = e not_false := rfl

Dependent If-Then-Else on False Yields Else Branch

Informal description

For any type $\alpha$, given functions $t : \text{False} \to \alpha$ and $e : \neg\text{False} \to \alpha$, the dependent if-then-else expression `dite False t e` evaluates to $e(\text{not\_false})$, where $\text{not\_false}$ is a proof that $\text{False}$ is not true.

ite_cond_eq_true theorem

{α : Sort u} {c : Prop} {_ : Decidable c} (a b : α) (h : c = True) : (if c then a else b) = a

Full source

theorem ite_cond_eq_true {α : Sort u} {c : Prop} {_ : Decidable c} (a b : α) (h : c = True) : (if c then a else b) = a := by simp [h]

Conditional Evaluation when Condition is True: $\text{ite}(c, a, b) = a$ if $c = \text{True}$

Informal description

For any type $\alpha$, proposition $c$ with a decidable instance, and elements $a, b \in \alpha$, if $c$ is equal to $\text{True}$, then the conditional expression $\text{ite}(c, a, b)$ evaluates to $a$.

ite_cond_eq_false theorem

{α : Sort u} {c : Prop} {_ : Decidable c} (a b : α) (h : c = False) : (if c then a else b) = b

Full source

theorem ite_cond_eq_false {α : Sort u} {c : Prop} {_ : Decidable c} (a b : α) (h : c = False) : (if c then a else b) = b := by simp [h]

Conditional Evaluation When Condition is False: $\text{ite}(c, a, b) = b$ if $c = \text{False}$

Informal description

For any type $\alpha$, proposition $c$ with a decidability instance, and elements $a, b \in \alpha$, if $c$ is equal to $\text{False}$, then the conditional expression $\text{ite}(c, a, b)$ evaluates to $b$.

dite_cond_eq_true theorem

 {α : Sort u} {c : Prop} {_ : Decidable c} {t : c → α} {e : ¬c → α} (h : c = True) : (dite c t e) = t (of_eq_true h)

Full source

theorem dite_cond_eq_true {α : Sort u} {c : Prop} {_ : Decidable c} {t : c → α} {e : ¬ c → α} (h : c = True) : (dite c t e) = t (of_eq_true h) := by simp [h]

Dependent If-Then-Else Evaluation When Condition is True: $\text{dite}(c, t, e) = t(\text{of\_eq\_true}(h))$ if $c = \text{True}$

Informal description

For any type $\alpha$, decidable proposition $c$, and functions $t : c \to \alpha$ and $e : \neg c \to \alpha$, if $c$ is equal to $\text{True}$, then the dependent if-then-else expression $\text{dite } c \text{ } t \text{ } e$ evaluates to $t$ applied to the proof that $c$ holds (obtained from the equality $c = \text{True}$).

dite_cond_eq_false theorem

 {α : Sort u} {c : Prop} {_ : Decidable c} {t : c → α} {e : ¬c → α} (h : c = False) : (dite c t e) = e (of_eq_false h)

Full source

theorem dite_cond_eq_false {α : Sort u} {c : Prop} {_ : Decidable c} {t : c → α} {e : ¬ c → α} (h : c = False) : (dite c t e) = e (of_eq_false h) := by simp [h]

Dependent If-Then-Else Evaluation When Condition is False: $\text{dite}(c, t, e) = e(\text{of\_eq\_false}(h))$ if $c = \text{False}$

Informal description

For any type $\alpha$, decidable proposition $c$, and functions $t : c \to \alpha$ and $e : ¬c \to \alpha$, if $c$ is equal to $\text{False}$, then the dependent if-then-else expression $\text{dite } c \text{ } t \text{ } e$ evaluates to $e$ applied to the proof that $\neg c$ holds (obtained from the equality $c = \text{False}$).

ite_self theorem

{α : Sort u} {c : Prop} {d : Decidable c} (a : α) : ite c a a = a

Full source

@[simp] theorem ite_self {α : Sort u} {c : Prop} {d : Decidable c} (a : α) : ite c a a = a := by cases d <;> rfl

Conditional Self-Identity: $\text{if } c \text{ then } a \text{ else } a = a$

Informal description

For any type $\alpha$, any proposition $c$ with a decision procedure, and any element $a : \alpha$, the expression `if $c$ then $a$ else $a$` is equal to $a$.

and_true theorem

(p : Prop) : (p ∧ True) = p

Full source

@[simp] theorem and_true (p : Prop) : (p ∧ True) = p := propext ⟨(·.1), (⟨·, trivial⟩)⟩

Conjunction with True: $p \land \text{True} = p$

Informal description

For any proposition $p$, the conjunction $p \land \text{True}$ is equivalent to $p$.

true_and theorem

(p : Prop) : (True ∧ p) = p

Full source

@[simp] theorem true_and (p : Prop) : (TrueTrue ∧ p) = p := propext ⟨(·.2), (⟨trivial, ·⟩)⟩

Conjunction with True: $\text{True} \land p \leftrightarrow p$

Informal description

For any proposition $p$, the conjunction of the true proposition and $p$ is equivalent to $p$, i.e., $\text{True} \land p \leftrightarrow p$.

instLawfulIdentityAndTrue instance

: Std.LawfulIdentity And True

Full source

instance : Std.LawfulIdentity And True where
  left_id := true_and
  right_id := and_true

$\text{True}$ as Identity for Conjunction

Informal description

The logical conjunction operation $\land$ with the constant $\text{True}$ forms a lawful identity structure, where $\text{True}$ acts as a right and left identity element for $\land$.

and_false theorem

(p : Prop) : (p ∧ False) = False

Full source

@[simp] theorem and_false (p : Prop) : (p ∧ False) = False := eq_false (·.2)

Conjunction with False: $p \land \text{False} = \text{False}$

Informal description

For any proposition $p$, the conjunction $p \land \text{False}$ is equivalent to $\text{False}$.

false_and theorem

(p : Prop) : (False ∧ p) = False

Full source

@[simp] theorem false_and (p : Prop) : (FalseFalse ∧ p) = False := eq_false (·.1)

Conjunction with False: $\text{False} \land p = \text{False}$

Informal description

For any proposition $p$, the conjunction $\text{False} \land p$ is equivalent to $\text{False}$.

and_self theorem

(p : Prop) : (p ∧ p) = p

Full source

@[simp] theorem and_self (p : Prop) : (p ∧ p) = p := propext ⟨(·.left), fun h => ⟨h, h⟩⟩

Idempotence of Conjunction: $p \land p = p$

Informal description

For any proposition $p$, the conjunction $p \land p$ is equivalent to $p$.

instIdempotentOpAnd instance

: Std.IdempotentOp And

Full source

instance : Std.IdempotentOp And := ⟨and_self⟩

Idempotence of Logical Conjunction

Informal description

The logical conjunction operation $\land$ is idempotent, meaning that for any proposition $p$, the conjunction $p \land p$ is equivalent to $p$.

and_not_self theorem

: ¬(a ∧ ¬a)

Full source

@[simp] theorem and_not_self : ¬(a ∧ ¬a) | ⟨ha, hn⟩ => absurd ha hn

Contradiction: $\neg(a \land \neg a)$

Informal description

For any proposition $a$, it is not the case that both $a$ and $\neg a$ hold simultaneously, i.e., $\neg(a \land \neg a)$.

not_and_self theorem

: ¬(¬a ∧ a)

Full source

@[simp] theorem not_and_self : ¬(¬a ∧ a) := and_not_selfand_not_self ∘ And.symm

Contradiction: $\neg(\neg a \land a)$

Informal description

For any proposition $a$, it is not the case that both $\neg a$ and $a$ hold simultaneously, i.e., $\neg(\neg a \land a)$.

and_imp theorem

: (a ∧ b → c) ↔ (a → b → c)

Full source

@[simp] theorem and_imp : (a ∧ b → c) ↔ (a → b → c) := ⟨fun h ha hb => h ⟨ha, hb⟩, fun h ⟨ha, hb⟩ => h ha hb⟩

Implication Equivalence: $(a \land b \to c) \leftrightarrow (a \to b \to c)$

Informal description

For any propositions $a$, $b$, and $c$, the implication $a \land b \to c$ holds if and only if $a \to (b \to c)$ holds.

not_and theorem

: ¬(a ∧ b) ↔ (a → ¬b)

Full source

@[simp] theorem not_and : ¬(a ∧ b)¬(a ∧ b) ↔ (a → ¬b) := and_imp

De Morgan's Law for Conjunction: $\neg(a \land b) \leftrightarrow (a \to \neg b)$

Informal description

For any propositions $a$ and $b$, the negation of their conjunction $\neg(a \land b)$ is equivalent to the implication $a \to \neg b$.

or_self theorem

(p : Prop) : (p ∨ p) = p

Full source

@[simp] theorem or_self (p : Prop) : (p ∨ p) = p := propext ⟨fun | .inl h | .inr h => h, .inl⟩

Idempotence of Disjunction: $p \lor p \leftrightarrow p$

Informal description

For any proposition $p$, the disjunction $p \lor p$ is equivalent to $p$.

instIdempotentOpOr instance

: Std.IdempotentOp Or

Full source

instance : Std.IdempotentOp Or := ⟨or_self⟩

Idempotence of Logical Disjunction

Informal description

The logical disjunction operation $\lor$ is idempotent.

or_true theorem

(p : Prop) : (p ∨ True) = True

Full source

@[simp] theorem or_true (p : Prop) : (p ∨ True) = True := eq_true (.inr trivial)

Disjunction with True is True

Informal description

For any proposition $p$, the disjunction $p \lor \text{True}$ is equivalent to $\text{True}$.

true_or theorem

(p : Prop) : (True ∨ p) = True

Full source

@[simp] theorem true_or (p : Prop) : (TrueTrue ∨ p) = True := eq_true (.inl trivial)

Disjunction with True is True

Informal description

For any proposition $p$, the disjunction $\text{True} \lor p$ is equivalent to $\text{True}$.

or_false theorem

(p : Prop) : (p ∨ False) = p

Full source

@[simp] theorem or_false (p : Prop) : (p ∨ False) = p := propext ⟨fun (.inl h) => h, .inl⟩

Disjunction with False: $p \lor \text{False} \iff p$

Informal description

For any proposition $p$, the disjunction $p \lor \text{False}$ is equivalent to $p$.

false_or theorem

(p : Prop) : (False ∨ p) = p

Full source

@[simp] theorem false_or (p : Prop) : (FalseFalse ∨ p) = p := propext ⟨fun (.inr h) => h, .inr⟩

False Disjunction Identity: $\text{False} \lor p \leftrightarrow p$

Informal description

For any proposition $p$, the disjunction $\text{False} \lor p$ is equivalent to $p$.

instLawfulIdentityOrFalse instance

: Std.LawfulIdentity Or False

Full source

instance : Std.LawfulIdentity Or False where
  left_id := false_or
  right_id := or_false

Disjunction with False as Identity

Informal description

The disjunction operation `Or` with `False` as the identity element forms a lawful identity structure. This means that for any proposition $p$, the operations $p \lor \text{False}$ and $\text{False} \lor p$ are both equivalent to $p$ itself.

iff_self theorem

(p : Prop) : (p ↔ p) = True

Full source

@[simp] theorem iff_self (p : Prop) : (p ↔ p) = True := eq_true .rfl

Equivalence of a Proposition with Itself is True

Informal description

For any proposition $p$, the equivalence $p \leftrightarrow p$ is equal to the true proposition $\text{True}$.

iff_true theorem

(p : Prop) : (p ↔ True) = p

Full source

@[simp] theorem iff_true (p : Prop) : (p ↔ True) = p := propext ⟨(·.2 trivial), fun h => ⟨fun _ => trivial, fun _ => h⟩⟩

Equivalence with True Simplifies to Proposition: $p \leftrightarrow \text{True} = p$

Informal description

For any proposition $p$, the equivalence $p \leftrightarrow \text{True}$ is logically equivalent to $p$ itself.

true_iff theorem

(p : Prop) : (True ↔ p) = p

Full source

@[simp] theorem true_iff (p : Prop) : (TrueTrue ↔ p) = p := propext ⟨(·.1 trivial), fun h => ⟨fun _ => h, fun _ => trivial⟩⟩

Equivalence of True with a Proposition is the Proposition Itself

Informal description

For any proposition $p$, the equivalence $(\text{True} \leftrightarrow p)$ is equal to $p$.

iff_false theorem

(p : Prop) : (p ↔ False) = ¬p

Full source

@[simp] theorem iff_false (p : Prop) : (p ↔ False) = ¬p := propext ⟨(·.1), (⟨·, False.elim⟩)⟩

Equivalence with False is Negation

Informal description

For any proposition $p$, the equivalence $p \leftrightarrow \text{False}$ holds if and only if $\neg p$ holds.

false_iff theorem

(p : Prop) : (False ↔ p) = ¬p

Full source

@[simp] theorem false_iff (p : Prop) : (FalseFalse ↔ p) = ¬p := propext ⟨(·.2), (⟨False.elim, ·⟩)⟩

Equivalence of False with a Proposition is Negation

Informal description

For any proposition $p$, the equivalence $(\text{False} \leftrightarrow p)$ is equal to $\neg p$.

false_implies theorem

(p : Prop) : (False → p) = True

Full source

@[simp] theorem false_implies (p : Prop) : (False → p) = True := eq_true False.elim

Implication from False is Always True

Informal description

For any proposition $p$, the implication $\text{False} \to p$ is equivalent to $\text{True}$.

forall_false theorem

(p : False → Prop) : (∀ h : False, p h) = True

Full source

@[simp] theorem forall_false (p : False → Prop) : (∀ h : False, p h) = True := eq_true (False.elim ·)

Universal Quantification over False is True

Informal description

For any proposition $p$ depending on a false hypothesis $h$, the universal quantification $\forall h : \text{False}, p(h)$ is equivalent to $\text{True}$.

implies_true theorem

(α : Sort u) : (α → True) = True

Full source

@[simp] theorem implies_true (α : Sort u) : (α → True) = True := eq_true fun _ => trivial

Implication to True is Trivial

Informal description

For any type $\alpha$, the implication $\alpha \to \text{True}$ is equivalent to $\text{True}$.

true_implies theorem

(p : Prop) : (True → p) = p

Full source

@[simp] theorem true_implies (p : Prop) : (True → p) = p := propext ⟨(· trivial), (fun _ => ·)⟩

Implication from True is Equivalent to Proposition

Informal description

For any proposition $p$, the implication $\text{True} \to p$ is equivalent to $p$.

not_false_eq_true theorem

: (¬False) = True

Full source

@[simp] theorem not_false_eq_true : (¬ False) = True := eq_true False.elim

Negation of False is True ($\neg \text{False} = \text{True}$)

Informal description

The negation of the false proposition is equivalent to the true proposition, i.e., $\neg \text{False} = \text{True}$.

not_true_eq_false theorem

: (¬True) = False

Full source

@[simp] theorem not_true_eq_false : (¬ True) = False := by decide

Negation of True is False

Informal description

The negation of the true proposition is equal to the false proposition, i.e., $\neg\text{True} = \text{False}$.

not_iff_self theorem

: ¬(¬a ↔ a)

Full source

@[simp] theorem not_iff_self : ¬(¬a ↔ a) | H => iff_not_self H.symm

Negation is Not Equivalent to Itself

Informal description

For any proposition $a$, it is not the case that the negation of $a$ is equivalent to $a$ itself, i.e., $\neg(\neg a \leftrightarrow a)$.

and_congr_right theorem

(h : a → (b ↔ c)) : a ∧ b ↔ a ∧ c

Full source

theorem and_congr_right (h : a → (b ↔ c)) : a ∧ ba ∧ b ↔ a ∧ c :=
  Iff.intro (fun ⟨ha, hb⟩ => And.intro ha ((h ha).mp hb))
            (fun ⟨ha, hb⟩ => And.intro ha ((h ha).mpr hb))

Right Conjunction Equivalence under Implication

Informal description

For any propositions $a$, $b$, and $c$, if $a$ implies that $b$ is equivalent to $c$, then the conjunction $a \land b$ is equivalent to $a \land c$.

and_congr_left theorem

(h : c → (a ↔ b)) : a ∧ c ↔ b ∧ c

Full source

theorem and_congr_left (h : c → (a ↔ b)) : a ∧ ca ∧ c ↔ b ∧ c :=
  Iff.trans and_comm (Iff.trans (and_congr_right h) and_comm)

Left Conjunction Equivalence under Implication: $a \land c \leftrightarrow b \land c$

Informal description

For any propositions $a$, $b$, and $c$, if $c$ implies that $a$ is equivalent to $b$, then the conjunction $a \land c$ is equivalent to $b \land c$.

and_assoc theorem

: (a ∧ b) ∧ c ↔ a ∧ (b ∧ c)

Full source

theorem and_assoc : (a ∧ b) ∧ c(a ∧ b) ∧ c ↔ a ∧ (b ∧ c) :=
  Iff.intro (fun ⟨⟨ha, hb⟩, hc⟩ => ⟨ha, hb, hc⟩)
            (fun ⟨ha, hb, hc⟩ => ⟨⟨ha, hb⟩, hc⟩)

Associativity of Logical Conjunction: $(a \land b) \land c \leftrightarrow a \land (b \land c)$

Informal description

For any propositions $a$, $b$, and $c$, the conjunction $(a \land b) \land c$ is equivalent to $a \land (b \land c)$.

instAssociativeAnd instance

: Std.Associative And

Full source

instance : Std.Associative And := ⟨fun _ _ _ => propext and_assoc⟩

Associativity of Logical Conjunction

Informal description

The logical conjunction operation $\land$ is associative.

and_self_left theorem

: a ∧ (a ∧ b) ↔ a ∧ b

Full source

@[simp] theorem and_self_left  : a ∧ (a ∧ b)a ∧ (a ∧ b) ↔ a ∧ b := by rw [←propext and_assoc, and_self]

Left Idempotence of Conjunction: $a \land (a \land b) \leftrightarrow a \land b$

Informal description

For any propositions $a$ and $b$, the conjunction $a \land (a \land b)$ is equivalent to $a \land b$.

and_self_right theorem

: (a ∧ b) ∧ b ↔ a ∧ b

Full source

@[simp] theorem and_self_right : (a ∧ b) ∧ b(a ∧ b) ∧ b ↔ a ∧ b := by rw [ propext and_assoc, and_self]

Right Idempotence of Conjunction: $(a \land b) \land b \leftrightarrow a \land b$

Informal description

For any propositions $a$ and $b$, the conjunction $(a \land b) \land b$ is equivalent to $a \land b$.

and_congr_right_iff theorem

: (a ∧ b ↔ a ∧ c) ↔ (a → (b ↔ c))

Full source

@[simp] theorem and_congr_right_iff : (a ∧ b ↔ a ∧ c) ↔ (a → (b ↔ c)) :=
  Iff.intro (fun h ha => by simp [ha] at h; exact h) and_congr_right

Equivalence of Right Conjunction under Implication: $(a \land b \leftrightarrow a \land c) \leftrightarrow (a \to (b \leftrightarrow c))$

Informal description

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

and_congr_left_iff theorem

: (a ∧ c ↔ b ∧ c) ↔ c → (a ↔ b)

Full source

@[simp] theorem and_congr_left_iff : (a ∧ c ↔ b ∧ c) ↔ c → (a ↔ b) := by
  rw [@and_comm _ c, @and_comm _ c, ← and_congr_right_iff]

Equivalence of Left Conjunction under Implication: $(a \land c \leftrightarrow b \land c) \leftrightarrow (c \to (a \leftrightarrow b))$

Informal description

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

and_iff_left_of_imp theorem

(h : a → b) : (a ∧ b) ↔ a

Full source

theorem and_iff_left_of_imp  (h : a → b) : (a ∧ b) ↔ a := Iff.intro And.left (fun ha => And.intro ha (h ha))

Conjunction Equivalence under Implication: $(a \land b) \leftrightarrow a$ when $a \to b$

Informal description

For any propositions $a$ and $b$, if $a$ implies $b$ (i.e., $a \to b$), then the conjunction $a \land b$ is equivalent to $a$ (i.e., $a \land b \leftrightarrow a$).

and_iff_right_of_imp theorem

(h : b → a) : (a ∧ b) ↔ b

Full source

theorem and_iff_right_of_imp (h : b → a) : (a ∧ b) ↔ b := Iff.trans And.comm (and_iff_left_of_imp h)

Conjunction Equivalence under Implication: $(a \land b) \leftrightarrow b$ when $b \to a$

Informal description

For any propositions $a$ and $b$, if $b$ implies $a$ (i.e., $b \to a$), then the conjunction $a \land b$ is equivalent to $b$ (i.e., $a \land b \leftrightarrow b$).

and_iff_left_iff_imp theorem

: ((a ∧ b) ↔ a) ↔ (a → b)

Full source

@[simp] theorem and_iff_left_iff_imp  : ((a ∧ b) ↔ a) ↔ (a → b) := Iff.intro (And.rightAnd.right ∘ ·.mpr) and_iff_left_of_imp

Equivalence of Conjunction and Implication: $(a \land b \leftrightarrow a) \leftrightarrow (a \to b)$

Informal description

For any propositions $a$ and $b$, the equivalence $(a \land b) \leftrightarrow a$ holds if and only if $a$ implies $b$ (i.e., $a \to b$).

and_iff_right_iff_imp theorem

: ((a ∧ b) ↔ b) ↔ (b → a)

Full source

@[simp] theorem and_iff_right_iff_imp : ((a ∧ b) ↔ b) ↔ (b → a) := Iff.intro (And.leftAnd.left ∘ ·.mpr) and_iff_right_of_imp

Conjunction-Implication Equivalence: $(a \land b \leftrightarrow b) \leftrightarrow (b \to a)$

Informal description

For any propositions $a$ and $b$, the equivalence $(a \land b) \leftrightarrow b$ holds if and only if $b$ implies $a$ (i.e., $b \to a$).

iff_self_and theorem

: (p ↔ p ∧ q) ↔ (p → q)

Full source

@[simp] theorem iff_self_and : (p ↔ p ∧ q) ↔ (p → q) := by rw [@Iff.comm p, and_iff_left_iff_imp]

Equivalence of Proposition and Conjunction Implies Implication: $(p \leftrightarrow p \land q) \leftrightarrow (p \to q)$

Informal description

For any propositions $p$ and $q$, the equivalence $p \leftrightarrow (p \land q)$ holds if and only if $p$ implies $q$ (i.e., $p \to q$).

iff_and_self theorem

: (p ↔ q ∧ p) ↔ (p → q)

Full source

@[simp] theorem iff_and_self : (p ↔ q ∧ p) ↔ (p → q) := by rw [and_comm, iff_self_and]

Equivalence of Proposition and Conjunction Implies Implication: $(p \leftrightarrow q \land p) \leftrightarrow (p \to q)$

Informal description

For any propositions $p$ and $q$, the equivalence $p \leftrightarrow (q \land p)$ holds if and only if $p$ implies $q$ (i.e., $p \to q$).

Or.imp theorem

(f : a → c) (g : b → d) (h : a ∨ b) : c ∨ d

Full source

theorem Or.imp (f : a → c) (g : b → d) (h : a ∨ b) : c ∨ d := h.elim (inlinl ∘ f) (inrinr ∘ g)

Implication Preserves Disjunction

Informal description

For any functions $f : a \to c$ and $g : b \to d$, and any proposition $h : a \lor b$, the proposition $c \lor d$ holds.

Or.imp_left theorem

(f : a → b) : a ∨ c → b ∨ c

Full source

theorem Or.imp_left (f : a → b) : a ∨ c → b ∨ c := .imp f id

Left Implication Preserves Disjunction

Informal description

For any function $f : a \to b$ and any proposition $a \lor c$, the proposition $b \lor c$ holds.

Or.imp_right theorem

(f : b → c) : a ∨ b → a ∨ c

Full source

theorem Or.imp_right (f : b → c) : a ∨ b → a ∨ c := .imp id f

Right Implication Preserves Disjunction

Informal description

For any function $f : b \to c$ and any proposition $a \lor b$, the proposition $a \lor c$ holds.

or_assoc theorem

: (a ∨ b) ∨ c ↔ a ∨ (b ∨ c)

Full source

theorem or_assoc : (a ∨ b) ∨ c(a ∨ b) ∨ c ↔ a ∨ (b ∨ c) :=
  Iff.intro (.rec (.imp_right .inl) (.inr.inr ∘ .inr))
            (.rec (.inl.inl ∘ .inl) (.imp_left .inr))

Associativity of Disjunction: $(a \lor b) \lor c \leftrightarrow a \lor (b \lor c)$

Informal description

For any propositions $a$, $b$, and $c$, the disjunction $(a \lor b) \lor c$ is equivalent to $a \lor (b \lor c)$.

instAssociativeOr instance

: Std.Associative Or

Full source

instance : Std.Associative Or := ⟨fun _ _ _ => propext or_assoc⟩

Associativity of Logical Disjunction

Informal description

The logical disjunction operation $\lor$ is associative.

or_self_left theorem

: a ∨ (a ∨ b) ↔ a ∨ b

Full source

@[simp] theorem or_self_left  : a ∨ (a ∨ b)a ∨ (a ∨ b) ↔ a ∨ b := by rw [←propext or_assoc, or_self]

Left Idempotence of Disjunction: $a \lor (a \lor b) \leftrightarrow a \lor b$

Informal description

For any propositions $a$ and $b$, the disjunction $a \lor (a \lor b)$ is equivalent to $a \lor b$.

or_self_right theorem

: (a ∨ b) ∨ b ↔ a ∨ b

Full source

@[simp] theorem or_self_right : (a ∨ b) ∨ b(a ∨ b) ∨ b ↔ a ∨ b := by rw [ propext or_assoc, or_self]

Right Idempotence of Disjunction: $(a \lor b) \lor b \leftrightarrow a \lor b$

Informal description

For any propositions $a$ and $b$, the disjunction $(a \lor b) \lor b$ is equivalent to $a \lor b$.

or_iff_right_of_imp theorem

(ha : a → b) : (a ∨ b) ↔ b

Full source

theorem or_iff_right_of_imp (ha : a → b) : (a ∨ b) ↔ b := Iff.intro (Or.rec ha id) .inr

Disjunction Equivalence Under Implication: $a \lor b \leftrightarrow b$ when $a \to b$

Informal description

For any propositions $a$ and $b$, if $a$ implies $b$ (i.e., $a \to b$), then the disjunction $a \lor b$ is equivalent to $b$ (i.e., $a \lor b \leftrightarrow b$).

or_iff_left_of_imp theorem

(hb : b → a) : (a ∨ b) ↔ a

Full source

theorem or_iff_left_of_imp  (hb : b → a) : (a ∨ b) ↔ a  := Iff.intro (Or.rec id hb) .inl

Disjunction Equivalence under Implication: $a \lor b \leftrightarrow a$ when $b \to a$

Informal description

For any propositions $a$ and $b$, if $b$ implies $a$ (i.e., $b \to a$), then the disjunction $a \lor b$ is equivalent to $a$ (i.e., $a \lor b \leftrightarrow a$).

or_iff_left_iff_imp theorem

: (a ∨ b ↔ a) ↔ (b → a)

Full source

@[simp] theorem or_iff_left_iff_imp  : (a ∨ b ↔ a) ↔ (b → a) := Iff.intro (·.mp ∘ Or.inr) or_iff_left_of_imp

Equivalence of Disjunction and Left Operand: $a \lor b \leftrightarrow a$ iff $b \to a$

Informal description

For any propositions $a$ and $b$, the equivalence $(a \lor b \leftrightarrow a)$ holds if and only if $b$ implies $a$ (i.e., $b \to a$).

or_iff_right_iff_imp theorem

: (a ∨ b ↔ b) ↔ (a → b)

Full source

@[simp] theorem or_iff_right_iff_imp : (a ∨ b ↔ b) ↔ (a → b) := by rw [or_comm, or_iff_left_iff_imp]

Equivalence of Disjunction and Right Operand: $a \lor b \leftrightarrow b$ iff $a \to b$

Informal description

For any propositions $a$ and $b$, the equivalence $(a \lor b \leftrightarrow b)$ holds if and only if $a$ implies $b$ (i.e., $a \to b$).

iff_self_or theorem

{a b : Prop} : (a ↔ a ∨ b) ↔ (b → a)

Full source

@[simp] theorem iff_self_or {a b : Prop} : (a ↔ a ∨ b) ↔ (b → a) :=
  propext (@Iff.comm _ a) ▸ @or_iff_left_iff_imp a b

Equivalence of Proposition and Its Disjunction: $a \leftrightarrow a \lor b$ iff $b \to a$

Informal description

For any propositions $a$ and $b$, the equivalence $(a \leftrightarrow a \lor b)$ holds if and only if $b$ implies $a$ (i.e., $b \to a$).

iff_or_self theorem

{a b : Prop} : (b ↔ a ∨ b) ↔ (a → b)

Full source

@[simp] theorem iff_or_self {a b : Prop} : (b ↔ a ∨ b) ↔ (a → b) :=
  propext (@Iff.comm _ b) ▸ @or_iff_right_iff_imp a b

Equivalence of Proposition and Its Disjunction with Another: $b \leftrightarrow a \lor b$ iff $a \to b$

Informal description

For any propositions $a$ and $b$, the equivalence $(b \leftrightarrow a \lor b)$ holds if and only if $a$ implies $b$ (i.e., $a \to b$).

Bool.or_false theorem

(b : Bool) : (b || false) = b

Full source

@[simp] theorem Bool.or_false (b : Bool) : (b || false) = b  := by cases b <;> rfl

Disjunction with False: $b \lor \text{false} = b$

Informal description

For any boolean value $b$, the disjunction of $b$ with `false` is equal to $b$, i.e., $b \lor \text{false} = b$.

Bool.or_true theorem

(b : Bool) : (b || true) = true

Full source

@[simp] theorem Bool.or_true (b : Bool) : (b || true) = true := by cases b <;> rfl

Boolean Disjunction with True Yields True

Informal description

For any boolean value $b$, the logical disjunction $b \lor \text{true}$ evaluates to $\text{true}$.

Bool.false_or theorem

(b : Bool) : (false || b) = b

Full source

@[simp] theorem Bool.false_or (b : Bool) : (falsefalse || b) = b  := by cases b <;> rfl

False OR $b$ equals $b$

Informal description

For any boolean value $b$, the expression $\mathrm{false} \lor b$ evaluates to $b$.

instLawfulIdentityBoolOrFalse instance

: Std.LawfulIdentity (· || ·) false

Full source

instance : Std.LawfulIdentity (· || ·) false where
  left_id := Bool.false_or
  right_id := Bool.or_false

`false` is the Identity Element for Boolean OR

Informal description

The boolean operation `OR` with `false` as its identity element is a lawful identity operation. That is, for any boolean value $b$, we have $b \lor \text{false} = b$ and $\text{false} \lor b = b$.

Bool.true_or theorem

(b : Bool) : (true || b) = true

Full source

@[simp] theorem Bool.true_or (b : Bool) : (truetrue || b) = true := by cases b <;> rfl

Disjunction with True: $\text{true} \lor b = \text{true}$

Informal description

For any boolean value $b$, the logical disjunction $\text{true} \lor b$ evaluates to $\text{true}$.

Bool.or_self theorem

(b : Bool) : (b || b) = b

Full source

@[simp] theorem Bool.or_self (b : Bool) : (b || b) = b       := by cases b <;> rfl

Idempotence of Logical Or: $b \lor b = b$

Informal description

For any boolean value $b$, the logical disjunction of $b$ with itself is equal to $b$, i.e., $b \lor b = b$.

instIdempotentOpBoolOr instance

: Std.IdempotentOp (· || ·)

Full source

instance : Std.IdempotentOp (· || ·) := ⟨Bool.or_self⟩

Idempotence of Boolean OR

Informal description

The logical OR operation `(· || ·)` on boolean values is idempotent.

Bool.or_eq_true theorem

(a b : Bool) : ((a || b) = true) = (a = true ∨ b = true)

Full source

@[simp] theorem Bool.or_eq_true (a b : Bool) : ((a || b) = true) = (a = true ∨ b = true) := by
  cases a <;> cases b <;> decide

Disjunction Equivalence: $a \lor b \leftrightarrow (a = \text{true} \lor b = \text{true})$

Informal description

For any boolean values $a$ and $b$, the disjunction $a \lor b$ evaluates to `true` if and only if either $a$ is `true` or $b$ is `true`.

Bool.and_false theorem

(b : Bool) : (b && false) = false

Full source

@[simp] theorem Bool.and_false (b : Bool) : (b && false) = false := by cases b <;> rfl

Boolean AND with False Yields False

Informal description

For any boolean value $b$, the logical AND of $b$ with `false` evaluates to `false`, i.e., $b \land \text{false} = \text{false}$.

Bool.and_true theorem

(b : Bool) : (b && true) = b

Full source

@[simp] theorem Bool.and_true (b : Bool) : (b && true) = b       := by cases b <;> rfl

Logical AND with True Preserves Boolean Value

Informal description

For any boolean value $b$, the logical AND of $b$ and $\texttt{true}$ is equal to $b$, i.e., $b \land \texttt{true} = b$.

Bool.false_and theorem

(b : Bool) : (false && b) = false

Full source

@[simp] theorem Bool.false_and (b : Bool) : (falsefalse && b) = false := by cases b <;> rfl

False AND Any Boolean is False

Informal description

For any boolean value $b$, the logical AND of `false` and $b$ evaluates to `false`, i.e., $\text{false} \land b = \text{false}$.

Bool.true_and theorem

(b : Bool) : (true && b) = b

Full source

@[simp] theorem Bool.true_and (b : Bool) : (truetrue && b) = b       := by cases b <;> rfl

Logical AND with True: $\text{true} \land b = b$

Informal description

For any boolean value $b$, the logical AND of `true` and $b$ is equal to $b$, i.e., $\text{true} \land b = b$.

instLawfulIdentityBoolAndTrue instance

: Std.LawfulIdentity (· && ·) true

Full source

instance : Std.LawfulIdentity (· && ·) true where
  left_id := Bool.true_and
  right_id := Bool.and_true

`AND` with `true` as Identity Element

Informal description

The boolean operation `AND` with `true` as the identity element satisfies the properties of a lawful identity. That is, for any boolean value $b$, we have $b \land \texttt{true} = b$ and $\texttt{true} \land b = b$.

Bool.and_self theorem

(b : Bool) : (b && b) = b

Full source

@[simp] theorem Bool.and_self (b : Bool) : (b && b) = b          := by cases b <;> rfl

Idempotence of Boolean Conjunction: $b \land b = b$

Informal description

For any boolean value $b$, the conjunction of $b$ with itself is equal to $b$, i.e., $b \land b = b$.

instIdempotentOpBoolAnd instance

: Std.IdempotentOp (· && ·)

Full source

instance : Std.IdempotentOp (· && ·) := ⟨Bool.and_self⟩

Idempotence of Boolean Conjunction

Informal description

The boolean conjunction operation `&&` is idempotent, meaning that for any boolean value $b$, applying the operation twice with the same argument yields the same result: $b \land b = b$.

Bool.and_eq_true theorem

(a b : Bool) : ((a && b) = true) = (a = true ∧ b = true)

Full source

@[simp] theorem Bool.and_eq_true (a b : Bool) : ((a && b) = true) = (a = true ∧ b = true) := by
  cases a <;> cases b <;> decide

Conjunction Equivalence: $(a \land b) = \text{true} \leftrightarrow (a = \text{true}) \land (b = \text{true})$

Informal description

For any boolean values $a$ and $b$, the conjunction $a \land b$ evaluates to `true` if and only if both $a$ and $b$ are `true`. In other words, $(a \land b) = \text{true} \leftrightarrow (a = \text{true}) \land (b = \text{true})$.

Bool.and_assoc theorem

(a b c : Bool) : (a && b && c) = (a && (b && c))

Full source

theorem Bool.and_assoc (a b c : Bool) : (a && ba && b && c) = (a && (b && c)) := by
  cases a <;> cases b <;> cases c <;> decide

Associativity of Boolean Conjunction: $a \land b \land c = a \land (b \land c)$

Informal description

For any boolean values $a$, $b$, and $c$, the conjunction $a \land b \land c$ is equal to $a \land (b \land c)$.

instAssociativeBoolAnd instance

: Std.Associative (· && ·)

Full source

instance : Std.Associative (· && ·) := ⟨Bool.and_assoc⟩

Associativity of Boolean Conjunction

Informal description

The boolean conjunction operation $\land$ is associative.

Bool.or_assoc theorem

(a b c : Bool) : (a || b || c) = (a || (b || c))

Full source

theorem Bool.or_assoc (a b c : Bool) : (a || ba || b || c) = (a || (b || c)) := by
  cases a <;> cases b <;> cases c <;> decide

Associativity of Boolean Disjunction

Informal description

For any boolean values $a$, $b$, and $c$, the disjunction operation satisfies the associativity property: $(a \lor b) \lor c = a \lor (b \lor c)$.

instAssociativeBoolOr instance

: Std.Associative (· || ·)

Full source

instance : Std.Associative (· || ·) := ⟨Bool.or_assoc⟩

Associativity of Boolean Disjunction

Informal description

The boolean disjunction operation $\lor$ is associative.

Bool.not_not theorem

(b : Bool) : (!!b) = b

Full source

@[simp] theorem Bool.not_not (b : Bool) : (!!b) = b := by cases b <;> rfl

Double Negation Identity for Booleans: $\neg(\neg b) = b$

Informal description

For any boolean value $b$, the double negation of $b$ is equal to $b$ itself, i.e., $\neg(\neg b) = b$.

Bool.not_true theorem

: (!true) = false

Full source

@[simp] theorem Bool.not_true  : (!true) = false := by decide

Negation of True is False

Informal description

The negation of the boolean value `true` is `false`, i.e., $\neg \text{true} = \text{false}$.

Bool.not_false theorem

: (!false) = true

Full source

@[simp] theorem Bool.not_false : (!false) = true := by decide

Negation of False is True

Informal description

The negation of the boolean value `false` is `true`, i.e., $\neg \text{false} = \text{true}$.

beq_true theorem

(b : Bool) : (b == true) = b

Full source

@[simp] theorem beq_true  (b : Bool) : (b == true)  =  b := by cases b <;> rfl

Boolean Equality with True: $(b == \texttt{true}) = b$

Informal description

For any boolean value $b$, the equality $(b == \texttt{true}) = b$ holds, where `==` denotes boolean equality.

beq_false theorem

(b : Bool) : (b == false) = !b

Full source

@[simp] theorem beq_false (b : Bool) : (b == false) = !b := by cases b <;> rfl

Boolean Equality with False is Negation

Informal description

For any boolean value $b$, the equality test $(b == \text{false})$ is equivalent to the negation of $b$, i.e., $(b == \text{false}) = \neg b$.

Bool.not_eq_eq_eq_not theorem

{a b : Bool} : ((!a) = b) ↔ (a = !b)

Full source

/--
We move `!` from the left hand side of an equality to the right hand side.
This helps confluence, and also helps combining pairs of `!`s.
-/
@[simp] theorem Bool.not_eq_eq_eq_not {a b : Bool} : ((!a) = b) ↔ (a = !b) := by
  cases a <;> cases b <;> simp

Negation Equality Swap: $\neg a = b \leftrightarrow a = \neg b$

Informal description

For any boolean values $a$ and $b$, the equality $\neg a = b$ holds if and only if $a = \neg b$.

Bool.not_eq_not theorem

{a b : Bool} : ¬a = !b ↔ a = b

Full source

@[simp] theorem Bool.not_eq_not {a b : Bool} : ¬a = !b¬a = !b ↔ a = b := by
  cases a <;> cases b <;> simp

Negation Preserves Boolean Equality: $\neg a = \neg b \leftrightarrow a = b$

Informal description

For any boolean values $a$ and $b$, the negation of $a$ is equal to the negation of $b$ if and only if $a$ is equal to $b$, i.e., $\neg a = \neg b \leftrightarrow a = b$.

Bool.not_not_eq theorem

{a b : Bool} : ¬(!a) = b ↔ a = b

Full source

theorem Bool.not_not_eq {a b : Bool} : ¬(!a) = b¬(!a) = b ↔ a = b := by simp

Negation of Boolean Equality: $\neg(\neg a = b) \leftrightarrow a = b$

Informal description

For any boolean values $a$ and $b$, the negation of the equality $\neg a = b$ is equivalent to $a = \neg b$.

Bool.not_eq_true' theorem

(b : Bool) : ((!b) = true) = (b = false)

Full source

theorem Bool.not_eq_true'  (b : Bool) : ((!b) = true) = (b = false) := by simp

Negation Equals True iff Boolean is False

Informal description

For any boolean value $b$, the negation of $b$ equals `true` if and only if $b$ equals `false`, i.e., $(\neg b = \texttt{true}) \leftrightarrow (b = \texttt{false})$.

Bool.not_eq_false' theorem

(b : Bool) : ((!b) = false) = (b = true)

Full source

theorem Bool.not_eq_false' (b : Bool) : ((!b) = false) = (b = true) := by simp

Negation Equals False iff Boolean is True

Informal description

For any boolean value $b$, the negation of $b$ equals `false` if and only if $b$ equals `true$, i.e., $\neg b = \text{false} \leftrightarrow b = \text{true}$.

Bool.not_eq_true theorem

(b : Bool) : (¬(b = true)) = (b = false)

Full source

@[simp] theorem Bool.not_eq_true (b : Bool) : (¬(b = true)) = (b = false) := by cases b <;> decide

Negation of Boolean Equality to True

Informal description

For any boolean value $b$, the statement $\neg(b = \texttt{true})$ is equivalent to $b = \texttt{false}$.

Bool.not_eq_false theorem

(b : Bool) : (¬(b = false)) = (b = true)

Full source

@[simp] theorem Bool.not_eq_false (b : Bool) : (¬(b = false)) = (b = true) := by cases b <;> decide

Negation of False Boolean Equals True

Informal description

For any boolean value $b$, the negation of $b$ being false is equivalent to $b$ being true, i.e., $\neg(b = \text{false}) \leftrightarrow (b = \text{true})$.

decide_eq_true_eq theorem

[Decidable p] : (decide p = true) = p

Full source

@[simp] theorem decide_eq_true_eq [Decidable p] : (decide p = true) = p :=
  propext <| Iff.intro of_decide_eq_true decide_eq_true

Decidable Proposition Decision Equivalence to True

Informal description

For any decidable proposition $p$, the statement that the decision procedure for $p$ returns `true` is equivalent to $p$ itself, i.e., $\text{decide}(p) = \texttt{true} \leftrightarrow p$.

decide_eq_false_iff_not theorem

{_ : Decidable p} : (decide p = false) ↔ ¬p

Full source

@[simp] theorem decide_eq_false_iff_not {_ : Decidable p} : (decide p = false) ↔ ¬p :=
  ⟨of_decide_eq_false, decide_eq_false⟩

Decision Procedure Yields False if and only if Proposition is False

Informal description

For any decidable proposition $p$, the decision procedure `decide p` returns `false` if and only if $p$ is false, i.e., $\text{decide}(p) = \text{false} \leftrightarrow \neg p$.

decide_not theorem

[g : Decidable p] [h : Decidable (Not p)] : decide (Not p) = !(decide p)

Full source

@[simp] theorem decide_not [g : Decidable p] [h : Decidable (Not p)] : decide (Not p) = !(decide p) := by
  cases g <;> (rename_i gp; simp [gp])

Decision Procedure for Negation Equals Negation of Decision Procedure

Informal description

For any decidable proposition $p$, the decision procedure for $\neg p$ is equal to the negation of the decision procedure for $p$, i.e., $\text{decide}(\neg p) = \neg \text{decide}(p)$.

not_decide_eq_true theorem

[h : Decidable p] : ((!decide p) = true) = ¬p

Full source

theorem not_decide_eq_true [h : Decidable p] : ((!decide p) = true) = ¬ p := by simp

Negation of Decision Equals True if and only if Proposition is False

Informal description

For any decidable proposition $p$, the negation of the decision procedure's result equals `true` if and only if $p$ is false, i.e., $\neg (\text{decide}(p)) = \text{true} \leftrightarrow \neg p$.

heq_eq_eq theorem

(a b : α) : HEq a b = (a = b)

Full source

@[simp] theorem heq_eq_eq (a b : α) : HEq a b = (a = b) := propext <| Iff.intro eq_of_heq heq_of_eq

Heterogeneous Equality Equals Homogeneous Equality

Informal description

For any two elements $a$ and $b$ of the same type $\alpha$, the heterogeneous equality $\text{HEq}\ a\ b$ is equivalent to the homogeneous equality $a = b$.

cond_true theorem

(a b : α) : cond true a b = a

Full source

@[simp] theorem cond_true (a b : α) : cond true a b = a := rfl

Conditional Evaluation with True Condition: $\mathrm{cond}(\mathrm{true}, a, b) = a$

Informal description

For any elements $a$ and $b$ of type $\alpha$, the conditional expression $\mathrm{cond}(\mathrm{true}, a, b)$ evaluates to $a$.

cond_false theorem

(a b : α) : cond false a b = b

Full source

@[simp] theorem cond_false (a b : α) : cond false a b = b := rfl

Conditional Evaluation for False: $\text{cond}(\text{false}, a, b) = b$

Informal description

For any elements $a$ and $b$ of type $\alpha$, the conditional expression `cond false a b` evaluates to $b$.

beq_self_eq_true theorem

[BEq α] [LawfulBEq α] (a : α) : (a == a) = true

Full source

@[simp] theorem beq_self_eq_true [BEq α] [LawfulBEq α] (a : α) : (a == a) = true := LawfulBEq.rfl

Reflexivity of Boolean Equality: $a == a = \text{true}$

Informal description

For any type $\alpha$ with a decidable equality relation (implementing `BEq` and `LawfulBEq` instances), and for any element $a \in \alpha$, the boolean equality check `a == a` evaluates to `true`.

beq_self_eq_true' theorem

[DecidableEq α] (a : α) : (a == a) = true

Full source

theorem beq_self_eq_true' [DecidableEq α] (a : α) : (a == a) = true := by simp

Reflexivity of Decidable Boolean Equality: $a == a = \text{true}$

Informal description

For any type $\alpha$ with a decidable equality relation and for any element $a \in \alpha$, the boolean equality check $a == a$ evaluates to $\text{true}$.

bne_self_eq_false theorem

[BEq α] [LawfulBEq α] (a : α) : (a != a) = false

Full source

@[simp] theorem bne_self_eq_false [BEq α] [LawfulBEq α] (a : α) : (a != a) = false := by simp [bne]

Irreflexivity of Boolean Inequality: $a \neq a = \text{false}$

Informal description

For any type $\alpha$ with a decidable equality relation (implementing `BEq` and `LawfulBEq` instances), and for any element $a \in \alpha$, the boolean inequality check `a != a` evaluates to `false`.

bne_self_eq_false' theorem

[DecidableEq α] (a : α) : (a != a) = false

Full source

theorem bne_self_eq_false' [DecidableEq α] (a : α) : (a != a) = false := by simp

Irreflexivity of Decidable Boolean Inequality: $a \neq a = \text{false}$

Informal description

For any type $\alpha$ with a decidable equality relation and for any element $a \in \alpha$, the boolean inequality check $a \neq a$ evaluates to $\text{false}$.

decide_False abbrev

Full source

@[deprecated decide_false (since := "2024-11-05")] abbrev decide_False := decide_false

Decidability of False Proposition

Informal description

The decision procedure for the proposition `False` evaluates to `false`.

decide_True abbrev

Full source

@[deprecated decide_true  (since := "2024-11-05")] abbrev decide_True  := decide_true

Decidability of True

Informal description

The proposition `True` is decidable and evaluates to `true`.

bne_iff_ne theorem

[BEq α] [LawfulBEq α] {a b : α} : a != b ↔ a ≠ b

Full source

@[simp] theorem bne_iff_ne [BEq α] [LawfulBEq α] {a b : α} : a != ba != b ↔ a ≠ b := by
  simp [bne]; rw [← beq_iff_eq (a := a) (b := b)]; simp [-beq_iff_eq]

Boolean Inequality Equivalent to Propositional Inequality

Informal description

For any type $\alpha$ with a decidable equality operation and lawful equality axioms, and for any elements $a, b \in \alpha$, the boolean inequality $a \neq b$ (written as `a != b`) holds if and only if $a$ is not equal to $b$ (i.e., $a \neq b$).

beq_eq_false_iff_ne theorem

[BEq α] [LawfulBEq α] {a b : α} : (a == b) = false ↔ a ≠ b

Full source

@[simp] theorem beq_eq_false_iff_ne [BEq α] [LawfulBEq α] {a b : α} : (a == b) = false ↔ a ≠ b := by
  rw [ne_eq, ← beq_iff_eq (a := a) (b := b)]
  cases a == b <;> decide

Boolean Equality Evaluates to False if and only if Elements are Not Equal

Informal description

For any type $\alpha$ with a decidable equality operation (`BEq α`) that satisfies the lawful equality axioms (`LawfulBEq α`), and for any elements $a, b \in \alpha$, the boolean equality `a == b` evaluates to `false` if and only if $a \neq b$.

bne_eq_false_iff_eq theorem

[BEq α] [LawfulBEq α] {a b : α} : (a != b) = false ↔ a = b

Full source

@[simp] theorem bne_eq_false_iff_eq [BEq α] [LawfulBEq α] {a b : α} : (a != b) = false ↔ a = b := by
  rw [bne, ← beq_iff_eq (a := a) (b := b)]
  cases a == b <;> decide

Boolean Inequality Evaluates to False if and only if Elements are Equal

Informal description

For any type $\alpha$ with a decidable equality operation (`BEq α`) that satisfies the lawful equality axioms (`LawfulBEq α`), and for any elements $a, b \in \alpha$, the boolean inequality `a != b` evaluates to `false` if and only if $a = b$.

Bool.beq_to_eq theorem

(a b : Bool) : (a == b) = (a = b)

Full source

theorem Bool.beq_to_eq (a b : Bool) : (a == b) = (a = b) := by simp

Boolean Equality Check Equals Propositional Equality

Informal description

For any boolean values $a$ and $b$, the boolean equality check `a == b` is equivalent to the propositional equality $a = b$.

Bool.not_beq_to_not_eq theorem

(a b : Bool) : (!(a == b)) = ¬(a = b)

Full source

theorem Bool.not_beq_to_not_eq (a b : Bool) : (!(a == b)) = ¬(a = b) := by simp

Negation of Boolean Equality Equals Logical Negation of Propositional Equality

Informal description

For any boolean values $a$ and $b$, the negation of their boolean equality `!(a == b)` is equal to the logical negation of their propositional equality $\neg(a = b)$.

Nat.le_zero_eq theorem

(a : Nat) : (a ≤ 0) = (a = 0)

Full source

@[simp] theorem Nat.le_zero_eq (a : Nat) : (a ≤ 0) = (a = 0) :=
  propext ⟨fun h => Nat.le_antisymm h (Nat.zero_le ..), fun h => by rw [h]; decide⟩

Natural Number Inequality to Zero: $a \leq 0 \leftrightarrow a = 0$

Informal description

For any natural number $a$, the inequality $a \leq 0$ holds if and only if $a = 0$.