ring mysteriously fails or succeeds on convertible goals

[andrew-appel]

In this example, we see that the ring tactic fails or succeeds on terms that are equivalence modulo change, and in fact the original term comes up naturally in one of my proofs. Is this a bug or a feature?

From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice.
From mathcomp Require Import fintype finfun bigop finset fingroup perm order.
From mathcomp Require Import div prime binomial ssralg countalg finalg zmodp matrix.
From mathcomp Require Import ssrnum reals interval classical_sets topology normedtype.
Require Import mathcomp.algebra_tactics.ring.
Open Scope ring_scope.

Lemma test: forall (F : realType)
 (n : nat)
 (c y : 'cV[F]_n.+1)
 (z : 'cV[F]_1),
@eq (Real.sort F)
  (@GRing.add
     (GRing_SemiRing__to__GRing_Nmodule (reals_Real__to__GRing_SemiRing F))
     (@fun_of_matrix (Real.sort F) 1 1
        (@mulmx (reals_Real__to__GRing_SemiRing F) 1 1 1
           (@mulmx (reals_Real__to__GRing_SemiRing F) 1 
              (S n) 1 (@trmx (Real.sort F) (S n) 1 y) c) z)
        (@GRing.zero (fintype_ordinal__canonical__GRing_Nmodule 0))
        (@GRing.zero (fintype_ordinal__canonical__GRing_Nmodule 0)))
     (@fun_of_matrix (Real.sort F) 1 1
        (@mulmx (reals_Real__to__GRing_SemiRing F) 1
           (GRing.one Datatypes_nat__canonical__GRing_SemiRing) 1
           (@mulmx (reals_Real__to__GRing_SemiRing F) 1 
              (S n) (GRing.one Datatypes_nat__canonical__GRing_SemiRing)
              (@trmx (Real.sort F) (S n) 1 y) c) z)
        (@GRing.zero (fintype_ordinal__canonical__GRing_Nmodule 0))
        (@GRing.zero (fintype_ordinal__canonical__GRing_Nmodule 0))))
  (@GRing.mul (reals_Real__to__GRing_SemiRing F) 2
     (@fun_of_matrix (Real.sort F) 1 1
        (@mulmx (reals_Real__to__GRing_SemiRing F) 1 1 1
           (@mulmx (reals_Real__to__GRing_SemiRing F) 1 
              (S n) 1 (@trmx (Real.sort F) (S n) 1 y) c) z)
        (@GRing.zero (fintype_ordinal__canonical__GRing_Nmodule 0))
        (@GRing.zero (fintype_ordinal__canonical__GRing_Nmodule 0)))).
Proof.
move => F n c y z.
Fail ring.
Succeed change (GRing.one Datatypes_nat__canonical__GRing_SemiRing) with (S O); ring.
Succeed set (a := fun_of_matrix _ 0 0); ring. 

And here is the detailed version information:

coq                          8.19.1         The Coq Proof Assistant
coq-mathcomp-algebra         2.2.0          Mathematical Components Library on Algebra
coq-mathcomp-algebra-tactics 1.2.3          Ring, field, lra, nra, and psatz tactics for Mathematical Components
coq-mathcomp-analysis        1.2.0          An analysis library for mathematical components
coq-mathcomp-bigenough       1.0.1          A small library to do epsilon - N reasoning
coq-mathcomp-classical       1.2.0          A library for classical logic for mathematical components
coq-mathcomp-field           2.2.0          Mathematical Components Library on Fields
coq-mathcomp-fingroup        2.2.0          Mathematical Components Library on finite groups
coq-mathcomp-finmap          2.1.0          Finite sets, finite maps, finitely supported functions
coq-mathcomp-solvable        2.2.0          Mathematical Components Library on finite groups (II)
coq-mathcomp-ssreflect       2.2.0          Small Scale Reflection
coq-mathcomp-zify            1.5.0+2.0+8.16 Micromega tactics for Mathematical Components

[pi8027]

Duplicate of #18

I'm not going to fix it very soon. I suggest using the set tactic as a workaround.

[gares]

This bug is also related to a (Coq) feature we recently discussed with @CohenCyril and @Tragicus, that would eagerly simplify (GRing.one Datatypes_nat__canonical__GRing_SemiRing) to (S O) at goal "creation time". With that in place, ring would work as expected.

[pi8027]

@gares I think GRing.one Datatypes_nat__canonical__GRing_SemiRing should not be simplified to S O automatically. This issue has to be eventually fixed in Algebra Tactics.