finsum_expand: Expand Finset sums to explicit additions

Tactics

• finsum_expand - expand ∑ k ∈ Finset.Icc 1 3, f k → f 1 + f 2 + f 3
• finsum_expand! - + computed bounds (2*2), non-literal Fin, dite, abs, matrix indexing

Supported

• Intervals: Icc, Ico, Ioc, Ioo, Iic, Iio
• Explicit finsets: {a, b, c}
• Fin sums: ∑ i : Fin n, f i (literal n via Fin.sum_univ_ofNat, else Fin.sum_univ_succ)

Shared utilities in LeanCert.Tactic.VecUtil. Debug: set_option trace.VecUtil.debug true

def tacticFinsum_expand : Lean.ParserDescr

Expand finite sums: ∑ k ∈ Finset.Icc 1 3, f k → f 1 + f 2 + f 3. Supports intervals (Icc, Ico, etc.), explicit finsets, and ∑ i : Fin n, f i. See finsum_expand! for computed bounds, dite, abs, matrix indexing.

Equations

• tacticFinsum_expand = Lean.ParserDescr.node `tacticFinsum_expand 1024 (Lean.ParserDescr.nonReservedSymbol "finsum_expand" false)

def tacticFinsum_expand! : Lean.ParserDescr

finsum_expand + computed bounds (Nat.reduceAdd/Mul/Sub), non-literal Fin (Fin.sum_univ_succ), dite, matrix indexing (VecUtil.vecConsFinMk), abs.

Equations

• tacticFinsum_expand! = Lean.ParserDescr.node `tacticFinsum_expand! 1024 (Lean.ParserDescr.nonReservedSymbol "finsum_expand!" false)