I saw the following warning in 8.20+rc1. Fine by me if it's deprecated, but what is the recommended replacement? The warning says nothing about that.
Warning: Use of the non-reference term lower_lower x r q in "using" clauses is deprecated [non-reference-hint-using,deprecated,default]
Example extracted from real code:
Require Import QArith QOrderedType.
Require Import Morphisms SetoidClass.
Structure R := {
lower : Q -> Prop;
upper : Q -> Prop;
lower_proper : Proper (Qeq ==> iff) lower;
lower_lower : forall q r, q < r -> lower r -> lower q;
disjoint : forall q, ~ (lower q /\ upper q);
}.
Lemma lower_below_upper (x : R) (q r : Q) : lower x q -> upper x r -> (q < r)%Q.
Proof.
intros Lq Ur.
destruct (Q_dec q r) as [[E1 | E2] | E3].
- assumption.
- exfalso. apply (disjoint x r).
auto using (lower_lower x r q).
(* Warning: Use of the non-reference term lower_lower x r q in "using" clauses is deprecated *)
Abort.
I guess you can also view this as feedback on 8.20+rc1, since the warning first appeared there.
turn it into a reference eg by doing pose
I guess you mean like this?
pose (lower_lower x r q) as p.
auto using p.
yes
for the record, I don't think regular Coq users have the slightest idea of the difference between regular terms and references, and from a cursory search it's not described in the refman
so if we do a PR to augment the deprecation warning with the pose suggestion, would that have any chance of making it into 8.20.0?
Certainly, we have one month and a half left.
OK, I'll put this on my TODO list then
IIRC the pose
trick is mentioned in the changelog. (edit: in this section)
note that you don't have to use the using clause anymore if you use pose, as the context variables are automatically added to the local hint db
is this a good idea in general (to add context variables to hint db)? Some projects tend to have enormous contexts
but it would be easy to just say in the warning message to use pose (<term>); auto
, since no name for the posed term is required
I suggest copying the changelog info, it actually recommends pose proof without a name rather than pose
:eyes: hm, it would be more accurate to clear the new term after auto — for the goals that aren't discharged. Also, the changelog suggests this trick for a slightly different change:
syntactic global references passed through the using clauses of auto-like tactics are now handled as plain references rather than interpreted terms. In particular, their typeclass arguments will not be inferred. In general, the previous behaviour can be emulated by replacing auto using foo with pose proof foo; auto (#18909, by Pierre-Marie Pédrot).
rather than here:
deprecated: non-reference hints in using clauses of auto-like tactics (#19006, by Pierre-Marie Pédrot).
Last updated: Oct 13 2024 at 01:02 UTC