Mathlib.Data.Fin.Tuple.Basic

Fin.tuple0_le theorem

{α : Fin 0 → Type*} [∀ i, Preorder (α i)] (f g : ∀ i, α i) : f ≤ g

Full source

theorem tuple0_le {α : Fin 0 → Type*} [∀ i, Preorder (α i)] (f g : ∀ i, α i) : f ≤ g :=
  finZeroElim

Trivial Ordering on Zero-Length Tuples

Informal description

For any family of types $\alpha : \text{Fin } 0 \to \text{Type}^*$ equipped with a preorder structure on each $\alpha i$, and for any two tuples $f, g : \forall i, \alpha i$, the relation $f \leq g$ holds.

Fin.tail definition

(q : ∀ i, α i) : ∀ i : Fin n, α i.succ

Full source

/-- The tail of an `n+1` tuple, i.e., its last `n` entries. -/
def tail (q : ∀ i, α i) : ∀ i : Fin n, α i.succ := fun i ↦ q i.succ

Tail of a dependent tuple

Informal description

Given a dependent tuple $ q $ of length $ n+1 $ (i.e., a function mapping each $ i : \text{Fin} (n+1) $ to an element of type $ \alpha i $), the tail of $ q $ is the tuple of length $ n $ obtained by removing the first element. Specifically, for each $ i : \text{Fin} n $, the $ i $-th element of the tail is $ q (i+1) $.

Fin.tail_def theorem

 {n : ℕ} {α : Fin (n + 1) → Sort*} {q : ∀ i, α i} : (tail fun k : Fin (n + 1) ↦ q k) = fun k : Fin n ↦ q k.succ

Full source

theorem tail_def {n : ℕ} {α : Fin (n + 1) → Sort*} {q : ∀ i, α i} :
    (tail fun k : Fin (n + 1) ↦ q k) = fun k : Fin n ↦ q k.succ :=
  rfl

Definition of Tail for Dependent Tuples: $\text{tail}(q) = \lambda k, q(k+1)$

Informal description

For any natural number $n$, any family of types $\alpha : \text{Fin}(n+1) \to \text{Sort}^*$, and any dependent tuple $q : \forall i, \alpha i$, the tail of the tuple $q$ is equal to the function that maps each $k : \text{Fin} n$ to $q(k.\text{succ})$. In other words, $\text{tail}(q) = \lambda k, q(k+1)$.

Fin.cons definition

(x : α 0) (p : ∀ i : Fin n, α i.succ) : ∀ i, α i

Full source

/-- Adding an element at the beginning of an `n`-tuple, to get an `n+1`-tuple. -/
def cons (x : α 0) (p : ∀ i : Fin n, α i.succ) : ∀ i, α i := fun j ↦ Fin.cases x p j

Prepend to a dependent tuple

Informal description

Given an element $x$ of type $\alpha(0)$ and a dependent tuple $p$ where each $p(i)$ has type $\alpha(i.\text{succ})$ for $i : \text{Fin} n$, the function $\text{Fin.cons}$ constructs a new dependent tuple of length $n+1$ by prepending $x$ to $p$. Specifically, for any index $j : \text{Fin} (n+1)$, the value at $j$ is defined as $x$ if $j = 0$, and $p(i)$ if $j = i.\text{succ}$ for some $i : \text{Fin} n$.

Fin.tail_cons theorem

: tail (cons x p) = p

Full source

@[simp]
theorem tail_cons : tail (cons x p) = p := by
  simp +unfoldPartialApp [tail, cons]

Tail of Cons Equals Original Tuple

Informal description

For any element $x$ of type $\alpha(0)$ and any dependent tuple $p$ where each $p(i)$ has type $\alpha(i.\text{succ})$ for $i : \text{Fin} n$, the tail of the tuple obtained by prepending $x$ to $p$ is equal to $p$ itself. That is, $\text{tail}(\text{cons}(x, p)) = p$.

Fin.cons_succ theorem

: cons x p i.succ = p i

Full source

@[simp]
theorem cons_succ : cons x p i.succ = p i := by simp [cons]

Successor Index Property of Prepended Tuple

Informal description

For any element $x$ of type $\alpha(0)$ and dependent tuple $p$ where each $p(i)$ has type $\alpha(i.\text{succ})$ for $i : \text{Fin} n$, the value of the prepended tuple $\text{cons}(x, p)$ at index $i.\text{succ}$ is equal to $p(i)$. In other words, $\text{cons}(x, p)(i+1) = p(i)$ for all $i : \text{Fin} n$.

Fin.cons_zero theorem

: cons x p 0 = x

Full source

@[simp]
theorem cons_zero : cons x p 0 = x := by simp [cons]

First Element of Prepended Tuple

Informal description

For any element $x$ of type $\alpha(0)$ and any dependent tuple $p$ where each $p(i)$ has type $\alpha(i.\text{succ})$ for $i : \text{Fin} n$, the value of the tuple $\text{Fin.cons}(x, p)$ at index $0$ is equal to $x$. In other words, $\text{Fin.cons}(x, p)(0) = x$.

Fin.cons_one theorem

{α : Fin (n + 2) → Sort*} (x : α 0) (p : ∀ i : Fin n.succ, α i.succ) : cons x p 1 = p 0

Full source

@[simp]
theorem cons_one {α : Fin (n + 2) → Sort*} (x : α 0) (p : ∀ i : Fin n.succ, α i.succ) :
    cons x p 1 = p 0 := by
  rw [← cons_succ x p]; rfl

Second Element of Prepended Tuple Equals First Element of Original Tuple

Informal description

For any type family $\alpha$ indexed by $\text{Fin}(n+2)$, element $x$ of type $\alpha(0)$, and dependent tuple $p$ where each $p(i)$ has type $\alpha(i.\text{succ})$ for $i : \text{Fin}(n+1)$, the value of the prepended tuple $\text{cons}(x, p)$ at index $1$ is equal to $p(0)$. That is, $\text{cons}(x, p)(1) = p(0)$.

Fin.cons_update theorem

: cons x (update p i y) = update (cons x p) i.succ y

Full source

