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: Oct 13 2024 at 01:02 UTC