Polynomial computations

Stream: Is there code for X?

[Nirvana Coppola]

Hi all! I was wondering if there is a smart way to prove two polynomials (in X, over the reals) are equal. For example, as of now the shortest prove I have that (X^2+c)^2 is what you expect is attached, and I'm struggling to believe something similar to ring_nf doesn't work. But ring_nf doesn't work. Am I missing something? :)

example : (X + C c)^2 = X^2 + C (2 * c) * X + C (c^2) := by
    ring_nf
    simp
    rw [mul_comm (C c) X, mul_assoc]
    simp
    left
    rfl

[Michael Stoll]

Can you read #mwe ? You are missing imports and variables.
The problem is that C 2 and 2 are treated as different by ring. The following works.

import Mathlib

open Polynomial

variable {R} [CommRing R] (c : R)

example : (X + C c)^2 = X^2 + C (2 * c) * X + C (c^2) := by
  simp only [map_mul, map_pow, show C (2 : R) = 2 from rfl]
  ring

[Nirvana Coppola]

Sorry about the missing parts! D: Thanks for the insight

[Damiano Testa]

If you want a version that works for a Semiring, you can do it as follows:

import Mathlib

open Polynomial

variable {R} [Semiring R] {c : R}

example : (X + C c)^2 = X^2 + C (2 * c) * X + C (c^2) := by
  rw [ext_iff_degree_le (n := 2) (by compute_degree!) (by compute_degree!)]
  intro n hn
  interval_cases n <;>
    simp [sq, mul_add, add_mul, two_mul]

[Eric Wieser]

Or without resorting to cases

example {R} [Semiring R] {c : R} : (X + C c)^2 = X^2 + C (2 * c) * X + C (c^2) := by
  simp only [sq, map_mul, map_ofNat]
  noncomm_ring
  rw [commute_X (C c)]
  abel

[Nirvana Coppola]

Thanks everyone!