/-- Updating a tuple and adding an element at the beginning commute. -/
@[simp]
theorem cons_update : cons x (update p i y) = update (cons x p) i.succ y := by
  ext j
  by_cases h : j = 0
  · rw [h]
    simp [Ne.symm (succ_ne_zero i)]
  · let j' := pred j h
    have : j'.succ = j := succ_pred j h
    rw [← this, cons_succ]
    by_cases h' : j' = i
    · rw [h']
      simp
    · have : j'.succ ≠ i.succ := by rwa [Ne, succ_inj]
      rw [update_of_ne h', update_of_ne this, cons_succ]

Commutation of Prepend and Update Operations on Tuples

Informal description

For any element $x$ of type $\alpha(0)$, dependent tuple $p$ where each $p(i)$ has type $\alpha(i.\text{succ})$ for $i : \text{Fin} n$, index $i : \text{Fin} n$, and element $y$ of type $\alpha(i.\text{succ})$, the operation of prepending $x$ to the tuple obtained by updating $p$ at index $i$ with $y$ is equal to updating the prepended tuple $\text{cons}(x, p)$ at index $i+1$ with $y$. In other words, $\text{cons}(x, \text{update}(p, i, y)) = \text{update}(\text{cons}(x, p), i+1, y)$.

Fin.cons_injective2 theorem

: Function.Injective2 (@cons n α)

Full source

/-- As a binary function, `Fin.cons` is injective. -/
theorem cons_injective2 : Function.Injective2 (@cons n α) := fun x₀ y₀ x y h ↦
  ⟨congr_fun h 0, funext fun i ↦ by simpa using congr_fun h (Fin.succ i)⟩

Injectivity of Tuple Prepend Operation

Informal description

The function $\text{Fin.cons}$, which prepends an element to a dependent tuple, is injective as a binary function. That is, for any type family $\alpha$ indexed by $\text{Fin}(n+1)$, if $\text{cons}(x_0, x) = \text{cons}(y_0, y)$, then $x_0 = y_0$ and $x = y$.

Fin.cons_inj theorem

{x₀ y₀ : α 0} {x y : ∀ i : Fin n, α i.succ} : cons x₀ x = cons y₀ y ↔ x₀ = y₀ ∧ x = y

Full source

@[simp]
theorem cons_inj {x₀ y₀ : α 0} {x y : ∀ i : Fin n, α i.succ} :
    conscons x₀ x = cons y₀ y ↔ x₀ = y₀ ∧ x = y :=
  cons_injective2.eq_iff

Equality of Prepended Tuples is Equivalent to Componentwise Equality

Informal description

For any elements $x_0, y_0$ of type $\alpha(0)$ and dependent tuples $x, y$ where each $x(i), y(i)$ has type $\alpha(i.\text{succ})$ for $i : \text{Fin} n$, the prepended tuples $\text{cons}(x_0, x)$ and $\text{cons}(y_0, y)$ are equal if and only if $x_0 = y_0$ and $x = y$.

Fin.cons_left_injective theorem

(x : ∀ i : Fin n, α i.succ) : Function.Injective fun x₀ ↦ cons x₀ x

Full source

theorem cons_left_injective (x : ∀ i : Fin n, α i.succ) : Function.Injective fun x₀ ↦ cons x₀ x :=
  cons_injective2.left _

Injectivity of Tuple Prepend Operation in First Argument

Informal description

For any dependent tuple $x$ where each $x(i)$ has type $\alpha(i.\text{succ})$ for $i : \text{Fin} n$, the function $\lambda x_0, \text{cons}(x_0, x)$ is injective. That is, if $\text{cons}(x_0, x) = \text{cons}(y_0, x)$, then $x_0 = y_0$.

Fin.cons_right_injective theorem

(x₀ : α 0) : Function.Injective (cons x₀)

Full source

theorem cons_right_injective (x₀ : α 0) : Function.Injective (cons x₀) :=
  cons_injective2.right _

Injectivity of Tuple Prepend Operation in Second Argument

Informal description

For any element $x_0$ of type $\alpha(0)$, the function $\text{cons}(x_0, \cdot)$ is injective. That is, for any two dependent tuples $p, q : \forall i : \text{Fin} n, \alpha(i.\text{succ})$, if $\text{cons}(x_0, p) = \text{cons}(x_0, q)$, then $p = q$.

Fin.update_cons_zero theorem

: update (cons x p) 0 z = cons z p

Full source

/-- Adding an element at the beginning of a tuple and then updating it amounts to adding it
directly. -/
theorem update_cons_zero : update (cons x p) 0 z = cons z p := by
  ext j
  by_cases h : j = 0
  · rw [h]
    simp
  · simp only [h, update_of_ne, Ne, not_false_iff]
    let j' := pred j h
    have : j'.succ = j := succ_pred j h
    rw [← this, cons_succ, cons_succ]

Update of First Element in Prepended Tuple

Informal description

For any element $x$ of type $\alpha(0)$, any dependent tuple $p$ where each $p(i)$ has type $\alpha(i.\text{succ})$ for $i : \text{Fin} n$, and any element $z$ of type $\alpha(0)$, updating the first element of the prepended tuple $\text{cons}(x, p)$ to $z$ yields the same result as directly prepending $z$ to $p$. In other words, $\text{update}(\text{cons}(x, p), 0, z) = \text{cons}(z, p)$.

Fin.cons_self_tail theorem

: cons (q 0) (tail q) = q

Full source

/-- Concatenating the first element of a tuple with its tail gives back the original tuple -/
@[simp]
theorem cons_self_tail : cons (q 0) (tail q) = q := by
  ext j
  by_cases h : j = 0
  · rw [h]
    simp
  · let j' := pred j h
    have : j'.succ = j := succ_pred j h
    rw [← this]
    unfold tail
    rw [cons_succ]

Reconstruction of Tuple from Head and Tail

Informal description

For any dependent tuple $q$ of length $n+1$, prepending the first element $q(0)$ to the tail of $q$ (which is obtained by removing the first element) reconstructs the original tuple $q$. In other words, $\text{cons}(q(0), \text{tail}(q)) = q$.

Fin.consEquiv definition

(α : Fin (n + 1) → Type*) : α 0 × (∀ i, α (succ i)) ≃ ∀ i, α i

Full source

/-- Equivalence between tuples of length `n + 1` and pairs of an element and a tuple of length `n`
given by separating out the first element of the tuple.

This is `Fin.cons` as an `Equiv`. -/
@[simps]
def consEquiv (α : Fin (n + 1) → Type*) : α 0 × (∀ i, α (succ i))α 0 × (∀ i, α (succ i)) ≃ ∀ i, α i where
  toFun f := cons f.1 f.2
  invFun f := (f 0, tail f)
  left_inv f := by simp
  right_inv f := by simp

Equivalence between dependent tuples and prepended pairs

Informal description

The equivalence `Fin.consEquiv` establishes a bijection between dependent tuples of length `n + 1` and pairs consisting of an element of type `α 0` and a dependent tuple of length `n` (where each element at position `i` has type `α (succ i)`). Specifically: - The forward direction (`toFun`) takes a pair `(x, p)` and constructs the tuple `Fin.cons x p` of length `n + 1` by prepending `x` to `p`. - The inverse direction (`invFun`) takes a tuple `f` of length `n + 1` and returns the pair `(f 0, Fin.tail f)`, where `Fin.tail f` is the tuple obtained by removing the first element of `f`. The bijection is verified by the proofs `left_inv` and `right_inv`, which show that these operations are mutual inverses.

Fin.consCases definition

{P : (∀ i : Fin n.succ, α i) → Sort v} (h : ∀ x₀ x, P (Fin.cons x₀ x)) (x : ∀ i : Fin n.succ, α i) : P x

Full source

/-- Recurse on an `n+1`-tuple by splitting it into a single element and an `n`-tuple. -/
@[elab_as_elim]
def consCases {P : (∀ i : Fin n.succ, α i) → Sort v} (h : ∀ x₀ x, P (Fin.cons x₀ x))
    (x : ∀ i : Fin n.succ, α i) : P x :=
  _root_.cast (by rw [cons_self_tail]) <| h (x 0) (tail x)

Case analysis for dependent tuples via head and tail decomposition

Informal description

Given a predicate `P` on dependent tuples of length `n + 1` and a proof `h` that `P` holds for any tuple constructed by prepending an element `x₀` to a tuple `x` of length `n`, the function `Fin.consCases` proves that `P` holds for any given dependent tuple `x` of length `n + 1` by decomposing it into its head `x 0` and tail `tail x`.

Fin.consCases_cons theorem

 {P : (∀ i : Fin n.succ, α i) → Sort v} (h : ∀ x₀ x, P (Fin.cons x₀ x)) (x₀ : α 0) (x : ∀ i : Fin n, α i.succ) :
  @consCases _ _ _ h (cons x₀ x) = h x₀ x

Full source

@[simp]
theorem consCases_cons {P : (∀ i : Fin n.succ, α i) → Sort v} (h : ∀ x₀ x, P (Fin.cons x₀ x))
    (x₀ : α 0) (x : ∀ i : Fin n, α i.succ) : @consCases _ _ _ h (cons x₀ x) = h x₀ x := by
  rw [consCases, cast_eq]
  congr

Consistency of $\text{consCases}$ with $\text{cons}$ construction

Informal description

For any predicate $P$ on dependent tuples of length $n+1$ (i.e., functions $\forall i : \text{Fin} (n+1), \alpha i$) and any proof $h$ that $P$ holds for tuples constructed via $\text{Fin.cons}$, the application of $\text{consCases}$ to a tuple $\text{cons}\,x₀\,x$ equals $h\,x₀\,x$. In other words, when decomposing a tuple constructed by prepending $x₀$ to $x$ via $\text{consCases}$, the result is exactly the proof $h$ applied to $x₀$ and $x$.

Fin.consInduction definition

 {α : Sort*} {P : ∀ {n : ℕ}, (Fin n → α) → Sort v} (h0 : P Fin.elim0)
  (h : ∀ {n} (x₀) (x : Fin n → α), P x → P (Fin.cons x₀ x)) : ∀ {n : ℕ} (x : Fin n → α), P x

Full source

/-- Recurse on a tuple by splitting into `Fin.elim0` and `Fin.cons`. -/
@[elab_as_elim]
def consInduction {α : Sort*} {P : ∀ {n : ℕ}, (Fin n → α) → Sort v} (h0 : P Fin.elim0)
    (h : ∀ {n} (x₀) (x : Fin n → α), P x → P (Fin.cons x₀ x)) : ∀ {n : ℕ} (x : Fin n → α), P x
  | 0, x => by convert h0
  | _ + 1, x => consCases (fun _ _ ↦ h _ _ <| consInduction h0 h _) x

Induction principle for tuples via prepending

Informal description

Given a type $\alpha$ and a predicate $P$ on tuples (functions $\text{Fin}\,n \to \alpha$ for varying $n$), if $P$ holds for the empty tuple and for any tuple constructed by prepending an element $x_0$ to a tuple $x$ (assuming $P$ holds for $x$), then $P$ holds for all tuples. This provides an induction principle for tuples based on their length and construction via prepending elements.

Fin.cons_injective_of_injective theorem

 {α} {x₀ : α} {x : Fin n → α} (hx₀ : x₀ ∉ Set.range x) (hx : Function.Injective x) :
  Function.Injective (cons x₀ x : Fin n.succ → α)

Full source

theorem cons_injective_of_injective {α} {x₀ : α} {x : Fin n → α} (hx₀ : x₀ ∉ Set.range x)
    (hx : Function.Injective x) : Function.Injective (cons x₀ x : Fin n.succ → α) := by
  refine Fin.cases ?_ ?_
  · refine Fin.cases ?_ ?_
    · intro
      rfl
    · intro j h
      rw [cons_zero, cons_succ] at h
      exact hx₀.elim ⟨_, h.symm⟩
  · intro i
    refine Fin.cases ?_ ?_
    · intro h
      rw [cons_zero, cons_succ] at h
      exact hx₀.elim ⟨_, h⟩
    · intro j h
      rw [cons_succ, cons_succ] at h
      exact congr_arg _ (hx h)

Injectivity of Prepended Tuple under Disjointness and Injectivity Conditions

Informal description

Let $\alpha$ be a type, $x_0$ an element of $\alpha$, and $x : \text{Fin} n \to \alpha$ a function. If $x_0$ is not in the range of $x$ and $x$ is injective, then the function $\text{cons}(x_0, x) : \text{Fin} (n+1) \to \alpha$ is injective.

Fin.cons_injective_iff theorem

 {α} {x₀ : α} {x : Fin n → α} :
  Function.Injective (cons x₀ x : Fin n.succ → α) ↔ x₀ ∉ Set.range x ∧ Function.Injective x

Full source

theorem cons_injective_iff {α} {x₀ : α} {x : Fin n → α} :
    Function.InjectiveFunction.Injective (cons x₀ x : Fin n.succ → α) ↔ x₀ ∉ Set.range x ∧ Function.Injective x := by
  refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ cons_injective_of_injective h.1 h.2⟩
  · rintro ⟨i, hi⟩
    replace h := @h i.succ 0
    simp [hi] at h
  · simpa [Function.comp] using h.comp (Fin.succ_injective _)

Injectivity Criterion for Prepended Tuple: $\text{cons}(x_0, x)$ injective $\leftrightarrow$ $x_0 \notin \text{range}(x) \land x$ injective

Informal description

For any type $\alpha$, element $x_0 \in \alpha$, and function $x : \text{Fin}\,n \to \alpha$, the prepended function $\text{cons}(x_0, x) : \text{Fin}\,(n+1) \to \alpha$ is injective if and only if $x_0$ is not in the range of $x$ and $x$ is injective.

Fin.forall_fin_zero_pi theorem

{α : Fin 0 → Sort*} {P : (∀ i, α i) → Prop} : (∀ x, P x) ↔ P finZeroElim

Full source

@[simp]
theorem forall_fin_zero_pi {α : Fin 0 → Sort*} {P : (∀ i, α i) → Prop} :
    (∀ x, P x) ↔ P finZeroElim :=
  ⟨fun h ↦ h _, fun h x ↦ Subsingleton.elim finZeroElim x ▸ h⟩

Universal Quantification over Empty Finite Tuple

Informal description

For any family of types `α` indexed by `Fin 0` (the empty finite type) and any predicate `P` on dependent functions `∀ i, α i`, the universal quantification `∀ x, P x` holds if and only if `P` holds for the unique function `finZeroElim : ∀ i, α i` (the empty function).

Fin.exists_fin_zero_pi theorem

{α : Fin 0 → Sort*} {P : (∀ i, α i) → Prop} : (∃ x, P x) ↔ P finZeroElim

Full source

@[simp]
theorem exists_fin_zero_pi {α : Fin 0 → Sort*} {P : (∀ i, α i) → Prop} :
    (∃ x, P x) ↔ P finZeroElim :=
  ⟨fun ⟨x, h⟩ ↦ Subsingleton.elim x finZeroElim ▸ h, fun h ↦ ⟨_, h⟩⟩

Existential Quantification over Empty Finite Tuple

Informal description

For any family of types $\alpha$ indexed by $\text{Fin}\ 0$ (the empty finite type) and any predicate $P$ on dependent functions $\forall i, \alpha i$, the existential quantification $\exists x, P x$ holds if and only if $P$ holds for the unique function $\text{finZeroElim} : \forall i, \alpha i$ (the empty function).

Fin.forall_fin_succ_pi theorem

{P : (∀ i, α i) → Prop} : (∀ x, P x) ↔ ∀ a v, P (Fin.cons a v)

Full source

theorem forall_fin_succ_pi {P : (∀ i, α i) → Prop} : (∀ x, P x) ↔ ∀ a v, P (Fin.cons a v) :=
  ⟨fun h a v ↦ h (Fin.cons a v), consCases⟩

Universal Quantification over Dependent Tuples via Head-Tail Decomposition

Informal description

For any predicate $P$ on dependent tuples of length $n+1$ (i.e., functions mapping each $i : \text{Fin} (n+1)$ to an element of type $\alpha i$), the universal quantification $\forall x, P(x)$ holds if and only if for all elements $a : \alpha 0$ and all dependent tuples $v$ of length $n$ (i.e., functions mapping each $i : \text{Fin} n$ to $\alpha (i.\text{succ})$), $P(\text{Fin.cons}(a, v))$ holds.

Fin.exists_fin_succ_pi theorem

{P : (∀ i, α i) → Prop} : (∃ x, P x) ↔ ∃ a v, P (Fin.cons a v)

Full source

theorem exists_fin_succ_pi {P : (∀ i, α i) → Prop} : (∃ x, P x) ↔ ∃ a v, P (Fin.cons a v) :=
  ⟨fun ⟨x, h⟩ ↦ ⟨x 0, tail x, (cons_self_tail x).symm ▸ h⟩, fun ⟨_, _, h⟩ ↦ ⟨_, h⟩⟩

Existential Quantification over Dependent Tuples via Head-Tail Decomposition

Informal description

For any predicate $P$ on dependent tuples of length $n+1$ (i.e., functions mapping each $i : \text{Fin} (n+1)$ to an element of type $\alpha i$), the existential quantification $\exists x, P(x)$ holds if and only if there exists an element $a : \alpha 0$ and a dependent tuple $v$ of length $n$ (i.e., a function mapping each $i : \text{Fin} n$ to $\alpha (i.\text{succ})$) such that $P(\text{cons}(a, v))$ holds.

Fin.tail_update_zero theorem

: tail (update q 0 z) = tail q

Full source

/-- Updating the first element of a tuple does not change the tail. -/
@[simp]
theorem tail_update_zero : tail (update q 0 z) = tail q := by
  ext j
  simp [tail]

Tail Preservation Under First Element Update

Informal description

For any dependent tuple $q$ of length $n+1$ (i.e., a function mapping each $i : \text{Fin} (n+1)$ to an element of type $\alpha i$) and any element $z$ of type $\alpha 0$, the tail of the tuple obtained by updating the first element of $q$ to $z$ is equal to the tail of $q$.

Fin.tail_update_succ theorem

: tail (update q i.succ y) = update (tail q) i y

Full source

/-- Updating a nonzero element and taking the tail commute. -/
@[simp]
theorem tail_update_succ : tail (update q i.succ y) = update (tail q) i y := by
  ext j
  by_cases h : j = i
  · rw [h]
    simp [tail]
  · simp [tail, (Fin.succ_injective n).ne h, h]

Commutation of Tail and Update at Successor Index

Informal description

For any dependent tuple $q$ of length $n+1$ (i.e., a function mapping each $i : \text{Fin} (n+1)$ to an element of type $\alpha i$), updating the $(i+1)$-th element of $q$ to $y$ and then taking the tail is equivalent to first taking the tail of $q$ and then updating its $i$-th element to $y$. In other words, the tail operation commutes with updating a nonzero element of the tuple: $$\text{tail}(\text{update } q (i+1) y) = \text{update } (\text{tail } q) i y$$

Fin.comp_cons theorem

{α : Sort*} {β : Sort*} (g : α → β) (y : α) (q : Fin n → α) : g ∘ cons y q = cons (g y) (g ∘ q)

Full source

theorem comp_cons {α : Sort*} {β : Sort*} (g : α → β) (y : α) (q : Fin n → α) :
    g ∘ cons y q = cons (g y) (g ∘ q) := by
  ext j
  by_cases h : j = 0
  · rw [h]
    rfl
  · let j' := pred j h
    have : j'.succ = j := succ_pred j h
    rw [← this, cons_succ, comp_apply, comp_apply, cons_succ]

Composition with Prepended Tuple Equals Prepended Composition: $g \circ \text{cons}(y,q) = \text{cons}(g(y), g \circ q)$

Informal description

Let $g : \alpha \to \beta$ be a function, $y \in \alpha$ an element, and $q : \text{Fin} n \to \alpha$ a tuple. Then the composition of $g$ with the prepended tuple $\text{cons}(y, q)$ is equal to the prepended tuple formed by $g(y)$ and the composition $g \circ q$. In other words, for any index $i \in \text{Fin} (n+1)$, we have: $$(g \circ \text{cons}(y, q))(i) = \text{cons}(g(y), g \circ q)(i)$$

Fin.comp_tail theorem

{α : Sort*} {β : Sort*} (g : α → β) (q : Fin n.succ → α) : g ∘ tail q = tail (g ∘ q)

Full source

theorem comp_tail {α : Sort*} {β : Sort*} (g : α → β) (q : Fin n.succ → α) :
    g ∘ tail q = tail (g ∘ q) := by
  ext j
  simp [tail]

Composition with Tail of Tuple Equals Tail of Composition

Informal description

Let $g : \alpha \to \beta$ be a function and $q : \text{Fin} (n+1) \to \alpha$ be a tuple of length $n+1$. Then the composition of $g$ with the tail of $q$ is equal to the tail of the composition of $g$ with $q$. In other words, $g \circ (\text{tail } q) = \text{tail } (g \circ q)$.

Fin.le_cons theorem

 [∀ i, Preorder (α i)] {x : α 0} {q : ∀ i, α i} {p : ∀ i : Fin n, α i.succ} : q ≤ cons x p ↔ q 0 ≤ x ∧ tail q ≤ p

Full source

theorem le_cons [∀ i, Preorder (α i)] {x : α 0} {q : ∀ i, α i} {p : ∀ i : Fin n, α i.succ} :
    q ≤ cons x p ↔ q 0 ≤ x ∧ tail q ≤ p :=
  forall_fin_succ.trans <| and_congr Iff.rfl <| forall_congr' fun j ↦ by simp [tail]

Preorder Comparison of Tuple with Prepended Tuple: $q \leq \text{cons}(x,p) \leftrightarrow q(0) \leq x \land \text{tail}(q) \leq p$

Informal description

Let $\{\alpha_i\}_{i \in \text{Fin}(n+1)}$ be a family of types equipped with preorders. For any element $x \in \alpha_0$, a dependent tuple $q \in \prod_{i \in \text{Fin}(n+1)} \alpha_i$, and a dependent tuple $p \in \prod_{i \in \text{Fin}(n)} \alpha_{i+1}$, we have that $q$ is less than or equal to the prepended tuple $\text{cons}(x, p)$ if and only if both $q(0) \leq x$ and the tail of $q$ is less than or equal to $p$.

Fin.cons_le theorem

 [∀ i, Preorder (α i)] {x : α 0} {q : ∀ i, α i} {p : ∀ i : Fin n, α i.succ} : cons x p ≤ q ↔ x ≤ q 0 ∧ p ≤ tail q

Full source

theorem cons_le [∀ i, Preorder (α i)] {x : α 0} {q : ∀ i, α i} {p : ∀ i : Fin n, α i.succ} :
    conscons x p ≤ q ↔ x ≤ q 0 ∧ p ≤ tail q :=
  @le_cons _ (fun i ↦ (α i)ᵒᵈ) _ x q p

Comparison of Prepended Tuple: $\text{cons}(x, p) \leq q \leftrightarrow x \leq q(0) \land p \leq \text{tail}(q)$

Informal description

Let $\{\alpha_i\}_{i \in \text{Fin}(n+1)}$ be a family of types equipped with preorders. For any element $x \in \alpha_0$, a dependent tuple $q \in \prod_{i \in \text{Fin}(n+1)} \alpha_i$, and a dependent tuple $p \in \prod_{i \in \text{Fin}(n)} \alpha_{i+1}$, the prepended tuple $\text{cons}(x, p)$ is less than or equal to $q$ if and only if both $x \leq q(0)$ and $p \leq \text{tail}(q)$.

Fin.cons_le_cons theorem

 [∀ i, Preorder (α i)] {x₀ y₀ : α 0} {x y : ∀ i : Fin n, α i.succ} : cons x₀ x ≤ cons y₀ y ↔ x₀ ≤ y₀ ∧ x ≤ y

Full source

theorem cons_le_cons [∀ i, Preorder (α i)] {x₀ y₀ : α 0} {x y : ∀ i : Fin n, α i.succ} :
    conscons x₀ x ≤ cons y₀ y ↔ x₀ ≤ y₀ ∧ x ≤ y :=
  forall_fin_succ.trans <| and_congr_right' <| by simp only [cons_succ, Pi.le_def]

Comparison of Prepended Tuples: $\text{cons}(x_0, x) \leq \text{cons}(y_0, y) \leftrightarrow x_0 \leq y_0 \land x \leq y$

Informal description

Let $\{\alpha_i\}_{i \in \text{Fin}(n+1)}$ be a family of types equipped with preorders. For any elements $x_0, y_0 \in \alpha_0$ and dependent tuples $x, y \in \prod_{i \in \text{Fin}(n)} \alpha_{i+1}$, the prepended tuple $\text{cons}(x_0, x)$ is less than or equal to $\text{cons}(y_0, y)$ if and only if both $x_0 \leq y_0$ and $x \leq y$.

Fin.range_fin_succ theorem

{α} (f : Fin (n + 1) → α) : Set.range f = insert (f 0) (Set.range (Fin.tail f))

Full source

theorem range_fin_succ {α} (f : Fin (n + 1) → α) :
    Set.range f = insert (f 0) (Set.range (Fin.tail f)) :=
  Set.ext fun _ ↦ exists_fin_succ.trans <| eq_comm.or Iff.rfl

Range Decomposition for Tuples: $\text{range}\, f = \{f(0)\} \cup \text{range}\, (\text{tail}\, f)$

Informal description

For any function $f : \text{Fin}(n+1) \to \alpha$, the range of $f$ is equal to the union of $\{f(0)\}$ and the range of the tail of $f$. In other words, the range of $f$ consists of the first element $f(0)$ together with all elements in the range of the function obtained by removing the first element from $f$.

Fin.range_cons theorem

{α} {n : ℕ} (x : α) (b : Fin n → α) : Set.range (Fin.cons x b : Fin n.succ → α) = insert x (Set.range b)

Full source

@[simp]
theorem range_cons {α} {n : ℕ} (x : α) (b : Fin n → α) :
    Set.range (Fin.cons x b : Fin n.succ → α) = insert x (Set.range b) := by
  rw [range_fin_succ, cons_zero, tail_cons]

Range of Prepended Tuple: $\text{range}(\text{cons}(x, b)) = \{x\} \cup \text{range}(b)$

Informal description

For any element $x$ of type $\alpha$ and any tuple $b : \text{Fin}\, n \to \alpha$, the range of the tuple obtained by prepending $x$ to $b$ is equal to the union of $\{x\}$ and the range of $b$. In other words, the range of $\text{Fin.cons}(x, b)$ is $\{x\} \cup \text{range}(b)$.

Fin.append definition

(a : Fin m → α) (b : Fin n → α) : Fin (m + n) → α

Full source

/-- Append a tuple of length `m` to a tuple of length `n` to get a tuple of length `m + n`.
This is a non-dependent version of `Fin.add_cases`. -/
def append (a : Fin m → α) (b : Fin n → α) : Fin (m + n) → α :=
  @Fin.addCases _ _ (fun _ => α) a b

Concatenation of tuples

Informal description

Given a tuple $a$ of length $m$ (i.e., a function $a : \text{Fin}\, m \to \alpha$) and a tuple $b$ of length $n$ (i.e., a function $b : \text{Fin}\, n \to \alpha$), the function $\text{Fin.append}\, a\, b$ constructs a new tuple of length $m + n$ by concatenating $a$ and $b$. More precisely, for $i < m$, the $i$-th element of the resulting tuple is $a\, i$, and for $m \leq i < m + n$, the $i$-th element is $b\, (i - m)$.

Fin.append_left theorem

(u : Fin m → α) (v : Fin n → α) (i : Fin m) : append u v (Fin.castAdd n i) = u i

Full source

@[simp]
theorem append_left (u : Fin m → α) (v : Fin n → α) (i : Fin m) :
    append u v (Fin.castAdd n i) = u i :=
  addCases_left _

Left Component Preservation in Tuple Concatenation

Informal description

For any tuple $u$ of length $m$ (i.e., a function $u : \text{Fin}\, m \to \alpha$), any tuple $v$ of length $n$ (i.e., a function $v : \text{Fin}\, n \to \alpha$), and any index $i \in \text{Fin}\, m$, the $i$-th element of the concatenated tuple $\text{append}\, u\, v$ is equal to $u\, i$. Here, $\text{Fin.castAdd}\, n\, i$ is the natural embedding of $i$ into $\text{Fin}\, (m + n)$.

Fin.append_right theorem

(u : Fin m → α) (v : Fin n → α) (i : Fin n) : append u v (natAdd m i) = v i

Full source

@[simp]
theorem append_right (u : Fin m → α) (v : Fin n → α) (i : Fin n) :
    append u v (natAdd m i) = v i :=
  addCases_right _

Right Component of Concatenated Tuples

Informal description

For any tuple $u$ of length $m$ (i.e., a function $u : \text{Fin}\, m \to \alpha$) and any tuple $v$ of length $n$ (i.e., a function $v : \text{Fin}\, n \to \alpha$), the concatenated tuple $\text{append}\, u\, v$ satisfies $\text{append}\, u\, v\, (\text{natAdd}\, m\, i) = v\, i$ for any index $i$ in $\text{Fin}\, n$. Here, $\text{natAdd}\, m\, i$ shifts the index $i$ by $m$ positions to the right.

Fin.append_right_nil theorem

(u : Fin m → α) (v : Fin n → α) (hv : n = 0) : append u v = u ∘ Fin.cast (by rw [hv, Nat.add_zero])

Full source

theorem append_right_nil (u : Fin m → α) (v : Fin n → α) (hv : n = 0) :
    append u v = u ∘ Fin.cast (by rw [hv, Nat.add_zero]) := by
  refine funext (Fin.addCases (fun l => ?_) fun r => ?_)
  · rw [append_left, Function.comp_apply]
    refine congr_arg u (Fin.ext ?_)
    simp
  · exact (Fin.cast hv r).elim0

Concatenation with Empty Tuple on the Right Preserves Original Tuple

Informal description

For any tuple $u$ of length $m$ (i.e., a function $u : \text{Fin}\, m \to \alpha$) and any tuple $v$ of length $n$ (i.e., a function $v : \text{Fin}\, n \to \alpha$) where $n = 0$, the concatenated tuple $\text{append}\, u\, v$ is equal to $u$ composed with the canonical embedding $\text{Fin.cast}$ that adjusts the type from $\text{Fin}\, m$ to $\text{Fin}\, (m + 0)$.

Fin.append_elim0 theorem

(u : Fin m → α) : append u Fin.elim0 = u ∘ Fin.cast (Nat.add_zero _)

Full source

@[simp]
theorem append_elim0 (u : Fin m → α) :
    append u Fin.elim0 = u ∘ Fin.cast (Nat.add_zero _) :=
  append_right_nil _ _ rfl

Concatenation with Empty Tuple on the Right Preserves Original Tuple via Cast

Informal description

For any tuple $u$ of length $m$ (i.e., a function $u : \text{Fin}\, m \to \alpha$), the concatenation of $u$ with the empty tuple $\text{Fin.elim0}$ is equal to $u$ composed with the canonical embedding $\text{Fin.cast}$ that adjusts the type from $\text{Fin}\, m$ to $\text{Fin}\, (m + 0)$.

Fin.append_left_nil theorem

(u : Fin m → α) (v : Fin n → α) (hu : m = 0) : append u v = v ∘ Fin.cast (by rw [hu, Nat.zero_add])

Full source

theorem append_left_nil (u : Fin m → α) (v : Fin n → α) (hu : m = 0) :
    append u v = v ∘ Fin.cast (by rw [hu, Nat.zero_add]) := by
  refine funext (Fin.addCases (fun l => ?_) fun r => ?_)
  · exact (Fin.cast hu l).elim0
  · rw [append_right, Function.comp_apply]
    refine congr_arg v (Fin.ext ?_)
    simp [hu]

Concatenation with Empty Tuple on the Left Preserves Right Tuple

Informal description

For any tuple $u$ of length $m$ (i.e., a function $u : \text{Fin}\, m \to \alpha$) and any tuple $v$ of length $n$ (i.e., a function $v : \text{Fin}\, n \to \alpha$), if $m = 0$, then the concatenated tuple $\text{append}\, u\, v$ is equal to $v$ composed with the canonical embedding $\text{Fin.cast}$ that adjusts the type from $\text{Fin}\, n$ to $\text{Fin}\, (0 + n)$.

Fin.elim0_append theorem

(v : Fin n → α) : append Fin.elim0 v = v ∘ Fin.cast (Nat.zero_add _)

Full source

@[simp]
theorem elim0_append (v : Fin n → α) :
    append Fin.elim0 v = v ∘ Fin.cast (Nat.zero_add _) :=
  append_left_nil _ _ rfl

Concatenation with Empty Tuple on the Left Preserves Original Tuple via Cast

Informal description

For any tuple $v$ of length $n$ (i.e., a function $v : \text{Fin}\, n \to \alpha$), the concatenation of the empty tuple $\text{Fin.elim0}$ with $v$ is equal to $v$ composed with the canonical embedding $\text{Fin.cast}$ that adjusts the type from $\text{Fin}\, n$ to $\text{Fin}\, (0 + n)$.

Fin.append_assoc theorem

 {p : ℕ} (a : Fin m → α) (b : Fin n → α) (c : Fin p → α) :
  append (append a b) c = append a (append b c) ∘ Fin.cast (Nat.add_assoc ..)

Full source

theorem append_assoc {p : ℕ} (a : Fin m → α) (b : Fin n → α) (c : Fin p → α) :
    append (append a b) c = appendappend a (append b c) ∘ Fin.cast (Nat.add_assoc ..) := by
  ext i
  rw [Function.comp_apply]
  refine Fin.addCases (fun l => ?_) (fun r => ?_) i
  · rw [append_left]
    refine Fin.addCases (fun ll => ?_) (fun lr => ?_) l
    · rw [append_left]
      simp [castAdd_castAdd]
    · rw [append_right]
      simp [castAdd_natAdd]
  · rw [append_right]
    simp [← natAdd_natAdd]

Associativity of Tuple Concatenation

Informal description

For any tuples $a : \text{Fin}\, m \to \alpha$, $b : \text{Fin}\, n \to \alpha$, and $c : \text{Fin}\, p \to \alpha$, the concatenation of $a$ and $b$ followed by $c$ is equal to the concatenation of $a$ with the concatenation of $b$ and $c$, up to a cast that accounts for the associativity of addition on the indices. That is, $\text{append}\, (\text{append}\, a\, b)\, c = \text{append}\, a\, (\text{append}\, b\, c) \circ \text{Fin.cast}\, (\text{Nat.add\_assoc}\, \ldots)$.

Fin.append_left_eq_cons theorem

 {n : ℕ} (x₀ : Fin 1 → α) (x : Fin n → α) : Fin.append x₀ x = Fin.cons (x₀ 0) x ∘ Fin.cast (Nat.add_comm ..)

Full source

/-- Appending a one-tuple to the left is the same as `Fin.cons`. -/
theorem append_left_eq_cons {n : ℕ} (x₀ : Fin 1 → α) (x : Fin n → α) :
    Fin.append x₀ x = Fin.consFin.cons (x₀ 0) x ∘ Fin.cast (Nat.add_comm ..) := by
  ext i
  refine Fin.addCases ?_ ?_ i <;> clear i
  · intro i
    rw [Subsingleton.elim i 0, Fin.append_left, Function.comp_apply, eq_comm]
    exact Fin.cons_zero _ _
  · intro i
    rw [Fin.append_right, Function.comp_apply, Fin.cast_natAdd, eq_comm, Fin.addNat_one]
    exact Fin.cons_succ _ _ _

Concatenation of a Singleton Tuple is Equivalent to Prepending

Informal description

For any one-element tuple $x₀ : \text{Fin}\, 1 \to \alpha$ and any tuple $x : \text{Fin}\, n \to \alpha$, the concatenation $\text{Fin.append}\, x₀\, x$ is equal to the tuple obtained by prepending the first element of $x₀$ to $x$ (via $\text{Fin.cons}$), composed with a cast that accounts for the commutativity of addition on the indices.

Fin.cons_eq_append theorem

(x : α) (xs : Fin n → α) : cons x xs = append (cons x Fin.elim0) xs ∘ Fin.cast (Nat.add_comm ..)

Full source

/-- `Fin.cons` is the same as appending a one-tuple to the left. -/
theorem cons_eq_append (x : α) (xs : Fin n → α) :
    cons x xs = appendappend (cons x Fin.elim0) xs ∘ Fin.cast (Nat.add_comm ..) := by
  funext i; simp [append_left_eq_cons]

Prepending as Concatenation with Singleton Tuple

Informal description

For any element $x$ of type $\alpha$ and any tuple $xs : \text{Fin}\, n \to \alpha$, the tuple obtained by prepending $x$ to $xs$ (via $\text{Fin.cons}$) is equal to the concatenation of the singleton tuple $(x)$ with $xs$ (via $\text{Fin.append}$), composed with a cast that accounts for the commutativity of addition on the indices. In other words, we have: \[ \text{Fin.cons}\, x\, xs = \text{Fin.append}\, (\text{Fin.cons}\, x\, \text{Fin.elim0})\, xs \circ \text{Fin.cast}\, (\text{Nat.add\_comm}\, \ldots) \]

Fin.append_cast_left theorem

 {n m} (xs : Fin n → α) (ys : Fin m → α) (n' : ℕ) (h : n' = n) :
  Fin.append (xs ∘ Fin.cast h) ys = Fin.append xs ys ∘ (Fin.cast <| by rw [h])

Full source

@[simp] lemma append_cast_left {n m} (xs : Fin n → α) (ys : Fin m → α) (n' : ℕ)
    (h : n' = n) :
    Fin.append (xs ∘ Fin.cast h) ys = Fin.appendFin.append xs ys ∘ (Fin.cast <| by rw [h]) := by
  subst h; simp

Concatenation of Tuples is Preserved Under Left Casting

Informal description

Let $n$, $m$, and $n'$ be natural numbers, and let $h : n' = n$ be an equality. Given tuples $xs : \text{Fin}\, n \to \alpha$ and $ys : \text{Fin}\, m \to \alpha$, the concatenation of the casted tuple $xs \circ \text{Fin.cast}\, h$ with $ys$ is equal to the concatenation of $xs$ and $ys$ composed with a cast that rewrites $n'$ to $n$ using $h$.

Fin.append_cast_right theorem

 {n m} (xs : Fin n → α) (ys : Fin m → α) (m' : ℕ) (h : m' = m) :
  Fin.append xs (ys ∘ Fin.cast h) = Fin.append xs ys ∘ (Fin.cast <| by rw [h])

Full source

@[simp] lemma append_cast_right {n m} (xs : Fin n → α) (ys : Fin m → α) (m' : ℕ)
    (h : m' = m) :
    Fin.append xs (ys ∘ Fin.cast h) = Fin.appendFin.append xs ys ∘ (Fin.cast <| by rw [h]) := by
  subst h; simp

Right Cast Compatibility of Tuple Concatenation

Informal description

Let $n$ and $m$ be natural numbers, and let $xs : \text{Fin}\, n \to \alpha$ and $ys : \text{Fin}\, m \to \alpha$ be tuples. For any natural number $m'$ such that $m' = m$, the concatenation of $xs$ with the casted tuple $ys \circ \text{Fin.cast}\, h$ is equal to the concatenation of $xs$ and $ys$ composed with a cast that adjusts the index by $h$. More precisely, we have: \[ \text{Fin.append}\, xs\, (ys \circ \text{Fin.cast}\, h) = \text{Fin.append}\, xs\, ys \circ \text{Fin.cast}\, (h) \] where the cast on the right-hand side is applied to the concatenated index space $\text{Fin}\, (n + m')$ to match $\text{Fin}\, (n + m)$.

Fin.append_rev theorem

 {m n} (xs : Fin m → α) (ys : Fin n → α) (i : Fin (m + n)) :
  append xs ys (rev i) = append (ys ∘ rev) (xs ∘ rev) (i.cast (Nat.add_comm ..))

Full source

lemma append_rev {m n} (xs : Fin m → α) (ys : Fin n → α) (i : Fin (m + n)) :
    append xs ys (rev i) = append (ys ∘ rev) (xs ∘ rev) (i.cast (Nat.add_comm ..)) := by
  rcases rev_surjective i with ⟨i, rfl⟩
  rw [rev_rev]
  induction i using Fin.addCases
  · simp [rev_castAdd]
  · simp [cast_rev, rev_addNat]

Reversed Concatenation of Tuples via Order Reversal

Informal description

For any tuples $xs : \text{Fin}\, m \to \alpha$ and $ys : \text{Fin}\, n \to \alpha$, and any index $i \in \text{Fin}\, (m + n)$, the reversed concatenated tuple satisfies: \[ \text{append}\, xs\, ys\, (\text{rev}\, i) = \text{append}\, (ys \circ \text{rev})\, (xs \circ \text{rev})\, (i.\text{cast}\, (\text{Nat.add\_comm}\, m\, n)) \] where $\text{rev}$ denotes the order-reversing permutation of $\text{Fin}\, k$ for any $k$, and $\text{cast}$ adjusts the index according to the commutativity of addition $m + n = n + m$.

Fin.append_comp_rev theorem

 {m n} (xs : Fin m → α) (ys : Fin n → α) :
  append xs ys ∘ rev = append (ys ∘ rev) (xs ∘ rev) ∘ Fin.cast (Nat.add_comm ..)

Full source

lemma append_comp_rev {m n} (xs : Fin m → α) (ys : Fin n → α) :
    appendappend xs ys ∘ rev = appendappend (ys ∘ rev) (xs ∘ rev) ∘ Fin.cast (Nat.add_comm ..) :=
  funext <| append_rev xs ys

Reversed Concatenation Commutes with Tuple Reversal

Informal description

For any tuples $xs : \text{Fin}\, m \to \alpha$ and $ys : \text{Fin}\, n \to \alpha$, the composition of the concatenated tuple $\text{append}\, xs\, ys$ with the order-reversing permutation $\text{rev}$ is equal to the concatenation of the reversed tuples $ys \circ \text{rev}$ and $xs \circ \text{rev}$, composed with a cast that adjusts the index according to the commutativity of addition $m + n = n + m$. In other words, the following diagram commutes: \[ \text{append}\, xs\, ys \circ \text{rev} = \text{append}\, (ys \circ \text{rev})\, (xs \circ \text{rev}) \circ \text{Fin.cast}\, (\text{Nat.add\_comm}\, m\, n) \]

Fin.append_castAdd_natAdd theorem

{f : Fin (m + n) → α} : append (fun i ↦ f (castAdd n i)) (fun i ↦ f (natAdd m i)) = f

Full source

theorem append_castAdd_natAdd {f : Fin (m + n) → α} :
    append (fun i ↦ f (castAdd n i)) (fun i ↦ f (natAdd m i)) = f := by
  unfold append addCases
  simp

Concatenation of Split Tuples Equals Original Function

Informal description

For any function $f : \text{Fin}\, (m + n) \to \alpha$, the concatenation of the tuples obtained by restricting $f$ to the first $m$ elements (via $\text{castAdd}$) and the last $n$ elements (via $\text{natAdd}$) equals $f$ itself. That is, \[ \text{append}\, (\lambda i, f(\text{castAdd}\, n\, i))\, (\lambda i, f(\text{natAdd}\, m\, i)) = f. \]

Fin.repeat definition

(m : ℕ) (a : Fin n → α) : Fin (m * n) → α

Full source

/-- Repeat `a` `m` times. For example `Fin.repeat 2 ![0, 3, 7] = ![0, 3, 7, 0, 3, 7]`. -/
def «repeat» (m : ℕ) (a : Fin n → α) : Fin (m * n) → α
  | i => a i.modNat

Repeated tuple construction

Informal description

Given a natural number $m$ and a tuple $a : \text{Fin } n \to \alpha$, the function $\text{Fin.repeat } m \ a$ constructs a new tuple of length $m \cdot n$ by repeating the tuple $a$ exactly $m$ times. Specifically, for any index $i \in \text{Fin } (m \cdot n)$, the value at $i$ is given by $a (i \mod n)$, where $\mod$ is taken with respect to $n$.

Fin.repeat_apply theorem

(a : Fin n → α) (i : Fin (m * n)) : Fin.repeat m a i = a i.modNat

Full source

@[simp]
theorem repeat_apply (a : Fin n → α) (i : Fin (m * n)) :
    Fin.repeat m a i = a i.modNat :=
  rfl

Value of Repeated Tuple at Index $i$ is $a(i \mod n)$

Informal description

For any tuple $a : \text{Fin } n \to \alpha$ and any index $i \in \text{Fin } (m \cdot n)$, the value of the repeated tuple $\text{Fin.repeat } m \ a$ at index $i$ is equal to $a$ evaluated at $i \mod n$, where $\mod$ is taken with respect to $n$.

Fin.repeat_zero theorem

(a : Fin n → α) : Fin.repeat 0 a = Fin.elim0 ∘ Fin.cast (Nat.zero_mul _)

Full source

@[simp]
theorem repeat_zero (a : Fin n → α) :
    Fin.repeat 0 a = Fin.elim0Fin.elim0 ∘ Fin.cast (Nat.zero_mul _) :=
  funext fun x => (x.cast (Nat.zero_mul _)).elim0

Empty Repeated Tuple Construction: $\text{Fin.repeat } 0 \ a = \text{Fin.elim0}$

Informal description

For any tuple $a : \text{Fin } n \to \alpha$, the repeated tuple construction with $m = 0$ yields the empty tuple, i.e., $\text{Fin.repeat } 0 \ a = \text{Fin.elim0} \circ \text{Fin.cast } (0 \cdot n)$.

Fin.repeat_one theorem

(a : Fin n → α) : Fin.repeat 1 a = a ∘ Fin.cast (Nat.one_mul _)

Full source

@[simp]
theorem repeat_one (a : Fin n → α) : Fin.repeat 1 a = a ∘ Fin.cast (Nat.one_mul _) := by
  generalize_proofs h
  apply funext
  rw [(Fin.rightInverse_cast h.symm).surjective.forall]
  intro i
  simp [modNat, Nat.mod_eq_of_lt i.is_lt]

Repeated Tuple Construction with Single Repetition

Informal description

For any tuple $a : \text{Fin } n \to \alpha$, the repeated tuple construction with repetition count $1$ satisfies $\text{Fin.repeat } 1 \ a = a \circ \text{Fin.cast } (1 \cdot n = n)$, where $\text{Fin.cast}$ adjusts the indices to account for the equality $1 \cdot n = n$.

Fin.repeat_succ theorem

 (a : Fin n → α) (m : ℕ) :
  Fin.repeat m.succ a = append a (Fin.repeat m a) ∘ Fin.cast ((Nat.succ_mul _ _).trans (Nat.add_comm ..))

Full source

theorem repeat_succ (a : Fin n → α) (m : ℕ) :
    Fin.repeat m.succ a =
      appendappend a (Fin.repeat m a) ∘ Fin.cast ((Nat.succ_mul _ _).trans (Nat.add_comm ..)) := by
  generalize_proofs h
  apply funext
  rw [(Fin.rightInverse_cast h.symm).surjective.forall]
  refine Fin.addCases (fun l => ?_) fun r => ?_
  · simp [modNat, Nat.mod_eq_of_lt l.is_lt]
  · simp [modNat]

Recursive Construction of Repeated Tuples: $\text{repeat}(m+1)\, a = \text{append}\, a\, (\text{repeat}\, m\, a)$

Informal description

For any tuple $a : \text{Fin}\, n \to \alpha$ and natural number $m$, the repeated tuple construction satisfies \[ \text{Fin.repeat}\, (m + 1)\, a = \text{Fin.append}\, a\, (\text{Fin.repeat}\, m\, a) \circ \text{Fin.cast}\, (n + m \cdot n = (m + 1) \cdot n) \] where $\text{Fin.cast}$ adjusts the indices to account for the equality $n + m \cdot n = (m + 1) \cdot n$.

Fin.repeat_add theorem

 (a : Fin n → α) (m₁ m₂ : ℕ) :
  Fin.repeat (m₁ + m₂) a = append (Fin.repeat m₁ a) (Fin.repeat m₂ a) ∘ Fin.cast (Nat.add_mul ..)

Full source

@[simp]
theorem repeat_add (a : Fin n → α) (m₁ m₂ : ℕ) : Fin.repeat (m₁ + m₂) a =
    appendappend (Fin.repeat m₁ a) (Fin.repeat m₂ a) ∘ Fin.cast (Nat.add_mul ..) := by
  generalize_proofs h
  apply funext
  rw [(Fin.rightInverse_cast h.symm).surjective.forall]
  refine Fin.addCases (fun l => ?_) fun r => ?_
  · simp [modNat, Nat.mod_eq_of_lt l.is_lt]
  · simp [modNat, Nat.add_mod]

Additivity of Repeated Tuple Construction: $\text{repeat}(m_1 + m_2)\, a = \text{append}(\text{repeat}\, m_1\, a, \text{repeat}\, m_2\, a)$

Informal description

For any tuple $a : \text{Fin}\, n \to \alpha$ and natural numbers $m_1, m_2$, the repeated tuple construction satisfies \[ \text{Fin.repeat}\, (m_1 + m_2)\, a = \text{Fin.append}\, (\text{Fin.repeat}\, m_1\, a)\, (\text{Fin.repeat}\, m_2\, a) \circ \text{Fin.cast}\, (m_1 \cdot n + m_2 \cdot n = (m_1 + m_2) \cdot n) \] where $\text{Fin.cast}$ adjusts the indices to account for the equality $m_1 \cdot n + m_2 \cdot n = (m_1 + m_2) \cdot n$.

Fin.repeat_rev theorem

(a : Fin n → α) (k : Fin (m * n)) : Fin.repeat m a k.rev = Fin.repeat m (a ∘ Fin.rev) k

Full source

theorem repeat_rev (a : Fin n → α) (k : Fin (m * n)) :
    Fin.repeat m a k.rev = Fin.repeat m (a ∘ Fin.rev) k :=
  congr_arg a k.modNat_rev

Repeated Tuple Evaluation under Index Reversal: $\text{Fin.repeat } m \ a \circ \text{rev} = \text{Fin.repeat } m \ (a \circ \text{rev})$

Informal description

For any tuple $a : \text{Fin } n \to \alpha$ and any index $k \in \text{Fin } (m \cdot n)$, the value of the repeated tuple $\text{Fin.repeat } m \ a$ at the reversed index $k.\text{rev}$ is equal to the value of the repeated tuple $\text{Fin.repeat } m \ (a \circ \text{Fin.rev})$ at the original index $k$. In other words, reversing the index and then evaluating the repeated tuple is equivalent to evaluating the repeated tuple of the reversed original tuple at the original index.

Fin.repeat_comp_rev theorem

(a : Fin n → α) : Fin.repeat m a ∘ Fin.rev = Fin.repeat m (a ∘ Fin.rev)

Full source

theorem repeat_comp_rev (a : Fin n → α) :
    Fin.repeatFin.repeat m a ∘ Fin.rev = Fin.repeat m (a ∘ Fin.rev) :=
  funext <| repeat_rev a

Composition of Repeated Tuple with Index Reversal: $\text{repeat}\, m\, a \circ \text{rev} = \text{repeat}\, m\, (a \circ \text{rev})$

Informal description

For any tuple $a : \text{Fin}\, n \to \alpha$, the composition of the repeated tuple $\text{Fin.repeat}\, m\, a$ with the index reversal function $\text{Fin.rev}$ is equal to the repeated tuple of the composition $a \circ \text{Fin.rev}$, i.e., \[ \text{Fin.repeat}\, m\, a \circ \text{Fin.rev} = \text{Fin.repeat}\, m\, (a \circ \text{Fin.rev}). \]

Fin.init definition

(q : ∀ i, α i) (i : Fin n) : α i.castSucc

Full source

/-- The beginning of an `n+1` tuple, i.e., its first `n` entries -/
def init (q : ∀ i, α i) (i : Fin n) : α i.castSucc :=
  q i.castSucc

Initial segment of a tuple

Informal description

Given a dependent tuple $ q $ of length $ n+1 $ (i.e., $ q_i $ has type $ \alpha_i $ for each $ i : \text{Fin} (n+1) $), the function $ \text{Fin.init} $ returns the initial segment of length $ n $ by projecting $ q $ onto the first $ n $ indices via the cast $ i \mapsto i.\text{castSucc} $. In other words, $ \text{Fin.init} \, q $ is the tuple $ (q_0, \dots, q_{n-1}) $.

Fin.init_def theorem

{q : ∀ i, α i} : (init fun k : Fin (n + 1) ↦ q k) = fun k : Fin n ↦ q k.castSucc

Full source

theorem init_def {q : ∀ i, α i} :
    (init fun k : Fin (n + 1) ↦ q k) = fun k : Fin n ↦ q k.castSucc :=
  rfl

Definition of Initial Segment of a Tuple

Informal description

For any dependent tuple $q$ of length $n+1$ (i.e., $q_i$ has type $\alpha_i$ for each $i \in \text{Fin}(n+1)$), the initial segment $\text{init}(q)$ is equal to the function that maps each $k \in \text{Fin}(n)$ to $q_{k.\text{castSucc}}$. In other words, $\text{init}(q)(k) = q_{k.\text{castSucc}}$ for all $k \in \text{Fin}(n)$.

Fin.snoc definition

(p : ∀ i : Fin n, α i.castSucc) (x : α (last n)) (i : Fin (n + 1)) : α i

Full source

/-- Adding an element at the end of an `n`-tuple, to get an `n+1`-tuple. The name `snoc` comes from
`cons` (i.e., adding an element to the left of a tuple) read in reverse order. -/
def snoc (p : ∀ i : Fin n, α i.castSucc) (x : α (last n)) (i : Fin (n + 1)) : α i :=
  if h : i.val < n then _root_.cast (by rw [Fin.castSucc_castLT i h]) (p (castLT i h))
  else _root_.cast (by rw [eq_last_of_not_lt h]) x

Appending an element to a dependent tuple

Informal description

Given a dependent tuple $p$ of length $n$ where each element $p_i$ has type $\alpha_{i.\text{castSucc}}$, and an element $x$ of type $\alpha_{\text{last } n}$, the function $\text{snoc}$ constructs a new dependent tuple of length $n+1$ by appending $x$ at the end. For each index $i$ in $\text{Fin } (n+1)$, the value at $i$ is: - $p_{\text{castLT } i \text{ } h}$ (appropriately cast) if $i$ corresponds to an index less than $n$ (where $h$ is a proof that $i < n$), - $x$ (appropriately cast) if $i$ corresponds to the last index.

Fin.init_snoc theorem

: init (snoc p x) = p

Full source

@[simp]
theorem init_snoc : init (snoc p x) = p := by
  ext i
  simp only [init, snoc, coe_castSucc, is_lt, cast_eq, dite_true]
  convert cast_eq rfl (p i)

Initial Segment of Appended Tuple Equals Original Tuple

Informal description

For any dependent tuple $p$ of length $n$ and any element $x$ of type $\alpha_{\text{last } n}$, the initial segment of the tuple obtained by appending $x$ to $p$ via $\text{snoc}$ is equal to $p$ itself. That is, $\text{init}(\text{snoc}(p, x)) = p$.

Fin.snoc_castSucc theorem

: snoc p x i.castSucc = p i

Full source

@[simp]
theorem snoc_castSucc : snoc p x i.castSucc = p i := by
  simp only [snoc, coe_castSucc, is_lt, cast_eq, dite_true]
  convert cast_eq rfl (p i)

Value of Appended Tuple at Cast Successor Index

Informal description

For any dependent tuple $p$ of length $n$ where each element $p_i$ has type $\alpha_{i.\text{castSucc}}$, any element $x$ of type $\alpha_{\text{last } n}$, and any index $i$ in $\text{Fin } n$, the value of the appended tuple $\text{snoc}(p, x)$ at the cast successor index $i.\text{castSucc}$ is equal to $p_i$.

Fin.snoc_comp_castSucc theorem

{α : Sort*} {a : α} {f : Fin n → α} : (snoc f a : Fin (n + 1) → α) ∘ castSucc = f

Full source

@[simp]
theorem snoc_comp_castSucc {α : Sort*} {a : α} {f : Fin n → α} :
    (snoc f a : Fin (n + 1) → α) ∘ castSucc = f :=
  funext fun i ↦ by rw [Function.comp_apply, snoc_castSucc]

Composition of Appended Tuple with Cast Successor Recovers Original Function

Informal description

For any type $\alpha$, element $a \in \alpha$, and function $f \colon \text{Fin } n \to \alpha$, the composition of the appended tuple $\text{snoc}(f, a) \colon \text{Fin } (n+1) \to \alpha$ with the cast successor operation $\text{castSucc} \colon \text{Fin } n \to \text{Fin } (n+1)$ equals the original function $f$. That is, $(\text{snoc}(f, a)) \circ \text{castSucc} = f$.

Fin.snoc_last theorem

: snoc p x (last n) = x

Full source

@[simp]
theorem snoc_last : snoc p x (last n) = x := by simp [snoc]

Last Element of Appended Tuple: $\text{snoc } p \text{ } x \text{ } (\text{last } n) = x$

Informal description

For any dependent tuple $p$ of length $n$ and any element $x$ of type $\alpha_{\text{last } n}$, the function $\text{snoc}$ satisfies $\text{snoc } p \text{ } x \text{ } (\text{last } n) = x$. In other words, appending $x$ to the tuple $p$ results in a new tuple where the last element is exactly $x$.

Fin.snoc_zero theorem

{α : Sort*} (p : Fin 0 → α) (x : α) : Fin.snoc p x = fun _ ↦ x

Full source

lemma snoc_zero {α : Sort*} (p : Fin 0 → α) (x : α) :
    Fin.snoc p x = fun _ ↦ x := by
  ext y
  have : Subsingleton (Fin (0 + 1)) := Fin.subsingleton_one
  simp only [Subsingleton.elim y (Fin.last 0), snoc_last]

Constant Function from Empty Tuple via $\text{snoc}$

Informal description

For any type $\alpha$ and any element $x : \alpha$, the function $\text{snoc}$ applied to an empty tuple $p : \text{Fin } 0 \to \alpha$ and $x$ yields the constant function that maps every index to $x$, i.e., $\text{snoc } p \text{ } x = \lambda \_ \mapsto x$.

Fin.snoc_comp_nat_add theorem

 {n m : ℕ} {α : Sort*} (f : Fin (m + n) → α) (a : α) :
  (snoc f a : Fin _ → α) ∘ (natAdd m : Fin (n + 1) → Fin (m + n + 1)) = snoc (f ∘ natAdd m) a

Full source

@[simp]
theorem snoc_comp_nat_add {n m : ℕ} {α : Sort*} (f : Fin (m + n) → α) (a : α) :
    (snoc f a : Fin _ → α) ∘ (natAdd m : Fin (n + 1) → Fin (m + n + 1)) =
      snoc (f ∘ natAdd m) a := by
  ext i
  refine Fin.lastCases ?_ (fun i ↦ ?_) i
  · simp only [Function.comp_apply]
    rw [snoc_last, natAdd_last, snoc_last]
  · simp only [comp_apply, snoc_castSucc]
    rw [natAdd_castSucc, snoc_castSucc]

Composition of Extended Tuple with Index Shift via $\text{natAdd}$

Informal description

For any natural numbers $n$ and $m$, any type $\alpha$, and any function $f : \text{Fin}(m + n) \to \alpha$, the composition of the extended tuple $\text{snoc}(f, a)$ with the index shift $\text{natAdd } m$ is equal to the extension of the composition $f \circ \text{natAdd } m$ with $a$. In other words: $$(\text{snoc}(f, a)) \circ \text{natAdd } m = \text{snoc}(f \circ \text{natAdd } m, a)$$

Fin.snoc_cast_add theorem

 {α : Fin (n + m + 1) → Sort*} (f : ∀ i : Fin (n + m), α i.castSucc) (a : α (last (n + m))) (i : Fin n) :
  (snoc f a) (castAdd (m + 1) i) = f (castAdd m i)

Full source

@[simp]
theorem snoc_cast_add {α : Fin (n + m + 1) → Sort*} (f : ∀ i : Fin (n + m), α i.castSucc)
    (a : α (last (n + m))) (i : Fin n) : (snoc f a) (castAdd (m + 1) i) = f (castAdd m i) :=
  dif_pos _

Behavior of Extended Tuple under Index Shift: $\text{snoc}(f, a)(\text{castAdd}(m+1, i)) = f(\text{castAdd}(m, i))$

Informal description

Let $\alpha : \text{Fin}(n + m + 1) \to \text{Sort}^*$ be a type family, $f : \forall i : \text{Fin}(n + m), \alpha(i.\text{castSucc})$ a dependent tuple, and $a : \alpha(\text{last}(n + m))$ an element. For any $i : \text{Fin}(n)$, the value of the extended tuple $\text{snoc}(f, a)$ at the index $\text{castAdd}(m + 1, i)$ equals the value of $f$ at the index $\text{castAdd}(m, i)$. In other words, when we append $a$ to the tuple $f$ and then evaluate at a shifted index, it's equivalent to evaluating $f$ at the corresponding unshifted index.

Fin.snoc_comp_cast_add theorem

 {n m : ℕ} {α : Sort*} (f : Fin (n + m) → α) (a : α) : (snoc f a : Fin _ → α) ∘ castAdd (m + 1) = f ∘ castAdd m

Full source

@[simp]
theorem snoc_comp_cast_add {n m : ℕ} {α : Sort*} (f : Fin (n + m) → α) (a : α) :
    (snoc f a : Fin _ → α) ∘ castAdd (m + 1) = f ∘ castAdd m :=
  funext (snoc_cast_add _ _)

Composition of Extended Tuple with Index Shift: $(\text{snoc}(f, a)) \circ \text{castAdd}(m + 1) = f \circ \text{castAdd}(m)$

Informal description

For any natural numbers $n$ and $m$, and any type $\alpha$, given a function $f : \text{Fin}(n + m) \to \alpha$ and an element $a : \alpha$, the composition of the extended function $\text{snoc}(f, a) : \text{Fin}(n + m + 1) \to \alpha$ with the index shift $\text{castAdd}(m + 1)$ is equal to the composition of $f$ with the index shift $\text{castAdd}(m)$. In other words, $(\text{snoc}(f, a)) \circ \text{castAdd}(m + 1) = f \circ \text{castAdd}(m)$.

Fin.snoc_update theorem

: snoc (update p i y) x = update (snoc p x) i.castSucc y

Full source

/-- Updating a tuple and adding an element at the end commute. -/
@[simp]
theorem snoc_update : snoc (update p i y) x = update (snoc p x) i.castSucc y := by
  ext j
  cases j using lastCases with
  | cast j => rcases eq_or_ne j i with rfl | hne <;> simp [*]
  | last => simp [Ne.symm]

Commutation of Update and Append Operations on Dependent Tuples

Informal description

Let $p$ be a dependent tuple of length $n$ where each element $p_i$ has type $\alpha_{i.\text{castSucc}}$, and let $x$ be an element of type $\alpha_{\text{last } n}$. For any index $i \in \text{Fin } n$ and any element $y$ of type $\alpha_{i.\text{castSucc}}$, updating the tuple $p$ at index $i$ with $y$ and then appending $x$ is equivalent to first appending $x$ to $p$ and then updating the resulting tuple at the cast successor index $i.\text{castSucc}$ with $y$. In other words, the following equality holds: $$\text{snoc}(\text{update}(p, i, y), x) = \text{update}(\text{snoc}(p, x), i.\text{castSucc}, y)$$

Fin.update_snoc_last theorem

: update (snoc p x) (last n) z = snoc p z

Full source

/-- Adding an element at the beginning of a tuple and then updating it amounts to adding it
directly. -/
theorem update_snoc_last : update (snoc p x) (last n) z = snoc p z := by
  ext j
  cases j using lastCases <;> simp

Updating Last Element of Appended Tuple is Equivalent to Direct Appending

Informal description

For any dependent tuple $p$ of length $n$ where each element $p_i$ has type $\alpha_{i.\text{castSucc}}$, any element $x$ of type $\alpha_{\text{last } n}$, and any element $z$ of type $\alpha_{\text{last } n}$, updating the last element of the appended tuple $\text{snoc}(p, x)$ to $z$ is equivalent to directly appending $z$ to $p$. In other words: $$\text{update}(\text{snoc}(p, x), \text{last } n, z) = \text{snoc}(p, z)$$

Fin.snoc_injective2 theorem

: Function.Injective2 (@snoc n α)

Full source

/-- As a binary function, `Fin.snoc` is injective. -/
theorem snoc_injective2 : Function.Injective2 (@snoc n α) := fun x y xₙ yₙ h ↦
  ⟨funext fun i ↦ by simpa using congr_fun h (castSucc i), by simpa using congr_fun h (last n)⟩

Injectivity of the $\text{snoc}$ Function on Dependent Tuples

Informal description

The binary function $\text{snoc}$ that appends an element to a dependent tuple is injective. That is, for any two dependent tuples $p, q$ of length $n$ and any two elements $x, y$ of type $\alpha_{\text{last } n}$, if $\text{snoc}(p, x) = \text{snoc}(q, y)$, then $p = q$ and $x = y$.

Fin.snoc_inj theorem

{x y : ∀ i : Fin n, α i.castSucc} {xₙ yₙ : α (last n)} : snoc x xₙ = snoc y yₙ ↔ x = y ∧ xₙ = yₙ

Full source

@[simp]
theorem snoc_inj {x y : ∀ i : Fin n, α i.castSucc} {xₙ yₙ : α (last n)} :
    snocsnoc x xₙ = snoc y yₙ ↔ x = y ∧ xₙ = yₙ :=
  snoc_injective2.eq_iff

Injectivity of Tuple Appending: $\text{snoc}(x, x_n) = \text{snoc}(y, y_n) \iff x = y \land x_n = y_n$

Informal description

For any two dependent tuples $x, y$ of length $n$ (where each element $x_i, y_i$ has type $\alpha_{i.\text{castSucc}}$) and any two elements $x_n, y_n$ of type $\alpha_{\text{last } n}$, the appended tuples $\text{snoc}(x, x_n)$ and $\text{snoc}(y, y_n)$ are equal if and only if $x = y$ and $x_n = y_n$.

Fin.snoc_right_injective theorem

(x : ∀ i : Fin n, α i.castSucc) : Function.Injective (snoc x)

Full source

theorem snoc_right_injective (x : ∀ i : Fin n, α i.castSucc) :
    Function.Injective (snoc x) :=
  snoc_injective2.right _

Right Injectivity of Tuple Appending: $\text{snoc}(x, a) = \text{snoc}(x, b) \Rightarrow a = b$

Informal description

For any dependent tuple $x$ of length $n$ (where each element $x_i$ has type $\alpha_{i.\text{castSucc}}$), the function $\text{snoc}(x, \cdot)$ that appends an element to $x$ is injective. That is, for any two elements $a, b$ of type $\alpha_{\text{last } n}$, if $\text{snoc}(x, a) = \text{snoc}(x, b)$, then $a = b$.

Fin.snoc_left_injective theorem

(xₙ : α (last n)) : Function.Injective (snoc · xₙ)

Full source

theorem snoc_left_injective (xₙ : α (last n)) : Function.Injective (snoc · xₙ) :=
  snoc_injective2.left _

Left Injectivity of Tuple Appending: $\text{snoc}(p, x_n) = \text{snoc}(q, x_n) \Rightarrow p = q$

Informal description

For any element $x_n$ of type $\alpha_{\text{last } n}$, the function that appends $x_n$ to a dependent tuple is injective. That is, for any two dependent tuples $p, q$ of length $n$, if $\text{snoc}(p, x_n) = \text{snoc}(q, x_n)$, then $p = q$.

Fin.snoc_init_self theorem

: snoc (init q) (q (last n)) = q

Full source

/-- Concatenating the first element of a tuple with its tail gives back the original tuple -/
@[simp]
theorem snoc_init_self : snoc (init q) (q (last n)) = q := by
  ext j
  by_cases h : j.val < n
  · simp only [init, snoc, h, cast_eq, dite_true, castSucc_castLT]
  · rw [eq_last_of_not_lt h]
    simp

Reconstruction of Tuple via Initial Segment and Last Element: $\text{snoc} (\text{init } q) (q (\text{last } n)) = q$

Informal description

For any dependent tuple $q$ of length $n+1$ (i.e., $q_i$ has type $\alpha_i$ for each $i \in \text{Fin} (n+1)$), appending the last element of $q$ to the initial segment of $q$ reconstructs the original tuple. That is, $\text{snoc} (\text{init } q) (q (\text{last } n)) = q$.

Fin.init_update_last theorem

: init (update q (last n) z) = init q

Full source

/-- Updating the last element of a tuple does not change the beginning. -/
@[simp]
theorem init_update_last : init (update q (last n) z) = init q := by
  ext j
  simp [init, Fin.ne_of_lt]

Initial Segment Unchanged by Last Element Update

Informal description

For any dependent tuple $q$ of length $n+1$ (i.e., $q_i$ has type $\alpha_i$ for each $i \in \text{Fin} (n+1)$) and any element $z$ of type $\alpha (\text{last } n)$, updating the last element of $q$ to $z$ does not change its initial segment. That is, $\text{init}(\text{update } q (\text{last } n) z) = \text{init } q$.

Fin.init_update_castSucc theorem

: init (update q i.castSucc y) = update (init q) i y

Full source

/-- Updating an element and taking the beginning commute. -/
@[simp]
theorem init_update_castSucc : init (update q i.castSucc y) = update (init q) i y := by
  ext j
  by_cases h : j = i
  · rw [h]
    simp [init]
  · simp [init, h, castSucc_inj]

Commutation of Initial Segment and Update via CastSucc

Informal description

For a dependent tuple $ q $ of length $ n+1 $ (i.e., $ q_i $ has type $ \alpha_i $ for each $ i : \text{Fin} (n+1) $), updating the $ i $-th element (via $ i.\text{castSucc} $) to $ y $ and then taking the initial segment of length $ n $ is equivalent to first taking the initial segment and then updating the $ i $-th element to $ y $. In other words, the following equality holds: \[ \text{init} (\text{update } q (i.\text{castSucc}) y) = \text{update } (\text{init } q) i y \]

Fin.tail_init_eq_init_tail theorem

{β : Sort*} (q : Fin (n + 2) → β) : tail (init q) = init (tail q)

Full source

/-- `tail` and `init` commute. We state this lemma in a non-dependent setting, as otherwise it
would involve a cast to convince Lean that the two types are equal, making it harder to use. -/
theorem tail_init_eq_init_tail {β : Sort*} (q : Fin (n + 2) → β) :
    tail (init q) = init (tail q) := by
  ext i
  simp [tail, init, castSucc_fin_succ]

Commutativity of Tail and Initial Segment Operations on Tuples

Informal description

For any tuple $q$ of length $n+2$ with elements in a type $\beta$, the tail of the initial segment of $q$ is equal to the initial segment of the tail of $q$. In other words, removing the first element after taking the first $n+1$ elements is the same as taking the first $n+1$ elements after removing the first element.

Fin.cons_snoc_eq_snoc_cons theorem

{β : Sort*} (a : β) (q : Fin n → β) (b : β) : @cons n.succ (fun _ ↦ β) a (snoc q b) = snoc (cons a q) b

Full source

/-- `cons` and `snoc` commute. We state this lemma in a non-dependent setting, as otherwise it
would involve a cast to convince Lean that the two types are equal, making it harder to use. -/
theorem cons_snoc_eq_snoc_cons {β : Sort*} (a : β) (q : Fin n → β) (b : β) :
    @cons n.succ (fun _ ↦ β) a (snoc q b) = snoc (cons a q) b := by
  ext i
  by_cases h : i = 0
  · simp [h, snoc, castLT]
  set j := pred i h with ji
  have : i = j.succ := by rw [ji, succ_pred]
  rw [this, cons_succ]
  by_cases h' : j.val < n
  · set k := castLT j h' with jk
    have : j = castSucc k := by rw [jk, castSucc_castLT]
    rw [this, ← castSucc_fin_succ, snoc]
    simp [pred, snoc, cons]
  rw [eq_last_of_not_lt h', succ_last]
  simp

Commutation of Prepend and Append Operations on Tuples: $\text{cons}(a, \text{snoc}(q, b)) = \text{snoc}(\text{cons}(a, q), b)$

Informal description

For any type $\beta$, element $a \in \beta$, tuple $q : \text{Fin } n \to \beta$, and element $b \in \beta$, the following equality holds: \[ \text{cons}(a, \text{snoc}(q, b)) = \text{snoc}(\text{cons}(a, q), b) \] where: - $\text{cons}(a, q')$ prepends $a$ to a tuple $q'$ of length $n+1$, - $\text{snoc}(q', b)$ appends $b$ to a tuple $q'$ of length $n$.

Fin.comp_snoc theorem

{α : Sort*} {β : Sort*} (g : α → β) (q : Fin n → α) (y : α) : g ∘ snoc q y = snoc (g ∘ q) (g y)

Full source

theorem comp_snoc {α : Sort*} {β : Sort*} (g : α → β) (q : Fin n → α) (y : α) :
    g ∘ snoc q y = snoc (g ∘ q) (g y) := by
  ext j
  by_cases h : j.val < n
  · simp [h, snoc, castSucc_castLT]
  · rw [eq_last_of_not_lt h]
    simp

Composition with Snoc: $g \circ (\text{snoc}\, q\, y) = \text{snoc}\, (g \circ q)\, (g\, y)$

Informal description

For any function $g : \alpha \to \beta$, any tuple $q : \text{Fin}\, n \to \alpha$, and any element $y : \alpha$, the composition of $g$ with the tuple obtained by appending $y$ to $q$ is equal to the tuple obtained by appending $g(y)$ to the composition $g \circ q$. That is, $g \circ (\text{snoc}\, q\, y) = \text{snoc}\, (g \circ q)\, (g\, y)$.

Fin.append_right_eq_snoc theorem

{α : Sort*} {n : ℕ} (x : Fin n → α) (x₀ : Fin 1 → α) : Fin.append x x₀ = Fin.snoc x (x₀ 0)

Full source

/-- Appending a one-tuple to the right is the same as `Fin.snoc`. -/
theorem append_right_eq_snoc {α : Sort*} {n : ℕ} (x : Fin n → α) (x₀ : Fin 1 → α) :
    Fin.append x x₀ = Fin.snoc x (x₀ 0) := by
  ext i
  refine Fin.addCases ?_ ?_ i <;> clear i
  · intro i
    rw [Fin.append_left]
    exact (@snoc_castSucc _ (fun _ => α) _ _ i).symm
  · intro i
    rw [Subsingleton.elim i 0, Fin.append_right]
    exact (@snoc_last _ (fun _ => α) _ _).symm

Concatenation with Singleton Tuple Equals Snoc: $\text{append}\, x\, x_0 = \text{snoc}\, x\, (x_0\, 0)$

Informal description

For any tuple $x$ of length $n$ (i.e., a function $x : \text{Fin}\, n \to \alpha$) and any one-element tuple $x_0$ (i.e., a function $x_0 : \text{Fin}\, 1 \to \alpha$), the concatenation $\text{append}\, x\, x_0$ is equal to appending the single element $x_0(0)$ to $x$ via $\text{snoc}$. That is, $\text{append}\, x\, x_0 = \text{snoc}\, x\, (x_0\, 0)$.

Fin.snoc_eq_append theorem

{α : Sort*} (xs : Fin n → α) (x : α) : snoc xs x = append xs (cons x Fin.elim0)

Full source

/-- `Fin.snoc` is the same as appending a one-tuple -/
theorem snoc_eq_append {α : Sort*} (xs : Fin n → α) (x : α) :
    snoc xs x = append xs (cons x Fin.elim0) :=
  (append_right_eq_snoc xs (cons x Fin.elim0)).symm

Snoc Equals Append with Singleton: $\text{snoc}\, xs\, x = \text{append}\, xs\, (\text{cons}\, x\, \text{elim0})$

Informal description

For any tuple $xs$ of length $n$ (i.e., a function $xs : \text{Fin}\, n \to \alpha$) and any element $x : \alpha$, the tuple obtained by appending $x$ to $xs$ via $\text{snoc}$ is equal to the concatenation of $xs$ with the singleton tuple containing $x$. That is, $\text{snoc}\, xs\, x = \text{append}\, xs\, (\text{cons}\, x\, \text{elim0})$.

Fin.append_left_snoc theorem

 {n m} {α : Sort*} (xs : Fin n → α) (x : α) (ys : Fin m → α) :
  Fin.append (Fin.snoc xs x) ys = Fin.append xs (Fin.cons x ys) ∘ Fin.cast (Nat.succ_add_eq_add_succ ..)

Full source

theorem append_left_snoc {n m} {α : Sort*} (xs : Fin n → α) (x : α) (ys : Fin m → α) :
    Fin.append (Fin.snoc xs x) ys =
      Fin.appendFin.append xs (Fin.cons x ys) ∘ Fin.cast (Nat.succ_add_eq_add_succ ..) := by
  rw [snoc_eq_append, append_assoc, append_left_eq_cons, append_cast_right]; rfl

Concatenation of Snoc-Appended Tuples Equals Cons-Prepended Tuples with Cast Adjustment

Informal description

For any tuples $xs : \text{Fin}\, n \to \alpha$, $x : \alpha$, and $ys : \text{Fin}\, m \to \alpha$, the concatenation of the tuple obtained by appending $x$ to $xs$ (via $\text{snoc}$) with $ys$ is equal to the concatenation of $xs$ with the tuple obtained by prepending $x$ to $ys$ (via $\text{cons}$), composed with a cast that accounts for the natural number identity $(n + 1) + m = n + (m + 1)$. In symbols: \[ \text{append}\, (\text{snoc}\, xs\, x)\, ys = \text{append}\, xs\, (\text{cons}\, x\, ys) \circ \text{Fin.cast}\, (n + 1 + m = n + (m + 1)) \]

Fin.append_right_cons theorem

 {n m} {α : Sort*} (xs : Fin n → α) (y : α) (ys : Fin m → α) :
  Fin.append xs (Fin.cons y ys) = Fin.append (Fin.snoc xs y) ys ∘ Fin.cast (Nat.succ_add_eq_add_succ ..).symm

Full source

theorem append_right_cons {n m} {α : Sort*} (xs : Fin n → α) (y : α) (ys : Fin m → α) :
    Fin.append xs (Fin.cons y ys) =
      Fin.appendFin.append (Fin.snoc xs y) ys ∘ Fin.cast (Nat.succ_add_eq_add_succ ..).symm := by
  rw [append_left_snoc]; rfl

Concatenation with Prepended Tuple Equals Appended Tuple Concatenation with Cast Adjustment

Informal description

For any tuples $xs : \text{Fin}\, n \to \alpha$, $y : \alpha$, and $ys : \text{Fin}\, m \to \alpha$, the concatenation of $xs$ with the tuple obtained by prepending $y$ to $ys$ (via $\text{cons}$) is equal to the concatenation of the tuple obtained by appending $y$ to $xs$ (via $\text{snoc}$) with $ys$, composed with a cast that accounts for the natural number identity $(n + (m + 1) = (n + 1) + m)$. In symbols: \[ \text{append}\, xs\, (\text{cons}\, y\, ys) = \text{append}\, (\text{snoc}\, xs\, y)\, ys \circ \text{Fin.cast}\, (n + (m + 1) = (n + 1) + m) \]

Fin.append_cons theorem

 {α : Sort*} (a : α) (as : Fin n → α) (bs : Fin m → α) :
  Fin.append (cons a as) bs = cons a (Fin.append as bs) ∘ (Fin.cast <| Nat.add_right_comm n 1 m)

Full source

theorem append_cons {α : Sort*} (a : α) (as : Fin n → α) (bs : Fin m → α) :
    Fin.append (cons a as) bs
    = conscons a (Fin.append as bs) ∘ (Fin.cast <| Nat.add_right_comm n 1 m) := by
  funext i
  rcases i with ⟨i, -⟩
  simp only [append, addCases, cons, castLT, cast, comp_apply]
  rcases i with - | i
  · simp
  · split_ifs with h
    · have : i < n := Nat.lt_of_succ_lt_succ h
      simp [addCases, this]
    · have : ¬i < n := Nat.not_le.mpr <| Nat.lt_succ.mp <| Nat.not_le.mp h
      simp [addCases, this]

Concatenation of Prepended Tuples with Cast Adjustment

Informal description

Let $\alpha$ be a type, $a$ an element of $\alpha$, and $as : \text{Fin}\, n \to \alpha$ and $bs : \text{Fin}\, m \to \alpha$ be tuples. Then the concatenation of the tuple obtained by prepending $a$ to $as$ with $bs$ is equal to the tuple obtained by prepending $a$ to the concatenation of $as$ and $bs$, composed with a cast function that adjusts the indices according to the natural number identity $(n + 1) + m = n + (1 + m)$. In symbols: \[ \text{Fin.append}\, (\text{cons}\, a\, as)\, bs = \text{cons}\, a\, (\text{Fin.append}\, as\, bs) \circ \text{Fin.cast}\, (n + 1 + m = n + (1 + m)) \]

Fin.append_snoc theorem

{α : Sort*} (as : Fin n → α) (bs : Fin m → α) (b : α) : Fin.append as (snoc bs b) = snoc (Fin.append as bs) b

Full source

theorem append_snoc {α : Sort*} (as : Fin n → α) (bs : Fin m → α) (b : α) :
    Fin.append as (snoc bs b) = snoc (Fin.append as bs) b := by
  funext i
  rcases i with ⟨i, isLt⟩
  simp only [append, addCases, castLT, cast_mk, subNat_mk, natAdd_mk, cast, snoc.eq_1,
    cast_eq, eq_rec_constant, Nat.add_eq, Nat.add_zero, castLT_mk]
  split_ifs with lt_n lt_add sub_lt nlt_add lt_add <;> (try rfl)
  · have := Nat.lt_add_right m lt_n
    contradiction
  · obtain rfl := Nat.eq_of_le_of_lt_succ (Nat.not_lt.mp nlt_add) isLt
    simp [Nat.add_comm n m] at sub_lt
  · have := Nat.sub_lt_left_of_lt_add (Nat.not_lt.mp lt_n) lt_add
    contradiction

Concatenation and Appending Commute: $\text{append}\, a\, (\text{snoc}\, b\, x) = \text{snoc}\, (\text{append}\, a\, b)\, x$

Informal description

For any tuples $a : \text{Fin}\, n \to \alpha$ and $b : \text{Fin}\, m \to \alpha$, and any element $x : \alpha$, the concatenation of $a$ with the tuple obtained by appending $x$ to $b$ is equal to the tuple obtained by appending $x$ to the concatenation of $a$ and $b$. In symbols: $\text{append}\, a\, (\text{snoc}\, b\, x) = \text{snoc}\, (\text{append}\, a\, b)\, x$.

Fin.comp_init theorem

{α : Sort*} {β : Sort*} (g : α → β) (q : Fin n.succ → α) : g ∘ init q = init (g ∘ q)

Full source

theorem comp_init {α : Sort*} {β : Sort*} (g : α → β) (q : Fin n.succ → α) :
    g ∘ init q = init (g ∘ q) := by
  ext j
  simp [init]

Composition Commutes with Initial Segment of Tuples

Informal description

For any function $g : \alpha \to \beta$ and any tuple $q : \text{Fin} (n+1) \to \alpha$, the composition of $g$ with the initial segment of $q$ is equal to the initial segment of the composition $g \circ q$. In other words, applying $g$ to each element of $\text{init}\, q$ is the same as taking the initial segment of the tuple obtained by applying $g$ to each element of $q$.

Fin.snocEquiv definition

(α : Fin (n + 1) → Type*) : α (last n) × (∀ i, α (castSucc i)) ≃ ∀ i, α i

Full source

/-- Equivalence between tuples of length `n + 1` and pairs of an element and a tuple of length `n`
given by separating out the last element of the tuple.

This is `Fin.snoc` as an `Equiv`. -/
@[simps]
def snocEquiv (α : Fin (n + 1) → Type*) : α (last n) × (∀ i, α (castSucc i))α (last n) × (∀ i, α (castSucc i)) ≃ ∀ i, α i where
  toFun f _ := Fin.snoc f.2 f.1 _
  invFun f := ⟨f _, Fin.init f⟩
  left_inv f := by simp
  right_inv f := by simp

Equivalence between tuples and pairs of last element and initial segment

Informal description

The equivalence `Fin.snocEquiv` establishes a bijection between dependent tuples of length `n + 1` (i.e., functions `∀ i : Fin (n + 1), α i`) and pairs consisting of an element of type `α (last n)` (the last component) and a dependent tuple of length `n` (the initial segment). Specifically: - The forward direction (`toFun`) takes a pair `(x, xs)` where `x : α (last n)` and `xs : ∀ i : Fin n, α (castSucc i)`, and constructs the tuple `Fin.snoc xs x` of length `n + 1`. - The reverse direction (`invFun`) decomposes a tuple `f : ∀ i : Fin (n + 1), α i` into the pair `(f (last n), Fin.init f)`, where `Fin.init f` is the initial segment of `f` (a tuple of length `n`). This equivalence is a formalization of the intuitive idea that a tuple of length `n + 1` can be uniquely split into its last element and the remaining initial segment of length `n`.

Fin.snocCases definition

{P : (∀ i : Fin n.succ, α i) → Sort*} (h : ∀ xs x, P (Fin.snoc xs x)) (x : ∀ i : Fin n.succ, α i) : P x

Full source

/-- Recurse on an `n+1`-tuple by splitting it its initial `n`-tuple and its last element. -/
@[elab_as_elim, inline]
def snocCases {P : (∀ i : Fin n.succ, α i) → Sort*}
    (h : ∀ xs x, P (Fin.snoc xs x))
    (x : ∀ i : Fin n.succ, α i) : P x :=
  _root_.cast (by rw [Fin.snoc_init_self]) <| h (Fin.init x) (x <| Fin.last _)

Case analysis for dependent tuples via initial segment and last element

Informal description

Given a dependent tuple $ x $ of length $ n+1 $ (i.e., $ x_i $ has type $ \alpha_i $ for each $ i : \text{Fin} (n+1) $), the function `Fin.snocCases` allows one to perform case analysis on $ x $ by decomposing it into its initial segment `Fin.init x` (a tuple of length $ n $) and its last element $ x (\text{last } n) $. Specifically, for any predicate $ P $ on dependent tuples of length $ n+1 $, if $ P $ holds for all tuples constructed via `Fin.snoc` (i.e., for all pairs of an initial segment and a last element), then $ P $ holds for any dependent tuple $ x $.

Fin.snocCases_snoc theorem

 {P : (∀ i : Fin (n + 1), α i) → Sort*} (h : ∀ x x₀, P (Fin.snoc x x₀)) (x : ∀ i : Fin n, (Fin.init α) i)
  (x₀ : α (Fin.last _)) : snocCases h (Fin.snoc x x₀) = h x x₀

Full source

@[simp] lemma snocCases_snoc
    {P : (∀ i : Fin (n+1), α i) → Sort*} (h : ∀ x x₀, P (Fin.snoc x x₀))
    (x : ∀ i : Fin n, (Fin.init α) i) (x₀ : α (Fin.last _)) :
    snocCases h (Fin.snoc x x₀) = h x x₀ := by
  rw [snocCases, cast_eq_iff_heq, Fin.init_snoc, Fin.snoc_last]

Computation Rule for $\text{snocCases}$ on Appended Tuples

Informal description

For any predicate $ P $ on dependent tuples of length $ n+1 $, if $ h $ is a proof that $ P $ holds for all tuples constructed by appending an element $ x_0 $ to a tuple $ x $ via $\text{snoc}$, then applying $\text{snocCases}$ to $ h $ and the tuple $\text{snoc}\,x\,x_0$ yields $ h\,x\,x_0 $. In other words, $\text{snocCases}\,h\,(\text{snoc}\,x\,x_0) = h\,x\,x_0$.

Fin.snocInduction definition

 {α : Sort*} {P : ∀ {n : ℕ}, (Fin n → α) → Sort*} (h0 : P Fin.elim0)
  (h : ∀ {n} (x : Fin n → α) (x₀), P x → P (Fin.snoc x x₀)) : ∀ {n : ℕ} (x : Fin n → α), P x

Full source

/-- Recurse on a tuple by splitting into `Fin.elim0` and `Fin.snoc`. -/
@[elab_as_elim]
def snocInduction {α : Sort*}
    {P : ∀ {n : ℕ}, (Fin n → α) → Sort*}
    (h0 : P Fin.elim0)
    (h : ∀ {n} (x : Fin n → α) (x₀), P x → P (Fin.snoc x x₀)) : ∀ {n : ℕ} (x : Fin n → α), P x
  | 0, x => by convert h0
  | _ + 1, x => snocCases (fun _ _ ↦ h _ _ <| snocInduction h0 h _) x

Induction principle for tuples via appending elements

Informal description

The function `Fin.snocInduction` provides an induction principle for tuples indexed by `Fin n`. Given a base case `h0` for the empty tuple `Fin.elim0` and an inductive step `h` that extends a tuple of length `n` by appending an element to form a tuple of length `n + 1`, the function allows proving a property `P` for all tuples of any length `n`. More precisely: - For the empty tuple (case `n = 0`), the property `P` holds by `h0`. - For a tuple `x` of length `n + 1`, the property `P` is established by decomposing `x` into its initial segment (of length `n`) and last element, then applying the inductive step `h`. This induction principle is particularly useful for reasoning about operations that build tuples by successively appending elements.

Fin.succAboveCases definition

 {α : Fin (n + 1) → Sort u} (i : Fin (n + 1)) (x : α i) (p : ∀ j : Fin n, α (i.succAbove j)) (j : Fin (n + 1)) : α j

Full source

/-- Define a function on `Fin (n + 1)` from a value on `i : Fin (n + 1)` and values on each
`Fin.succAbove i j`, `j : Fin n`. This version is elaborated as eliminator and works for
propositions, see also `Fin.insertNth` for a version without an `@[elab_as_elim]`
attribute. -/
@[elab_as_elim]
def succAboveCases {α : Fin (n + 1) → Sort u} (i : Fin (n + 1)) (x : α i)
    (p : ∀ j : Fin n, α (i.succAbove j)) (j : Fin (n + 1)) : α j :=
  if hj : j = i then Eq.rec x hj.symm
  else
    if hlt : j < i then @Eq.recOn _ _ (fun x _ ↦ α x) _ (succAbove_castPred_of_lt _ _ hlt) (p _)
    else @Eq.recOn _ _ (fun x _ ↦ α x) _ (succAbove_pred_of_lt _ _ <|
    (Fin.lt_or_lt_of_ne hj).resolve_left hlt) (p _)

Induction principle for $\text{Fin}(n+1)$ via $\text{succAbove}$

Informal description

Given a family of types $\alpha$ indexed by $\text{Fin}(n+1)$, an element $i \in \text{Fin}(n+1)$, a value $x \in \alpha_i$, and a function $p$ that assigns to each $j \in \text{Fin}(n)$ a value in $\alpha_{i.\text{succAbove}\,j}$, the function $\text{succAboveCases}$ constructs a value in $\alpha_j$ for any $j \in \text{Fin}(n+1)$. Specifically, for any $j \in \text{Fin}(n+1)$: - If $j = i$, it returns $x$. - If $j < i$, it returns $p$ applied to the predecessor of $j$ under the condition $j < i$. - Otherwise, it returns $p$ applied to the predecessor of $j$ under the condition $i < j$. This serves as an induction/recursion principle for $\text{Fin}(n+1)$, allowing one to define or prove properties for all elements of $\text{Fin}(n+1)$ by specifying values at $i$ and at all $\text{succAbove}\,i\,j$ for $j \in \text{Fin}(n)$.

Fin.forall_iff_castSucc theorem

{P : Fin (n + 1) → Prop} : (∀ i, P i) ↔ P (last n) ∧ ∀ i : Fin n, P i.castSucc

Full source

lemma forall_iff_castSucc {P : Fin (n + 1) → Prop} :
    (∀ i, P i) ↔ P (last n) ∧ ∀ i : Fin n, P i.castSucc :=
  ⟨fun h ↦ ⟨h _, fun _ ↦ h _⟩, fun h ↦ lastCases h.1 h.2⟩

Universal Quantification on $\text{Fin}(n+1)$ via Last Element and Cast Succ

Informal description

For any predicate $P$ on $\text{Fin}(n+1)$, the universal quantification $\forall i, P(i)$ holds if and only if $P$ holds at the last element $\text{last}(n)$ and for all $i \in \text{Fin}(n)$, $P$ holds at the casted element $i.\text{castSucc}$.

Fin.exists_iff_castSucc theorem

{P : Fin (n + 1) → Prop} : (∃ i, P i) ↔ P (last n) ∨ ∃ i : Fin n, P i.castSucc

Full source

lemma exists_iff_castSucc {P : Fin (n + 1) → Prop} :
    (∃ i, P i) ↔ P (last n) ∨ ∃ i : Fin n, P i.castSucc where
  mp := by
    rintro ⟨i, hi⟩
    induction' i using lastCases
    · exact .inl hi
    · exact .inr ⟨_, hi⟩
  mpr := by rintro (h | ⟨i, hi⟩) <;> exact ⟨_, ‹_›⟩

Existence Criterion via Cast Successor in Finite Types

Informal description

For any predicate $P$ on the finite type $\text{Fin}(n+1)$, the existence of an index $i$ satisfying $P(i)$ is equivalent to either $P$ holding at the last index $\text{last}(n)$, or there exists an index $j \in \text{Fin}(n)$ such that $P$ holds at the cast successor $j.\text{castSucc}$.

Fin.forall_iff_succAbove theorem

{P : Fin (n + 1) → Prop} (p : Fin (n + 1)) : (∀ i, P i) ↔ P p ∧ ∀ i, P (p.succAbove i)

Full source

theorem forall_iff_succAbove {P : Fin (n + 1) → Prop} (p : Fin (n + 1)) :
    (∀ i, P i) ↔ P p ∧ ∀ i, P (p.succAbove i) :=
  ⟨fun h ↦ ⟨h _, fun _ ↦ h _⟩, fun h ↦ succAboveCases p h.1 h.2⟩

Universal Quantification on $\text{Fin}(n+1)$ via Pivot and $\text{succAbove}$

Informal description

For any predicate $P$ on $\text{Fin}(n+1)$ and any pivot element $p \in \text{Fin}(n+1)$, the universal quantification $\forall i, P(i)$ holds if and only if $P(p)$ holds and for all $i \in \text{Fin}(n)$, $P$ holds at $p.\text{succAbove}\,i$.

Fin.exists_iff_succAbove theorem

{P : Fin (n + 1) → Prop} (p : Fin (n + 1)) : (∃ i, P i) ↔ P p ∨ ∃ i, P (p.succAbove i)

Full source

lemma exists_iff_succAbove {P : Fin (n + 1) → Prop} (p : Fin (n + 1)) :
    (∃ i, P i) ↔ P p ∨ ∃ i, P (p.succAbove i) where
  mp := by
    rintro ⟨i, hi⟩
    induction' i using p.succAboveCases
    · exact .inl hi
    · exact .inr ⟨_, hi⟩
  mpr := by rintro (h | ⟨i, hi⟩) <;> exact ⟨_, ‹_›⟩

Existence Criterion via $\text{succAbove}$ in Finite Types

Informal description

For any predicate $P$ on the finite type $\text{Fin}(n+1)$ and any pivot index $p \in \text{Fin}(n+1)$, the following equivalence holds: there exists an index $i$ satisfying $P(i)$ if and only if either $P(p)$ holds or there exists an index $j \in \text{Fin}(n)$ such that $P$ holds at the index obtained by applying the $\text{succAbove}$ operation to $p$ and $j$.

Fin.removeNth definition

(p : Fin (n + 1)) (f : ∀ i, α i) : ∀ i, α (p.succAbove i)

Full source

/-- Remove the `p`-th entry of a tuple. -/
def removeNth (p : Fin (n + 1)) (f : ∀ i, α i) : ∀ i, α (p.succAbove i) := fun i ↦ f (p.succAbove i)

Removing an entry from a dependent tuple at a pivot index

Informal description

For a pivot index $p$ in $\text{Fin}(n+1)$ and a dependent tuple $f$ where each element $f_i$ has type $\alpha_i$, the operation $\text{removeNth}$ produces a new tuple by removing the $p$-th entry. Specifically, for each index $i$ in $\text{Fin}(n)$, the new tuple at position $i$ is $f$ evaluated at the index obtained by applying the $\text{succAbove}$ operation to $p$ and $i$, i.e., $f(\text{succAbove}(p, i))$.

Fin.insertNth definition

(i : Fin (n + 1)) (x : α i) (p : ∀ j : Fin n, α (i.succAbove j)) (j : Fin (n + 1)) : α j

Full source

/-- Insert an element into a tuple at a given position. For `i = 0` see `Fin.cons`,
for `i = Fin.last n` see `Fin.snoc`. See also `Fin.succAboveCases` for a version elaborated
as an eliminator. -/
def insertNth (i : Fin (n + 1)) (x : α i) (p : ∀ j : Fin n, α (i.succAbove j)) (j : Fin (n + 1)) :
    α j :=
  succAboveCases i x p j

Insertion into a dependent tuple at a pivot index

Informal description

Given a pivot index $i \in \text{Fin}(n+1)$, an element $x \in \alpha_i$, and a dependent tuple $p$ where each $p_j$ has type $\alpha_{i.\text{succAbove}\,j}$ for $j \in \text{Fin}(n)$, the function $\text{insertNth}$ constructs a new tuple of type $\forall j \in \text{Fin}(n+1), \alpha_j$ by inserting $x$ at position $i$ and shifting the remaining elements according to $\text{succAbove}$. Specifically: - For $j = i$, it returns $x$. - For $j \neq i$, it returns $p_k$ where $k$ is the index obtained by applying $\text{succAbove}$ to $i$ and $j$.

Fin.insertNth_apply_same theorem

(i : Fin (n + 1)) (x : α i) (p : ∀ j, α (i.succAbove j)) : insertNth i x p i = x

Full source

@[simp]
theorem insertNth_apply_same (i : Fin (n + 1)) (x : α i) (p : ∀ j, α (i.succAbove j)) :
    insertNth i x p i = x := by simp [insertNth, succAboveCases]

Insertion at Pivot Index Preserves Element Value

Informal description

For any pivot index $i \in \text{Fin}(n+1)$, element $x \in \alpha_i$, and dependent tuple $p$ where each $p_j$ has type $\alpha_{i.\text{succAbove}\,j}$ for $j \in \text{Fin}(n)$, the function $\text{insertNth}$ satisfies $\text{insertNth}\,i\,x\,p\,i = x$.

Fin.insertNth_apply_succAbove theorem

(i : Fin (n + 1)) (x : α i) (p : ∀ j, α (i.succAbove j)) (j : Fin n) : insertNth i x p (i.succAbove j) = p j

Full source

@[simp]
theorem insertNth_apply_succAbove (i : Fin (n + 1)) (x : α i) (p : ∀ j, α (i.succAbove j))
    (j : Fin n) : insertNth i x p (i.succAbove j) = p j := by
  simp only [insertNth, succAboveCases, dif_neg (succAbove_ne _ _), succAbove_lt_iff_castSucc_lt]
  split_ifs with hlt
  · generalize_proofs H₁ H₂; revert H₂
    generalize hk : castPred ((succAbove i) j) H₁ = k
    rw [castPred_succAbove _ _ hlt] at hk; cases hk
    intro; rfl
  · generalize_proofs H₀ H₁ H₂; revert H₂
    generalize hk : pred (succAbove i j) H₁ = k
    rw [pred_succAbove _ _ (Fin.not_lt.1 hlt)] at hk; cases hk
    intro; rfl

Insertion at Shifted Index Preserves Tuple Value: $\text{insertNth}\,i\,x\,p\,(i.\text{succAbove}\,j) = p_j$

Informal description

For any pivot index $i \in \text{Fin}(n+1)$, element $x \in \alpha_i$, and dependent tuple $p$ where each $p_j$ has type $\alpha_{i.\text{succAbove}\,j}$ for $j \in \text{Fin}(n)$, the function $\text{insertNth}$ satisfies $\text{insertNth}\,i\,x\,p\,(i.\text{succAbove}\,j) = p_j$ for all $j \in \text{Fin}(n)$.

Fin.succAbove_cases_eq_insertNth theorem

: @succAboveCases = @insertNth

Full source

@[simp]
theorem succAbove_cases_eq_insertNth : @succAboveCases = @insertNth :=
  rfl

Equivalence of `succAboveCases` and `insertNth` for dependent tuples

Informal description

The function `succAboveCases` is equal to the function `insertNth` for constructing dependent tuples on `Fin (n + 1)`.

Fin.removeNth_insertNth theorem

(p : Fin (n + 1)) (a : α p) (f : ∀ i, α (succAbove p i)) : removeNth p (insertNth p a f) = f

Full source

@[simp] lemma removeNth_insertNth (p : Fin (n + 1)) (a : α p) (f : ∀ i, α (succAbove p i)) :
    removeNth p (insertNth p a f) = f := by ext; unfold removeNth; simp

Inverse Relationship Between Insertion and Removal at Pivot Index: $\text{removeNth}\,p \circ \text{insertNth}\,p = \text{id}$

Informal description

For any pivot index $p \in \text{Fin}(n+1)$, element $a \in \alpha_p$, and dependent tuple $f$ where each $f_i$ has type $\alpha_{p.\text{succAbove}\,i}$ for $i \in \text{Fin}(n)$, the operation of removing the $p$-th entry from the tuple obtained by inserting $a$ at position $p$ in $f$ yields the original tuple $f$. That is, $\text{removeNth}\,p\,(\text{insertNth}\,p\,a\,f) = f$.

Fin.removeNth_zero theorem

(f : ∀ i, α i) : removeNth 0 f = tail f

Full source

@[simp] lemma removeNth_zero (f : ∀ i, α i) : removeNth 0 f = tail f := by
  ext; simp [tail, removeNth]

Removing the First Entry of a Tuple is Equivalent to Taking Its Tail

Informal description

For any dependent tuple $f$ of length $n+1$ (where each element $f_i$ has type $\alpha_i$), removing the first entry (at index $0$) using $\text{removeNth}$ is equivalent to taking the tail of $f$, i.e., $\text{removeNth}\,0\,f = \text{tail}\,f$.

Fin.removeNth_last theorem

{α : Type*} (f : Fin (n + 1) → α) : removeNth (last n) f = init f

Full source

@[simp] lemma removeNth_last {α : Type*} (f : Fin (n + 1) → α) : removeNth (last n) f = init f := by
  ext; simp [init, removeNth]

Removing Last Entry Equals Initial Segment of Tuple

Informal description

For any tuple $f$ of length $n+1$ with elements in a type $\alpha$, removing the last entry of $f$ (using `removeNth` with pivot index `last n`) is equal to taking the initial segment of $f$ (using `init`). In other words, $\text{removeNth} (\text{last } n) f = \text{init} f$.

Fin.insertNth_comp_succAbove theorem

(i : Fin (n + 1)) (x : β) (p : Fin n → β) : insertNth i x p ∘ i.succAbove = p

Full source

@[simp]
theorem insertNth_comp_succAbove (i : Fin (n + 1)) (x : β) (p : Fin n → β) :
    insertNthinsertNth i x p ∘ i.succAbove = p :=
  funext (insertNth_apply_succAbove i _ _)

Insertion-Shift Composition Preserves Tuple: $(\text{insertNth}\,i\,x\,p) \circ i.\text{succAbove} = p$

Informal description

For any pivot index $i \in \text{Fin}(n+1)$, element $x \in \beta$, and tuple $p : \text{Fin}(n) \to \beta$, the composition of the insertion function $\text{insertNth}\,i\,x\,p$ with the shift function $i.\text{succAbove}$ equals $p$, i.e., $(\text{insertNth}\,i\,x\,p) \circ i.\text{succAbove} = p$.

Fin.insertNth_eq_iff theorem

 {p : Fin (n + 1)} {a : α p} {f : ∀ i, α (p.succAbove i)} {g : ∀ j, α j} :
  insertNth p a f = g ↔ a = g p ∧ f = removeNth p g

Full source

theorem insertNth_eq_iff {p : Fin (n + 1)} {a : α p} {f : ∀ i, α (p.succAbove i)} {g : ∀ j, α j} :
    insertNthinsertNth p a f = g ↔ a = g p ∧ f = removeNth p g := by
  simp [funext_iff, forall_iff_succAbove p, removeNth]

Equivalence of Insertion and Removal for Dependent Tuples at Pivot Index

Informal description

For a pivot index $p \in \text{Fin}(n+1)$, an element $a \in \alpha_p$, a dependent tuple $f$ where each $f_i \in \alpha_{p.\text{succAbove}\,i}$ for $i \in \text{Fin}(n)$, and a dependent tuple $g$ where each $g_j \in \alpha_j$ for $j \in \text{Fin}(n+1)$, the following equivalence holds: \[ \text{insertNth}\,p\,a\,f = g \quad \leftrightarrow \quad a = g_p \land f = \text{removeNth}\,p\,g \] This means that inserting $a$ into $f$ at position $p$ yields $g$ if and only if $a$ equals the $p$-th element of $g$ and $f$ equals the tuple obtained by removing the $p$-th element from $g$.

Fin.insertNth_injective2 theorem

{p : Fin (n + 1)} : Function.Injective2 (@insertNth n α p)

Full source

/-- As a binary function, `Fin.insertNth` is injective. -/
theorem insertNth_injective2 {p : Fin (n + 1)} :
    Function.Injective2 (@insertNth n α p) := fun xₚ yₚ x y h ↦
  ⟨by simpa using congr_fun h p, funext fun i ↦ by simpa using congr_fun h (succAbove p i)⟩

Injectivity of $\text{insertNth}_p$ as a Binary Function

Informal description

For any pivot index $p \in \text{Fin}(n+1)$, the function $\text{insertNth}_p$ is injective as a binary function. That is, for any two pairs $(x_1, y_1)$ and $(x_2, y_2)$ in $\alpha_p \times (\prod_{i \in \text{Fin}(n)} \alpha_{p.\text{succAbove}\,i})$, if $\text{insertNth}_p\,x_1\,y_1 = \text{insertNth}_p\,x_2\,y_2$, then $x_1 = x_2$ and $y_1 = y_2$.

Fin.insertNth_inj theorem

 {p : Fin (n + 1)} {x y : ∀ i, α (succAbove p i)} {xₚ yₚ : α p} : insertNth p xₚ x = insertNth p yₚ y ↔ xₚ = yₚ ∧ x = y

Full source

@[simp]
theorem insertNth_inj {p : Fin (n + 1)} {x y : ∀ i, α (succAbove p i)} {xₚ yₚ : α p} :
    insertNthinsertNth p xₚ x = insertNth p yₚ y ↔ xₚ = yₚ ∧ x = y :=
  insertNth_injective2.eq_iff

Injectivity of Tuple Insertion at Pivot Index: $\text{insertNth}_p\,x_p\,x = \text{insertNth}_p\,y_p\,y \leftrightarrow x_p = y_p \land x = y$

Informal description

For any pivot index $p \in \text{Fin}(n+1)$, elements $x_p, y_p \in \alpha_p$, and dependent tuples $x, y \in \prod_{i \in \text{Fin}(n)} \alpha_{p.\text{succAbove}\,i}$, the equality $\text{insertNth}_p\,x_p\,x = \text{insertNth}_p\,y_p\,y$ holds if and only if $x_p = y_p$ and $x = y$.

Fin.insertNth_left_injective theorem

{p : Fin (n + 1)} (x : ∀ i, α (succAbove p i)) : Function.Injective (insertNth p · x)

Full source

theorem insertNth_left_injective {p : Fin (n + 1)} (x : ∀ i, α (succAbove p i)) :
    Function.Injective (insertNth p · x) :=
  insertNth_injective2.left _

Injectivity of $\text{insertNth}_p\,(\cdot)\,x$ in the pivot element

Informal description

For any pivot index $p \in \text{Fin}(n+1)$ and any dependent tuple $x \in \prod_{i \in \text{Fin}(n)} \alpha_{p.\text{succAbove}\,i}$, the function $\text{insertNth}_p\,(\cdot)\,x$ is injective. That is, for any two elements $y_p, z_p \in \alpha_p$, if $\text{insertNth}_p\,y_p\,x = \text{insertNth}_p\,z_p\,x$, then $y_p = z_p$.

Fin.insertNth_right_injective theorem

{p : Fin (n + 1)} (x : α p) : Function.Injective (insertNth p x)

Full source

theorem insertNth_right_injective {p : Fin (n + 1)} (x : α p) :
    Function.Injective (insertNth p x) :=
  insertNth_injective2.right _

Injectivity of $\text{insertNth}_p\,x$ in the Tuple Argument

Informal description

For any pivot index $p \in \text{Fin}(n+1)$ and any element $x \in \alpha_p$, the function $\text{insertNth}_p\,x$ is injective. That is, for any two tuples $y, z \in \prod_{i \in \text{Fin}(n)} \alpha_{p.\text{succAbove}\,i}$, if $\text{insertNth}_p\,x\,y = \text{insertNth}_p\,x\,z$, then $y = z$.

Fin.insertNth_apply_below theorem

 {i j : Fin (n + 1)} (h : j < i) (x : α i) (p : ∀ k, α (i.succAbove k)) :
  i.insertNth x p j = @Eq.recOn _ _ (fun x _ ↦ α x) _ (succAbove_castPred_of_lt _ _ h) (p <| j.castPred _)

Full source

theorem insertNth_apply_below {i j : Fin (n + 1)} (h : j < i) (x : α i)
    (p : ∀ k, α (i.succAbove k)) :
    i.insertNth x p j = @Eq.recOn _ _ (fun x _ ↦ α x) _
    (succAbove_castPred_of_lt _ _ h) (p <| j.castPred _) := by
  rw [insertNth, succAboveCases, dif_neg (Fin.ne_of_lt h), dif_pos h]

Value of Inserted Tuple Below Pivot Index

Informal description

For any indices $i, j \in \text{Fin}(n+1)$ with $j < i$, an element $x \in \alpha_i$, and a dependent tuple $p$ where each $p_k$ has type $\alpha_{i.\text{succAbove}\,k}$ for $k \in \text{Fin}(n)$, the value of the tuple $\text{insertNth}\,i\,x\,p$ at index $j$ is equal to $p_{j.\text{castPred}}$ after an appropriate type cast via $\text{succAbove\_castPred\_of\_lt}$.

Fin.insertNth_apply_above theorem

 {i j : Fin (n + 1)} (h : i < j) (x : α i) (p : ∀ k, α (i.succAbove k)) :
  i.insertNth x p j = @Eq.recOn _ _ (fun x _ ↦ α x) _ (succAbove_pred_of_lt _ _ h) (p <| j.pred _)

Full source

theorem insertNth_apply_above {i j : Fin (n + 1)} (h : i < j) (x : α i)
    (p : ∀ k, α (i.succAbove k)) :
    i.insertNth x p j = @Eq.recOn _ _ (fun x _ ↦ α x) _
    (succAbove_pred_of_lt _ _ h) (p <| j.pred _) := by
  rw [insertNth, succAboveCases, dif_neg (Fin.ne_of_gt h), dif_neg (Fin.lt_asymm h)]

Value of Inserted Tuple Above Pivot Index

Informal description

For any indices $i, j \in \text{Fin}(n+1)$ with $i < j$, an element $x \in \alpha_i$, and a dependent tuple $p$ where each $p_k$ has type $\alpha_{i.\text{succAbove}\,k}$ for $k \in \text{Fin}(n)$, the value of the tuple $\text{insertNth}\,i\,x\,p$ at index $j$ is equal to $p_{j.\text{pred}}$ after an appropriate type cast via $\text{succAbove\_pred\_of\_lt}$.

Fin.insertNth_zero theorem

 (x : α 0) (p : ∀ j : Fin n, α (succAbove 0 j)) :
  insertNth 0 x p = cons x fun j ↦ _root_.cast (congr_arg α (congr_fun succAbove_zero j)) (p j)

Full source

theorem insertNth_zero (x : α 0) (p : ∀ j : Fin n, α (succAbove 0 j)) :
    insertNth 0 x p =
      cons x fun j ↦ _root_.cast (congr_arg α (congr_fun succAbove_zero j)) (p j) := by
  refine insertNth_eq_iff.2 ⟨by simp, ?_⟩
  ext j
  convert (cons_succ x p j).symm

Insertion at Zero Equals Prepending with Casts

Informal description

For any element $x$ of type $\alpha(0)$ and a dependent tuple $p$ where each $p(j)$ has type $\alpha(\text{succAbove}(0, j))$ for $j \in \text{Fin}(n)$, inserting $x$ at position $0$ via $\text{insertNth}$ is equivalent to prepending $x$ to the tuple obtained by casting each $p(j)$ appropriately. Specifically, \[ \text{insertNth}\,0\,x\,p = \text{cons}\,x\,\left(\lambda j, \text{cast}\,(\text{congr\_arg}\,\alpha\,(\text{succAbove\_zero}\,j))\,(p(j))\right). \]

Fin.insertNth_zero' theorem

(x : β) (p : Fin n → β) : @insertNth _ (fun _ ↦ β) 0 x p = cons x p

Full source

@[simp]
theorem insertNth_zero' (x : β) (p : Fin n → β) : @insertNth _ (fun _ ↦ β) 0 x p = cons x p := by
  simp [insertNth_zero]

Insertion at Zero with Constant Type Family Equals Prepending

Informal description

For any element $x$ of type $\beta$ and a tuple $p : \text{Fin} n \to \beta$, inserting $x$ at position $0$ in $p$ via $\text{insertNth}$ (with constant type family $\alpha = \lambda \_, \beta$) is equivalent to prepending $x$ to $p$ via $\text{cons}$. That is, \[ \text{insertNth}\,0\,x\,p = \text{cons}\,x\,p. \]

Fin.insertNth_last theorem

 (x : α (last n)) (p : ∀ j : Fin n, α ((last n).succAbove j)) :
  insertNth (last n) x p = snoc (fun j ↦ _root_.cast (congr_arg α (succAbove_last_apply j)) (p j)) x

Full source

theorem insertNth_last (x : α (last n)) (p : ∀ j : Fin n, α ((last n).succAbove j)) :
    insertNth (last n) x p =
      snoc (fun j ↦ _root_.cast (congr_arg α (succAbove_last_apply j)) (p j)) x := by
  refine insertNth_eq_iff.2 ⟨by simp, ?_⟩
  ext j
  apply eq_of_heq
  trans snoc (fun j ↦ _root_.cast (congr_arg α (succAbove_last_apply j)) (p j)) x j.castSucc
  · rw [snoc_castSucc]
    exact (cast_heq _ _).symm
  · apply congr_arg_heq
    rw [succAbove_last]

Insertion at Last Position Equals Appending with Casts

Informal description

For a dependent tuple $p$ where each $p_j$ has type $\alpha_{(\text{last } n).\text{succAbove}\,j}$ for $j \in \text{Fin}(n)$, and an element $x \in \alpha_{\text{last } n}$, inserting $x$ at the last position of $p$ via $\text{insertNth}$ is equivalent to appending $x$ to the tuple obtained by casting each $p_j$ appropriately, i.e., \[ \text{insertNth}\,(\text{last } n)\,x\,p = \text{snoc}\,(\lambda j, \text{cast}\,(\text{congr\_arg}\,\alpha\,(\text{succAbove\_last\_apply}\,j))\,(p_j))\,x. \]

Fin.insertNth_last' theorem

(x : β) (p : Fin n → β) : @insertNth _ (fun _ ↦ β) (last n) x p = snoc p x

Full source

@[simp]
theorem insertNth_last' (x : β) (p : Fin n → β) :
    @insertNth _ (fun _ ↦ β) (last n) x p = snoc p x := by simp [insertNth_last]

Insertion at Last Position Equals Appending for Constant Type Family

Informal description

For any element $x$ of type $\beta$ and a tuple $p : \text{Fin}(n) \to \beta$, inserting $x$ at the last position in $p$ via $\text{insertNth}$ (with constant type family $\alpha = \lambda \_, \beta$) is equivalent to appending $x$ to $p$ via $\text{snoc}$. That is, \[ \text{insertNth}\,(\text{last } n)\,x\,p = \text{snoc}\,p\,x. \]

Fin.insertNth_rev theorem

 {α : Sort*} (i : Fin (n + 1)) (a : α) (f : Fin n → α) (j : Fin (n + 1)) :
  insertNth (α := fun _ ↦ α) i a f (rev j) = insertNth (α := fun _ ↦ α) i.rev a (f ∘ rev) j

Full source

lemma insertNth_rev {α : Sort*} (i : Fin (n + 1)) (a : α) (f : Fin n → α) (j : Fin (n + 1)) :
    insertNth (α := fun _ ↦ α) i a f (rev j) = insertNth (α := fun _ ↦ α) i.rev a (f ∘ rev) j := by
  induction j using Fin.succAboveCases
  · exact rev i
  · simp
  · simp [rev_succAbove]

Insertion and Reversal Commute in Tuples: $\text{insertNth}\,i\,a\,f\,(\text{rev}\,j) = \text{insertNth}\,(\text{rev}\,i)\,a\,(f \circ \text{rev})\,j$

Informal description

For any type $\alpha$, pivot index $i \in \text{Fin}(n+1)$, element $a \in \alpha$, function $f : \text{Fin}(n) \to \alpha$, and index $j \in \text{Fin}(n+1)$, we have: \[ \text{insertNth}\,i\,a\,f\,(\text{rev}\,j) = \text{insertNth}\,(\text{rev}\,i)\,a\,(f \circ \text{rev})\,j \] where $\text{rev}$ denotes the order-reversing permutation of $\text{Fin}(n+1)$.

Fin.insertNth_comp_rev theorem

 {α} (i : Fin (n + 1)) (x : α) (p : Fin n → α) :
  (Fin.insertNth i x p) ∘ Fin.rev = Fin.insertNth (Fin.rev i) x (p ∘ Fin.rev)

Full source

theorem insertNth_comp_rev {α} (i : Fin (n + 1)) (x : α) (p : Fin n → α) :
    (Fin.insertNth i x p) ∘ Fin.rev = Fin.insertNth (Fin.rev i) x (p ∘ Fin.rev) := by
  funext x
  apply insertNth_rev

Commutativity of Insertion and Reversal in Tuples: $(\text{insertNth}\,i\,x\,p) \circ \text{rev} = \text{insertNth}\,(\text{rev}\,i)\,x\,(p \circ \text{rev})$

Informal description

For any type $\alpha$, pivot index $i \in \text{Fin}(n+1)$, element $x \in \alpha$, and function $p : \text{Fin}(n) \to \alpha$, the composition of $\text{insertNth}\,i\,x\,p$ with the order-reversing permutation $\text{rev}$ on $\text{Fin}(n+1)$ is equal to inserting $x$ at the reversed index $\text{rev}\,i$ into the function $p \circ \text{rev}$. In symbols: \[ (\text{insertNth}\,i\,x\,p) \circ \text{rev} = \text{insertNth}\,(\text{rev}\,i)\,x\,(p \circ \text{rev}) \]

Fin.cons_rev theorem

 {α n} (a : α) (f : Fin n → α) (i : Fin <| n + 1) :
  cons (α := fun _ => α) a f i.rev = snoc (α := fun _ => α) (f ∘ Fin.rev : Fin _ → α) a i

Full source

theorem cons_rev {α n} (a : α) (f : Fin n → α) (i : Fin <| n + 1) :
    cons (α := fun _ => α) a f i.rev = snoc (α := fun _ => α) (f ∘ Fin.rev : Fin _ → α) a i := by
  simpa using insertNth_rev 0 a f i

Reversed Cons Equals Snoc of Reversed Function: $\text{cons}\,a\,f\,(\text{rev}\,i) = \text{snoc}\,(f \circ \text{rev})\,a\,i$

Informal description

For any type $\alpha$, natural number $n$, element $a \in \alpha$, function $f : \text{Fin}\,n \to \alpha$, and index $i \in \text{Fin}\,(n+1)$, we have: \[ \text{cons}\,a\,f\,(\text{rev}\,i) = \text{snoc}\,(f \circ \text{rev})\,a\,i \] where $\text{rev}$ denotes the order-reversing permutation of $\text{Fin}\,(n+1)$.

Fin.cons_comp_rev theorem

{α n} (a : α) (f : Fin n → α) : Fin.cons a f ∘ Fin.rev = Fin.snoc (f ∘ Fin.rev) a

Full source

theorem cons_comp_rev {α n} (a : α) (f : Fin n → α) :
    Fin.consFin.cons a f ∘ Fin.rev = Fin.snoc (f ∘ Fin.rev) a := by
  funext i; exact cons_rev ..

Composition of Cons with Reversal Equals Snoc of Reversed Function: $\text{cons}\,a\,f \circ \text{rev} = \text{snoc}\,(f \circ \text{rev})\,a$

Informal description

For any type $\alpha$, natural number $n$, element $a \in \alpha$, and function $f : \text{Fin}\,n \to \alpha$, the composition of $\text{cons}\,a\,f$ with the order-reversing permutation $\text{rev}$ on $\text{Fin}\,(n+1)$ is equal to $\text{snoc}\,(f \circ \text{rev})\,a$. In symbols: \[ \text{cons}\,a\,f \circ \text{rev} = \text{snoc}\,(f \circ \text{rev})\,a \]

Fin.snoc_rev theorem

 {α n} (a : α) (f : Fin n → α) (i : Fin <| n + 1) :
  snoc (α := fun _ => α) f a i.rev = cons (α := fun _ => α) a (f ∘ Fin.rev : Fin _ → α) i

Full source

theorem snoc_rev {α n} (a : α) (f : Fin n → α) (i : Fin <| n + 1) :
    snoc (α := fun _ => α) f a i.rev = cons (α := fun _ => α) a (f ∘ Fin.rev : Fin _ → α) i := by
  simpa using insertNth_rev (last n) a f i

Reversed Snoc Equals Cons of Reversed Function: $\text{snoc}\,f\,a\,(\text{rev}\,i) = \text{cons}\,a\,(f \circ \text{rev})\,i$

Informal description

For any type $\alpha$, natural number $n$, element $a \in \alpha$, function $f : \text{Fin}\,n \to \alpha$, and index $i \in \text{Fin}\,(n+1)$, we have: \[ \text{snoc}\,f\,a\,(\text{rev}\,i) = \text{cons}\,a\,(f \circ \text{rev})\,i \] where $\text{rev}$ denotes the order-reversing permutation of $\text{Fin}\,(n+1)$.

Fin.snoc_comp_rev theorem

{α n} (a : α) (f : Fin n → α) : Fin.snoc f a ∘ Fin.rev = Fin.cons a (f ∘ Fin.rev)

Full source

theorem snoc_comp_rev {α n} (a : α) (f : Fin n → α) :
    Fin.snocFin.snoc f a ∘ Fin.rev = Fin.cons a (f ∘ Fin.rev) :=
  funext <| snoc_rev a f

Composition of Snoc with Reversal Equals Cons of Reversed Function: $(\text{snoc}\,f\,a) \circ \text{rev} = \text{cons}\,a\,(f \circ \text{rev})$

Informal description

For any type $\alpha$, natural number $n$, element $a \in \alpha$, and function $f : \text{Fin}\,n \to \alpha$, the composition of the function $\text{snoc}\,f\,a$ (which appends $a$ to $f$) with the order-reversing permutation $\text{rev}$ on $\text{Fin}\,(n+1)$ is equal to the function $\text{cons}\,a\,(f \circ \text{rev})$ (which prepends $a$ to $f \circ \text{rev}$). In other words: \[ (\text{snoc}\,f\,a) \circ \text{rev} = \text{cons}\,a\,(f \circ \text{rev}) \]

Fin.insertNth_binop theorem

 (op : ∀ j, α j → α j → α j) (i : Fin (n + 1)) (x y : α i) (p q : ∀ j, α (i.succAbove j)) :
  (i.insertNth (op i x y) fun j ↦ op _ (p j) (q j)) = fun j ↦ op j (i.insertNth x p j) (i.insertNth y q j)

Full source

theorem insertNth_binop (op : ∀ j, α j → α j → α j) (i : Fin (n + 1)) (x y : α i)
    (p q : ∀ j, α (i.succAbove j)) :
    (i.insertNth (op i x y) fun j ↦ op _ (p j) (q j)) = fun j ↦
      op j (i.insertNth x p j) (i.insertNth y q j) :=
  insertNth_eq_iff.2 <| by unfold removeNth; simp

Componentwise Binary Operation Commutes with Insertion in Dependent Tuples

Informal description

Let $n$ be a natural number, and for each $j \in \text{Fin}(n+1)$, let $\alpha_j$ be a type equipped with a binary operation $\text{op}_j : \alpha_j \to \alpha_j \to \alpha_j$. Given a pivot index $i \in \text{Fin}(n+1)$, elements $x, y \in \alpha_i$, and dependent tuples $p, q$ where each $p_j, q_j \in \alpha_{i.\text{succAbove}\,j}$ for $j \in \text{Fin}(n)$, the following equality holds: \[ \text{insertNth}\,i\,(\text{op}_i\,x\,y)\,(\lambda j, \text{op}_{i.\text{succAbove}\,j}\,(p_j)\,(q_j)) = \lambda j, \text{op}_j\,(\text{insertNth}\,i\,x\,p\,j)\,(\text{insertNth}\,i\,y\,q\,j) \] This means that inserting the operation result $\text{op}_i\,x\,y$ at position $i$ into the tuple formed by applying $\text{op}$ componentwise to $p$ and $q$ is the same as applying $\text{op}$ componentwise to the tuples obtained by inserting $x$ into $p$ and $y$ into $q$ at position $i$.

Fin.insertNth_le_iff theorem

 {i : Fin (n + 1)} {x : α i} {p : ∀ j, α (i.succAbove j)} {q : ∀ j, α j} :
  i.insertNth x p ≤ q ↔ x ≤ q i ∧ p ≤ fun j ↦ q (i.succAbove j)

Full source

theorem insertNth_le_iff {i : Fin (n + 1)} {x : α i} {p : ∀ j, α (i.succAbove j)} {q : ∀ j, α j} :
    i.insertNth x p ≤ q ↔ x ≤ q i ∧ p ≤ fun j ↦ q (i.succAbove j) := by
  simp [Pi.le_def, forall_iff_succAbove i]

Characterization of Order Relation for Inserted Tuple: $\text{insertNth}\,i\,x\,p \leq q$ iff $x \leq q_i$ and $p \leq$ shifted $q$

Informal description

For any pivot index $i \in \text{Fin}(n+1)$, element $x \in \alpha_i$, dependent tuple $p$ where each $p_j \in \alpha_{i.\text{succAbove}\,j}$ for $j \in \text{Fin}(n)$, and dependent tuple $q$ where each $q_j \in \alpha_j$, the inequality $\text{insertNth}\,i\,x\,p \leq q$ holds if and only if both $x \leq q_i$ and $p \leq (j \mapsto q(i.\text{succAbove}\,j))$ hold.

Fin.le_insertNth_iff theorem

 {i : Fin (n + 1)} {x : α i} {p : ∀ j, α (i.succAbove j)} {q : ∀ j, α j} :
  q ≤ i.insertNth x p ↔ q i ≤ x ∧ (fun j ↦ q (i.succAbove j)) ≤ p

Full source

theorem le_insertNth_iff {i : Fin (n + 1)} {x : α i} {p : ∀ j, α (i.succAbove j)} {q : ∀ j, α j} :
    q ≤ i.insertNth x p ↔ q i ≤ x ∧ (fun j ↦ q (i.succAbove j)) ≤ p := by
  simp [Pi.le_def, forall_iff_succAbove i]

Characterization of Order Relation for Inserted Tuple: $q \leq \text{insertNth}\,i\,x\,p$ iff $q_i \leq x$ and shifted $q \leq p$

Informal description

For any pivot index $i \in \text{Fin}(n+1)$, element $x \in \alpha_i$, dependent tuple $p$ where each $p_j \in \alpha_{i.\text{succAbove}\,j}$ for $j \in \text{Fin}(n)$, and dependent tuple $q$ where each $q_j \in \alpha_j$, the inequality $q \leq \text{insertNth}\,i\,x\,p$ holds if and only if both $q_i \leq x$ and the shifted tuple $(j \mapsto q(i.\text{succAbove}\,j)) \leq p$ hold.

Fin.removeNth_update theorem

(p : Fin (n + 1)) (x) (f : ∀ j, α j) : removeNth p (update f p x) = removeNth p f

Full source

@[simp] lemma removeNth_update (p : Fin (n + 1)) (x) (f : ∀ j, α j) :
    removeNth p (update f p x) = removeNth p f := by ext i; simp [removeNth, succAbove_ne]

Removing an updated entry equals removing the original entry

Informal description

For any pivot index $p \in \text{Fin}(n+1)$, any element $x$ of type $\alpha_p$, and any dependent tuple $f$ where each $f_j$ has type $\alpha_j$, updating the $p$-th entry of $f$ to $x$ and then removing the $p$-th entry yields the same result as simply removing the $p$-th entry from $f$. That is, $$\text{removeNth}_p (\text{update}_f p x) = \text{removeNth}_p f.$$

Fin.insertNth_removeNth theorem

(p : Fin (n + 1)) (x) (f : ∀ j, α j) : insertNth p x (removeNth p f) = update f p x

Full source

@[simp] lemma insertNth_removeNth (p : Fin (n + 1)) (x) (f : ∀ j, α j) :
    insertNth p x (removeNth p f) = update f p x := by simp [Fin.insertNth_eq_iff]

Insertion after Removal Equals Update: $\text{insertNth}_p\,x\,(\text{removeNth}_p f) = \text{update}_f p\,x$

Informal description

For any pivot index $p \in \text{Fin}(n+1)$, any element $x$ of type $\alpha_p$, and any dependent tuple $f$ where each $f_j$ has type $\alpha_j$, inserting $x$ at position $p$ into the tuple obtained by removing the $p$-th entry from $f$ is equal to updating the $p$-th entry of $f$ to $x$. That is, $$\text{insertNth}_p\,x\,(\text{removeNth}_p f) = \text{update}_f p\,x.$$

Fin.insertNth_self_removeNth theorem

(p : Fin (n + 1)) (f : ∀ j, α j) : insertNth p (f p) (removeNth p f) = f

Full source

lemma insertNth_self_removeNth (p : Fin (n + 1)) (f : ∀ j, α j) :
    insertNth p (f p) (removeNth p f) = f := by simp

Reconstruction of Tuple via Insertion and Removal: $\text{insertNth}_p\,(f p)\,(\text{removeNth}_p f) = f$

Informal description

For any pivot index $p \in \text{Fin}(n+1)$ and any dependent tuple $f$ where each $f_j$ has type $\alpha_j$, inserting the $p$-th entry of $f$ at position $p$ into the tuple obtained by removing the $p$-th entry from $f$ reconstructs the original tuple $f$. That is, $$\text{insertNth}_p\,(f p)\,(\text{removeNth}_p f) = f.$$

Fin.update_insertNth theorem

(p : Fin (n + 1)) (x y : α p) (f : ∀ i, α (p.succAbove i)) : update (p.insertNth x f) p y = p.insertNth y f

Full source

@[simp]
theorem update_insertNth (p : Fin (n + 1)) (x y : α p) (f : ∀ i, α (p.succAbove i)) :
    update (p.insertNth x f) p y = p.insertNth y f := by
  ext i
  cases i using p.succAboveCases <;> simp [succAbove_ne]

Update Commutes with Insertion in Dependent Tuples: $\text{update}\,(\text{insertNth}_p\,x\,f)\,p\,y = \text{insertNth}_p\,y\,f$

Informal description

For any pivot index $p \in \text{Fin}(n+1)$, elements $x, y \in \alpha_p$, and dependent tuple $f$ where each $f_i$ has type $\alpha_{p.\text{succAbove}\,i}$ for $i \in \text{Fin}(n)$, updating the value at index $p$ in the tuple $\text{insertNth}_p\,x\,f$ to $y$ is equal to inserting $y$ at index $p$ in the original tuple $f$. That is, $$\text{update}\,(\text{insertNth}_p\,x\,f)\,p\,y = \text{insertNth}_p\,y\,f.$$

Fin.insertNthEquiv definition

(α : Fin (n + 1) → Type u) (p : Fin (n + 1)) : α p × (∀ i, α (p.succAbove i)) ≃ ∀ i, α i

Full source

/-- Equivalence between tuples of length `n + 1` and pairs of an element and a tuple of length `n`
given by separating out the `p`-th element of the tuple.

This is `Fin.insertNth` as an `Equiv`. -/
@[simps]
def insertNthEquiv (α : Fin (n + 1) → Type u) (p : Fin (n + 1)) :
    α p × (∀ i, α (p.succAbove i))α p × (∀ i, α (p.succAbove i)) ≃ ∀ i, α i where
  toFun f := insertNth p f.1 f.2
  invFun f := (f p, removeNth p f)
  left_inv f := by ext <;> simp
  right_inv f := by simp

Equivalence between dependent tuples and pairs at a pivot index

Informal description

For a family of types $\alpha_i$ indexed by $i \in \text{Fin}(n+1)$ and a pivot index $p \in \text{Fin}(n+1)$, there is an equivalence between: 1. The product type $\alpha_p \times \left(\prod_{i \in \text{Fin}(n)} \alpha_{p.\text{succAbove}\,i}\right)$, consisting of an element of $\alpha_p$ paired with a dependent tuple of length $n$ where the $i$-th element has type $\alpha_{p.\text{succAbove}\,i}$. 2. The type of all dependent tuples $\prod_{i \in \text{Fin}(n+1)} \alpha_i$. The equivalence is given by: - The forward direction inserts the element of $\alpha_p$ at position $p$ in the tuple, using $\text{insertNth}$. - The backward direction extracts the element at position $p$ and removes it from the tuple, using $\text{removeNth}$.

Fin.insertNthEquiv_zero theorem

(α : Fin (n + 1) → Type*) : insertNthEquiv α 0 = consEquiv α

Full source

@[simp] lemma insertNthEquiv_zero (α : Fin (n + 1) → Type*) : insertNthEquiv α 0 = consEquiv α :=
  Equiv.symm_bijective.injective <| by ext <;> rfl

Equivalence between Insertion at Zero and Prepending in Dependent Tuples

Informal description

For any family of types $\alpha_i$ indexed by $i \in \text{Fin}(n+1)$, the equivalence `insertNthEquiv α 0` (which inserts an element at position $0$) is equal to `consEquiv α` (which prepends an element to the tuple). In other words, inserting an element at the beginning of a dependent tuple is equivalent to prepending an element to the tuple.

Fin.insertNthEquiv_last theorem

(n : ℕ) (α : Type*) : insertNthEquiv (fun _ ↦ α) (last n) = snocEquiv (fun _ ↦ α)

Full source

/-- Note this lemma can only be written about non-dependent tuples as `insertNth (last n) = snoc` is
not a definitional equality. -/
@[simp] lemma insertNthEquiv_last (n : ℕ) (α : Type*) :
    insertNthEquiv (fun _ ↦ α) (last n) = snocEquiv (fun _ ↦ α) := by ext; simp

Equality of Insertion at Last Index and Appending for Constant Tuples

Informal description

For any natural number $n$ and type $\alpha$, the equivalence `insertNthEquiv` at the last index `last n` (which inserts an element at the end of a tuple) is equal to the equivalence `snocEquiv` (which appends an element to a tuple), when both are specialized to constant type families $\lambda \_, \alpha$.

Fin.find definition

: ∀ {n : ℕ} (p : Fin n → Prop) [DecidablePred p], Option (Fin n)

Full source

/-- `find p` returns the first index `n` where `p n` is satisfied, and `none` if it is never
satisfied. -/
def find : ∀ {n : ℕ} (p : Fin n → Prop) [DecidablePred p], Option (Fin n)
  | 0, _p, _ => none
  | n + 1, p, _ => by
    exact
      Option.casesOn (@find n (fun i ↦ p (i.castLT (Nat.lt_succ_of_lt i.2))) _)
        (if _ : p (Fin.last n) then some (Fin.last n) else none) fun i ↦
        some (i.castLT (Nat.lt_succ_of_lt i.2))

First satisfying index in `Fin n`

Informal description

For a predicate `p` on the finite type `Fin n` (the canonical type with `n` elements), `Fin.find p` returns the first index `i : Fin n` where `p i` holds, if such an index exists, and returns `none` otherwise.

Fin.find_spec theorem

: ∀ {n : ℕ} (p : Fin n → Prop) [DecidablePred p] {i : Fin n} (_ : i ∈ Fin.find p), p i

Full source

/-- If `find p = some i`, then `p i` holds -/
theorem find_spec :
    ∀ {n : ℕ} (p : Fin n → Prop) [DecidablePred p] {i : Fin n} (_ : i ∈ Fin.find p), p i
  | 0, _, _, _, hi => Option.noConfusion hi
  | n + 1, p, I, i, hi => by
    rw [find] at hi
    rcases h : find fun i : Fin n ↦ p (i.castLT (Nat.lt_succ_of_lt i.2)) with - | j
    · rw [h] at hi
      dsimp at hi
      split_ifs at hi with hl
      · simp only [Option.mem_def, Option.some.injEq] at hi
        exact hi ▸ hl
      · exact (Option.not_mem_none _ hi).elim
    · rw [h] at hi
      dsimp at hi
      rw [← Option.some_inj.1 hi]
      exact @find_spec n (fun i ↦ p (i.castLT (Nat.lt_succ_of_lt i.2))) _ _ h

Correctness of $\mathrm{find}$ for Finite Types

Informal description

For any natural number $n$, a decidable predicate $p$ on $\mathrm{Fin}\,n$, and an index $i \in \mathrm{Fin}\,n$, if $i$ is in the result of $\mathrm{find}\,p$ (i.e., $\mathrm{find}\,p = \mathrm{some}\,i$), then $p(i)$ holds.

Fin.isSome_find_iff theorem

: ∀ {n : ℕ} {p : Fin n → Prop} [DecidablePred p], (find p).isSome ↔ ∃ i, p i

Full source

/-- `find p` does not return `none` if and only if `p i` holds at some index `i`. -/
theorem isSome_find_iff :
    ∀ {n : ℕ} {p : Fin n → Prop} [DecidablePred p], (find p).isSome ↔ ∃ i, p i
  | 0, _, _ => iff_of_false (fun h ↦ Bool.noConfusion h) fun ⟨i, _⟩ ↦ Fin.elim0 i
  | n + 1, p, _ =>
    ⟨fun h ↦ by
      rw [Option.isSome_iff_exists] at h
      obtain ⟨i, hi⟩ := h
      exact ⟨i, find_spec _ hi⟩, fun ⟨⟨i, hin⟩, hi⟩ ↦ by
      dsimp [find]
      rcases h : find fun i : Fin n ↦ p (i.castLT (Nat.lt_succ_of_lt i.2)) with - | j
      · split_ifs with hl
        · exact Option.isSome_some
        · have := (@isSome_find_iff n (fun x ↦ p (x.castLT (Nat.lt_succ_of_lt x.2))) _).2
              ⟨⟨i, lt_of_le_of_ne (Nat.le_of_lt_succ hin) fun h ↦ by cases h; exact hl hi⟩, hi⟩
          rw [h] at this
          exact this
      · simp⟩

Existence of Satisfying Index in Finite Tuples via $\mathrm{find}$

Informal description

For any natural number $n$ and a decidable predicate $p$ on $\mathrm{Fin}\,n$, the result of $\mathrm{find}\,p$ is non-empty (i.e., $\mathrm{find}\,p \neq \mathrm{none}$) if and only if there exists some index $i \in \mathrm{Fin}\,n$ such that $p(i)$ holds.

Fin.find_eq_none_iff theorem

{n : ℕ} {p : Fin n → Prop} [DecidablePred p] : find p = none ↔ ∀ i, ¬p i

Full source

/-- `find p` returns `none` if and only if `p i` never holds. -/
theorem find_eq_none_iff {n : ℕ} {p : Fin n → Prop} [DecidablePred p] :
    findfind p = none ↔ ∀ i, ¬p i := by rw [← not_exists, ← isSome_find_iff]; cases find p <;> simp

Characterization of $\mathrm{find}$ Returning `none` in Finite Tuples

Informal description

For any natural number $n$ and a decidable predicate $p$ on $\mathrm{Fin}\,n$, the function $\mathrm{find}\,p$ returns `none` if and only if there does not exist any index $i \in \mathrm{Fin}\,n$ such that $p(i)$ holds. In other words, $\mathrm{find}\,p = \mathrm{none} \leftrightarrow \forall i, \neg p(i)$.

Fin.find_min theorem

 : ∀ {n : ℕ} {p : Fin n → Prop} [DecidablePred p] {i : Fin n} (_ : i ∈ Fin.find p) {j : Fin n} (_ : j < i), ¬p j

Full source

/-- If `find p` returns `some i`, then `p j` does not hold for `j < i`, i.e., `i` is minimal among
the indices where `p` holds. -/
theorem find_min :
    ∀ {n : ℕ} {p : Fin n → Prop} [DecidablePred p] {i : Fin n} (_ : i ∈ Fin.find p) {j : Fin n}
      (_ : j < i), ¬p j
  | 0, _, _, _, hi, _, _, _ => Option.noConfusion hi
  | n + 1, p, _, i, hi, ⟨j, hjn⟩, hj, hpj => by
    rw [find] at hi
    rcases h : find fun i : Fin n ↦ p (i.castLT (Nat.lt_succ_of_lt i.2)) with - | k
    · simp only [h] at hi
      split_ifs at hi with hl
      · cases hi
        rw [find_eq_none_iff] at h
        exact h ⟨j, hj⟩ hpj
      · exact Option.not_mem_none _ hi
    · rw [h] at hi
      dsimp at hi
      obtain rfl := Option.some_inj.1 hi
      exact find_min h (show (⟨j, lt_trans hj k.2⟩ : Fin n) < k from hj) hpj

Minimality of First Satisfying Index in Finite Tuples

Informal description

For any natural number $n$ and a decidable predicate $p$ on $\mathrm{Fin}\,n$, if $i$ is the first index returned by $\mathrm{find}\,p$ (i.e., $i \in \mathrm{find}\,p$), then for any index $j < i$, the predicate $p(j)$ does not hold.

Fin.find_min' theorem

{p : Fin n → Prop} [DecidablePred p] {i : Fin n} (h : i ∈ Fin.find p) {j : Fin n} (hj : p j) : i ≤ j

Full source

theorem find_min' {p : Fin n → Prop} [DecidablePred p] {i : Fin n} (h : i ∈ Fin.find p) {j : Fin n}
    (hj : p j) : i ≤ j := Fin.not_lt.1 fun hij ↦ find_min h hij hj

Minimality of First Satisfying Index in Finite Tuples with Respect to Predicate

Informal description

For any natural number $n$ and a decidable predicate $p$ on $\mathrm{Fin}\,n$, if $i$ is the first index returned by $\mathrm{find}\,p$ (i.e., $i \in \mathrm{find}\,p$), then for any index $j$ satisfying $p(j)$, we have $i \leq j$.

Fin.nat_find_mem_find theorem

 {p : Fin n → Prop} [DecidablePred p] (h : ∃ i, ∃ hin : i < n, p ⟨i, hin⟩) :
  (⟨Nat.find h, (Nat.find_spec h).fst⟩ : Fin n) ∈ find p

Full source

theorem nat_find_mem_find {p : Fin n → Prop} [DecidablePred p]
    (h : ∃ i, ∃ hin : i < n, p ⟨i, hin⟩) :
    (⟨Nat.find h, (Nat.find_spec h).fst⟩ : Fin n) ∈ find p := by
  let ⟨i, hin, hi⟩ := h
  rcases hf : find p with - | f
  · rw [find_eq_none_iff] at hf
    exact (hf ⟨i, hin⟩ hi).elim
  · refine Option.some_inj.2 (Fin.le_antisymm ?_ ?_)
    · exact find_min' hf (Nat.find_spec h).snd
    · exact Nat.find_min' _ ⟨f.2, by convert find_spec p hf⟩

Correspondence between $\mathrm{Nat.find}$ and $\mathrm{Fin.find}$ for Satisfiable Predicates

Informal description

For any natural number $n$ and a decidable predicate $p$ on $\mathrm{Fin}\,n$, if there exists an index $i < n$ such that $p(i)$ holds, then the element $\langle \mathrm{Nat.find}\,h, (\mathrm{Nat.find\_spec}\,h).1 \rangle$ of $\mathrm{Fin}\,n$ is contained in $\mathrm{find}\,p$, where $h$ is the proof of existence of such an $i$.

Fin.mem_find_iff theorem

{p : Fin n → Prop} [DecidablePred p] {i : Fin n} : i ∈ Fin.find p ↔ p i ∧ ∀ j, p j → i ≤ j

Full source

theorem mem_find_iff {p : Fin n → Prop} [DecidablePred p] {i : Fin n} :
    i ∈ Fin.find pi ∈ Fin.find p ↔ p i ∧ ∀ j, p j → i ≤ j :=
  ⟨fun hi ↦ ⟨find_spec _ hi, fun _ ↦ find_min' hi⟩, by
    rintro ⟨hpi, hj⟩
    cases hfp : Fin.find p
    · rw [find_eq_none_iff] at hfp
      exact (hfp _ hpi).elim
    · exact Option.some_inj.2 (Fin.le_antisymm (find_min' hfp hpi) (hj _ (find_spec _ hfp)))⟩

Characterization of Membership in $\mathrm{find}$ for Finite Tuples

Informal description

For any natural number $n$, a decidable predicate $p$ on $\mathrm{Fin}\,n$, and an index $i \in \mathrm{Fin}\,n$, the index $i$ is in the result of $\mathrm{find}\,p$ if and only if $p(i)$ holds and for all indices $j \in \mathrm{Fin}\,n$ satisfying $p(j)$, we have $i \leq j$. In other words, $i \in \mathrm{find}\,p \leftrightarrow \big(p(i) \land \forall j, p(j) \to i \leq j\big)$.

Fin.find_eq_some_iff theorem

{p : Fin n → Prop} [DecidablePred p] {i : Fin n} : Fin.find p = some i ↔ p i ∧ ∀ j, p j → i ≤ j

Full source

theorem find_eq_some_iff {p : Fin n → Prop} [DecidablePred p] {i : Fin n} :
    Fin.findFin.find p = some i ↔ p i ∧ ∀ j, p j → i ≤ j :=
  mem_find_iff

Characterization of $\mathrm{find}\,p = \mathrm{some}\,i$ for Finite Tuples

Informal description

For any natural number $n$, a decidable predicate $p$ on $\mathrm{Fin}\,n$, and an index $i \in \mathrm{Fin}\,n$, the result of $\mathrm{find}\,p$ is equal to $\mathrm{some}\,i$ if and only if $p(i)$ holds and for all indices $j \in \mathrm{Fin}\,n$ satisfying $p(j)$, we have $i \leq j$. In other words, $\mathrm{find}\,p = \mathrm{some}\,i \leftrightarrow \big(p(i) \land \forall j, p(j) \to i \leq j\big)$.

Fin.mem_find_of_unique theorem

{p : Fin n → Prop} [DecidablePred p] (h : ∀ i j, p i → p j → i = j) {i : Fin n} (hi : p i) : i ∈ Fin.find p

Full source

theorem mem_find_of_unique {p : Fin n → Prop} [DecidablePred p] (h : ∀ i j, p i → p j → i = j)
    {i : Fin n} (hi : p i) : i ∈ Fin.find p :=
  mem_find_iff.2 ⟨hi, fun j hj ↦ Fin.le_of_eq <| h i j hi hj⟩

Unique Satisfying Index Belongs to Find Result in Finite Tuples

Informal description

For any natural number $n$, a decidable predicate $p$ on $\mathrm{Fin}\,n$, and an index $i \in \mathrm{Fin}\,n$, if $p$ is uniquely satisfied at $i$ (i.e., for all $j \in \mathrm{Fin}\,n$, $p(j)$ implies $j = i$), then $i$ is in the result of $\mathrm{find}\,p$. In other words, if $p(i)$ holds and $p$ is uniquely satisfied at $i$, then $i \in \mathrm{find}\,p$.

Fin.contractNth definition

(j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n) : α

Full source

/-- Sends `(g₀, ..., gₙ)` to `(g₀, ..., op gⱼ gⱼ₊₁, ..., gₙ)`. -/
def contractNth (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n) : α :=
  if (k : ℕ) < j then g (Fin.castSucc k)
  else if (k : ℕ) = j then op (g (Fin.castSucc k)) (g k.succ) else g k.succ

Tuple contraction at a given position

Informal description

Given a position $j$ in a tuple of length $n+1$, a binary operation $\mathrm{op} : \alpha \to \alpha \to \alpha$, and a tuple $g : \mathrm{Fin}(n+1) \to \alpha$, the function $\mathrm{contractNth}$ returns a new tuple of length $n$ where: - For indices $k < j$, the value is $g(k)$ (using $\mathrm{Fin.castSucc}$ to adjust the index). - For index $k = j$, the value is $\mathrm{op}(g(k), g(k+1))$. - For indices $k > j$, the value is $g(k+1)$. In other words, this operation contracts the tuple at position $j$ by combining the elements at positions $j$ and $j+1$ using the operation $\mathrm{op}$.

Fin.contractNth_apply_of_lt theorem

 (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n) (h : (k : ℕ) < j) :
  contractNth j op g k = g (Fin.castSucc k)

Full source

theorem contractNth_apply_of_lt (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n)
    (h : (k : ℕ) < j) : contractNth j op g k = g (Fin.castSucc k) :=
  if_pos h

Contracted Tuple Value for Indices Less Than Pivot

Informal description

For a position $j$ in a tuple of length $n+1$, a binary operation $\mathrm{op} : \alpha \to \alpha \to \alpha$, and a tuple $g : \mathrm{Fin}(n+1) \to \alpha$, if $k$ is an index in the contracted tuple of length $n$ such that $k < j$ (as natural numbers), then the value of the contracted tuple at $k$ is equal to $g$ evaluated at the casted index $\mathrm{Fin.castSucc}\,k$. In other words, $\mathrm{contractNth}\,j\,\mathrm{op}\,g\,k = g(\mathrm{castSucc}\,k)$ when $k < j$.

Fin.contractNth_apply_of_eq theorem

 (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n) (h : (k : ℕ) = j) :
  contractNth j op g k = op (g (Fin.castSucc k)) (g k.succ)

Full source

theorem contractNth_apply_of_eq (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n)
    (h : (k : ℕ) = j) : contractNth j op g k = op (g (Fin.castSucc k)) (g k.succ) := by
  have : ¬(k : ℕ) < j := not_lt.2 (le_of_eq h.symm)
  rw [contractNth, if_neg this, if_pos h]

Value of Contracted Tuple at Matching Index

Informal description

Let $j$ be a position in a tuple of length $n+1$, $\mathrm{op} : \alpha \to \alpha \to \alpha$ a binary operation, and $g : \mathrm{Fin}(n+1) \to \alpha$ a tuple. For any index $k : \mathrm{Fin}(n)$ such that $k = j$ (as natural numbers), the contracted tuple satisfies: \[ \mathrm{contractNth}\,j\,\mathrm{op}\,g\,k = \mathrm{op}\,(g\,(\mathrm{castSucc}\,k))\,(g\,(k.\mathrm{succ})) \]

Fin.contractNth_apply_of_gt theorem

 (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n) (h : (j : ℕ) < k) :
  contractNth j op g k = g k.succ

Full source

theorem contractNth_apply_of_gt (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n)
    (h : (j : ℕ) < k) : contractNth j op g k = g k.succ := by
  rw [contractNth, if_neg (not_lt_of_gt h), if_neg (Ne.symm <| ne_of_lt h)]

Contraction of Tuple at Index Greater Than Given Position

Informal description

For any position $j$ in a tuple of length $n+1$, a binary operation $\mathrm{op} : \alpha \to \alpha \to \alpha$, and a tuple $g : \mathrm{Fin}(n+1) \to \alpha$, if an index $k$ satisfies $j < k$ (as natural numbers), then the contracted tuple at $k$ is equal to $g(k+1)$. That is, $\mathrm{contractNth}\,j\,\mathrm{op}\,g\,k = g(k+1)$.

Fin.contractNth_apply_of_ne theorem

 (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n) (hjk : (j : ℕ) ≠ k) :
  contractNth j op g k = g (j.succAbove k)

Full source

theorem contractNth_apply_of_ne (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n)
    (hjk : (j : ℕ) ≠ k) : contractNth j op g k = g (j.succAbove k) := by
  rcases lt_trichotomy (k : ℕ) j with (h | h | h)
  · rwa [j.succAbove_of_castSucc_lt, contractNth_apply_of_lt]
    · rwa [Fin.lt_iff_val_lt_val]
  · exact False.elim (hjk h.symm)
  · rwa [j.succAbove_of_le_castSucc, contractNth_apply_of_gt]
    · exact Fin.le_iff_val_le_val.2 (le_of_lt h)

Contracted Tuple Value at Unequal Indices via $\mathrm{succAbove}$

Informal description

For a position $j$ in a tuple of length $n+1$, a binary operation $\mathrm{op} : \alpha \to \alpha \to \alpha$, and a tuple $g : \mathrm{Fin}(n+1) \to \alpha$, if an index $k$ in the contracted tuple satisfies $j \neq k$ (as natural numbers), then the value of the contracted tuple at $k$ is equal to $g$ evaluated at the index adjusted by $\mathrm{succAbove}$, i.e., $\mathrm{contractNth}\,j\,\mathrm{op}\,g\,k = g(j.\mathrm{succAbove}\,k)$.

Fin.comp_contractNth theorem

 {β : Sort*} (opα : α → α → α) (opβ : β → β → β) {f : α → β} (hf : ∀ x y, f (opα x y) = opβ (f x) (f y))
  (j : Fin (n + 1)) (g : Fin (n + 1) → α) : f ∘ contractNth j opα g = contractNth j opβ (f ∘ g)

Full source

lemma comp_contractNth {β : Sort*} (opα : α → α → α) (opβ : β → β → β) {f : α → β}
    (hf : ∀ x y, f (opα x y) = opβ (f x) (f y)) (j : Fin (n + 1)) (g : Fin (n + 1) → α) :
    f ∘ contractNth j opα g = contractNth j opβ (f ∘ g) := by
  ext x
  rcases lt_trichotomy (x : ℕ) j with (h|h|h)
  · simp only [Function.comp_apply, contractNth_apply_of_lt, h]
  · simp only [Function.comp_apply, contractNth_apply_of_eq, h, hf]
  · simp only [Function.comp_apply, contractNth_apply_of_gt, h]

Composition Homomorphism Property for Contracted Tuples

Informal description

Let $\alpha$ and $\beta$ be types, and let $\mathrm{op}_\alpha : \alpha \to \alpha \to \alpha$ and $\mathrm{op}_\beta : \beta \to \beta \to \beta$ be binary operations. Given a function $f : \alpha \to \beta$ that satisfies the homomorphism condition $f(\mathrm{op}_\alpha\,x\,y) = \mathrm{op}_\beta\,(f\,x)\,(f\,y)$ for all $x, y \in \alpha$, a position $j$ in a tuple of length $n+1$, and a tuple $g : \mathrm{Fin}(n+1) \to \alpha$, the composition of $f$ with the contracted tuple $\mathrm{contractNth}\,j\,\mathrm{op}_\alpha\,g$ is equal to the contracted tuple of the composition $f \circ g$ with respect to $\mathrm{op}_\beta$ at position $j$. That is, \[ f \circ (\mathrm{contractNth}\,j\,\mathrm{op}_\alpha\,g) = \mathrm{contractNth}\,j\,\mathrm{op}_\beta\,(f \circ g). \]

Fin.sigma_eq_of_eq_comp_cast theorem

{α : Type*} : ∀ {a b : Σ ii, Fin ii → α} (h : a.fst = b.fst), a.snd = b.snd ∘ Fin.cast h → a = b

Full source

/-- To show two sigma pairs of tuples agree, it to show the second elements are related via
`Fin.cast`. -/
theorem sigma_eq_of_eq_comp_cast {α : Type*} :
    ∀ {a b : Σ ii, Fin ii → α} (h : a.fst = b.fst), a.snd = b.snd ∘ Fin.cast h → a = b
  | ⟨ai, a⟩, ⟨bi, b⟩, hi, h => by
    dsimp only at hi
    subst hi
    simpa using h

Equality of Dependent Pairs via Cast Composition

Informal description

Let $\alpha$ be a type, and let $a$ and $b$ be pairs of the form $(n, f)$ where $n$ is a natural number and $f$ is a function from $\text{Fin}(n)$ to $\alpha$. If the first components of $a$ and $b$ are equal (i.e., $a_1 = b_1$) and the second component of $a$ is equal to the composition of the second component of $b$ with the canonical cast function $\text{Fin.cast}$ (i.e., $a_2 = b_2 \circ \text{Fin.cast}(h)$ where $h$ is the proof of $a_1 = b_1$), then $a = b$.

Fin.sigma_eq_iff_eq_comp_cast theorem

{α : Type*} {a b : Σ ii, Fin ii → α} : a = b ↔ ∃ h : a.fst = b.fst, a.snd = b.snd ∘ Fin.cast h

Full source

/-- `Fin.sigma_eq_of_eq_comp_cast` as an `iff`. -/
theorem sigma_eq_iff_eq_comp_cast {α : Type*} {a b : Σ ii, Fin ii → α} :
    a = b ↔ ∃ h : a.fst = b.fst, a.snd = b.snd ∘ Fin.cast h :=
  ⟨fun h ↦ h ▸ ⟨rfl, funext <| Fin.rec fun _ _ ↦ rfl⟩, fun ⟨_, h'⟩ ↦
    sigma_eq_of_eq_comp_cast _ h'⟩

Characterization of Equality for Dependent Pairs via Cast Composition

Informal description

Let $\alpha$ be a type, and let $a$ and $b$ be dependent pairs of the form $(n, f)$ where $n$ is a natural number and $f : \text{Fin}(n) \to \alpha$. Then $a = b$ if and only if there exists a proof $h : a_1 = b_1$ (equality of the first components) such that $a_2 = b_2 \circ \text{Fin.cast}(h)$ (the second component of $a$ equals the composition of the second component of $b$ with the canonical cast function induced by $h$).

piFinTwoEquiv definition

(α : Fin 2 → Type u) : (∀ i, α i) ≃ α 0 × α 1

Full source

/-- `Π i : Fin 2, α i` is equivalent to `α 0 × α 1`. See also `finTwoArrowEquiv` for a
non-dependent version and `prodEquivPiFinTwo` for a version with inputs `α β : Type u`. -/
@[simps -fullyApplied]
def piFinTwoEquiv (α : Fin 2 → Type u) : (∀ i, α i) ≃ α 0 × α 1 where
  toFun f := (f 0, f 1)
  invFun p := Fin.cons p.1 <| Fin.cons p.2 finZeroElim
  left_inv _ := funext <| Fin.forall_fin_two.2 ⟨rfl, rfl⟩
  right_inv := fun _ => rfl

Equivalence between dependent functions on `Fin 2` and pairs

Informal description

The equivalence `piFinTwoEquiv` establishes a bijection between dependent functions on `Fin 2` (i.e., pairs of elements where the first is of type `α 0` and the second is of type `α 1`) and the Cartesian product `α 0 × α 1`. Specifically: - The forward direction maps a function `f : ∀ i : Fin 2, α i` to the pair `(f 0, f 1)`. - The backward direction reconstructs the function from a pair `(x, y)` by prepending `x` and `y` using `Fin.cons`, with the empty case handled by `finZeroElim`.

Mathlib.Data.Fin.Tuple.Basic

Main declarations

Adding at the start

Adding at the end

Adding in the middle

Miscellaneous