How to lemma polynomial equality

Stream: mathlib4

[Andrew Z]

Hi, I have a newbie question about solving goal for univariate polynomials that I know are equivalent:

the unsolved goal is: ⊢ Polynomial.C 13 * Polynomial.X = Polynomial.X * Polynomial.C 5 * 2 + Polynomial.X * Polynomial.C 3

the coeff_val lemma passes

import Mathlib.Algebra.Polynomial.Basic
import Mathlib.Algebra.Polynomial.Eval.Defs
import Mathlib.Algebra.MvPolynomial.SchwartzZippel
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Ring
import Mathlib.Data.ZMod.Basic
import Mathlib.Tactic

@[simp]
noncomputable def test_p : MvPolynomial (Fin 2) (ZMod 19) := 3 * MvPolynomial.X 0 * MvPolynomial.X 1 + 5 * MvPolynomial.X 0 + 1

@[simp]
noncomputable def point_00 : (ZMod 19) := MvPolynomial.eval ![0, 0] test_p
lemma point_00_val : point_00 = (1 : ZMod 19) := by
  simp [point_00, test_p]

@[simp]
noncomputable def point_01 : (ZMod 19) := MvPolynomial.eval ![1, 0] test_p
lemma point_01_val : point_01 = (6 : ZMod 19) := by
  simp [point_00, test_p]
  ring_nf

@[simp]
noncomputable def point_10 : (ZMod 19) := MvPolynomial.eval ![0, 1] test_p
lemma point_10_val : point_10 = (1 : ZMod 19) := by
  simp [point_10, test_p]

@[simp]
noncomputable def point_11 : (ZMod 19) := MvPolynomial.eval ![1, 1] test_p
lemma point_11_val : point_11 = (9 : ZMod 19) := by
  simp [point_11, test_p]
  ring_nf

@[simp]
noncomputable def sum_0 : (ZMod 19) := point_00 + point_10
lemma sum_0_val : sum_0 = (2 : ZMod 19) := by
  simp [point_11, test_p]
  ring_nf

@[simp]
noncomputable def sum_1 : (ZMod 19) := point_01 + point_11
lemma sum_1_val : sum_1 = (15 : ZMod 19) := by
  simp [point_11, test_p]
  ring_nf


@[simp]
noncomputable def coeff : (ZMod 19) := sum_1 - sum_0
lemma coeff_val : coeff = (13 : ZMod 19) := by
  simp [coeff, test_p]
  ring_nf


noncomputable def expected_g_0 : Polynomial (ZMod 19) :=  Polynomial.C 13 *  Polynomial.X +  Polynomial.C sum_0
noncomputable def computed_g_0 : Polynomial (ZMod 19) := Polynomial.C coeff * Polynomial.X + Polynomial.C sum_0

lemma equal_value : expected_g_0 = computed_g_0 := by
  unfold computed_g_0 expected_g_0
  simp [coeff]
  ring_nf

  -- simp [test_p, List.range, List.foldl, List.flatMap, List.map, List.range.loop, coeff]
  -- ring_nf
  -- rfl

Appreciate the support. Thanks.

[Ruben Van de Velde]

First error:

Function expected at
  ZMod
but this term has type
  ?m.1

Note: Expected a function because this term is being applied to the argument
  19

Please update your code with the relevant imports and anything else needed to make it a #mwe (click the link)

[Andrew Z]

I updated with the whole file. Thanks

[František Silváši 🦉]

Here's a step by step proof; there's about half a million ways to make this shorter of course :).

open Polynomial in
lemma equal_value : expected_g_0 = computed_g_0 := by
  unfold computed_g_0 expected_g_0
  simp [_root_.coeff]
  ring_nf
  symm
  calc X * C (5 : ZMod 19) * 2 + X * C 3
    _ = X * (C 5 * 2) + X * C 3 := by rw [mul_assoc]
    _ = X * (C 5 * 2 + C 3)     := by rw [mul_add]
    _ = X * (C 5 * C 2 + C 3)   := by rfl
    _ = X * (C (5 * 2) + C 3)   := by rw [←C_mul]
    _ = X * (C (5 * 2 + 3))     := by rw [C_add]
    _ = X * (C 13)              := rfl
    _ = C 13 * X                := by rw [mul_comm]

[Andrew Z]

Thank you @František Silváši 🦉 :smiley:

[Andrew Z]

I’m not sure if it’s reasonable to manually do this each time

[Andrew Z]

I thought ring_nf would accomplish this. Does anyone know of a tactic or way to do this without completing the proof manually?

[Kim Morrison]

open Polynomial in
lemma equal_value : expected_g_0 = computed_g_0 := by
  unfold computed_g_0 expected_g_0
  simp [_root_.coeff]
  ring_nf
  symm
  calc X * C (5 : ZMod 19) * 2 + X * C 3
    _ = X * (C (5 * 2 + 3))     := by grind [C_ofNat, C_mul, C_add]
    _ = X * (C 13)              := rfl
    _ = C 13 * X                := by grind

also works, although it is terrible and embarrassing that the rfl step is apparently necessary there!

(How to obtain this from @František Silváši 🦉's proof? Work out which lemma the first rfl is using (remember: rfl is a code smell!), then replace each rw [X] with grind or grind [X], then start combining steps.)

Presumably there are a lot of polynomial-related lemmas we need to annotate for @[grind], but I think no one has got there yet.

[Damiano Testa]

If you do not want to do a lot of manual labor, you can also prove it like this:

lemma equal_value : expected_g_0 = computed_g_0 := by
  unfold computed_g_0 expected_g_0
  congr
  aesop

[Andrew Z]

@Damiano Testa :gold: :muscle: :pray: