Slice notation instances for Fin tuples

This file provides instances of the generic slice type classes (SliceLT, SliceGE, Slice) for Fin tuples, enabling Python-like slice notation:

• v⟦:m⟧ takes the first m elements
• v⟦m:⟧ drops the first m elements
• v⟦m₁:m₂⟧ takes elements from index m₁ to m₂ - 1

The instances work for both homogeneous (Fin n → α) and heterogeneous ((i : Fin n) → α i) Fin tuples, delegating to the existing Fin.take and Fin.drop operations.

Each notation also supports manual proof syntax with 'h:

• v⟦:m⟧'h for explicit proof in take operations
• v⟦m:⟧'h for explicit proof in drop operations
• v⟦m₁:m₂⟧'⟨h₁, h₂⟩ for explicit proofs in range operations

Examples

variable (v : Fin 10 → ℕ)

#check v⟦:5⟧   -- Takes first 5 elements: Fin 5 → ℕ
#check v⟦3:⟧   -- Drops first 3 elements: Fin 7 → ℕ
#check v⟦2:8⟧  -- Elements 2 through 7: Fin 6 → ℕ

Instances for Fin tuples

@[implicit_reducible]

instance Fin.instSliceLTForallNatLeForallCastLE {n : ℕ} {α : Fin n → Type u_1} : SliceLT ((i : Fin n) → α i) ℕ (fun (x : (i : Fin n) → α i) (stop : ℕ) => stop ≤ n) fun (x : (i : Fin n) → α i) (stop : ℕ) (h : stop ≤ n) => (i : Fin stop) → α (castLE h i)

@[implicit_reducible]

instance Fin.instSliceGEForallNatLeForallCastAddNat {n : ℕ} {α : Fin n → Type u_1} : SliceGE ((i : Fin n) → α i) ℕ (fun (x : (i : Fin n) → α i) (start : ℕ) => start ≤ n) fun (x : (i : Fin n) → α i) (start : ℕ) (h : start ≤ n) => (i : Fin (n - start)) → α (Fin.cast ⋯ (i.addNat start))

@[implicit_reducible]

instance Fin.instSliceForallNatAndLeForallCastLECastAddNat {n : ℕ} {α : Fin n → Type u_1} : Slice ((i : Fin n) → α i) ℕ ℕ (fun (x : (i : Fin n) → α i) (start stop : ℕ) => start ≤ stop ∧ stop ≤ n) fun (x : (i : Fin n) → α i) (start stop : ℕ) (h : start ≤ stop ∧ stop ≤ n) => (i : Fin (stop - start)) → α (castLE ⋯ (Fin.cast ⋯ (i.addNat start)))

Examples showing the Python-like slice notation works correctly

Comprehensive Tuple Notation System with Better Definitional Equality

This file provides a unified notation system for Fin-indexed tuples with better definitional equality through pattern matching. The system supports homogeneous vectors, heterogeneous tuples, dependent tuples, and functorial operations, all with consistent notation patterns.

Vector and Tuple Construction Notation:

Homogeneous Vectors (all elements have the same type):

• !v[a, b, c] - basic homogeneous vector
• !v⟨α⟩[a, b, c] - with explicit type ascription

Heterogeneous Tuples (elements can have different types):

• !h[a, b, c] - basic heterogeneous tuple (uses hcons)
• !h⟨α⟩[a, b, c] - heterogeneous tuple with type vector ascription
• !h⦃F⦄[a, b, c] - functorial with explicit unary functor F but implicit type vector
• !h⦃F⦄⟨α⟩[a, b, c] - functorial with unary functor F and type vector α
• !h⦃F⦄⟨α₁⟩⟨α₂⟩[a, b, c] - functorial with binary functor F and type vectors α₁ and α₂

Dependent Tuples (with explicit motive specification):

• !d[a, b, c] - basic dependent tuple (uses dcons)
• !d⟨motive⟩[a, b, c] - with explicit motive

Infix Operations:

Cons Operations (prepend element):

• a ::ᵛ v - homogeneous cons
• a ::ᵛ⟨α⟩ v - homogeneous cons with explicit type ascription
• a ::ʰ t - heterogeneous cons
• a ::ʰ⟨α; β⟩ t - heterogeneous cons with explicit type ascription
• a ::ʰ⦃F⦄ t - functorial cons (unary) with type besides F inferred
• a ::ʰ⦃F⦄⟨α; β⟩ t - functorial cons (unary) with explicit type ascription
• a ::ʰ⦃F⦄⟨α₁; β₁⟩⟨α₂; β₂⟩ t - functorial cons (binary) with explicit type ascription
• a ::ᵈ t - dependent cons
• a ::ᵈ⟨motive⟩ t - dependent cons with explicit motive

