Stream: math-comp users

Topic: Using auto with mathcomp


view this post on Zulip Jim Portegies (Apr 06 2023 at 10:16):

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.

view this post on Zulip Paolo Giarrusso (Apr 06 2023 at 11:05):

Definition foo := @GRing.addrC R. Local Hint Resolve foo : wp_algebra. should work without the warning, right? (EDIT: Yes indeed)

view this post on Zulip Paolo Giarrusso (Apr 06 2023 at 11:07):

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

view this post on Zulip Paolo Giarrusso (Apr 06 2023 at 11:10):

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].

view this post on Zulip Laurent Théry (Apr 06 2023 at 11:13):

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.

view this post on Zulip Laurent Théry (Apr 06 2023 at 11:20):

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

view this post on Zulip Jim Portegies (Apr 06 2023 at 12:36):

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.

view this post on Zulip Jim Portegies (Apr 06 2023 at 12:38):

(Indeed I am aware of the ring tactic).

view this post on Zulip Laurent Théry (Apr 06 2023 at 13:53):

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.

view this post on Zulip Laurent Théry (Apr 06 2023 at 14:12):

seems a proper way to do that is

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

view this post on Zulip Paolo Giarrusso (Apr 06 2023 at 17:44):

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

view this post on Zulip Paolo Giarrusso (Apr 06 2023 at 17:46):

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

view this post on Zulip Paolo Giarrusso (Apr 06 2023 at 17:47):

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

view this post on Zulip Patrick Nicodemus (Apr 07 2023 at 00:19):

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