I want to use the familiar notation of arithmetic operations on integers in ssreflect (ssrint). I have succeeded (I don't know how to do it better) in using the notation for subtraction by opening distn_scope
as follows:
From mathcomp Require Import all_ssreflect ssrint.
Open Scope distn_scope.
Parameter x y : int.
Check x - y : int.
However, I have not been able to use the notation for addition or unary subtraction (minus operation). More specifically, I would like the following Check
command to work after the above script.
Check oppzD : - (x + y) = -x + -y.
To solve this problem, what libraries should be loaded (and which scopes should be opened)?
In addition, I would be very happy if you could tell me how to search the manual (or use some commands) to solve this kind of situations.
int
uses the generic notations for algebra defined in ring_scope
and declared in ssralg
.
Regarding finding this kind of things on your own, I only have a hackish solution, hopefully others will know better. You can Check
something that uses the objects you want (Check oppzD.
in your case is perfect). With oppzD
here, you would see things like ssralg.GRing.opp
and ssralg.GRing.add
, which tells you to look at ssralg
. If you had ssralg
imported, you would see things like -%R
and (_ + _)%R
. To look further into it, you can use Set Printing All
and Check
a notation, e.g. Check (_ + _)%R.
This would make GRing.add
appear, which you can then Locate
. Then, the end of the header documentation of ssralg
would tell you about ring_scope
.