Release v4.6.0-rc1 · leanprover/lean4

Add custom simplification procedures (aka simprocs) to simp. Simprocs can be triggered by the simplifier on a specified term-pattern. Here is an small example:

import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat

def foo (x : Nat) : Nat :=
  x + 10

/--
The `simproc` `reduceFoo` is invoked on terms that match the pattern `foo _`.
-/
simproc reduceFoo (foo _) :=
  /- A term of type `Expr → SimpM Step -/
  fun e => do
    /-
    The `Step` type has three constructors: `.done`, `.visit`, `.continue`.
    * The constructor `.done` instructs `simp` that the result does
      not need to be simplied further.
    * The constructor `.visit` instructs `simp` to visit the resulting expression.
    * The constructor `.continue` instructs `simp` to try other simplification procedures.

    All three constructors take a `Result`. The `.continue` contructor may also take `none`.
    `Result` has two fields `expr` (the new expression), and `proof?` (an optional proof).
     If the new expression is definitionally equal to the input one, then `proof?` can be omitted or set to `none`.
    -/
    /- `simp` uses matching modulo reducibility. So, we ensure the term is a `foo`-application. -/
    unless e.isAppOfArity ``foo 1 do
      return .continue
    /- `Nat.fromExpr?` tries to convert an expression into a `Nat` value -/
    let some n ← Nat.fromExpr? e.appArg!
      | return .continue
    return .done { expr := Lean.mkNatLit (n+10) }

We disable simprocs support by using the command set_option simprocs false. This command is particularly useful when porting files to v4.6.0.
Simprocs can be scoped, manually added to simp commands, and suppressed using -. They are also supported by simp?. simp only does not execute any simproc. Here are some examples for the simproc defined above.

example : x + foo 2 = 12 + x := by
  set_option simprocs false in
    /- This `simp` command does not make progress since `simproc`s are disabled. -/
    fail_if_success simp
  simp_arith

example : x + foo 2 = 12 + x := by
  /- `simp only` must not use the default simproc set. -/
  fail_if_success simp only
  simp_arith

example : x + foo 2 = 12 + x := by
  /-
  `simp only` does not use the default simproc set,
  but we can provide simprocs as arguments. -/
  simp only [reduceFoo]
  simp_arith

example : x + foo 2 = 12 + x := by
  /- We can use `-` to disable `simproc`s. -/
  fail_if_success simp [-reduceFoo]
  simp_arith

The command register_simp_attr <id> now creates a simp and a simproc set with the name <id>. The following command instructs Lean to insert the reduceFoo simplification procedure into the set my_simp. If no set is specified, Lean uses the default simp set.

simproc [my_simp] reduceFoo (foo _) := ...

The syntax of the termination_by and decreasing_by termination hints is overhauled:
- They are now placed directly after the function they apply to, instead of
  after the whole mutual block.
- Therefore, the function name no longer has to be mentioned in the hint.
- If the function has a where clause, the termination_by and
  decreasing_by for that function come before the where. The
  functions in the where clause can have their own termination hints, each
  following the corresponding definition.
- The termination_by clause can only bind “extra parameters”, that are not
  already bound by the function header, but are bound in a lambda (:= fun x y z =>) or in patterns (| x, n + 1 => …). These extra parameters used to
  be understood as a suffix of the function parameters; now it is a prefix.
Migration guide: In simple cases just remove the function name, and any
variables already bound at the header.
```
 def foo : Nat → Nat → Nat := …
-termination_by foo a b => a - b
+termination_by a b => a - b
```
or
```
 def foo : Nat → Nat → Nat := …
-termination_by _ a b => a - b
+termination_by a b => a - b
```
If the parameters are bound in the function header (before the :), remove them as well:
```
 def foo (a b : Nat) : Nat := …
-termination_by foo a b => a - b
+termination_by a - b
```
Else, if there are multiple extra parameters, make sure to refer to the right
ones; the bound variables are interpreted from left to right, no longer from
right to left:
```
 def foo : Nat → Nat → Nat → Nat
   | a, b, c => …
-termination_by foo b c => b
+termination_by a b => b
```
In the case of a mutual block, place the termination arguments (without the
function name) next to the function definition:
```
-mutual
-def foo : Nat → Nat → Nat := …
-def bar : Nat → Nat := …
-end
-termination_by
-  foo a b => a - b
-  bar a => a
+mutual
+def foo : Nat → Nat → Nat := …
+termination_by a b => a - b
+def bar : Nat → Nat := …
+termination_by a => a
+end
```
Similarly, if you have (mutual) recursion through where or let rec, the
termination hints are now placed directly after the function they apply to:
```
-def foo (a b : Nat) : Nat := …
-  where bar (x : Nat) : Nat := …
-termination_by
-  foo a b => a - b
-  bar x => x
+def foo (a b : Nat) : Nat := …
+termination_by a - b
+  where
+    bar (x : Nat) : Nat := …
+    termination_by x

