I thought !hornerE would just do the trick, but it didn't and I'm wondering if it's me thinking wrong or a bug to report:
From mathcomp Require Import all_ssreflect all_algebra ssralg ssrint ssrnum.
From mathcomp.analysis Require Import reals.
From mathcomp.algebra_tactics Require Import ring.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory.
Local Open Scope ring_scope.
Import GRing.
Section BadHornerE.
Variable RR: realType.
Definition RX := { poly RR }.
Definition Psum := (4 *: 'X^3 - 3 *: 'X + 1) : RX.
Variable a: RR.
Lemma nameless: Psum.[a] == 4 * a^+ 3 - 3 * a + 1.
Proof.
(* rewrite !hornerE. should be enough, I think, but gives an awful result *)
by rewrite !hornerD hornerN !hornerZ horner_exp hornerX hornerC.
Qed.
End BadHornerE.
Please bugreport it.
Done!
Ah, wrong project indeed... thanks!
Julien Puydt has marked this topic as resolved.
Last updated: Nov 29 2023 at 17:01 UTC