Ssreflect Users Discussion List

[Ralf Jung <>]

Hi all,

We are formalizing a shallow embedding of a logic in Coq, and we are
using scopes such that we can use the same notation for logic-level and
Coq-level assertions. However, unfortunately, this does not work well
with the ssreflect rewrite patterns: If, for example, "_ ★ _" is
registered as notation in a scope delimited by M, I have to write

  rewrite [(a ★ _)%M]lemma.

These additional parenthesis get very tedious. Is there any alternative
available? Or, if not, is there any chance that a syntax like

  rewrite [a ★ _]lemma%M.

could be supported?

I attached a simple file demonstrating the issue.

Kind regards,
Ralf
Require Import mathcomp.ssreflect.ssreflect Setoid.

Delimit Scope my_scope with M.
Notation "a ★ b" := (a /\ b) (at level 40) : my_scope.

Lemma sep_comm a b : (a ★ b <-> b ★ a)%M.
Proof. tauto. Qed.

Goal forall a b, (a ★ b <-> b ★ a)%M.
Proof.
  move=>a ?.
  (* Need nested parentheses to give a rewrite pattern. *)
  rewrite [(a ★ _)%M]sep_comm.