Stream: math-comp users

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


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ana de Almeida Borges (May 16 2022 at 22:58):

I think you're looking for GRing.addrN

view this post on Zulip 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.

view this post on Zulip 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?)


Last updated: Feb 08 2023 at 04:04 UTC