-def foo (a b : Nat) : Nat :=
-  let rec bar (x : Nat) :  Nat := …
-  …
-termination_by
-  foo a b => a - b
-  bar x => x
+def foo (a b : Nat) : Nat :=
+  let rec bar (x : Nat) : Nat := …
+    termination_by x
+  …
+termination_by a - b
```
In cases where a single decreasing_by clause applied to multiple mutually
recursive functions before, the tactic now has to be duplicated.
The semantics of decreasing_by changed; the tactic is applied to all
termination proof goals together, not individually.

This helps when writing termination proofs interactively, as one can focus
each subgoal individually, for example using ·. Previously, the given
tactic script had to work for all goals, and one had to resort to tactic
combinators like first:
```
 def foo (n : Nat) := … foo e1 … foo e2 …
-decreasing_by
-simp_wf
-first | apply something_about_e1; …
-      | apply something_about_e2; …
+decreasing_by
+all_goals simp_wf
+· apply something_about_e1; …
+· apply something_about_e2; …
```
To obtain the old behaviour of applying a tactic to each goal individually,
use all_goals:
```
 def foo (n : Nat) := …
-decreasing_by some_tactic
+decreasing_by all_goals some_tactic
```
In the case of mutual recursion each decreasing_by now applies to just its
function. If some functions in a recursive group do not have their own
decreasing_by, the default decreasing_tactic is used. If the same tactic
ought to be applied to multiple functions, the decreasing_by clause has to
be repeated at each of these functions.
Modify InfoTree.context to facilitate augmenting it with partial contexts while elaborating a command. This breaks backwards compatibility with all downstream projects that traverse the InfoTree manually instead of going through the functions in InfoUtils.lean, as well as those manually creating and saving InfoTrees. See PR #3159 for how to migrate your code.
Add language server support for call hierarchy requests (PR #3082). The change to the .ilean format in this PR means that projects must be fully rebuilt once in order to generate .ilean files with the new format before features like "find references" work correctly again.
Structure instances with multiple sources (for example {a, b, c with x := 0}) now have their fields filled from these sources
in strict left-to-right order. Furthermore, the structure instance elaborator now aggressively use sources to fill in subobject
fields, which prevents unnecessary eta expansion of the sources,
and hence greatly reduces the reliance on costly structure eta reduction. This has a large impact on mathlib,
reducing total CPU instructions by 3% and enabling impactful refactors like leanprover-community/mathlib4#8386
which reduces the build time by almost 20%.
See PR #2478 and RFC #2451.
Add pretty printer settings to omit deeply nested terms (pp.deepTerms false and pp.deepTerms.threshold) (PR #3201)
Add pretty printer options pp.numeralTypes and pp.natLit.
When pp.numeralTypes is true, then natural number literals, integer literals, and rational number literals
are pretty printed with type ascriptions, such as (2 : Rat), (-2 : Rat), and (-2 / 3 : Rat).
When pp.natLit is true, then raw natural number literals are pretty printed as nat_lit 2.
PR #2933 and RFC #3021.

Lake updates:

improved platform information & control #3226
lake update from unsupported manifest versions #3149

Other improvements:

make intro be aware of let_fun #3115
produce simpler proof terms in rw #3121
fuse nested mkCongrArg calls in proofs generated by simp #3203
induction using followed by a general term #3188
allow generalization in let [#3060](#3060, fixing #3065
reducing out-of-bounds swap! should return a, not `default`` #3197, fixing #3196
derive BEq on structure with Prop-fields #3191, fixing #3140
refine through more casesOnApp/matcherApp #3176, fixing #3175
do not strip dotted components from lean module names #2994, fixing #2999
fix deriving only deriving the first declaration for some handlers #3058, fixing #3057
do not instantiate metavariables in kabstract/rw for disallowed occurrences #2539, fixing #2538
hover info for cases h : ... #3084

What's Changed

