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: Oct 13 2024 at 01:02 UTC