v4.18.0-rc1

Stream: general

[Kim Morrison]

We're not quite there with the Verso release for v4.18.0-rc1, but that will follow shortly:

% script/release_checklist.py v4.18.0-rc1

Performing preliminary checks...
  ✅ Branch releases/v4.18.0 exists
  ✅ CMake version settings are correct in src/CMakeLists.txt
  ✅ Tag v4.18.0-rc1 exists
  ✅ Release page for v4.18.0-rc1 exists
  ✅ Release notes look good.

Checking repositories...

Repository: Batteries
  ✅ On compatible toolchain (>= v4.18.0-rc1)
  ✅ Tag v4.18.0-rc1 exists
  ✅ Bump branch bump/v4.19.0 exists
  ✅ Bump branch correctly uses toolchain: leanprover/lean4:nightly-2025-03-03

Repository: lean4checker
  ✅ On compatible toolchain (>= v4.18.0-rc1)
  ✅ Tag v4.18.0-rc1 exists

Repository: quote4
  ✅ On compatible toolchain (>= v4.18.0-rc1)
  ✅ Tag v4.18.0-rc1 exists

Repository: doc-gen4
  ✅ On compatible toolchain (>= v4.18.0-rc1)
  ✅ Tag v4.18.0-rc1 exists

Repository: Verso
  ❌ Not on target toolchain (needs ≥ v4.18.0-rc1, but main is on leanprover/lean4:nightly-2025-02-19)

Repository: Cli
  ✅ On compatible toolchain (>= v4.18.0-rc1)
  ✅ Tag v4.18.0-rc1 exists

Repository: ProofWidgets4
  ✅ On compatible toolchain (>= v4.18.0-rc1)

Repository: Aesop
  ✅ On compatible toolchain (>= v4.18.0-rc1)
  ✅ Tag v4.18.0-rc1 exists

Repository: import-graph
  ✅ On compatible toolchain (>= v4.18.0-rc1)
  ✅ Tag v4.18.0-rc1 exists

Repository: plausible
  ✅ On compatible toolchain (>= v4.18.0-rc1)
  ✅ Tag v4.18.0-rc1 exists

Repository: Mathlib
  ✅ On compatible toolchain (>= v4.18.0-rc1)
  ✅ Tag v4.18.0-rc1 exists
  ✅ Bump branch bump/v4.19.0 exists
  ✅ Bump branch correctly uses toolchain: leanprover/lean4:nightly-2025-03-03

Repository: REPL
  ✅ On compatible toolchain (>= v4.18.0-rc1)
  ✅ Tag v4.18.0-rc1 exists

Checking lean4 master branch configuration...
  ✅ lean4 master branch is configured for next development cycle

[Yaël Dillies]

I think this is an important change to mention for mathlib:

• lean4#7100 modifies the structure syntax so that parents can be named, like in
  structure S extends toParent : P
  Breaking change: The syntax is also modified so that the resultant type comes before the extends clause, for example structure S : Prop extends P. This is necessary to prevent a parsing ambiguity, but also this is the natural place for the resultant type. Implements RFC lean4#7099.

[Rémy Degenne]

Is there an explanation somewhere of what the grind tactic does, and what type of problems it is supposed to be solving?
I read the name grind 100 times in those release notes but I have only that very fuzzy idea that it's supposed to be a new powerful tactic for solving many goals.

[Henrik Böving]

There does not yet exist such an explanation and using it practically is going to require annotating the standard library first (which the FRO is going to do in due time). In short grind combines most notably:

• forward and backward reasoning
• doing automated case analysis
• omega but complete (current omega can't do all of linear integer arithmetic) and more optimized
• the theory of uninterpreted functions which boils down to reasoning by congruence and quantifier instantiation

There is over 60 tests in this directory prefixd with grind_ if you want to see what that combination can achieve already

[Yaël Dillies]

Henrik Böving said:

• omega but complete

How is it supposed to compare to omega performance-wise?

[Markus Himmel]

Does "and more optimized" not answer your question?

[Yaël Dillies]

Oh, I guess it does, yes

[Patrick Massot]

Is grind meant to subsume cc as well?

[Henrik Böving]

congruence closure is one of the algorithms at play in the theory of uninterpreted functions so it should be able to do that yeah. For example

example (a b c : ℕ) (f : ℕ → ℕ) (h: a = b) (h' : b = c) : f a = f c := by grind

example (f : ℕ → ℕ) (x : ℕ)
  (H1 : f (f (f x)) = x) (H2 : f (f (f (f (f x)))) = x) :
  f x = x := by grind

already works

[Violeta Hernández]

I've been playing around with aesop as of late, and "forward and backward reasoning/automated case analysis" is where I've found that tactic to be the most useful. As a user, are there any differences between aesop and grind I should keep in mind?

[Henrik Böving]

Grind isn't really fully locked in yet but the procedure it uses works very differently, for example Aesop applies simp_all repeatedly while grind uses its own annotations and rewriting style procedures (even though you might often want to write both) and there is more technical differences beyond that. I'd suggest to wait on exact usage guidelines until its out of its incubation phase^^

[Patrick Massot]

I’m curious about all those commits we see mentioning divisibility. Is it important to prove divisibility statement in program verification? Or is it motivated by internal procedures of grind that need to prove or use divisibility to prove user facing goals that do not mention divisibility?

[Marcus Rossel]

Patrick Massot said:

I’m curious about all those commits we see mentioning divisibility. Is it important to prove divisibility statement in program verification? Or is it motivated by internal procedures of grind that need to prove or use divisibility to prove user facing goals that do not mention divisibility?

From what I can tell, all the divisibility stuff is used by grind to solve linear integer arithmetic as in Cutting to the Chase.

[Shreyas Srinivas]

Patrick Massot said:

I’m curious about all those commits we see mentioning divisibility. Is it important to prove divisibility statement in program verification? Or is it motivated by internal procedures of grind that need to prove or use divisibility to prove user facing goals that do not mention divisibility?

It is definitely useful for solving linear systems of equations which is important in many real time system scenarios. I recently learnt of a line of work in algorithms theory that explores the complexity of computing matrix invariants without division and the complexity is much higher. So I can imagine that linear arithmetic procedures in general have lower complexity with division.

[Henrik Böving]

Marcus Rossel said:

Patrick Massot said:

I’m curious about all those commits we see mentioning divisibility. Is it important to prove divisibility statement in program verification? Or is it motivated by internal procedures of grind that need to prove or use divisibility to prove user facing goals that do not mention divisibility?

From what I can tell, all the divisibility stuff is used by grind to solve linear integer arithmetic as in Cutting to the Case.

Yes this is the reason, the cutsat algorithm can generate formulas internally that have divisibility constraints. Note that grind is not a 1:1 implementation of cutsat, it contains many special cases to avoid case splitting if possible as that would not be efficient in a system like Lean.

[Kim Morrison]

In particular, in docs#Int.cooper_resolution_dvd_left notice that even when the input divisibility constraint is trivial (d=1), Cooper resolution may produce an non-trivial divisibility constraint.

[Kim Morrison]

(And if you're wondering "doesn't omega already solve these problems": the cutsat-like implementation in grind is more complete, probably faster, generates counterexamples (and can even generate diverse counterexamples, and then "notice" candidate equalities when the counterexamples have coincidences)... Lots of goodies coming.)

[Patrick Massot]

Thanks for all those answers!