## Stream: Coq users

### Topic: ring tactic in mathcomp

#### Côme Neyrand (Jun 26 2020 at 09:32):

Hello, I am trying to prove a lemma with the ring tactic, it works with QArith but not when R is of type RealDomainType.
Here's my code :

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

Import GRing.Theory Num.Theory.

Open Scope ring_scope.

Section det.

Variable R : realDomainType.

Definition det3x3 (a1 a2 a3
b1 b2 b3
c1 c2 c3 : R) :=
a1 * b2 * c3 + a2 * b3 * c1 + a3 * b1 * c2 -
a1 * b3 * c2 - a3 * b2 * c1 - a2 * b1 * c3.

Definition x_ (A : R * R) := let (a_x, _) := A in a_x.

Definition y_ (A : R * R) := let (_, a_y) := A in a_y.

Definition pt_norm (A : R * R) :=
(x_ A) * (x_ A) + (y_ A) * (y_ A).

Definition tr_area (A B C : R * R) :=
det3x3 (x_ A) (y_ A) 1
(x_ B) (y_ B) 1
(x_ C) (y_ C) 1.

Definition dist (A B C D : R * R) :=
(pt_norm A) * (tr_area B C D) - (pt_norm B) * (tr_area A C D) +
(pt_norm C) * (tr_area A B D) - (pt_norm D) * (tr_area A B C).

Lemma power_diff (A B C D E : R * R) :
tr_area A D B * dist A B C E - tr_area A B C * dist A D B E =
tr_area A E B * dist A B C D.
Proof.
move: A B C D E.
move => [a_x a_y][b_x b_y][c_x c_y][d_x d_y][e_x e_y].
rewrite /dist /pt_norm /tr_area /det3x3 /x_ /y_.
ring.
Qed.

End det.
``````

Do you have any solutions ? thanks.

#### Kazuhiko Sakaguchi (Jul 01 2020 at 06:02):

@Côme Neyrand The same question sometimes comes up. Some workarounds can be found here: https://github.com/math-comp/math-comp/issues/401 https://github.com/coq/coq/issues/11998

#### Côme Neyrand (Jul 01 2020 at 08:00):

Thank you

Last updated: Jun 18 2024 at 09:02 UTC