## Stream: math-comp users

### Topic: ✔ How to use x - x = 0 in a ring ?

#### Julien Puydt (May 16 2022 at 22:14):

I'm pretty sure I'm missing something, because simplifying x -x to 0 in some expression shouldn't need this lemma:

``````From mathcomp Require Import all_ssreflect all_algebra.

Open Scope ring_scope.

Lemma xminusx: forall A: ringType, forall x: A, x - x = 0.
Proof.
move=> A x.
apply/eqP.
by rewrite GRing.subr_eq0.
Qed.
``````

#### Julien Puydt (May 16 2022 at 22:21):

Notice that the following is simpler, but a bit unsatisfying because I still don't know how to get x-x rewritten to 0 in either an hypothesis or the current goal without this lemma:

``````From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp.algebra_tactics Require Import ring.

Open Scope ring_scope.

Lemma xminusx: forall A: comRingType, forall x: A, x - x = 0.
Proof.
move=> A x.
by ring.
Qed.
``````

#### Ana de Almeida Borges (May 16 2022 at 22:58):

I think you're looking for `GRing.addrN`

#### Ana de Almeida Borges (May 16 2022 at 23:04):

I'm not familiar with the ring library, so here is the algorithm I followed to reach this conclusion:

1. I know from experience with MathComp that often these kinds of lemmas are hard to find with naive searches because they are defined using keywords
2. I tried to find the name of the operation whose notation is `_ - _`
1.1 I first tried `subr` and `GRing.subr` because it sounded right
1.2. When that didn't work I fell back to `Locate "_ - _"`, which told me it's `GRing.add` together with `GRing.opp`

3. I did `Search GRing.add 0`

4. One of the first hits was
``````GRing.addrN: forall [V : zmodType], right_inverse 0 -%R +%R
``````

This seemed promising, so I tested it and it worked.

#### Ana de Almeida Borges (May 16 2022 at 23:06):

Apparently `GRing.subrr` is exactly the same statement with a more intuitive name (why are there two of them?)

#### Julien Puydt (May 17 2022 at 05:03):

Wonderful ; indeed I didn't find those because I tried to search in the direction of "opp"/"oppr"... thanks!

#### Notification Bot (May 17 2022 at 05:03):

Julien Puydt has marked this topic as resolved.

Last updated: Jul 15 2024 at 21:02 UTC