ring and ∑

Stream: metaprogramming / tactics

[Tomas Skrivan]

I would like to have a tactic, presumably based on ring, that can deal with ∑. What would be the recommended way of dealing with this?

I'm thinking of extending Ring.ExSum with one extra constructor

 | sum (is : Array Expr) (As : Array Expr) (b : ExProd _ _)

where is is list of free variables with As list of sets over which b should be summed over. However this mean I would have to effectively fork ring. Would there be an approach that keeps most of the ring tactic intact?

Also ideally this should extend to module tactic and different big operators like ∏ or ∫ and ∑' where I would expect users to provide a tactic that could discharge any integrability conditions.

My imagined usage of ring_nf that can do this

import Mathlib.Tactic.Ring
import Mathlib.Algebra.BigOperators.Ring

open BigOperators

variable
  {n} {m} {R} [CommRing R] (f g : Fin n → Fin m → R)
  (ψ : Fin n → R) (φ : Fin m → R) (a : R)

example : ∑ i, ∑ j, f i j + ∑ j, ∑ i, g i j
          =
          ∑ i, ∑ j, (f i j + g i j) := by
  conv => lhs; ring_nf +sum_together

example : ∑ i, ∑ j, (f i j + g i j)
          =
          ∑ i, ∑ j, f i j + ∑ i, ∑ j, g i j := by
  conv => lhs; ring_nf +sum_apart

example : ∑ i, ∑ j, a * f i j
          =
          a * ∑ i, ∑ j, f i j := by
  conv => lhs; ring_nf +sum_mul_pull

-- here we automatically whic
example : ∑ i, ∑ j, f i j * φ j
          =
          ∑ j, φ j * ∑ i, f i j := by
  conv => lhs; ring_nf +sum_mul_pull

[Kevin Buzzard]

Can simp [appropriate lemmas]; ring do this?

[Tomas Skrivan]

I don't think so. For example, I want to pull all the aⱼ i from ∑ i, (a₁ i * ... * aₙ i) that do not depend on i.

[Tomas Skrivan]

Hmm, maybe you can. Here is my attempt. It can turn

∑ i, (a i * b i) * (c * d i * c * a i)

intro

c^2 * ∑ i, d i * b i * (a i)^2

code

import Mathlib.Tactic.Ring
import Mathlib.Algebra.BigOperators.Ring

open BigOperators

variable
  {n} {m} {R} [CommRing R] (f g : Fin n → Fin m → R)
  (ψ : Fin n → R) (φ : Fin m → R) (a : R)

def List.iprod {α I : Type _} [Mul α] [One α] (i : I)  : List (I → α) → α :=
  foldr (fun x y => x i * y) 1

def sum_prod (consts : List R) (vars : List (Fin n → R)) (rest : Fin n → R): R :=
  consts.prod * ∑ i, (vars.iprod i) * rest i

theorem start (a : Fin n → R) : ∑ i, a i = sum_prod [] [] a := sorry

@[simp high]
theorem store_const (a : R) (b : Fin n → R) :
  sum_prod consts vars (fun i => a * b i)
  =
  sum_prod (a :: consts) vars b   := sorry

@[simp low]
theorem store_var (a b : Fin n → R) :
  sum_prod consts vars (fun i => a i * b i)
  =
  sum_prod (consts) (a :: vars) b := sorry

@[simp]
theorem right_assoc (a b c : Fin n → R) :
  sum_prod consts vars (fun i => (a i * b i) * c i)
  =
  sum_prod consts vars (fun i => a i * (b i * c i)) := sorry


example (a b d : Fin n → R) (c : R) :
    ∑ i, (a i * b i) * (c * d i * c * a i)
    =
    c^2 * ∑ i, d i * b i * (a i)^2 := by
  conv =>
    lhs
    simp only [start]
    simp
    simp [sum_prod,List.iprod,← mul_assoc]
    ring_nf

[Tomas Skrivan]

The main idea is to define an auxiliary definition sum_prod which holds the data appropriately sorted. With that you run a set of carefully crafted simp theorems which bit by bit parse the whole expression and sorts all those terms. I'm a bit uneasy about the fact that you are at the peril of simp's theorem precedence and high order unification.