Ana de Almeida Borges (Mar 01 2022 at 12:42): Ana de Almeida Borges (Mar 01 2022 at 12:42):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.
Ana de Almeida Borges (Mar 01 2022 at 12:49):Oh, I see. So, to be clear, the old behavior is to show the side-condition first?
Guillaume Melquiond (Mar 01 2022 at 12:50):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.
Guillaume Melquiond (Mar 01 2022 at 12:52):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.
Ana de Almeida Borges (Mar 01 2022 at 12:55):Do you (does anyone) know whether there are plans to port MathComp to showing side-conditions first and unsetting that flag by default?
Laurent Théry (Mar 01 2022 at 13:02):would be nice to have some tools that would make this kind of port semi-automatically
Last updated: Oct 13 2024 at 01:02 UTC