Custom Fin tuple operations with better definitional equality

This file provides custom tuple operations that use pattern matching for better definitional equality, replacing standard library functions that rely on complex constructions like cases, addCases, and conditional statements with casts.

Utility operations:

• Fin.rtake: Taking from the right (i.e. the end) of a tuple
• Fin.drop: Dropping from the left (i.e. the beginning) of a tuple
• Fin.rdrop: Dropping from the right (i.e. the end) of a tuple
• Fin.extract: Extract a sub-tuple from a given range
• Fin.rightpad: Padding (or truncation) on the right of a tuple
• Fin.leftpad: Padding (or truncation) on the left of a tuple

Three-Tier Construction System:

Dependent operations (d*): Work with a unified motive Fin n → Sort* that determines the type at each position. These are the foundational operations.

• Fin.dcons, Fin.dconcat, Fin.dappend

Homogeneous operations (v*): Specialize the dependent operations to constant-type motives fun _ => α, creating vectors where all elements have the same type.

• Fin.vcons, Fin.vconcat, Fin.vappend

Functorial operations (f*): Apply a type constructor F uniformly across all positions of a heterogeneous tuple, with the return type constructed using v* operations at the type level. We define versions for both the unary and binary versions of F (arbitrary arity version?)

• Fin.fcons, Fin.fconcat, Fin.fappend
• Fin.fcons₂, Fin.fconcat₂, Fin.fappend₂

Heterogeneous operations (h*): Specialize the unary functorial operations to the identity functor, allowing different types at each position without requiring an explicit motive.

• Fin.hcons, Fin.hconcat, Fin.happend

Empty tuples:

• Fin.dempty/Fin.vempty: Empty tuples for dependent and homogeneous cases

def Fin.rtake {n : ℕ} {α : Fin n → Sort u_1} (m : ℕ) (h : m ≤ n) (v : (i : Fin n) → α i) (i : Fin m) : α (Fin.cast ⋯ (natAdd (n - m) i))

Take the last m elements of a finite vector

def Fin.drop {n : ℕ} {α : Fin n → Sort u_1} (m : ℕ) (h : m ≤ n) (v : (i : Fin n) → α i) (i : Fin (n - m)) : α (Fin.cast ⋯ (i.addNat m))

Drop the first m elements of an n-tuple where m ≤ n, returning an (n - m)-tuple.

@[reducible, inline]

abbrev Fin.rdrop {n : ℕ} {α : Fin n → Sort u_1} (m : ℕ) (h : m ≤ n) (v : (i : Fin n) → α i) (i : Fin (n - m)) : α (Fin.cast ⋯ (castAdd m i))

Drop the last m elements of an n-tuple where m ≤ n, returning an (n - m)-tuple.

This is defined to be taking the first n - m elements of the tuple. Thus, one should not use this and use Fin.take instead.

def Fin.extract {n : ℕ} {α : Fin n → Sort u_1} (start stop : ℕ) (h1 : start ≤ stop) (h2 : stop ≤ n) (v : (i : Fin n) → α i) (i : Fin (stop - start)) : α ⟨↑i + start, ⋯⟩

Extract a sub-tuple from a Fin-tuple, from index start to stop - 1.

theorem Fin.extract_start_zero_eq_take {n : ℕ} {α : Fin n → Sort u_1} (stop : ℕ) (h : stop ≤ n) (v : (i : Fin n) → α i) : extract 0 stop ⋯ h v = take stop h v

Extracting with start = 0 is the same as taking the first stop elements.

theorem Fin.extract_stop_last_eq_drop {n : ℕ} {α : Fin n → Sort u_1} (start : ℕ) (h : start ≤ n) (v : (i : Fin n) → α i) : extract start n h ⋯ v = drop start h v

Extracting with stop = n is the same as dropping the first start elements.

def Fin.rightpad {m : ℕ} {α : Sort u_1} (n : ℕ) (a : α) (v : Fin m → α) : Fin n → α

Pad a Fin-indexed vector on the right with an element a.

This becomes truncation if n < m.

def Fin.leftpad {m : ℕ} {α : Sort u_1} (n : ℕ) (a : α) (v : Fin m → α) : Fin n → α

Pad a Fin-indexed vector on the left with an element a.

This becomes truncation if n < m.

def Fin.dcons {n : ℕ} {motive : Fin (n + 1) → Sort u} (a : motive 0) (b : (i : Fin n) → motive i.succ) (i : Fin (n + 1)) : motive i

Dependent cons with unified motive: prepends a : motive 0 to a dependent tuple (i : Fin n) → motive i.succ using pattern matching for better definitional equality.

This is meant to replace Fin.cons for dependent tuples with a unified motive.

Notation: a ::ᵈ b or a ::ᵈ⟨motive⟩ b for explicit motive specification.

