linear_combination for groups

Stream: mathlib4

[Yaël Dillies]

I just stumbled upon a goal which was very linear_combination-flavoured.

import Mathlib.Tactic.LinearCombination

example {G : Type} [AddCommGroup G] {a b c d : G} (h : a + b = c + d) :
    d - c + (b - a) = d - a + (d - a) := by linear_combination h
-- failed to synthesize `CommSemiring G`

[Yaël Dillies]

Sadly, I am only in a group G and linear_combination expects at least CommSemiring. Of course, this should not matter, since G is a Nat-module and I was only going to input Nat scalars.

[Yaël Dillies]

Would that be too much of a scope-creep to support modules in linear_combination instead of just rings?

[Mitchell Lee]

linear_combination just takes a linear combination of the equations you feed to it, yielding an equation that can be proved by just congr. Then it uses a normalization tactic (by default ring_nf) to show that the resulting equation is equivalent to the one you are trying to show. linear_combination doesn't do any simplification at all by itself. That means you can get it to prove equations about abelian groups by using abel_nf as the normalization tactic instead of ring_nf.

import Mathlib

example {G : Type} [AddCommGroup G] {a b c d : G} (h : a + b = c + d) :
    d - c + (b - a) = d - a + (d - a) := by linear_combination (norm := abel_nf) h

[Mitchell Lee]

However, there are two issues with this approach.

1. linear_combination cannot combine equations using •, only using *. For example:

import Mathlib

example {G : Type} [AddCommGroup G] {a b c d : G} (h : a = c) :
    /-
    typeclass instance problem is stuck, it is often due to metavariables
      HSMul ℕ ?m.1763 ?m.1764
    -/
    2 • a = 2 • c := by linear_combination (norm := abel_nf) 2 • h

(This can be fixed by extending linear_combination.)

2. abel_nf works great for abelian groups. But as far as I know, there is no currently no normalization tactic for general module-valued expressions. (See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Feature.20request.3A.20.22module_nf.22.)
   For example, there is no tactic that can prove an equation like this.

import Mathlib

example {R : Type} [CommRing R] {V : Type} [AddCommGroup V] [Module R V] (x : R) (v w : V) :
    (1 + x ^ 2) • (v + w) - x • (x • v - w) = v + (1 + x + x ^ 2) • w := by
  sorry

(This is not an issue with linear_combination, and there is no way that linear_combination could possibly prove this theorem unless there was a separate module_nf tactic that could already prove it by itself.)