ring and scalar multiplication

Stream: metaprogramming / tactics

[Yaël Dillies]

Consider the following stupid identity involving scalar multiplication:

import Mathlib.Algebra.Module.Basic
import Mathlib.Tactic.Ring

example {𝕜 E F : Type*} [CommRing 𝕜] [CommRing E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F]
  [Module E F] [IsScalarTower 𝕜 E F] [SMulCommClass 𝕜 E F] (a b : 𝕜) (x₁ y₁ : E) (x₂ y₂ : F) :
  (a • x₁ + b • y₁) • (a • x₂ + b • y₂) =
    (a * a) • x₁ • x₂ + (b * b) • y₁ • y₂ + (a * b) • (x₁ • y₂ + y₁ • x₂) := by
  simp only [mul_add, add_smul, smul_add]
  rw [←smul_smul_smul_comm a, ←smul_smul_smul_comm b, ←smul_smul_smul_comm a b,
    ←smul_smul_smul_comm b b, smul_eq_mul, smul_eq_mul, smul_eq_mul, smul_eq_mul, mul_comm b,
    add_comm _ ((b * b) • y₁ • y₂), add_add_add_comm, add_comm ((a * b) • y₁ • x₂)]

ring fails on this, even though the corresponding multiplication identity is easily dispatched:

example {𝕜 : Type*} [CommRing 𝕜] (a b x₁ y₁ x₂ y₂ : 𝕜) :
  (a * x₁ + b * y₁) * (a * x₂ + b * y₂) =
    (a * a) * x₁ * x₂ + (b * b) * y₁ * y₂ + (a * b) * (x₁ * y₂ + y₁ * x₂) := by ring

[Yaël Dillies]

This type of goals naturally shows up when one generalises results from rings to modules, see eg #7650.

[Yaël Dillies]

Two questions:

1. Should this be part of ring?
2. Should there be yet another tactic specialised in this specific kind of goals?

[Yaël Dillies]

(note I can't reuse ring by putting everything in a single type because I don't have Algebra instances lying around)

[Anne Baanen]

The ring tactic framework is powerful enough to accomodate smul, although implementing it would be a very large refactor.