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.
```

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`

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.

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.
```

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.
```

Last remaining issue: polynomial evaluation getting stuck.

Last updated: Jul 25 2024 at 16:02 UTC