Stream: Coq users

Topic: Order of side conditions for ssr rewrite


view this post on Zulip 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.

view this post on Zulip Guillaume Melquiond (Mar 01 2022 at 12:45):

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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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 *)

view this post on Zulip Ana de Almeida Borges (Mar 01 2022 at 12:53):

Yeah. Here is the doc for future reference.

view this post on Zulip 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?

view this post on Zulip 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: Mar 29 2024 at 12:02 UTC