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).
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).
ah, that looks quite plausible, so we might have depended on a bug (hardly first time)
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
so the behavior is relevant, tho I don't have an actual explanation
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
maybe due to typeclass indirection (local vs. non-local leq
)
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 indirectsimpl never
exposed by #13448
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)
typeclass management is a black art, episode 700
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)
well, in this case I didn't see that the simpl went through a bunch of typeclass definitions
I also got that familiar typeclass "action at a distance" feeling. Not a robust formal notion, but usually a useful intuition
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.
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