Stream: math-comp users

Topic: Failing with hornerE


view this post on Zulip Julien Puydt (Aug 10 2022 at 10:09):

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.

view this post on Zulip Cyril Cohen (Sep 08 2022 at 13:51):

Please bugreport it.

view this post on Zulip Julien Puydt (Sep 08 2022 at 14:10):

Done!

view this post on Zulip Julien Puydt (Sep 08 2022 at 14:16):

Ah, wrong project indeed... thanks!


Last updated: Jan 29 2023 at 19:02 UTC