Stream: Coq devs & plugin devs

Topic: Changes to simpl in 8.18?


view this post on Zulip Karl Palmskog (Jul 09 2023 at 15:59):

I was able to make a failing file work in 8.18 and master, that works fine before in 8.17, with the following diff:

diff --git a/theories/StrictKleeneAlgebra.v b/theories/StrictKleeneAlgebra.v
index 9f307d8..091e76b 100644
--- a/theories/StrictKleeneAlgebra.v
+++ b/theories/StrictKleeneAlgebra.v
@@ -168,10 +168,10 @@ Section F.
     constructor; eauto with typeclass_instances.
      intros A [a|]; simpl; constructor; try reflexivity.
       apply star_make_left.
-     intros A B [a|] [c|] Hac; simpl in *; try constructor.
+     intros A B [a|] [c|] Hac; unfold Classes.leq in *; simpl in *; try constructor.
       apply star_destruct_left. inversion_clear Hac. assumption.
       rewrite dot_neutral_left. apply plus_idem.
-     intros A B [a|] [c|] Hac; simpl in *; try constructor.
+     intros A B [a|] [c|] Hac; unfold Classes.leq in *; simpl in *; try constructor.
       apply star_destruct_right. inversion_clear Hac. assumption.
       rewrite dot_neutral_right. apply plus_idem.
   Qed.

Did something change related to simpl/cbn (possibly w.r.t. typeclasses) in 8.18? I tried reading the changelog, but didn't see anything obvious. The reason this diff is needed is kind of mystifying. (Corresponding project PR).

view this post on Zulip Paolo Giarrusso (Jul 09 2023 at 19:15):

There's _one_ bugfix that will require more unfoldings:

Fixed: The simpl tactic now respects the simpl never flag even when the subject function is referred to through another definition. (#13448, fixes #13428, by Yves Bertot).

view this post on Zulip Karl Palmskog (Jul 09 2023 at 19:20):

ah, that looks quite plausible, so we might have depended on a bug (hardly first time)

view this post on Zulip Paolo Giarrusso (Jul 09 2023 at 19:31):

I don't understand _how exactly_ the proof is affected, but in 8.17 unfolding Classes.leq reveals equal which _is_ marked as simpl never

view this post on Zulip Paolo Giarrusso (Jul 09 2023 at 19:33):

so the behavior is relevant, tho I don't have an actual explanation

view this post on Zulip Gaëtan Gilbert (Jul 09 2023 at 19:34):

that does look like the bug that got fixed:

Arguments plus : simpl never.
Definition plus' := plus.

Lemma test2 P : P (plus' 1 2).
Proof.
simpl.
(* 8.17: |- P 3
8.18: |- P (plus' 1 2) *)

view this post on Zulip Paolo Giarrusso (Jul 09 2023 at 19:42):

indeed — but with unfold plus' you'll just get simpl never behavior in both versions, so it's not obvious why that'd fix the proof

view this post on Zulip Karl Palmskog (Jul 09 2023 at 19:45):

maybe due to typeclass indirection (local vs. non-local leq)

view this post on Zulip Karl Palmskog (Jul 09 2023 at 19:46):

anyway, I can see more people being bitten by this bugfix, maybe it should be flagged up more prominently, e.g.,

if simpl no longer reduces something, this may be due to an indirect simpl never exposed by #13448

view this post on Zulip Karl Palmskog (Jul 09 2023 at 20:05):

ah, it looks like this was in the end due to a "rogue" simpl never on a typeclass field that was meant to be local (https://github.com/coq-community/atbr/pull/39)

view this post on Zulip Karl Palmskog (Jul 09 2023 at 20:07):

typeclass management is a black art, episode 700

view this post on Zulip Paolo Giarrusso (Jul 09 2023 at 21:26):

Blaming this on TCs and not records seems a bit unfair, especially when fair complaints are plentiful (default hint modes, I'm looking at you)

view this post on Zulip Karl Palmskog (Jul 09 2023 at 21:33):

well, in this case I didn't see that the simpl went through a bunch of typeclass definitions

view this post on Zulip Karl Palmskog (Jul 09 2023 at 21:35):

I also got that familiar typeclass "action at a distance" feeling. Not a robust formal notion, but usually a useful intuition

view this post on Zulip Janno (Jul 10 2023 at 08:06):

I think I found the same breakage in https://github.com/Janno/BRiCk/commit/8a1a6894b6518674bcaa6655f794b6c6e9aec840 but I haven't investigated further. The simpl change was my first guess so I just assumed the change was to be expected.

view this post on Zulip Paolo Giarrusso (Jul 10 2023 at 09:34):

if sb let their canonical structure projections simplify you'd risk the same results.
I guess the difference is that math-comp has an extremely regular and robust pattern? stdpp typeclasses are often simpl never for similar reasons


Last updated: Oct 13 2024 at 01:02 UTC