## Stream: math-comp users

### Topic: Polynomials

#### Julien Puydt (May 18 2022 at 19:50):

I'm now digging my way into polynomials, and again I'm finding things a bit unwieldy:

``````From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp.algebra_tactics Require Import ring.

(* those need explanations: in MC book? *)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Open Scope ring_scope.

Section First.

Check 'X.
Fail Check 2*'X.
Fail Check 2%:Q * 'X.
Check 2%:Q *: 'X. (* not in a ring but only a module *)

Definition QX := { poly rat_Ring }.
Check 2%:Q *: 'X : QX. (* force being in a ring *)

Check 2%:Q *: 'X + 1 :QX.
Check (2%:Q *: 'X - 1)^2 : QX.
Check ('X+1) * (2%:Q *: 'X -1)^2 : QX.

End First.

Section Second.

(* below: no :QX gives an error because the ring can't be guessed *)
Lemma trivial: ('X+1) * ('X - 1) = ('X^2 -1 :QX).
Proof.
by ring.
Qed.

End Second.

Section Third.

(* ugly *)
Definition P := 'X^2 - 3%:Q *: 'X + 2%:Q *: 'X^0 : QX.

(* Compute P.[1]. ISSUE: gets stuck! *)

Lemma easy: P = ('X-1) * ('X - 2%:Q *: 'X^0).
Proof.
unfold P. (* QUESTION: why do my %:Q's turn into %:~R ? *)
by ring. (* ISSUE: Tactic failure: Not a valid ring equation *)
Qed.

End Third.
``````

#### Pierre Roux (May 18 2022 at 20:39):

Julien Puydt said:

``````Lemma trivial: ('X+1) * ('X - 1) = ('X^2 -1 :QX).
``````

I'd rather write

``````Lemma trivial : ('X + 1) * ('X - 1) = 'X^2 - 1 :> QX.
``````

Julien Puydt said:

``````unfold P. (* QUESTION: why do my %:Q's turn into %:~R ? *)
``````

If you look at

``````Locate "%:Q".
``````

you'll see that the notation `n%:Q` stands for `intmul (GRing.one _) (n : int) : rat`, that is `(n : int)%:~R : rat`

#### Julien Puydt (May 20 2022 at 11:50):

Ok, I managed to get on getting factorization results ; for future reference if someone else gets stuck:

``````Section Third.

Definition P := 'X^2 - 3%:R * 'X + 2%:R * 'X^0 : QX.

(* Compute P.[1]. ISSUE: gets stuck! *)

Lemma easy: P = ('X-1) * ('X - 2%:R * 'X^0).
Proof.
unfold P.
by ring.
Qed.

End Third.
``````

The idea -- as far as I understand -- is that if I convert 2 and 3 to rationals, I have to use *: , and that means I'm not in a ring anymore. If I declare them as ring elements, then I can use * -- and the final : QX ensures the ring is the one I want to work within.

Still working on the rest.

#### Julien Puydt (May 20 2022 at 12:01):

Eh, as far as I understand doesn't seem to be that much: with the example I'm really interested in, ring still isn't happy:

``````Section Serious.

Definition P1 := ('X + 1) * (2%:R * 'X - 1)^2 :QX.
Check P1.
Definition P2 := (4%:R * 'X^3 - 3%:R * 'X + 1) : QX.
Check P2.

Lemma factorisation: P1 = P2.
Proof.
unfold P1.
unfold P2.
by ring.
Qed.
End Serious.
``````

#### Julien Puydt (May 20 2022 at 12:57):

The problem is the power two on a polynomial!

Here is the working proof:

``````Section Serious.

Definition P1 := ('X + 1) * (2%:R * 'X - 1) ^+ 2 : QX.
Check P1.
Definition P2 := (4%:R * 'X^3 - 3%:R * 'X + 1) : QX.
Check P2.

Lemma factorisation: P1 = P2.
Proof.
unfold P1.
unfold P2.
by ring.
Qed.

End Serious.
``````

#### Julien Puydt (May 20 2022 at 13:03):

Last remaining issue: polynomial evaluation getting stuck.

Last updated: Jul 25 2024 at 16:02 UTC