feat: simprocs for String and Char <, <=, >, >=

Fixes two output bugs with cloud releases: (1) the fetch as part of an
`extraDep` was not properly isolated in a job, and (2) the release job
would be shown even if the release had already been successfully
fetched.

Also includes some related touchups, including the addition of show all
jobs on `-v` which helps with debugging job counts.

.github/ISSUE_TEMPLATE/bug_report.md

@@ -9,9 +9,15 @@ assignees: ''
 
 ### Prerequisites
 
-* [ ] Put an X between the brackets on this line if you have done all of the following:
-    * Check that your issue is not already [filed](https://github.com/leanprover/lean4/issues).
-    * Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.
+Please put an X between the brackets as you perform the following steps:
+
+* [ ] Check that your issue is not already filed:
+      https://github.com/leanprover/lean4/issues
+* [ ] Reduce the issue to a minimal, self-contained, reproducible test case.
+      Avoid dependencies to Mathlib or Batteries.
+* [ ] Test your test case against the latest nightly release, for example on
+      https://live.lean-lang.org/#project=lean-nightly
+      (You can also use the settings there to switch to “Lean nightly”)
 
 ### Description
 
@@ -33,8 +39,8 @@ assignees: ''
 
 ### Versions
 
-[Output of `#eval Lean.versionString` or of `lean --version` in the folder that the issue occured in]
-[OS version]
+[Output of `#eval Lean.versionString`]
+[OS version, if not using live.lean-lang.org.]
 
 ### Additional Information
 

.github/workflows/ci.yml

@@ -6,7 +6,6 @@ on:
     tags:
       - '*'
   pull_request:
-    types: [opened, synchronize, reopened, labeled]
   merge_group:
   schedule:
     - cron: '0 7 * * *'  # 8AM CET/11PM PT
@@ -41,12 +40,18 @@ jobs:
     steps:
       - name: Run quick CI?
         id: set-quick
-        env:
-          quick: ${{
-            github.event_name == 'pull_request' && !contains( github.event.pull_request.labels.*.name, 'full-ci')
-           }}
+        # We do not use github.event.pull_request.labels.*.name here because
+        # re-running a run does not update that list, and we do want to be able to
+        # rerun the workflow run after settings the `full-ci` label.
         run: |
-          echo "quick=${{env.quick}}" >> "$GITHUB_OUTPUT"
+          if [ "${{ github.event_name }}" == 'pull_request' ]
+          then
+            echo "quick=$(gh api repos/${{ github.repository_owner }}/${{ github.event.repository.name }}/pulls/${{ github.event.pull_request.number }} --jq '.labels | any(.name == "full-ci") | not')" >> "$GITHUB_OUTPUT"
+          else
+            echo "quick=false" >> "$GITHUB_OUTPUT"
+          fi
+        env:
+          GH_TOKEN: ${{ github.token }}
 
       - name: Configure build matrix
         id: set-matrix
@@ -54,7 +59,10 @@ jobs:
         with:
           script: |
             const quick = ${{ steps.set-quick.outputs.quick }};
-            console.log(`quick: ${quick}`)
+            console.log(`quick: ${quick}`);
+            // use large runners outside PRs where available (original repo)
+            // disabled for now as this mostly just speeds up the test suite which is not a bottleneck
+            // let large = ${{ github.event_name != 'pull_request' && github.repository == 'leanprover/lean4' }} ? "-large" : "";
             let matrix = [
               {
                 // portable release build: use channel with older glibc (2.27)

.github/workflows/nix-ci.yml

@@ -6,7 +6,6 @@ on:
     tags:
       - '*'
   pull_request:
-    types: [opened, synchronize, reopened, labeled]
   merge_group:
 
 concurrency:

.github/workflows/pr-release.yml

@@ -126,11 +126,11 @@ jobs:
           if [ "$NIGHTLY_SHA" = "$MERGE_BASE_SHA" ]; then
             echo "The merge base of this PR coincides with the nightly release"
 
-            STD_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover/std4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
+            BATTERIES_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/batteries.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
             MATHLIB_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/mathlib4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
 
-            if [[ -n "$STD_REMOTE_TAGS" ]]; then
-              echo "... and Std has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
+            if [[ -n "$BATTERIES_REMOTE_TAGS" ]]; then
+              echo "... and Batteries has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
               MESSAGE=""
 
               if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then
@@ -140,8 +140,8 @@ jobs:
                 MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Mathlib CI should run now."
               fi
             else
-              echo "... but Std does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
-              MESSAGE="- ❗ Std CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Std CI should run now."
+              echo "... but Batteries does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
+              MESSAGE="- ❗ Batteries CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Batteries CI should run now."
             fi
 
           else
@@ -151,7 +151,7 @@ jobs:
 
             git -C lean4.git fetch origin nightly-with-mathlib 
             NIGHTLY_WITH_MATHLIB_SHA="$(git -C lean4.git rev-parse "origin/nightly-with-mathlib")"
-            MESSAGE="- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MATHLIB_SHA\`."
+            MESSAGE="- ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MATHLIB_SHA\`."
           fi
 
           if [[ -n "$MESSAGE" ]]; then
@@ -223,27 +223,27 @@ jobs:
               description: description,
             });
 
-      # We next automatically create a Std branch using this toolchain.
-      # Std doesn't itself have a mechanism to report results of CI from this branch back to Lean
-      # Instead this is taken care of by Mathlib CI, which will fail if Std fails.
+      # We next automatically create a Batteries branch using this toolchain.
+      # Batteries doesn't itself have a mechanism to report results of CI from this branch back to Lean
+      # Instead this is taken care of by Mathlib CI, which will fail if Batteries fails.
       - name: Cleanup workspace
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
         run: |
           sudo rm -rf ./*
 
-      # Checkout the Std repository with all branches
-      - name: Checkout Std repository
+      # Checkout the Batteries repository with all branches
+      - name: Checkout Batteries repository
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
         uses: actions/checkout@v3
         with:
-          repository: leanprover/std4
+          repository: leanprover-community/batteries
           token: ${{ secrets.MATHLIB4_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
 
       - name: Check if tag exists
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        id: check_std_tag
+        id: check_batteries_tag
         run: |
           git config user.name "leanprover-community-mathlib4-bot"
           git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
@@ -251,7 +251,7 @@ jobs:
           if git ls-remote --heads --tags --exit-code origin "nightly-testing-${MOST_RECENT_NIGHTLY}" >/dev/null; then
             BASE="nightly-testing-${MOST_RECENT_NIGHTLY}"
           else
-            echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' tag at Std. Falling back to 'nightly-testing'."
+            echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' tag at Batteries. Falling back to 'nightly-testing'."
             BASE=nightly-testing
           fi
 
@@ -268,7 +268,7 @@ jobs:
           else
             echo "Branch already exists, pushing an empty commit."
             git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
-            # The Std `nightly-testing` or `nightly-testing-YYYY-MM-DD` branch may have moved since this branch was created, so merge their changes.
+            # The Batteries `nightly-testing` or `nightly-testing-YYYY-MM-DD` branch may have moved since this branch was created, so merge their changes.
             # (This should no longer be possible once `nightly-testing-YYYY-MM-DD` is a tag, but it is still safe to merge.)
             git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
             git commit --allow-empty -m "Trigger CI for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
@@ -321,7 +321,7 @@ jobs:
             git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE"
             echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}" > lean-toolchain
             git add lean-toolchain
-            sed -i "s/require std from git \"https:\/\/github.com\/leanprover\/std4\" @ \".\+\"/require std from git \"https:\/\/github.com\/leanprover\/std4\" @ \"nightly-testing-${MOST_RECENT_NIGHTLY}\"/" lakefile.lean
+            sed -i "s/require batteries from git \"https:\/\/github.com\/leanprover-community\/batteries\" @ \".\+\"/require batteries from git \"https:\/\/github.com\/leanprover-community\/batteries\" @ \"nightly-testing-${MOST_RECENT_NIGHTLY}\"/" lakefile.lean
             git add lakefile.lean
             git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
           else

.github/workflows/restart-on-label.yml

@@ -0,0 +1,31 @@
+name: Restart by label
+on:
+  pull_request_target:
+    types:
+      - unlabeled
+      - labeled
+jobs:
+  restart-on-label:
+    runs-on: ubuntu-latest
+    if: contains(github.event.label.name, 'full-ci')
+    steps:
+    - run: |
+        # Finding latest CI workflow run on current pull request
+        # (unfortunately cannot search by PR number, only base branch,
+        # and that is't even unique given PRs from forks, but the risk
+        # of confusion is low and the danger is mild)
+        run_id=$(gh run list -e pull_request -b "$head_ref" --workflow 'CI' --limit 1 \
+          --limit 1 --json databaseId --jq '.[0].databaseId')
+        echo "Run id: ${run_id}"
+        gh run view "$run_id"
+        echo "Cancelling (just in case)"
+        gh run cancel "$run_id" || echo "(failed)"
+        echo "Waiting for 10s"
+        sleep 10
+        echo "Rerunning"
+        gh run rerun "$run_id"
+      shell: bash
+      env:
+        head_ref: ${{ github.head_ref }}
+        GH_TOKEN: ${{ github.token }}
+        GH_REPO: ${{ github.repository }}

README.md

@@ -22,4 +22,4 @@ Please read our [Contribution Guidelines](CONTRIBUTING.md) first.
 
 # Building from Source
 
-See [Building Lean](https://lean-lang.org/lean4/doc/make/index.html).
+See [Building Lean](https://lean-lang.org/lean4/doc/make/index.html) (documentation source: [doc/make/index.md](doc/make/index.md)).

RELEASES.md

@@ -8,7 +8,33 @@ This file contains work-in-progress notes for the upcoming release, as well as p
 Please check the [releases](https://github.com/leanprover/lean4/releases) page for the current status
 of each version.
 
-v4.8.0 (development in progress)
+v4.9.0 (development in progress)
+---------
+
+* Functions defined by well-founded recursion are now marked as
+  `@[irreducible]`, which should prevent expensive and often unfruitful
+  unfolding of such definitions.
+
+  Existing proofs that hold by definitional equality (e.g. `rfl`) can be
+  rewritten to explictly unfold the function definition (using `simp`,
+  `unfold`, `rw`), or the recursive function can be temporariliy made
+  semireducible (using `unseal f in` before the command) or the function
+  definition itself can be marked as `@[semireducible]` to get the previous
+  behavor.
+
+* The `MessageData.ofPPFormat` constructor has been removed.
+  Its functionality has been split into two:
+
+  - for lazy structured messages, please use `MessageData.lazy`;
+  - for embedding `Format` or `FormatWithInfos`, use `MessageData.ofFormatWithInfos`.
+
+  An example migration can be found in [#3929](https://github.com/leanprover/lean4/pull/3929/files#diff-5910592ab7452a0e1b2616c62d22202d2291a9ebb463145f198685aed6299867L109).
+
+* The `MessageData.ofFormat` constructor has been turned into a function.
+  If you need to inspect `MessageData`,
+  you can pattern-match on `MessageData.ofFormatWithInfos`.
+
+v4.8.0
 ---------
 
 * **Executables configured with `supportInterpreter := true` on Windows should now be run via `lake exe` to function properly.**
@@ -85,6 +111,8 @@ v4.8.0 (development in progress)
   [#3798](https://github.com/leanprover/lean4/pull/3798) and
   [#3978](https://github.com/leanprover/lean4/pull/3978).
 
+* Hovers for terms in `match` expressions in the Infoview now reliably show the correct term.
+
 * Added `@[induction_eliminator]` and `@[cases_eliminator]` attributes to be able to define custom eliminators
   for the `induction` and `cases` tactics, replacing the `@[eliminator]` attribute.
   Gives custom eliminators for `Nat` so that `induction` and `cases` put goal states into terms of `0` and `n + 1`

doc/BoolExpr.lean

@@ -1,4 +1,4 @@
-open Std
+open Batteries
 open Lean
 
 inductive BoolExpr where

doc/dev/bootstrap.md

@@ -84,10 +84,12 @@ gh workflow run update-stage0.yml
 Leaving stage0 updates to the CI automation is preferable, but should you need
 to do it locally, you can use `make update-stage0-commit` in `build/release` to
 update `stage0` from `stage1` or `make -C stageN update-stage0-commit` to
-update from another stage.
+update from another stage. This command will automatically stage the updated files
+and introduce a commit,so make sure to commit your work before that.
 
-This command will automatically stage the updated files and introduce a commit,
-so make sure to commit your work before that.
+If you rebased the branch (either onto a newer version of `master`, or fixing
+up some commits prior to the stage0 update, recreate the stage0 update commits.
+The script `script/rebase-stage0.sh` can be used for that.
 
 The CI should prevent PRs with changes to stage0 (besides `stdlib_flags.h`)
 from entering `master` through the (squashing!) merge queue, and label such PRs
@@ -95,6 +97,7 @@ with the `changes-stage0` label. Such PRs should have a cleaned up history,
 with separate stage0 update commits; then coordinate with the admins to merge
 your PR using rebase merge, bypassing the merge queue.
 
+
 ## Further Bootstrapping Complications
 
 As written above, changes in meta code in the current stage usually will only

doc/dev/ffi.md

@@ -53,10 +53,59 @@ In the case of `@[extern]` all *irrelevant* types are removed first; see next se
   Its runtime value is either a pointer to an opaque bignum object or, if the lowest bit of the "pointer" is 1 (`lean_is_scalar`), an encoded unboxed natural number (`lean_box`/`lean_unbox`).
 * A universe `Sort u`, type constructor `... → Sort u`, or proposition `p : Prop` is *irrelevant* and is either statically erased (see above) or represented as a `lean_object *` with the runtime value `lean_box(0)`
 * Any other type is represented by `lean_object *`.
-  Its runtime value is a pointer to an object of a subtype of `lean_object` (see respective declarations in `lean.h`) or the unboxed value `lean_box(cidx)` for the `cidx`th constructor of an inductive type if this constructor does not have any relevant parameters.
+  Its runtime value is a pointer to an object of a subtype of `lean_object` (see the "Inductive types" section below) or the unboxed value `lean_box(cidx)` for the `cidx`th constructor of an inductive type if this constructor does not have any relevant parameters.
 
   Example: the runtime value of `u : Unit` is always `lean_box(0)`.
 
+#### Inductive types
+
+For inductive types which are in the fallback `lean_object *` case above and not trivial constructors, the type is stored as a `lean_ctor_object`, and `lean_is_ctor` will return true. A `lean_ctor_object` stores the constructor index in the header, and the fields are stored in the `m_objs` portion of the object.
+
+The memory order of the fields is derived from the types and order of the fields in the declaration. They are ordered as follows:
+
+* Non-scalar fields stored as `lean_object *`
+* Fields of type `USize`
+* Other scalar fields, in decreasing order by size
+
+Within each group the fields are ordered in declaration order. **Warning**: Trivial wrapper types still count toward a field being treated as non-scalar for this purpose.
+
+* To access fields of the first kind, use `lean_ctor_get(val, i)` to get the `i`th non-scalar field.
+* To access `USize` fields, use `lean_ctor_get_usize(val, n+i)` to get the `i`th usize field and `n` is the total number of fields of the first kind.
+* To access other scalar fields, use `lean_ctor_get_uintN(val, off)` or `lean_ctor_get_usize(val, off)` as appropriate. Here `off` is the byte offset of the field in the structure, starting at `n*sizeof(void*)` where `n` is the number of fields of the first two kinds.
+
+For example, a structure such as
+```lean
+structure S where
+  ptr_1 : Array Nat
+  usize_1 : USize
+  sc64_1 : UInt64
+  ptr_2 : { x : UInt64 // x > 0 } -- wrappers don't count as scalars
+  sc64_2 : Float -- `Float` is 64 bit
+  sc8_1 : Bool
+  sc16_1 : UInt16
+  sc8_2 : UInt8
+  sc64_3 : UInt64
+  usize_2 : USize
+  ptr_3 : Char -- trivial wrapper around `UInt32`
+  sc32_1 : UInt32
+  sc16_2 : UInt16
+```
+would get re-sorted into the following memory order:
+
+* `S.ptr_1` - `lean_ctor_get(val, 0)`
+* `S.ptr_2` - `lean_ctor_get(val, 1)`
+* `S.ptr_3` - `lean_ctor_get(val, 2)`
+* `S.usize_1` - `lean_ctor_get_usize(val, 3)`
+* `S.usize_2` - `lean_ctor_get_usize(val, 4)`
+* `S.sc64_1` - `lean_ctor_get_uint64(val, sizeof(void*)*5)`
+* `S.sc64_2` - `lean_ctor_get_float(val, sizeof(void*)*5 + 8)`
+* `S.sc64_3` - `lean_ctor_get_uint64(val, sizeof(void*)*5 + 16)`
+* `S.sc32_1` - `lean_ctor_get_uint32(val, sizeof(void*)*5 + 24)`
+* `S.sc16_1` - `lean_ctor_get_uint16(val, sizeof(void*)*5 + 28)`
+* `S.sc16_2` - `lean_ctor_get_uint16(val, sizeof(void*)*5 + 30)`
+* `S.sc8_1` - `lean_ctor_get_uint8(val, sizeof(void*)*5 + 32)`
+* `S.sc8_2` - `lean_ctor_get_uint8(val, sizeof(void*)*5 + 33)`
+
 ### Borrowing
 
 By default, all `lean_object *` parameters of an `@[extern]` function are considered *owned*, i.e. the external code is passed a "virtual RC token" and is responsible for passing this token along to another consuming function (exactly once) or freeing it via `lean_dec`.

doc/dev/release_checklist.md

@@ -50,13 +50,13 @@ We'll use `v4.6.0` as the intended release version as a running example.
       - Toolchain bump PR
       - Create and push the tag
       - Merge the tag into `stable`
-    - [Std](https://github.com/leanprover-community/std4)
+    - [Batteries](https://github.com/leanprover-community/batteries)
       - No dependencies
       - Toolchain bump PR
       - Create and push the tag
       - Merge the tag into `stable`
     - [ProofWidgets4](https://github.com/leanprover-community/ProofWidgets4)
-      - Dependencies: `Std`
+      - Dependencies: `Batteries`
       - Note on versions and branches:
         - `ProofWidgets` uses a sequential version tagging scheme, e.g. `v0.0.29`,
           which does not refer to the toolchain being used.
@@ -65,7 +65,7 @@ We'll use `v4.6.0` as the intended release version as a running example.
       - Toolchain bump PR
       - Create and push the tag, following the version convention of the repository
     - [Aesop](https://github.com/leanprover-community/aesop)
-      - Dependencies: `Std`
+      - Dependencies: `Batteries`
       - Toolchain bump PR including updated Lake manifest
       - Create and push the tag
       - Merge the tag into `stable`
@@ -79,7 +79,7 @@ We'll use `v4.6.0` as the intended release version as a running example.
       - Create and push the tag
       - There is no `stable` branch; skip this step
     - [Mathlib](https://github.com/leanprover-community/mathlib4)
-      - Dependencies: `Aesop`, `ProofWidgets4`, `lean4checker`, `Std`, `doc-gen4`, `import-graph`
+      - Dependencies: `Aesop`, `ProofWidgets4`, `lean4checker`, `Batteries`, `doc-gen4`, `import-graph`
       - Toolchain bump PR notes:
         - In addition to updating the `lean-toolchain` and `lakefile.lean`,
           in `.github/workflows/build.yml.in` in the `lean4checker` section update the line
@@ -123,8 +123,8 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
 
 - Decide which nightly release you want to turn into a release candidate.
   We will use `nightly-2024-02-29` in this example.
-- It is essential that Std and Mathlib already have reviewed branches compatible with this nightly.
-  - Check that both Std and Mathlib's `bump/v4.7.0` branch contain `nightly-2024-02-29`
+- It is essential that Batteries and Mathlib already have reviewed branches compatible with this nightly.
+  - Check that both Batteries and Mathlib's `bump/v4.7.0` branch contain `nightly-2024-02-29`
     in their `lean-toolchain`.
   - The steps required to reach that state are beyond the scope of this checklist, but see below!
 - Create the release branch from this nightly tag:
@@ -182,7 +182,7 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
   - We do this for the same list of repositories as for stable releases, see above.
     As above, there are dependencies between these, and so the process above is iterative.
     It greatly helps if you can merge the `bump/v4.7.0` PRs yourself!
-  - For Std/Aesop/Mathlib, which maintain a `nightly-testing` branch, make sure there is a tag
+  - For Batteries/Aesop/Mathlib, which maintain a `nightly-testing` branch, make sure there is a tag
     `nightly-testing-2024-02-29` with date corresponding to the nightly used for the release
     (create it if not), and then on the `nightly-testing` branch `git reset --hard master`, and force push.
 - Make an announcement!
@@ -204,7 +204,7 @@ In particular, updating the downstream repositories is significantly more work
 # Preparing `bump/v4.7.0` branches
 
 While not part of the release process per se,
-this is a brief summary of the work that goes into updating Std/Aesop/Mathlib to new versions.
+this is a brief summary of the work that goes into updating Batteries/Aesop/Mathlib to new versions.
 
 Please read https://leanprover-community.github.io/contribute/tags_and_branches.html
 

doc/monads/states.lean

@@ -15,7 +15,7 @@ data type containing several important pieces of information. First and foremost
 current player, and it has a random generator.
 -/
 
-open Std (HashMap)
+open Batteries (HashMap)
 abbrev TileIndex := Nat × Nat -- a 2D index
 
 inductive TileState where

nix/bootstrap.nix

@@ -180,7 +180,7 @@ rec {
       update-stage0 =
         let cTree = symlinkJoin { name = "cs"; paths = [ Init.cTree Lean.cTree ]; }; in
         writeShellScriptBin "update-stage0" ''
-          CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/update-stage0"}
+          CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/lib/update-stage0"}
         '';
       update-stage0-commit = writeShellScriptBin "update-stage0-commit" ''
         set -euo pipefail

script/lib/README.md

@@ -0,0 +1,2 @@
+This directory contains various scripts that are *not* meant to be called
+directly, but through other scripts or makefiles.

script/lib/rebase-editor.sh

@@ -0,0 +1,19 @@
+#!/usr/bin/env bash
+
+
+# Script internal to `./script/rebase-stage0.sh`
+
+# Determine OS type for sed in-place editing
+SED_CMD=("sed" "-i")
+if [[ "$OSTYPE" == "darwin"* ]]
+then
+    # macOS requires an empty string argument with -i for in-place editing
+    SED_CMD=("sed" "-i" "")
+fi
+
+if [ "$STAGE0_WITH_NIX" = true ]
+then
+  "${SED_CMD[@]}" '/chore: update stage0/ s,.*,x nix run .#update-stage0-commit,' "$1"
+else
+  "${SED_CMD[@]}" '/chore: update stage0/ s,.*,x make -j32 -C build/release update-stage0 \&\& git commit -m "chore: update stage0",' "$1"
+fi

script/rebase-stage0.sh

@@ -0,0 +1,24 @@
+#!/usr/bin/env bash
+
+# This script rebases onto the given branch/commit, and updates
+# all `chore: update stage0` commits along the way.
+
+# Whether to use nix or make to update stage0
+if [ "$1" = "-nix" ]
+then
+   export STAGE0_WITH_NIX=true
+   shift
+fi
+
+# Check if an argument is provided
+if [ "$#" -eq 0 ]; then
+    echo "Usage: $0 [-nix] <options to git rebase -i>"
+    exit 1
+fi
+
+REPO_ROOT=$(git rev-parse --show-toplevel)
+
+# Run git rebase in interactive mode, but automatically edit the todo list
+# using the defined GIT_SEQUENCE_EDITOR command
+GIT_SEQUENCE_EDITOR="$REPO_ROOT/script/lib/rebase-editor.sh" git rebase -i "$@"
+

src/CMakeLists.txt

@@ -9,7 +9,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 8)
+set(LEAN_VERSION_MINOR 9)
 set(LEAN_VERSION_PATCH 0)
 set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
@@ -315,6 +315,12 @@ endif()
 string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
 string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
 
+# in local builds, link executables and not just dynlibs against C++ stdlib as well,
+# which is required for e.g. asan
+if(NOT LEAN_STANDALONE)
+  string(APPEND CMAKE_EXE_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
+endif()
+
 # flags for user binaries = flags for toolchain binaries + Lake
 string(APPEND LEANC_STATIC_LINKER_FLAGS " ${TOOLCHAIN_STATIC_LINKER_FLAGS} -lLake")
 
@@ -585,7 +591,7 @@ endif()
 
 if(PREV_STAGE)
   add_custom_target(update-stage0
-    COMMAND bash -c 'CSRCS=${CMAKE_BINARY_DIR}/lib/temp script/update-stage0'
+    COMMAND bash -c 'CSRCS=${CMAKE_BINARY_DIR}/lib/temp script/lib/update-stage0'
     DEPENDS make_stdlib
     WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/..")
 

src/Init.lean

@@ -34,3 +34,4 @@ import Init.BinderPredicates
 import Init.Ext
 import Init.Omega
 import Init.MacroTrace
+import Init.Grind

src/Init/ByCases.lean

@@ -63,3 +63,16 @@ theorem ite_some_none_eq_none [Decidable P] :
 @[simp] theorem ite_some_none_eq_some [Decidable P] :
     (if P then some x else none) = some y ↔ P ∧ x = y := by
   split <;> simp_all
+
+-- This is not marked as `simp` as it is already handled by `dite_eq_right_iff`.
+theorem dite_some_none_eq_none [Decidable P] {x : P → α} :
+    (if h : P then some (x h) else none) = none ↔ ¬P := by
+  simp only [dite_eq_right_iff]
+  rfl
+
+@[simp] theorem dite_some_none_eq_some [Decidable P] {x : P → α} {y : α} :
+    (if h : P then some (x h) else none) = some y ↔ ∃ h : P, x h = y := by
+  by_cases h : P <;> simp only [h, dite_cond_eq_true, dite_cond_eq_false, Option.some.injEq,
+    false_iff, not_exists]
+  case pos => exact ⟨fun h_eq ↦ Exists.intro h h_eq, fun h_exists => h_exists.2⟩
+  case neg => exact fun h_false _ ↦ h_false

src/Init/Core.lean

@@ -1114,9 +1114,6 @@ theorem eta (a : {x // p x}) (h : p (val a)) : mk (val a) h = a := by
   cases a
   exact rfl
 
-instance {α : Type u} {p : α → Prop} {a : α} (h : p a) : Inhabited {x // p x} where
-  default := ⟨a, h⟩
-
 instance {α : Type u} {p : α → Prop} [DecidableEq α] : DecidableEq {x : α // p x} :=
   fun ⟨a, h₁⟩ ⟨b, h₂⟩ =>
     if h : a = b then isTrue (by subst h; exact rfl)

src/Init/Data/Array/Basic.lean

@@ -31,6 +31,7 @@ def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
   go (i : Nat) (acc : Array α) : Array α :=
     if h : i < n then go (i+1) (acc.push (f ⟨i, h⟩)) else acc
 termination_by n - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 /-- The array `#[0, 1, ..., n - 1]`. -/
 def range (n : Nat) : Array Nat :=
@@ -43,7 +44,7 @@ instance : EmptyCollection (Array α) := ⟨Array.empty⟩
 instance : Inhabited (Array α) where
   default := Array.empty
 
-def isEmpty (a : Array α) : Bool :=
+@[simp] def isEmpty (a : Array α) : Bool :=
   a.size = 0
 
 def singleton (v : α) : Array α :=
@@ -52,7 +53,7 @@ def singleton (v : α) : Array α :=
 /-- Low-level version of `fget` which is as fast as a C array read.
    `Fin` values are represented as tag pointers in the Lean runtime. Thus,
    `fget` may be slightly slower than `uget`. -/
-@[extern "lean_array_uget"]
+@[extern "lean_array_uget", simp]
 def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
   a[i.toNat]
 
@@ -306,6 +307,7 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
     else
       pure r
   termination_by as.size - i
+  decreasing_by simp_wf; decreasing_trivial_pre_omega
   map 0 (mkEmpty as.size)
 
 @[inline]
@@ -378,6 +380,7 @@ def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as :
       else
         pure false
       termination_by stop - j
+      decreasing_by simp_wf; decreasing_trivial_pre_omega
     loop start
   if h : stop ≤ as.size then
     any stop h
@@ -463,6 +466,7 @@ def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
       if p as[j] then some j else loop (j + 1)
     else none
     termination_by as.size - j
+    decreasing_by simp_wf; decreasing_trivial_pre_omega
   loop 0
 
 def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
@@ -557,6 +561,7 @@ def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) (
   else
     true
 termination_by a.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 @[inline] def isEqv (a b : Array α) (p : α → α → Bool) : Bool :=
   if h : a.size = b.size then
@@ -661,6 +666,7 @@ def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size)
     else indexOfAux a v (i+1)
   else none
 termination_by a.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
   indexOfAux a v 0
@@ -703,6 +709,7 @@ def popWhile (p : α → Bool) (as : Array α) : Array α :=
   else
     as
 termination_by as.size
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def takeWhile (p : α → Bool) (as : Array α) : Array α :=
   let rec go (i : Nat) (r : Array α) : Array α :=
@@ -715,6 +722,7 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
     else
       r
     termination_by as.size - i
+    decreasing_by simp_wf; decreasing_trivial_pre_omega
   go 0 #[]
 
 /-- Remove the element at a given index from an array without bounds checks, using a `Fin` index.
@@ -725,16 +733,15 @@ def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
   if h : i.val + 1 < a.size then
     let a' := a.swap ⟨i.val + 1, h⟩ i
     let i' : Fin a'.size := ⟨i.val + 1, by simp [a', h]⟩
-    have : a'.size - i' < a.size - i := by
-      simp [a', Nat.sub_succ_lt_self _ _ i.isLt]
     a'.feraseIdx i'
   else
     a.pop
 termination_by a.size - i.val
+decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ i.isLt
 
 theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
   induction a, i using Array.feraseIdx.induct with
-  | @case1 a i h a' _ _ ih =>
+  | @case1 a i h a' _ ih =>
     unfold feraseIdx
     simp [h, a', ih]
   | case2 a i h =>
@@ -763,6 +770,7 @@ def erase [BEq α] (as : Array α) (a : α) : Array α :=
     else
       as
     termination_by j.1
+    decreasing_by simp_wf; decreasing_trivial_pre_omega
   let j := as.size
   let as := as.push a
   loop as ⟨j, size_push .. ▸ j.lt_succ_self⟩
@@ -816,6 +824,7 @@ def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : N
   else
     true
 termination_by as.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 /-- Return true iff `as` is a prefix of `bs`.
 That is, `bs = as ++ t` for some `t : List α`.-/
@@ -837,6 +846,7 @@ private def allDiffAux [BEq α] (as : Array α) (i : Nat) : Bool :=
   else
     true
 termination_by as.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def allDiff [BEq α] (as : Array α) : Bool :=
   allDiffAux as 0
@@ -852,6 +862,7 @@ def allDiff [BEq α] (as : Array α) : Bool :=
   else
     cs
 termination_by as.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 @[inline] def zipWith (as : Array α) (bs : Array β) (f : α → β → γ) : Array γ :=
   zipWithAux f as bs 0 #[]

src/Init/Data/Array/BasicAux.lean

@@ -48,6 +48,7 @@ where
       let b ← f as[i]
       go (i+1) ⟨acc.val.push b, by simp [acc.property]⟩ hlt
   termination_by as.size - i
+  decreasing_by decreasing_trivial_pre_omega
 
 @[inline] private unsafe def mapMonoMImp [Monad m] (as : Array α) (f : α → m α) : m (Array α) :=
   go 0 as

src/Init/Data/Array/DecidableEq.lean

@@ -21,6 +21,8 @@ theorem eq_of_isEqvAux [DecidableEq α] (a b : Array α) (hsz : a.size = b.size)
     subst heq
     exact absurd (Nat.lt_of_lt_of_le high low) (Nat.lt_irrefl j)
 termination_by a.size - i
+decreasing_by decreasing_trivial_pre_omega
+
 
 theorem eq_of_isEqv [DecidableEq α] (a b : Array α) : Array.isEqv a b (fun x y => x = y) → a = b := by
   simp [Array.isEqv]
@@ -37,6 +39,7 @@ theorem isEqvAux_self [DecidableEq α] (a : Array α) (i : Nat) : Array.isEqvAux
   case inl h => simp [h, isEqvAux_self a (i+1)]
   case inr h => simp [h]
 termination_by a.size - i
+decreasing_by decreasing_trivial_pre_omega
 
 theorem isEqv_self [DecidableEq α] (a : Array α) : Array.isEqv a a (fun x y => x = y) = true := by
   simp [isEqv, isEqvAux_self]

src/Init/Data/Array/Lemmas.lean

@@ -21,6 +21,13 @@ namespace Array
 
 attribute [simp] data_toArray uset
 
+@[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
+
+@[simp] theorem toArray_data : (a : Array α) → a.data.toArray = a
+  | ⟨l⟩ => ext' (data_toArray l)
+
+@[simp] theorem data_length {l : Array α} : l.data.length = l.size := rfl
+
 @[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl
 
 @[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
@@ -131,6 +138,7 @@ where
       simp [aux (i+1), map_eq_pure_bind]; rfl
     · rw [List.drop_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
   termination_by arr.size - i
+  decreasing_by decreasing_trivial_pre_omega
 
 @[simp] theorem map_data (f : α → β) (arr : Array α) : (arr.map f).data = arr.data.map f := by
   rw [map, mapM_eq_foldlM]
@@ -140,7 +148,8 @@ where
   simp [H]
 
 @[simp] theorem size_map (f : α → β) (arr : Array α) : (arr.map f).size = arr.size := by
-  simp [size]
+  simp only [← data_length]
+  simp
 
 @[simp] theorem pop_data (arr : Array α) : arr.pop.data = arr.data.dropLast := rfl
 
@@ -307,5 +316,749 @@ termination_by n - i
     (ofFn f)[i] = f ⟨i, size_ofFn f ▸ h⟩ :=
   getElem_ofFn_go _ _ _ (by simp) (by simp) nofun
 
+/-- # mkArray -/
+
+@[simp] theorem mkArray_data (n : Nat) (v : α) : (mkArray n v).data = List.replicate n v := rfl
+
+@[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
+    (mkArray n v)[i] = v := by simp [Array.getElem_eq_data_get]
+
+/-- # mem -/
+
+theorem mem_data {a : α} {l : Array α} : a ∈ l.data ↔ a ∈ l := (mem_def _ _).symm
+
+theorem not_mem_nil (a : α) : ¬ a ∈ #[] := nofun
+
+/-- # get lemmas -/
+
+theorem getElem?_mem {l : Array α} {i : Fin l.size} : l[i] ∈ l := by
+  erw [Array.mem_def, getElem_eq_data_get]
+  apply List.get_mem
+
+theorem getElem_fin_eq_data_get (a : Array α) (i : Fin _) : a[i] = a.data.get i := rfl
+
+@[simp] theorem ugetElem_eq_getElem (a : Array α) {i : USize} (h : i.toNat < a.size) :
+  a[i] = a[i.toNat] := rfl
+
+theorem getElem?_eq_getElem (a : Array α) (i : Nat) (h : i < a.size) : a[i]? = a[i] :=
+  getElem?_pos ..
+
+theorem get?_len_le (a : Array α) (i : Nat) (h : a.size ≤ i) : a[i]? = none := by
+  simp [getElem?_neg, h]
+
+theorem getElem_mem_data (a : Array α) (h : i < a.size) : a[i] ∈ a.data := by
+  simp only [getElem_eq_data_get, List.get_mem]
+
+theorem getElem?_eq_data_get? (a : Array α) (i : Nat) : a[i]? = a.data.get? i := by
+  by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg, List.get?_eq_get, eq_comm]; rfl
+
+theorem get?_eq_data_get? (a : Array α) (i : Nat) : a.get? i = a.data.get? i :=
+  getElem?_eq_data_get? ..
+
+theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD default := by
+  simp [get!_eq_getD]
+
+@[simp] theorem back_eq_back? [Inhabited α] (a : Array α) : a.back = a.back?.getD default := by
+  simp [back, back?]
+
+@[simp] theorem back?_push (a : Array α) : (a.push x).back? = some x := by
+  simp [back?, getElem?_eq_data_get?]
+
+theorem back_push [Inhabited α] (a : Array α) : (a.push x).back = x := by simp
+
+theorem get?_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
+    (a.push x)[i]? = some a[i] := by
+  rw [getElem?_pos, get_push_lt]
+
+theorem get?_push_eq (a : Array α) (x : α) : (a.push x)[a.size]? = some x := by
+  rw [getElem?_pos, get_push_eq]
+
+theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x else a[i]? := by
+  match Nat.lt_trichotomy i a.size with
+  | Or.inl g =>
+    have h1 : i < a.size + 1 := by omega
+    have h2 : i ≠ a.size := by omega
+    simp [getElem?, size_push, g, h1, h2, get_push_lt]
+  | Or.inr (Or.inl heq) =>
+    simp [heq, getElem?_pos, get_push_eq]
+  | Or.inr (Or.inr g) =>
+    simp only [getElem?, size_push]
+    have h1 : ¬ (i < a.size) := by omega
+    have h2 : ¬ (i < a.size + 1) := by omega
+    have h3 : i ≠ a.size := by omega
+    simp [h1, h2, h3]
+
+@[simp] theorem get?_size {a : Array α} : a[a.size]? = none := by
+  simp only [getElem?, Nat.lt_irrefl, dite_false]
+
+@[simp] theorem data_set (a : Array α) (i v) : (a.set i v).data = a.data.set i.1 v := rfl
+
+theorem get_set_eq (a : Array α) (i : Fin a.size) (v : α) :
+    (a.set i v)[i.1] = v := by
+  simp only [set, getElem_eq_data_get, List.get_set_eq]
+
+theorem get?_set_eq (a : Array α) (i : Fin a.size) (v : α) :
+    (a.set i v)[i.1]? = v := by simp [getElem?_pos, i.2]
+
+@[simp] theorem get?_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α)
+    (h : i.1 ≠ j) : (a.set i v)[j]? = a[j]? := by
+  by_cases j < a.size <;> simp [getElem?_pos, getElem?_neg, *]
+
+theorem get?_set (a : Array α) (i : Fin a.size) (j : Nat) (v : α) :
+    (a.set i v)[j]? = if i.1 = j then some v else a[j]? := by
+  if h : i.1 = j then subst j; simp [*] else simp [*]
+
+theorem get_set (a : Array α) (i : Fin a.size) (j : Nat) (hj : j < a.size) (v : α) :
+    (a.set i v)[j]'(by simp [*]) = if i = j then v else a[j] := by
+  if h : i.1 = j then subst j; simp [*] else simp [*]
+
+@[simp] theorem get_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α) (hj : j < a.size)
+    (h : i.1 ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
+  simp only [set, getElem_eq_data_get, List.get_set_ne _ h]
+
+theorem getElem_setD (a : Array α) (i : Nat) (v : α) (h : i < (setD a i v).size) :
+  (setD a i v)[i] = v := by
+  simp at h
+  simp only [setD, h, dite_true, get_set, ite_true]
+
+theorem set_set (a : Array α) (i : Fin a.size) (v v' : α) :
+    (a.set i v).set ⟨i, by simp [i.2]⟩ v' = a.set i v' := by simp [set, List.set_set]
+
+private theorem fin_cast_val (e : n = n') (i : Fin n) : e ▸ i = ⟨i.1, e ▸ i.2⟩ := by cases e; rfl
+
+theorem swap_def (a : Array α) (i j : Fin a.size) :
+    a.swap i j = (a.set i (a.get j)).set ⟨j.1, by simp [j.2]⟩ (a.get i) := by
+  simp [swap, fin_cast_val]
+
+theorem data_swap (a : Array α) (i j : Fin a.size) :
+    (a.swap i j).data = (a.data.set i (a.get j)).set j (a.get i) := by simp [swap_def]
+
+theorem get?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)[k]? =
+    if j = k then some a[i.1] else if i = k then some a[j.1] else a[k]? := by
+  simp [swap_def, get?_set, ← getElem_fin_eq_data_get]
+
+@[simp] theorem swapAt_def (a : Array α) (i : Fin a.size) (v : α) :
+    a.swapAt i v = (a[i.1], a.set i v) := rfl
+
+-- @[simp] -- FIXME: gives a weird linter error
+theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
+    a.swapAt! i v = (a[i], a.set ⟨i, h⟩ v) := by simp [swapAt!, h]
+
+@[simp] theorem data_pop (a : Array α) : a.pop.data = a.data.dropLast := by simp [pop]
+
+@[simp] theorem pop_empty : (#[] : Array α).pop = #[] := rfl
+
+@[simp] theorem pop_push (a : Array α) : (a.push x).pop = a := by simp [pop]
+
+@[simp] theorem getElem_pop (a : Array α) (i : Nat) (hi : i < a.pop.size) :
+    a.pop[i] = a[i]'(Nat.lt_of_lt_of_le (a.size_pop ▸ hi) (Nat.sub_le _ _)) :=
+  List.get_dropLast ..
+
+theorem eq_empty_of_size_eq_zero {as : Array α} (h : as.size = 0) : as = #[] := by
+  apply ext
+  · simp [h]
+  · intros; contradiction
+
+theorem eq_push_pop_back_of_size_ne_zero [Inhabited α] {as : Array α} (h : as.size ≠ 0) :
+    as = as.pop.push as.back := by
+  apply ext
+  · simp [Nat.sub_add_cancel (Nat.zero_lt_of_ne_zero h)]
+  · intros i h h'
+    if hlt : i < as.pop.size then
+      rw [get_push_lt (h:=hlt), getElem_pop]
+    else
+      have heq : i = as.pop.size :=
+        Nat.le_antisymm (size_pop .. ▸ Nat.le_pred_of_lt h) (Nat.le_of_not_gt hlt)
+      cases heq; rw [get_push_eq, back, ←size_pop, get!_eq_getD, getD, dif_pos h]; rfl
+
+theorem eq_push_of_size_ne_zero {as : Array α} (h : as.size ≠ 0) :
+    ∃ (bs : Array α) (c : α), as = bs.push c :=
+  let _ : Inhabited α := ⟨as[0]⟩
+  ⟨as.pop, as.back, eq_push_pop_back_of_size_ne_zero h⟩
+
+theorem size_eq_length_data (as : Array α) : as.size = as.data.length := rfl
+
+@[simp] theorem size_swap! (a : Array α) (i j) :
+    (a.swap! i j).size = a.size := by unfold swap!; split <;> (try split) <;> simp [size_swap]
+
+@[simp] theorem size_reverse (a : Array α) : a.reverse.size = a.size := by
+  let rec go (as : Array α) (i j) : (reverse.loop as i j).size = as.size := by
+    rw [reverse.loop]
+    if h : i < j then
+      have := reverse.termination h
+      simp [(go · (i+1) ⟨j-1, ·⟩), h]
+    else simp [h]
+    termination_by j - i
+  simp only [reverse]; split <;> simp [go]
+
+@[simp] theorem size_range {n : Nat} : (range n).size = n := by
+  unfold range
+  induction n with
+  | zero      => simp [Nat.fold]
+  | succ k ih =>
+    rw [Nat.fold, flip]
+    simp only [mkEmpty_eq, size_push] at *
+    omega
+
+@[simp] theorem reverse_data (a : Array α) : a.reverse.data = a.data.reverse := by
+  let rec go (as : Array α) (i j hj)
+      (h : i + j + 1 = a.size) (h₂ : as.size = a.size)
+      (H : ∀ k, as.data.get? k = if i ≤ k ∧ k ≤ j then a.data.get? k else a.data.reverse.get? k)
+      (k) : (reverse.loop as i ⟨j, hj⟩).data.get? k = a.data.reverse.get? k := by
+    rw [reverse.loop]; dsimp; split <;> rename_i h₁
+    · have := reverse.termination h₁
+      match j with | j+1 => ?_
+      simp at *
+      rw [(go · (i+1) j)]
+      · rwa [Nat.add_right_comm i]
+      · simp [size_swap, h₂]
+      · intro k
+        rw [← getElem?_eq_data_get?, get?_swap]
+        simp [getElem?_eq_data_get?, getElem_eq_data_get, ← List.get?_eq_get, H, Nat.le_of_lt h₁]
+        split <;> rename_i h₂
+        · simp [← h₂, Nat.not_le.2 (Nat.lt_succ_self _)]
+          exact (List.get?_reverse' _ _ (Eq.trans (by simp_arith) h)).symm
+        split <;> rename_i h₃
+        · simp [← h₃, Nat.not_le.2 (Nat.lt_succ_self _)]
+          exact (List.get?_reverse' _ _ (Eq.trans (by simp_arith) h)).symm
+        simp only [Nat.succ_le, Nat.lt_iff_le_and_ne.trans (and_iff_left h₃),
+          Nat.lt_succ.symm.trans (Nat.lt_iff_le_and_ne.trans (and_iff_left (Ne.symm h₂)))]
+    · rw [H]; split <;> rename_i h₂
+      · cases Nat.le_antisymm (Nat.not_lt.1 h₁) (Nat.le_trans h₂.1 h₂.2)
+        cases Nat.le_antisymm h₂.1 h₂.2
+        exact (List.get?_reverse' _ _ h).symm
+      · rfl
+    termination_by j - i
+  simp only [reverse]; split
+  · match a with | ⟨[]⟩ | ⟨[_]⟩ => rfl
+  · have := Nat.sub_add_cancel (Nat.le_of_not_le ‹_›)
+    refine List.ext <| go _ _ _ _ (by simp [this]) rfl fun k => ?_
+    split; {rfl}; rename_i h
+    simp [← show k < _ + 1 ↔ _ from Nat.lt_succ (n := a.size - 1), this] at h
+    rw [List.get?_eq_none.2 ‹_›, List.get?_eq_none.2 (a.data.length_reverse ▸ ‹_›)]
+
+/-! ### foldl / foldr -/
+
+-- This proof is the pure version of `Array.SatisfiesM_foldlM`,
+-- reproduced to avoid a dependency on `SatisfiesM`.
+theorem foldl_induction
+    {as : Array α} (motive : Nat → β → Prop) {init : β} (h0 : motive 0 init) {f : β → α → β}
+    (hf : ∀ i : Fin as.size, ∀ b, motive i.1 b → motive (i.1 + 1) (f b as[i])) :
+    motive as.size (as.foldl f init) := by
+  let rec go {i j b} (h₁ : j ≤ as.size) (h₂ : as.size ≤ i + j) (H : motive j b) :
+    (motive as.size) (foldlM.loop (m := Id) f as as.size (Nat.le_refl _) i j b) := by
+    unfold foldlM.loop; split
+    · next hj =>
+      split
+      · cases Nat.not_le_of_gt (by simp [hj]) h₂
+      · exact go hj (by rwa [Nat.succ_add] at h₂) (hf ⟨j, hj⟩ b H)
+    · next hj => exact Nat.le_antisymm h₁ (Nat.ge_of_not_lt hj) ▸ H
+  simpa [foldl, foldlM] using go (Nat.zero_le _) (Nat.le_refl _) h0
+
+-- This proof is the pure version of `Array.SatisfiesM_foldrM`,
+-- reproduced to avoid a dependency on `SatisfiesM`.
+theorem foldr_induction
+    {as : Array α} (motive : Nat → β → Prop) {init : β} (h0 : motive as.size init) {f : α → β → β}
+    (hf : ∀ i : Fin as.size, ∀ b, motive (i.1 + 1) b → motive i.1 (f as[i] b)) :
+    motive 0 (as.foldr f init) := by
+  let rec go {i b} (hi : i ≤ as.size) (H : motive i b) :
+    (motive 0) (foldrM.fold (m := Id) f as 0 i hi b) := by
+    unfold foldrM.fold; simp; split
+    · next hi => exact (hi ▸ H)
+    · next hi =>
+      split; {simp at hi}
+      · next i hi' =>
+        exact go _ (hf ⟨i, hi'⟩ b H)
+  simp [foldr, foldrM]; split; {exact go _ h0}
+  · next h => exact (Nat.eq_zero_of_not_pos h ▸ h0)
+
+/-! ### map -/
+
+@[simp] theorem mem_map {f : α → β} {l : Array α} : b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b := by
+  simp only [mem_def, map_data, List.mem_map]
+
+theorem mapM_eq_mapM_data [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
+    arr.mapM f = return mk (← arr.data.mapM f) := by
+  rw [mapM_eq_foldlM, foldlM_eq_foldlM_data, ← List.foldrM_reverse]
+  conv => rhs; rw [← List.reverse_reverse arr.data]
+  induction arr.data.reverse with
+  | nil => simp; rfl
+  | cons a l ih => simp [ih]; simp [map_eq_pure_bind, push]
+
+theorem mapM_map_eq_foldl (as : Array α) (f : α → β) (i) :
+    mapM.map (m := Id) f as i b = as.foldl (start := i) (fun r a => r.push (f a)) b := by
+  unfold mapM.map
+  split <;> rename_i h
+  · simp only [Id.bind_eq]
+    dsimp [foldl, Id.run, foldlM]
+    rw [mapM_map_eq_foldl, dif_pos (by omega), foldlM.loop, dif_pos h]
+    -- Calling `split` here gives a bad goal.
+    have : size as - i = Nat.succ (size as - i - 1) := by omega
+    rw [this]
+    simp [foldl, foldlM, Id.run, Nat.sub_add_eq]
+  · dsimp [foldl, Id.run, foldlM]
+    rw [dif_pos (by omega), foldlM.loop, dif_neg h]
+    rfl
+termination_by as.size - i
+
+theorem map_eq_foldl (as : Array α) (f : α → β) :
+    as.map f = as.foldl (fun r a => r.push (f a)) #[] :=
+  mapM_map_eq_foldl _ _ _
+
+theorem map_induction (as : Array α) (f : α → β) (motive : Nat → Prop) (h0 : motive 0)
+    (p : Fin as.size → β → Prop) (hs : ∀ i, motive i.1 → p i (f as[i]) ∧ motive (i+1)) :
+    motive as.size ∧
+      ∃ eq : (as.map f).size = as.size, ∀ i h, p ⟨i, h⟩ ((as.map f)[i]) := by
+  have t := foldl_induction (as := as) (β := Array β)
+    (motive := fun i arr => motive i ∧ arr.size = i ∧ ∀ i h2, p i arr[i.1])
+    (init := #[]) (f := fun r a => r.push (f a)) ?_ ?_
+  obtain ⟨m, eq, w⟩ := t
+  · refine ⟨m, by simpa [map_eq_foldl] using eq, ?_⟩
+    intro i h
+    simp [eq] at w
+    specialize w ⟨i, h⟩ h
+    simpa [map_eq_foldl] using w
+  · exact ⟨h0, rfl, nofun⟩
+  · intro i b ⟨m, ⟨eq, w⟩⟩
+    refine ⟨?_, ?_, ?_⟩
+    · exact (hs _ m).2
+    · simp_all
+    · intro j h
+      simp at h ⊢
+      by_cases h' : j < size b
+      · rw [get_push]
+        simp_all
+      · rw [get_push, dif_neg h']
+        simp only [show j = i by omega]
+        exact (hs _ m).1
+
+theorem map_spec (as : Array α) (f : α → β) (p : Fin as.size → β → Prop)
+    (hs : ∀ i, p i (f as[i])) :
+    ∃ eq : (as.map f).size = as.size, ∀ i h, p ⟨i, h⟩ ((as.map f)[i]) := by
+  simpa using map_induction as f (fun _ => True) trivial p (by simp_all)
+
+@[simp] theorem getElem_map (f : α → β) (as : Array α) (i : Nat) (h) :
+    ((as.map f)[i]) = f (as[i]'(size_map .. ▸ h)) := by
+  have := map_spec as f (fun i b => b = f (as[i]))
+  simp only [implies_true, true_implies] at this
+  obtain ⟨eq, w⟩ := this
+  apply w
+  simp_all
+
+/-! ### mapIdx -/
+
+-- This could also be prove from `SatisfiesM_mapIdxM`.
+theorem mapIdx_induction (as : Array α) (f : Fin as.size → α → β)
+    (motive : Nat → Prop) (h0 : motive 0)
+    (p : Fin as.size → β → Prop)
+    (hs : ∀ i, motive i.1 → p i (f i as[i]) ∧ motive (i + 1)) :
+    motive as.size ∧ ∃ eq : (Array.mapIdx as f).size = as.size,
+      ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) := by
+  let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : ∀ i h h', p ⟨i, h⟩ bs[i]) (hm : motive j) :
+    let arr : Array β := Array.mapIdxM.map (m := Id) as f i j h bs
+    motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i] := by
+    induction i generalizing j bs with simp [mapIdxM.map]
+    | zero =>
+      have := (Nat.zero_add _).symm.trans h
+      exact ⟨this ▸ hm, h₁ ▸ this, fun _ _ => h₂ ..⟩
+    | succ i ih =>
+      apply @ih (bs.push (f ⟨j, by omega⟩ as[j])) (j + 1) (by omega) (by simp; omega)
+      · intro i i_lt h'
+        rw [get_push]
+        split
+        · apply h₂
+        · simp only [size_push] at h'
+          obtain rfl : i = j := by omega
+          apply (hs ⟨i, by omega⟩ hm).1
+      · exact (hs ⟨j, by omega⟩ hm).2
+  simp [mapIdx, mapIdxM]; exact go rfl nofun h0
+
+theorem mapIdx_spec (as : Array α) (f : Fin as.size → α → β)
+    (p : Fin as.size → β → Prop) (hs : ∀ i, p i (f i as[i])) :
+    ∃ eq : (Array.mapIdx as f).size = as.size,
+      ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) :=
+  (mapIdx_induction _ _ (fun _ => True) trivial p fun _ _ => ⟨hs .., trivial⟩).2
+
+@[simp] theorem size_mapIdx (a : Array α) (f : Fin a.size → α → β) : (a.mapIdx f).size = a.size :=
+  (mapIdx_spec (p := fun _ _ => True) (hs := fun _ => trivial)).1
+
+@[simp] theorem size_zipWithIndex (as : Array α) : as.zipWithIndex.size = as.size :=
+  Array.size_mapIdx _ _
+
+@[simp] theorem getElem_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat)
+    (h : i < (mapIdx a f).size) :
+    haveI : i < a.size := by simp_all
+    (a.mapIdx f)[i] = f ⟨i, this⟩ a[i] :=
+  (mapIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i _
+
+/-! ### modify -/
+
+@[simp] theorem size_modify (a : Array α) (i : Nat) (f : α → α) : (a.modify i f).size = a.size := by
+  unfold modify modifyM Id.run
+  split <;> simp
+
+theorem get_modify {arr : Array α} {x i} (h : i < arr.size) :
+    (arr.modify x f).get ⟨i, by simp [h]⟩ =
+    if x = i then f (arr.get ⟨i, h⟩) else arr.get ⟨i, h⟩ := by
+  simp [modify, modifyM, Id.run]; split
+  · simp [get_set _ _ _ h]; split <;> simp [*]
+  · rw [if_neg (mt (by rintro rfl; exact h) ‹_›)]
+
+/-! ### filter -/
+
+@[simp] theorem filter_data (p : α → Bool) (l : Array α) :
+    (l.filter p).data = l.data.filter p := by
+  dsimp only [filter]
+  rw [foldl_eq_foldl_data]
+  generalize l.data = l
+  suffices ∀ a, (List.foldl (fun r a => if p a = true then push r a else r) a l).data =
+      a.data ++ List.filter p l by
+    simpa using this #[]
+  induction l with simp
+  | cons => split <;> simp [*]
+
+@[simp] theorem filter_filter (q) (l : Array α) :
+    filter p (filter q l) = filter (fun a => p a ∧ q a) l := by
+  apply ext'
+  simp only [filter_data, List.filter_filter]
+
+@[simp] theorem mem_filter : x ∈ filter p as ↔ x ∈ as ∧ p x := by
+  simp only [mem_def, filter_data, List.mem_filter]
+
+theorem mem_of_mem_filter {a : α} {l} (h : a ∈ filter p l) : a ∈ l :=
+  (mem_filter.mp h).1
+
+/-! ### filterMap -/
+
+@[simp] theorem filterMap_data (f : α → Option β) (l : Array α) :
+    (l.filterMap f).data = l.data.filterMap f := by
+  dsimp only [filterMap, filterMapM]
+  rw [foldlM_eq_foldlM_data]
+  generalize l.data = l
+  have this : ∀ a : Array β, (Id.run (List.foldlM (m := Id) ?_ a l)).data =
+    a.data ++ List.filterMap f l := ?_
+  exact this #[]
+  induction l
+  · simp_all [Id.run]
+  · simp_all [Id.run]
+    split <;> simp_all
+
+@[simp] theorem mem_filterMap (f : α → Option β) (l : Array α) {b : β} :
+    b ∈ filterMap f l ↔ ∃ a, a ∈ l ∧ f a = some b := by
+  simp only [mem_def, filterMap_data, List.mem_filterMap]
+
+/-! ### empty -/
+
+theorem size_empty : (#[] : Array α).size = 0 := rfl
+
+theorem empty_data : (#[] : Array α).data = [] := rfl
+
+/-! ### append -/
+
+theorem push_eq_append_singleton (as : Array α) (x) : as.push x = as ++ #[x] := rfl
+
+@[simp] theorem mem_append {a : α} {s t : Array α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t := by
+  simp only [mem_def, append_data, List.mem_append]
+
+theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
+  simp only [size, append_data, List.length_append]
+
+theorem get_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
+    (as ++ bs)[i] = as[i] := by
+  simp only [getElem_eq_data_get]
+  have h' : i < (as.data ++ bs.data).length := by rwa [← data_length, append_data] at h
+  conv => rhs; rw [← List.get_append_left (bs:=bs.data) (h':=h')]
+  apply List.get_of_eq; rw [append_data]
+
+theorem get_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i)
+    (hlt : i - as.size < bs.size := Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) :
+    (as ++ bs)[i] = bs[i - as.size] := by
+  simp only [getElem_eq_data_get]
+  have h' : i < (as.data ++ bs.data).length := by rwa [← data_length, append_data] at h
+  conv => rhs; rw [← List.get_append_right (h':=h') (h:=Nat.not_lt_of_ge hle)]
+  apply List.get_of_eq; rw [append_data]
+
+@[simp] theorem append_nil (as : Array α) : as ++ #[] = as := by
+  apply ext'; simp only [append_data, empty_data, List.append_nil]
+
+@[simp] theorem nil_append (as : Array α) : #[] ++ as = as := by
+  apply ext'; simp only [append_data, empty_data, List.nil_append]
+
+theorem append_assoc (as bs cs : Array α) : as ++ bs ++ cs = as ++ (bs ++ cs) := by
+  apply ext'; simp only [append_data, List.append_assoc]
+
+/-! ### extract -/
+
+theorem extract_loop_zero (as bs : Array α) (start : Nat) : extract.loop as 0 start bs = bs := by
+  rw [extract.loop]; split <;> rfl
+
+theorem extract_loop_succ (as bs : Array α) (size start : Nat) (h : start < as.size) :
+    extract.loop as (size+1) start bs = extract.loop as size (start+1) (bs.push as[start]) := by
+  rw [extract.loop, dif_pos h]; rfl
+
+theorem extract_loop_of_ge (as bs : Array α) (size start : Nat) (h : start ≥ as.size) :
+    extract.loop as size start bs = bs := by
+  rw [extract.loop, dif_neg (Nat.not_lt_of_ge h)]
+
+theorem extract_loop_eq_aux (as bs : Array α) (size start : Nat) :
+    extract.loop as size start bs = bs ++ extract.loop as size start #[] := by
+  induction size using Nat.recAux generalizing start bs with
+  | zero => rw [extract_loop_zero, extract_loop_zero, append_nil]
+  | succ size ih =>
+    if h : start < as.size then
+      rw [extract_loop_succ (h:=h), ih (bs.push _), push_eq_append_singleton]
+      rw [extract_loop_succ (h:=h), ih (#[].push _), push_eq_append_singleton, nil_append]
+      rw [append_assoc]
+    else
+      rw [extract_loop_of_ge (h:=Nat.le_of_not_lt h)]
+      rw [extract_loop_of_ge (h:=Nat.le_of_not_lt h)]
+      rw [append_nil]
+
+theorem extract_loop_eq (as bs : Array α) (size start : Nat) (h : start + size ≤ as.size) :
+  extract.loop as size start bs = bs ++ as.extract start (start + size) := by
+  simp [extract]; rw [extract_loop_eq_aux, Nat.min_eq_left h, Nat.add_sub_cancel_left]
+
+theorem size_extract_loop (as bs : Array α) (size start : Nat) :
+    (extract.loop as size start bs).size = bs.size + min size (as.size - start) := by
+  induction size using Nat.recAux generalizing start bs with
+  | zero => rw [extract_loop_zero, Nat.zero_min, Nat.add_zero]
+  | succ size ih =>
+    if h : start < as.size then
+      rw [extract_loop_succ (h:=h), ih, size_push, Nat.add_assoc, ←Nat.add_min_add_left,
+        Nat.sub_succ, Nat.one_add, Nat.one_add, Nat.succ_pred_eq_of_pos (Nat.sub_pos_of_lt h)]
+    else
+      have h := Nat.le_of_not_gt h
+      rw [extract_loop_of_ge (h:=h), Nat.sub_eq_zero_of_le h, Nat.min_zero, Nat.add_zero]
+
+@[simp] theorem size_extract (as : Array α) (start stop : Nat) :
+    (as.extract start stop).size = min stop as.size - start := by
+  simp [extract]; rw [size_extract_loop, size_empty, Nat.zero_add, Nat.sub_min_sub_right,
+    Nat.min_assoc, Nat.min_self]
+
+theorem get_extract_loop_lt_aux (as bs : Array α) (size start : Nat) (hlt : i < bs.size) :
+    i < (extract.loop as size start bs).size := by
+  rw [size_extract_loop]
+  apply Nat.lt_of_lt_of_le hlt
+  exact Nat.le_add_right ..
+
+theorem get_extract_loop_lt (as bs : Array α) (size start : Nat) (hlt : i < bs.size)
+    (h := get_extract_loop_lt_aux as bs size start hlt) :
+    (extract.loop as size start bs)[i] = bs[i] := by
+  apply Eq.trans _ (get_append_left (bs:=extract.loop as size start #[]) hlt)
+  · rw [size_append]; exact Nat.lt_of_lt_of_le hlt (Nat.le_add_right ..)
+  · congr; rw [extract_loop_eq_aux]
+
+theorem get_extract_loop_ge_aux (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size)
+    (h : i < (extract.loop as size start bs).size) : start + i - bs.size < as.size := by
+  have h : i < bs.size + (as.size - start) := by
+      apply Nat.lt_of_lt_of_le h
+      rw [size_extract_loop]
+      apply Nat.add_le_add_left
+      exact Nat.min_le_right ..
+  rw [Nat.add_sub_assoc hge]
+  apply Nat.add_lt_of_lt_sub'
+  exact Nat.sub_lt_left_of_lt_add hge h
+
+theorem get_extract_loop_ge (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size)
+    (h : i < (extract.loop as size start bs).size)
+    (h' := get_extract_loop_ge_aux as bs size start hge h) :
+    (extract.loop as size start bs)[i] = as[start + i - bs.size] := by
+  induction size using Nat.recAux generalizing start bs with
+  | zero =>
+    rw [size_extract_loop, Nat.zero_min, Nat.add_zero] at h
+    omega
+  | succ size ih =>
+    have : start < as.size := by
+      apply Nat.lt_of_le_of_lt (Nat.le_add_right start (i - bs.size))
+      rwa [← Nat.add_sub_assoc hge]
+    have : i < (extract.loop as size (start+1) (bs.push as[start])).size := by
+      rwa [← extract_loop_succ]
+    have heq : (extract.loop as (size+1) start bs)[i] =
+        (extract.loop as size (start+1) (bs.push as[start]))[i] := by
+      congr 1; rw [extract_loop_succ]
+    rw [heq]
+    if hi : bs.size = i then
+      cases hi
+      have h₁ : bs.size < (bs.push as[start]).size := by rw [size_push]; exact Nat.lt_succ_self ..
+      have h₂ : bs.size < (extract.loop as size (start+1) (bs.push as[start])).size := by
+        rw [size_extract_loop]; apply Nat.lt_of_lt_of_le h₁; exact Nat.le_add_right ..
+      have h : (extract.loop as size (start + 1) (push bs as[start]))[bs.size] = as[start] := by
+        rw [get_extract_loop_lt as (bs.push as[start]) size (start+1) h₁ h₂, get_push_eq]
+      rw [h]; congr; rw [Nat.add_sub_cancel]
+    else
+      have hge : bs.size + 1 ≤ i := Nat.lt_of_le_of_ne hge hi
+      rw [ih (bs.push as[start]) (start+1) ((size_push ..).symm ▸ hge)]
+      congr 1; rw [size_push, Nat.add_right_comm, Nat.add_sub_add_right]
+
+theorem get_extract_aux {as : Array α} {start stop : Nat} (h : i < (as.extract start stop).size) :
+    start + i < as.size := by
+  rw [size_extract] at h; apply Nat.add_lt_of_lt_sub'; apply Nat.lt_of_lt_of_le h
+  apply Nat.sub_le_sub_right; apply Nat.min_le_right
+
+@[simp] theorem get_extract {as : Array α} {start stop : Nat}
+    (h : i < (as.extract start stop).size) :
+    (as.extract start stop)[i] = as[start + i]'(get_extract_aux h) :=
+  show (extract.loop as (min stop as.size - start) start #[])[i]
+    = as[start + i]'(get_extract_aux h) by rw [get_extract_loop_ge]; rfl; exact Nat.zero_le _
+
+@[simp] theorem extract_all (as : Array α) : as.extract 0 as.size = as := by
+  apply ext
+  · rw [size_extract, Nat.min_self, Nat.sub_zero]
+  · intros; rw [get_extract]; congr; rw [Nat.zero_add]
+
+theorem extract_empty_of_stop_le_start (as : Array α) {start stop : Nat} (h : stop ≤ start) :
+    as.extract start stop = #[] := by
+  simp [extract]; rw [←Nat.sub_min_sub_right, Nat.sub_eq_zero_of_le h, Nat.zero_min,
+    extract_loop_zero]
+
+theorem extract_empty_of_size_le_start (as : Array α) {start stop : Nat} (h : as.size ≤ start) :
+    as.extract start stop = #[] := by
+  simp [extract]; rw [←Nat.sub_min_sub_right, Nat.sub_eq_zero_of_le h, Nat.min_zero,
+    extract_loop_zero]
+
+@[simp] theorem extract_empty (start stop : Nat) : (#[] : Array α).extract start stop = #[] :=
+  extract_empty_of_size_le_start _ (Nat.zero_le _)
+
+/-! ### any -/
+
+-- Auxiliary for `any_iff_exists`.
+theorem anyM_loop_iff_exists (p : α → Bool) (as : Array α) (start stop) (h : stop ≤ as.size) :
+    anyM.loop (m := Id) p as stop h start = true ↔
+      ∃ i : Fin as.size, start ≤ ↑i ∧ ↑i < stop ∧ p as[i] = true := by
+  unfold anyM.loop
+  split <;> rename_i h₁
+  · dsimp
+    split <;> rename_i h₂
+    · simp only [true_iff]
+      refine ⟨⟨start, by omega⟩, by dsimp; omega, by dsimp; omega, h₂⟩
+    · rw [anyM_loop_iff_exists]
+      constructor
+      · rintro ⟨i, ge, lt, h⟩
+        have : start ≠ i := by rintro rfl; omega
+        exact ⟨i, by omega, lt, h⟩
+      · rintro ⟨i, ge, lt, h⟩
+        have : start ≠ i := by rintro rfl; erw [h] at h₂; simp_all
+        exact ⟨i, by omega, lt, h⟩
+  · simp
+    omega
+termination_by stop - start
+
+-- This could also be proved from `SatisfiesM_anyM_iff_exists` in `Batteries.Data.Array.Init.Monadic`
+theorem any_iff_exists (p : α → Bool) (as : Array α) (start stop) :
+    any as p start stop ↔ ∃ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop ∧ p as[i] := by
+  dsimp [any, anyM, Id.run]
+  split
+  · rw [anyM_loop_iff_exists]; rfl
+  · rw [anyM_loop_iff_exists]
+    constructor
+    · rintro ⟨i, ge, _, h⟩
+      exact ⟨i, by omega, by omega, h⟩
+    · rintro ⟨i, ge, _, h⟩
+      exact ⟨i, by omega, by omega, h⟩
+
+theorem any_eq_true (p : α → Bool) (as : Array α) :
+    any as p ↔ ∃ i : Fin as.size, p as[i] := by simp [any_iff_exists, Fin.isLt]
+
+theorem any_def {p : α → Bool} (as : Array α) : as.any p = as.data.any p := by
+  rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true]; simp only [List.mem_iff_get]
+  exact ⟨fun ⟨i, h⟩ => ⟨_, ⟨i, rfl⟩, h⟩, fun ⟨_, ⟨i, rfl⟩, h⟩ => ⟨i, h⟩⟩
+
+/-! ### all -/
+
+theorem all_eq_not_any_not (p : α → Bool) (as : Array α) (start stop) :
+    all as p start stop = !(any as (!p ·) start stop) := by
+  dsimp [all, allM]
+  rfl
+
+theorem all_iff_forall (p : α → Bool) (as : Array α) (start stop) :
+    all as p start stop ↔ ∀ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop → p as[i] := by
+  rw [all_eq_not_any_not]
+  suffices ¬(any as (!p ·) start stop = true) ↔
+      ∀ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop → p as[i] by
+    simp_all
+  rw [any_iff_exists]
+  simp
+
+theorem all_eq_true (p : α → Bool) (as : Array α) : all as p ↔ ∀ i : Fin as.size, p as[i] := by
+  simp [all_iff_forall, Fin.isLt]
+
+theorem all_def {p : α → Bool} (as : Array α) : as.all p = as.data.all p := by
+  rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]; simp only [List.mem_iff_get]
+  constructor
+  · rintro w x ⟨r, rfl⟩
+    rw [← getElem_eq_data_get]
+    apply w
+  · intro w i
+    exact w as[i] ⟨i, (getElem_eq_data_get as i.2).symm⟩
+
+theorem all_eq_true_iff_forall_mem {l : Array α} : l.all p ↔ ∀ x, x ∈ l → p x := by
+  simp only [all_def, List.all_eq_true, mem_def]
+
+/-! ### contains -/
+
+theorem contains_def [DecidableEq α] {a : α} {as : Array α} : as.contains a ↔ a ∈ as := by
+  rw [mem_def, contains, any_def, List.any_eq_true]; simp [and_comm]
+
+instance [DecidableEq α] (a : α) (as : Array α) : Decidable (a ∈ as) :=
+  decidable_of_iff _ contains_def
+
+/-! ### swap -/
+
+open Fin
+
+@[simp] theorem get_swap_right (a : Array α) {i j : Fin a.size} : (a.swap i j)[j.val] = a[i] :=
+  by simp only [swap, fin_cast_val, get_eq_getElem, getElem_set_eq, getElem_fin]
+
+@[simp] theorem get_swap_left (a : Array α) {i j : Fin a.size} : (a.swap i j)[i.val] = a[j] :=
+  if he : ((Array.size_set _ _ _).symm ▸ j).val = i.val then by
+    simp only [←he, fin_cast_val, get_swap_right, getElem_fin]
+  else by
+    apply Eq.trans
+    · apply Array.get_set_ne
+      · simp only [size_set, Fin.isLt]
+      · assumption
+    · simp [get_set_ne]
+
+@[simp] theorem get_swap_of_ne (a : Array α) {i j : Fin a.size} (hp : p < a.size)
+    (hi : p ≠ i) (hj : p ≠ j) : (a.swap i j)[p]'(a.size_swap .. |>.symm ▸ hp) = a[p] := by
+  apply Eq.trans
+  · have : ((a.size_set i (a.get j)).symm ▸ j).val = j.val := by simp only [fin_cast_val]
+    apply Array.get_set_ne
+    · simp only [this]
+      apply Ne.symm
+      · assumption
+  · apply Array.get_set_ne
+    · apply Ne.symm
+      · assumption
+
+theorem get_swap (a : Array α) (i j : Fin a.size) (k : Nat) (hk: k < a.size) :
+    (a.swap i j)[k]'(by simp_all) = if k = i then a[j] else if k = j then a[i]  else a[k] := by
+  split
+  · simp_all only [get_swap_left]
+  · split <;> simp_all
+
+theorem get_swap' (a : Array α) (i j : Fin a.size) (k : Nat) (hk' : k < (a.swap i j).size) :
+    (a.swap i j)[k] = if k = i then a[j] else if k = j then a[i] else a[k]'(by simp_all) := by
+  apply get_swap
+
+@[simp] theorem swap_swap (a : Array α) {i j : Fin a.size} :
+    (a.swap i j).swap ⟨i.1, (a.size_swap ..).symm ▸i.2⟩ ⟨j.1, (a.size_swap ..).symm ▸j.2⟩ = a := by
+  apply ext
+  · simp only [size_swap]
+  · intros
+    simp only [get_swap']
+    split
+    · simp_all
+    · split <;> simp_all
+
+theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i := by
+  apply ext
+  · simp only [size_swap]
+  · intros
+    simp only [get_swap']
+    split
+    · split <;> simp_all
+    · split <;> simp_all
+
 
 end Array

src/Init/Data/Array/Mem.lean

@@ -27,13 +27,20 @@ theorem sizeOf_lt_of_mem [SizeOf α] {as : Array α} (h : a ∈ as) : sizeOf a <
   cases as with | _ as =>
   exact Nat.lt_trans (List.sizeOf_get ..) (by simp_arith)
 
+@[simp] theorem sizeOf_getElem [SizeOf α] (as : Array α) (i : Nat) (h : i < as.size) :
+  sizeOf (as[i]'h) < sizeOf as := sizeOf_get _ _
+
 /-- This tactic, added to the `decreasing_trivial` toolbox, proves that
 `sizeOf arr[i] < sizeOf arr`, which is useful for well founded recursions
 over a nested inductive like `inductive T | mk : Array T → T`. -/
 macro "array_get_dec" : tactic =>
   `(tactic| first
-    | apply sizeOf_get
-    | apply Nat.lt_trans (sizeOf_get ..); simp_arith)
+    -- subsumed by simp
+    -- | with_reducible apply sizeOf_get
+    -- | with_reducible apply sizeOf_getElem
+    | (with_reducible apply Nat.lt_trans (sizeOf_get ..)); simp_arith
+    | (with_reducible apply Nat.lt_trans (sizeOf_getElem ..)); simp_arith
+    )
 
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| array_get_dec)
 
@@ -43,9 +50,10 @@ provided that `a ∈ arr` which is useful for well founded recursions over a nes
 -- NB: This is analogue to tactic `sizeOf_list_dec`
 macro "array_mem_dec" : tactic =>
   `(tactic| first
-    | apply Array.sizeOf_lt_of_mem; assumption; done
-    | apply Nat.lt_trans (Array.sizeOf_lt_of_mem ?h)
-      case' h => assumption
+    | with_reducible apply Array.sizeOf_lt_of_mem; assumption; done
+    | with_reducible
+        apply Nat.lt_trans (Array.sizeOf_lt_of_mem ?h)
+        case' h => assumption
       simp_arith)
 
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| array_mem_dec)

src/Init/Data/Array/QSort.lean

@@ -27,6 +27,7 @@ def qpartition (as : Array α) (lt : α → α → Bool) (lo hi : Nat) : Nat ×
       let as := as.swap! i hi
       (i, as)
     termination_by hi - j
+    decreasing_by all_goals simp_wf; decreasing_trivial_pre_omega
   loop as lo lo
 
 @[inline] partial def qsort (as : Array α) (lt : α → α → Bool) (low := 0) (high := as.size - 1) : Array α :=

src/Init/Data/Array/Subarray.lean

@@ -15,14 +15,14 @@ structure Subarray (α : Type u)  where
   start_le_stop : start ≤ stop
   stop_le_array_size : stop ≤ array.size
 
-@[deprecated Subarray.array]
+@[deprecated Subarray.array (since := "2024-04-13")]
 abbrev Subarray.as (s : Subarray α) : Array α := s.array
 
-@[deprecated Subarray.start_le_stop]
+@[deprecated Subarray.start_le_stop (since := "2024-04-13")]
 theorem Subarray.h₁ (s : Subarray α) : s.start ≤ s.stop := s.start_le_stop
 
-@[deprecated Subarray.stop_le_array_size]
-theorem Subarray.h₂ (s : Subarray α) : s.stop ≤ s.as.size := s.stop_le_array_size
+@[deprecated Subarray.stop_le_array_size (since := "2024-04-13")]
+theorem Subarray.h₂ (s : Subarray α) : s.stop ≤ s.array.size := s.stop_le_array_size
 
 namespace Subarray
 

src/Init/Data/BitVec/Basic.lean

@@ -34,7 +34,8 @@ structure BitVec (w : Nat) where
   O(1), because we use `Fin` as the internal representation of a bitvector. -/
   toFin : Fin (2^w)
 
-@[deprecated] protected abbrev Std.BitVec := _root_.BitVec
+@[deprecated (since := "2024-04-12")]
+protected abbrev Std.BitVec := _root_.BitVec
 
 -- We manually derive the `DecidableEq` instances for `BitVec` because
 -- we want to have builtin support for bit-vector literals, and we
@@ -73,7 +74,7 @@ protected def toNat (a : BitVec n) : Nat := a.toFin.val
 /-- Return the bound in terms of toNat. -/
 theorem isLt (x : BitVec w) : x.toNat < 2^w := x.toFin.isLt
 
-@[deprecated isLt]
+@[deprecated isLt (since := "2024-03-12")]
 theorem toNat_lt (x : BitVec n) : x.toNat < 2^n := x.isLt
 
 /-- Theorem for normalizing the bit vector literal representation. -/

src/Init/Data/BitVec/Bitblast.lean

@@ -159,4 +159,43 @@ theorem add_eq_adc (w : Nat) (x y : BitVec w) : x + y = (adc x y false).snd := b
 theorem allOnes_sub_eq_not (x : BitVec w) : allOnes w - x = ~~~x := by
   rw [← add_not_self x, BitVec.add_comm, add_sub_cancel]
 
+/-! ### Negation -/
+
+theorem bit_not_testBit (x : BitVec w) (i : Fin w) :
+  getLsb (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsb i)))) ()).snd) i.val = !(getLsb x i.val) := by
+  apply iunfoldr_getLsb (fun _ => ()) i (by simp)
+
+theorem bit_not_add_self (x : BitVec w) :
+  ((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsb i)))) ()).snd + x  = -1 := by
+  simp only [add_eq_adc]
+  apply iunfoldr_replace_snd (fun _ => false) (-1) false rfl
+  intro i; simp only [ BitVec.not, adcb, testBit_toNat]
+  rw [iunfoldr_replace_snd (fun _ => ()) (((iunfoldr (fun i c => (c, !(x.getLsb i)))) ()).snd)]
+  <;> simp [bit_not_testBit, negOne_eq_allOnes, getLsb_allOnes]
+
+theorem bit_not_eq_not (x : BitVec w) :
+  ((iunfoldr (fun i c => (c, !(x.getLsb i)))) ()).snd = ~~~ x := by
+  simp [←allOnes_sub_eq_not, BitVec.eq_sub_iff_add_eq.mpr (bit_not_add_self x), ←negOne_eq_allOnes]
+
+theorem bit_neg_eq_neg (x : BitVec w) : -x = (adc (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsb i)))) ()).snd) (BitVec.ofNat w 1) false).snd:= by
+  simp only [← add_eq_adc]
+  rw [iunfoldr_replace_snd ((fun _ => ())) (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsb i)))) ()).snd) _ rfl]
+  · rw [BitVec.eq_sub_iff_add_eq.mpr (bit_not_add_self x), sub_toAdd, BitVec.add_comm _ (-x)]
+    simp [← sub_toAdd, BitVec.sub_add_cancel]
+  · simp [bit_not_testBit x _]
+
+/-! ### Inequalities (le / lt) -/
+
+theorem ult_eq_not_carry (x y : BitVec w) : x.ult y = !carry w x (~~~y) true := by
+  simp only [BitVec.ult, carry, toNat_mod_cancel, toNat_not, toNat_true, ge_iff_le, ← decide_not,
+    Nat.not_le, decide_eq_decide]
+  rw [Nat.mod_eq_of_lt (by omega)]
+  omega
+
+theorem ule_eq_not_ult (x y : BitVec w) : x.ule y = !y.ult x := by
+  simp [BitVec.ule, BitVec.ult, ← decide_not]
+
+theorem ule_eq_carry (x y : BitVec w) : x.ule y = carry w y (~~~x) true := by
+  simp [ule_eq_not_ult, ult_eq_not_carry]
+
 end BitVec

src/Init/Data/BitVec/Folds.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joe Hendrix
+Authors: Joe Hendrix, Harun Khan
 -/
 prelude
 import Init.Data.BitVec.Lemmas
@@ -48,6 +48,51 @@ private theorem iunfoldr.eq_test
     intro i
     simp_all [truncate_succ]
 
+theorem iunfoldr_getLsb' {f : Fin w → α → α × Bool} (state : Nat → α)
+    (ind : ∀(i : Fin w), (f i (state i.val)).fst = state (i.val+1)) :
+  (∀ i : Fin w, getLsb (iunfoldr f (state 0)).snd i.val = (f i (state i.val)).snd)
+  ∧ (iunfoldr f (state 0)).fst = state w := by
+  unfold iunfoldr
+  simp
+  apply Fin.hIterate_elim
+        (fun j (p : α × BitVec j) => (hj : j ≤ w) →
+         (∀ i : Fin j,  getLsb p.snd i.val = (f ⟨i.val, Nat.lt_of_lt_of_le i.isLt hj⟩ (state i.val)).snd)
+          ∧ p.fst = state j)
+  case hj => simp
+  case init =>
+    intro
+    apply And.intro
+    · intro i
+      have := Fin.size_pos i
+      contradiction
+    · rfl
+  case step =>
+    intro j ⟨s, v⟩ ih hj
+    apply And.intro
+    case left =>
+      intro i
+      simp only [getLsb_cons]
+      have hj2 : j.val ≤ w := by simp
+      cases (Nat.lt_or_eq_of_le (Nat.lt_succ.mp i.isLt)) with
+      | inl h3 => simp [if_neg, (Nat.ne_of_lt h3)]
+                  exact (ih hj2).1 ⟨i.val, h3⟩
+      | inr h3 => simp [h3, if_pos]
+                  cases (Nat.eq_zero_or_pos j.val) with
+                  | inl hj3 => congr
+                               rw [← (ih hj2).2]
+                  | inr hj3 => congr
+                               exact (ih hj2).2
+    case right =>
+      simp
+      have hj2 : j.val ≤ w := by simp
+      rw [← ind j, ← (ih hj2).2]
+
+
+theorem iunfoldr_getLsb {f : Fin w → α → α × Bool} (state : Nat → α) (i : Fin w)
+    (ind : ∀(i : Fin w), (f i (state i.val)).fst = state (i.val+1)) :
+  getLsb (iunfoldr f (state 0)).snd i.val = (f i (state i.val)).snd := by
+  exact (iunfoldr_getLsb' state ind).1 i
+
 /--
 Correctness theorem for `iunfoldr`.
 -/
@@ -58,4 +103,11 @@ theorem iunfoldr_replace
     iunfoldr f a = (state w, value) := by
   simp [iunfoldr.eq_test state value a init step]
 
+theorem iunfoldr_replace_snd
+  {f : Fin w → α → α × Bool} (state : Nat → α) (value : BitVec w) (a : α)
+    (init : state 0 = a)
+    (step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsb i.val)) :
+    (iunfoldr f a).snd = value := by
+  simp [iunfoldr.eq_test state value a init step]
+
 end BitVec

src/Init/Data/BitVec/Lemmas.lean

@@ -2,6 +2,7 @@
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joe Hendrix, Harun Khan, Alex Keizer, Abdalrhman M Mohamed,
+
 -/
 prelude
 import Init.Data.Bool
@@ -103,7 +104,13 @@ theorem eq_of_getMsb_eq {x y : BitVec w}
     have q := pred ⟨w - 1 - i, q_lt⟩
     simpa [q_lt, Nat.sub_sub_self, r] using q
 
-@[simp] theorem of_length_zero {x : BitVec 0} : x = 0#0 := by ext; simp
+-- This cannot be a `@[simp]` lemma, as it would be tried at every term.
+theorem of_length_zero {x : BitVec 0} : x = 0#0 := by ext; simp
+
+@[simp] theorem toNat_zero_length (x : BitVec 0) : x.toNat = 0 := by simp [of_length_zero]
+@[simp] theorem getLsb_zero_length (x : BitVec 0) : x.getLsb i = false := by simp [of_length_zero]
+@[simp] theorem getMsb_zero_length (x : BitVec 0) : x.getMsb i = false := by simp [of_length_zero]
+@[simp] theorem msb_zero_length (x : BitVec 0) : x.msb = false := by simp [BitVec.msb, of_length_zero]
 
 theorem eq_of_toFin_eq : ∀ {x y : BitVec w}, x.toFin = y.toFin → x = y
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
@@ -139,7 +146,8 @@ theorem getLsb_ofNat (n : Nat) (x : Nat) (i : Nat) :
   getLsb (x#n) i = (i < n && x.testBit i) := by
   simp [getLsb, BitVec.ofNat, Fin.val_ofNat']
 
-@[simp, deprecated toNat_ofNat] theorem toNat_zero (n : Nat) : (0#n).toNat = 0 := by trivial
+@[simp, deprecated toNat_ofNat (since := "2024-02-22")]
+theorem toNat_zero (n : Nat) : (0#n).toNat = 0 := by trivial
 
 @[simp] theorem getLsb_zero : (0#w).getLsb i = false := by simp [getLsb]
 
@@ -238,6 +246,12 @@ theorem eq_of_toInt_eq {i j : BitVec n} : i.toInt = j.toInt → i = j := by
   have _jlt := j.isLt
   split <;> split <;> omega
 
+theorem toInt_inj (x y : BitVec n) : x.toInt = y.toInt ↔ x = y :=
+  Iff.intro eq_of_toInt_eq (congrArg BitVec.toInt)
+
+theorem toInt_ne (x y : BitVec n) : x.toInt ≠ y.toInt ↔ x ≠ y  := by
+  rw [Ne, toInt_inj]
+
 @[simp] theorem toNat_ofInt {n : Nat} (i : Int) :
   (BitVec.ofInt n i).toNat = (i % (2^n : Nat)).toNat := by
   unfold BitVec.ofInt
@@ -336,7 +350,7 @@ theorem nat_eq_toNat (x : BitVec w) (y : Nat)
 @[simp] theorem getMsb_zeroExtend_add {x : BitVec w} (h : k ≤ i) :
     (x.zeroExtend (w + k)).getMsb i = x.getMsb (i - k) := by
   by_cases h : w = 0
-  · subst h; simp
+  · subst h; simp [of_length_zero]
   simp only [getMsb, getLsb_zeroExtend]
   by_cases h₁ : i < w + k <;> by_cases h₂ : i - k < w <;> by_cases h₃ : w + k - 1 - i < w + k
     <;> simp [h₁, h₂, h₃]
@@ -595,6 +609,17 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
     (shiftLeftZeroExtend x i).msb = x.msb := by
   simp [shiftLeftZeroExtend_eq, BitVec.msb]
 
+theorem shiftLeft_shiftLeft {w : Nat} (x : BitVec w) (n m : Nat) :
+    (x <<< n) <<< m = x <<< (n + m) := by
+  ext i
+  simp only [getLsb_shiftLeft, Fin.is_lt, decide_True, Bool.true_and]
+  rw [show i - (n + m) = (i - m - n) by omega]
+  cases h₂ : decide (i < m) <;>
+  cases h₃ : decide (i - m < w) <;>
+  cases h₄ : decide (i - m < n) <;>
+  cases h₅ : decide (i < n + m) <;>
+    simp at * <;> omega
+
 /-! ### ushiftRight -/
 
 @[simp, bv_toNat] theorem toNat_ushiftRight (x : BitVec n) (i : Nat) :
@@ -680,6 +705,11 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
   simp only [getLsb_append, cond_eq_if]
   split <;> simp [*]
 
+theorem shiftRight_shiftRight {w : Nat} (x : BitVec w) (n m : Nat) :
+    (x >>> n) >>> m = x >>> (n + m) := by
+  ext i
+  simp [Nat.add_assoc n m i]
+
 /-! ### rev -/
 
 theorem getLsb_rev (x : BitVec w) (i : Fin w) :
@@ -890,10 +920,19 @@ theorem sub_toAdd {n} (x y : BitVec n) : x - y = x + - y := by
 
 theorem add_sub_cancel (x y : BitVec w) : x + y - y = x := by
   apply eq_of_toNat_eq
-  have y_toNat_le := Nat.le_of_lt y.toNat_lt
+  have y_toNat_le := Nat.le_of_lt y.isLt
   rw [toNat_sub, toNat_add, Nat.mod_add_mod, Nat.add_assoc, ← Nat.add_sub_assoc y_toNat_le,
     Nat.add_sub_cancel_left, Nat.add_mod_right, toNat_mod_cancel]
 
+theorem sub_add_cancel (x y : BitVec w) : x - y + y = x := by
+  rw [sub_toAdd, BitVec.add_assoc, BitVec.add_comm _ y,
+      ← BitVec.add_assoc, ← sub_toAdd, add_sub_cancel]
+
+theorem eq_sub_iff_add_eq {x y z : BitVec w} : x = z - y ↔ x + y = z := by
+  apply Iff.intro <;> intro h
+  · simp [h, sub_add_cancel]
+  · simp [←h, add_sub_cancel]
+
 theorem negOne_eq_allOnes : -1#w = allOnes w := by
   apply eq_of_toNat_eq
   if g : w = 0 then
@@ -903,6 +942,13 @@ theorem negOne_eq_allOnes : -1#w = allOnes w := by
     have r : (2^w - 1) < 2^w := by omega
     simp [Nat.mod_eq_of_lt q, Nat.mod_eq_of_lt r]
 
+theorem neg_eq_not_add (x : BitVec w) : -x = ~~~x + 1 := by
+  apply eq_of_toNat_eq
+  simp only [toNat_neg, ofNat_eq_ofNat, toNat_add, toNat_not, toNat_ofNat, Nat.add_mod_mod]
+  congr
+  have hx : x.toNat < 2^w := x.isLt
+  rw [Nat.sub_sub, Nat.add_comm 1 x.toNat, ← Nat.sub_sub, Nat.sub_add_cancel (by omega)]
+
 /-! ### mul -/
 
 theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := by rfl

src/Init/Data/Bool.lean

@@ -360,7 +360,8 @@ def toNat (b:Bool) : Nat := cond b 1 0
 theorem toNat_le (c : Bool) : c.toNat ≤ 1 := by
   cases c <;> trivial
 
-@[deprecated toNat_le] abbrev toNat_le_one := toNat_le
+@[deprecated toNat_le (since := "2024-02-23")]
+abbrev toNat_le_one := toNat_le
 
 theorem toNat_lt (b : Bool) : b.toNat < 2 :=
   Nat.lt_succ_of_le (toNat_le _)

src/Init/Data/Fin/Fold.lean

@@ -12,6 +12,7 @@ import Init.Data.Nat.Linear
   loop (x : α) (i : Nat) : α :=
     if h : i < n then loop (f x ⟨i, h⟩) (i+1) else x
   termination_by n - i
+  decreasing_by decreasing_trivial_pre_omega
 
 /-- Folds over `Fin n` from the right: `foldr 3 f x = f 0 (f 1 (f 2 x))`. -/
 @[inline] def foldr (n) (f : Fin n → α → α) (init : α) : α := loop ⟨n, Nat.le_refl n⟩ init where

src/Init/Data/Fin/Iterate.lean

@@ -23,6 +23,7 @@ def hIterateFrom (P : Nat → Sort _) {n} (f : ∀(i : Fin n), P i.val → P (i.
     have p : i = n := (or_iff_left g).mp (Nat.eq_or_lt_of_le ubnd)
     _root_.cast (congrArg P p) a
   termination_by n - i
+  decreasing_by decreasing_trivial_pre_omega
 
 /--
 `hIterate` is a heterogenous iterative operation that applies a

src/Init/Data/Fin/Lemmas.lean

@@ -11,6 +11,9 @@ import Init.ByCases
 import Init.Conv
 import Init.Omega
 
+-- Remove after the next stage0 update
+set_option allowUnsafeReducibility true
+
 namespace Fin
 
 /-- If you actually have an element of `Fin n`, then the `n` is always positive -/
@@ -59,7 +62,8 @@ theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta ..
 @[simp] theorem val_ofNat' (a : Nat) (is_pos : n > 0) :
   (Fin.ofNat' a is_pos).val = a % n := rfl
 
-@[deprecated ofNat'_zero_val] theorem ofNat'_zero_val : (Fin.ofNat' 0 h).val = 0 := Nat.zero_mod _
+@[deprecated ofNat'_zero_val (since := "2024-02-22")]
+theorem ofNat'_zero_val : (Fin.ofNat' 0 h).val = 0 := Nat.zero_mod _
 
 @[simp] theorem mod_val (a b : Fin n) : (a % b).val = a.val % b.val :=
   rfl
@@ -602,6 +606,7 @@ A version of `Fin.succRec` taking `i : Fin n` as the first argument. -/
     @Fin.succRecOn (n + 1) i.succ motive zero succ = succ n i (Fin.succRecOn i zero succ) := by
   cases i; rfl
 
+
 /-- Define `motive i` by induction on `i : Fin (n + 1)` via induction on the underlying `Nat` value.
 This function has two arguments: `zero` handles the base case on `motive 0`,
 and `succ` defines the inductive step using `motive i.castSucc`.
@@ -610,8 +615,12 @@ and `succ` defines the inductive step using `motive i.castSucc`.
 @[elab_as_elim] def induction {motive : Fin (n + 1) → Sort _} (zero : motive 0)
     (succ : ∀ i : Fin n, motive (castSucc i) → motive i.succ) :
     ∀ i : Fin (n + 1), motive i
-  | ⟨0, hi⟩ => by rwa [Fin.mk_zero]
-  | ⟨i+1, hi⟩ => succ ⟨i, Nat.lt_of_succ_lt_succ hi⟩ (induction zero succ ⟨i, Nat.lt_of_succ_lt hi⟩)
+  | ⟨i, hi⟩ => go i hi
+where
+  -- Use a curried function so that this is structurally recursive
+  go : ∀ (i : Nat) (hi : i < n + 1), motive ⟨i, hi⟩
+  | 0, hi => by rwa [Fin.mk_zero]
+  | i+1, hi => succ ⟨i, Nat.lt_of_succ_lt_succ hi⟩ (go i (Nat.lt_of_succ_lt hi))
 
 @[simp] theorem induction_zero {motive : Fin (n + 1) → Sort _} (zero : motive 0)
     (hs : ∀ i : Fin n, motive (castSucc i) → motive i.succ) :

src/Init/Data/Int/DivModLemmas.lean

@@ -14,6 +14,8 @@ import Init.RCases
 # Lemmas about integer division needed to bootstrap `omega`.
 -/
 
+-- Remove after the next stage0 update
+set_option allowUnsafeReducibility true
 
 open Nat (succ)
 
@@ -142,12 +144,14 @@ theorem eq_one_of_mul_eq_one_left {a b : Int} (H : 0 ≤ b) (H' : a * b = 1) : b
   | ofNat _ => show ofNat _ = _ by simp
   | -[_+1] => show -ofNat _ = _ by simp
 
+unseal Nat.div in
 @[simp] protected theorem div_zero : ∀ a : Int, div a 0 = 0
   | ofNat _ => show ofNat _ = _ by simp
   | -[_+1] => rfl
 
 @[simp] theorem zero_fdiv (b : Int) : fdiv 0 b = 0 := by cases b <;> rfl
 
+unseal Nat.div in
 @[simp] protected theorem fdiv_zero : ∀ a : Int, fdiv a 0 = 0
   | 0      => rfl
   | succ _ => rfl
@@ -178,7 +182,7 @@ theorem fdiv_eq_div {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : fdiv a b = div a
 
 @[simp] theorem mod_zero : ∀ a : Int, mod a 0 = a
   | ofNat _ => congrArg ofNat <| Nat.mod_zero _
-  | -[_+1] => rfl
+  | -[_+1] => congrArg (fun n => -ofNat n) <| Nat.mod_zero _
 
 @[simp] theorem zero_fmod (b : Int) : fmod 0 b = 0 := by cases b <;> rfl
 
@@ -225,7 +229,9 @@ theorem mod_add_div : ∀ a b : Int, mod a b + b * (a.div b) = a
   | ofNat m, -[n+1] => by
     show (m % succ n + -↑(succ n) * -↑(m / succ n) : Int) = m
     rw [Int.neg_mul_neg]; exact congrArg ofNat (Nat.mod_add_div ..)
-  | -[_+1], 0 => rfl
+  | -[m+1], 0 => by
+    show -(↑((succ m) % 0) : Int) + 0 * -↑(succ m / 0) = -↑(succ m)
+    rw [Nat.mod_zero, Int.zero_mul, Int.add_zero]
   | -[m+1], ofNat n => by
     show -(↑((succ m) % n) : Int) + ↑n * -↑(succ m / n) = -↑(succ m)
     rw [Int.mul_neg, ← Int.neg_add]
@@ -763,11 +769,13 @@ theorem ediv_eq_ediv_of_mul_eq_mul {a b c d : Int}
   | (n:Nat) => congrArg ofNat (Nat.div_one _)
   | -[n+1] => by simp [Int.div, neg_ofNat_succ]; rfl
 
+unseal Nat.div in
 @[simp] protected theorem div_neg : ∀ a b : Int, a.div (-b) = -(a.div b)
   | ofNat m, 0 => show ofNat (m / 0) = -↑(m / 0) by rw [Nat.div_zero]; rfl
   | ofNat m, -[n+1] | -[m+1], succ n => (Int.neg_neg _).symm
   | ofNat m, succ n | -[m+1], 0 | -[m+1], -[n+1] => rfl
 
+unseal Nat.div in
 @[simp] protected theorem neg_div : ∀ a b : Int, (-a).div b = -(a.div b)
   | 0, n => by simp [Int.neg_zero]
   | succ m, (n:Nat) | -[m+1], 0 | -[m+1], -[n+1] => rfl
@@ -936,6 +944,7 @@ theorem fdiv_nonneg {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a.fdiv b :
   match a, b, eq_ofNat_of_zero_le Ha, eq_ofNat_of_zero_le Hb with
   | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => ofNat_fdiv .. ▸ ofNat_zero_le _
 
+unseal Nat.div in
 theorem fdiv_nonpos : ∀ {a b : Int}, 0 ≤ a → b ≤ 0 → a.fdiv b ≤ 0
   | 0, 0, _, _ | 0, -[_+1], _, _ | succ _, 0, _, _ | succ _, -[_+1], _, _ => ⟨_⟩
 

src/Init/Data/List.lean

@@ -9,3 +9,4 @@ import Init.Data.List.BasicAux
 import Init.Data.List.Control
 import Init.Data.List.Lemmas
 import Init.Data.List.Impl
+import Init.Data.List.TakeDrop

src/Init/Data/List/BasicAux.lean

@@ -226,9 +226,10 @@ theorem sizeOf_lt_of_mem [SizeOf α] {as : List α} (h : a ∈ as) : sizeOf a <
 over a nested inductive like `inductive T | mk : List T → T`. -/
 macro "sizeOf_list_dec" : tactic =>
   `(tactic| first
-    | apply sizeOf_lt_of_mem; assumption; done
-    | apply Nat.lt_trans (sizeOf_lt_of_mem ?h)
-      case' h => assumption
+    | with_reducible apply sizeOf_lt_of_mem; assumption; done
+    | with_reducible
+        apply Nat.lt_trans (sizeOf_lt_of_mem ?h)
+        case' h => assumption
       simp_arith)
 
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| sizeOf_list_dec)

src/Init/Data/List/TakeDrop.lean

@@ -0,0 +1,360 @@
+/-
+Copyright (c) 2014 Parikshit Khanna. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
+-/
+prelude
+import Init.Data.List.Lemmas
+import Init.Data.Nat.Lemmas
+
+/-!
+# Lemmas about `List.take`, `List.drop`, `List.zip` and `List.zipWith`.
+
+These are in a separate file from most of the list lemmas
+as they required importing more lemmas about natural numbers.
+-/
+
+namespace List
+
+open Nat
+
+/-! ### take -/
+
+abbrev take_succ_cons := @take_cons_succ
+
+@[simp] theorem length_take : ∀ (i : Nat) (l : List α), length (take i l) = min i (length l)
+  | 0, l => by simp [Nat.zero_min]
+  | succ n, [] => by simp [Nat.min_zero]
+  | succ n, _ :: l => by simp [Nat.succ_min_succ, length_take]
+
+theorem length_take_le (n) (l : List α) : length (take n l) ≤ n := by simp [Nat.min_le_left]
+
+theorem length_take_le' (n) (l : List α) : length (take n l) ≤ l.length :=
+  by simp [Nat.min_le_right]
+
+theorem length_take_of_le (h : n ≤ length l) : length (take n l) = n := by simp [Nat.min_eq_left h]
+
+theorem take_all_of_le {n} {l : List α} (h : length l ≤ n) : take n l = l :=
+  take_length_le h
+
+@[simp]
+theorem take_left : ∀ l₁ l₂ : List α, take (length l₁) (l₁ ++ l₂) = l₁
+  | [], _ => rfl
+  | a :: l₁, l₂ => congrArg (cons a) (take_left l₁ l₂)
+
+theorem take_left' {l₁ l₂ : List α} {n} (h : length l₁ = n) : take n (l₁ ++ l₂) = l₁ := by
+  rw [← h]; apply take_left
+
+theorem take_take : ∀ (n m) (l : List α), take n (take m l) = take (min n m) l
+  | n, 0, l => by rw [Nat.min_zero, take_zero, take_nil]
+  | 0, m, l => by rw [Nat.zero_min, take_zero, take_zero]
+  | succ n, succ m, nil => by simp only [take_nil]
+  | succ n, succ m, a :: l => by
+    simp only [take, succ_min_succ, take_take n m l]
+
+theorem take_replicate (a : α) : ∀ n m : Nat, take n (replicate m a) = replicate (min n m) a
+  | n, 0 => by simp [Nat.min_zero]
+  | 0, m => by simp [Nat.zero_min]
+  | succ n, succ m => by simp [succ_min_succ, take_replicate]
+
+theorem map_take (f : α → β) :
+    ∀ (L : List α) (i : Nat), (L.take i).map f = (L.map f).take i
+  | [], i => by simp
+  | _, 0 => by simp
+  | h :: t, n + 1 => by dsimp; rw [map_take f t n]
+
+/-- Taking the first `n` elements in `l₁ ++ l₂` is the same as appending the first `n` elements
+of `l₁` to the first `n - l₁.length` elements of `l₂`. -/
+theorem take_append_eq_append_take {l₁ l₂ : List α} {n : Nat} :
+    take n (l₁ ++ l₂) = take n l₁ ++ take (n - l₁.length) l₂ := by
+  induction l₁ generalizing n
+  · simp
+  · cases n
+    · simp [*]
+    · simp only [cons_append, take_cons_succ, length_cons, succ_eq_add_one, cons.injEq,
+        append_cancel_left_eq, true_and, *]
+      congr 1
+      omega
+
+theorem take_append_of_le_length {l₁ l₂ : List α} {n : Nat} (h : n ≤ l₁.length) :
+    (l₁ ++ l₂).take n = l₁.take n := by
+  simp [take_append_eq_append_take, Nat.sub_eq_zero_of_le h]
+
+/-- Taking the first `l₁.length + i` elements in `l₁ ++ l₂` is the same as appending the first
+`i` elements of `l₂` to `l₁`. -/
+theorem take_append {l₁ l₂ : List α} (i : Nat) :
+    take (l₁.length + i) (l₁ ++ l₂) = l₁ ++ take i l₂ := by
+  rw [take_append_eq_append_take, take_all_of_le (Nat.le_add_right _ _), Nat.add_sub_cancel_left]
+
+/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
+length `> i`. Version designed to rewrite from the big list to the small list. -/
+theorem get_take (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) :
+    get L ⟨i, hi⟩ = get (L.take j) ⟨i, length_take .. ▸ Nat.lt_min.mpr ⟨hj, hi⟩⟩ :=
+  get_of_eq (take_append_drop j L).symm _ ▸ get_append ..
+
+/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
+length `> i`. Version designed to rewrite from the small list to the big list. -/
+theorem get_take' (L : List α) {j i} :
+    get (L.take j) i =
+    get L ⟨i.1, Nat.lt_of_lt_of_le i.2 (length_take_le' _ _)⟩ := by
+  let ⟨i, hi⟩ := i; rw [length_take, Nat.lt_min] at hi; rw [get_take L _ hi.1]
+
+theorem get?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n).get? m = l.get? m := by
+  induction n generalizing l m with
+  | zero =>
+    exact absurd h (Nat.not_lt_of_le m.zero_le)
+  | succ _ hn =>
+    cases l with
+    | nil => simp only [take_nil]
+    | cons hd tl =>
+      cases m
+      · simp only [get?, take]
+      · simpa only using hn (Nat.lt_of_succ_lt_succ h)
+
+theorem get?_take_eq_none {l : List α} {n m : Nat} (h : n ≤ m) :
+    (l.take n).get? m = none :=
+  get?_eq_none.mpr <| Nat.le_trans (length_take_le _ _) h
+
+theorem get?_take_eq_if {l : List α} {n m : Nat} :
+    (l.take n).get? m = if m < n then l.get? m else none := by
+  split
+  · next h => exact get?_take h
+  · next h => exact get?_take_eq_none (Nat.le_of_not_lt h)
+
+@[simp]
+theorem nth_take_of_succ {l : List α} {n : Nat} : (l.take (n + 1)).get? n = l.get? n :=
+  get?_take (Nat.lt_succ_self n)
+
+theorem take_succ {l : List α} {n : Nat} : l.take (n + 1) = l.take n ++ (l.get? n).toList := by
+  induction l generalizing n with
+  | nil =>
+    simp only [Option.toList, get?, take_nil, append_nil]
+  | cons hd tl hl =>
+    cases n
+    · simp only [Option.toList, get?, eq_self_iff_true, take, nil_append]
+    · simp only [hl, cons_append, get?, eq_self_iff_true, take]
+
+@[simp]
+theorem take_eq_nil_iff {l : List α} {k : Nat} : l.take k = [] ↔ l = [] ∨ k = 0 := by
+  cases l <;> cases k <;> simp [Nat.succ_ne_zero]
+
+@[simp]
+theorem take_eq_take :
+    ∀ {l : List α} {m n : Nat}, l.take m = l.take n ↔ min m l.length = min n l.length
+  | [], m, n => by simp [Nat.min_zero]
+  | _ :: xs, 0, 0 => by simp
+  | x :: xs, m + 1, 0 => by simp [Nat.zero_min, succ_min_succ]
+  | x :: xs, 0, n + 1 => by simp [Nat.zero_min, succ_min_succ]
+  | x :: xs, m + 1, n + 1 => by simp [succ_min_succ, take_eq_take]; omega
+
+theorem take_add (l : List α) (m n : Nat) : l.take (m + n) = l.take m ++ (l.drop m).take n := by
+  suffices take (m + n) (take m l ++ drop m l) = take m l ++ take n (drop m l) by
+    rw [take_append_drop] at this
+    assumption
+  rw [take_append_eq_append_take, take_all_of_le, append_right_inj]
+  · simp only [take_eq_take, length_take, length_drop]
+    omega
+  apply Nat.le_trans (m := m)
+  · apply length_take_le
+  · apply Nat.le_add_right
+
+theorem take_eq_nil_of_eq_nil : ∀ {as : List α} {i}, as = [] → as.take i = []
+  | _, _, rfl => take_nil
+
+theorem ne_nil_of_take_ne_nil {as : List α} {i : Nat} (h: as.take i ≠ []) : as ≠ [] :=
+  mt take_eq_nil_of_eq_nil h
+
+theorem dropLast_eq_take (l : List α) : l.dropLast = l.take l.length.pred := by
+  cases l with
+  | nil => simp [dropLast]
+  | cons x l =>
+    induction l generalizing x with
+    | nil => simp [dropLast]
+    | cons hd tl hl => simp [dropLast, hl]
+
+theorem dropLast_take {n : Nat} {l : List α} (h : n < l.length) :
+    (l.take n).dropLast = l.take n.pred := by
+  simp only [dropLast_eq_take, length_take, Nat.le_of_lt h, take_take, pred_le, Nat.min_eq_left]
+
+theorem map_eq_append_split {f : α → β} {l : List α} {s₁ s₂ : List β}
+    (h : map f l = s₁ ++ s₂) : ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = s₁ ∧ map f l₂ = s₂ := by
+  have := h
+  rw [← take_append_drop (length s₁) l] at this ⊢
+  rw [map_append] at this
+  refine ⟨_, _, rfl, append_inj this ?_⟩
+  rw [length_map, length_take, Nat.min_eq_left]
+  rw [← length_map l f, h, length_append]
+  apply Nat.le_add_right
+
+/-! ### drop -/
+
+@[simp]
+theorem drop_eq_nil_iff_le {l : List α} {k : Nat} : l.drop k = [] ↔ l.length ≤ k := by
+  refine' ⟨fun h => _, drop_eq_nil_of_le⟩
+  induction k generalizing l with
+  | zero =>
+    simp only [drop] at h
+    simp [h]
+  | succ k hk =>
+    cases l
+    · simp
+    · simp only [drop] at h
+      simpa [Nat.succ_le_succ_iff] using hk h
+
+theorem drop_length_cons {l : List α} (h : l ≠ []) (a : α) :
+    (a :: l).drop l.length = [l.getLast h] := by
+  induction l generalizing a with
+  | nil =>
+    cases h rfl
+  | cons y l ih =>
+    simp only [drop, length]
+    by_cases h₁ : l = []
+    · simp [h₁]
+    rw [getLast_cons' _ h₁]
+    exact ih h₁ y
+
+/-- Dropping the elements up to `n` in `l₁ ++ l₂` is the same as dropping the elements up to `n`
+in `l₁`, dropping the elements up to `n - l₁.length` in `l₂`, and appending them. -/
+theorem drop_append_eq_append_drop {l₁ l₂ : List α} {n : Nat} :
+    drop n (l₁ ++ l₂) = drop n l₁ ++ drop (n - l₁.length) l₂ := by
+  induction l₁ generalizing n
+  · simp
+  · cases n
+    · simp [*]
+    · simp only [cons_append, drop_succ_cons, length_cons, succ_eq_add_one, append_cancel_left_eq, *]
+      congr 1
+      omega
+
+theorem drop_append_of_le_length {l₁ l₂ : List α} {n : Nat} (h : n ≤ l₁.length) :
+    (l₁ ++ l₂).drop n = l₁.drop n ++ l₂ := by
+  simp [drop_append_eq_append_drop, Nat.sub_eq_zero_of_le h]
+
+
+/-- Dropping the elements up to `l₁.length + i` in `l₁ + l₂` is the same as dropping the elements
+up to `i` in `l₂`. -/
+@[simp]
+theorem drop_append {l₁ l₂ : List α} (i : Nat) : drop (l₁.length + i) (l₁ ++ l₂) = drop i l₂ := by
+  rw [drop_append_eq_append_drop, drop_eq_nil_of_le] <;>
+    simp [Nat.add_sub_cancel_left, Nat.le_add_right]
+
+theorem drop_sizeOf_le [SizeOf α] (l : List α) (n : Nat) : sizeOf (l.drop n) ≤ sizeOf l := by
+  induction l generalizing n with
+  | nil => rw [drop_nil]; apply Nat.le_refl
+  | cons _ _ lih =>
+    induction n with
+    | zero => apply Nat.le_refl
+    | succ n =>
+      exact Trans.trans (lih _) (Nat.le_add_left _ _)
+
+theorem lt_length_drop (L : List α) {i j : Nat} (h : i + j < L.length) : j < (L.drop i).length := by
+  have A : i < L.length := Nat.lt_of_le_of_lt (Nat.le.intro rfl) h
+  rw [(take_append_drop i L).symm] at h
+  simpa only [Nat.le_of_lt A, Nat.min_eq_left, Nat.add_lt_add_iff_left, length_take,
+    length_append] using h
+
+/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
+dropping the first `i` elements. Version designed to rewrite from the big list to the small list. -/
+theorem get_drop (L : List α) {i j : Nat} (h : i + j < L.length) :
+    get L ⟨i + j, h⟩ = get (L.drop i) ⟨j, lt_length_drop L h⟩ := by
+  have : i ≤ L.length := Nat.le_trans (Nat.le_add_right _ _) (Nat.le_of_lt h)
+  rw [get_of_eq (take_append_drop i L).symm ⟨i + j, h⟩, get_append_right'] <;>
+    simp [Nat.min_eq_left this, Nat.add_sub_cancel_left, Nat.le_add_right]
+
+/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
+dropping the first `i` elements. Version designed to rewrite from the small list to the big list. -/
+theorem get_drop' (L : List α) {i j} :
+    get (L.drop i) j = get L ⟨i + j, by
+      rw [Nat.add_comm]
+      exact Nat.add_lt_of_lt_sub (length_drop i L ▸ j.2)⟩ := by
+  rw [get_drop]
+
+@[simp]
+theorem get?_drop (L : List α) (i j : Nat) : get? (L.drop i) j = get? L (i + j) := by
+  ext
+  simp only [get?_eq_some, get_drop', Option.mem_def]
+  constructor <;> intro ⟨h, ha⟩
+  · exact ⟨_, ha⟩
+  · refine ⟨?_, ha⟩
+    rw [length_drop]
+    rw [Nat.add_comm] at h
+    apply Nat.lt_sub_of_add_lt h
+
+@[simp] theorem drop_drop (n : Nat) : ∀ (m) (l : List α), drop n (drop m l) = drop (n + m) l
+  | m, [] => by simp
+  | 0, l => by simp
+  | m + 1, a :: l =>
+    calc
+      drop n (drop (m + 1) (a :: l)) = drop n (drop m l) := rfl
+      _ = drop (n + m) l := drop_drop n m l
+      _ = drop (n + (m + 1)) (a :: l) := rfl
+
+theorem take_drop : ∀ (m n : Nat) (l : List α), take n (drop m l) = drop m (take (m + n) l)
+  | 0, _, _ => by simp
+  | _, _, [] => by simp
+  | _+1, _, _ :: _ => by simpa [Nat.succ_add, take_succ_cons, drop_succ_cons] using take_drop ..
+
+theorem drop_take : ∀ (m n : Nat) (l : List α), drop n (take m l) = take (m - n) (drop n l)
+  | 0, _, _ => by simp
+  | _, 0, _ => by simp
+  | _, _, [] => by simp
+  | m+1, n+1, h :: t => by
+    simp [take_succ_cons, drop_succ_cons, drop_take m n t]
+    congr 1
+    omega
+
+theorem map_drop (f : α → β) :
+    ∀ (L : List α) (i : Nat), (L.drop i).map f = (L.map f).drop i
+  | [], i => by simp
+  | L, 0 => by simp
+  | h :: t, n + 1 => by
+    dsimp
+    rw [map_drop f t]
+
+theorem reverse_take {α} {xs : List α} (n : Nat) (h : n ≤ xs.length) :
+    xs.reverse.take n = (xs.drop (xs.length - n)).reverse := by
+  induction xs generalizing n <;>
+    simp only [reverse_cons, drop, reverse_nil, Nat.zero_sub, length, take_nil]
+  next xs_hd xs_tl xs_ih =>
+  cases Nat.lt_or_eq_of_le h with
+  | inl h' =>
+    have h' := Nat.le_of_succ_le_succ h'
+    rw [take_append_of_le_length, xs_ih _ h']
+    rw [show xs_tl.length + 1 - n = succ (xs_tl.length - n) from _, drop]
+    · rwa [succ_eq_add_one, Nat.sub_add_comm]
+    · rwa [length_reverse]
+  | inr h' =>
+    subst h'
+    rw [length, Nat.sub_self, drop]
+    suffices xs_tl.length + 1 = (xs_tl.reverse ++ [xs_hd]).length by
+      rw [this, take_length, reverse_cons]
+    rw [length_append, length_reverse]
+    rfl
+
+@[simp]
+theorem get_cons_drop : ∀ (l : List α) i, get l i :: drop (i + 1) l = drop i l
+  | _::_, ⟨0, _⟩ => rfl
+  | _::_, ⟨i+1, _⟩ => get_cons_drop _ ⟨i, _⟩
+
+theorem drop_eq_get_cons {n} {l : List α} (h) : drop n l = get l ⟨n, h⟩ :: drop (n + 1) l :=
+  (get_cons_drop _ ⟨n, h⟩).symm
+
+theorem drop_eq_nil_of_eq_nil : ∀ {as : List α} {i}, as = [] → as.drop i = []
+  | _, _, rfl => drop_nil
+
+theorem ne_nil_of_drop_ne_nil {as : List α} {i : Nat} (h: as.drop i ≠ []) : as ≠ [] :=
+  mt drop_eq_nil_of_eq_nil h
+
+/-! ### zipWith -/
+
+@[simp] theorem length_zipWith (f : α → β → γ) (l₁ l₂) :
+    length (zipWith f l₁ l₂) = min (length l₁) (length l₂) := by
+  induction l₁ generalizing l₂ <;> cases l₂ <;>
+    simp_all [succ_min_succ, Nat.zero_min, Nat.min_zero]
+
+/-! ### zip -/
+
+@[simp] theorem length_zip (l₁ : List α) (l₂ : List β) :
+    length (zip l₁ l₂) = min (length l₁) (length l₂) := by
+  simp [zip]
+
+end List

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -50,7 +50,10 @@ noncomputable def div2Induction {motive : Nat → Sort u}
       apply hyp
       exact Nat.div_lt_self n_pos (Nat.le_refl _)
 
-@[simp] theorem zero_and (x : Nat) : 0 &&& x = 0 := by rfl
+@[simp] theorem zero_and (x : Nat) : 0 &&& x = 0 := by
+  simp only [HAnd.hAnd, AndOp.and, land]
+  unfold bitwise
+  simp
 
 @[simp] theorem and_zero (x : Nat) : x &&& 0 = 0 := by
   simp only [HAnd.hAnd, AndOp.and, land]
@@ -188,8 +191,6 @@ theorem lt_pow_two_of_testBit (x : Nat) (p : ∀i, i ≥ n → testBit x i = fal
   have test_false := p _ i_ge_n
   simp only [test_true] at test_false
 
-/-! ### testBit -/
-
 private theorem succ_mod_two : succ x % 2 = 1 - x % 2 := by
   induction x with
   | zero =>
@@ -233,7 +234,7 @@ theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) :
     rw [Nat.sub_eq_zero_iff_le] at i_sub_j_eq
     exact Nat.not_le_of_gt j_lt_i i_sub_j_eq
   | d+1 =>
-    simp [Nat.pow_succ, Nat.mul_comm _ 2,  Nat.mul_add_mod]
+    simp [Nat.pow_succ, Nat.mul_comm _ 2, Nat.mul_add_mod]
 
 @[simp] theorem testBit_mod_two_pow (x j i : Nat) :
     testBit (x % 2^j) i = (decide (i < j) && testBit x i) := by
@@ -257,7 +258,7 @@ theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) :
             exact Nat.lt_add_of_pos_right (Nat.two_pow_pos j)
       simp only [hyp y y_lt_x]
       if i_lt_j : i < j then
-        rw [ Nat.add_comm _ (2^_), testBit_two_pow_add_gt i_lt_j]
+        rw [Nat.add_comm _ (2^_), testBit_two_pow_add_gt i_lt_j]
       else
         simp [i_lt_j]
 
@@ -402,12 +403,12 @@ theorem and_pow_two_identity {x : Nat} (lt : x < 2^n) : x &&& 2^n-1 = x := by
 
 /-! ### lor -/
 
-@[simp] theorem or_zero (x : Nat) : 0 ||| x = x := by
+@[simp] theorem zero_or (x : Nat) : 0 ||| x = x := by
   simp only [HOr.hOr, OrOp.or, lor]
   unfold bitwise
   simp [@eq_comm _ 0]
 
-@[simp] theorem zero_or (x : Nat) : x ||| 0 = x := by
+@[simp] theorem or_zero (x : Nat) : x ||| 0 = x := by
   simp only [HOr.hOr, OrOp.or, lor]
   unfold bitwise
   simp [@eq_comm _ 0]

src/Init/Data/Nat/Div.lean

@@ -82,22 +82,34 @@ decreasing_by apply div_rec_lemma; assumption
 
 @[extern "lean_nat_mod"]
 protected def mod : @& Nat → @& Nat → Nat
-  /- This case is not needed mathematically as the case below is equal to it; however, it makes
-  `0 % n = 0` true definitionally rather than just propositionally.
-  This property is desirable for `Fin n`, as it means `(ofNat 0 : Fin n).val = 0` by definition.
-  Primarily, this is valuable because mathlib in Lean3 assumed this was true definitionally, and so
-  keeping this definitional equality makes mathlib easier to port to mathlib4. -/
+  /-
+  Nat.modCore is defined by well-founded recursion and thus irreducible. Nevertheless it is
+  desireable if trivial `Nat.mod` calculations, namely
+  * `Nat.mod 0 m` for all `m`
+  * `Nat.mod n (m+n)` for concrete literals `n`
+  reduce definitionally.
+  This property is desirable for `Fin n` literals, as it means `(ofNat 0 : Fin n).val = 0` by
+  definition.
+   -/
   | 0, _ => 0
-  | x@(_ + 1), y => Nat.modCore x y
+  | n@(_ + 1), m =>
+    if m ≤ n -- NB: if n < m does not reduce as well as `m ≤ n`!
+    then Nat.modCore n m
+    else n
 
 instance instMod : Mod Nat := ⟨Nat.mod⟩
 
-protected theorem modCore_eq_mod (x y : Nat) : Nat.modCore x y = x % y := by
-  cases x with
-  | zero =>
+protected theorem modCore_eq_mod (n m : Nat) : Nat.modCore n m = n % m := by
+  show Nat.modCore n m = Nat.mod n m
+  match n, m with
+  | 0, _ =>
     rw [Nat.modCore]
     exact if_neg fun ⟨hlt, hle⟩ => Nat.lt_irrefl _ (Nat.lt_of_lt_of_le hlt hle)
-  | succ x => rfl
+  | (_ + 1), _ =>
+    rw [Nat.mod]; dsimp
+    refine iteInduction (fun _ => rfl) (fun h => ?false) -- cannot use `split` this early yet
+    rw [Nat.modCore]
+    exact if_neg fun ⟨_hlt, hle⟩ => h hle
 
 theorem mod_eq (x y : Nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x := by
   rw [←Nat.modCore_eq_mod, ←Nat.modCore_eq_mod, Nat.modCore]

src/Init/Data/Nat/Gcd.lean

@@ -37,11 +37,11 @@ def gcd (m n : @& Nat) : Nat :=
   termination_by m
   decreasing_by simp_wf; apply mod_lt _ (zero_lt_of_ne_zero _); assumption
 
-@[simp] theorem gcd_zero_left (y : Nat) : gcd 0 y = y :=
-  rfl
+@[simp] theorem gcd_zero_left (y : Nat) : gcd 0 y = y := by
+  rw [gcd]; rfl
 
-theorem gcd_succ (x y : Nat) : gcd (succ x) y = gcd (y % succ x) (succ x) :=
-  rfl
+theorem gcd_succ (x y : Nat) : gcd (succ x) y = gcd (y % succ x) (succ x) := by
+  rw [gcd]; rfl
 
 @[simp] theorem gcd_one_left (n : Nat) : gcd 1 n = 1 := by
   rw [gcd_succ, mod_one]
@@ -64,7 +64,7 @@ instance : Std.IdempotentOp gcd := ⟨gcd_self⟩
 
 theorem gcd_rec (m n : Nat) : gcd m n = gcd (n % m) m :=
   match m with
-  | 0 => by have := (mod_zero n).symm; rwa [gcd_zero_right]
+  | 0 => by have := (mod_zero n).symm; rwa [gcd, gcd_zero_right]
   | _ + 1 => by simp [gcd_succ]
 
 @[elab_as_elim] theorem gcd.induction {P : Nat → Nat → Prop} (m n : Nat)

src/Init/Data/Nat/Lemmas.lean

@@ -137,14 +137,14 @@ protected theorem sub_le_iff_le_add' {a b c : Nat} : a - b ≤ c ↔ a ≤ b + c
 protected theorem le_sub_iff_add_le {n : Nat} (h : k ≤ m) : n ≤ m - k ↔ n + k ≤ m :=
   ⟨Nat.add_le_of_le_sub h, Nat.le_sub_of_add_le⟩
 
-@[deprecated Nat.le_sub_iff_add_le]
+@[deprecated Nat.le_sub_iff_add_le (since := "2024-02-19")]
 protected theorem add_le_to_le_sub (n : Nat) (h : m ≤ k) : n + m ≤ k ↔ n ≤ k - m :=
   (Nat.le_sub_iff_add_le h).symm
 
 protected theorem add_le_of_le_sub' {n k m : Nat} (h : m ≤ k) : n ≤ k - m → m + n ≤ k :=
   Nat.add_comm .. ▸ Nat.add_le_of_le_sub h
 
-@[deprecated Nat.add_le_of_le_sub']
+@[deprecated Nat.add_le_of_le_sub' (since := "2024-02-19")]
 protected theorem add_le_of_le_sub_left {n k m : Nat} (h : m ≤ k) : n ≤ k - m → m + n ≤ k :=
   Nat.add_le_of_le_sub' h
 
@@ -401,11 +401,11 @@ protected theorem mul_min_mul_left (a b c : Nat) : min (a * b) (a * c) = a * min
 
 /-! ### mul -/
 
-@[deprecated Nat.mul_le_mul_left]
+@[deprecated Nat.mul_le_mul_left (since := "2024-02-19")]
 protected theorem mul_le_mul_of_nonneg_left {a b c : Nat} : a ≤ b → c * a ≤ c * b :=
   Nat.mul_le_mul_left c
 
-@[deprecated Nat.mul_le_mul_right]
+@[deprecated Nat.mul_le_mul_right (since := "2024-02-19")]
 protected theorem mul_le_mul_of_nonneg_right {a b c : Nat} : a ≤ b → a * c ≤ b * c :=
   Nat.mul_le_mul_right c
 
@@ -478,6 +478,7 @@ protected theorem mul_lt_mul_of_lt_of_lt {a b c d : Nat} (hac : a < c) (hbd : b
 
 theorem succ_mul_succ (a b) : succ a * succ b = a * b + a + b + 1 := by
   rw [succ_mul, mul_succ]; rfl
+
 theorem mul_le_add_right (m k n : Nat) : k * m ≤ m + n ↔ (k-1) * m ≤ n := by
   match k with
   | 0 =>
@@ -677,6 +678,10 @@ protected theorem pow_lt_pow_iff_right {a n m : Nat} (h : 1 < a) :
 
 /-! ### log2 -/
 
+@[simp]
+theorem log2_zero : Nat.log2 0 = 0 := by
+  simp [Nat.log2]
+
 theorem le_log2 (h : n ≠ 0) : k ≤ n.log2 ↔ 2 ^ k ≤ n := by
   match k with
   | 0 => simp [show 1 ≤ n from Nat.pos_of_ne_zero h]
@@ -697,7 +702,7 @@ theorem log2_self_le (h : n ≠ 0) : 2 ^ n.log2 ≤ n := (le_log2 h).1 (Nat.le_r
 
 theorem lt_log2_self : n < 2 ^ (n.log2 + 1) :=
   match n with
-  | 0 => Nat.zero_lt_two
+  | 0 => by simp
   | n+1 => (log2_lt n.succ_ne_zero).1 (Nat.le_refl _)
 
 /-! ### dvd -/

src/Init/Data/Option/Basic.lean

@@ -18,8 +18,8 @@ def getM [Alternative m] : Option α → m α
   | none     => failure
   | some a   => pure a
 
-@[deprecated getM] def toMonad [Monad m] [Alternative m] : Option α → m α :=
-  getM
+@[deprecated getM (since := "2024-04-17")]
+def toMonad [Monad m] [Alternative m] : Option α → m α := getM
 
 /-- Returns `true` on `some x` and `false` on `none`. -/
 @[inline] def isSome : Option α → Bool

src/Init/Data/Stream.lean

@@ -94,7 +94,7 @@ instance : Stream (Subarray α) α where
   next? s :=
     if h : s.start < s.stop then
       have : s.start + 1 ≤ s.stop := Nat.succ_le_of_lt h
-      some (s.as.get ⟨s.start, Nat.lt_of_lt_of_le h s.stop_le_array_size⟩,
+      some (s.array.get ⟨s.start, Nat.lt_of_lt_of_le h s.stop_le_array_size⟩,
         { s with start := s.start + 1, start_le_stop := this })
     else
       none

src/Init/Data/String/Basic.lean

@@ -24,23 +24,59 @@ instance : LT String :=
 instance decLt (s₁ s₂ : @& String) : Decidable (s₁ < s₂) :=
   List.hasDecidableLt s₁.data s₂.data
 
+@[reducible] protected def le (a b : String) : Prop := ¬ b < a
+
+instance : LE String :=
+  ⟨String.le⟩
+
+instance decLE (s₁ s₂ : String) : Decidable (s₁ ≤ s₂) :=
+  inferInstanceAs (Decidable (Not _))
+
+/--
+Returns the length of a string in Unicode code points.
+
+Examples:
+* `"".length = 0`
+* `"abc".length = 3`
+* `"L∃∀N".length = 4`
+-/
 @[extern "lean_string_length"]
 def length : (@& String) → Nat
   | ⟨s⟩ => s.length
 
-/-- The internal implementation uses dynamic arrays and will perform destructive updates
-   if the String is not shared. -/
+/--
+Pushes a character onto the end of a string.
+
+The internal implementation uses dynamic arrays and will perform destructive updates
+if the string is not shared.
+
+Example: `"abc".push 'd' = "abcd"`
+-/
 @[extern "lean_string_push"]
 def push : String → Char → String
   | ⟨s⟩, c => ⟨s ++ [c]⟩
 
-/-- The internal implementation uses dynamic arrays and will perform destructive updates
-   if the String is not shared. -/
+/--
+Appends two strings.
+
+The internal implementation uses dynamic arrays and will perform destructive updates
+if the string is not shared.
+
+Example: `"abc".append "def" = "abcdef"`
+-/
 @[extern "lean_string_append"]
 def append : String → (@& String) → String
   | ⟨a⟩, ⟨b⟩ => ⟨a ++ b⟩
 
-/-- O(n) in the runtime, where n is the length of the String -/
+/--
+Converts a string to a list of characters.
+
+Even though the logical model of strings is as a structure that wraps a list of characters,
+this operation takes time and space linear in the length of the string, because the compiler
+uses an optimized representation as dynamic arrays.
+
+Example: `"abc".toList = ['a', 'b', 'c']`
+-/
 def toList (s : String) : List Char :=
   s.data
 
@@ -59,9 +95,17 @@ def utf8GetAux : List Char → Pos → Pos → Char
   | c::cs, i, p => if i = p then c else utf8GetAux cs (i + c) p
 
 /--
-  Return character at position `p`. If `p` is not a valid position
-  returns `(default : Char)`.
-  See `utf8GetAux` for the reference implementation.
+Returns the character at position `p` of a string. If `p` is not a valid position,
+returns `(default : Char)`.
+
+See `utf8GetAux` for the reference implementation.
+
+Examples:
+* `"abc".get ⟨1⟩ = 'b'`
+* `"abc".get ⟨3⟩ = (default : Char) = 'A'`
+
+Positions can also be invalid if a byte index points into the middle of a multi-byte UTF-8
+character. For example,`"L∃∀N".get ⟨2⟩ = (default : Char) = 'A'`.
 -/
 @[extern "lean_string_utf8_get"]
 def get (s : @& String) (p : @& Pos) : Char :=
@@ -72,12 +116,30 @@ def utf8GetAux? : List Char → Pos → Pos → Option Char
   | [],    _, _ => none
   | c::cs, i, p => if i = p then c else utf8GetAux? cs (i + c) p
 
+/--
+Returns the character at position `p`. If `p` is not a valid position, returns `none`.
+
+Examples:
+* `"abc".get? ⟨1⟩ = some 'b'`
+* `"abc".get? ⟨3⟩ = none`
+
+Positions can also be invalid if a byte index points into the middle of a multi-byte UTF-8
+character. For example, `"L∃∀N".get? ⟨2⟩ = none`
+-/
 @[extern "lean_string_utf8_get_opt"]
 def get? : (@& String) → (@& Pos) → Option Char
   | ⟨s⟩, p => utf8GetAux? s 0 p
 
 /--
-  Similar to `get`, but produces a panic error message if `p` is not a valid `String.Pos`.
+Returns the character at position `p` of a string. If `p` is not a valid position,
+returns `(default : Char)` and produces a panic error message.
+
+Examples:
+* `"abc".get! ⟨1⟩ = 'b'`
+* `"abc".get! ⟨3⟩` panics
+
+Positions can also be invalid if a byte index points into the middle of a multi-byte UTF-8 character. For example,
+`"L∃∀N".get! ⟨2⟩` panics.
 -/
 @[extern "lean_string_utf8_get_bang"]
 def get! (s : @& String) (p : @& Pos) : Char :=
@@ -89,13 +151,48 @@ def utf8SetAux (c' : Char) : List Char → Pos → Pos → List Char
   | c::cs, i, p =>
     if i = p then (c'::cs) else c::(utf8SetAux c' cs (i + c) p)
 
+/--
+Replaces the character at a specified position in a string with a new character. If the position
+is invalid, the string is returned unchanged.
+
+If both the replacement character and the replaced character are ASCII characters and the string
+is not shared, destructive updates are used.
+
+Examples:
+* `"abc".set ⟨1⟩ 'B' = "aBc"`
+* `"abc".set ⟨3⟩ 'D' = "abc"`
+* `"L∃∀N".set ⟨4⟩ 'X' = "L∃XN"`
+
+Because `'∃'` is a multi-byte character, the byte index `2` in `L∃∀N` is an invalid position,
+so `"L∃∀N".set ⟨2⟩ 'X' = "L∃∀N"`.
+-/
 @[extern "lean_string_utf8_set"]
 def set : String → (@& Pos) → Char → String
   | ⟨s⟩, i, c => ⟨utf8SetAux c s 0 i⟩
 
+/--
+Replaces the character at position `p` in the string `s` with the result of applying `f` to that character.
+If `p` is an invalid position, the string is returned unchanged.
+
+Examples:
+* `abc.modify ⟨1⟩ Char.toUpper = "aBc"`
+* `abc.modify ⟨3⟩ Char.toUpper = "abc"`
+-/
 def modify (s : String) (i : Pos) (f : Char → Char) : String :=
   s.set i <| f <| s.get i
 
+/--
+Returns the next position in a string after position `p`. If `p` is not a valid position or `p = s.endPos`,
+the result is unspecified.
+
+Examples:
+* `"abc".next ⟨1⟩ = String.Pos.mk 2`
+* `"L∃∀N".next ⟨1⟩ = String.Pos.mk 4`, since `'∃'` is a multi-byte UTF-8 character
+
+Cases where the result is unspecified:
+* `"abc".next ⟨3⟩`, since `3 = s.endPos`
+* `"L∃∀N".next ⟨2⟩`, since `2` points into the middle of a multi-byte UTF-8 character
+-/
 @[extern "lean_string_utf8_next"]
 def next (s : @& String) (p : @& Pos) : Pos :=
   let c := get s p
@@ -594,13 +691,15 @@ def substrEq (s1 : String) (off1 : String.Pos) (s2 : String) (off2 : String.Pos)
   off1.byteIdx + sz ≤ s1.endPos.byteIdx && off2.byteIdx + sz ≤ s2.endPos.byteIdx && loop off1 off2 { byteIdx := off1.byteIdx + sz }
 where
   loop (off1 off2 stop1 : Pos) :=
-    if h : off1.byteIdx < stop1.byteIdx then
+    if _h : off1.byteIdx < stop1.byteIdx then
       let c₁ := s1.get off1
       let c₂ := s2.get off2
-      have := Nat.sub_lt_sub_left h (Nat.add_lt_add_left (one_le_csize c₁) off1.1)
       c₁ == c₂ && loop (off1 + c₁) (off2 + c₂) stop1
     else true
   termination_by stop1.1 - off1.1
+  decreasing_by
+    have := Nat.sub_lt_sub_left _h (Nat.add_lt_add_left (one_le_csize c₁) off1.1)
+    decreasing_tactic
 
 /-- Return true iff `p` is a prefix of `s` -/
 def isPrefixOf (p : String) (s : String) : Bool :=

src/Init/Data/String/Extra.lean

@@ -132,13 +132,17 @@ theorem Iterator.sizeOf_next_lt_of_hasNext (i : String.Iterator) (h : i.hasNext)
   cases i; rename_i s pos; simp [Iterator.next, Iterator.sizeOf_eq]; simp [Iterator.hasNext] at h
   exact Nat.sub_lt_sub_left h (String.lt_next s pos)
 
-macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply String.Iterator.sizeOf_next_lt_of_hasNext; assumption)
+macro_rules
+| `(tactic| decreasing_trivial) =>
+  `(tactic| with_reducible apply String.Iterator.sizeOf_next_lt_of_hasNext; assumption)
 
 theorem Iterator.sizeOf_next_lt_of_atEnd (i : String.Iterator) (h : ¬ i.atEnd = true) : sizeOf i.next < sizeOf i :=
   have h : i.hasNext := decide_eq_true <| Nat.gt_of_not_le <| mt decide_eq_true h
   sizeOf_next_lt_of_hasNext i h
 
-macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply String.Iterator.sizeOf_next_lt_of_atEnd; assumption)
+macro_rules
+| `(tactic| decreasing_trivial) =>
+  `(tactic| with_reducible apply String.Iterator.sizeOf_next_lt_of_atEnd; assumption)
 
 namespace Iterator
 

src/Init/Grind.lean

@@ -0,0 +1,9 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Grind.Norm
+import Init.Grind.Tactics
+import Init.Grind.Lemmas

src/Init/Grind/Lemmas.lean

@@ -0,0 +1,14 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Core
+
+namespace Lean.Grind
+
+theorem intro_with_eq (p p' q : Prop) (he : p = p') (h : p' → q) : p → q :=
+  fun hp => h (he.mp hp)
+
+end Lean.Grind

src/Init/Grind/Norm.lean

@@ -0,0 +1,110 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.SimpLemmas
+import Init.Classical
+import Init.ByCases
+
+namespace Lean.Grind
+/-!
+Normalization theorems for the `grind` tactic.
+
+We are also going to use simproc's in the future.
+-/
+
+-- Not
+attribute [grind_norm] Classical.not_not
+
+-- Ne
+attribute [grind_norm] ne_eq
+
+-- Iff
+@[grind_norm] theorem iff_eq (p q : Prop) : (p ↔ q) = (p = q) := by
+  by_cases p <;> by_cases q <;> simp [*]
+
+-- Eq
+attribute [grind_norm] eq_self heq_eq_eq
+
+-- Prop equality
+@[grind_norm] theorem eq_true_eq (p : Prop) : (p = True) = p := by simp
+@[grind_norm] theorem eq_false_eq (p : Prop) : (p = False) = ¬p := by simp
+@[grind_norm] theorem not_eq_prop (p q : Prop) : (¬(p = q)) = (p = ¬q) := by
+  by_cases p <;> by_cases q <;> simp [*]
+
+-- True
+attribute [grind_norm] not_true
+
+-- False
+attribute [grind_norm] not_false_eq_true
+
+-- Implication as a clause
+@[grind_norm] theorem imp_eq (p q : Prop) : (p → q) = (¬ p ∨ q) := by
+  by_cases p <;> by_cases q <;> simp [*]
+
+-- And
+@[grind_norm↓] theorem not_and (p q : Prop) : (¬(p ∧ q)) = (¬p ∨ ¬q) := by
+  by_cases p <;> by_cases q <;> simp [*]
+attribute [grind_norm] and_true true_and and_false false_and and_assoc
+
+-- Or
+attribute [grind_norm↓] not_or
+attribute [grind_norm] or_true true_or or_false false_or or_assoc
+
+-- ite
+attribute [grind_norm] ite_true ite_false
+@[grind_norm↓] theorem not_ite {_ : Decidable p} (q r : Prop) : (¬ite p q r) = ite p (¬q) (¬r) := by
+  by_cases p <;> simp [*]
+
+-- Forall
+@[grind_norm↓] theorem not_forall (p : α → Prop) : (¬∀ x, p x) = ∃ x, ¬p x := by simp
+attribute [grind_norm] forall_and
+
+-- Exists
+@[grind_norm↓] theorem not_exists (p : α → Prop) : (¬∃ x, p x) = ∀ x, ¬p x := by simp
+attribute [grind_norm] exists_const exists_or
+
+-- Bool cond
+@[grind_norm] theorem cond_eq_ite (c : Bool) (a b : α) : cond c a b = ite c a b := by
+  cases c <;> simp [*]
+
+-- Bool or
+attribute [grind_norm]
+  Bool.or_false Bool.or_true Bool.false_or Bool.true_or Bool.or_eq_true Bool.or_assoc
+
+-- Bool and
+attribute [grind_norm]
+  Bool.and_false Bool.and_true Bool.false_and Bool.true_and Bool.and_eq_true Bool.and_assoc
+
+-- Bool not
+attribute [grind_norm]
+  Bool.not_not
+
+-- beq
+attribute [grind_norm] beq_iff_eq
+
+-- bne
+attribute [grind_norm] bne_iff_ne
+
+-- Bool not eq true/false
+attribute [grind_norm] Bool.not_eq_true Bool.not_eq_false
+
+-- decide
+attribute [grind_norm] decide_eq_true_eq decide_not not_decide_eq_true
+
+-- Nat LE
+attribute [grind_norm] Nat.le_zero_eq
+
+-- Nat/Int LT
+@[grind_norm] theorem Nat.lt_eq (a b : Nat) : (a < b) = (a + 1 ≤ b) := by
+  simp [Nat.lt, LT.lt]
+
+@[grind_norm] theorem Int.lt_eq (a b : Int) : (a < b) = (a + 1 ≤ b) := by
+  simp [Int.lt, LT.lt]
+
+-- GT GE
+attribute [grind_norm] GT.gt GE.ge
+
+end Lean.Grind

src/Init/Grind/Tactics.lean

@@ -0,0 +1,14 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Tactics
+
+namespace Lean.Grind
+/-!
+`grind` tactic and related tactics.
+-/
+
+end Lean.Grind

src/Init/Meta.lean

@@ -1057,6 +1057,7 @@ where
     else
       Syntax.mkCApp (Name.mkStr2 "Array" ("mkArray" ++ toString xs.size)) args
   termination_by xs.size - i
+  decreasing_by decreasing_trivial_pre_omega
 
 instance [Quote α `term] : Quote (Array α) `term where
   quote := quoteArray

src/Init/MetaTypes.lean

@@ -169,6 +169,11 @@ structure Config where
   That is, given a local context containing entry `x : t := e`, the free variable `x` reduces to `e`.
   -/
   zetaDelta         : Bool := false
+  /--
+  When `index` (default : `true`) is `false`, `simp` will only use the root symbol
+  to find candidate `simp` theorems. It approximates Lean 3 `simp` behavior.
+  -/
+  index             : Bool := true
   deriving Inhabited, BEq
 
 -- Configuration object for `simp_all`

src/Init/Notation.lean

@@ -296,7 +296,7 @@ macro_rules | `($x - $y)   => `(binop% HSub.hSub $x $y)
 macro_rules | `($x * $y)   => `(binop% HMul.hMul $x $y)
 macro_rules | `($x / $y)   => `(binop% HDiv.hDiv $x $y)
 macro_rules | `($x % $y)   => `(binop% HMod.hMod $x $y)
--- exponentiation should be considered a right action (#2220)
+-- exponentiation should be considered a right action (#2854)
 macro_rules | `($x ^ $y)   => `(rightact% HPow.hPow $x $y)
 macro_rules | `($x ++ $y)  => `(binop% HAppend.hAppend $x $y)
 macro_rules | `(- $x)      => `(unop% Neg.neg $x)
@@ -687,4 +687,27 @@ syntax (name := checkSimp) "#check_simp " term "~>" term : command
 -/
 syntax (name := checkSimpFailure) "#check_simp " term "!~>" : command
 
+/--
+The `seal foo` command ensures that the definition of `foo` is sealed, meaning it is marked as `[irreducible]`.
+This command is particularly useful in contexts where you want to prevent the reduction of `foo` in proofs.
+
+In terms of functionality, `seal foo` is equivalent to `attribute [local irreducible] foo`.
+This attribute specifies that `foo` should be treated as irreducible only within the local scope,
+which helps in maintaining the desired abstraction level without affecting global settings.
+-/
+syntax "seal " (ppSpace ident)+ : command
+
+/--
+The `unseal foo` command ensures that the definition of `foo` is unsealed, meaning it is marked as `[semireducible]`, the
+default reducibility setting. This command is useful when you need to allow some level of reduction of `foo` in proofs.
+
+Functionally, `unseal foo` is equivalent to `attribute [local semireducible] foo`.
+Applying this attribute makes `foo` semireducible only within the local scope.
+-/
+syntax "unseal " (ppSpace ident)+ : command
+
+macro_rules
+  | `(seal $fs:ident*) => `(attribute [local irreducible] $fs:ident*)
+  | `(unseal $fs:ident*) => `(attribute [local semireducible] $fs:ident*)
+
 end Parser

src/Init/NotationExtra.lean

@@ -87,6 +87,7 @@ macro:35 xs:bracketedExplicitBinders " × " b:term:35  : term => expandBrackedBi
 macro:35 xs:bracketedExplicitBinders " ×' " b:term:35 : term => expandBrackedBinders ``PSigma xs b
 end
 
+namespace Lean
 -- first step of a `calc` block
 syntax calcFirstStep := ppIndent(colGe term (" := " term)?)
 -- enforce indentation of calc steps so we know when to stop parsing them
@@ -136,6 +137,7 @@ syntax (name := calcTactic) "calc" calcSteps : tactic
 @[inherit_doc «calc»]
 macro tk:"calc" steps:calcSteps : conv =>
   `(conv| tactic => calc%$tk $steps)
+end Lean
 
 @[app_unexpander Unit.unit] def unexpandUnit : Lean.PrettyPrinter.Unexpander
   | `($(_)) => `(())
@@ -361,6 +363,7 @@ macro_rules
   | `(letI $_:ident $_* : $_ := $_; $_) => Lean.Macro.throwUnsupported -- handled by elab
 
 
+namespace Lean
 syntax cdotTk := patternIgnore("· " <|> ". ")
 /-- `· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. -/
 syntax (name := cdot) cdotTk tacticSeqIndentGt : tactic
@@ -368,12 +371,11 @@ syntax (name := cdot) cdotTk tacticSeqIndentGt : tactic
 /--
   Similar to `first`, but succeeds only if one the given tactics solves the current goal.
 -/
-syntax (name := solve) "solve" withPosition((ppDedent(ppLine) colGe "| " tacticSeq)+) : tactic
+syntax (name := solveTactic) "solve" withPosition((ppDedent(ppLine) colGe "| " tacticSeq)+) : tactic
 
 macro_rules
   | `(tactic| solve $[| $ts]* ) => `(tactic| focus first $[| ($ts); done]*)
 
-namespace Lean
 /-! # `repeat` and `while` notation -/
 
 inductive Loop where

src/Init/Omega/Coeffs.lean

@@ -68,7 +68,7 @@ abbrev map (f : Int → Int) (xs : Coeffs) : Coeffs := List.map f xs
 /-- Shim for `.enum.find?`. -/
 abbrev findIdx? (f : Int → Bool) (xs : Coeffs) : Option Nat :=
   -- List.findIdx? f xs
-  -- We could avoid `Std.Data.List.Basic` by using the less efficient:
+  -- We could avoid `Batteries.Data.List.Basic` by using the less efficient:
   xs.enum.find? (f ·.2) |>.map (·.1)
 /-- Shim for `IntList.bmod`. -/
 abbrev bmod (x : Coeffs) (m : Nat) : Coeffs := IntList.bmod x m

src/Init/Prelude.lean

@@ -4372,7 +4372,7 @@ def defaultMaxRecDepth := 512
 
 /-- The message to display on stack overflow. -/
 def maxRecDepthErrorMessage : String :=
-  "maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)"
+  "maximum recursion depth has been reached\nuse `set_option maxRecDepth <num>` to increase limit\nuse `set_option diagnostics true` to get diagnostic information"
 
 namespace Syntax
 

src/Init/System/IO.lean

@@ -210,8 +210,44 @@ def sleep (ms : UInt32) : BaseIO Unit :=
 /-- Request cooperative cancellation of the task. The task must explicitly call `IO.checkCanceled` to react to the cancellation. -/
 @[extern "lean_io_cancel"] opaque cancel : @& Task α → BaseIO Unit
 
+/-- The current state of a `Task` in the Lean runtime's task manager. -/
+inductive TaskState
+  /--
+  The `Task` is waiting to be run.
+  It can be waiting for dependencies to complete or
+  sitting in the task manager queue waiting for a thread to run on.
+  -/
+  | waiting
+  /--
+  The `Task` is actively running on a thread or,
+  in the case of a `Promise`, waiting for a call to `IO.Promise.resolve`.
+  -/
+  | running
+  /--
+  The `Task` has finished running and its result is available.
+  Calling `Task.get` or `IO.wait` on the task will not block.
+  -/
+  | finished
+  deriving Inhabited, Repr, DecidableEq, Ord
+
+instance : LT TaskState := ltOfOrd
+instance : LE TaskState := leOfOrd
+instance : Min TaskState := minOfLe
+instance : Max TaskState := maxOfLe
+
+protected def TaskState.toString : TaskState → String
+  | .waiting => "waiting"
+  | .running => "running"
+  | .finished => "finished"
+
+instance : ToString TaskState := ⟨TaskState.toString⟩
+
+/-- Returns current state of the `Task` in the Lean runtime's task manager. -/
+@[extern "lean_io_get_task_state"] opaque getTaskState : @& Task α → BaseIO TaskState
+
 /-- Check if the task has finished execution, at which point calling `Task.get` will return immediately. -/
-@[extern "lean_io_has_finished"] opaque hasFinished : @& Task α → BaseIO Bool
+@[inline] def hasFinished (task : Task α) : BaseIO Bool := do
+  return (← getTaskState task) matches .finished
 
 /-- Wait for the task to finish, then return its result. -/
 @[extern "lean_io_wait"] opaque wait (t : Task α) : BaseIO α :=
@@ -625,7 +661,13 @@ partial def FS.removeDirAll (p : FilePath) : IO Unit := do
 
 namespace Process
 
-/-- Returns the process ID of the current process. -/
+/-- Returns the current working directory of the calling process. -/
+@[extern "lean_io_process_get_current_dir"] opaque getCurrentDir : IO FilePath
+
+/-- Sets the current working directory of the calling process. -/
+@[extern "lean_io_process_set_current_dir"] opaque setCurrentDir (path : @& FilePath) : IO Unit
+
+/-- Returns the process ID of the calling process. -/
 @[extern "lean_io_process_get_pid"] opaque getPID : BaseIO UInt32
 
 inductive Stdio where

src/Init/Tactics.lean

@@ -368,7 +368,7 @@ for new reflexive relations.
 Remark: `rfl` is an extensible tactic. We later add `macro_rules` to try different
 reflexivity theorems (e.g., `Iff.rfl`).
 -/
-macro "rfl" : tactic => `(tactic| fail "The rfl tactic failed. Possible reasons:
+macro "rfl" : tactic => `(tactic| case' _ => fail "The rfl tactic failed. Possible reasons:
 - The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
 - The arguments of the relation are not equal.
 Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.")
@@ -835,7 +835,7 @@ syntax (name := renameI) "rename_i" (ppSpace colGt binderIdent)+ : tactic
 /--
 `repeat tac` repeatedly applies `tac` to the main goal until it fails.
 That is, if `tac` produces multiple subgoals, only subgoals up to the first failure will be visited.
-The `Std` library provides `repeat'` which repeats separately in each subgoal.
+The `Batteries` library provides `repeat'` which repeats separately in each subgoal.
 -/
 syntax "repeat " tacticSeq : tactic
 macro_rules
@@ -1266,7 +1266,7 @@ Optional arguments passed via a configuration argument as `solve_by_elim (config
   but it is often useful to change to `.reducible`,
   so semireducible definitions will not be unfolded when trying to apply a lemma.
 
-See also the doc-comment for `Std.Tactic.BacktrackConfig` for the options
+See also the doc-comment for `Lean.Meta.Tactic.Backtrack.BacktrackConfig` for the options
 `proc`, `suspend`, and `discharge` which allow further customization of `solve_by_elim`.
 Both `apply_assumption` and `apply_rules` are implemented via these hooks.
 -/
@@ -1425,6 +1425,16 @@ If there are several with the same priority, it is uses the "most recent one". E
 -/
 syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? (ppSpace prio)? : attr
 
+/--
+Theorems tagged with the `grind_norm` attribute are used by the `grind` tactic normalizer/pre-processor.
+-/
+syntax (name := grind_norm) "grind_norm" (Tactic.simpPre <|> Tactic.simpPost)? (ppSpace prio)? : attr
+
+/--
+Simplification procedures tagged with the `grind_norm_proc` attribute are used by the `grind` tactic normalizer/pre-processor.
+-/
+syntax (name := grind_norm_proc) "grind_norm_proc" (Tactic.simpPre <|> Tactic.simpPost)? : attr
+
 
 /-- The possible `norm_cast` kinds: `elim`, `move`, or `squash`. -/
 syntax normCastLabel := &"elim" <|> &"move" <|> &"squash"

src/Init/WFTactics.lean

@@ -25,9 +25,16 @@ syntax "decreasing_trivial" : tactic
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| (simp (config := { arith := true, failIfUnchanged := false })) <;> done)
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| omega)
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| assumption)
-macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.sub_succ_lt_self; assumption) -- a - (i+1) < a - i if i < a
-macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.pred_lt'; assumption) -- i-1 < i if j < i
-macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.pred_lt; assumption)  -- i-1 < i if i ≠ 0
+
+/--
+Variant of `decreasing_trivial` that does not use `omega`, intended to be used in core modules
+before `omega` is available.
+-/
+syntax "decreasing_trivial_pre_omega" : tactic
+macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.sub_succ_lt_self; assumption) -- a - (i+1) < a - i if i < a
+macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.pred_lt'; assumption) -- i-1 < i if j < i
+macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.pred_lt; assumption)  -- i-1 < i if i ≠ 0
+
 
 /-- Constructs a proof of decreasing along a well founded relation, by applying
 lexicographic order lemmas and using `ts` to solve the base case. If it fails,

src/Lean.lean

@@ -37,3 +37,4 @@ import Lean.Log
 import Lean.Linter
 import Lean.SubExpr
 import Lean.LabelAttribute
+import Lean.AddDecl

src/Lean/AddDecl.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.CoreM
+
+namespace Lean
+
+def Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration) : Except KernelException Environment :=
+  addDeclCore env (Core.getMaxHeartbeats opts).toUSize decl
+
+def Environment.addAndCompile (env : Environment) (opts : Options) (decl : Declaration) : Except KernelException Environment := do
+  let env ← addDecl env opts decl
+  compileDecl env opts decl
+
+def addDecl (decl : Declaration) : CoreM Unit := do
+  profileitM Exception "type checking" (← getOptions) do
+    withTraceNode `Kernel (fun _ => return m!"typechecking declaration") do
+      if !(← MonadLog.hasErrors) && decl.hasSorry then
+        logWarning "declaration uses 'sorry'"
+      match (← getEnv).addDecl (← getOptions) decl with
+      | .ok    env => setEnv env
+      | .error ex  => throwKernelException ex
+
+def addAndCompile (decl : Declaration) : CoreM Unit := do
+  addDecl decl
+  compileDecl decl
+
+end Lean

src/Lean/Compiler/ExternAttr.lean

@@ -66,12 +66,13 @@ builtin_initialize externAttr : ParametricAttribute ExternAttrData ←
     descr := "builtin and foreign functions"
     getParam := fun _ stx => syntaxToExternAttrData stx
     afterSet := fun declName _ => do
-      let mut env ← getEnv
-      if env.isProjectionFn declName || env.isConstructor declName then do
-        env ← ofExcept <| addExtern env declName
+      let env ← getEnv
+      if env.isProjectionFn declName || env.isConstructor declName then
+        if let some (.thmInfo ..) := env.find? declName then
+          -- We should not mark theorems as extern
+          return ()
+        let env ← ofExcept <| addExtern env declName
         setEnv env
-      else
-        pure ()
   }
 
 @[export lean_get_extern_attr_data]

src/Lean/Compiler/IR/RC.lean

@@ -9,9 +9,10 @@ import Lean.Compiler.IR.CompilerM
 import Lean.Compiler.IR.LiveVars
 
 namespace Lean.IR.ExplicitRC
-/-! Insert explicit RC instructions. So, it assumes the input code does not contain `inc` nor `dec` instructions.
-   This transformation is applied before lower level optimizations
-   that introduce the instructions `release` and `set`
+/-!
+Insert explicit RC instructions. So, it assumes the input code does not contain `inc` nor `dec` instructions.
+This transformation is applied before lower level optimizations
+that introduce the instructions `release` and `set`
 -/
 
 structure VarInfo where

src/Lean/Compiler/IR/ResetReuse.lean

@@ -9,152 +9,238 @@ import Lean.Compiler.IR.LiveVars
 import Lean.Compiler.IR.Format
 
 namespace Lean.IR.ResetReuse
-/-! Remark: the insertResetReuse transformation is applied before we have
-   inserted `inc/dec` instructions, and performed lower level optimizations
-   that introduce the instructions `release` and `set`. -/
-
-/-! Remark: the functions `S`, `D` and `R` defined here implement the
-  corresponding functions in the paper "Counting Immutable Beans"
-
-  Here are the main differences:
-  - We use the State monad to manage the generation of fresh variable names.
-  - Support for join points, and `uset` and `sset` instructions for unboxed data.
-  - `D` uses the auxiliary function `Dmain`.
-  - `Dmain` returns a pair `(b, found)` to avoid quadratic behavior when checking
-    the last occurrence of the variable `x`.
-  - Because we have join points in the actual implementation, a variable may be live even if it
-    does not occur in a function body. See example at `livevars.lean`.
+/-!
+Remark: the insertResetReuse transformation is applied before we have
+inserted `inc/dec` instructions, and performed lower level optimizations
+that introduce the instructions `release` and `set`.
 -/
 
-private def mayReuse (c₁ c₂ : CtorInfo) : Bool :=
+/-!
+Remark: the functions `S`, `D` and `R` defined here implement the
+corresponding functions in the paper "Counting Immutable Beans"
+
+Here are the main differences:
+- We use the State monad to manage the generation of fresh variable names.
+- Support for join points, and `uset` and `sset` instructions for unboxed data.
+- `D` uses the auxiliary function `Dmain`.
+- `Dmain` returns a pair `(b, found)` to avoid quadratic behavior when checking
+  the last occurrence of the variable `x`.
+- Because we have join points in the actual implementation, a variable may be live even if it
+  does not occur in a function body. See example at `livevars.lean`.
+-/
+
+private def mayReuse (c₁ c₂ : CtorInfo) (relaxedReuse : Bool) : Bool :=
   c₁.size == c₂.size && c₁.usize == c₂.usize && c₁.ssize == c₂.ssize &&
   /- The following condition is a heuristic.
-     We don't want to reuse cells from different types even when they are compatible
+     If `relaxedReuse := false`, then we don't want to reuse cells from
+     different constructors even when they are compatible
      because it produces counterintuitive behavior. -/
-  c₁.name.getPrefix == c₂.name.getPrefix
+  (relaxedReuse || c₁.name.getPrefix == c₂.name.getPrefix)
 
-private partial def S (w : VarId) (c : CtorInfo) : FnBody → FnBody
-  | FnBody.vdecl x t v@(Expr.ctor c' ys) b   =>
-    if mayReuse c c' then
+/--
+Replace `ctor` applications with `reuse` applications if compatible.
+`w` contains the "memory cell" being reused.
+-/
+private partial def S (w : VarId) (c : CtorInfo) (relaxedReuse : Bool) (b : FnBody) : FnBody :=
+  go b
+where
+  go : FnBody → FnBody
+  | .vdecl x t v@(.ctor c' ys) b   =>
+    if mayReuse c c' relaxedReuse then
       let updtCidx := c.cidx != c'.cidx
-      FnBody.vdecl x t (Expr.reuse w c' updtCidx ys) b
+      .vdecl x t (.reuse w c' updtCidx ys) b
     else
-      FnBody.vdecl x t v (S w c b)
-  | FnBody.jdecl j ys v b   =>
-    let v' := S w c v
-    if v == v' then FnBody.jdecl j ys v (S w c b)
-    else FnBody.jdecl j ys v' b
-  | FnBody.case tid x xType alts    => FnBody.case tid x xType <| alts.map fun alt => alt.modifyBody (S w c)
+      .vdecl x t v (go b)
+  | .jdecl j ys v b   =>
+    let v' := go v
+    if v == v' then
+      .jdecl j ys v (go b)
+    else
+      .jdecl j ys v' b
+  | .case tid x xType alts =>
+    .case tid x xType <| alts.map fun alt => alt.modifyBody go
   | b =>
-    if b.isTerminal then b
-    else let
-      (instr, b) := b.split
-      instr.setBody (S w c b)
+    if b.isTerminal then
+      b
+    else
+      let (instr, b) := b.split
+      instr.setBody (go b)
+
+structure Context where
+  lctx      : LocalContext := {}
+  /--
+  Contains all variables in `cases` statements in the current path
+  and variables that are already in `reset` statements when we
+  invoke `R`.
+
+  We use this information to prevent double-reset in code such as
+  ```
+  case x_i : obj of
+  Prod.mk →
+    case x_i : obj of
+    Prod.mk →
+    ...
+  ```
+
+  A variable can already be in a `reset` statement when we
+  invoke `R` because we execute it with and without `relaxedReuse`.
+  -/
+  alreadyFound : PHashSet VarId := {}
+  /--
+  If `relaxedReuse := true`, then allow memory cells from different
+  constructors to be reused. For example, we can reuse a `PSigma.mk`
+  to allocate a `Prod.mk`. To avoid counterintuitive behavior,
+  we first try `relaxedReuse := false`, and then `relaxedReuse := true`.
+  -/
+  relaxedReuse : Bool := false
 
 /-- We use `Context` to track join points in scope. -/
-abbrev M := ReaderT LocalContext (StateT Index Id)
+abbrev M := ReaderT Context (StateT Index Id)
 
 private def mkFresh : M VarId := do
-  let idx ← getModify (fun n => n + 1)
-  pure { idx := idx }
+  let idx ← getModify fun n => n + 1
+  return { idx := idx }
 
+/--
+Helper function for applying `S`. We only introduce a `reset` if we managed
+to replace a `ctor` withe `reuse` in `b`.
+-/
 private def tryS (x : VarId) (c : CtorInfo) (b : FnBody) : M FnBody := do
   let w ← mkFresh
-  let b' := S w c b
-  if b == b' then pure b
-  else pure $ FnBody.vdecl w IRType.object (Expr.reset c.size x) b'
+  let b' := S w c (← read).relaxedReuse b
+  if b == b' then
+    return b
+  else
+    return .vdecl w IRType.object (.reset c.size x) b'
 
 private def Dfinalize (x : VarId) (c : CtorInfo) : FnBody × Bool → M FnBody
-  | (b, true)  => pure b
+  | (b, true)  => return b
   | (b, false) => tryS x c b
 
 private def argsContainsVar (ys : Array Arg) (x : VarId) : Bool :=
   ys.any fun arg => match arg with
-    | Arg.var y => x == y
-    | _         => false
+    | .var y => x == y
+    | _      => false
 
 private def isCtorUsing (b : FnBody) (x : VarId) : Bool :=
   match b with
-  | (FnBody.vdecl _ _ (Expr.ctor _ ys) _) => argsContainsVar ys x
+  | .vdecl _ _ (.ctor _ ys) _ => argsContainsVar ys x
   | _ => false
 
-/-- Given `Dmain b`, the resulting pair `(new_b, flag)` contains the new body `new_b`,
-   and `flag == true` if `x` is live in `b`.
+/--
+Given `Dmain b`, the resulting pair `(new_b, flag)` contains the new body `new_b`,
+and `flag == true` if `x` is live in `b`.
 
-   Note that, in the function `D` defined in the paper, for each `let x := e; F`,
-   `D` checks whether `x` is live in `F` or not. This is great for clarity but it
-   is expensive: `O(n^2)` where `n` is the size of the function body. -/
-private partial def Dmain (x : VarId) (c : CtorInfo) : FnBody → M (FnBody × Bool)
-  | e@(FnBody.case tid y yType alts) => do
-    let ctx ← read
-    if e.hasLiveVar ctx x then do
+Note that, in the function `D` defined in the paper, for each `let x := e; F`,
+`D` checks whether `x` is live in `F` or not. This is great for clarity but it
+is expensive: `O(n^2)` where `n` is the size of the function body. -/
+private partial def Dmain (x : VarId) (c : CtorInfo) (e : FnBody) : M (FnBody × Bool) := do
+  match e with
+  | .case tid y yType alts =>
+    if e.hasLiveVar (← read).lctx x then
       /- If `x` is live in `e`, we recursively process each branch. -/
       let alts ← alts.mapM fun alt => alt.mmodifyBody fun b => Dmain x c b >>= Dfinalize x c
-      pure (FnBody.case tid y yType alts, true)
-    else pure (e, false)
-  | FnBody.jdecl j ys v b   => do
-    let (b, found) ← withReader (fun ctx => ctx.addJP j ys v) (Dmain x c b)
+      return (.case tid y yType alts, true)
+    else
+      return (e, false)
+  | .jdecl j ys v b =>
+    let (b, found) ← withReader (fun ctx => { ctx with lctx := ctx.lctx.addJP j ys v }) (Dmain x c b)
     let (v, _ /- found' -/) ← Dmain x c v
     /- If `found' == true`, then `Dmain b` must also have returned `(b, true)` since
        we assume the IR does not have dead join points. So, if `x` is live in `j` (i.e., `v`),
        then it must also live in `b` since `j` is reachable from `b` with a `jmp`.
        On the other hand, `x` may be live in `b` but dead in `j` (i.e., `v`). -/
-    pure (FnBody.jdecl j ys v b, found)
-  | e => do
-    let ctx ← read
+    return (.jdecl j ys v b, found)
+  | e =>
     if e.isTerminal then
-      pure (e, e.hasLiveVar ctx x)
+      return (e, e.hasLiveVar (← read).lctx x)
     else do
       let (instr, b) := e.split
       if isCtorUsing instr x then
         /- If the scrutinee `x` (the one that is providing memory) is being
            stored in a constructor, then reuse will probably not be able to reuse memory at runtime.
            It may work only if the new cell is consumed, but we ignore this case. -/
-        pure (e, true)
+        return (e, true)
       else
         let (b, found) ← Dmain x c b
         /- Remark: it is fine to use `hasFreeVar` instead of `hasLiveVar`
-           since `instr` is not a `FnBody.jmp` (it is not a terminal) nor it is a `FnBody.jdecl`. -/
+           since `instr` is not a `FnBody.jmp` (it is not a terminal) nor
+           it is a `FnBody.jdecl`. -/
         if found || !instr.hasFreeVar x then
-          pure (instr.setBody b, found)
+          return (instr.setBody b, found)
         else
           let b ← tryS x c b
-          pure (instr.setBody b, true)
+          return (instr.setBody b, true)
 
 private def D (x : VarId) (c : CtorInfo) (b : FnBody) : M FnBody :=
   Dmain x c b >>= Dfinalize x c
 
-partial def R : FnBody → M FnBody
-  | FnBody.case tid x xType alts   => do
+partial def R (e : FnBody) : M FnBody := do
+  match e with
+  | .case tid x xType alts =>
+    let alreadyFound := (← read).alreadyFound.contains x
+    withReader (fun ctx => { ctx with alreadyFound := ctx.alreadyFound.insert x }) do
       let alts ← alts.mapM fun alt => do
         let alt ← alt.mmodifyBody R
         match alt with
-        | Alt.ctor c b =>
-          if c.isScalar then pure alt
-          else Alt.ctor c <$> D x c b
-        | _            => pure alt
-      pure $ FnBody.case tid x xType alts
-  | FnBody.jdecl j ys v b   => do
+        | .ctor c b =>
+          if c.isScalar || alreadyFound then
+            -- If `alreadyFound`, then we don't try to reuse memory cell to avoid
+            -- double reset.
+            return alt
+          else
+            .ctor c <$> D x c b
+        | _ => return alt
+      return .case tid x xType alts
+  | .jdecl j ys v b =>
     let v ← R v
-    let b ← withReader (fun ctx => ctx.addJP j ys v) (R b)
-    pure $ FnBody.jdecl j ys v b
-  | e => do
-    if e.isTerminal then pure e
-    else do
+    let b ← withReader (fun ctx => { ctx with lctx := ctx.lctx.addJP j ys v }) (R b)
+    return .jdecl j ys v b
+  | e =>
+    if e.isTerminal then
+      return e
+    else
       let (instr, b) := e.split
       let b ← R b
-      pure (instr.setBody b)
+      return instr.setBody b
+
+abbrev N := StateT (PHashSet VarId) Id
+
+partial def collectResets (e : FnBody) : N Unit := do
+  match e with
+  | .case _ _ _ alts => alts.forM fun alt => collectResets alt.body
+  | .jdecl _ _ v b => collectResets v; collectResets b
+  | .vdecl _ _ (.reset _ x) b => modify fun s => s.insert x; collectResets b
+  | e => unless e.isTerminal do
+    let (_, b) := e.split
+    collectResets b
 
 end ResetReuse
-
 open ResetReuse
 
-def Decl.insertResetReuse (d : Decl) : Decl :=
+
+def Decl.insertResetReuseCore (d : Decl) (relaxedReuse : Bool) : Decl :=
   match d with
-  | .fdecl (body := b) ..=>
+  | .fdecl (body := b) .. =>
     let nextIndex := d.maxIndex + 1
-    let bNew      := (R b {}).run' nextIndex
+    -- First time we execute `insertResetReuseCore`, `relaxedReuse := false`.
+    let alreadyFound : PHashSet VarId := if relaxedReuse then (collectResets b *> get).run' {} else {}
+    let bNew := R b { relaxedReuse, alreadyFound } |>.run' nextIndex
     d.updateBody! bNew
   | other => other
 
+def Decl.insertResetReuse (d : Decl) : Decl :=
+  /-
+  We execute the reset/reuse algorithm twice. The first time, we only reuse memory cells
+  between identical constructor memory cells. That is, we do not reuse a `PSigma.mk` memory cell
+  when allocating a `Prod.mk` memory cell, even though they have the same layout. Recall
+  that the reset/reuse placement algorithm is a heuristic, and the first pass prevents reuses
+  that are unlikely to be useful at runtime. Then, we run the procedure again,
+  relaxing this restriction. If there are still opportunities for reuse, we will take advantage of them.
+
+  The second pass addresses issue #4089.
+  -/
+  d.insertResetReuseCore (relaxedReuse := false)
+  |>.insertResetReuseCore (relaxedReuse := true)
+
 end Lean.IR

src/Lean/Compiler/InitAttr.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.AddDecl
 import Lean.Elab.InfoTree.Main
 
 namespace Lean

src/Lean/Compiler/Old.lean

@@ -67,9 +67,4 @@ opaque compileDecls (env : Environment) (opt : @& Options) (decls : @& List Name
 def compileDecl (env : Environment) (opt : @& Options) (decl : @& Declaration) : Except KernelException Environment :=
   compileDecls env opt (Compiler.getDeclNamesForCodeGen decl)
 
-
-def addAndCompile (env : Environment) (opt : Options) (decl : Declaration) : Except KernelException Environment := do
-  let env ← addDecl env decl
-  compileDecl env opt decl
-
 end Environment

src/Lean/CoreM.lean

@@ -13,13 +13,27 @@ import Lean.Elab.InfoTree.Types
 import Lean.MonadEnv
 
 namespace Lean
-namespace Core
+register_builtin_option diagnostics : Bool := {
+  defValue := false
+  group    := "diagnostics"
+  descr    := "collect diagnostic information"
+}
+
+register_builtin_option diagnostics.threshold : Nat := {
+  defValue := 20
+  group    := "diagnostics"
+  descr    := "only diagnostic counters above this threshold are reported by the definitional equality"
+}
 
 register_builtin_option maxHeartbeats : Nat := {
   defValue := 200000
   descr := "maximum amount of heartbeats per command. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit"
 }
 
+def useDiagnosticMsg := s!"use `set_option {diagnostics.name} true` to get diagnostic information"
+
+namespace Core
+
 builtin_initialize registerTraceClass `Kernel
 
 def getMaxHeartbeats (opts : Options) : Nat :=
@@ -67,11 +81,10 @@ structure Context where
   maxHeartbeats  : Nat := getMaxHeartbeats options
   currMacroScope : MacroScope := firstFrontendMacroScope
   /--
-  If `catchRuntimeEx = false`, then given `try x catch ex => h ex`,
-  an runtime exception occurring in `x` is not handled by `h`.
-  Recall that runtime exceptions are `maxRecDepth` or `maxHeartbeats`.
+  If `diag := true`, different parts of the system collect diagnostics.
+  Use the `set_option diag true` to set it to true.
   -/
-  catchRuntimeEx : Bool := false
+  diag           : Bool := false
   deriving Nonempty
 
 /-- CoreM is a monad for manipulating the Lean environment.
@@ -104,7 +117,22 @@ instance : MonadOptions CoreM where
   getOptions := return (← read).options
 
 instance : MonadWithOptions CoreM where
-  withOptions f x := withReader (fun ctx => { ctx with options := f ctx.options }) x
+  withOptions f x := do
+    let options := f (← read).options
+    let diag := diagnostics.get options
+    if Kernel.isDiagnosticsEnabled (← getEnv) != diag then
+      modifyEnv fun env => Kernel.enableDiag env diag
+    withReader
+      (fun ctx =>
+        { ctx with
+          options
+          diag
+          maxRecDepth := maxRecDepth.get options })
+      x
+
+-- Helper function for ensuring fields that depend on `options` have the correct value.
+@[inline] private def withConsistentCtx (x : CoreM α) : CoreM α := do
+  withOptions id x
 
 instance : AddMessageContext CoreM where
   addMessageContext := addMessageContextPartial
@@ -192,7 +220,7 @@ def mkFreshUserName (n : Name) : CoreM Name :=
   mkFreshNameImp n
 
 @[inline] def CoreM.run (x : CoreM α) (ctx : Context) (s : State) : EIO Exception (α × State) :=
-  (x ctx).run s
+  ((withConsistentCtx x) ctx).run s
 
 @[inline] def CoreM.run' (x : CoreM α) (ctx : Context) (s : State) : EIO Exception α :=
   Prod.fst <$> x.run ctx s
@@ -206,7 +234,7 @@ def mkFreshUserName (n : Name) : CoreM Name :=
 instance [MetaEval α] : MetaEval (CoreM α) where
   eval env opts x _ := do
     let x : CoreM α := do try x finally printTraces
-    let (a, s) ← x.toIO { maxRecDepth := maxRecDepth.get opts, options := opts, fileName := "<CoreM>", fileMap := default } { env := env }
+    let (a, s) ← (withConsistentCtx x).toIO { fileName := "<CoreM>", fileMap := default, options := opts } { env := env }
     MetaEval.eval s.env opts a (hideUnit := true)
 
 -- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`
@@ -218,8 +246,16 @@ protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m
     -- should never be visible to users!
     throw <| Exception.error .missing "elaboration interrupted"
 
+register_builtin_option debug.moduleNameAtTimeout : Bool := {
+  defValue := true
+  group    := "debug"
+  descr    := "include module name in deterministic timeout error messages.\nRemark: we set this option to false to increase the stability of our test suite"
+}
+
 def throwMaxHeartbeat (moduleName : Name) (optionName : Name) (max : Nat) : CoreM Unit := do
-  let msg := s!"(deterministic) timeout at '{moduleName}', maximum number of heartbeats ({max/1000}) has been reached (use 'set_option {optionName} <num>' to set the limit)"
+  let includeModuleName := debug.moduleNameAtTimeout.get (← getOptions)
+  let atModuleName := if includeModuleName then s!" at `{moduleName}`" else ""
+  let msg := s!"(deterministic) timeout{atModuleName}, maximum number of heartbeats ({max/1000}) has been reached\nuse `set_option {optionName} <num>` to set the limit\n{useDiagnosticMsg}"
   throw <| Exception.error (← getRef) (MessageData.ofFormat (Std.Format.text msg))
 
 def checkMaxHeartbeatsCore (moduleName : String) (optionName : Name) (max : Nat) : CoreM Unit := do
@@ -296,7 +332,8 @@ export Core (CoreM mkFreshUserName checkSystem withCurrHeartbeats)
   We used a similar hack at `Exception.isMaxRecDepth` -/
 def Exception.isMaxHeartbeat (ex : Exception) : Bool :=
   match ex with
-  | Exception.error _ (MessageData.ofFormat (Std.Format.text msg)) => "(deterministic) timeout".isPrefixOf msg
+  | Exception.error _ (MessageData.ofFormatWithInfos ⟨Std.Format.text msg, _⟩) =>
+    "(deterministic) timeout".isPrefixOf msg
   | _ => false
 
 /-- Creates the expression `d → b` -/
@@ -306,15 +343,6 @@ def mkArrow (d b : Expr) : CoreM Expr :=
 /-- Iterated `mkArrow`, creates the expression `a₁ → a₂ → … → aₙ → b`. Also see `arrowDomainsN`. -/
 def mkArrowN (ds : Array Expr) (e : Expr) : CoreM Expr := ds.foldrM mkArrow e
 
-def addDecl (decl : Declaration) : CoreM Unit := do
-  profileitM Exception "type checking" (← getOptions) do
-    withTraceNode `Kernel (fun _ => return m!"typechecking declaration") do
-      if !(← MonadLog.hasErrors) && decl.hasSorry then
-        logWarning "declaration uses 'sorry'"
-      match (← getEnv).addDecl decl with
-      | Except.ok    env => setEnv env
-      | Except.error ex  => throwKernelException ex
-
 private def supportedRecursors :=
   #[``Empty.rec, ``False.rec, ``Eq.ndrec, ``Eq.rec, ``Eq.recOn, ``Eq.casesOn, ``False.casesOn, ``Empty.casesOn, ``And.rec, ``And.casesOn]
 
@@ -368,13 +396,16 @@ def compileDecls (decls : List Name) : CoreM Unit := do
   | Except.error ex =>
     throwKernelException ex
 
-def addAndCompile (decl : Declaration) : CoreM Unit := do
-  addDecl decl;
-  compileDecl decl
+def getDiag (opts : Options) : Bool :=
+  diagnostics.get opts
+
+/-- Return `true` if diagnostic information collection is enabled. -/
+def isDiagnosticsEnabled : CoreM Bool :=
+  return (← read).diag
 
 def ImportM.runCoreM (x : CoreM α) : ImportM α := do
   let ctx ← read
-  let (a, _) ← x.toIO { options := ctx.opts, fileName := "<ImportM>", fileMap := default } { env := ctx.env }
+  let (a, _) ← (withOptions (fun _ => ctx.opts) x).toIO { fileName := "<ImportM>", fileMap := default } { env := ctx.env }
   return a
 
 /-- Return `true` if the exception was generated by one our resource limits. -/
@@ -389,30 +420,36 @@ in these monads, but on `CommandElabM`. See issues #2775 and #2744 as well as `M
   try
     x
   catch ex =>
-    if ex.isRuntime && !(← read).catchRuntimeEx then
-      throw ex
+    if ex.isRuntime then
+      throw ex -- We should use `tryCatchRuntimeEx` for catching runtime exceptions
     else
       h ex
 
+@[inline] protected def Core.tryCatchRuntimeEx (x : CoreM α) (h : Exception → CoreM α) : CoreM α := do
+  try
+    x
+  catch ex =>
+    h ex
+
 instance : MonadExceptOf Exception CoreM where
   throw    := throw
   tryCatch := Core.tryCatch
 
-@[inline] def Core.withCatchingRuntimeEx (flag : Bool) (x : CoreM α) : CoreM α :=
-  withReader (fun ctx => { ctx with catchRuntimeEx := flag }) x
+class MonadRuntimeException (m : Type → Type) where
+  tryCatchRuntimeEx (body : m α) (handler : Exception → m α) : m α
+
+export MonadRuntimeException (tryCatchRuntimeEx)
+
+instance : MonadRuntimeException CoreM where
+  tryCatchRuntimeEx := Core.tryCatchRuntimeEx
+
+@[inline] instance [MonadRuntimeException m] : MonadRuntimeException (ReaderT ρ m) where
+  tryCatchRuntimeEx := fun x c r => tryCatchRuntimeEx (x r) (fun e => (c e) r)
+
+@[inline] instance [MonadRuntimeException m] : MonadRuntimeException (StateRefT' ω σ m) where
+  tryCatchRuntimeEx := fun x c s => tryCatchRuntimeEx (x s) (fun e => c e s)
 
 @[inline] def mapCoreM [MonadControlT CoreM m] [Monad m] (f : forall {α}, CoreM α → CoreM α) {α} (x : m α) : m α :=
   controlAt CoreM fun runInBase => f <| runInBase x
 
-/--
-Execute `x` with `catchRuntimeEx = flag`. That is, given `try x catch ex => h ex`,
-if `x` throws a runtime exception, the handler `h` will be invoked if `flag = true`
-Recall that
--/
-@[inline] def withCatchingRuntimeEx [MonadControlT CoreM m] [Monad m] (x : m α) : m α :=
-  mapCoreM (Core.withCatchingRuntimeEx true) x
-
-@[inline] def withoutCatchingRuntimeEx [MonadControlT CoreM m] [Monad m] (x : m α) : m α :=
-  mapCoreM (Core.withCatchingRuntimeEx false) x
-
 end Lean

src/Lean/Data/HashMap.lean

@@ -92,6 +92,7 @@ def moveEntries [Hashable α] (i : Nat) (source : Array (AssocList α β)) (targ
      moveEntries (i+1) source target
   else target
 termination_by source.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β :=
   let bucketsNew : HashMapBucket α β := ⟨

src/Lean/Data/HashSet.lean

@@ -84,6 +84,7 @@ def moveEntries [Hashable α] (i : Nat) (source : Array (List α)) (target : Has
   else
     target
 termination_by source.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def expand [Hashable α] (size : Nat) (buckets : HashSetBucket α) : HashSetImp α :=
   let bucketsNew : HashSetBucket α := ⟨

src/Lean/Data/RBTree.lean

@@ -100,7 +100,7 @@ def fromArray (l : Array α) (cmp : α → α → Ordering) : RBTree α cmp :=
   RBMap.any t (fun a _ => p a)
 
 def subset (t₁ t₂ : RBTree α cmp) : Bool :=
-  t₁.all fun a => (t₂.find? a).toBool
+  t₁.all fun a => (t₂.find? a).isSome
 
 def seteq (t₁ t₂ : RBTree α cmp) : Bool :=
   subset t₁ t₂ && subset t₂ t₁

src/Lean/Declaration.lean

@@ -135,6 +135,11 @@ structure TheoremVal extends ConstantVal where
   all : List Name := [name]
   deriving Inhabited, BEq
 
+@[export lean_mk_theorem_val]
+def mkTheoremValEx (name : Name) (levelParams : List Name) (type : Expr) (value : Expr) (all : List Name) : TheoremVal := {
+  name, levelParams, type, value, all
+}
+
 /-- Value for an opaque constant declaration `opaque x : t := e` -/
 structure OpaqueVal extends ConstantVal where
   value : Expr

src/Lean/Elab/Binders.lean

@@ -7,6 +7,7 @@ prelude
 import Lean.Elab.Quotation.Precheck
 import Lean.Elab.Term
 import Lean.Elab.BindersUtil
+import Lean.Elab.SyntheticMVars
 import Lean.Elab.PreDefinition.WF.TerminationHint
 
 namespace Lean.Elab.Term
@@ -70,30 +71,34 @@ def kindOfBinderName (binderName : Name) : LocalDeclKind :=
   else
     .default
 
-partial def quoteAutoTactic : Syntax → TermElabM Syntax
-  | stx@(.ident ..) => throwErrorAt stx "invalid auto tactic, identifier is not allowed"
+partial def quoteAutoTactic : Syntax → CoreM Expr
+  | .ident _ _ val preresolved =>
+    return mkApp4 (.const ``Syntax.ident [])
+      (.const ``SourceInfo.none [])
+      (.app (.const ``String.toSubstring []) (mkStrLit (toString val)))
+      (toExpr val)
+      (toExpr preresolved)
   | stx@(.node _ k args) => do
     if stx.isAntiquot then
       throwErrorAt stx "invalid auto tactic, antiquotation is not allowed"
     else
-      let mut quotedArgs ← `(Array.empty)
+      let ty := .const ``Syntax []
+      let mut quotedArgs := mkApp (.const ``Array.empty [.zero]) ty
       for arg in args do
         if k == nullKind && (arg.isAntiquotSuffixSplice || arg.isAntiquotSplice) then
           throwErrorAt arg "invalid auto tactic, antiquotation is not allowed"
         else
           let quotedArg ← quoteAutoTactic arg
-          quotedArgs ← `(Array.push $quotedArgs $quotedArg)
-      `(Syntax.node SourceInfo.none $(quote k) $quotedArgs)
-  | .atom _ val => `(mkAtom $(quote val))
+          quotedArgs := mkApp3 (.const ``Array.push [.zero]) ty quotedArgs quotedArg
+      return mkApp3 (.const ``Syntax.node []) (.const ``SourceInfo.none []) (toExpr k) quotedArgs
+  | .atom _ val => return .app (.const ``mkAtom []) (toExpr val)
   | .missing    => throwError "invalid auto tactic, tactic is missing"
 
 def declareTacticSyntax (tactic : Syntax) : TermElabM Name :=
   withFreshMacroScope do
     let name ← MonadQuotation.addMacroScope `_auto
     let type := Lean.mkConst `Lean.Syntax
-    let tactic ← quoteAutoTactic tactic
-    let value ← elabTerm tactic type
-    let value ← instantiateMVars value
+    let value ← quoteAutoTactic tactic
     trace[Elab.autoParam] value
     let decl := Declaration.defnDecl { name, levelParams := [], type, value, hints := .opaque,
                                        safety := DefinitionSafety.safe }
@@ -642,7 +647,29 @@ def elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx : Syntax) (va
     (expectedType? : Option Expr) (useLetExpr : Bool) (elabBodyFirst : Bool) (usedLetOnly : Bool) : TermElabM Expr := do
   let (type, val, binders) ← elabBindersEx binders fun xs => do
     let (binders, fvars) := xs.unzip
-    let type ← elabType typeStx
+    /-
+    We use `withSynthesize` to ensure that any postponed elaboration problem
+    and nested tactics in `type` are resolved before elaborating `val`.
+    Resolved: we want to avoid synthethic opaque metavariables in `type`.
+    Recall that this kind of metavariable is non-assignable, and `isDefEq`
+    may waste a lot of time unfolding declarations before failing.
+    See issue #4051 for an example.
+
+    Here is the analysis for issue #4051.
+    - Given `have x : type := value; body`, we were previously elaborating `value` even
+      if `type` contained postponed elaboration problems.
+    - Moreover, the metavariables in `type` corresponding to postponed elaboration
+      problems cannot be assigned by `isDefEq` since the elaborator is supposed to assign them.
+    - Then, when checking whether type of `value` is definitionally equal to `type`,
+      a very long-time was spent unfolding a bunch of declarations before it failed.
+      In #4051, it was unfolding `Array.swaps` which is defined by well-founded recursion.
+      After the failure, the elaborator inserted a postponed coercion
+      that would be resolved later as soon as the types don't have unassigned metavariables.
+
+    We use `postpone := .partial` to allow type class (TC) resolution problems to be postponed
+    Recall that TC resolution does **not** produce synthetic opaque metavariables.
+    -/
+    let type ← withSynthesize (postpone := .partial) <| elabType typeStx
     registerCustomErrorIfMVar type typeStx "failed to infer 'let' declaration type"
     if elabBodyFirst then
       let type ← mkForallFVars fvars type

src/Lean/Elab/BuiltinCommand.lean

@@ -123,7 +123,7 @@ private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM
   n[1].forArgsM addUnivLevel
 
 @[builtin_command_elab «init_quot»] def elabInitQuot : CommandElab := fun _ => do
-  match (← getEnv).addDecl Declaration.quotDecl with
+  match (← getEnv).addDecl (← getOptions) Declaration.quotDecl with
   | Except.ok env   => setEnv env
   | Except.error ex => throwError (ex.toMessageData (← getOptions))
 

src/Lean/Elab/BuiltinNotation.lean

@@ -98,7 +98,7 @@ open Meta
       show Nat from 0
     ```
     -/
-    let type ← withSynthesize (mayPostpone := true) do
+    let type ← withSynthesize (postpone := .yes) do
       let type ← elabType type
       if let some expectedType := expectedType? then
         -- Recall that a similar approach is used when elaborating applications
@@ -205,7 +205,7 @@ private def elabTParserMacroAux (prec lhsPrec e : Term) : TermElabM Syntax := do
   | _                                        => Macro.throwUnsupported
 
 @[builtin_term_elab «sorry»] def elabSorry : TermElab := fun stx expectedType? => do
-  let stxNew ← `(sorryAx _ false)
+  let stxNew ← `(@sorryAx _ false) -- Remark: we use `@` to ensure `sorryAx` will not consume auot params
   withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
 
 /-- Return syntax `Prod.mk elems[0] (Prod.mk elems[1] ... (Prod.mk elems[elems.size - 2] elems[elems.size - 1])))` -/
@@ -314,11 +314,11 @@ where
 
 @[builtin_term_elab typeAscription] def elabTypeAscription : TermElab
   | `(($e : $type)), _ => do
-    let type ← withSynthesize (mayPostpone := true) <| elabType type
+    let type ← withSynthesize (postpone := .yes) <| elabType type
     let e ← elabTerm e type
     ensureHasType type e
   | `(($e :)), expectedType? => do
-    let e ← withSynthesize (mayPostpone := false) <| elabTerm e none
+    let e ← withSynthesize (postpone := .no) <| elabTerm e none
     ensureHasType expectedType? e
   | _, _ => throwUnsupportedSyntax
 
@@ -388,7 +388,7 @@ private def withLocalIdentFor (stx : Term) (e : Expr) (k : Term → TermElabM Ex
                return (← mkEqRec motive h (← mkEqSymm heq), none)
          let motive ← mkMotive lhs expectedAbst
          if badMotive?.isSome || !(← isTypeCorrect motive) then
-           -- Before failing try tos use `subst`
+           -- Before failing try to use `subst`
            if ← (isSubstCandidate lhs rhs <||> isSubstCandidate rhs lhs) then
              withLocalIdentFor heqStx heq fun heqStx => do
                let h ← instantiateMVars h
@@ -408,7 +408,13 @@ private def withLocalIdentFor (stx : Term) (e : Expr) (k : Term → TermElabM Ex
        | none =>
          let h ← elabTerm hStx none
          let hType ← inferType h
-         let hTypeAbst ← kabstract hType lhs
+         let mut hTypeAbst ← kabstract hType lhs
+         unless hTypeAbst.hasLooseBVars do
+           hTypeAbst ← kabstract hType rhs
+           unless hTypeAbst.hasLooseBVars do
+             throwError "invalid `▸` notation, the equality{indentExpr heq}\nhas type {indentExpr heqType}\nbut neither side of the equality is mentioned in the type{indentExpr hType}"
+           heq ← mkEqSymm heq
+           (lhs, rhs) := (rhs, lhs)
          let motive ← mkMotive lhs hTypeAbst
          unless (← isTypeCorrect motive) do
            throwError "invalid `▸` notation, failed to compute motive for the substitution"

src/Lean/Elab/BuiltinTerm.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Meta.Diagnostics
 import Lean.Elab.Open
 import Lean.Elab.SetOption
 import Lean.Elab.Eval
@@ -313,8 +314,12 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
 
 @[builtin_term_elab «set_option»] def elabSetOption : TermElab := fun stx expectedType? => do
   let options ← Elab.elabSetOption stx[1] stx[3]
-  withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options }) do
-    elabTerm stx[5] expectedType?
+  withOptions (fun _ => options) do
+    try
+      elabTerm stx[5] expectedType?
+    finally
+      if stx[1].getId == `diagnostics then
+        reportDiag
 
 @[builtin_term_elab withAnnotateTerm] def elabWithAnnotateTerm : TermElab := fun stx expectedType? => do
   match stx with

src/Lean/Elab/Calc.lean

@@ -42,7 +42,7 @@ def mkCalcTrans (result resultType step stepType : Expr) : MetaM (Expr × Expr)
     unless (← getCalcRelation? resultType).isSome do
       throwError "invalid 'calc' step, step result is not a relation{indentExpr resultType}"
     return (result, resultType)
-  | _ => throwError "invalid 'calc' step, failed to synthesize `Trans` instance{indentExpr selfType}"
+  | _ => throwError "invalid 'calc' step, failed to synthesize `Trans` instance{indentExpr selfType}\n{useDiagnosticMsg}"
 
 /--
 Adds a type annotation to a hole that occurs immediately at the beginning of the term.
@@ -112,10 +112,12 @@ def elabCalcSteps (steps : TSyntax ``calcSteps) : TermElabM Expr := do
   return result?.get!.1
 
 /-- Elaborator for the `calc` term mode variant. -/
-@[builtin_term_elab «calc»]
+@[builtin_term_elab Lean.calc]
 def elabCalc : TermElab := fun stx expectedType? => do
   let steps : TSyntax ``calcSteps := ⟨stx[1]⟩
   let result ← elabCalcSteps steps
   synthesizeSyntheticMVarsUsingDefault
   let result ← ensureHasType expectedType? result
   return result
+
+end Lean.Elab.Term

src/Lean/Elab/Command.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Gabriel Ebner
 -/
 prelude
+import Lean.Meta.Diagnostics
 import Lean.Elab.Binders
 import Lean.Elab.SyntheticMVars
 import Lean.Elab.SetOption
@@ -127,19 +128,6 @@ def mkMessageAux (ctx : Context) (ref : Syntax) (msgData : MessageData) (severit
   let endPos := ref.getTailPos?.getD pos
   mkMessageCore ctx.fileName ctx.fileMap msgData severity pos endPos
 
-private def mkCoreContext (ctx : Context) (s : State) (heartbeats : Nat) : Core.Context :=
-  let scope        := s.scopes.head!
-  { fileName       := ctx.fileName
-    fileMap        := ctx.fileMap
-    options        := scope.opts
-    currRecDepth   := ctx.currRecDepth
-    maxRecDepth    := s.maxRecDepth
-    ref            := ctx.ref
-    currNamespace  := scope.currNamespace
-    openDecls      := scope.openDecls
-    initHeartbeats := heartbeats
-    currMacroScope := ctx.currMacroScope }
-
 private def addTraceAsMessagesCore (ctx : Context) (log : MessageLog) (traceState : TraceState) : MessageLog := Id.run do
   if traceState.traces.isEmpty then return log
   let mut traces : HashMap (String.Pos × String.Pos) (Array MessageData) := ∅
@@ -165,31 +153,49 @@ private def addTraceAsMessages : CommandElabM Unit := do
       traceState.traces := {}
     }
 
-def liftCoreM (x : CoreM α) : CommandElabM α := do
+private def runCore (x : CoreM α) : CommandElabM α := do
   let s ← get
   let ctx ← read
   let heartbeats ← IO.getNumHeartbeats
-  let Eα := Except Exception α
-  let x : CoreM Eα := try let a ← x; pure <| Except.ok a catch ex => pure <| Except.error ex
-  let x : EIO Exception (Eα × Core.State) := (ReaderT.run x (mkCoreContext ctx s heartbeats)).run { env := s.env, ngen := s.ngen, traceState := s.traceState, messages := {}, infoState.enabled := s.infoState.enabled }
+  let env := Kernel.resetDiag s.env
+  let scope := s.scopes.head!
+  let coreCtx : Core.Context := {
+    fileName       := ctx.fileName
+    fileMap        := ctx.fileMap
+    currRecDepth   := ctx.currRecDepth
+    maxRecDepth    := s.maxRecDepth
+    ref            := ctx.ref
+    currNamespace  := scope.currNamespace
+    openDecls      := scope.openDecls
+    initHeartbeats := heartbeats
+    currMacroScope := ctx.currMacroScope
+    options        := scope.opts
+  }
+  let x : EIO _ _ := x.run coreCtx {
+    env
+    ngen := s.ngen
+    nextMacroScope := s.nextMacroScope
+    infoState.enabled := s.infoState.enabled
+    traceState := s.traceState
+  }
   let (ea, coreS) ← liftM x
   modify fun s => { s with
-    env := coreS.env
-    ngen := coreS.ngen
-    messages := s.messages ++ coreS.messages
+    env               := coreS.env
+    nextMacroScope    := coreS.nextMacroScope
+    ngen              := coreS.ngen
+    infoState.trees   := s.infoState.trees.append coreS.infoState.trees
     traceState.traces := coreS.traceState.traces.map fun t => { t with ref := replaceRef t.ref ctx.ref }
-    infoState.trees := s.infoState.trees.append coreS.infoState.trees
+    messages          := s.messages ++ coreS.messages
   }
-  match ea with
-  | Except.ok a    => pure a
-  | Except.error e => throw e
+  return ea
+
+def liftCoreM (x : CoreM α) : CommandElabM α := do
+  MonadExcept.ofExcept (← runCore (observing x))
 
 private def ioErrorToMessage (ctx : Context) (ref : Syntax) (err : IO.Error) : Message :=
   let ref := getBetterRef ref ctx.macroStack
   mkMessageAux ctx ref (toString err) MessageSeverity.error
 
-@[inline] def liftEIO {α} (x : EIO Exception α) : CommandElabM α := liftM x
-
 @[inline] def liftIO {α} (x : IO α) : CommandElabM α := do
   let ctx ← read
   IO.toEIO (fun (ex : IO.Error) => Exception.error ctx.ref ex.toString) x
@@ -269,7 +275,7 @@ private def elabCommandUsing (s : State) (stx : Syntax) : List (KeyedDeclsAttrib
       (fun _ => do set s; elabCommandUsing s stx elabFns)
 
 /-- Elaborate `x` with `stx` on the macro stack -/
-def withMacroExpansion {α} (beforeStx afterStx : Syntax) (x : CommandElabM α) : CommandElabM α :=
+def withMacroExpansion (beforeStx afterStx : Syntax) (x : CommandElabM α) : CommandElabM α :=
   withInfoContext (mkInfo := pure <| .ofMacroExpansionInfo { stx := beforeStx, output := afterStx, lctx := .empty }) do
     withReader (fun ctx => { ctx with macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack }) x
 
@@ -402,7 +408,6 @@ def printExpr (e : Expr) : MetaM Unit := do
 def liftTermElabM (x : TermElabM α) : CommandElabM α := do
   let ctx ← read
   let s   ← get
-  let heartbeats ← IO.getNumHeartbeats
   -- dbg_trace "heartbeats: {heartbeats}"
   let scope := s.scopes.head!
   -- We execute `x` with an empty message log. Thus, `x` cannot modify/view messages produced by previous commands.
@@ -411,18 +416,9 @@ def liftTermElabM (x : TermElabM α) : CommandElabM α := do
   -- make sure `observing` below also catches runtime exceptions (like we do by default in
   -- `CommandElabM`)
   let _ := MonadAlwaysExcept.except (m := TermElabM)
-  let x : MetaM _      := (observing x).run (mkTermContext ctx s) { levelNames := scope.levelNames }
-  let x : CoreM _      := x.run mkMetaContext {}
-  let x : EIO _ _      := x.run (mkCoreContext ctx s heartbeats) { env := s.env, ngen := s.ngen, nextMacroScope := s.nextMacroScope, infoState.enabled := s.infoState.enabled, traceState := s.traceState }
-  let (((ea, _), _), coreS) ← liftEIO x
-  modify fun s => { s with
-    env               := coreS.env
-    nextMacroScope    := coreS.nextMacroScope
-    ngen              := coreS.ngen
-    infoState.trees   := s.infoState.trees.append coreS.infoState.trees
-    traceState.traces := coreS.traceState.traces.map fun t => { t with ref := replaceRef t.ref ctx.ref }
-    messages          := s.messages ++ coreS.messages
-  }
+  let x : MetaM _ := (observing (try x finally Meta.reportDiag)).run (mkTermContext ctx s) { levelNames := scope.levelNames }
+  let x : CoreM _ := x.run mkMetaContext {}
+  let ((ea, _), _) ← runCore x
   MonadExcept.ofExcept ea
 
 /--

src/Lean/Elab/Deriving/Repr.lean

@@ -70,6 +70,8 @@ where
           if localDecl.binderInfo.isExplicit then
             if (← inferType x).isAppOf indVal.name then
               rhs ← `($rhs ++ Format.line ++ $(mkIdent auxFunName):ident $a:ident max_prec)
+            else if (← isType x <||> isProof x) then
+              rhs ← `($rhs ++ Format.line ++ "_")
             else
               rhs ← `($rhs ++ Format.line ++ reprArg $a)
         patterns := patterns.push (← `(@$(mkIdent ctorName):ident $ctorArgs:term*))

src/Lean/Elab/Extra.lean

@@ -96,7 +96,7 @@ Here are brief descriptions of each of the operator types:
 - `rightact% f a b` elaborates `f a b` as a right action (the `b` operand "acts upon" the `a` operand).
   Only `a` participates in the protocol since `b` can have an unrelated type.
   This is used by `HPow` since, for example, there are both `Real -> Nat -> Real` and `Real -> Real -> Real`
-  exponentiation functions, and we prefer the former in the case of `x ^ 2`, but `binop%` would choose the latter. (#2220)
+  exponentiation functions, and we prefer the former in the case of `x ^ 2`, but `binop%` would choose the latter. (#2854)
 - There are also `binrel%` and `binrel_no_prop%` (see the docstring for `elabBinRelCore`).
 
 The elaborator works as follows:
@@ -188,7 +188,7 @@ private partial def toTree (s : Syntax) : TermElabM Tree := do
   the macro declaration names in the `op` nodes.
   -/
   let result ← go s
-  synthesizeSyntheticMVars (mayPostpone := true)
+  synthesizeSyntheticMVars (postpone := .yes)
   return result
 where
   go (s : Syntax) := do
@@ -241,7 +241,10 @@ private def hasCoe (fromType toType : Expr) : TermElabM Bool := do
 
 private structure AnalyzeResult where
   max?            : Option Expr := none
-  hasUncomparable : Bool := false -- `true` if there are two types `α` and `β` where we don't have coercions in any direction.
+  /-- `true` if there are two types `α` and `β` where we don't have coercions in any direction. -/
+  hasUncomparable : Bool := false
+  /-- `true` if there are any leaf terms with an unknown type (according to `isUnknown`). -/
+  hasUnknown      : Bool := false
 
 private def isUnknown : Expr → Bool
   | .mvar ..        => true
@@ -255,7 +258,7 @@ private def analyze (t : Tree) (expectedType? : Option Expr) : TermElabM Analyze
     match expectedType? with
     | none => pure none
     | some expectedType =>
-      let expectedType ← instantiateMVars expectedType
+      let expectedType := (← instantiateMVars expectedType).cleanupAnnotations
       if isUnknown expectedType then pure none else pure (some expectedType)
   (go t *> get).run' { max? }
 where
@@ -268,12 +271,40 @@ where
        | .binop _ _ _ lhs rhs => go lhs; go rhs
        | .unop _ _ arg => go arg
        | .term _ _ val =>
-         let type ← instantiateMVars (← inferType val)
-         unless isUnknown type do
+         let type := (← instantiateMVars (← inferType val)).cleanupAnnotations
+         if isUnknown type then
+           modify fun s => { s with hasUnknown := true }
+         else
            match (← get).max? with
            | none     => modify fun s => { s with max? := type }
            | some max =>
-             unless (← withNewMCtxDepth <| isDefEqGuarded max type) do
+             /-
+              Remark: Previously, we used `withNewMCtxDepth` to prevent metavariables in `max` and `type` from being assigned.
+
+              Reason: This is a heuristic procedure for introducing coercions in scenarios such as:
+              - Given `(n : Nat) (i : Int)`, elaborate `n = i`. The coercion must be inserted at `n`.
+                Consider the elaboration problem `(n + 0) + i`, where the type of term `0` is a metavariable.
+                We do not want it to be elaborated as `(Int.ofNat n + Int.ofNat (0 : Nat)) + i`; instead, we prefer the result to be `(Int.ofNat n + (0 : Int)) + i`.
+                Here is another example where we avoid assigning metavariables: `max := BitVec n` and `type := BitVec ?m`.
+
+              However, the combination `withNewMCtxDepth <| isDefEqGuarded max type` introduced performance issues in several
+              Mathlib files because `isDefEq` was spending a lot of time unfolding definitions in `max` and `type` before failing.
+
+              To address this issue, we allowed only reducible definitions to be unfolded during this check, using
+              `withNewMCtxDepth <| withReducible <| isDefEqGuarded max type`. This change fixed some performance issues but created new ones.
+              Lean was now spending time trying to use `hasCoe`, likely occurring in places where `withNewMCtxDepth <| isDefEqGuarded max type`
+              used to succeed but was now failing after we introduced `withReducible`.
+
+              We then considered using just `isDefEqGuarded max type` and changing the definition of `isUnknown`. In the new definition,
+              the else-case would be `| e => e.hasExprMVar` instead of `| _ => false`. However, we could not even compile this repo using
+              this configuration. The problem arises because some files require coercions even when `max` contains metavariables,
+              for example: `max := Option ?m` and `type := Name`.
+
+              As a result, rather than restricting reducibility, we decided to set `Meta.Config.isDefEqStuckEx := true`.
+              This means that if `isDefEq` encounters a subproblem `?m =?= a` where `?m` is non-assignable, it aborts the test
+              instead of unfolding definitions.
+             -/
+             unless (← withNewMCtxDepth <| withConfig (fun config => { config with isDefEqStuckEx := true }) <| isDefEqGuarded max type) do
                if (← hasCoe type max) then
                  return ()
                else if (← hasCoe max type) then
@@ -404,7 +435,7 @@ mutual
       | .unop ref f arg =>
         return .unop ref f (← go arg none false false)
       | .term ref trees e =>
-        let type ← instantiateMVars (← inferType e)
+        let type := (← instantiateMVars (← inferType e)).cleanupAnnotations
         trace[Elab.binop] "visiting {e} : {type} =?= {maxType}"
         if isUnknown type then
           if let some f := f? then
@@ -422,12 +453,17 @@ mutual
 
   private partial def toExpr (tree : Tree) (expectedType? : Option Expr) : TermElabM Expr := do
     let r ← analyze tree expectedType?
-    trace[Elab.binop] "hasUncomparable: {r.hasUncomparable}, maxType: {r.max?}"
+    trace[Elab.binop] "hasUncomparable: {r.hasUncomparable}, hasUnknown: {r.hasUnknown}, maxType: {r.max?}"
     if r.hasUncomparable || r.max?.isNone then
       let result ← toExprCore tree
       ensureHasType expectedType? result
     else
       let result ← toExprCore (← applyCoe tree r.max?.get! (isPred := false))
+      unless r.hasUnknown do
+        -- Record the resulting maxType calculation.
+        -- We can do this when all the types are known, since in this case `hasUncomparable` is valid.
+        -- If they're not known, recording maxType like this can lead to heterogeneous operations failing to elaborate.
+        discard <| isDefEqGuarded (← inferType result) r.max?.get!
       trace[Elab.binop] "result: {result}"
       ensureHasType expectedType? result
 
@@ -449,7 +485,7 @@ def elabOp : TermElab := fun stx expectedType? => do
 
   - `binrel% R x y` elaborates `R x y` using the `binop%/...` expression trees in both `x` and `y`.
     It is similar to how `binop% R x y` elaborates but with a significant difference:
-    it does not use the expected type when computing the types of the operads.
+    it does not use the expected type when computing the types of the operands.
   - `binrel_no_prop% R x y` elaborates `R x y` like `binrel% R x y`, but if the resulting type for `x` and `y`
     is `Prop` they are coerced to `Bool`.
     This is used for relations such as `==` which do not support `Prop`, but we still want
@@ -460,7 +496,6 @@ def elabBinRelCore (noProp : Bool) (stx : Syntax) (expectedType? : Option Expr)
   | some f => withSynthesizeLight do
     /-
     We used to use `withSynthesize (mayPostpone := true)` here instead of `withSynthesizeLight` here.
-    Recall that `withSynthesizeLight` is equivalent to `withSynthesize (mayPostpone := true) (synthesizeDefault := false)`.
     It seems too much to apply default instances at binary relations. For example, we cannot elaborate
     ```
     def as : List Int := [-1, 2, 0, -3, 4]
@@ -494,7 +529,7 @@ def elabBinRelCore (noProp : Bool) (stx : Syntax) (expectedType? : Option Expr)
     let rhs ← withRef rhsStx <| toTree rhsStx
     let tree := .binop stx .regular f lhs rhs
     let r ← analyze tree none
-    trace[Elab.binrel] "hasUncomparable: {r.hasUncomparable}, maxType: {r.max?}"
+    trace[Elab.binrel] "hasUncomparable: {r.hasUncomparable}, hasUnknown: {r.hasUnknown}, maxType: {r.max?}"
     if r.hasUncomparable || r.max?.isNone then
       -- Use default elaboration strategy + `toBoolIfNecessary`
       let lhs ← toExprCore lhs

src/Lean/Elab/Frontend.lean

@@ -154,9 +154,9 @@ def runFrontend
 
     return (s.commandState.env, !s.commandState.messages.hasErrors)
 
-  let ctx := { inputCtx with mainModuleName, opts, trustLevel }
+  let ctx := { inputCtx with }
   let processor := Language.Lean.process
-  let snap ← processor none ctx
+  let snap ← processor (fun _ => pure <| .ok { mainModuleName, opts, trustLevel }) none ctx
   let snaps := Language.toSnapshotTree snap
   snaps.runAndReport opts jsonOutput
   if let some ileanFileName := ileanFileName? then

src/Lean/Elab/Inductive.lean

@@ -324,7 +324,7 @@ private def elabCtors (indFVars : Array Expr) (indFVar : Expr) (params : Array E
           | some ctorType =>
             let type ← Term.elabType ctorType
             trace[Elab.inductive] "elabType {ctorView.declName} : {type} "
-            Term.synthesizeSyntheticMVars (mayPostpone := true)
+            Term.synthesizeSyntheticMVars (postpone := .yes)
             let type ← instantiateMVars type
             let type ← checkParamOccs type
             forallTelescopeReducing type fun _ resultingType => do
@@ -686,8 +686,8 @@ private def computeFixedIndexBitMask (numParams : Nat) (indType : InductiveType)
               maskRef.modify fun mask => mask.set! i false
           for x in xs[numParams:] do
             let xType ← inferType x
-            let cond (e : Expr) := indFVars.any (fun indFVar => e.getAppFn == indFVar) && e.getAppNumArgs > numParams
-            xType.forEachWhere cond fun e => do
+            let cond (e : Expr) := indFVars.any (fun indFVar => e.getAppFn == indFVar)
+            xType.forEachWhere (stopWhenVisited := true) cond fun e => do
               let eArgs := e.getAppArgs
               for i in [numParams:eArgs.size] do
                 if i >= typeArgs.size then
@@ -695,6 +695,19 @@ private def computeFixedIndexBitMask (numParams : Nat) (indType : InductiveType)
                 else
                   unless eArgs[i]! == typeArgs[i]! do
                     maskRef.modify (resetMaskAt · i)
+              /-If an index is missing in the arguments of the inductive type, then it must be non-fixed.
+                Consider the following example:
+                ```lean
+                inductive All {I : Type u} (P : I → Type v) : List I → Type (max u v) where
+                  | cons : P x → All P xs → All P (x :: xs)
+
+                inductive Iμ {I : Type u}  : I → Type (max u v) where
+                  | mk : (i : I)  → All Iμ [] → Iμ i
+                ```
+                because `i` doesn't appear in `All Iμ []`, the index shouldn't be fixed.
+              -/
+              for i in [eArgs.size:arity] do
+                maskRef.modify (resetMaskAt · i)
         go ctors
     go indType.ctors
 

src/Lean/Elab/InfoTree/Main.lean

@@ -102,8 +102,10 @@ def ContextInfo.runCoreM (info : ContextInfo) (x : CoreM α) : IO α := do
     have been used in `lctx` and `info.mctx`.
   -/
   (·.1) <$>
-    x.toIO { options := info.options, currNamespace := info.currNamespace, openDecls := info.openDecls, fileName := "<InfoTree>", fileMap := default }
-           { env := info.env, ngen := info.ngen }
+    (withOptions (fun _ => info.options) x).toIO
+      { currNamespace := info.currNamespace, openDecls := info.openDecls
+        fileName := "<InfoTree>", fileMap := default }
+      { env := info.env, ngen := info.ngen }
 
 def ContextInfo.runMetaM (info : ContextInfo) (lctx : LocalContext) (x : MetaM α) : IO α := do
   (·.1) <$> info.runCoreM (x.run { lctx := lctx } { mctx := info.mctx })

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -228,20 +228,23 @@ private def shouldUseSimpMatch (e : Expr) : MetaM Bool := do
             throwThe Unit ()
   return (← (find e).run) matches .error _
 
-partial def mkEqnTypes (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr) := do
+partial def mkEqnTypes (tryRefl : Bool) (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr) := do
   let (_, eqnTypes) ← go mvarId |>.run { declNames } |>.run #[]
   return eqnTypes
 where
   go (mvarId : MVarId) : ReaderT Context (StateRefT (Array Expr) MetaM) Unit := do
     trace[Elab.definition.eqns] "mkEqnTypes step\n{MessageData.ofGoal mvarId}"
-    if (← tryURefl mvarId) then
-      saveEqn mvarId
-      return ()
+    if tryRefl then
+      if (← tryURefl mvarId) then
+        saveEqn mvarId
+        return ()
 
     if let some mvarId ← expandRHS? mvarId then
       return (← go mvarId)
---  The following `funext?` was producing an overapplied `lhs`. Possible refinement: only do it if we want to apply `splitMatch` on the body of the lambda
-/-    if let some mvarId ← funext? mvarId then
+
+    --  The following `funext?` was producing an overapplied `lhs`. Possible refinement: only do it
+    --  if we want to apply `splitMatch` on the body of the lambda
+    /- if let some mvarId ← funext? mvarId then
         return (← go mvarId) -/
 
     if (← shouldUseSimpMatch (← mvarId.getType')) then

src/Lean/Elab/PreDefinition/Main.lean

@@ -90,6 +90,11 @@ private def addAsAxioms (preDefs : Array PreDefinition) : TermElabM Unit := do
     applyAttributesOf #[preDef] AttributeApplicationTime.afterTypeChecking
     applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
 
+def ensureFunIndReservedNamesAvailable (preDefs : Array PreDefinition) : MetaM Unit := do
+  preDefs.forM fun preDef =>
+    withRef preDef.ref <| ensureReservedNameAvailable preDef.declName "induct"
+  withRef preDefs[0]!.ref <| ensureReservedNameAvailable preDefs[0]!.declName "mutual_induct"
+
 def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLCtx {} {} do
   for preDef in preDefs do
     trace[Elab.definition.body] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
@@ -121,6 +126,7 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
       addAndCompilePartial preDefs
       preDefs.forM (·.termination.ensureNone "partial")
     else
+      ensureFunIndReservedNamesAvailable preDefs
       try
         let hasHints := preDefs.any fun preDef => preDef.termination.isNotNone
         if hasHints then

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -62,7 +62,7 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
     let us := info.levelParams.map mkLevelParam
     let target ← mkEq (mkAppN (Lean.mkConst info.declName us) xs) body
     let goal ← mkFreshExprSyntheticOpaqueMVar target
-    mkEqnTypes #[info.declName] goal.mvarId!
+    mkEqnTypes (tryRefl := true) #[info.declName] goal.mvarId!
   let baseName := info.declName
   let mut thmNames := #[]
   for i in [: eqnTypes.size] do

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -9,6 +9,7 @@ import Lean.Meta.Tactic.Split
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Eqns
 import Lean.Meta.ArgsPacker.Basic
+import Init.Data.Array.Basic
 
 namespace Lean.Elab.WF
 open Meta
@@ -39,41 +40,6 @@ private def rwFixEq (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
   mvarId.assign (← mkEqTrans h mvarNew)
   return mvarNew.mvarId!
 
-/--
-  Simplify `match`-expressions when trying to prove equation theorems for a recursive declaration defined using well-founded recursion.
-  It is similar to `simpMatch?`, but is also tries to fold `WellFounded.fix` applications occurring in discriminants.
-  See comment at `tryToFoldWellFoundedFix`.
--/
-def simpMatchWF? (mvarId : MVarId) : MetaM (Option MVarId) :=
-  mvarId.withContext do
-    let target ← instantiateMVars (← mvarId.getType)
-    let discharge? ← mvarId.withContext do SplitIf.mkDischarge?
-    let (targetNew, _) ← Simp.main target (← Split.getSimpMatchContext) (methods := { pre, discharge? })
-    let mvarIdNew ← applySimpResultToTarget mvarId target targetNew
-    if mvarId != mvarIdNew then return some mvarIdNew else return none
-where
-  pre (e : Expr) : SimpM Simp.Step := do
-    let some app ← matchMatcherApp? e
-      | return Simp.Step.continue
-    -- First try to reduce matcher
-    match (← reduceRecMatcher? e) with
-    | some e' => return Simp.Step.done { expr := e' }
-    | none    => Simp.simpMatchCore app.matcherName e
-
-/--
-  Given a goal of the form `|- f.{us} a_1 ... a_n b_1 ... b_m = ...`, return `(us, #[a_1, ..., a_n])`
-  where `f` is a constant named `declName`, and `n = info.fixedPrefixSize`.
--/
-private def getFixedPrefix (declName : Name) (info : EqnInfo) (mvarId : MVarId) : MetaM (List Level × Array Expr) := mvarId.withContext do
-  let target ← mvarId.getType'
-  let some (_, lhs, _) := target.eq? | unreachable!
-  let lhsArgs := lhs.getAppArgs
-  if lhsArgs.size < info.fixedPrefixSize || !lhs.getAppFn matches .const .. then
-    throwError "failed to generate equational theorem for '{declName}', unexpected number of arguments in the equation left-hand-side\n{mvarId}"
-  let result := lhsArgs[:info.fixedPrefixSize]
-  trace[Elab.definition.wf.eqns] "fixedPrefix: {result}"
-  return (lhs.getAppFn.constLevels!, result)
-
 private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
   trace[Elab.definition.wf.eqns] "proving: {type}"
   withNewMCtxDepth do
@@ -81,11 +47,11 @@ private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
     let (_, mvarId) ← main.mvarId!.intros
     let rec go (mvarId : MVarId) : MetaM Unit := do
       trace[Elab.definition.wf.eqns] "step\n{MessageData.ofGoal mvarId}"
-      if (← tryURefl mvarId) then
+      if ← withAtLeastTransparency .all (tryURefl mvarId) then
         return ()
       else if (← tryContradiction mvarId) then
         return ()
-      else if let some mvarId ← simpMatchWF? mvarId then
+      else if let some mvarId ← simpMatch? mvarId then
         go mvarId
       else if let some mvarId ← simpIf? mvarId then
         go mvarId
@@ -114,7 +80,8 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
     let us := info.levelParams.map mkLevelParam
     let target ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
     let goal ← mkFreshExprSyntheticOpaqueMVar target
-    mkEqnTypes info.declNames goal.mvarId!
+    withReducible do
+      mkEqnTypes (tryRefl := false) info.declNames goal.mvarId!
   let mut thmNames := #[]
   for i in [: eqnTypes.size] do
     let type := eqnTypes[i]!

src/Lean/Elab/PreDefinition/WF/Main.lean

@@ -132,12 +132,15 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
       return { unaryPreDef with value }
   trace[Elab.definition.wf] ">> {preDefNonRec.declName} :=\n{preDefNonRec.value}"
   let preDefs ← preDefs.mapM fun d => eraseRecAppSyntax d
-  if (← isOnlyOneUnaryDef preDefs fixedPrefixSize) then
-    addNonRec preDefNonRec (applyAttrAfterCompilation := false)
-  else
-    withEnableInfoTree false do
+  -- Do not complain if the user sets @[semireducible], which usually is a noop,
+  -- we recognize that below and then do not set @[irreducible]
+  withOptions (allowUnsafeReducibility.set · true) do
+    if (← isOnlyOneUnaryDef preDefs fixedPrefixSize) then
       addNonRec preDefNonRec (applyAttrAfterCompilation := false)
-    addNonRecPreDefs fixedPrefixSize argsPacker preDefs preDefNonRec
+    else
+      withEnableInfoTree false do
+        addNonRec preDefNonRec (applyAttrAfterCompilation := false)
+      addNonRecPreDefs fixedPrefixSize argsPacker preDefs preDefNonRec
   -- We create the `_unsafe_rec` before we abstract nested proofs.
   -- Reason: the nested proofs may be referring to the _unsafe_rec.
   addAndCompilePartialRec preDefs
@@ -146,6 +149,10 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
   for preDef in preDefs do
     markAsRecursive preDef.declName
     applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
+    -- Unless the user asks for something else, mark the definition as irreducible
+    unless preDef.modifiers.attrs.any fun a =>
+      a.name = `reducible || a.name = `semireducible do
+      setIrreducibleAttribute preDef.declName
 
 builtin_initialize registerTraceClass `Elab.definition.wf
 

src/Lean/Elab/StructInst.lean

@@ -821,7 +821,9 @@ partial def reduce (structNames : Array Name) (e : Expr) : MetaM Expr := do
     | some r => reduce structNames r
     | none   => return e.updateProj! (← reduce structNames b)
   | .app f .. =>
-    match (← reduceProjOf? e structNames.contains) with
+    -- Recall that proposition fields are theorems. Thus, we must set transparency to .all
+    -- to ensure they are unfolded here
+    match (← withTransparency .all <| reduceProjOf? e structNames.contains) with
     | some r => reduce structNames r
     | none   =>
       let f := f.getAppFn
@@ -937,7 +939,7 @@ private def elabStructInstAux (stx : Syntax) (expectedType? : Option Expr) (sour
 
      TODO: investigate whether this design decision may have unintended side effects or produce confusing behavior.
   -/
-  let { val := r, struct, instMVars } ← withSynthesize (mayPostpone := true) <| elabStruct struct expectedType?
+  let { val := r, struct, instMVars } ← withSynthesize (postpone := .yes) <| elabStruct struct expectedType?
   trace[Elab.struct] "before propagate {r}"
   DefaultFields.propagate struct
   synthesizeAppInstMVars instMVars r

src/Lean/Elab/Structure.lean

@@ -82,15 +82,6 @@ def StructFieldInfo.isSubobject (info : StructFieldInfo) : Bool :=
   | StructFieldKind.subobject => true
   | _                         => false
 
-structure ElabStructResult where
-  decl            : Declaration
-  projInfos       : List ProjectionInfo
-  projInstances   : List Name -- projections (to parent classes) that must be marked as instances.
-  mctx            : MetavarContext
-  lctx            : LocalContext
-  localInsts      : LocalInstances
-  defaultAuxDecls : Array (Name × Expr × Expr)
-
 private def defaultCtorName := `mk
 
 /-
@@ -713,8 +704,8 @@ private def registerStructure (structName : Name) (infos : Array StructFieldInfo
           subobject? :=
             if info.kind == StructFieldKind.subobject then
               match env.find? info.declName with
-              | some (ConstantInfo.defnInfo val) =>
-                match val.type.getForallBody.getAppFn with
+              | some info =>
+                match info.type.getForallBody.getAppFn with
                 | Expr.const parentName .. => some parentName
                 | _ => panic! "ill-formed structure"
               | _ => panic! "ill-formed environment"

src/Lean/Elab/SyntheticMVars.lean

@@ -288,6 +288,32 @@ private def processPostponedUniverseContraints : TermElabM Unit := do
 private def markAsResolved (mvarId : MVarId) : TermElabM Unit :=
   modify fun s => { s with syntheticMVars := s.syntheticMVars.erase mvarId }
 
+/--
+Auxiliary type for `synthesizeSyntheticMVars`. It specifies
+whether pending synthetic metavariables can be postponed or not.
+-/
+inductive PostponeBehavior where
+  /--
+  Any kind of pending synthetic metavariable can be postponed.
+  Universe constrains may also be postponed.
+  -/
+  | yes
+  /--
+  Pending synthetic metavariables cannot be postponed.
+  -/
+  | no
+  /--
+  Synthectic metavariables associated with type class resolution can be postponed.
+  Motivation: this kind of metavariable are not synthethic opaque, and can be assigned by `isDefEq`.
+  Unviverse constraints can also be postponed.
+  -/
+  | «partial»
+  deriving Inhabited, Repr, BEq
+
+def PostponeBehavior.ofBool : Bool → PostponeBehavior
+  | true  => .yes
+  | false => .no
+
 mutual
 
   /--
@@ -314,26 +340,26 @@ mutual
     Regarding issue #1380, we addressed the issue by avoiding the elaboration postponement step. However, the same issue can happen
     in more complicated scenarios.
     -/
-    try
-      let remainingGoals ← withInfoHole mvarId <| Tactic.run mvarId do
-        withTacticInfoContext tacticCode do
-          -- also put an info node on the `by` keyword specifically -- the token may be `canonical` and thus shown in the info
-          -- view even though it is synthetic while a node like `tacticCode` never is (#1990)
-          withTacticInfoContext tacticCode[0] do
-            evalTactic code
-        synthesizeSyntheticMVars (mayPostpone := false)
-      unless remainingGoals.isEmpty do
-        if report then
-          reportUnsolvedGoals remainingGoals
+    tryCatchRuntimeEx
+      (do let remainingGoals ← withInfoHole mvarId <| Tactic.run mvarId do
+            withTacticInfoContext tacticCode do
+              -- also put an info node on the `by` keyword specifically -- the token may be `canonical` and thus shown in the info
+              -- view even though it is synthetic while a node like `tacticCode` never is (#1990)
+              withTacticInfoContext tacticCode[0] do
+                evalTactic code
+            synthesizeSyntheticMVars (postpone := .no)
+          unless remainingGoals.isEmpty do
+            if report then
+              reportUnsolvedGoals remainingGoals
+            else
+              throwError "unsolved goals\n{goalsToMessageData remainingGoals}")
+      fun ex => do
+        if report && (← read).errToSorry then
+          for mvarId in (← getMVars (mkMVar mvarId)) do
+            mvarId.admit
+          logException ex
         else
-          throwError "unsolved goals\n{goalsToMessageData remainingGoals}"
-    catch ex =>
-      if report && (← read).errToSorry then
-        for mvarId in (← getMVars (mkMVar mvarId)) do
-          mvarId.admit
-        logException ex
-      else
-        throw ex
+          throw ex
 
   /-- Try to synthesize the given pending synthetic metavariable. -/
   private partial def synthesizeSyntheticMVar (mvarId : MVarId) (postponeOnError : Bool) (runTactics : Bool) : TermElabM Bool := do
@@ -388,25 +414,27 @@ mutual
     return numSyntheticMVars != remainingPendingMVars.length
 
   /--
-    Try to process pending synthetic metavariables. If `mayPostpone == false`,
-    then `pendingMVars` is `[]` after executing this method.
+    Try to process pending synthetic metavariables.
+
+    If `postpone == .no`,then `pendingMVars` is `[]` after executing this method.
+    If `postpone == .partial`, then `pendingMVars` contains only `.tc` and `.coe` kinds.
 
     It keeps executing `synthesizeSyntheticMVarsStep` while progress is being made.
-    If `mayPostpone == false`, then it applies default instances to `SyntheticMVarKind.typeClass` (if available)
+    If `postpone != .yes`, then it applies default instances to `SyntheticMVarKind.typeClass` (if available)
     metavariables that are still unresolved, and then tries to resolve metavariables
-    with `mayPostpone == false`. That is, we force them to produce error messages and/or commit to
-    a "best option". If, after that, we still haven't made progress, we report "stuck" errors.
+    with `postponeOnError == false`. That is, we force them to produce error messages and/or commit to
+    a "best option". If, after that, we still haven't made progress, we report "stuck" errors If `postpone == .no`.
 
     Remark: we set `ignoreStuckTC := true` when elaborating `simp` arguments. Then,
     pending TC problems become implicit parameters for the simp theorem.
   -/
-  partial def synthesizeSyntheticMVars (mayPostpone := true) (ignoreStuckTC := false) : TermElabM Unit := do
+  partial def synthesizeSyntheticMVars (postpone := PostponeBehavior.yes) (ignoreStuckTC := false) : TermElabM Unit := do
     let rec loop (_ : Unit) : TermElabM Unit := do
       withRef (← getSomeSyntheticMVarsRef) <| withIncRecDepth do
         unless (← get).pendingMVars.isEmpty do
           if ← synthesizeSyntheticMVarsStep (postponeOnError := false) (runTactics := false) then
             loop ()
-          else if !mayPostpone then
+          else if postpone != .yes then
             /- Resume pending metavariables with "elaboration postponement" disabled.
                We postpone elaboration errors in this step by setting `postponeOnError := true`.
                Example:
@@ -431,48 +459,58 @@ mutual
               loop ()
             else if ← synthesizeSyntheticMVarsStep (postponeOnError := false) (runTactics := true) then
               loop ()
-            else
+            else if postpone == .no then
               reportStuckSyntheticMVars ignoreStuckTC
     loop ()
-    unless mayPostpone do
+    if postpone == .no then
      processPostponedUniverseContraints
 end
 
 def synthesizeSyntheticMVarsNoPostponing (ignoreStuckTC := false) : TermElabM Unit :=
-  synthesizeSyntheticMVars (mayPostpone := false) (ignoreStuckTC := ignoreStuckTC)
+  synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := ignoreStuckTC)
 
 /-- Keep invoking `synthesizeUsingDefault` until it returns false. -/
 private partial def synthesizeUsingDefaultLoop : TermElabM Unit := do
   if (← synthesizeUsingDefault) then
-    synthesizeSyntheticMVars (mayPostpone := true)
+    synthesizeSyntheticMVars (postpone := .yes)
     synthesizeUsingDefaultLoop
 
 def synthesizeSyntheticMVarsUsingDefault : TermElabM Unit := do
-  synthesizeSyntheticMVars (mayPostpone := true)
+  synthesizeSyntheticMVars (postpone := .yes)
   synthesizeUsingDefaultLoop
 
-private partial def withSynthesizeImp {α} (k : TermElabM α) (mayPostpone : Bool) (synthesizeDefault : Bool) : TermElabM α := do
-  let pendingMVarsSaved := (← get).pendingMVars
-  modify fun s => { s with pendingMVars := [] }
-  try
-    let a ← k
-    synthesizeSyntheticMVars mayPostpone
-    if mayPostpone && synthesizeDefault then
-      synthesizeUsingDefaultLoop
-    return a
-  finally
-    modify fun s => { s with pendingMVars := s.pendingMVars ++ pendingMVarsSaved }
+private partial def withSynthesizeImp (k : TermElabM α) (postpone : PostponeBehavior) : TermElabM α := do
+   let pendingMVarsSaved := (← get).pendingMVars
+   modify fun s => { s with pendingMVars := [] }
+   try
+     let a ← k
+     synthesizeSyntheticMVars (postpone := postpone)
+     if postpone == .yes then
+       synthesizeUsingDefaultLoop
+     return a
+   finally
+     modify fun s => { s with pendingMVars := s.pendingMVars ++ pendingMVarsSaved }
 
 /--
   Execute `k`, and synthesize pending synthetic metavariables created while executing `k` are solved.
   If `mayPostpone == false`, then all of them must be synthesized.
   Remark: even if `mayPostpone == true`, the method still uses `synthesizeUsingDefault` -/
-@[inline] def withSynthesize [MonadFunctorT TermElabM m] [Monad m] (k : m α) (mayPostpone := false) : m α :=
-  monadMap (m := TermElabM) (withSynthesizeImp · mayPostpone (synthesizeDefault := true)) k
+@[inline] def withSynthesize [MonadFunctorT TermElabM m] [Monad m] (k : m α) (postpone := PostponeBehavior.no) : m α :=
+  monadMap (m := TermElabM) (withSynthesizeImp · postpone) k
 
-/-- Similar to `withSynthesize`, but sets `mayPostpone` to `true`, and do not use `synthesizeUsingDefault` -/
+private partial def withSynthesizeLightImp (k : TermElabM α) : TermElabM α := do
+  let pendingMVarsSaved := (← get).pendingMVars
+  modify fun s => { s with pendingMVars := [] }
+  try
+    let a ← k
+    synthesizeSyntheticMVars (postpone := .yes)
+    return a
+  finally
+    modify fun s => { s with pendingMVars := s.pendingMVars ++ pendingMVarsSaved }
+
+/-- Similar to `withSynthesize`, but uses `postpone := .true`, does not use use `synthesizeUsingDefault` -/
 @[inline] def withSynthesizeLight [MonadFunctorT TermElabM m] [Monad m] (k : m α) : m α :=
-  monadMap (m := TermElabM) (withSynthesizeImp · (mayPostpone := true) (synthesizeDefault := false)) k
+  monadMap (m := TermElabM) (withSynthesizeLightImp ·) k
 
 /-- Elaborate `stx`, and make sure all pending synthetic metavariables created while elaborating `stx` are solved. -/
 def elabTermAndSynthesize (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr :=

src/Lean/Elab/Tactic/Basic.lean

@@ -231,15 +231,15 @@ def closeUsingOrAdmit (tac : TacticM Unit) : TacticM Unit := do
   /- Important: we must define `closeUsingOrAdmit` before we define
      the instance `MonadExcept` for `TacticM` since it backtracks the state including error messages. -/
   let mvarId :: mvarIds ← getUnsolvedGoals | throwNoGoalsToBeSolved
-  try
-    focusAndDone tac
-  catch ex =>
-    if (← read).recover then
-      logException ex
-      admitGoal mvarId
-      setGoals mvarIds
-    else
-      throw ex
+  tryCatchRuntimeEx
+    (focusAndDone tac)
+    fun ex => do
+      if (← read).recover then
+        logException ex
+        admitGoal mvarId
+        setGoals mvarIds
+      else
+        throw ex
 
 instance : MonadBacktrack SavedState TacticM where
   saveState := Tactic.saveState

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Meta.Diagnostics
 import Lean.Meta.Tactic.Apply
 import Lean.Meta.Tactic.Assumption
 import Lean.Meta.Tactic.Contradiction
@@ -122,7 +123,7 @@ def evalSepByIndentTactic (stx : Syntax) : TacticM Unit := do
     withInfoContext (pure ()) initInfo
     evalSepByIndentTactic stx[1]
 
-@[builtin_tactic cdot] def evalTacticCDot : Tactic := fun stx => do
+@[builtin_tactic Lean.cdot] def evalTacticCDot : Tactic := fun stx => do
   -- adjusted copy of `evalTacticSeqBracketed`; we used to use the macro
   -- ``| `(tactic| $cdot:cdotTk $tacs) => `(tactic| {%$cdot ($tacs) }%$cdot)``
   -- but the token antiquotation does not copy trailing whitespace, leading to
@@ -163,8 +164,12 @@ private def getOptRotation (stx : Syntax) : Nat :=
 
 @[builtin_tactic Parser.Tactic.set_option] def elabSetOption : Tactic := fun stx => do
   let options ← Elab.elabSetOption stx[1] stx[3]
-  withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options }) do
-    evalTactic stx[5]
+  withOptions (fun _ => options) do
+    try
+      evalTactic stx[5]
+    finally
+      if stx[1].getId == `diagnostics then
+        reportDiag
 
 @[builtin_tactic Parser.Tactic.allGoals] def evalAllGoals : Tactic := fun stx => do
   let mvarIds ← getGoals
@@ -265,7 +270,7 @@ where
       pure (fvarId, [mvarId])
     if let some typeStx := typeStx? then
       withMainContext do
-        let type ← Term.withSynthesize (mayPostpone := true) <| Term.elabType typeStx
+        let type ← Term.withSynthesize (postpone := .yes) <| Term.elabType typeStx
         let fvar := mkFVar fvarId
         let fvarType ← inferType fvar
         unless (← isDefEqGuarded type fvarType) do

src/Lean/Elab/Tactic/Calc.lean

@@ -11,7 +11,7 @@ namespace Lean.Elab.Tactic
 open Meta
 
 /-- Elaborator for the `calc` tactic mode variant. -/
-@[builtin_tactic calcTactic]
+@[builtin_tactic Lean.calcTactic]
 def evalCalc : Tactic := fun stx => withMainContext do
   let steps : TSyntax ``calcSteps := ⟨stx[1]⟩
   let (val, mvarIds) ← withCollectingNewGoalsFrom (tagSuffix := `calc) do
@@ -32,3 +32,5 @@ def evalCalc : Tactic := fun stx => withMainContext do
     return val
   (← getMainGoal).assign val
   replaceMainGoal mvarIds
+
+end Lean.Elab.Tactic

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -29,7 +29,7 @@ def runTermElab (k : TermElabM α) (mayPostpone := false) : TacticM α := do
   else
     Term.withoutErrToSorry go
 where
-  go := k <* Term.synthesizeSyntheticMVars (mayPostpone := mayPostpone)
+  go := k <* Term.synthesizeSyntheticMVars (postpone := .ofBool mayPostpone)
 
 /-- Elaborate `stx` in the current `MVarContext`. If given, the `expectedType` will be used to help
 elaboration but not enforced (use `elabTermEnsuringType` to enforce an expected type). -/

src/Lean/Elab/Tactic/Induction.lean

@@ -524,7 +524,7 @@ private def elabTermForElim (stx : Syntax) : TermElabM Expr := do
       return e
   Term.withoutErrToSorry <| Term.withoutHeedElabAsElim do
     let e ← Term.elabTerm stx none (implicitLambda := false)
-    Term.synthesizeSyntheticMVars (mayPostpone := false) (ignoreStuckTC := true)
+    Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true)
     let e ← instantiateMVars e
     let e := e.eta
     if e.hasMVar then

src/Lean/Elab/Tactic/Meta.lean

@@ -14,7 +14,7 @@ open Term
 def runTactic (mvarId : MVarId) (tacticCode : Syntax) (ctx : Context := {}) (s : State := {}) : MetaM (List MVarId × State) := do
   instantiateMVarDeclMVars mvarId
   let go : TermElabM (List MVarId) :=
-    withSynthesize (mayPostpone := false) do Tactic.run mvarId (Tactic.evalTactic tacticCode *> Tactic.pruneSolvedGoals)
+    withSynthesize do Tactic.run mvarId (Tactic.evalTactic tacticCode *> Tactic.pruneSolvedGoals)
   go.run ctx s
 
 end Lean.Elab

src/Lean/Elab/Tactic/NormCast.lean

@@ -146,7 +146,9 @@ It tries to rewrite an expression using the elim and move lemmas.
 On failure, it calls the splitting procedure heuristic.
 -/
 partial def upwardAndElim (up : SimpTheorems) (e : Expr) : SimpM Simp.Step := do
-  let r ← withDischarger prove do
+  -- Remark: we set `wellBehavedDischarge := false` because `prove` may access arbitrary elements in the local context.
+  -- See comment at `Methods.wellBehavedDischarge`
+  let r ← withDischarger prove (wellBehavedDischarge := false) do
     Simp.rewrite? e up.post up.erased (tag := "squash") (rflOnly := false)
   let r := r.getD { expr := e }
   let r ← r.mkEqTrans (← splittingProcedure r.expr)