Stream: Coq devs & plugin devs

Topic: non-reference term in "using" clauses is deprecated


view this post on Zulip Karl Palmskog (Jul 13 2024 at 20:03):

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.

view this post on Zulip Karl Palmskog (Jul 13 2024 at 20:04):

I guess you can also view this as feedback on 8.20+rc1, since the warning first appeared there.

view this post on Zulip Gaëtan Gilbert (Jul 13 2024 at 20:43):

turn it into a reference eg by doing pose

view this post on Zulip Karl Palmskog (Jul 13 2024 at 21:17):

I guess you mean like this?

 pose (lower_lower x r q) as p.
 auto using p.

view this post on Zulip Gaëtan Gilbert (Jul 13 2024 at 21:21):

yes

view this post on Zulip Karl Palmskog (Jul 14 2024 at 08:38):

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

view this post on Zulip Karl Palmskog (Jul 14 2024 at 08:39):

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?

view this post on Zulip Pierre Roux (Jul 14 2024 at 08:40):

Certainly, we have one month and a half left.

view this post on Zulip Karl Palmskog (Jul 14 2024 at 08:40):

OK, I'll put this on my TODO list then

view this post on Zulip Pierre-Marie Pédrot (Jul 14 2024 at 13:05):

IIRC the pose trick is mentioned in the changelog. (edit: in this section)

view this post on Zulip Pierre-Marie Pédrot (Jul 14 2024 at 13:07):

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

view this post on Zulip Karl Palmskog (Jul 14 2024 at 13:26):

is this a good idea in general (to add context variables to hint db)? Some projects tend to have enormous contexts

view this post on Zulip Karl Palmskog (Jul 14 2024 at 13:46):

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

view this post on Zulip Pierre-Marie Pédrot (Jul 15 2024 at 13:45):

I suggest copying the changelog info, it actually recommends pose proof without a name rather than pose

view this post on Zulip Paolo Giarrusso (Jul 29 2024 at 08:36):

: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