Showing polynomial equality in coq/ssreflect

I am trying to prove equality of polynomials by explicit computation in coq. Here's an example showing where I get stuck:

From mathcomp Require Import all_ssreflect all_algebra.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import GRing.Theory.
Local Open Scope ring_scope.

Variable F : fieldType.
Variable w : F.

Definition test1 (k : nat) := w%:P*w%:P*'X^k + w%:P.

Definition test2 (k : nat) := w%:P*'X^k + 1%:P.

Lemma foo: w%:P* (test2 2) = (test1 2).
Proof.
unfold test2. unfold test1.

The first step must involve actually "performing the multiplication" but I couldn't quite see how to do that. I suppose next that showing two polynomials are equal requires showing that they are equal term-by-term, but I could not find an existing lemma encapsulating that.

I would also love to be able to know how to define the polynomial X^k + 1; writing

Definition test3 (k : nat) := 'X^k + 1%:P.

did not work.

More generally, if anyone can point to reasonable documentation, tutorials, etc. to doing algebra using ssreflect I would be grateful. (I'm not sure such things exist, unfortunately.)

Here is the solution to you small problem.

From mathcomp Require Import all_ssreflect all_algebra.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import GRing.Theory.
Local Open Scope ring_scope.

Variable F : fieldType.
Variable w : F.

Definition test1 (k : nat) := w%:P*w%:P*'X^k + w%:P.

Definition test2 (k : nat) := w%:P*'X^k + 1%:P.

Lemma foo: w%:P* (test2 2) = (test1 2).
Proof.
rewrite /test1/test2.
by rewrite mulrDr mulr1 mulrA.
Qed.

The solution of this problem only relies on ring theorems: distributivity of multiplication over addition, 1 being a neutral element for multiplication, and associativity of multiplication.

A seasoned user will know that mulrDr is to be used here for the following reason:

• the pattern we want to work on has the following shape _ * (_ + _)
• multiplication will be noted mul in the theorem name,
• we know we are only using ring properties of multiplication and addition this brings the first occurence of r
• the second important part of the pattern is addition, this brings the D in the theorem name
• the additions is on the right of the multiplication, this brings the last r in the theorem name.

Similarly, there exists a mulrDl theorem in the library, whose statement is easy to guess from the name.

The same reasoning makes that I know to use mulr1 (multiplication of an arbitrary ring element r by 1 --- here there is no added suffix after 1, multiplication of 1 by r would be written mul1r).

Here, there is a little more knowledge that is used. You use 1%:P to denote the constant polynomial of value 1, where the 1 we are talking about is actually the neutral element for multiplication in ring F. You could have used 1, this would have meant the neutral element in ring {poly F}. It turns out the two are convertible, so that mulr1 can actually be used.

For mulrA : multiplication in a ring, associativity.

The name of theorems follows a philosophy that is explained in the header comments of files

https://github.com/coq/coq/blob/master/theories/ssr/ssrbool.v

https://math-comp.github.io/htmldoc_2_2_0/mathcomp.algebra.ssralg.html

(you can replace htmldoc_2_2_0 by according to the latest distribution of mathematical components).

Reading all the header comments of all files that you are depending on in mathematical components will probably be useful. You should also have a look at the book

https://math-comp.github.io/mcb/

Of course, this is a lot of documentation and it may feel overwhelming, but the size of the library makes that we cannot document everything in much more detail. In the end, one may need to read some of the files completely in order to understand the treasures that are stored there. For instance, the bigop file contains a complete treatment of iterated operators that deserves a lot of attention. It is hard to discover how to use these theorems without knowing that they exist at all.

Now, let's study why you test3 definition fail. When I run your command, I get the following message:

Error:
The following term contains unresolved implicit arguments:
  (fun k : nat => 'X^k + 1%:P)
More precisely: 
- ?t: Cannot infer an internal placeholder of type 
  "ringType" in environment:
  k : nat

This means that the notation X^k + 1%:P does not bring any information about the type of polynomials that we are creating here. The notation X^k denotes the the monomial x^k in any polynomial ring, and 1%:P denotes the constant monomial with coefficient 1 in any ring, but any ring must have a 1, so that does not give any information. Here, I assume you want to work with polynomials whose coefficients are in F, so you have to make this precise. Here is a command that works:

Definition test3 (k : nat) : {poly F} := 'X^k + 1%:P.