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!

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`

.

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`

.

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`

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`

.

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"`

).

Pierre Roux said:

(or just

`Set Printing Notations`

)

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

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