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.
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.
I think you're looking for GRing.addrN
I'm not familiar with the ring library, so here is the algorithm I followed to reach this conclusion:
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
I did Search GRing.add 0
GRing.addrN: forall [V : zmodType], right_inverse 0 -%R +%R
This seemed promising, so I tested it and it worked.
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