Module docstring
{"Remark: land/lor can be defined without using (% n), but we are trying to minimize the number of Nat theorems needed to bootstrap Lean. "}
Fin.coeToNat
instance
: CoeOut (Fin n) Nat
Full source
instance coeToNat : CoeOut (Fin n) Nat :=
⟨fun v => v.val⟩Informal description
For any natural number $n$, there is a canonical way to view an element of $\text{Fin}\ n$ (the type of natural numbers less than $n$) as a natural number.
Fin.elim0
definition
{α : Sort u} : Fin 0 → α
Full source
/--
The type `Fin 0` is uninhabited, so it can be used to derive any result whatsoever.
This is similar to `Empty.elim`. It can be thought of as a compiler-checked assertion that a code
path is unreachable, or a logical contradiction from which `False` and thus anything else could be
derived.
-/
def elim0.{u} {α : Sort u} : Fin 0 → α
| ⟨_, h⟩ => absurd h (not_lt_zero _)Informal description
Given any type $\alpha$, the function maps any element of $\text{Fin}\ 0$ (the empty type of natural numbers less than 0) to a term of type $\alpha$. This serves as a compiler-checked assertion that the code path is unreachable, since $\text{Fin}\ 0$ is uninhabited.
Fin.succ
definition
: Fin n → Fin (n + 1)
Informal description
The successor function on `Fin n` maps an element `⟨i, h⟩` of `Fin n` (where `i` is a natural number less than `n`) to `⟨i + 1, Nat.succ_lt_succ h⟩` in `Fin (n + 1)`. Unlike adding 1 modulo `n`, this operation increases the bound by 1, ensuring the result remains within the new bound.
**Examples:**
- `(2 : Fin 3).succ = (3 : Fin 4)`
- `(2 : Fin 3) + 1 = (0 : Fin 3)` (wraps around)
Fin.ofNat'
definition
(n : Nat) [NeZero n] (a : Nat) : Fin n
Informal description
Given a natural number `n` (with `n ≠ 0`) and another natural number `a`, the function returns `a` modulo `n` as an element of the finite type `Fin n` (natural numbers less than `n`).
Fin.ofNat
definition
{n : Nat} (a : Nat) : Fin (n + 1)
Full source
/--
Returns `a` modulo `n + 1` as a `Fin n.succ`.
-/
@[deprecated Fin.ofNat' (since := "2024-11-27")]
protected def ofNat {n : Nat} (a : Nat) : Fin (n + 1) :=
⟨a % (n+1), Nat.mod_lt _ (Nat.zero_lt_succ _)⟩Informal description
Given a natural number $a$ and a natural number $n$, the function returns $a$ modulo $n + 1$ as an element of the finite type `Fin (n + 1)` (natural numbers less than $n + 1$).
Fin.toNat
definition
(i : Fin n) : Nat
Informal description
The function extracts the underlying natural number from a term of type `Fin n`, which represents natural numbers less than `n`. This is equivalent to the coercion from `Fin n` to `Nat`.
Fin.toNat_eq_val
theorem
{i : Fin n} : i.toNat = i.val
Full source
@[simp] theorem toNat_eq_val {i : Fin n} : i.toNat = i.val := rflInformal description
For any element $i$ of the finite type `Fin n`, the natural number value obtained by applying the `toNat` function to $i$ is equal to the underlying value $i.val$ of $i$.
Fin.add
definition
: Fin n → Fin n → Fin n
Informal description
The addition operation on `Fin n` (natural numbers modulo `n`) is defined by adding the underlying natural numbers and taking the result modulo `n`. Specifically, for two elements `⟨a, h⟩` and `⟨b, _⟩` of `Fin n`, their sum is `⟨(a + b) % n, mlt h⟩`, where `mlt h` ensures the result is less than `n`.
Fin.mul
definition
: Fin n → Fin n → Fin n
Full source
/--
Multiplication modulo `n`, usually invoked via the `*` operator.
Examples:
* `(2 : Fin 10) * (2 : Fin 10) = (4 : Fin 10)`
* `(2 : Fin 10) * (7 : Fin 10) = (4 : Fin 10)`
* `(3 : Fin 10) * (7 : Fin 10) = (1 : Fin 10)`
-/
protected def mul : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(a * b) % n, mlt h⟩Informal description
The multiplication operation on `Fin n` (natural numbers modulo `n`) is defined by multiplying the underlying natural numbers and taking the result modulo `n`. Specifically, for two elements $\langle a, h_a \rangle$ and $\langle b, h_b \rangle$ of `Fin n`, their product is $\langle (a * b) \mod n, h \rangle$, where $h$ ensures the result is less than $n$.
Fin.sub
definition
: Fin n → Fin n → Fin n
Full source
/--
Subtraction modulo `n`, usually invoked via the `-` operator.
Examples:
* `(5 : Fin 11) - (3 : Fin 11) = (2 : Fin 11)`
* `(3 : Fin 11) - (5 : Fin 11) = (9 : Fin 11)`
-/
protected def sub : Fin n → Fin n → Fin n
/-
The definition of `Fin.sub` has been updated to improve performance.
The right-hand-side of the following `match` was originally
```
⟨(a + (n - b)) % n, mlt h⟩
```
This caused significant performance issues when testing definitional equality,
such as `x =?= x - 1` where `x : Fin n` and `n` is a big number,
as Lean spent a long time reducing
```
((n - 1) + x.val) % n
```
For example, this was an issue for `Fin 2^64` (i.e., `UInt64`).
This change improves performance by leveraging the fact that `Nat.add` is defined
using recursion on the second argument.
See issue #4413.
-/
| ⟨a, h⟩, ⟨b, _⟩ => ⟨((n - b) + a) % n, mlt h⟩Informal description
Given two elements $\langle a, h_a \rangle$ and $\langle b, h_b \rangle$ of `Fin n` (where $a, b < n$), their subtraction is defined as $\langle ((n - b) + a) \mod n, h \rangle$, where $h$ ensures the result is less than $n$. This operation effectively computes $a - b \mod n$, handling wraparound when $b > a$.
Fin.mod
definition
: Fin n → Fin n → Fin n
Informal description
The modulus operation for bounded natural numbers in `Fin n` takes two elements `⟨a, h₁⟩` and `⟨b, h₂⟩` (where `a` and `b` are natural numbers less than `n`) and returns `⟨a % b, h₃⟩`, where `a % b` is the modulus of `a` by `b` as natural numbers, and `h₃` is a proof that `a % b < n`. This operation is equivalent to the `%` operator on `Nat`, but ensures the result remains within the bounds of `Fin n`.
Fin.div
definition
: Fin n → Fin n → Fin n
Full source
/--
Division of bounded numbers, usually invoked via the `/` operator.
The resulting value is that computed by the `/` operator on `Nat`. In particular, the result of
division by `0` is `0`.
Examples:
* `(5 : Fin 10) / (2 : Fin 10) = (2 : Fin 10)`
* `(5 : Fin 10) / (0 : Fin 10) = (0 : Fin 10)`
* `(5 : Fin 10) / (7 : Fin 10) = (0 : Fin 10)`
-/
protected def div : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨a / b, Nat.lt_of_le_of_lt (Nat.div_le_self _ _) h⟩Informal description
The division operation on `Fin n` (natural numbers less than `n`) is defined such that for any two elements `⟨a, h⟩` and `⟨b, _⟩` in `Fin n`, their division is `⟨a / b, _⟩`, where `a / b` is the natural number division of `a` by `b`. The result is guaranteed to be less than `n` due to the property that `a / b ≤ a`, and `a < n`. Division by zero yields zero.
Fin.modn
definition
: Fin n → Nat → Fin n
Informal description
The function `Fin.modn` takes a bounded natural number `⟨a, h⟩` in `Fin n` (where `a` is a natural number less than `n`) and a natural number `m`, and returns the bounded natural number `⟨a % m, h'⟩` in `Fin n`, where `a % m` is the modulus of `a` by `m` and `h'` is a proof that `a % m < n`. This operation computes the modulus while preserving the boundedness property.
Fin.land
definition
: Fin n → Fin n → Fin n
Informal description
The function takes two elements of `Fin n` (natural numbers less than `n`) and returns their bitwise AND operation, taken modulo `n`. Specifically, for `⟨a, h⟩` and `⟨b, _⟩` in `Fin n`, it returns `⟨(a AND b) % n, _⟩`, where `a AND b` is the bitwise AND of `a` and `b`, and the result is reduced modulo `n` to ensure it remains within bounds.
Fin.lor
definition
: Fin n → Fin n → Fin n
Informal description
The function takes two elements of `Fin n` (natural numbers less than `n`) and returns their bitwise OR, modulo `n`.
Fin.xor
definition
: Fin n → Fin n → Fin n
Informal description
The bitwise XOR (exclusive or) operation on two elements of `Fin n`, which are natural numbers less than `n`. Given two elements `⟨a, h⟩` and `⟨b, _⟩` of `Fin n`, the result is the natural number `(a XOR b) % n`, where `XOR` is the bitwise XOR operation on natural numbers, and the result is taken modulo `n` to ensure it remains within the bounds of `Fin n`.
Fin.shiftLeft
definition
: Fin n → Fin n → Fin n
Full source
/--
Bitwise left shift of bounded numbers, with wraparound on overflow.
Examples:
* `(1 : Fin 10) <<< (1 : Fin 10) = (2 : Fin 10)`
* `(1 : Fin 10) <<< (3 : Fin 10) = (8 : Fin 10)`
* `(1 : Fin 10) <<< (4 : Fin 10) = (6 : Fin 10)`
-/
def shiftLeft : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(a <<< b) % n, mlt h⟩Informal description
The function takes two elements of `Fin n` (natural numbers less than `n`) and returns the result of left-shifting the first element by the number of bits specified by the second element, modulo `n`. This operation wraps around on overflow, ensuring the result remains within the bounds of `Fin n`.
Fin.shiftRight
definition
: Fin n → Fin n → Fin n
Full source
/--
Bitwise right shift of bounded numbers.
This operator corresponds to logical rather than arithmetic bit shifting. The new bits are always
`0`.
Examples:
* `(15 : Fin 16) >>> (1 : Fin 16) = (7 : Fin 16)`
* `(15 : Fin 16) >>> (2 : Fin 16) = (3 : Fin 16)`
* `(15 : Fin 17) >>> (2 : Fin 17) = (3 : Fin 17)`
-/
def shiftRight : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(a >>> b) % n, mlt h⟩Informal description
The bitwise right shift operation on bounded natural numbers. Given two elements `⟨a, h⟩` and `⟨b, _⟩` of `Fin n`, where `a` and `b` are natural numbers less than `n`, the operation returns `⟨(a >>> b) % n, _⟩`. This is a logical right shift, meaning new bits are filled with zeros. The result is taken modulo `n` to ensure it remains within the bounds of `Fin n`.
Examples:
- For `n = 16`, `15 >>> 1 = 7`
- For `n = 16`, `15 >>> 2 = 3`
- For `n = 17`, `15 >>> 2 = 3`
Fin.instAdd
instance
: Add (Fin n)
Informal description
The type `Fin n` of natural numbers less than `n` is equipped with an addition operation defined by adding the underlying natural numbers and taking the result modulo `n`.
Fin.instSub
instance
: Sub (Fin n)
Informal description
For any natural number $n$, the type $\mathrm{Fin}\,n$ of natural numbers less than $n$ has a subtraction operation inherited from the natural numbers, computed modulo $n$.
Fin.instMul
instance
: Mul (Fin n)
Informal description
For any natural number $n$, the type $\mathrm{Fin}\,n$ of natural numbers less than $n$ is equipped with a multiplication operation defined by multiplying the underlying natural numbers and taking the result modulo $n$.
Fin.instMod
instance
: Mod (Fin n)
Informal description
For any natural number $n$, the type $\mathrm{Fin}\,n$ of natural numbers less than $n$ has a modulus operation inherited from the natural numbers.
Fin.instDiv
instance
: Div (Fin n)
Informal description
For any natural number $n$, the type $\mathrm{Fin}\,n$ of natural numbers less than $n$ has a division operation defined by the natural number division on their underlying values.
Fin.instAndOp
instance
: AndOp (Fin n)
Informal description
For any natural number $n$, the type $\mathrm{Fin}\,n$ of natural numbers less than $n$ is equipped with a bitwise AND operation, where for any two elements $a, b \in \mathrm{Fin}\,n$, their AND is computed as the bitwise AND of their underlying natural numbers, taken modulo $n$.
Fin.instOrOp
instance
: OrOp (Fin n)
Informal description
For any natural number $n$, the type $\mathrm{Fin}\,n$ of natural numbers less than $n$ is equipped with a bitwise OR operation.
Fin.instXor
instance
: Xor (Fin n)
Informal description
For any natural number $n$, the type $\mathrm{Fin}\,n$ of natural numbers less than $n$ is equipped with a bitwise XOR operation, where the XOR of two elements $\langle a, h \rangle$ and $\langle b, \_ \rangle$ in $\mathrm{Fin}\,n$ is defined as $(a \oplus b) \bmod n$, with $\oplus$ denoting the bitwise XOR operation on natural numbers.
Fin.instShiftLeft
instance
: ShiftLeft (Fin n)
Full source
instance : ShiftLeft (Fin n) where
shiftLeft := Fin.shiftLeftInformal description
For any natural number $n$, the type $\mathrm{Fin}\,n$ of natural numbers less than $n$ has a left shift operation that wraps around on overflow.
Fin.instShiftRight
instance
: ShiftRight (Fin n)
Full source
instance : ShiftRight (Fin n) where
shiftRight := Fin.shiftRightInformal description
For any natural number $n$, the type $\text{Fin } n$ of natural numbers less than $n$ has a right shift operation $\texttt{>>>}$ defined by $(a \texttt{>>>} b) \mod n$ for $a, b \in \text{Fin } n$.
Fin.instOfNat
instance
{n : Nat} [NeZero n] {i : Nat} : OfNat (Fin n) i
Informal description
For any natural number `n` with `n ≠ 0` and any natural number `i`, the finite type `Fin n` (natural numbers less than `n`) can interpret `i` as an element via the `OfNat` typeclass.
Fin.instInhabited
instance
{n : Nat} [NeZero n] : Inhabited (Fin n)
Full source
instance instInhabited {n : Nat} [NeZero n] : Inhabited (Fin n) where
default := 0Informal description
For any natural number $n$ with $n \neq 0$, the type $\mathrm{Fin}\,n$ of natural numbers less than $n$ is inhabited, meaning it has a designated default element.
Fin.zero_eta
theorem
: (⟨0, Nat.zero_lt_succ _⟩ : Fin (n + 1)) = 0
Full source
@[simp] theorem zero_eta : (⟨0, Nat.zero_lt_succ _⟩ : Fin (n + 1)) = 0 := rflInformal description
For any natural number $n$, the element $\langle 0, \text{Nat.zero\_lt\_succ}\,n \rangle$ in the finite type $\mathrm{Fin}(n + 1)$ is equal to the zero element $0$.
Fin.ne_of_val_ne
theorem
{i j : Fin n} (h : val i ≠ val j) : i ≠ j
Full source
theorem ne_of_val_ne {i j : Fin n} (h : valval i ≠ val j) : i ≠ j :=
fun h' => absurd (val_eq_of_eq h') hInformal description
For any two elements $i$ and $j$ of the finite type $\mathrm{Fin}\,n$, if their underlying natural number values are distinct (i.e., $\mathrm{val}\,i \neq \mathrm{val}\,j$), then $i$ and $j$ are distinct elements (i.e., $i \neq j$).
Fin.val_ne_of_ne
theorem
{i j : Fin n} (h : i ≠ j) : val i ≠ val j
Full source
theorem val_ne_of_ne {i j : Fin n} (h : i ≠ j) : valval i ≠ val j :=
fun h' => absurd (eq_of_val_eq h') hInformal description
For any two distinct elements $i$ and $j$ of the finite type $\mathrm{Fin}\,n$ (i.e., $i \neq j$), their underlying natural number values are also distinct (i.e., $\mathrm{val}\,i \neq \mathrm{val}\,j$).
Fin.modn_lt
theorem
: ∀ {m : Nat} (i : Fin n), m > 0 → (modn i m).val < m
Informal description
For any natural number $m > 0$ and any element $i$ of the finite type $\mathrm{Fin}\,n$, the value of $i \bmod m$ is less than $m$, i.e., $(\mathrm{modn}\,i\,m).\mathrm{val} < m$.
Fin.val_lt_of_le
theorem
(i : Fin b) (h : b ≤ n) : i.val < n
Full source
theorem val_lt_of_le (i : Fin b) (h : b ≤ n) : i.val < n :=
Nat.lt_of_lt_of_le i.isLt hInformal description
For any element $i$ of the finite type $\mathrm{Fin}\,b$ and any natural number $n$ such that $b \leq n$, the underlying natural number value of $i$ satisfies $\mathrm{val}\,i < n$.
Fin.pos
theorem
(i : Fin n) : 0 < n
Full source
/-- If you actually have an element of `Fin n`, then the `n` is always positive -/
protected theorem pos (i : Fin n) : 0 < n :=
Nat.lt_of_le_of_lt (Nat.zero_le _) i.2Informal description
For any element $i$ of the finite type $\mathrm{Fin}\,n$, the upper bound $n$ is strictly positive, i.e., $0 < n$.
Fin.last
definition
(n : Nat) : Fin (n + 1)
Full source
/--
The greatest value of `Fin (n+1)`, namely `n`.
Examples:
* `Fin.last 4 = (4 : Fin 5)`
* `(Fin.last 0).val = (0 : Nat)`
-/
@[inline] def last (n : Nat) : Fin (n + 1) := ⟨n, n.lt_succ_self⟩Informal description
The function `Fin.last` takes a natural number `n` and returns the greatest element of the finite type `Fin (n + 1)`, which is the natural number `n` itself (viewed as an element of `Fin (n + 1)` since `n < n + 1`).
Fin.castLT
definition
(i : Fin m) (h : i.1 < n) : Fin n
Full source
/--
Replaces the bound with another that is suitable for the value.
The proof embedded in `i` can be used to cast to a larger bound even if the concrete value is not
known.
Examples:
```lean example
example : Fin 12 := (7 : Fin 10).castLT (by decide : 7 < 12)
```
```lean example
example (i : Fin 10) : Fin 12 :=
i.castLT <| by
cases i; simp; omega
```
-/
@[inline] def castLT (i : Fin m) (h : i.1 < n) : Fin n := ⟨i.1, h⟩Informal description
Given a natural number `i` in `Fin m` (i.e., `i < m`) and a proof `h` that `i < n`, the function `Fin.castLT` returns `i` as an element of `Fin n`. This allows casting a finite natural number to a larger bound when the value is known to satisfy the new bound.
Fin.castLE
definition
(h : n ≤ m) (i : Fin n) : Fin m
Full source
/--
Coarsens a bound to one at least as large.
See also `Fin.castAdd` for a version that represents the larger bound with addition rather than an
explicit inequality proof.
-/
@[inline] def castLE (h : n ≤ m) (i : Fin n) : Fin m := ⟨i, Nat.lt_of_lt_of_le i.2 h⟩Informal description
Given a natural number inequality proof $h : n \leq m$ and an element $i$ of the finite type `Fin n`, the function `Fin.castLE` returns the corresponding element in `Fin m` by preserving the value of $i$ and using the inequality to ensure it remains within bounds.
Fin.cast
definition
(eq : n = m) (i : Fin n) : Fin m
Full source
/--
Uses a proof that two bounds are equal to allow a value bounded by one to be used with the other.
In other words, when `eq : n = m`, `Fin.cast eq i` converts `i : Fin n` into a `Fin m`.
-/
@[inline] protected def cast (eq : n = m) (i : Fin n) : Fin m := ⟨i, eq ▸ i.2⟩Informal description
Given an equality proof $n = m$, the function $\text{Fin.cast}$ converts an element $i$ of the finite type $\text{Fin }n$ (natural numbers less than $n$) to an element of $\text{Fin }m$ by preserving the value of $i$ and using the equality to adjust the bound.
Fin.castAdd
definition
(m) : Fin n → Fin (n + m)
Full source
/--
Coarsens a bound to one at least as large.
See also `Fin.natAdd` and `Fin.addNat` for addition functions that increase the bound, and
`Fin.castLE` for a version that uses an explicit inequality proof.
-/
@[inline] def castAdd (m) : Fin n → Fin (n + m) :=
castLE <| Nat.le_add_right n mInformal description
The function `Fin.castAdd` takes a natural number `m` and maps an element `i` of the finite type `Fin n` (natural numbers less than `n`) to an element of `Fin (n + m)` by preserving the value of `i` and using the inequality `n ≤ n + m` to ensure it remains within bounds.
Fin.castSucc
definition
: Fin n → Fin (n + 1)
Informal description
The function maps an element $i$ of the finite type $\text{Fin } n$ (natural numbers less than $n$) to the corresponding element in $\text{Fin } (n + 1)$ by preserving the value of $i$ and adjusting the bound by one.
Fin.addNat
definition
(i : Fin n) (m) : Fin (n + m)
Full source
/--
Adds a natural number to a `Fin`, increasing the bound.
This is a generalization of `Fin.succ`.
`Fin.natAdd` is a version of this function that takes its `Nat` parameter first.
Examples:
* `Fin.addNat (5 : Fin 8) 3 = (8 : Fin 11)`
* `Fin.addNat (0 : Fin 8) 1 = (1 : Fin 9)`
* `Fin.addNat (1 : Fin 8) 2 = (3 : Fin 10)`
-/
def addNat (i : Fin n) (m) : Fin (n + m) := ⟨i + m, Nat.add_lt_add_right i.2 _⟩Informal description
Given a natural number $m$ and an element $i$ of the finite type $\text{Fin } n$ (representing natural numbers less than $n$), the function $\text{Fin.addNat}$ returns the element $i + m$ in the finite type $\text{Fin } (n + m)$. This operation preserves the bound by increasing it from $n$ to $n + m$.
Fin.natAdd
definition
(n) (i : Fin m) : Fin (n + m)
Full source
/--
Adds a natural number to a `Fin`, increasing the bound.
This is a generalization of `Fin.succ`.
`Fin.addNat` is a version of this function that takes its `Nat` parameter second.
Examples:
* `Fin.natAdd 3 (5 : Fin 8) = (8 : Fin 11)`
* `Fin.natAdd 1 (0 : Fin 8) = (1 : Fin 9)`
* `Fin.natAdd 1 (2 : Fin 8) = (3 : Fin 9)`
-/
def natAdd (n) (i : Fin m) : Fin (n + m) := ⟨n + i, Nat.add_lt_add_left i.2 _⟩Informal description
Given a natural number $n$ and an element $i$ of the finite type $\text{Fin } m$ (representing natural numbers less than $m$), the function $\text{Fin.natAdd}$ returns the element $n + i$ in the finite type $\text{Fin } (n + m)$. This operation preserves the bound by increasing it from $m$ to $n + m$.
Fin.rev
definition
(i : Fin n) : Fin n
Full source
/--
Replaces a value with its difference from the largest value in the type.
Considering the values of `Fin n` as a sequence `0`, `1`, …, `n-2`, `n-1`, `Fin.rev` finds the
corresponding element of the reversed sequence. In other words, it maps `0` to `n-1`, `1` to `n-2`,
..., and `n-1` to `0`.
Examples:
* `(5 : Fin 6).rev = (0 : Fin 6)`
* `(0 : Fin 6).rev = (5 : Fin 6)`
* `(2 : Fin 5).rev = (2 : Fin 5)`
-/
@[inline] def rev (i : Fin n) : Fin n := ⟨n - (i + 1), Nat.sub_lt i.pos (Nat.succ_pos _)⟩Informal description
For an element $i$ of the finite type $\text{Fin } n$ (representing natural numbers less than $n$), the function $\text{Fin.rev}$ maps $i$ to $n - (i + 1)$. This operation reverses the order of elements in $\text{Fin } n$, sending $0$ to $n-1$, $1$ to $n-2$, ..., and $n-1$ to $0$.
Fin.subNat
definition
(m) (i : Fin (n + m)) (h : m ≤ i) : Fin n
Full source
/--
Subtraction of a natural number from a `Fin`, with the bound narrowed.
This is a generalization of `Fin.pred`. It is guaranteed to not underflow or wrap around.
Examples:
* `(5 : Fin 9).subNat 2 (by decide) = (3 : Fin 7)`
* `(5 : Fin 9).subNat 0 (by decide) = (5 : Fin 9)`
* `(3 : Fin 9).subNat 3 (by decide) = (0 : Fin 6)`
-/
@[inline] def subNat (m) (i : Fin (n + m)) (h : m ≤ i) : Fin n :=
⟨i - m, Nat.sub_lt_right_of_lt_add h i.2⟩Informal description
Given a natural number $m$ and an element $i$ of the finite type $\mathrm{Fin}\,(n + m)$ (representing a natural number less than $n + m$), if $m \leq i$ holds, then the function $\mathrm{subNat}$ returns the element $i - m$ in the finite type $\mathrm{Fin}\,n$. This operation is guaranteed to not underflow or wrap around, ensuring the result is a valid element of $\mathrm{Fin}\,n$.
**Examples:**
- $(5 : \mathrm{Fin}\,9).\mathrm{subNat}\,2 = (3 : \mathrm{Fin}\,7)$
- $(5 : \mathrm{Fin}\,9).\mathrm{subNat}\,0 = (5 : \mathrm{Fin}\,9)$
- $(3 : \mathrm{Fin}\,9).\mathrm{subNat}\,3 = (0 : \mathrm{Fin}\,6)$
Fin.pred
definition
{n : Nat} (i : Fin (n + 1)) (h : i ≠ 0) : Fin n
Full source
/--
The predecessor of a non-zero element of `Fin (n+1)`, with the bound decreased.
Examples:
* `(4 : Fin 8).pred (by decide) = (3 : Fin 7)`
* `(1 : Fin 2).pred (by decide) = (0 : Fin 1)`
-/
@[inline] def pred {n : Nat} (i : Fin (n + 1)) (h : i ≠ 0) : Fin n :=
subNat 1 i <| Nat.pos_of_ne_zero <| mt (Fin.eq_of_val_eq (j := 0)) hInformal description
For a non-zero element \( i \) of the finite type \(\text{Fin}\,(n + 1)\) (representing natural numbers less than \( n + 1 \)), the function \(\text{Fin.pred}\) returns the predecessor of \( i \) as an element of \(\text{Fin}\,n\).
**Examples:**
- \((4 : \text{Fin}\,8).\text{pred} = (3 : \text{Fin}\,7)\)
- \((1 : \text{Fin}\,2).\text{pred} = (0 : \text{Fin}\,1)\)
Fin.val_inj
theorem
{a b : Fin n} : a.1 = b.1 ↔ a = b
Full source
theorem val_inj {a b : Fin n} : a.1 = b.1 ↔ a = b := ⟨Fin.eq_of_val_eq, Fin.val_eq_of_eq⟩Informal description
For any two elements $a$ and $b$ of the finite type $\mathrm{Fin}\,n$, the underlying natural number values of $a$ and $b$ are equal if and only if $a$ and $b$ are equal as elements of $\mathrm{Fin}\,n$. In other words, the natural number projection $\mathrm{val} : \mathrm{Fin}\,n \to \mathbb{N}$ is injective.
Fin.val_congr
theorem
{n : Nat} {a b : Fin n} (h : a = b) : (a : Nat) = (b : Nat)
Informal description
For any natural number $n$ and any elements $a, b$ of the finite type $\mathrm{Fin}\,n$, if $a = b$ then their underlying natural number values are equal, i.e., $(a : \mathbb{N}) = (b : \mathbb{N})$.
Fin.val_le_of_le
theorem
{n : Nat} {a b : Fin n} (h : a ≤ b) : (a : Nat) ≤ (b : Nat)
Full source
theorem val_le_of_le {n : Nat} {a b : Fin n} (h : a ≤ b) : (a : Nat) ≤ (b : Nat) := hInformal description
For any natural number $n$ and any elements $a, b$ of $\mathrm{Fin}\,n$ (the type of natural numbers less than $n$), if $a \leq b$ in the partial order on $\mathrm{Fin}\,n$, then the underlying natural number value of $a$ is less than or equal to the underlying natural number value of $b$.
Fin.val_le_of_ge
theorem
{n : Nat} {a b : Fin n} (h : a ≥ b) : (b : Nat) ≤ (a : Nat)
Full source
theorem val_le_of_ge {n : Nat} {a b : Fin n} (h : a ≥ b) : (b : Nat) ≤ (a : Nat) := hInformal description
For any natural number $n$ and any elements $a, b$ of $\mathrm{Fin}\,n$ (the type of natural numbers less than $n$), if $a \geq b$ in the partial order on $\mathrm{Fin}\,n$, then the underlying natural number value of $b$ is less than or equal to the underlying natural number value of $a$.
Fin.val_add_one_le_of_lt
theorem
{n : Nat} {a b : Fin n} (h : a < b) : (a : Nat) + 1 ≤ (b : Nat)
Full source
theorem val_add_one_le_of_lt {n : Nat} {a b : Fin n} (h : a < b) : (a : Nat) + 1 ≤ (b : Nat) := hInformal description
For any natural number $n$ and any elements $a, b$ of $\mathrm{Fin}\,n$ (the type of natural numbers less than $n$), if $a < b$ in the strict order on $\mathrm{Fin}\,n$, then the underlying natural number value of $a$ plus one is less than or equal to the underlying natural number value of $b$.
Fin.val_add_one_le_of_gt
theorem
{n : Nat} {a b : Fin n} (h : a > b) : (b : Nat) + 1 ≤ (a : Nat)
Full source
theorem val_add_one_le_of_gt {n : Nat} {a b : Fin n} (h : a > b) : (b : Nat) + 1 ≤ (a : Nat) := hInformal description
For any natural number $n$ and elements $a, b$ of $\mathrm{Fin}\,n$ (the type of natural numbers less than $n$), if $a > b$ in the order on $\mathrm{Fin}\,n$, then the underlying natural number value of $b$ plus one is less than or equal to the underlying natural number value of $a$.
Fin.exists_iff
theorem
{p : Fin n → Prop} : (Exists fun i => p i) ↔ Exists fun i => Exists fun h => p ⟨i, h⟩
Full source
theorem exists_iff {p : Fin n → Prop} : (Exists fun i => p i) ↔ Exists fun i => Exists fun h => p ⟨i, h⟩ :=
⟨fun ⟨⟨i, hi⟩, hpi⟩ => ⟨i, hi, hpi⟩, fun ⟨i, hi, hpi⟩ => ⟨⟨i, hi⟩, hpi⟩⟩Informal description
For any predicate $p$ on the finite type $\text{Fin}\,n$, the statement $(\exists i : \text{Fin}\,n, p\,i)$ is equivalent to $(\exists i : \mathbb{N}, \exists h : i < n, p\,\langle i, h \rangle)$.