Concat Operations (append element):

• v :+ᵛ a - homogeneous concat
• v :+ᵛ⟨α⟩ a - homogeneous concat with explicit type ascription
• t :+ʰ a - heterogeneous concat
• t :+ʰ⟨α; β⟩ a - heterogeneous concat with explicit type ascription
• t :+ʰ⦃F⦄ a - functorial concat (unary) with type besides F inferred
• t :+ʰ⦃F⦄⟨α; β⟩ a - functorial concat (unary)
• t :+ʰ⦃F⦄⟨α₁; β₁⟩⟨α₂; β₂⟩ a - functorial concat (binary)
• t :+ᵈ a - dependent concat
• t :+ᵈ⟨motive⟩ a - dependent concat with explicit motive

Append Operations (concatenate two tuples):

• u ++ᵛ v - homogeneous append
• u ++ᵛ⟨α⟩ v - homogeneous append with explicit type ascription
• u ++ʰ v - heterogeneous append
• u ++ʰ⟨α; β⟩ v - heterogeneous append with explicit type ascription
• u ++ʰ⦃F⦄ v - functorial append (unary) with type besides F inferred
• u ++ʰ⦃F⦄⟨α; β⟩ v - functorial append (unary)
• u ++ʰ⦃F⦄⟨α₁; β₁⟩⟨α₂; β₂⟩ v - functorial append (binary)
• u ++ᵈ v - dependent append
• u ++ᵈ⟨motive⟩ v - dependent append with explicit motive

Design Principles:

1. Better Definitional Equality: All operations use pattern matching instead of cases, addCases, or conditional statements for superior computational behavior.

2. Unified h Superscript: All heterogeneous and functorial operations use the h superscript with explicit type ascriptions when needed.

3. Semicolon Separators: Functorial operations use α; β syntax to clearly distinguish the two type arguments required for functor application.

4. Consistent Type Ascriptions: Explicit type information uses ⟨...⟩ brackets throughout.

5. Unexpander Conflict Resolution: Each construction function (hcons, dcons, etc.) has its own dedicated notation to prevent pretty-printing ambiguities.

This system replaces Mathlib's Matrix.vecCons/Matrix.vecEmpty approach with our custom functions that provide better definitional equality and a more comprehensive type hierarchy.

def Fin.«term_::ᵛ_» : Lean.TrailingParserDescr

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.«term_:+ᵛ_» : Lean.TrailingParserDescr

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

Notation: v :+ᵛ a.

def Fin.«term_::ᵛ⟨_⟩_» : Lean.TrailingParserDescr

::ᵛ⟨α⟩ notation for homogeneous cons with explicit element type.

def Fin.«term_:+ᵛ⟨_⟩_» : Lean.TrailingParserDescr

:+ᵛ⟨α⟩ notation for homogeneous concat with explicit element type.

def Fin.«term_++ᵛ⟨_⟩_» : Lean.TrailingParserDescr

++ᵛ⟨α⟩ notation for homogeneous append with explicit element type.

def Fin.finVecNotation : Lean.ParserDescr

!v[...] notation constructs a vector using our custom functions. Uses !v[...] to distinguish from standard ![].

def Fin.finVecNotationWithType : Lean.ParserDescr

!v⟨α⟩[...] notation constructs a vector with explicit type ascription. Uses angle brackets to specify the element type, then square brackets for values.

def Fin.vconsUnexpander : Lean.PrettyPrinter.Unexpander

Unexpander for the !v[x, y, ...] notation.

def Fin.vemptyUnexpander : Lean.PrettyPrinter.Unexpander

Unexpander for the !v[] notation.

def Fin.«term_::ʰ_» : Lean.TrailingParserDescr

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.«term_:+ʰ_» : Lean.TrailingParserDescr

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.«term_::ʰ⟨_;_⟩_» : Lean.TrailingParserDescr

::ʰ⟨α; β⟩ notation for hcons with explicit type ascriptions

def Fin.«term_:+ʰ⟨_;_⟩_» : Lean.TrailingParserDescr

:+ʰ⟨α; β⟩ notation for hconcat with explicit type ascriptions

def Fin.«term_::ʰ⦃_⦄_» : Lean.TrailingParserDescr

Functorial cons with explicit functor but inferred type families: ::ʰ⦃F⦄.

def Fin.«term_::ʰ⦃_⦄⟨_;_⟩_» : Lean.TrailingParserDescr

Functorial cons (unary) with explicit types: ::ʰ⦃F⦄⟨α; β⟩.

