doc-next-gen

Init.ByCases

Module docstring

{"# by_cases tactic and if-then-else support ","## if-then-else "}

if_true theorem
{_ : Decidable True} (t e : α) : ite True t e = t
Full source 
@[simp] theorem if_true {_ : Decidable True} (t e : α) : ite True t e = t := if_pos trivial
If-then-else with True Condition Always Takes First Branch
Informal description
For any type $\alpha$ and any terms $t, e : \alpha$, the if-then-else expression `if True then t else e` evaluates to $t$.
if_false theorem
{_ : Decidable False} (t e : α) : ite False t e = e
Full source 
@[simp] theorem if_false {_ : Decidable False} (t e : α) : ite False t e = e := if_neg id
Conditional Evaluation for False: `if False then t else e = e`
Informal description
For any type $\alpha$ and elements $t, e \in \alpha$, the conditional expression `if False then t else e` evaluates to $e$.
ite_id theorem
[Decidable c] {α} (t : α) : (if c then t else t) = t
Full source 
theorem ite_id [Decidable c] {α} (t : α) : (if c then t else t) = t := by split <;> rfl
Conditional with Identical Branches Reduces to Branch Value
Informal description
For any decidable proposition $c$ and any element $t$ of type $\alpha$, the conditional expression `if c then t else t` is equal to $t$.
apply_dite theorem
(f : α → β) (P : Prop) [Decidable P] (x : P → α) (y : ¬P → α) : f (dite P x y) = dite P (fun h => f (x h)) (fun h => f (y h))
Full source 
/-- A function applied to a `dite` is a `dite` of that function applied to each of the branches. -/
theorem apply_dite (f : α → β) (P : Prop) [Decidable P] (x : P → α) (y : ¬P → α) :
    f (dite P x y) = dite P (fun h => f (x h)) (fun h => f (y h)) := by
  by_cases h : P <;> simp [h]
Function Application Commutes with Dependent If-Then-Else: $f(\text{dite } P \text{ } x \text{ } y) = \text{dite } P \text{ } (f \circ x) \text{ } (f \circ y)$
Informal description
For any types $\alpha$ and $\beta$, function $f : \alpha \to \beta$, decidable proposition $P$, and functions $x : P \to \alpha$ and $y : \neg P \to \alpha$, the application of $f$ to a dependent if-then-else expression equals a dependent if-then-else expression where $f$ is applied to each branch. That is, $$f(\text{dite } P \text{ } x \text{ } y) = \text{dite } P \text{ } (\lambda h.\, f(x(h))) \text{ } (\lambda h.\, f(y(h))).$$
apply_ite theorem
(f : α → β) (P : Prop) [Decidable P] (x y : α) : f (ite P x y) = ite P (f x) (f y)
Full source 
/-- A function applied to a `ite` is a `ite` of that function applied to each of the branches. -/
theorem apply_ite (f : α → β) (P : Prop) [Decidable P] (x y : α) :
    f (ite P x y) = ite P (f x) (f y) :=
  apply_dite f P (fun _ => x) (fun _ => y)
Function Application Commutes with If-Then-Else: $f(\text{ite } P \text{ } x \text{ } y) = \text{ite } P \text{ } (f x) \text{ } (f y)$
Informal description
For any function $f : \alpha \to \beta$, decidable proposition $P$, and elements $x, y \in \alpha$, the application of $f$ to an if-then-else expression equals an if-then-else expression where $f$ is applied to each branch. That is, $$f(\text{if } P \text{ then } x \text{ else } y) = \text{if } P \text{ then } f(x) \text{ else } f(y).$$
dite_eq_ite theorem
[Decidable P] : (dite P (fun _ => a) (fun _ => b)) = ite P a b
Full source 
/-- A `dite` whose results do not actually depend on the condition may be reduced to an `ite`. -/
@[simp] theorem dite_eq_ite [Decidable P] :
  (dite P (fun _ => a) (fun _ => b)) = ite P a b := rfl
Equality of Dependent and Non-dependent If-then-else for Constant Branches
Informal description
For any decidable proposition $P$ and any elements $a, b$ of a type $\alpha$, the dependent if-then-else expression `dite P (fun _ => a) (fun _ => b)` is equal to the standard if-then-else expression `ite P a b`.
ite_some_none_eq_none theorem
[Decidable P] : (if P then some x else none) = none ↔ ¬P
Full source 
@[deprecated "Use `ite_eq_right_iff`" (since := "2024-09-18")]
theorem ite_some_none_eq_none [Decidable P] :
    (if P then some x else none) = none ↔ ¬ P := by
  simp only [ite_eq_right_iff, reduceCtorEq]
  rfl
Conditional Option Equals None if and only if Condition is False
Informal description
For any proposition $P$ with a `Decidable` instance, the conditional expression `if P then some x else none` equals `none` if and only if $P$ is false, i.e., $\neg P$ holds.
ite_some_none_eq_some theorem
[Decidable P] : (if P then some x else none) = some y ↔ P ∧ x = y
Full source 
@[deprecated "Use `Option.ite_none_right_eq_some`" (since := "2024-09-18")]
theorem ite_some_none_eq_some [Decidable P] :
    (if P then some x else none) = some y ↔ P ∧ x = y := by
  split <;> simp_all
Conditional Option Equals Some if and only if Condition Holds and Values Are Equal
Informal description
For any decidable proposition $P$ and elements $x, y$ of a type $\alpha$, the conditional expression `if P then some x else none` equals `some y` if and only if $P$ holds and $x = y$.
dite_some_none_eq_none theorem
[Decidable P] {x : P → α} : (if h : P then some (x h) else none) = none ↔ ¬P
Full source 
@[deprecated "Use `dite_eq_right_iff" (since := "2024-09-18")]
theorem dite_some_none_eq_none [Decidable P] {x : P → α} :
    (if h : P then some (x h) else none) = none ↔ ¬P := by
  simp
Dependent if-then-else yields `none` if and only if condition is false
Informal description
For any decidable proposition $P$ and any function $x : P \to \alpha$, the dependent if-then-else expression `(if h : P then some (x h) else none)` equals `none` if and only if $P$ is false, i.e., $\neg P$ holds.
dite_some_none_eq_some theorem
[Decidable P] {x : P → α} {y : α} : (if h : P then some (x h) else none) = some y ↔ ∃ h : P, x h = y
Full source 
@[deprecated "Use `Option.dite_none_right_eq_some`" (since := "2024-09-18")]
theorem dite_some_none_eq_some [Decidable P] {x : P → α} {y : α} :
    (if h : P then some (x h) else none) = some y ↔ ∃ h : P, x h = y := by
  by_cases h : P <;> simp [h]
Dependent If-Then-Else Yields `some y` if and only if Condition is True and $x(h) = y$
Informal description
For any decidable proposition $P$, any function $x : P \to \alpha$, and any element $y \in \alpha$, the dependent if-then-else expression `(if h : P then some (x h) else none)` equals `some y` if and only if there exists a proof $h$ of $P$ such that $x(h) = y$.