v4.13.0 discussion

Stream: general

[Kim Morrison]

Discussion of the v4.13.0 release can go here!

[Asei Inoue]

blog post coming soon?

[Kim Morrison]

No blog post this month, please enjoy the release notes instead. :-)

[Joachim Breitner]

In lie of a proper release announcement with highlight, here is a feature that I had a highlight prepared for

---

The simplifier is now able to discharge side-goals that, after simplification, are of the form ∀ …, a = b, where a and b are definitionally equal. Usually these side-goals are solved by simplification using docs#eq_self, but that does not work when there are metavariables involved. This allows rewrite rules like

List.attach_map' {α : Type _} {β : Type _} {p : α → Prop} {l : List α} {f : { x // x ∈ l } → β}
  {g : α → β} {hf : ∀ x h, f ⟨x, h⟩ = g x} : l.attach.map f = l.map g

to work, where the parameter g does not appear on the rules’ left-hand-side, but will become known once the side-condition hf is discharged by simp.

This change allows the simplifier to clean up idioms related to functions like docs#List.attach, which are sometimes needed for nested recursion.

[Ruben Van de Velde]

Ugh, what happened to the v4.13.0 tag in mathlib? EulerProducts seems to have been updated to it in https://github.com/MichaelStollBayreuth/EulerProducts/commit/51a29f3dfcc57cbd802bfc100a381b4d83136fa4 but it now resolves to a newer incompatible commit

[Kim Morrison]

Apologies, the Mathlib tag was moved, see https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/cache.20and.20proofwidgets/near/480118432

[Ruben Van de Velde]

Unfortunately EulerProducts has already moved ahead, so there seems to be no good way to get a version of it that works with the new tag :/

[Ruben Van de Velde]

I guess this is on PNT+ for trying to stick to the tags while depending on a project that moves faster

[Michael Stoll]

Apologies for moving faster...

[Ruben Van de Velde]

No worries, just an annoying confluence of events

[Edward van de Meent]

something fun that has dropped in batteries is the #help note command, which finally gives an easy way to read the mathlib library notes!
test it in the playground:

import Mathlib

#help note ""

[Eric Wieser]

Ruben Van de Velde said:

Unfortunately EulerProducts has already moved ahead, so there seems to be no good way to get a version of it that works with the new tag :/

The right thing to do here would be to make a branch in EulerProducts using the corrected mathlib tag, and update the EulerProducts tag to point there. It doesn't matter that the commit in question wouldn't be in the main branch.