Stream: math-comp users

Topic: Mathcomp notation `{in [predC unit], _}`

view this post on Zulip Laura Brædder (Jun 23 2023 at 11:06):

Hello again. In somewhat of an extension to my last question (Problem with exports in ssralg.v), I ended up using the older version of mathcomp, i.e. the one without hierarchy builder. I'm trying to prove that we have a unit ring. According to ssralg.v, the conditions for a unit ring is that it has the following mixin where R is a ringType:

unit : pred R;
inv : R -> R;
_ : {in unit, left_inverse 1 inv *%R};
 _ : {in unit, right_inverse 1 inv *%R};
 _ : forall x y, y * x = 1 /\ x * y = 1 -> unit x;
 _ : {in [predC unit], inv =1 id}

I'm having trouble working with in [predC unit]. Is there a way to find some documentation for this notation? I've tried using both Search and About, but that didn't really give me anything useful. Is there some smart command I don't know about? Or is it a matter of asking the right way in Search or About.
Well, to be more precise, when I unfold and pick an arbitrary x as a variable, it becomes x \in [pred x | x \notin unit], which I don't think gives me more than before. So my question is, how does one find the meaning of these statements and, in particular, the notation... I hope it makes sense. Thanks!

view this post on Zulip Cyril Cohen (Jun 23 2023 at 11:13):

The doc is here it's basically a smart notation that takes a universally quantified proposition and inserts a membership to a predicate i.e. {in A, forall x, P x} is mapped to forall x, x \in A -> P x.

view this post on Zulip Cyril Cohen (Jun 23 2023 at 11:14):

Now you can simplify _ \in _ statements using the inE rewrite multi-rule, which should reduce x \in [pred x | x \notin unit] to x \notin unit.

view this post on Zulip Cyril Cohen (Jun 23 2023 at 11:17):

side note: the fact that you have unit instead of GRing.unit makes me wonder if you have imported the module GRing itself, which is not recommended, one should only import GRing.Theory, cf the header of ssralg.v

view this post on Zulip Laura Brædder (Jun 23 2023 at 11:20):

Thank you, @Cyril Cohen! I do get the right rewrite which is much easier to work with. Also, this is not my actual code. I've made my own set of units which is why I don't have GRing.unit.

view this post on Zulip Pierre Roux (Jun 23 2023 at 15:36):

About understanding what a notation is, there are two main solutions: using Set Printing All (or just Set Printing Notations) or Locate (for instance Locate "predC").

view this post on Zulip Ana de Almeida Borges (Jun 26 2023 at 00:06):

Pierre Roux said:

(or just Set Printing Notations)

For clarification, the above is a typo, it should be Unset Printing Notations

view this post on Zulip Ana de Almeida Borges (Jun 26 2023 at 00:16):

Note that there is sometimes some magic involved in using Locate for notations: some tokens need to be surrounded by spaces and others need to not be surrounded by spaces, and the way to know which is which is to already know how the notation is defined (or trial and error, or experience at predicting mathcomp defaults). For example:

From mathcomp Require Import all_ssreflect.

Locate "[seq _ | _ <- _]". (* Unknown notation *)
Locate "[seq _ | _ <- _ ]". (* Unknown notation *)
Locate "[ seq _ | _ <- _ ]". (* success! *)
Locate "[ s eq _ | _ <- _ ]". (* Unknown notation *)

(I don't think anyone would actually try the last one, but I include it to illustrate that spaces can't be added everywhere willy-nilly.)

You can also Locate for a subset of the notation as Pierre mentions, and probably should do so in cases such as this one where trying to locate the exact notation can be tricky. The disadvantage is that you need to visually find it from the list of outputs. For example, Locate "seq" with the above import generates 15 results.

I mostly use Unset Printing Notations for this purpose. It's definitely my favorite and most used of the printing flags. [Edit: ok, it might be less useful than Set Printing Coercions]

Last updated: Jul 25 2024 at 16:02 UTC