bump to nightly-2023-08-17

Stream: mathlib4

[Scott Morrison]

Today's bump is massive, touching over 200 files, as it includes the change to core that make simp fail if it makes no progress.

I've been keeping this afloat for a while, and it has rotted a few times, so as per usual for me the git history is a complete mess. Sorry?

Review very much appreciated, as I don't want to have to keep this from rotting for any longer than necessary. We're still waiting on a bump to aesop and to std to go through before it can be merged.

[Eric Wieser]

Do you mean 2023-08-16 in #6610? I can't find the PR.

[Scott Morrison]

#6019

[Notification Bot]

13 messages were moved from this topic to #general > difficulties with git rebase by Scott Morrison.

[Eric Wieser]

Regarding rot and the dependencies; most of these simp removals also compile without the bump, right? If you PRd those by themselves then we could merge them before the upstream PRs are merged.

[Scott Morrison]

That ... is an excellent point. I think I badly underestimated how long it would take me to get the Lean 4 patch merged, so kept hoping it could all happen in one go.

[Eric Wieser]

#6632 starts that

[Eric Wieser]

It's your PR, with all the build configuration removed, and anything that might be an implementation bug kicked out too

[Alex J. Best]

One thing I'm a bit worried about is that the current simp_rw implementation does a simp only [] first before doing anything else. This was added when we were thinking about doing fail_if_no_progress for simp_rw to make it clear that the progress was coming from the simp lemma requested (rather than just some zeta reduction or something simp did by default). See https://github.com/leanprover-community/mathlib4/blob/485b736d48a5d94ff465810656263ba25f677808/Mathlib/Tactic/SimpRw.lean#L57, I wonder if this should now become a try simp only [] before trying to find failures, as there may be a lot of spurious failures if this simp only is doing nothing and now failing, and not the user requested ones.

[Eric Wieser]

I'd argue that try simp only [] should be simp only (fail_if_no_progress := false)

[Eric Wieser]

try is probably acceptable in proofs, but we shouldn't use it as a substitute for the new configuration when building tactics

[Scott Morrison]

Okay, I've just squashed all the commits on this epic PR, and I have a local build+test.

Let's get this in! :-)

[Richard Copley]

@@ -398,8 +398,11 @@ theorem _root_.Wbtw.wOppSide₁₃ {s : AffineSubspace R P} {x y z : P} (h : Wbt
   rcases ht0.lt_or_eq with (ht0' | rfl); swap
   · rw [lineMap_apply_zero]; simp
   refine' Or.inr (Or.inr ⟨1 - t, t, sub_pos.2 ht1', ht0', _⟩)
-  simp_rw [lineMap_apply, vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, ← neg_vsub_eq_vsub_rev z x,
-    vsub_self, zero_sub, ← neg_one_smul R (z -ᵥ x), ← add_smul, smul_neg, ← neg_smul, smul_smul]
+  -- TODO: after lean4#2336 "simp made no progress feature"
+  -- had to add `_` to several lemmas here. Not sure why!
+  simp_rw [lineMap_apply _, vadd_vsub_assoc _, vsub_vadd_eq_vsub_sub _,
+    ← neg_vsub_eq_vsub_rev z x, vsub_self _, zero_sub, ← neg_one_smul R (z -ᵥ x),
+    ← add_smul, smul_neg, ← neg_smul, smul_smul]
   ring_nf
 #align wbtw.w_opp_side₁₃ Wbtw.wOppSide₁₃

Same lemmas, no?

[Richard Copley]

Oh sorry, I misread

[Scott Morrison]

A reminder on #6019. The next nightly is about to land, and I'd love to try out the auto-merge-after-CI label, but need this out of the way first. :-)

[Eric Wieser]

Not directly related to the PR; but is there any way we can make simp (config := {failIfUnchanged := false}) less of a mouthful? Is there a reason we dropped the simp {failIfUnchanged := false}-style syntax from Lean 3?