def Fin.dconcat {n : ℕ} {motive : Fin (n + 1) → Sort u} (u : (i : Fin n) → motive i.castSucc) (a : motive (last n)) (i : Fin (n + 1)) : motive i

Dependent snoc with unified motive: appends a : motive (last n) to the end of a dependent tuple (i : Fin n) → motive i.castSucc using pattern matching for better definitional equality.

This is meant to replace Fin.snoc for dependent tuples with a unified motive.

Notation: u :+ᵈ a or u :+ᵈ⟨motive⟩ a for explicit motive specification.

def Fin.dappend {m n : ℕ} {motive : Fin (m + n) → Sort u} (u : (i : Fin m) → motive (castAdd n i)) (v : (i : Fin n) → motive (natAdd m i)) (i : Fin (m + n)) : motive i

Dependent append with unified motive: concatenates two dependent tuples under a shared motive using pattern matching for better definitional equality.

This is meant to replace Fin.addCases for dependent tuples with a unified motive.

Notation: u ++ᵈ v or u ++ᵈ⟨motive⟩ v for explicit motive specification.

@[reducible, inline]

abbrev Fin.vempty {α : Sort u_2} : Fin 0 → α

vempty is the empty vector, and a wrapper around Fin.elim0.

Notation: !v[] or !v⟨α⟩[] with explicit type ascription.

def Fin.vcons {α : Sort u_1} {n : ℕ} (a : α) (v : Fin n → α) : Fin (n + 1) → α

Homogeneous cons: prepends a : α to a vector by specializing dcons to the constant-type motive fun _ => α.

Notation: a ::ᵛ v (using standard :: for vectors).

def Fin.vconcat {α : Sort u_1} {n : ℕ} (v : Fin n → α) (a : α) : Fin (n + 1) → α

Homogeneous snoc: appends a : α to the end of a vector by specializing dconcat to the constant-type motive fun _ => α.

Notation: v :+ᵛ a.

def Fin.vappend {m n : ℕ} {α : Sort u_2} (u : Fin m → α) (v : Fin n → α) : Fin (m + n) → α

Homogeneous append: concatenates two vectors by specializing dappend to the constant-type motive fun _ => α.

Notation: u ++ᵛ v or standard u ++ v.

def Fin.dempty {α : Fin 0 → Sort u} (i : Fin 0) : α i

dempty is the dependent empty tuple.

Notation: !d[], !d⟨motive⟩[], or !h[] for heterogeneous usage.

def Fin.fcons {A : Sort u} {F : A → Sort v} {n : ℕ} {α : A} {β : Fin n → A} (a : F α) (b : (i : Fin n) → F (β i)) (i : Fin (n + 1)) : F (vcons α β i)

Functorial cons: prepends a : F α to a functorial tuple (i : Fin n) → F (β i), with the return type constructed as (i : Fin (n + 1)) → F (vcons α β i) where F is applied to the motive built by vcons at the type level.

Unlike dcons which requires an explicit unified motive, fcons uses vcons to automatically construct the motive from the input types and applies functor F uniformly. When F is the identity functor, this reduces to hcons.

Notation: a ::ʰ⦃F⦄⟨α; β⟩ b with explicit functor and type ascriptions.

def Fin.fcons₂ {A : Sort u} {B : Sort v} {F : A → B → Sort w} {n : ℕ} {α₁ : A} {β₁ : Fin n → A} {α₂ : B} {β₂ : Fin n → B} (a₁ : F α₁ α₂) (b : (i : Fin n) → F (β₁ i) (β₂ i)) (i : Fin (n + 1)) : F (vcons α₁ β₁ i) (vcons α₂ β₂ i)

Functorial cons with two arguments: prepends a : F α₁ α₂ to a functorial tuple (i : Fin n) → F (β₁ i) (β₂ i), with the return type constructed as (i : Fin (n + 1)) → F (vcons α₁ β₁ i) (vcons α₂ β₂ i) where F is applied to the two motives built by vcons at the type level.

Notation: a ::ʰ⦃F⦄⟨α₁; β₁⟩⟨α₂; β₂⟩ b with explicit binary functor and type ascriptions.

def Fin.hcons {n : ℕ} {α : Sort u} {β : Fin n → Sort u} (a : α) (b : (i : Fin n) → β i) (i : Fin (n + 1)) : vcons α β i

Heterogeneous cons: prepends a : α to a tuple (i : Fin n) → β i, with the return type constructed as (i : Fin (n + 1)) → vcons α β i where vcons builds the motive at the type level.

This is a specialization of fcons to the identity functor, allowing different types at each position without requiring an explicit motive.

Notation: a ::ʰ b.

def Fin.fconcat {A : Sort u} {F : A → Sort v} {n : ℕ} {α : Fin n → A} {β : A} (u : (i : Fin n) → F (α i)) (a : F β) (i : Fin (n + 1)) : F (vconcat α β i)