def Fin.«term_::ʰ⦃_⦄⟨_;_⟩⟨_;_⟩_» : Lean.TrailingParserDescr

Functorial cons (binary) with explicit types: ::ʰ⦃F⦄⟨α₁; β₁⟩⟨α₂; β₂⟩.

def Fin.«term_::ᵈ_» : Lean.TrailingParserDescr

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.«term_:+ᵈ_» : Lean.TrailingParserDescr

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.«term_::ᵈ⟨_⟩_» : Lean.TrailingParserDescr

::ᵈ⟨motive⟩ notation for dcons with explicit motive specification

def Fin.«term_:+ᵈ⟨_⟩_» : Lean.TrailingParserDescr

:+ᵈ⟨motive⟩ notation for dconcat with explicit motive specification

def Fin.finHeterogeneousNotation : Lean.ParserDescr

!h[...] notation constructs a heterogeneous tuple using hcons. For automatic type inference without explicit motive.

def Fin.finHeterogeneousNotationWithTypeVec : Lean.ParserDescr

!h⟨α⟩[...] notation constructs a heterogeneous tuple with explicit type vector ascription. Uses angle brackets to specify the type vector, then square brackets for values.

def Fin.finFunctorialHeterogeneousNotationShorthand : Lean.ParserDescr

!h⦃F⦄[...] functorial heterogeneous tuple with explicit functor and implicit type vectors.

def Fin.finDependentNotation : Lean.ParserDescr

!d[...] notation constructs a dependent tuple using our custom dependent functions. Uses !d[...] for dependent tuples with explicit motives.

def Fin.finDependentNotationWithmotive : Lean.ParserDescr

!d⟨motive⟩[...] notation constructs a dependent tuple with explicit motive specification. Uses angle brackets to specify the motive, then square brackets for values.

Functorial heterogeneous tuple constructors with explicit type vectors

def Fin.finFunctorialHeterogeneousNotation : Lean.ParserDescr

Unary functorial: !h⦃F⦄⟨α⟩[...] where α : Fin n → Sort _.

def Fin.finFunctorialBinaryHeterogeneousNotation : Lean.ParserDescr

Binary functorial: !h⦃F⦄⟨α₁⟩⟨α₂⟩[...] where α₁, α₂ : Fin n → Sort _.

def Fin.fconsUnexpander : Lean.PrettyPrinter.Unexpander

def Fin.fcons₂Unexpander : Lean.PrettyPrinter.Unexpander

Functorial concat infix forms to match documentation

def Fin.«term_:+ʰ⦃_⦄_» : Lean.TrailingParserDescr

def Fin.«term_:+ʰ⦃_⦄⟨_;_⟩_» : Lean.TrailingParserDescr

def Fin.«term_:+ʰ⦃_⦄⟨_;_⟩⟨_;_⟩_» : Lean.TrailingParserDescr

def Fin.hconsUnexpander : Lean.PrettyPrinter.Unexpander

Unexpander for the !h[x, y, ...] notation using hcons.

def Fin.demptyUnexpander : Lean.PrettyPrinter.Unexpander

Unexpander for the !h[] and !d[] notation.

def Fin.dconsUnexpander : Lean.PrettyPrinter.Unexpander

Unexpander for the !d[x, y, ...] notation using dcons with explicit motive.

def «term_++ᵛ_» : Lean.TrailingParserDescr

Homogeneous vector append notation ++ᵛ

def «term_++ᵈ_» : Lean.TrailingParserDescr

Dependent append notation ++ᵈ

def «term_++ʰ_» : Lean.TrailingParserDescr

Heterogeneous append notation ++ʰ

def «term_++ʰ⟨_;_⟩_» : Lean.TrailingParserDescr

Heterogeneous append with explicit type ascriptions: ++ʰ⟨α; β⟩

def «term_++ᵈ⟨_⟩_» : Lean.TrailingParserDescr

Dependent append with explicit motive: ++ᵈ⟨motive⟩

def «term_++ʰ⦃_⦄_» : Lean.TrailingParserDescr

Functorial heterogeneous append with explicit functor but inferred types: ++ʰ⦃F⦄.

def «term_++ʰ⦃_⦄⟨_;_⟩_» : Lean.TrailingParserDescr

Functorial heterogeneous append with unary functor: ++ʰ⦃F⦄⟨α; β⟩

def «term_++ʰ⦃_⦄⟨_;_⟩⟨_;_⟩_» : Lean.TrailingParserDescr

Functorial heterogeneous append with binary functor: ++ʰ⦃F⦄⟨α₁; β₁⟩⟨α₂; β₂⟩

def Mymotive : Fin 3 → Type

def MyTypeVec : Fin 3 → Type