Stream: math-comp users

Topic: Polynomials


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Julien Puydt (May 20 2022 at 13:03):

Last remaining issue: polynomial evaluation getting stuck.


Last updated: Feb 08 2023 at 08:02 UTC