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 indirect`simpl 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: Jun 13 2024 at 06:01 UTC