Karl Palmskog (Jul 09 2023 at 15:59): 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).
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).
Karl Palmskog (Jul 09 2023 at 19:20):ah, that looks quite plausible, so we might have depended on a bug (hardly first time)
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
Paolo Giarrusso (Jul 09 2023 at 19:33):so the behavior is relevant, tho I don't have an actual explanation
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) *)
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
Karl Palmskog (Jul 09 2023 at 19:45):maybe due to typeclass indirection (local vs. non-local leq)
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
simplno longer reduces something, this may be due to an indirectsimpl neverexposed by #13448
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)
Karl Palmskog (Jul 09 2023 at 20:07):typeclass management is a black art, episode 700
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)
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
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
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.
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