Lean 4.5.0

David Thrane Christiansen

2024-02-04

Release Announcements

Lean version 4.5.0 has been released! This release contains a number of quality-of-life improvements.

Please see the detailed release notes for a complete list of changes.

String Literals

Taking inspiration from Rust and Python, Lean's string literals are now more flexible. String gaps make it easier to write long strings on multiple lines without introducing newlines into the string, and raw strings allow string literals to include characters that would otherwise be escaped.

String gaps are indicated with a backslash right before a newline, which causes the newline and the spaces at the beginning of the next line to be ignored:

"this string is only one line long."#eval "this string \
         is only one line \
  long."

"this string is only one line long."

Gaps also work with interpolation:

"this string contains 1\n  newline with two spaces."#eval s!"this string \
     contains {Nat.pred 2}
  newline with two spaces."

"this string contains 1\n  newline with two spaces."

Raw strings don't process backslash escapes. This is primarily useful when representing escape sequences in a string literal, as they would otherwise need to be double-escaped. Raw literals begin with a lowercase r:

"This is a backslash: \\"#eval r"This is a backslash: \"

"This is a backslash: \\"

To include a double-quote character in a raw literal, surround the opening and closing double-quotes with hash marks:

"I said \"hello\""#eval r#"I said "hello""#

"I said \"hello\""

More hash marks can be used to enable the inclusion of hash-marked strings without escaping:

"I said #\"hello\"#"#eval r##"I said #"hello"#"##

"I said #\"hello\"#"

Error Message Improvements

Many error messages have been made more friendly and actionable.

Mutual Blocks

Instead of reporting invalid mutual block when mixing inductive types and definitions in the same block, Lean now provides more guidance:

invalid mutual block: either all elements of the block must be inductive declarations, or they must all be definitions/theorems/abbrevsmutual
  inductive A
  | mkA : String → A

  def a : A := .mkA "a"
end

invalid mutual block: either all elements of the block must be inductive declarations, or they must all be definitions/theorems/abbrevs

Lexicographic Termination Arguments

When checking recursive functions, Lean tries to justify that the function always terminates with two techniques: structural recursion, in which all recursive calls are passed syntactic sub-terms of one of the arguments, and well-founded recursion, in which termination is justfied by appeal to some other notion of size. Joachim Breitner's blog post describes these techniques in detail. Crucially, well-founded recursion can combine size changes of multiple arguments, and it can often discover these combinations automatically.

Starting in version 4.5.0, Lean now provides a table that describes why it can't combine decreasing sizes. For this definition:

def f (j k n : Nat) : Nat :=
  match j, k, n with
  | 0, 0, 0 => 0
  | j, k + 1, n => fail to show termination for
  f
with errors
argument #1 was not used for structural recursion
  failed to eliminate recursive application
    _root_.f j k (n + 1)

argument #2 was not used for structural recursion
  failed to eliminate recursive application
    _root_.f 0 1 n

argument #3 was not used for structural recursion
  failed to eliminate recursive application
    _root_.f j k (n + 1)

structural recursion cannot be used

Could not find a decreasing measure.
The arguments relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
            j k n
1) 9:19-32  = < ?
2) 10:19-26 = ? _
Please use `termination_by` to specify a decreasing measure.f j k (n + 1)
  | 0, 0, n + 1 => f 0 1 n
  | _, 0, _ => 3

Lean reports the following error:

fail to show termination for
  f
with errors
argument #1 was not used for structural recursion
  failed to eliminate recursive application
    _root_.f j k (n + 1)

argument #2 was not used for structural recursion
  failed to eliminate recursive application
    _root_.f 0 1 n

argument #3 was not used for structural recursion
  failed to eliminate recursive application
    _root_.f j k (n + 1)

structural recursion cannot be used

Could not find a decreasing measure.
The arguments relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
            j k n
1) 9:19-32  = < ?
2) 10:19-26 = ? _
Please use `termination_by` to specify a decreasing measure.

The last part of the message describes the relationship of each recursive call to their argument values that Lean found. In particular, in the first case with a recursive call (| j, k + 1, n => f j k (n + 1)), the value for j remains the same, the value for k decreases, and the relationship between the input value for n and its value in the recursive call is unknown. In the second recursive case (| 0, 0, n + 1 => f 0 1 n), n remained equal, and because Lean did not conclude anything about k, it gave up searching for a lexicographic order.

Changes to `termination_by`

In Lean 4.6.0, the syntax for indicating termination measures for recursive functions will be revamped, making it more consistent and removing many confusing corner cases. To prepare for this change, Lean 4.5.0 no longer supports the little-used termination_by' syntax, which is largely a relic of Lean 4's early history. This feature allowed well-founded relations to be specified directly as expressions rather than using the WellFoundedRelation class. To migrate code that uses termination_by' to termination_by in 4.5.0, replace calls to measure with their arguments as follows:

termination_by' measure (fun ⟨i, _⟩ => as.size - i)

termination_by i _ => as.size - i

If the well-founded relation you want to use is not the one that the WellFoundedRelation type class would infer for your termination argument, you can use WellFounded.wrap to provide the appropriate relation explicitly:

termination_by' ⟨r, hwf⟩

termination_by x => hwf.wrap x

Further Improvements

Further improvements were made to the widget system, support for snippet text edits were added to Lean's LSP implementation, and many bugs were fixed. The complete details are available in the detailed release notes.