Hi all,

I'm trying to understand if one can use auto (or similar tactics) efficiently with the mathcomp library. Below I try to give an example to illustrate my question. Adding the Hint `(@GRing.addrC R)`

works, but gives a warning, and seems to specific because the hint now depends on the particular ringType R. Ideally I would add (GRing.addrC) as a hint but that also gives a warning and it doesn't work, as in it doesn't solve the goal. What would be your recommendation here?

Best,

Jim

```
From mathcomp Require Import ssralg.
Variable R : ringType.
Open Scope ring_scope.
Lemma comm_with_zero :
forall a : R,
0 + a = a + 0.
Proof.
intro a.
(** auto fails to make progress here. *)
assert_fails progress auto using (GRing.addrC).
assert_fails progress auto using (@GRing.addrC _).
(** auto makes progress when using @GRing.addrC R *)
assert_succeeds solve [auto using (@GRing.addrC R)].
(** Following gives a warning *)
Local Hint Resolve (GRing.addrC) : wp_algebra.
(** This does solve the goal *)
assert_fails progress auto with wp_algebra.
(** Adding @GRing.addrC R to the database works,
although gives a warning, but
this seems too specific for a hint. *)
Local Hint Resolve (@GRing.addrC R) : wp_algebra.
assert_succeeds solve [auto with wp_algebra].
(** This also solves the goal *)
simple apply GRing.addrC.
Qed.
```

`Definition foo := @GRing.addrC R. Local Hint Resolve foo : wp_algebra.`

should work without the warning, right? (EDIT: Yes indeed)

the warning in `Local Hint Resolve (GRing.addrC) : wp_algebra.`

is just because hints aren't supposed to be arbitrary terms, just names, so `Local Hint Resolve GRing.addrC : wp_algebra.`

avoids it

alternatively, this works, but it'll be tried too often because it doesn't have a syntactic pattern:

```
Local Hint Extern 1 => simple apply GRing.addrC : wp_algebra.
assert_succeeds solve [eauto with wp_algebra].
```

I wonder if it is not the way `Hint`

decides on which constant to add the Hint. This works

```
Definition myaddrC (V : zmodType) (a b : V) := GRing.addrC a b.
Hint Immediate myaddrC.
Lemma comm_with_zero :
forall (R : ringType) (a : R),
0 + a = a + 0.
Proof.
move=> *.
auto.
Qed.
```

```
```

anyway, @Jim Portegies are you aware that tactics like `ring`

are available thanks to `algebra tactics`

? But I guess you need to have a `comRingType`

Thanks! The solution by @Laurent Théry in principle works well, but there is still something puzzling me. It seems that by adding `myaddrC`

in that way, the definition in GRing.addrC gets unfolded in such a way that the auto procedure can pattern match. But without unfolding, the auto procedure seems to miss that it can use it.

```
From mathcomp Require Import ssralg.
Variable R : ringType.
Open Scope ring_scope.
Definition my_addrC_v0 {V : zmodType} := @GRing.addrC V.
Definition my_addrC_v1 {V : zmodType} (a b : V):= @GRing.addrC V a b.
Check my_addrC_v0.
Check my_addrC_v1.
Lemma comm_with_zero_again :
forall a : R,
0 + a = a + 0.
Proof.
assert_fails progress debug auto using my_addrC_v0.
debug auto using my_addrC_v1.
Qed.
```

(Indeed I am aware of the ring tactic).

It seems it is attached to the constant `commutative`

.

```
Check GRing.addrC.
Hint Immediate GRing.addrC.
Goal forall (R: ringType), commutative (+%R : R -> R -> R).
move=> R.
auto.
Qed.
```

my definition of `myaddrC`

just unfolds the constant `commutative`

to expose the constant `eq`

.

seems a proper way to do that is

```
Hint Extern 0 (_ = _) => simple apply GRing.addrC.
```

That's indeed a general problem with (e)auto: it only uses syntactic patterns to check whether a hint could apply to a goal.

The engine from typeclasses eauto is much more flexible (but doesn't use evarconv, sadly, which makes it very buggy on math-comp code)

With eauto, as a beginner I've often ended up with proofs where lots of unfoldings must be done explicitly, while eauto hides the actual proof steps; explicit apply calls can be more readable than that

Paolo Giarrusso said:

The engine from typeclasses eauto is much more flexible (but doesn't use evarconv, sadly, which makes it very buggy on math-comp code)

Can you give more detail on what you mean by 'more flexible?' Like, what would you imagine a better eauto would do

Last updated: Jul 15 2024 at 20:02 UTC