chore: update tests for #2966 to use test_extern by @semorrison in #3092
chore: begin development cycle for v4.6.0 by @semorrison in #3109
fix: hover info for cases h : ... by @digama0 in #3084
chore: remove workaround in widgets by @Vtec234 in #3105
chore: include full build in stdlib benchmark by @Kha in #3104
doc: fix typos by @marcusrossel in #3114
test: test “motive is not type correct” by @nomeata in #3122
chore: remove unused argument at DiscrTree by @leodemoura in #3123
feat: delaborate have inside do blocks by @kmill in #3116
doc: fix typo “reursive” by @nomeata in #3131
feat: do not instantiate metavariables in kabstract/rw for disallowed occurrences by @semorrison in #2539
chore: Netlify deployment for manual by @david-christiansen in #3138
fix: reduceNat? match terms with free or meta variables by @joehendrix in #3139
chore: pr-release.yaml: indicate information using github status by @nomeata in #3137
feat: let get_elem_tactic_trivial handle [a]'h.2 by @nomeata in #3132
chore: pr-release.yml: Suggest nightly-with-mathlib by @nomeata in #3148
fix: manage all declarations in a given derive by @arthur-adjedj in #3058
doc: Document that Float corresponds to 64-bit double in C by @girving in #3147
refactor: WF.Eqns: remove unreachable fix-folding by @nomeata in #3133
feat: add Simprocs by @leodemoura in #3124
chore: fix typo from #3148 in pr-release bot by @semorrison in #3154
doc: state that Float is IEEE compliant by @girving in #3157
feat: extract delabAppCore, define withOverApp, and make over-applied projections pretty print by @kmill in #3083
fix: do not strip dotted components from lean module names by @eric-wieser in #2994
chore: actually include full build in benchmark by @Kha in #3158
feat: per-function termination hints by @nomeata in #3040
doc: mention termination_by and decreasing_by by @nomeata in #3016
feat: lake update from unsupported manifest versions by @tydeu in #3149
feat: add bitwise operations to reduceNat? and kernel by @joehendrix in #3134
chore: use more specific import in OfScientific by @joehendrix in #3165
chore: use termination_by in Nat.gcd by @joehendrix in #3164
chore: pr-release.yml: parentheses are significant in jq by @nomeata in #3169
chore: pr-release: more robust comment id recognition by @nomeata in #3173
fix: Fix/GuessLex: refine through more casesOnApp/matcherApp by @nomeata in #3176
feat: lake: GNU/BSD OS detection in test scripts by @digama0 in #3180
doc: fix typos by @marcusrossel in #3178
chore: CI: add actionlint action, fix actions by @nomeata in #3156
test: failed to infer implicit target by @nomeata in #3189
fix: derive BEq on structure with Prop-fields by @arthur-adjedj in #3191
fix: checkTargets check for duplicate target by @nomeata in #3171
feat: new implementation for simp (config := { ground := true }) by @leodemoura in #3187
refactor: rewrite: produce simpler proof terms by @nomeata in #3121
fix: reducing out-of-bounds swap! should return a, not default by @nomeata in #3197
chore: CI looks for nightly-testing-YYYY-MM-DD at Mathlib as either a branch or tag by @semorrison in #3199
doc: clarify and expand docstrings for the instantiate functions by @kmill in #3183
chore: CI creates lean-pr-testing-NNNN branches at Std too by @semorrison in #3200
feat: partial context info by @mhuisi in #3159
doc: update RELEASES.md for #3159 by @mhuisi in #3205
doc: add missing 'not' in simprocs example in RELEASES.md by @dwrensha in #3206
feat: make mkApp, mkApp2, ..., mkApp10 have @[match_pattern] attribute by @kmill in #2900
fix: allow generalization in let by @eric-wieser in #3060
fix: predefinition preprocessing: float .mdata out of non-unary applications by @nomeata in #3204
feat: System.Platform.target by @Kha in #3207
feat: cleanups to ACI and Identity classes by @joehendrix in #3195
fix: broken internal links in the docs by @david-christiansen in #3216
doc: remove nightly and other outdated references by @Kha in #3027
feat: synchronous execution of task continuations by @Kha in #3013
feat: add call hierarchy support by @mhuisi in #3082
feat: induction using by @nomeata in #3188
refactor: fuse nested mkCongrArg calls by @nomeata in #3203
doc: update link target by @david-christiansen in #3218
doc: adjust RELEASES.md call hierarchy url by @mhuisi in #3220
fix: do not throw C++ heartbeat exceptions in pure functions by @Kha in #3224
doc: expand docstring for intros by @kmill in #2777
chore: add GitHub token to manual link checker by @david-christiansen in #3235
feat: make intro be aware of let_fun by @kmill in #3115
chore: remove unused GH Pages deployment by @Kha in #3217
refactor: forallAltTelescope to take altNumParams by @nomeata in #3230
feat: elidible subterms by @mhuisi in #3201
feat: @[unused_variables_ignore_fn] attribute by @digama0 in #3184
doc: add doc for FileMap by @joneugster in #3221
feat: lake: improved platform information & control by @tydeu in #3226
feat: use supplied structure fields left to right and eta reduce terms in structure instance elaboration by @mattrobball in #2478
refactor: cleanup simp types and pre and post method semantics by @leodemoura in #3210
feat: pp.numericTypes option for printing number literals with type ascriptions by @kmill in #2933
chore: CI: do not fail on broken links by @Kha in #3238
doc: fix typos by @marcusrossel in #3236

New Contributors

@girving made their first contribution in #3147
@mattrobball made their first contribution in #2478

Full Changelog: v4.5.0...v4.6.0-rc1

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

v4.6.0-rc1

Choose a tag to compare

Sorry, something went wrong.

Sorry, something went wrong.

Uh oh!

No results found

What's Changed

New Contributors

Contributors

Uh oh!