Lean 4.5.0
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:
#eval "this string \
is only one line \
long."
"this string is only one line long."
Gaps also work with interpolation:
#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:
#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:
#eval r#"I said "hello""#
"I said \"hello\""
More hash marks can be used to enable the inclusion of hash-marked strings without escaping:
#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:
mutual
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 => f j k (n + 1)
| 0, 0, n + 1 => f 0 1 n
| _, 0, _ => 3Lean 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.