I found an inconsistency in the behavior of the ssr rewrite provided by Coq and the one provided by MathComp. Is this a bug, and if so is it a Coq bug or a MathComp one? I don't know in which issue tracker to report this.
Variables (p q : bool). Axiom H : p = true -> q = true. (* Regular rewrite *) Goal q = true. rewrite H. (* side-condition appears last *) Abort. From Coq Require Import ssreflect. (* ssr rewrite from Coq *) Goal q = true. rewrite H. (* side-condition appears first *) Abort. From mathcomp Require Import all_ssreflect. (* ssr rewrite from mathcomp *) Goal q = true. rewrite H. (* side-condition appears last *) Abort.
This is controlled by a flag (something like
SsrRewriteGoalOrder). I suppose that, if you only import
ssreflect, the flag does not get set and you get old behavior.
Oh, I see. So, to be clear, the old behavior is to show the side-condition first?
I am not so sure. I think this is the new behavior (or at least that is the one I would like). But for compatibility reasons, both vanilla Coq and full MathComp use the old behavior of having the side condition appear last.
From Coq Require Import ssreflect. Set SsrOldRewriteGoalsOrder. (* ssr rewrite from Coq *) Goal q = true. rewrite H. (* side-condition appears last *)
Yeah. Here is the doc for future reference.
Do you (does anyone) know whether there are plans to port MathComp to showing side-conditions first and unsetting that flag by default?
would be nice to have some tools that would make this kind of port semi-automatically
Last updated: Feb 06 2023 at 12:04 UTC