ite_eq_right_iff
theorem ite_eq_right_iff :
∀ {α : Sort u_1} {a b : α} {P : Prop} [inst : Decidable P], (if P then a else b) = b ↔ P → a = b
This theorem states that for any type `α`, any two values `a` and `b` of type `α`, and any proposition `P`, if `P` is decidable, then the conditional expression "if `P` then `a` else `b`" being equal to `b` is logically equivalent to stating that if `P` holds, then `a` equals `b`. In other words, if the result of the conditional expression is `b`, it either means that `P` is false, or `P` is true, but `a` equals `b`.
More concisely: For any type `α`, decidable proposition `P` over `α`, values `a`, `b` of type `α`, if `P` implies `a = b`, then the if-then-else expression "if `P` then `a` else `b`" equals `b`.
|
dite_eq_left_iff
theorem dite_eq_left_iff :
∀ {α : Sort u_1} {a : α} {P : Prop} [inst : Decidable P] {B : ¬P → α},
dite P (fun x => a) B = a ↔ ∀ (h : ¬P), B h = a
This theorem states that for any type `α`, any instance `a` of `α`, a Proposition `P` and a function `B` that maps `¬P` to `α` (where `P` is a decidable proposition), the expression `dite P (fun x => a) B` is equal to `a` if and only if for every instance `h` where `¬P` holds, `B h` is equal to `a`. In other words, this theorem relates the equality of a dependent if-then-else expression (`dite`) and a certain instance of the type, to the condition that a function applied to every instance of the negation of the proposition results in that same instance.
More concisely: For any type `α`, proposition `P`, instance `a` of `α`, and function `B` mapping `¬P` to `α`, `dite P (fun x => a) B` equals `a` if and only if for all `h` with `¬P h`, `B h` equals `a`.
|
apply_ite
theorem apply_ite :
∀ {α : Sort u_1} {β : Sort u_2} (f : α → β) (P : Prop) [inst : Decidable P] (x y : α),
f (if P then x else y) = if P then f x else f y
This theorem states that for any function `f` mapping from a sort `α` to a sort `β`, a proposition `P`, and two objects `x` and `y` of sort `α`, applying `f` to the result of an 'if-then-else' expression (where `P` is the condition, `x` is the result if `P` is true, and `y` is the result if `P` is false) is the same as constructing a new 'if-then-else' expression where `f` is applied to `x` if `P` is true, and `f` is applied to `y` if `P` is false. In other words, it is permissible to move a function application inside an 'if-then-else' expression. This theorem requires that `P` be decidable.
More concisely: For any decidable proposition P and functions f from sort α to sort β, the application of f to the result of an if-then-else expression (using P as the condition and x, y as the results for true and false, respectively) is equal to the if-then-else expression where f is applied to x if P holds, and f is applied to y otherwise.
|
apply_dite
theorem apply_dite :
∀ {α : Sort u_1} {β : Sort u_2} (f : α → β) (P : Prop) [inst : Decidable P] (x : P → α) (y : ¬P → α),
f (dite P x y) = if h : P then f (x h) else f (y h)
This theorem states that for any propositional function `P` and a function `f` from `α` to `β`, applying `f` to the result of `dite`, which chooses between two options depending on the truth or falsity of `P`, is the same as choosing between the applications of `f` to each option depending on the truth or falsity of `P`. This essentially means that `f` can be distributed over `dite`. If `P` is true, `f` is applied to `x(h)`; if `P` is false, `f` is applied to `y(h)`. Here, `h` is a proof of `P`'s truth or falsity, `x` is a function from `P` to `α`, and `y` is a function from ¬`P` to `α`.
More concisely: For any propositional function P and functions f from α to β, x from P to α, and y from ¬P to α, the application of f to dite (P x) (h) is equivalent to dite (P h) (x h) (y h).
|
if_true
theorem if_true : ∀ {α : Sort u_1} {x : Decidable True} (t e : α), (if True then t else e) = t
This theorem, `if_true`, states that for any type `α` and any two elements `t` and `e` of that type, the result of an `if` expression that is always `True` is equal to `t`. In other words, given a decision on the truth value (`True` in this case), the ternary `if` expression will always yield the `then` branch, regardless of what the `else` branch contains.
More concisely: For any type `α` and elements `t, e : α`, if `if h : True then t else e` is well-defined, then `if h then t else e = t`.
|
dite_eq_right_iff
theorem dite_eq_right_iff :
∀ {α : Sort u_1} {b : α} {P : Prop} [inst : Decidable P] {A : P → α},
(dite P A fun x => b) = b ↔ ∀ (h : P), A h = b
The theorem `dite_eq_right_iff` states that for any type `α`, element `b` of type `α`, proposition `P`, and function `A` from `P` to `α`, the expression `(dite P A fun x => b)` equals `b` if and only if for all proofs `h` of `P`, `A h` equals `b`. Here `dite` is a construct that, given a proposition `P`, a function `A` from `P` to `α`, and a default value `b`, selects `A h` if `P` is true for some `h`, and `b` otherwise. This theorem is about the equality relationship between the `dite` construct and its default value.
More concisely: For any type α, proposition P, element b of α, and function A from P to α, the expression (dite P A b) equals b if and only if for all h proving P, Ah equals b.
|
ite_eq_left_iff
theorem ite_eq_left_iff :
∀ {α : Sort u_1} {a b : α} {P : Prop} [inst : Decidable P], (if P then a else b) = a ↔ ¬P → b = a
This theorem, `ite_eq_left_iff`, states that for any type `α`, any two values `a` and `b` of that type, and any proposition `P`, given that `P` is decidable, `(if P then a else b) = a` if and only if `¬P` implies that `b = a`. In simpler terms, it's stating that if deciding `P` results in `a`, then it's equivalent to saying that if `P` is not true, then `b` must be equal to `a`.
More concisely: For any type `α`, proposition `P` decidable over it, values `a, b : α`, if and only if `(if P then a else b) = a` is equivalent to `¬P → b = a`.
|
dite_eq_ite
theorem dite_eq_ite :
∀ {P : Prop} {α : Sort u_1} {a b : α} [inst : Decidable P], (if x : P then a else b) = if P then a else b := by
sorry
This theorem states that for any proposition `P` and any type `α`, if we have two values `a` and `b` of type `α` and a decidable instance for `P`, then an expression with a dependent if-then-else (`dite`) where the result does not actually depend on the proof of `P` can be simplified to a regular if-then-else (`ite`). In other words, even if you initially wrote something that depends on proving `P`, if the end results `a` and `b` don't actually involve that proof, then you can simplify the expression by removing the dependency on the proof.
More concisely: Given a decidable proposition `P` and values `a` and `b` of type `α`, if the expression `dite P a b` does not depend on the proof of `P`, then it can be simplified to `ite (decide P) a b`.
|
if_false
theorem if_false : ∀ {α : Sort u_1} {x : Decidable False} (t e : α), (if False then t else e) = e
This theorem states that for any type `α` and any two instances `t` and `e` of `α`, the result of the conditional expression "if False then `t` else `e`" is always `e`. It doesn't matter how we decide on "False," because the "if" part of the conditional is never true by definition, so we always get the "else" part.
More concisely: For all types `α` and instances `t` and `e` of `α`, the conditional expression `if False then t else e` equals `e`.
|