Documentation

LeanCert.Tactic.VecUtil

VecUtil: Shared vector/matrix simplification utilities #

Helpers for Matrix.vecCons expressions, used by VecSimp and FinSumExpand.

Metaprogramming utilities (in VecUtil namespace) #

Shared tactics (outside namespace, for use by other tactics) #

Options #

source
opaque VecUtil.fuel :
Lean.Option ℕ

Maximum recursion depth for vector element extraction. Default: 128.

source
def VecUtil.getFinVal? (e : Lean.Expr) :
Lean.MetaM (Option ℕ)

Extract natural number from a Fin expression. Handles both Fin.mk n proof and numeric literals like (2 : Fin 3). Returns some n if successful, otherwise none.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[irreducible]
    def VecUtil.getVecElem (fuel idx : ℕ) (e : Lean.Expr) :
    Lean.MetaM (Option Lean.Expr)

    Recursively traverse a vecCons chain to extract the element at index idx. Returns some elem if successful, none otherwise.

    Handles:

    • Explicit vecCons chains: vecCons a (vecCons b ...) idx
    • Lambda tails from matrix column extraction: fun i => vecCons ... i
    • Nested vecCons after lambda reduction: when applying a lambda returns another vecCons application that needs further element extraction

    Uses a fuel parameter for termination (decreases on each recursive call).

    Implementation notes #

    inferType vs bindingDomain!: For lambda tails, we use inferType to get the domain type rather than bindingDomain!, because lambdas without explicit binder annotations (e.g., fun i => ... vs fun (i : Fin 2) => ...) may not have the Fin type directly accessible in the binder.

    instantiateMVars + reduce before nat?: When extracting the dimension n from Fin n, we must first instantiateMVars on the type (to substitute assigned metavariables), then reduce nExpr before calling nat?. Without explicit type annotations, nExpr may be Nat.succ ?m (a metavariable wrapped in Nat.succ) rather than a raw literal like 2. The nat? function only matches raw nat literals, so instantiating then reducing converts Nat.succ ?m → 2.

    Recursive extraction: After reducing a lambda application, the result may still be a vecCons applied to an index (e.g., vecCons a tail (Fin.mk k proof)). We recursively extract from this to handle arbitrary nesting depth.

    Equations
    Instances For
      source
      def VecUtil.vecConsFinMk :
      Lean.Meta.Simp.DSimproc

      Simproc: Reduce ![a, b, c, ...] i to the i-th element.

      Handles:

      • Numeric literal indices: ![a, b, c] 2 → c (via int?)
      • Explicit Fin.mk applications: ![a, b, c] ⟨1, proof⟩ → b (via Fin.val reduction)
      • Lambda tails from matrix column extraction: when the tail is fun i => Matrix.vecCons ..., applies the lambda to a synthesized Fin index

      First tries int? to extract raw integer literals (like Mathlib's cons_val), then falls back to reducing Fin.val for explicit Fin.mk expressions.

      The expression structure is: App (Matrix.vecCons α n head tail) idx which gives 5 args total to the vecCons function.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Shared tactics for vector/matrix simplification #

        source
        def tacticVec_index_simp_with_dite :
        Lean.ParserDescr

        Vector indexing with dite conditions and absolute values.

        Reduces ![a,b,c] i → element and handles:

        • if h : 1 ≤ 2 then x else y → x (decidable dite conditions)
        • |literal| → reduced absolute value (positive or negative)

        Strategy: Include abs lemmas IN the main iteration so simp can:

        1. Descend into |...| expressions
        2. Apply of_apply to unwrap Matrix.of
        3. Apply vecConsFinMk to reduce indexing
        4. Apply abs lemmas once we have a literal (for ℚ with decide) Then use norm_num to handle ℝ literals where decide doesn't work. Used by vec_simp!.
        Equations
        Instances For