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:

"this string is only one line long."
#eval "this string \
         is only one line \
  long."
"this string is only one line long." : String
"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
Nat.pred (a✝ : Nat) : Nat
The predecessor function on natural numbers.

This definition is overridden in the compiler to use `n - 1` instead.
The definition provided here is the logical model.
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: \\" : String
"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\"" : String
"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\"#" : String
"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
In Lean, every concrete type other than the universes
and every type constructor other than dependent arrows
is an instance of a general family of type constructions known as inductive types.
It is remarkable that it is possible to construct a substantial edifice of mathematics
based on nothing more than the type universes, dependent arrow types, and inductive types;
everything else follows from those.
Intuitively, an inductive type is built up from a specified list of constructor.
For example, `List α` is the list of elements of type `α`, and is defined as follows:
```
inductive List (α : Type u) where
| nil
| cons (head : α) (tail : List α)
```
A list of elements of type `α` is either the empty list, `nil`,
or an element `head : α` followed by a list `tail : List α`.
For more information about [inductive types](https://lean-lang.org/theorem_proving_in_lean4/inductive_types.html).
A | mkA : String A def a : A := .mkA "a"
"a" : String
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
Nat → Nat → Nat → Nat
(j
Nat
k
Nat
n
Nat
: Nat
Nat : Type
The type of natural numbers, starting at zero. It is defined as an
inductive type freely generated by "zero is a natural number" and
"the successor of a natural number is a natural number".

You can prove a theorem `P n` about `n : Nat` by `induction n`, which will
expect a proof of the theorem for `P 0`, and a proof of `P (succ i)` assuming
a proof of `P i`. The same method also works to define functions by recursion
on natural numbers: induction and recursion are two expressions of the same
operation from lean's point of view.

```
open Nat
example (n : Nat) : n < succ n := by
  induction n with
  | zero =>
    show 0 < 1
    decide
  | succ i ih => -- ih : i < succ i
    show succ i < succ (succ i)
    exact Nat.succ_lt_succ ih
```

This type is special-cased by both the kernel and the compiler:
* The type of expressions contains "`Nat` literals" as a primitive constructor,
  and the kernel knows how to reduce zero/succ expressions to nat literals.
* If implemented naively, this type would represent a numeral `n` in unary as a
  linked list with `n` links, which is horribly inefficient. Instead, the
  runtime itself has a special representation for `Nat` which stores numbers up
  to 2^63 directly and larger numbers use an arbitrary precision "bignum"
  library (usually [GMP](https://gmplib.org/)).
) : Nat
Nat : Type
The type of natural numbers, starting at zero. It is defined as an
inductive type freely generated by "zero is a natural number" and
"the successor of a natural number is a natural number".

You can prove a theorem `P n` about `n : Nat` by `induction n`, which will
expect a proof of the theorem for `P 0`, and a proof of `P (succ i)` assuming
a proof of `P i`. The same method also works to define functions by recursion
on natural numbers: induction and recursion are two expressions of the same
operation from lean's point of view.

```
open Nat
example (n : Nat) : n < succ n := by
  induction n with
  | zero =>
    show 0 < 1
    decide
  | succ i ih => -- ih : i < succ i
    show succ i < succ (succ i)
    exact Nat.succ_lt_succ ih
```

This type is special-cased by both the kernel and the compiler:
* The type of expressions contains "`Nat` literals" as a primitive constructor,
  and the kernel knows how to reduce zero/succ expressions to nat literals.
* If implemented naively, this type would represent a numeral `n` in unary as a
  linked list with `n` links, which is horribly inefficient. Instead, the
  runtime itself has a special representation for `Nat` which stores numbers up
  to 2^63 directly and larger numbers use an arbitrary precision "bignum"
  library (usually [GMP](https://gmplib.org/)).
:= match
Pattern matching. `match e, ... with | p, ... => f | ...` matches each given
term `e` against each pattern `p` of a match alternative. When all patterns
of an alternative match, the `match` term evaluates to the value of the
corresponding right-hand side `f` with the pattern variables bound to the
respective matched values.
If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available
within `f`.

When not constructing a proof, `match` does not automatically substitute variables
matched on in dependent variables' types. Use `match (generalizing := true) ...` to
enforce this.

Syntax quotations can also be used in a pattern match.
This matches a `Syntax` value against quotations, pattern variables, or `_`.

Quoted identifiers only match identical identifiers - custom matching such as by the preresolved
names only should be done explicitly.

`Syntax.atom`s are ignored during matching by default except when part of a built-in literal.
For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they
should participate in matching.
For example, in
```lean
syntax "c" ("foo" <|> "bar") ...
```
`foo` and `bar` are indistinguishable during matching, but in
```lean
syntax foo := "foo"
syntax "c" (foo <|> "bar") ...
```
they are not.
j
Nat
, k
Nat
, n
Nat
with
Pattern matching. `match e, ... with | p, ... => f | ...` matches each given
term `e` against each pattern `p` of a match alternative. When all patterns
of an alternative match, the `match` term evaluates to the value of the
corresponding right-hand side `f` with the pattern variables bound to the
respective matched values.
If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available
within `f`.

When not constructing a proof, `match` does not automatically substitute variables
matched on in dependent variables' types. Use `match (generalizing := true) ...` to
enforce this.

Syntax quotations can also be used in a pattern match.
This matches a `Syntax` value against quotations, pattern variables, or `_`.

Quoted identifiers only match identical identifiers - custom matching such as by the preresolved
names only should be done explicitly.

`Syntax.atom`s are ignored during matching by default except when part of a built-in literal.
For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they
should participate in matching.
For example, in
```lean
syntax "c" ("foo" <|> "bar") ...
```
`foo` and `bar` are indistinguishable during matching, but in
```lean
syntax foo := "foo"
syntax "c" (foo <|> "bar") ...
```
they are not.
| 0, 0, 0 => 0 | j
Nat
, k
Nat
+ 1, n
Nat
=> 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) 122:19-32 = < ? 2) 123:19-26 = ? _ Please use `termination_by` to specify a decreasing measure.f
Nat → Nat → Nat → Nat
j
Nat
k
Nat
(n
Nat
+ 1) | 0, 0, n
Nat
+ 1 => f
Nat → Nat → Nat → Nat
0 1 n
Nat
| _, 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) 122:19-32 = < ?
2) 123: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.