The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

Hi Abhishek,

There is already a preprocessor tactic for arithmetics : zify
zify; ring works for your goal.

Best,
--
Frédéric


On Fri, 2021-01-08 at 11:07 -0800, Abhishek Anand wrote:
> It was a bit surprising that ring couldn't solve the lemma below:
> Should it be extended to preprocess the goal as I do in the
> ringpp Ltac below?
> It seems that would strictly increase the potence of ring.
> Has someone written such more potent ring tactics and are willing to
> share? 
> 
> Require Import ZArith.
> 
> Lemma ringz (numCpu: positive): (3 * 1 * Z.pos numCpu * Z.pos (1 *
> 16))%Z = (3 * 1 * Z.pos (1 * 16 * numCpu))%Z.
> Proof.
>   Fail ring.
> Ltac ringpp :=
>   repeat rewrite Pos2Z.inj_mul;
>   repeat rewrite Pos2Z.inj_add;
>   ring.
> 
>   ringpp.
> 
> 
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/