Functorial snoc: appends a : F β to the end of a functorial tuple (i : Fin n) → F (α i), with the return type constructed as (i : Fin (n + 1)) → F (vconcat α β i) where F is applied to the motive built by vconcat at the type level.

Unlike dconcat which requires an explicit unified motive, fconcat uses vconcat to automatically construct the motive from the input types and applies functor F uniformly. When F is the identity functor, this reduces to hconcat.

Notation: u :+ʰ⦃F⦄⟨α; β⟩ a with explicit functor and type ascriptions.

def Fin.fconcat₂ {A : Sort u} {B : Sort v} {F : A → B → Sort w} {n : ℕ} {α₁ : Fin n → A} {β₁ : A} {α₂ : Fin n → B} {β₂ : B} (u : (i : Fin n) → F (α₁ i) (α₂ i)) (a : F β₁ β₂) (i : Fin (n + 1)) : F (vconcat α₁ β₁ i) (vconcat α₂ β₂ i)

Functorial snoc with two arguments: appends a : F β₁ β₂ to the end of a functorial tuple (i : Fin n) → F (α₁ i) (α₂ i), with the return type constructed as (i : Fin (n + 1)) → F (vconcat α₁ β₁ i) (vconcat α₂ β₂ i) where F is applied to the two motives built by vconcat at the type level.

Notation: u :+ʰ⦃F⦄⟨α₁; β₁⟩⟨α₂; β₂⟩ a with explicit binary functor and type ascriptions.

def Fin.hconcat {n : ℕ} {α : Fin n → Sort u} {β : Sort u} (u : (i : Fin n) → α i) (a : β) (i : Fin (n + 1)) : vconcat α β i

Heterogeneous snoc: appends a : β to the end of a tuple (i : Fin n) → α i, with the return type constructed as (i : Fin (n + 1)) → vconcat α β i where vconcat builds the motive at the type level.

This is a specialization of fconcat to the identity functor.

Notation: u :+ʰ a.

def Fin.fappend {A : Sort u} {F : A → Sort v} {m n : ℕ} {α : Fin m → A} {β : Fin n → A} (u : (i : Fin m) → F (α i)) (v : (i : Fin n) → F (β i)) (i : Fin (m + n)) : F (vappend α β i)

Functorial append: concatenates functorial tuples (i : Fin m) → F (α i) and (i : Fin n) → F (β i), with the return type constructed as (i : Fin (m + n)) → F (vappend α β i) where F is applied to the motive built by vappend at the type level.

Unlike dappend which requires an explicit unified motive, fappend uses vappend to automatically construct the motive from the input types and applies functor F uniformly. When F is the identity functor, this reduces to happend.

Notation: u ++ʰ⦃F⦄⟨α; β⟩ v with explicit functor and type ascriptions.

def Fin.fappend₂ {A : Sort u} {B : Sort v} {F : A → B → Sort w} {m n : ℕ} {α₁ : Fin m → A} {β₁ : Fin n → A} {α₂ : Fin m → B} {β₂ : Fin n → B} (u : (i : Fin m) → F (α₁ i) (α₂ i)) (v : (i : Fin n) → F (β₁ i) (β₂ i)) (i : Fin (m + n)) : F (vappend α₁ β₁ i) (vappend α₂ β₂ i)

Functorial append with two arguments: concatenates functorial tuples (i : Fin m) → F (α i) and (i : Fin n) → F (β i), with the return type constructed as (i : Fin (m + n)) → F (vappend α₁ β₁ i) (vappend α₂ β₂ i) where F is applied to the two motives built by vappend at the type level.

Notation: u ++ʰ⦃F⦄⟨α₁; β₁⟩⟨α₂; β₂⟩ v with explicit binary functor and type ascriptions.

def Fin.happend {m n : ℕ} {α : Fin m → Sort u} {β : Fin n → Sort u} (u : (i : Fin m) → α i) (v : (i : Fin n) → β i) (i : Fin (m + n)) : vappend α β i

Heterogeneous append: concatenates tuples (i : Fin m) → α i and (i : Fin n) → β i, with the return type constructed as (i : Fin (m + n)) → vappend α β i where vappend builds the motive at the type level.

This is a specialization of fappend to the identity functor.

Notation: u ++ʰ v.

def Fin.dcast {n n' : ℕ} {α : Fin n → Sort u} {α' : Fin n' → Sort u} (h : n' = n) (hα : ∀ (i : Fin n'), α (Fin.cast h i) = α' i) (v : (i : Fin n) → α i) (i : Fin n') : α' i

Cast a dependent or heterogeneous vector across an equality n' = n and a family of equalities ∀ i, α (Fin.cast h i) = α' i.

This is meant to replace Fin.cast for our use cases, as this definition offers better definitional equality.