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
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
equal which _is_ marked as
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
anyway, I can see more people being bitten by this bugfix, maybe it should be flagged up more prominently, e.g.,
simplno longer reduces something, this may be due to an indirect
simpl neverexposed 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: Nov 29 2023 at 21:01 UTC