merge master

This makes it reflect how we are writing release notes for 4.9.0,
including how to handle the `releases_drafts` folder and how and when to
update `RELEASES.md`.

Co-authored-by: Kim Morrison <kim@tqft.net>

.github/workflows/actionlint.yml

@@ -15,7 +15,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
     - name: Checkout
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
     - name: actionlint
       uses: raven-actions/actionlint@v1
       with:

.github/workflows/ci.yml

@@ -52,7 +52,7 @@ jobs:
 
     steps:
       - name: Checkout
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         # don't schedule nightlies on forks
         if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4' || inputs.action == 'release nightly'
       - name: Set Nightly
@@ -397,7 +397,7 @@ jobs:
           else
             ${{ matrix.tar || 'tar' }} cf - $dir | zstd -T0 --no-progress -o pack/$dir.tar.zst
           fi
-      - uses: actions/upload-artifact@v3
+      - uses: actions/upload-artifact@v4
         if: matrix.release
         with:
           name: build-${{ matrix.name }}
@@ -470,7 +470,7 @@ jobs:
     runs-on: ubuntu-latest
     needs: build
     steps:
-      - uses: actions/download-artifact@v3
+      - uses: actions/download-artifact@v4
         with:
           path: artifacts
       - name: Release
@@ -495,12 +495,12 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           # needed for tagging
           fetch-depth: 0
           token: ${{ secrets.PUSH_NIGHTLY_TOKEN }}
-      - uses: actions/download-artifact@v3
+      - uses: actions/download-artifact@v4
         with:
           path: artifacts
       - name: Prepare Nightly Release

.github/workflows/nix-ci.yml

@@ -50,7 +50,7 @@ jobs:
       NIX_BUILD_ARGS: --print-build-logs --fallback
     steps:
       - name: Checkout
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           # the default is to use a virtual merge commit between the PR and master: just use the PR
           ref: ${{ github.event.pull_request.head.sha }}

.github/workflows/pr-release.yml

@@ -234,7 +234,7 @@ jobs:
       # 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
+        uses: actions/checkout@v4
         with:
           repository: leanprover-community/batteries
           token: ${{ secrets.MATHLIB4_BOT }}
@@ -291,7 +291,7 @@ jobs:
       # Checkout the mathlib4 repository with all branches
       - name: Checkout mathlib4 repository
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           repository: leanprover-community/mathlib4
           token: ${{ secrets.MATHLIB4_BOT }}

.github/workflows/update-stage0.yml

@@ -23,7 +23,7 @@ jobs:
     # This action should push to an otherwise protected branch, so it
     # uses a deploy key with write permissions, as suggested at
     # https://stackoverflow.com/a/76135647/946226
-    - uses: actions/checkout@v3
+    - uses: actions/checkout@v4
       with:
         ssh-key: ${{secrets.STAGE0_SSH_KEY}}
     - run: echo "should_update_stage0=yes" >> "$GITHUB_ENV"

CODEOWNERS

@@ -42,4 +42,4 @@
 /src/Lean/Elab/Tactic/Guard.lean @digama0
 /src/Init/Guard.lean @digama0
 /src/Lean/Server/CodeActions/ @digama0
-
+/src/Std/ @TwoFX

doc/dev/release_checklist.md

@@ -5,7 +5,8 @@ See below for the checklist for release candidates.
 
 We'll use `v4.6.0` as the intended release version as a running example.
 
-- One week before the planned release, ensure that someone has written the first draft of the release blog post
+- One week before the planned release, ensure that (1) someone has written the release notes and (2) someone has written the first draft of the release blog post.
+  If there is any material in `./releases_drafts/`, then the release notes are not done. (See the section "Writing the release notes".)
 - `git checkout releases/v4.6.0`
   (This branch should already exist, from the release candidates.)
 - `git pull`
@@ -13,11 +14,6 @@ We'll use `v4.6.0` as the intended release version as a running example.
   - `set(LEAN_VERSION_MINOR 6)` (for whichever `6` is appropriate)
   - `set(LEAN_VERSION_IS_RELEASE 1)`
   - (both of these should already be in place from the release candidates)
-- In `RELEASES.md`, verify that the `v4.6.0` section has been completed during the release candidate cycle.
-  It should be in bullet point form, with a point for every significant PR,
-  and may have a paragraph describing each major new language feature.
-  It should have a "breaking changes" section calling out changes that are specifically likely
-  to cause problems for downstream users.
 - `git tag v4.6.0`
 - `git push $REMOTE v4.6.0`, where `$REMOTE` is the upstream Lean repository (e.g., `origin`, `upstream`)
 - Now wait, while CI runs.
@@ -28,8 +24,9 @@ We'll use `v4.6.0` as the intended release version as a running example.
     you may want to start on the release candidate checklist now.
 - Go to https://github.com/leanprover/lean4/releases and verify that the `v4.6.0` release appears.
   - Edit the release notes on Github to select the "Set as the latest release".
-  - Copy and paste the Github release notes from the previous releases candidate for this version
-    (e.g. `v4.6.0-rc1`), and quickly sanity check.
+  - Follow the instructions in creating a release candidate for the "GitHub release notes" step,
+    now that we have a written `RELEASES.md` section.
+    Do a quick sanity check.
 - Next, we will move a curated list of downstream repos to the latest stable release.
   - For each of the repositories listed below:
     - Make a PR to `master`/`main` changing the toolchain to `v4.6.0`
@@ -92,6 +89,10 @@ We'll use `v4.6.0` as the intended release version as a running example.
       - Toolchain bump PR including updated Lake manifest
       - Create and push the tag
       - Merge the tag into `stable`
+- The `v4.6.0` section of `RELEASES.md` is out of sync between
+  `releases/v4.6.0` and `master`. This should be reconciled:
+  - Replace the `v4.6.0` section on `master` with the `v4.6.0` section on `releases/v4.6.0`
+    and commit this to `master`.
 - Merge the release announcement PR for the Lean website - it will be deployed automatically
 - Finally, make an announcement!
   This should go in https://leanprover.zulipchat.com/#narrow/stream/113486-announce, with topic `v4.6.0`.
@@ -102,7 +103,6 @@ We'll use `v4.6.0` as the intended release version as a running example.
 
 ## Optimistic(?) time estimates:
 - Initial checks and push the tag: 30 minutes.
-- Note that if `RELEASES.md` has discrepancies this could take longer!
 - Waiting for the release: 60 minutes.
 - Fixing release notes: 10 minutes.
 - Bumping toolchains in downstream repositories, up to creating the Mathlib PR: 30 minutes.
@@ -129,29 +129,26 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
     git checkout nightly-2024-02-29
     git checkout -b releases/v4.7.0
     ```
-- In `RELEASES.md` remove `(development in progress)` from the `v4.7.0` section header.
-- Our current goal is to have written release notes only about major language features or breaking changes,
-  and to rely on automatically generated release notes for bugfixes and minor changes.
-  - Do not wait on `RELEASES.md` being perfect before creating the `release/v4.7.0` branch. It is essential to choose the nightly which will become the release candidate as early as possible, to avoid confusion.
-  - If there are major changes not reflected in `RELEASES.md` already, you may need to solicit help from the authors.
-  - Minor changes and bug fixes do not need to be documented in `RELEASES.md`: they will be added automatically on the Github release page.
-  - Commit your changes to `RELEASES.md`, and push.
-  - Remember that changes to `RELEASES.md` after you have branched `releases/v4.7.0` should also be cherry-picked back to `master`.
+- In `RELEASES.md` replace `Development in progress` in the `v4.7.0` section with `Release notes to be written.`
+- We will rely on automatically generated release notes for release candidates,
+  and the written release notes will be used for stable versions only.
+  It is essential to choose the nightly that will become the release candidate as early as possible, to avoid confusion.
 - In `src/CMakeLists.txt`,
   - verify that you see `set(LEAN_VERSION_MINOR 7)` (for whichever `7` is appropriate); this should already have been updated when the development cycle began.
   - `set(LEAN_VERSION_IS_RELEASE 1)` (this should be a change; on `master` and nightly releases it is always `0`).
   - Commit your changes to `src/CMakeLists.txt`, and push.
 - `git tag v4.7.0-rc1`
 - `git push origin v4.7.0-rc1`
+- Ping the FRO Zulip that release notes need to be written. The release notes do not block completing the rest of this checklist.
 - Now wait, while CI runs.
   - You can monitor this at `https://github.com/leanprover/lean4/actions/workflows/ci.yml`, looking for the `v4.7.0-rc1` tag.
   - This step can take up to an hour.
-- Once the release appears at https://github.com/leanprover/lean4/releases/
+- (GitHub release notes) Once the release appears at https://github.com/leanprover/lean4/releases/
   - Edit the release notes on Github to select the "Set as a pre-release box".
-  - Copy the section of `RELEASES.md` for this version into the Github release notes.
-  - Use the title "Changes since v4.6.0 (from RELEASES.md)"
-  - Then in the "previous tag" dropdown, select `v4.6.0`, and click "Generate release notes".
-  - This will add a list of all the commits since the last stable version.
+  - If release notes have been written already, copy the section of `RELEASES.md` for this version into the Github release notes
+    and use the title "Changes since v4.6.0 (from RELEASES.md)".
+  - Otherwise, in the "previous tag" dropdown, select `v4.6.0`, and click "Generate release notes".
+    This will add a list of all the commits since the last stable version.
     - Delete anything already mentioned in the hand-written release notes above.
     - Delete "update stage0" commits, and anything with a completely inscrutable commit message.
     - Briefly rearrange the remaining items by category (e.g. `simp`, `lake`, `bug fixes`),
@@ -177,6 +174,9 @@ 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!
+    It is essential for Mathlib CI that you then create the next `bump/v4.8.0` branch
+    for the next development cycle.
+    Set the `lean-toolchain` file on this branch to same `nightly` you used for this release.
   - 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.
@@ -187,12 +187,17 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
   Please also make sure that whoever is handling social media knows the release is out.
 - Begin the next development cycle (i.e. for `v4.8.0`) on the Lean repository, by making a PR that:
   - Updates `src/CMakeLists.txt` to say `set(LEAN_VERSION_MINOR 8)`
-  - In `RELEASES.md`, update the `v4.7.0` section to say:
-    "Release candidate, release notes will be copied from branch `releases/v4.7.0` once completed."
-    Make sure that whoever is preparing the release notes during this cycle knows that it is their job to do so!
-  - In `RELEASES.md`, update the `v4.8.0` section to say:
-    "Development in progress".
-  - In `RELEASES.md`, verify that the old section `v4.6.0` has the full releases notes from the `releases/v4.6.0` branch.
+  - Replaces the "development in progress" in the `v4.7.0` section of `RELEASES.md` with
+    ```
+    Release candidate, release notes will be copied from `branch releases/v4.7.0` once completed.
+    ```
+    and inserts the following section before that section:
+    ```
+    v4.8.0
+    ----------
+    Development in progress.
+    ```
+  - Removes all the entries from the `./releases_drafts/` folder.
 
 ## Time estimates:
 Slightly longer than the corresponding steps for a stable release.
@@ -226,3 +231,18 @@ Please read https://leanprover-community.github.io/contribute/tags_and_branches.
 * It is always okay to merge in the following directions:
   `master` -> `bump/v4.7.0` -> `bump/nightly-2024-02-15` -> `nightly-testing`.
   Please remember to push any merges you make to intermediate steps!
+
+# Writing the release notes
+
+We are currently trying a system where release notes are compiled all at once from someone looking through the commit history.
+The exact steps are a work in progress.
+Here is the general idea:
+
+* The work is done right on the `releases/v4.6.0` branch sometime after it is created but before the stable release is made.
+  The release notes for `v4.6.0` will be copied to `master`.
+* There can be material for release notes entries in commit messages.
+* There can also be pre-written entries in `./releases_drafts`, which should be all incorporated in the release notes and then deleted from the branch.
+  See `./releases_drafts/README.md` for more information.
+* The release notes should be written from a downstream expert user's point of view.
+
+This section will be updated when the next release notes are written (for `v4.10.0`).

src/Init/Control/Lawful/Instances.lean

@@ -193,8 +193,8 @@ theorem run_bind_lift {α σ : Type u} [Monad m] [LawfulMonad m] (x : m α) (f :
 
 @[simp] theorem run_monadLift {α σ : Type u} [Monad m] [MonadLiftT n m] (x : n α) (s : σ) : (monadLift x : StateT σ m α).run s = (monadLift x : m α) >>= fun a => pure (a, s) := rfl
 
-@[simp] theorem run_monadMap [Monad m] [MonadFunctor n m] (f : {β : Type u} → n β → n β) (x : StateT σ m α) (s : σ)
-    : (monadMap @f x : StateT σ m α).run s = monadMap @f (x.run s) := rfl
+@[simp] theorem run_monadMap [MonadFunctor n m] (f : {β : Type u} → n β → n β) (x : StateT σ m α) (s : σ) :
+    (monadMap @f x : StateT σ m α).run s = monadMap @f (x.run s) := rfl
 
 @[simp] theorem run_seq {α β σ : Type u} [Monad m] [LawfulMonad m] (f : StateT σ m (α → β)) (x : StateT σ m α) (s : σ) : (f <*> x).run s = (f.run s >>= fun fs => (fun (p : α × σ) => (fs.1 p.1, p.2)) <$> x.run fs.2) := by
   show (f >>= fun g => g <$> x).run s = _

src/Init/Control/StateRef.lean

@@ -64,5 +64,5 @@ end StateRefT'
 instance (ω σ : Type) (m : Type → Type) : MonadControl m (StateRefT' ω σ m) :=
   inferInstanceAs (MonadControl m (ReaderT _ _))
 
-instance {m : Type → Type} {ω σ : Type} [MonadFinally m] [Monad m] : MonadFinally (StateRefT' ω σ m) :=
+instance {m : Type → Type} {ω σ : Type} [MonadFinally m] : MonadFinally (StateRefT' ω σ m) :=
   inferInstanceAs (MonadFinally (ReaderT _ _))

src/Init/Core.lean

@@ -1362,6 +1362,9 @@ theorem iff_false_right (ha : ¬a) : (b ↔ a) ↔ ¬b := Iff.comm.trans (iff_fa
 theorem of_iff_true    (h : a ↔ True) : a := h.mpr trivial
 theorem iff_true_intro (h : a) : a ↔ True := iff_of_true h trivial
 
+theorem eq_iff_true_of_subsingleton [Subsingleton α] (x y : α) : x = y ↔ True :=
+  iff_true_intro (Subsingleton.elim ..)
+
 theorem not_of_iff_false : (p ↔ False) → ¬p := Iff.mp
 theorem iff_false_intro (h : ¬a) : a ↔ False := iff_of_false h id
 
@@ -1867,7 +1870,7 @@ instance : Subsingleton (Squash α) where
 /--
 `Antisymm (·≤·)` says that `(·≤·)` is antisymmetric, that is, `a ≤ b → b ≤ a → a = b`.
 -/
-class Antisymm {α : Sort u} (r : α → α → Prop) where
+class Antisymm {α : Sort u} (r : α → α → Prop) : Prop where
   /-- An antisymmetric relation `(·≤·)` satisfies `a ≤ b → b ≤ a → a = b`. -/
   antisymm {a b : α} : r a b → r b a → a = b
 

src/Init/Data.lean

@@ -35,3 +35,4 @@ import Init.Data.Queue
 import Init.Data.Channel
 import Init.Data.Cast
 import Init.Data.Sum
+import Init.Data.BEq

src/Init/Data/Array.lean

@@ -13,3 +13,4 @@ import Init.Data.Array.Mem
 import Init.Data.Array.Attach
 import Init.Data.Array.BasicAux
 import Init.Data.Array.Lemmas
+import Init.Data.Array.TakeDrop

src/Init/Data/BitVec/Lemmas.lean

@@ -1437,7 +1437,7 @@ theorem toNat_twoPow (w : Nat) (i : Nat) : (twoPow w i).toNat = 2^i % 2^w := by
 @[simp]
 theorem getLsb_twoPow (i j : Nat) : (twoPow w i).getLsb j = ((i < w) && (i = j)) := by
   rcases w with rfl | w
-  · simp; omega
+  · simp
   · simp only [twoPow, getLsb_shiftLeft, getLsb_ofNat]
     by_cases hj : j < i
     · simp only [hj, decide_True, Bool.not_true, Bool.and_false, Bool.false_and, Bool.false_eq,

src/Init/Data/Char/Lemmas.lean

@@ -31,11 +31,9 @@ theorem utf8Size_eq (c : Char) : c.utf8Size = 1 ∨ c.utf8Size = 2 ∨ c.utf8Siz
   rw [Char.ofNat, dif_pos]
   rfl
 
-@[ext] theorem ext : {a b : Char} → a.val = b.val → a = b
+@[ext] protected theorem ext : {a b : Char} → a.val = b.val → a = b
   | ⟨_,_⟩, ⟨_,_⟩, rfl => rfl
 
-theorem ext_iff {x y : Char} : x = y ↔ x.val = y.val := ⟨congrArg _, Char.ext⟩
-
 end Char
 
 @[deprecated Char.utf8Size (since := "2024-06-04")] abbrev String.csize := Char.utf8Size

src/Init/Data/Fin/Lemmas.lean

@@ -37,9 +37,7 @@ theorem pos_iff_nonempty {n : Nat} : 0 < n ↔ Nonempty (Fin n) :=
 
 @[simp] protected theorem eta (a : Fin n) (h : a < n) : (⟨a, h⟩ : Fin n) = a := rfl
 
-@[ext] theorem ext {a b : Fin n} (h : (a : Nat) = b) : a = b := eq_of_val_eq h
-
-theorem ext_iff {a b : Fin n} : a = b ↔ a.1 = b.1 := val_inj.symm
+@[ext] protected theorem ext {a b : Fin n} (h : (a : Nat) = b) : a = b := eq_of_val_eq h
 
 theorem val_ne_iff {a b : Fin n} : a.1 ≠ b.1 ↔ a ≠ b := not_congr val_inj
 
@@ -47,12 +45,12 @@ theorem forall_iff {p : Fin n → Prop} : (∀ i, p i) ↔ ∀ i h, p ⟨i, h⟩
   ⟨fun h i hi => h ⟨i, hi⟩, fun h ⟨i, hi⟩ => h i hi⟩
 
 protected theorem mk.inj_iff {n a b : Nat} {ha : a < n} {hb : b < n} :
-    (⟨a, ha⟩ : Fin n) = ⟨b, hb⟩ ↔ a = b := ext_iff
+    (⟨a, ha⟩ : Fin n) = ⟨b, hb⟩ ↔ a = b := Fin.ext_iff
 
 theorem val_mk {m n : Nat} (h : m < n) : (⟨m, h⟩ : Fin n).val = m := rfl
 
 theorem eq_mk_iff_val_eq {a : Fin n} {k : Nat} {hk : k < n} :
-    a = ⟨k, hk⟩ ↔ (a : Nat) = k := ext_iff
+    a = ⟨k, hk⟩ ↔ (a : Nat) = k := Fin.ext_iff
 
 theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta ..
 
@@ -145,7 +143,7 @@ theorem eq_succ_of_ne_zero {n : Nat} {i : Fin (n + 1)} (hi : i ≠ 0) : ∃ j :
 
 @[simp] theorem val_rev (i : Fin n) : rev i = n - (i + 1) := rfl
 
-@[simp] theorem rev_rev (i : Fin n) : rev (rev i) = i := ext <| by
+@[simp] theorem rev_rev (i : Fin n) : rev (rev i) = i := Fin.ext <| by
   rw [val_rev, val_rev, ← Nat.sub_sub, Nat.sub_sub_self (by exact i.2), Nat.add_sub_cancel]
 
 @[simp] theorem rev_le_rev {i j : Fin n} : rev i ≤ rev j ↔ j ≤ i := by
@@ -171,12 +169,12 @@ theorem le_last (i : Fin (n + 1)) : i ≤ last n := Nat.le_of_lt_succ i.is_lt
 theorem last_pos : (0 : Fin (n + 2)) < last (n + 1) := Nat.succ_pos _
 
 theorem eq_last_of_not_lt {i : Fin (n + 1)} (h : ¬(i : Nat) < n) : i = last n :=
-  ext <| Nat.le_antisymm (le_last i) (Nat.not_lt.1 h)
+  Fin.ext <| Nat.le_antisymm (le_last i) (Nat.not_lt.1 h)
 
 theorem val_lt_last {i : Fin (n + 1)} : i ≠ last n → (i : Nat) < n :=
   Decidable.not_imp_comm.1 eq_last_of_not_lt
 
-@[simp] theorem rev_last (n : Nat) : rev (last n) = 0 := ext <| by simp
+@[simp] theorem rev_last (n : Nat) : rev (last n) = 0 := Fin.ext <| by simp
 
 @[simp] theorem rev_zero (n : Nat) : rev 0 = last n := by
   rw [← rev_rev (last _), rev_last]
@@ -244,11 +242,11 @@ theorem zero_ne_one : (0 : Fin (n + 2)) ≠ 1 := Fin.ne_of_lt one_pos
 @[simp] theorem succ_lt_succ_iff {a b : Fin n} : a.succ < b.succ ↔ a < b := Nat.succ_lt_succ_iff
 
 @[simp] theorem succ_inj {a b : Fin n} : a.succ = b.succ ↔ a = b := by
-  refine ⟨fun h => ext ?_, congrArg _⟩
+  refine ⟨fun h => Fin.ext ?_, congrArg _⟩
   apply Nat.le_antisymm <;> exact succ_le_succ_iff.1 (h ▸ Nat.le_refl _)
 
 theorem succ_ne_zero {n} : ∀ k : Fin n, Fin.succ k ≠ 0
-  | ⟨k, _⟩, heq => Nat.succ_ne_zero k <| ext_iff.1 heq
+  | ⟨k, _⟩, heq => Nat.succ_ne_zero k <| congrArg Fin.val heq
 
 @[simp] theorem succ_zero_eq_one : Fin.succ (0 : Fin (n + 1)) = 1 := rfl
 
@@ -267,7 +265,7 @@ theorem one_lt_succ_succ (a : Fin n) : (1 : Fin (n + 2)) < a.succ.succ := by
   rw [← succ_zero_eq_one, succ_lt_succ_iff]; exact succ_pos a
 
 @[simp] theorem add_one_lt_iff {n : Nat} {k : Fin (n + 2)} : k + 1 < k ↔ k = last _ := by
-  simp only [lt_def, val_add, val_last, ext_iff]
+  simp only [lt_def, val_add, val_last, Fin.ext_iff]
   let ⟨k, hk⟩ := k
   match Nat.eq_or_lt_of_le (Nat.le_of_lt_succ hk) with
   | .inl h => cases h; simp [Nat.succ_pos]
@@ -285,7 +283,7 @@ theorem one_lt_succ_succ (a : Fin n) : (1 : Fin (n + 2)) < a.succ.succ := by
     split <;> simp [*, (Nat.succ_ne_zero _).symm, Nat.ne_of_gt (Nat.lt_succ_self _)]
 
 @[simp] theorem last_le_iff {n : Nat} {k : Fin (n + 1)} : last n ≤ k ↔ k = last n := by
-  rw [ext_iff, Nat.le_antisymm_iff, le_def, and_iff_right (by apply le_last)]
+  rw [Fin.ext_iff, Nat.le_antisymm_iff, le_def, and_iff_right (by apply le_last)]
 
 @[simp] theorem lt_add_one_iff {n : Nat} {k : Fin (n + 1)} : k < k + 1 ↔ k < last n := by
   rw [← Decidable.not_iff_not]; simp
@@ -306,10 +304,10 @@ theorem succ_succ_ne_one (a : Fin n) : Fin.succ (Fin.succ a) ≠ 1 :=
 @[simp] theorem castLE_mk (i n m : Nat) (hn : i < n) (h : n ≤ m) :
     castLE h ⟨i, hn⟩ = ⟨i, Nat.lt_of_lt_of_le hn h⟩ := rfl
 
-@[simp] theorem castLE_zero {n m : Nat} (h : n.succ ≤ m.succ) : castLE h 0 = 0 := by simp [ext_iff]
+@[simp] theorem castLE_zero {n m : Nat} (h : n.succ ≤ m.succ) : castLE h 0 = 0 := by simp [Fin.ext_iff]
 
 @[simp] theorem castLE_succ {m n : Nat} (h : m + 1 ≤ n + 1) (i : Fin m) :
-    castLE h i.succ = (castLE (Nat.succ_le_succ_iff.mp h) i).succ := by simp [ext_iff]
+    castLE h i.succ = (castLE (Nat.succ_le_succ_iff.mp h) i).succ := by simp [Fin.ext_iff]
 
 @[simp] theorem castLE_castLE {k m n} (km : k ≤ m) (mn : m ≤ n) (i : Fin k) :
     Fin.castLE mn (Fin.castLE km i) = Fin.castLE (Nat.le_trans km mn) i :=
@@ -322,7 +320,7 @@ theorem succ_succ_ne_one (a : Fin n) : Fin.succ (Fin.succ a) ≠ 1 :=
 @[simp] theorem coe_cast (h : n = m) (i : Fin n) : (cast h i : Nat) = i := rfl
 
 @[simp] theorem cast_last {n' : Nat} {h : n + 1 = n' + 1} : cast h (last n) = last n' :=
-  ext (by rw [coe_cast, val_last, val_last, Nat.succ.inj h])
+  Fin.ext (by rw [coe_cast, val_last, val_last, Nat.succ.inj h])
 
 @[simp] theorem cast_mk (h : n = m) (i : Nat) (hn : i < n) : cast h ⟨i, hn⟩ = ⟨i, h ▸ hn⟩ := rfl
 
@@ -348,7 +346,7 @@ theorem castAdd_lt {m : Nat} (n : Nat) (i : Fin m) : (castAdd n i : Nat) < m :=
 
 /-- For rewriting in the reverse direction, see `Fin.cast_castAdd_left`. -/
 theorem castAdd_cast {n n' : Nat} (m : Nat) (i : Fin n') (h : n' = n) :
-    castAdd m (Fin.cast h i) = Fin.cast (congrArg (. + m) h) (castAdd m i) := ext rfl
+    castAdd m (Fin.cast h i) = Fin.cast (congrArg (. + m) h) (castAdd m i) := Fin.ext rfl
 
 theorem cast_castAdd_left {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :
     cast h (castAdd m i) = castAdd m (cast (Nat.add_right_cancel h) i) := rfl
@@ -397,7 +395,7 @@ theorem castSucc_lt_iff_succ_le {n : Nat} {i : Fin n} {j : Fin (n + 1)} :
 @[simp] theorem castSucc_lt_castSucc_iff {a b : Fin n} :
     Fin.castSucc a < Fin.castSucc b ↔ a < b := .rfl
 
-theorem castSucc_inj {a b : Fin n} : castSucc a = castSucc b ↔ a = b := by simp [ext_iff]
+theorem castSucc_inj {a b : Fin n} : castSucc a = castSucc b ↔ a = b := by simp [Fin.ext_iff]
 
 theorem castSucc_lt_last (a : Fin n) : castSucc a < last n := a.is_lt
 
@@ -409,7 +407,7 @@ theorem castSucc_lt_last (a : Fin n) : castSucc a < last n := a.is_lt
 theorem castSucc_pos {i : Fin (n + 1)} (h : 0 < i) : 0 < castSucc i := by
   simpa [lt_def] using h
 
-@[simp] theorem castSucc_eq_zero_iff (a : Fin (n + 1)) : castSucc a = 0 ↔ a = 0 := by simp [ext_iff]
+@[simp] theorem castSucc_eq_zero_iff (a : Fin (n + 1)) : castSucc a = 0 ↔ a = 0 := by simp [Fin.ext_iff]
 
 theorem castSucc_ne_zero_iff (a : Fin (n + 1)) : castSucc a ≠ 0 ↔ a ≠ 0 :=
   not_congr <| castSucc_eq_zero_iff a
@@ -421,7 +419,7 @@ theorem castSucc_fin_succ (n : Nat) (j : Fin n) :
 theorem coeSucc_eq_succ {a : Fin n} : castSucc a + 1 = a.succ := by
   cases n
   · exact a.elim0
-  · simp [ext_iff, add_def, Nat.mod_eq_of_lt (Nat.succ_lt_succ a.is_lt)]
+  · simp [Fin.ext_iff, add_def, Nat.mod_eq_of_lt (Nat.succ_lt_succ a.is_lt)]
 
 theorem lt_succ {a : Fin n} : castSucc a < a.succ := by
   rw [castSucc, lt_def, coe_castAdd, val_succ]; exact Nat.lt_succ_self a.val
@@ -454,7 +452,7 @@ theorem cast_addNat_left {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :
 
 @[simp] theorem cast_addNat_right {n m m' : Nat} (i : Fin n) (h : n + m' = n + m) :
     cast h (addNat i m') = addNat i m :=
-  ext <| (congrArg ((· + ·) (i : Nat)) (Nat.add_left_cancel h) : _)
+  Fin.ext <| (congrArg ((· + ·) (i : Nat)) (Nat.add_left_cancel h) : _)
 
 @[simp] theorem coe_natAdd (n : Nat) {m : Nat} (i : Fin m) : (natAdd n i : Nat) = n + i := rfl
 
@@ -474,7 +472,7 @@ theorem cast_natAdd_right {n n' m : Nat} (i : Fin n') (h : m + n' = m + n) :
 
 @[simp] theorem cast_natAdd_left {n m m' : Nat} (i : Fin n) (h : m' + n = m + n) :
     cast h (natAdd m' i) = natAdd m i :=
-  ext <| (congrArg (· + (i : Nat)) (Nat.add_right_cancel h) : _)
+  Fin.ext <| (congrArg (· + (i : Nat)) (Nat.add_right_cancel h) : _)
 
 theorem castAdd_natAdd (p m : Nat) {n : Nat} (i : Fin n) :
     castAdd p (natAdd m i) = cast (Nat.add_assoc ..).symm (natAdd m (castAdd p i)) := rfl
@@ -484,27 +482,27 @@ theorem natAdd_castAdd (p m : Nat) {n : Nat} (i : Fin n) :
 
 theorem natAdd_natAdd (m n : Nat) {p : Nat} (i : Fin p) :
     natAdd m (natAdd n i) = cast (Nat.add_assoc ..) (natAdd (m + n) i) :=
-  ext <| (Nat.add_assoc ..).symm
+  Fin.ext <| (Nat.add_assoc ..).symm
 
 @[simp]
 theorem cast_natAdd_zero {n n' : Nat} (i : Fin n) (h : 0 + n = n') :
     cast h (natAdd 0 i) = cast ((Nat.zero_add _).symm.trans h) i :=
-  ext <| Nat.zero_add _
+  Fin.ext <| Nat.zero_add _
 
 @[simp]
 theorem cast_natAdd (n : Nat) {m : Nat} (i : Fin m) :
-    cast (Nat.add_comm ..) (natAdd n i) = addNat i n := ext <| Nat.add_comm ..
+    cast (Nat.add_comm ..) (natAdd n i) = addNat i n := Fin.ext <| Nat.add_comm ..
 
 @[simp]
 theorem cast_addNat {n : Nat} (m : Nat) (i : Fin n) :
-    cast (Nat.add_comm ..) (addNat i m) = natAdd m i := ext <| Nat.add_comm ..
+    cast (Nat.add_comm ..) (addNat i m) = natAdd m i := Fin.ext <| Nat.add_comm ..
 
 @[simp] theorem natAdd_last {m n : Nat} : natAdd n (last m) = last (n + m) := rfl
 
 theorem natAdd_castSucc {m n : Nat} {i : Fin m} : natAdd n (castSucc i) = castSucc (natAdd n i) :=
   rfl
 
-theorem rev_castAdd (k : Fin n) (m : Nat) : rev (castAdd m k) = addNat (rev k) m := ext <| by
+theorem rev_castAdd (k : Fin n) (m : Nat) : rev (castAdd m k) = addNat (rev k) m := Fin.ext <| by
   rw [val_rev, coe_castAdd, coe_addNat, val_rev, Nat.sub_add_comm (Nat.succ_le_of_lt k.is_lt)]
 
 theorem rev_addNat (k : Fin n) (m : Nat) : rev (addNat k m) = castAdd m (rev k) := by
@@ -534,7 +532,7 @@ theorem pred_eq_iff_eq_succ {n : Nat} (i : Fin (n + 1)) (hi : i ≠ 0) (j : Fin
 theorem pred_mk_succ (i : Nat) (h : i < n + 1) :
     Fin.pred ⟨i + 1, Nat.add_lt_add_right h 1⟩ (ne_of_val_ne (Nat.ne_of_gt (mk_succ_pos i h))) =
       ⟨i, h⟩ := by
-  simp only [ext_iff, coe_pred, Nat.add_sub_cancel]
+  simp only [Fin.ext_iff, coe_pred, Nat.add_sub_cancel]
 
 @[simp] theorem pred_mk_succ' (i : Nat) (h₁ : i + 1 < n + 1 + 1) (h₂) :
     Fin.pred ⟨i + 1, h₁⟩ h₂ = ⟨i, Nat.lt_of_succ_lt_succ h₁⟩ := pred_mk_succ i _
@@ -554,14 +552,14 @@ theorem pred_mk {n : Nat} (i : Nat) (h : i < n + 1) (w) : Fin.pred ⟨i, h⟩ w
     ∀ {a b : Fin (n + 1)} {ha : a ≠ 0} {hb : b ≠ 0}, a.pred ha = b.pred hb ↔ a = b
   | ⟨0, _⟩, _, ha, _ => by simp only [mk_zero, ne_eq, not_true] at ha
   | ⟨i + 1, _⟩, ⟨0, _⟩, _, hb => by simp only [mk_zero, ne_eq, not_true] at hb
-  | ⟨i + 1, hi⟩, ⟨j + 1, hj⟩, ha, hb => by simp [ext_iff, Nat.succ.injEq]
+  | ⟨i + 1, hi⟩, ⟨j + 1, hj⟩, ha, hb => by simp [Fin.ext_iff, Nat.succ.injEq]
 
 @[simp] theorem pred_one {n : Nat} :
     Fin.pred (1 : Fin (n + 2)) (Ne.symm (Fin.ne_of_lt one_pos)) = 0 := rfl
 
 theorem pred_add_one (i : Fin (n + 2)) (h : (i : Nat) < n + 1) :
     pred (i + 1) (Fin.ne_of_gt (add_one_pos _ (lt_def.2 h))) = castLT i h := by
-  rw [ext_iff, coe_pred, coe_castLT, val_add, val_one, Nat.mod_eq_of_lt, Nat.add_sub_cancel]
+  rw [Fin.ext_iff, coe_pred, coe_castLT, val_add, val_one, Nat.mod_eq_of_lt, Nat.add_sub_cancel]
   exact Nat.add_lt_add_right h 1
 
 @[simp] theorem coe_subNat (i : Fin (n + m)) (h : m ≤ i) : (i.subNat m h : Nat) = i - m := rfl
@@ -573,10 +571,10 @@ theorem pred_add_one (i : Fin (n + 2)) (h : (i : Nat) < n + 1) :
     pred (castSucc i.succ) (Fin.ne_of_gt (castSucc_pos i.succ_pos)) = castSucc i := rfl
 
 @[simp] theorem addNat_subNat {i : Fin (n + m)} (h : m ≤ i) : addNat (subNat m i h) m = i :=
-  ext <| Nat.sub_add_cancel h
+  Fin.ext <| Nat.sub_add_cancel h
 
 @[simp] theorem subNat_addNat (i : Fin n) (m : Nat) (h : m ≤ addNat i m := le_coe_addNat m i) :
-    subNat m (addNat i m) h = i := ext <| Nat.add_sub_cancel i m
+    subNat m (addNat i m) h = i := Fin.ext <| Nat.add_sub_cancel i m
 
 @[simp] theorem natAdd_subNat_cast {i : Fin (n + m)} (h : n ≤ i) :
     natAdd n (subNat n (cast (Nat.add_comm ..) i) h) = i := by simp [← cast_addNat]; rfl
@@ -810,10 +808,10 @@ theorem coe_mul {n : Nat} : ∀ a b : Fin n, ((a * b : Fin n) : Nat) = a * b % n
 protected theorem mul_one (k : Fin (n + 1)) : k * 1 = k := by
   match n with
   | 0 => exact Subsingleton.elim (α := Fin 1) ..
-  | n+1 => simp [ext_iff, mul_def, Nat.mod_eq_of_lt (is_lt k)]
+  | n+1 => simp [Fin.ext_iff, mul_def, Nat.mod_eq_of_lt (is_lt k)]
 
 protected theorem mul_comm (a b : Fin n) : a * b = b * a :=
-  ext <| by rw [mul_def, mul_def, Nat.mul_comm]
+  Fin.ext <| by rw [mul_def, mul_def, Nat.mul_comm]
 instance : Std.Commutative (α := Fin n) (· * ·) := ⟨Fin.mul_comm⟩
 
 protected theorem mul_assoc (a b c : Fin n) : a * b * c = a * (b * c) := by
@@ -829,9 +827,9 @@ instance : Std.LawfulIdentity (α := Fin (n + 1)) (· * ·) 1 where
   left_id := Fin.one_mul
   right_id := Fin.mul_one
 
-protected theorem mul_zero (k : Fin (n + 1)) : k * 0 = 0 := by simp [ext_iff, mul_def]
+protected theorem mul_zero (k : Fin (n + 1)) : k * 0 = 0 := by simp [Fin.ext_iff, mul_def]
 
 protected theorem zero_mul (k : Fin (n + 1)) : (0 : Fin (n + 1)) * k = 0 := by
-  simp [ext_iff, mul_def]
+  simp [Fin.ext_iff, mul_def]
 
 end Fin

src/Init/Data/List/Basic.lean

@@ -32,7 +32,7 @@ The operations are organized as follow:
 * List membership: `isEmpty`, `elem`, `contains`, `mem` (and the `∈` notation),
   and decidability for predicates quantifying over membership in a `List`.
 * Sublists: `take`, `drop`, `takeWhile`, `dropWhile`, `partition`, `dropLast`,
-  `isPrefixOf`, `isPrefixOf?`, `isSuffixOf`, `isSuffixOf?`, `rotateLeft` and `rotateRight`.
+  `isPrefixOf`, `isPrefixOf?`, `isSuffixOf`, `isSuffixOf?`, `Subset`, `Sublist`, `rotateLeft` and `rotateRight`.
 * Manipulating elements: `replace`, `insert`, `erase`, `eraseIdx`, `find?`, `findSome?`, and `lookup`.
 * Logic: `any`, `all`, `or`, and `and`.
 * Zippers: `zipWith`, `zip`, `zipWithAll`, and `unzip`.
@@ -866,6 +866,40 @@ def isSuffixOf [BEq α] (l₁ l₂ : List α) : Bool :=
 def isSuffixOf? [BEq α] (l₁ l₂ : List α) : Option (List α) :=
   Option.map List.reverse <| isPrefixOf? l₁.reverse l₂.reverse
 
+/-! ### Subset -/
+
+/--
+`l₁ ⊆ l₂` means that every element of `l₁` is also an element of `l₂`, ignoring multiplicity.
+-/
+protected def Subset (l₁ l₂ : List α) := ∀ ⦃a : α⦄, a ∈ l₁ → a ∈ l₂
+
+instance : HasSubset (List α) := ⟨List.Subset⟩
+
+instance [DecidableEq α] : DecidableRel (Subset : List α → List α → Prop) :=
+  fun _ _ => decidableBAll _ _
+
+/-! ### Sublist and isSublist -/
+
+/-- `l₁ <+ l₂`, or `Sublist l₁ l₂`, says that `l₁` is a (non-contiguous) subsequence of `l₂`. -/
+inductive Sublist {α} : List α → List α → Prop
+  /-- the base case: `[]` is a sublist of `[]` -/
+  | slnil : Sublist [] []
+  /-- If `l₁` is a subsequence of `l₂`, then it is also a subsequence of `a :: l₂`. -/
+  | cons a : Sublist l₁ l₂ → Sublist l₁ (a :: l₂)
+  /-- If `l₁` is a subsequence of `l₂`, then `a :: l₁` is a subsequence of `a :: l₂`. -/
+  | cons₂ a : Sublist l₁ l₂ → Sublist (a :: l₁) (a :: l₂)
+
+@[inherit_doc] scoped infixl:50 " <+ " => Sublist
+
+/-- True if the first list is a potentially non-contiguous sub-sequence of the second list. -/
+def isSublist [BEq α] : List α → List α → Bool
+  | [], _ => true
+  | _, [] => false
+  | l₁@(hd₁::tl₁), hd₂::tl₂ =>
+    if hd₁ == hd₂
+    then tl₁.isSublist tl₂
+    else l₁.isSublist tl₂
+
 /-! ### rotateLeft -/
 
 /--
@@ -908,6 +942,55 @@ def rotateRight (xs : List α) (n : Nat := 1) : List α :=
 
 @[simp] theorem rotateRight_nil : ([] : List α).rotateRight n = [] := rfl
 
+/-! ## Pairwise, Nodup -/
+
+section Pairwise
+
+variable (R : α → α → Prop)
+
+/--
+`Pairwise R l` means that all the elements with earlier indexes are
+`R`-related to all the elements with later indexes.
+```
+Pairwise R [1, 2, 3] ↔ R 1 2 ∧ R 1 3 ∧ R 2 3
+```
+For example if `R = (·≠·)` then it asserts `l` has no duplicates,
+and if `R = (·<·)` then it asserts that `l` is (strictly) sorted.
+-/
+inductive Pairwise : List α → Prop
+  /-- All elements of the empty list are vacuously pairwise related. -/
+  | nil : Pairwise []
+  /-- `a :: l` is `Pairwise R` if `a` `R`-relates to every element of `l`,
+  and `l` is `Pairwise R`. -/
+  | cons : ∀ {a : α} {l : List α}, (∀ a', a' ∈ l → R a a') → Pairwise l → Pairwise (a :: l)
+
+attribute [simp] Pairwise.nil
+
+variable {R}
+
+@[simp] theorem pairwise_cons : Pairwise R (a::l) ↔ (∀ a', a' ∈ l → R a a') ∧ Pairwise R l :=
+  ⟨fun | .cons h₁ h₂ => ⟨h₁, h₂⟩, fun ⟨h₁, h₂⟩ => h₂.cons h₁⟩
+
+instance instDecidablePairwise [DecidableRel R] :
+    (l : List α) → Decidable (Pairwise R l)
+  | [] => isTrue .nil
+  | hd :: tl =>
+    match instDecidablePairwise tl with
+    | isTrue ht =>
+      match decidableBAll (R hd) tl with
+      | isFalse hf => isFalse fun hf' => hf (pairwise_cons.1 hf').1
+      | isTrue ht' => isTrue <| pairwise_cons.mpr (And.intro ht' ht)
+    | isFalse hf => isFalse fun | .cons _ ih => hf ih
+
+end Pairwise
+
+/-- `Nodup l` means that `l` has no duplicates, that is, any element appears at most
+  once in the List. It is defined as `Pairwise (≠)`. -/
+def Nodup : List α → Prop := Pairwise (· ≠ ·)
+
+instance nodupDecidable [DecidableEq α] : ∀ l : List α, Decidable (Nodup l) :=
+  instDecidablePairwise
+
 /-! ## Manipulating elements -/
 
 /-! ### replace -/

src/Init/Data/List/Lemmas.lean

@@ -313,6 +313,10 @@ theorem forall_mem_cons {p : α → Prop} {a : α} {l : List α} :
   ⟨fun H => ⟨H _ (.head ..), fun _ h => H _ (.tail _ h)⟩,
    fun ⟨H₁, H₂⟩ _ => fun | .head .. => H₁ | .tail _ h => H₂ _ h⟩
 
+@[simp]
+theorem forall_mem_ne {a : α} {l : List α} : (∀ a' : α, a' ∈ l → ¬a = a') ↔ a ∉ l :=
+  ⟨fun h m => h _ m rfl, fun h _ m e => h (e.symm ▸ m)⟩
+
 theorem exists_mem_nil (p : α → Prop) : ¬ (∃ x, ∃ _ : x ∈ @nil α, p x) := nofun
 
 theorem forall_mem_nil (p : α → Prop) : ∀ (x) (_ : x ∈ @nil α), p x := nofun
@@ -394,6 +398,26 @@ theorem mem_iff_getElem? {a} {l : List α} : a ∈ l ↔ ∃ n : Nat, l[n]? = so
 theorem mem_iff_get? {a} {l : List α} : a ∈ l ↔ ∃ n, l.get? n = some a := by
   simp [getElem?_eq_some, Fin.exists_iff, mem_iff_get]
 
+theorem forall_getElem (l : List α) (p : α → Prop) :
+    (∀ (n : Nat) h, p (l[n]'h)) ↔ ∀ a, a ∈ l → p a := by
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    simp only [length_cons, mem_cons, forall_eq_or_imp]
+    constructor
+    · intro w
+      constructor
+      · exact w 0 (by simp)
+      · apply ih.1
+        intro n h
+        simpa using w (n+1) (Nat.add_lt_add_right h 1)
+    · rintro ⟨h, w⟩
+      rintro (_ | n) h
+      · simpa
+      · apply w
+        simp only [getElem_cons_succ]
+        exact getElem_mem l n (lt_of_succ_lt_succ h)
+
 @[simp] theorem decide_mem_cons [BEq α] [LawfulBEq α] {l : List α} :
     decide (y ∈ a :: l) = (y == a || decide (y ∈ l)) := by
   cases h : y == a <;> simp_all
@@ -422,7 +446,6 @@ theorem all_eq {l : List α} : l.all p = decide (∀ x, x ∈ l →  p x) := by
   match l, i with
   | [], _ => by
     simp at h
-    contradiction
   | _ :: _, 0 => by simp
   | _ :: l, i + 1 => by simp [getElem_set_eq]
 
@@ -937,6 +960,10 @@ theorem filter_congr {p q : α → Bool} :
 
 @[deprecated filter_congr (since := "2024-06-20")] abbrev filter_congr' := @filter_congr
 
+@[simp] theorem filter_sublist {p : α → Bool} : ∀ (l : List α), filter p l <+ l
+  | [] => .slnil
+  | a :: l => by rw [filter]; split <;> simp [Sublist.cons, Sublist.cons₂, filter_sublist l]
+
 /-! ### filterMap -/
 
 @[simp] theorem filterMap_cons_none {f : α → Option β} (a : α) (l : List α) (h : f a = none) :
@@ -1244,6 +1271,9 @@ theorem eq_nil_or_concat : ∀ l : List α, l = [] ∨ ∃ L b, l = concat L b
   | [] => by simp
   | b :: l => by simp [mem_join, or_and_right, exists_or]
 
+@[simp] theorem join_eq_nil_iff {L : List (List α)} : L.join = [] ↔ ∀ l ∈ L, l = [] := by
+  induction L <;> simp_all
+
 theorem exists_of_mem_join : a ∈ join L → ∃ l, l ∈ L ∧ a ∈ l := mem_join.1
 
 theorem mem_join_of_mem (lL : l ∈ L) (al : a ∈ l) : a ∈ join L := mem_join.2 ⟨l, lL, al⟩
@@ -1896,6 +1926,438 @@ variable [BEq α]
 
 end isSuffixOf
 
+/-! ### Subset -/
+
+/-! ### List subset -/
+
+theorem subset_def {l₁ l₂ : List α} : l₁ ⊆ l₂ ↔ ∀ {a : α}, a ∈ l₁ → a ∈ l₂ := .rfl
+
+@[simp] theorem nil_subset (l : List α) : [] ⊆ l := nofun
+
+@[simp] theorem Subset.refl (l : List α) : l ⊆ l := fun _ i => i
+
+theorem Subset.trans {l₁ l₂ l₃ : List α} (h₁ : l₁ ⊆ l₂) (h₂ : l₂ ⊆ l₃) : l₁ ⊆ l₃ :=
+  fun _ i => h₂ (h₁ i)
+
+instance : Trans (Membership.mem : α → List α → Prop) Subset Membership.mem :=
+  ⟨fun h₁ h₂ => h₂ h₁⟩
+
+instance : Trans (Subset : List α → List α → Prop) Subset Subset :=
+  ⟨Subset.trans⟩
+
+@[simp] theorem subset_cons (a : α) (l : List α) : l ⊆ a :: l := fun _ => Mem.tail _
+
+theorem subset_of_cons_subset {a : α} {l₁ l₂ : List α} : a :: l₁ ⊆ l₂ → l₁ ⊆ l₂ :=
+  fun s _ i => s (mem_cons_of_mem _ i)
+
+theorem subset_cons_of_subset (a : α) {l₁ l₂ : List α} : l₁ ⊆ l₂ → l₁ ⊆ a :: l₂ :=
+  fun s _ i => .tail _ (s i)
+
+theorem cons_subset_cons {l₁ l₂ : List α} (a : α) (s : l₁ ⊆ l₂) : a :: l₁ ⊆ a :: l₂ :=
+  fun _ => by simp only [mem_cons]; exact Or.imp_right (@s _)
+
+@[simp] theorem subset_append_left (l₁ l₂ : List α) : l₁ ⊆ l₁ ++ l₂ := fun _ => mem_append_left _
+
+@[simp] theorem subset_append_right (l₁ l₂ : List α) : l₂ ⊆ l₁ ++ l₂ := fun _ => mem_append_right _
+
+theorem subset_append_of_subset_left (l₂ : List α) : l ⊆ l₁ → l ⊆ l₁ ++ l₂ :=
+fun s => Subset.trans s <| subset_append_left _ _
+
+theorem subset_append_of_subset_right (l₁ : List α) : l ⊆ l₂ → l ⊆ l₁ ++ l₂ :=
+fun s => Subset.trans s <| subset_append_right _ _
+
+@[simp] theorem cons_subset : a :: l ⊆ m ↔ a ∈ m ∧ l ⊆ m := by
+  simp only [subset_def, mem_cons, or_imp, forall_and, forall_eq]
+
+@[simp] theorem append_subset {l₁ l₂ l : List α} :
+    l₁ ++ l₂ ⊆ l ↔ l₁ ⊆ l ∧ l₂ ⊆ l := by simp [subset_def, or_imp, forall_and]
+
+theorem subset_nil {l : List α} : l ⊆ [] ↔ l = [] :=
+  ⟨fun h => match l with | [] => rfl | _::_ => (nomatch h (.head ..)), fun | rfl => Subset.refl _⟩
+
+theorem map_subset {l₁ l₂ : List α} (f : α → β) (H : l₁ ⊆ l₂) : map f l₁ ⊆ map f l₂ :=
+  fun x => by simp only [mem_map]; exact .imp fun a => .imp_left (@H _)
+
+/-! ### Sublist and isSublist -/
+
+@[simp] theorem nil_sublist : ∀ l : List α, [] <+ l
+  | [] => .slnil
+  | a :: l => (nil_sublist l).cons a
+
+@[simp] theorem Sublist.refl : ∀ l : List α, l <+ l
+  | [] => .slnil
+  | a :: l => (Sublist.refl l).cons₂ a
+
+theorem Sublist.trans {l₁ l₂ l₃ : List α} (h₁ : l₁ <+ l₂) (h₂ : l₂ <+ l₃) : l₁ <+ l₃ := by
+  induction h₂ generalizing l₁ with
+  | slnil => exact h₁
+  | cons _ _ IH => exact (IH h₁).cons _
+  | @cons₂ l₂ _ a _ IH =>
+    generalize e : a :: l₂ = l₂'
+    match e ▸ h₁ with
+    | .slnil => apply nil_sublist
+    | .cons a' h₁' => cases e; apply (IH h₁').cons
+    | .cons₂ a' h₁' => cases e; apply (IH h₁').cons₂
+
+instance : Trans (@Sublist α) Sublist Sublist := ⟨Sublist.trans⟩
+
+@[simp] theorem sublist_cons (a : α) (l : List α) : l <+ a :: l := (Sublist.refl l).cons _
+
+theorem sublist_of_cons_sublist : a :: l₁ <+ l₂ → l₁ <+ l₂ :=
+  (sublist_cons a l₁).trans
+
+@[simp]
+theorem cons_sublist_cons : a :: l₁ <+ a :: l₂ ↔ l₁ <+ l₂ :=
+  ⟨fun | .cons _ s => sublist_of_cons_sublist s | .cons₂ _ s => s, .cons₂ _⟩
+
+theorem sublist_or_mem_of_sublist (h : l <+ l₁ ++ a :: l₂) : l <+ l₁ ++ l₂ ∨ a ∈ l := by
+  induction l₁ generalizing l with
+  | nil => match h with
+    | .cons _ h => exact .inl h
+    | .cons₂ _ h => exact .inr (.head ..)
+  | cons b l₁ IH =>
+    match h with
+    | .cons _ h => exact (IH h).imp_left (Sublist.cons _)
+    | .cons₂ _ h => exact (IH h).imp (Sublist.cons₂ _) (.tail _)
+
+theorem Sublist.subset : l₁ <+ l₂ → l₁ ⊆ l₂
+  | .slnil, _, h => h
+  | .cons _ s, _, h => .tail _ (s.subset h)
+  | .cons₂ .., _, .head .. => .head ..
+  | .cons₂ _ s, _, .tail _ h => .tail _ (s.subset h)
+
+instance : Trans (@Sublist α) Subset Subset :=
+  ⟨fun h₁ h₂ => trans h₁.subset h₂⟩
+
+instance : Trans Subset (@Sublist α) Subset :=
+  ⟨fun h₁ h₂ => trans h₁ h₂.subset⟩
+
+instance : Trans (Membership.mem : α → List α → Prop) Sublist Membership.mem :=
+  ⟨fun h₁ h₂ => h₂.subset h₁⟩
+
+theorem mem_of_cons_sublist {a : α} {l₁ l₂ : List α} (s : a :: l₁ <+ l₂) : a ∈ l₂ :=
+  (cons_subset.1 s.subset).1
+
+@[simp] theorem sublist_nil {l : List α} : l <+ [] ↔ l = [] :=
+  ⟨fun s => subset_nil.1 s.subset, fun H => H ▸ Sublist.refl _⟩
+
+theorem Sublist.length_le : l₁ <+ l₂ → length l₁ ≤ length l₂
+  | .slnil => Nat.le_refl 0
+  | .cons _l s => le_succ_of_le (length_le s)
+  | .cons₂ _ s => succ_le_succ (length_le s)
+
+theorem Sublist.eq_of_length : l₁ <+ l₂ → length l₁ = length l₂ → l₁ = l₂
+  | .slnil, _ => rfl
+  | .cons a s, h => nomatch Nat.not_lt.2 s.length_le (h ▸ lt_succ_self _)
+  | .cons₂ a s, h => by rw [s.eq_of_length (succ.inj h)]
+
+theorem Sublist.eq_of_length_le (s : l₁ <+ l₂) (h : length l₂ ≤ length l₁) : l₁ = l₂ :=
+  s.eq_of_length <| Nat.le_antisymm s.length_le h
+
+protected theorem Sublist.map (f : α → β) {l₁ l₂} (s : l₁ <+ l₂) : map f l₁ <+ map f l₂ := by
+  induction s with
+  | slnil => simp
+  | cons a s ih =>
+    simpa using cons (f a) ih
+  | cons₂ a s ih =>
+    simpa using cons₂ (f a) ih
+
+protected theorem Sublist.filterMap (f : α → Option β) (s : l₁ <+ l₂) :
+    filterMap f l₁ <+ filterMap f l₂ := by
+  induction s <;> simp [filterMap_cons] <;> split <;> simp [*, cons, cons₂]
+
+protected theorem Sublist.filter (p : α → Bool) {l₁ l₂} (s : l₁ <+ l₂) : filter p l₁ <+ filter p l₂ := by
+  rw [← filterMap_eq_filter]; apply s.filterMap
+
+theorem sublist_filterMap_iff {l₁ : List β} {f : α → Option β} :
+    l₁ <+ l₂.filterMap f ↔ ∃ l', l' <+ l₂ ∧ l₁ = l'.filterMap f := by
+  induction l₂ generalizing l₁ with
+  | nil => simp
+  | cons a l₂ ih =>
+    simp only [filterMap_cons]
+    split
+    · simp only [ih]
+      constructor
+      · rintro ⟨l', h, rfl⟩
+        exact ⟨l', Sublist.cons a h, rfl⟩
+      · rintro ⟨l', h, rfl⟩
+        cases h with
+        | cons _ h =>
+          exact ⟨l', h, rfl⟩
+        | cons₂ _ h =>
+          rename_i l'
+          exact ⟨l', h, by simp_all⟩
+    · constructor
+      · intro w
+        cases w with
+        | cons _ h =>
+          obtain ⟨l', s, rfl⟩ := ih.1 h
+          exact ⟨l', Sublist.cons a s, rfl⟩
+        | cons₂ _ h =>
+          rename_i l'
+          obtain ⟨l', s, rfl⟩ := ih.1 h
+          refine ⟨a :: l', Sublist.cons₂ a s, ?_⟩
+          rwa [filterMap_cons_some]
+      · rintro ⟨l', h, rfl⟩
+        replace h := h.filterMap f
+        rwa [filterMap_cons_some] at h
+        assumption
+
+theorem sublist_map_iff {l₁ : List β} {f : α → β} :
+    l₁ <+ l₂.map f ↔ ∃ l', l' <+ l₂ ∧ l₁ = l'.map f := by
+  simp only [← filterMap_eq_map, sublist_filterMap_iff]
+
+theorem sublist_filter_iff {l₁ : List α} {p : α → Bool} :
+    l₁ <+ l₂.filter p ↔ ∃ l', l' <+ l₂ ∧ l₁ = l'.filter p := by
+  simp only [← filterMap_eq_filter, sublist_filterMap_iff]
+
+@[simp] theorem sublist_append_left : ∀ l₁ l₂ : List α, l₁ <+ l₁ ++ l₂
+  | [], _ => nil_sublist _
+  | _ :: l₁, l₂ => (sublist_append_left l₁ l₂).cons₂ _
+
+@[simp] theorem sublist_append_right : ∀ l₁ l₂ : List α, l₂ <+ l₁ ++ l₂
+  | [], _ => Sublist.refl _
+  | _ :: l₁, l₂ => (sublist_append_right l₁ l₂).cons _
+
+@[simp] theorem singleton_sublist {a : α} {l} : [a] <+ l ↔ a ∈ l := by
+  refine ⟨fun h => h.subset (mem_singleton_self _), fun h => ?_⟩
+  obtain ⟨_, _, rfl⟩ := append_of_mem h
+  exact ((nil_sublist _).cons₂ _).trans (sublist_append_right ..)
+
+theorem sublist_append_of_sublist_left (s : l <+ l₁) : l <+ l₁ ++ l₂ :=
+  s.trans <| sublist_append_left ..
+
+theorem sublist_append_of_sublist_right (s : l <+ l₂) : l <+ l₁ ++ l₂ :=
+  s.trans <| sublist_append_right ..
+
+@[simp] theorem append_sublist_append_left : ∀ l, l ++ l₁ <+ l ++ l₂ ↔ l₁ <+ l₂
+  | [] => Iff.rfl
+  | _ :: l => cons_sublist_cons.trans (append_sublist_append_left l)
+
+theorem Sublist.append_left : l₁ <+ l₂ → ∀ l, l ++ l₁ <+ l ++ l₂ :=
+  fun h l => (append_sublist_append_left l).mpr h
+
+theorem Sublist.append_right : l₁ <+ l₂ → ∀ l, l₁ ++ l <+ l₂ ++ l
+  | .slnil, _ => Sublist.refl _
+  | .cons _ h, _ => (h.append_right _).cons _
+  | .cons₂ _ h, _ => (h.append_right _).cons₂ _
+
+theorem Sublist.append (hl : l₁ <+ l₂) (hr : r₁ <+ r₂) : l₁ ++ r₁ <+ l₂ ++ r₂ :=
+  (hl.append_right _).trans ((append_sublist_append_left _).2 hr)
+
+theorem sublist_cons_iff {a : α} {l l'} :
+    l <+ a :: l' ↔ l <+ l' ∨ ∃ r, l = a :: r ∧ r <+ l' := by
+  constructor
+  · intro h
+    cases h with
+    | cons _ h => exact Or.inl h
+    | cons₂ _ h => exact Or.inr ⟨_, rfl, h⟩
+  · rintro (h | ⟨r, rfl, h⟩)
+    · exact h.cons _
+    · exact h.cons₂ _
+
+theorem cons_sublist_iff {a : α} {l l'} :
+    a :: l <+ l' ↔ ∃ r₁ r₂, l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂ := by
+  induction l' with
+  | nil => simp
+  | cons a' l' ih =>
+    constructor
+    · intro w
+      cases w with
+      | cons _ w =>
+        obtain ⟨r₁, r₂, rfl, h₁, h₂⟩ := ih.1 w
+        exact ⟨a' :: r₁, r₂, by simp, mem_cons_of_mem a' h₁, h₂⟩
+      | cons₂ _ w =>
+        exact ⟨[a], l', by simp, mem_singleton_self _, w⟩
+    · rintro ⟨r₁, r₂, w, h₁, h₂⟩
+      rw [w, ← singleton_append]
+      exact Sublist.append (by simpa) h₂
+
+theorem sublist_append_iff {l : List α} :
+    l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂ := by
+  induction r₁ generalizing l with
+  | nil =>
+    constructor
+    · intro w
+      refine ⟨[], l, by simp_all⟩
+    · rintro ⟨l₁, l₂, rfl, w₁, w₂⟩
+      simp_all
+  | cons r r₁ ih =>
+    constructor
+    · intro w
+      simp only [cons_append] at w
+      cases w with
+      | cons _ w =>
+        obtain ⟨l₁, l₂, rfl, w₁, w₂⟩ := ih.1 w
+        exact ⟨l₁, l₂, rfl, Sublist.cons r w₁, w₂⟩
+      | cons₂ _ w =>
+        rename_i l
+        obtain ⟨l₁, l₂, rfl, w₁, w₂⟩ := ih.1 w
+        refine ⟨r :: l₁, l₂, by simp, cons_sublist_cons.mpr w₁, w₂⟩
+    · rintro ⟨l₁, l₂, rfl, w₁, w₂⟩
+      cases w₁ with
+      | cons _ w₁ =>
+        exact Sublist.cons _ (Sublist.append w₁ w₂)
+      | cons₂ _ w₁ =>
+        rename_i l
+        exact Sublist.cons₂ _ (Sublist.append w₁ w₂)
+
+theorem append_sublist_iff {l₁ l₂ : List α} :
+    l₁ ++ l₂ <+ r ↔ ∃ r₁ r₂, r = r₁ ++ r₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂ := by
+  induction l₁ generalizing r with
+  | nil =>
+    constructor
+    · intro w
+      refine ⟨[], r, by simp_all⟩
+    · rintro ⟨r₁, r₂, rfl, -, w₂⟩
+      simp only [nil_append]
+      exact sublist_append_of_sublist_right w₂
+  | cons a l₁ ih =>
+    constructor
+    · rw [cons_append, cons_sublist_iff]
+      rintro ⟨r₁, r₂, rfl, h₁, h₂⟩
+      obtain ⟨s₁, s₂, rfl, t₁, t₂⟩ := ih.1 h₂
+      refine ⟨r₁ ++ s₁, s₂, by simp, ?_, t₂⟩
+      rw [← singleton_append]
+      exact Sublist.append (by simpa) t₁
+    · rintro ⟨r₁, r₂, rfl, h₁, h₂⟩
+      exact Sublist.append h₁ h₂
+
+theorem Sublist.reverse : l₁ <+ l₂ → l₁.reverse <+ l₂.reverse
+  | .slnil => Sublist.refl _
+  | .cons _ h => by rw [reverse_cons]; exact sublist_append_of_sublist_left h.reverse
+  | .cons₂ _ h => by rw [reverse_cons, reverse_cons]; exact h.reverse.append_right _
+
+@[simp] theorem reverse_sublist : l₁.reverse <+ l₂.reverse ↔ l₁ <+ l₂ :=
+  ⟨fun h => l₁.reverse_reverse ▸ l₂.reverse_reverse ▸ h.reverse, Sublist.reverse⟩
+
+theorem sublist_reverse_iff : l₁ <+ l₂.reverse ↔ l₁.reverse <+ l₂ :=
+  by rw [← reverse_sublist, reverse_reverse]
+
+@[simp] theorem append_sublist_append_right (l) : l₁ ++ l <+ l₂ ++ l ↔ l₁ <+ l₂ :=
+  ⟨fun h => by
+    have := h.reverse
+    simp only [reverse_append, append_sublist_append_left, reverse_sublist] at this
+    exact this,
+   fun h => h.append_right l⟩
+
+@[simp] theorem replicate_sublist_replicate {m n} (a : α) :
+    replicate m a <+ replicate n a ↔ m ≤ n := by
+  refine ⟨fun h => ?_, fun h => ?_⟩
+  · have := h.length_le; simp only [length_replicate] at this ⊢; exact this
+  · induction h with
+    | refl => apply Sublist.refl
+    | step => simp [*, replicate, Sublist.cons]
+
+theorem sublist_replicate_iff : l <+ replicate m a ↔ ∃ n, n ≤ m ∧ l = replicate n a := by
+  induction l generalizing m with
+  | nil =>
+    simp only [nil_sublist, true_iff]
+    exact ⟨0, zero_le m, by simp⟩
+  | cons b l ih =>
+    constructor
+    · intro w
+      cases m with
+      | zero => simp at w
+      | succ m =>
+        simp [replicate_succ] at w
+        cases w with
+        | cons _ w =>
+          obtain ⟨n, le, rfl⟩ := ih.1 (sublist_of_cons_sublist w)
+          obtain rfl := (mem_replicate.1 (mem_of_cons_sublist w)).2
+          exact ⟨n+1, Nat.add_le_add_right le 1, rfl⟩
+        | cons₂ _ w =>
+          obtain ⟨n, le, rfl⟩ := ih.1 w
+          refine ⟨n+1, Nat.add_le_add_right le 1, by simp [replicate_succ]⟩
+    · rintro ⟨n, le, w⟩
+      rw [w]
+      exact (replicate_sublist_replicate a).2 le
+
+theorem sublist_join_of_mem {L : List (List α)} {l} (h : l ∈ L) : l <+ L.join := by
+  induction L with
+  | nil => cases h
+  | cons l' L ih =>
+    rcases mem_cons.1 h with (rfl | h)
+    · simp [h]
+    · simp [ih h, join_cons, sublist_append_of_sublist_right]
+
+theorem sublist_join_iff {L : List (List α)} {l} :
+    l <+ L.join ↔
+      ∃ L' : List (List α), l = L'.join ∧ ∀ i (_ : i < L'.length), L'[i] <+ L[i]?.getD [] := by
+  induction L generalizing l with
+  | nil =>
+    constructor
+    · intro w
+      simp only [join_nil, sublist_nil] at w
+      subst w
+      exact ⟨[], by simp, fun i x => by cases x⟩
+    · rintro ⟨L', rfl, h⟩
+      simp only [join_nil, sublist_nil, join_eq_nil_iff]
+      simp only [getElem?_nil, Option.getD_none, sublist_nil] at h
+      exact (forall_getElem L' (· = [])).1 h
+  | cons l' L ih =>
+    simp only [join_cons, sublist_append_iff, ih]
+    constructor
+    · rintro ⟨l₁, l₂, rfl, s, L', rfl, h⟩
+      refine ⟨l₁ :: L', by simp, ?_⟩
+      intro i lt
+      cases i <;> simp_all
+    · rintro ⟨L', rfl, h⟩
+      cases L' with
+      | nil =>
+        exact ⟨[], [], by simp, by simp, [], by simp, fun i x => by cases x⟩
+      | cons l₁ L' =>
+        exact ⟨l₁, L'.join, by simp, by simpa using h 0 (by simp), L', rfl,
+          fun i lt => by simpa using h (i+1) (Nat.add_lt_add_right lt 1)⟩
+
+theorem join_sublist_iff {L : List (List α)} {l} :
+    L.join <+ l ↔
+      ∃ L' : List (List α), l = L'.join ∧ ∀ i (_ : i < L.length), L[i] <+ L'[i]?.getD [] := by
+  induction L generalizing l with
+  | nil =>
+    constructor
+    · intro _
+      exact ⟨[l], by simp, fun i x => by cases x⟩
+    · rintro ⟨L', rfl, _⟩
+      simp only [join_nil, nil_sublist]
+  | cons l' L ih =>
+    simp only [join_cons, append_sublist_iff, ih]
+    constructor
+    · rintro ⟨l₁, l₂, rfl, s, L', rfl, h⟩
+      refine ⟨l₁ :: L', by simp, ?_⟩
+      intro i lt
+      cases i <;> simp_all
+    · rintro ⟨L', rfl, h⟩
+      cases L' with
+      | nil =>
+        exact ⟨[], [], by simp, by simpa using h 0 (by simp), [], by simp,
+          fun i x => by simpa using h (i+1) (Nat.add_lt_add_right x 1)⟩
+      | cons l₁ L' =>
+        exact ⟨l₁, L'.join, by simp, by simpa using h 0 (by simp), L', rfl,
+          fun i lt => by simpa using h (i+1) (Nat.add_lt_add_right lt 1)⟩
+
+@[simp] theorem isSublist_iff_sublist [BEq α] [LawfulBEq α] {l₁ l₂ : List α} :
+    l₁.isSublist l₂ ↔ l₁ <+ l₂ := by
+  cases l₁ <;> cases l₂ <;> simp [isSublist]
+  case cons.cons hd₁ tl₁ hd₂ tl₂ =>
+    if h_eq : hd₁ = hd₂ then
+      simp [h_eq, cons_sublist_cons, isSublist_iff_sublist]
+    else
+      simp only [beq_iff_eq, h_eq]
+      constructor
+      · intro h_sub
+        apply Sublist.cons
+        exact isSublist_iff_sublist.mp h_sub
+      · intro h_sub
+        cases h_sub
+        case cons h_sub =>
+          exact isSublist_iff_sublist.mpr h_sub
+        case cons₂ =>
+          contradiction
+
+instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <+ l₂) :=
+  decidable_of_iff (l₁.isSublist l₂) isSublist_iff_sublist
+
 /-! ### rotateLeft -/
 
 @[simp] theorem rotateLeft_zero (l : List α) : rotateLeft l 0 = l := by
@@ -1912,6 +2374,97 @@ end isSuffixOf
 -- TODO Batteries defines its own `getElem?_rotate`, which we need to adapt.
 -- TODO Prove `map_rotateRight`, using `ext` and `getElem?_rotateRight`.
 
+/-! ## Pairwise and Nodup -/
+
+/-! ### Pairwise -/
+
+theorem Pairwise.sublist : l₁ <+ l₂ → l₂.Pairwise R → l₁.Pairwise R
+  | .slnil, h => h
+  | .cons _ s, .cons _ h₂ => h₂.sublist s
+  | .cons₂ _ s, .cons h₁ h₂ => (h₂.sublist s).cons fun _ h => h₁ _ (s.subset h)
+
+theorem pairwise_map {l : List α} :
+    (l.map f).Pairwise R ↔ l.Pairwise fun a b => R (f a) (f b) := by
+  induction l
+  · simp
+  · simp only [map, pairwise_cons, forall_mem_map_iff, *]
+
+theorem pairwise_append {l₁ l₂ : List α} :
+    (l₁ ++ l₂).Pairwise R ↔ l₁.Pairwise R ∧ l₂.Pairwise R ∧ ∀ a ∈ l₁, ∀ b ∈ l₂, R a b := by
+  induction l₁ <;> simp [*, or_imp, forall_and, and_assoc, and_left_comm]
+
+theorem pairwise_reverse {l : List α} :
+    l.reverse.Pairwise R ↔ l.Pairwise (fun a b => R b a) := by
+  induction l <;> simp [*, pairwise_append, and_comm]
+
+@[simp] theorem pairwise_replicate {n : Nat} {a : α} :
+    (replicate n a).Pairwise R ↔ n ≤ 1 ∨ R a a := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    simp only [replicate_succ, pairwise_cons, mem_replicate, ne_eq, and_imp,
+      forall_eq_apply_imp_iff, ih]
+    constructor
+    · rintro ⟨h, h' | h'⟩
+      · by_cases w : n = 0
+        · left
+          subst w
+          simp
+        · right
+          exact h w
+      · right
+        exact h'
+    · rintro (h | h)
+      · obtain rfl := eq_zero_of_le_zero (le_of_lt_succ h)
+        simp
+      · exact ⟨fun _ => h, Or.inr h⟩
+
+theorem Pairwise.imp {α R S} (H : ∀ {a b}, R a b → S a b) :
+    ∀ {l : List α}, l.Pairwise R → l.Pairwise S
+  | _, .nil => .nil
+  | _, .cons h₁ h₂ => .cons (H ∘ h₁ ·) (h₂.imp H)
+
+/-! ### Nodup -/
+
+@[simp]
+theorem nodup_nil : @Nodup α [] :=
+  Pairwise.nil
+
+@[simp]
+theorem nodup_cons {a : α} {l : List α} : Nodup (a :: l) ↔ a ∉ l ∧ Nodup l := by
+  simp only [Nodup, pairwise_cons, forall_mem_ne]
+
+theorem Nodup.sublist : l₁ <+ l₂ → Nodup l₂ → Nodup l₁ :=
+  Pairwise.sublist
+
+theorem Sublist.nodup : l₁ <+ l₂ → Nodup l₂ → Nodup l₁ :=
+  Nodup.sublist
+
+theorem getElem?_inj {xs : List α}
+    (h₀ : i < xs.length) (h₁ : Nodup xs) (h₂ : xs[i]? = xs[j]?) : i = j := by
+  induction xs generalizing i j with
+  | nil => cases h₀
+  | cons x xs ih =>
+    match i, j with
+    | 0, 0 => rfl
+    | i+1, j+1 =>
+      cases h₁ with
+      | cons ha h₁ =>
+        simp only [getElem?_cons_succ] at h₂
+        exact congrArg (· + 1) (ih (Nat.lt_of_succ_lt_succ h₀) h₁ h₂)
+    | i+1, 0 => ?_
+    | 0, j+1 => ?_
+    all_goals
+      simp only [get?_eq_getElem?, getElem?_cons_zero, getElem?_cons_succ] at h₂
+      cases h₁; rename_i h' h
+      have := h x ?_ rfl; cases this
+      rw [mem_iff_get?]
+      simp only [get?_eq_getElem?]
+    exact ⟨_, h₂⟩; exact ⟨_ , h₂.symm⟩
+
+@[simp] theorem nodup_replicate {n : Nat} {a : α} :
+    (replicate n a).Nodup ↔ n ≤ 1 := by simp [Nodup]
+
 /-! ## Manipulating elements -/
 
 /-! ### replace -/
@@ -1983,7 +2536,7 @@ theorem eq_or_mem_of_mem_insert {l : List α} (h : a ∈ l.insert b) : a = b ∨
 end insert
 
 /-! ### erase -/
-
+-- Results here can be refactored to use results about `eraseP` if this is later moved to Lean.
 section erase
 variable [BEq α]
 
@@ -2008,6 +2561,37 @@ theorem erase_of_not_mem [LawfulBEq α] {a : α} : ∀ {l : List α}, a ∉ l
   rw [erase_of_not_mem]
   simp_all
 
+theorem erase_sublist (a : α) (l : List α) : l.erase a <+ l := by
+  induction l with
+  | nil => simp
+  | cons b l ih =>
+    simp only [erase_cons]
+    split
+    · exact sublist_cons b l
+    · exact cons_sublist_cons.mpr ih
+
+theorem Nodup.erase_eq_filter [BEq α] [LawfulBEq α] {l} (d : Nodup l) (a : α) : l.erase a = l.filter (· != a) := by
+  induction d with
+  | nil => rfl
+  | cons m _n ih =>
+    rename_i b l
+    by_cases h : b = a
+    · subst h
+      rw [erase_cons_head, filter_cons_of_neg _ (by simp)]
+      apply Eq.symm
+      rw [filter_eq_self]
+      simpa [@eq_comm α] using m
+    · simp [beq_false_of_ne h, ih, h]
+
+theorem Nodup.mem_erase_iff [BEq α] [LawfulBEq α] {a : α} (d : Nodup l) : a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l := by
+  rw [Nodup.erase_eq_filter d, mem_filter, and_comm, bne_iff_ne]
+
+theorem Nodup.not_mem_erase [BEq α] [LawfulBEq α] {a : α} (h : Nodup l) : a ∉ l.erase a := fun H => by
+  simpa using ((Nodup.mem_erase_iff h).mp H).left
+
+theorem Nodup.erase [BEq α] [LawfulBEq α] (a : α) : Nodup l → Nodup (l.erase a) :=
+  Nodup.sublist <| erase_sublist _ _
+
 end erase
 
 /-! ### find? -/
@@ -2089,8 +2673,9 @@ theorem findSome?_replicate : findSome? f (replicate n a) = if n = 0 then none e
 @[simp] theorem findSome?_replicate_of_pos (h : 0 < n) : findSome? f (replicate n a) = f a := by
   simp [findSome?_replicate, Nat.ne_of_gt h]
 
-@[simp] theorem find?_replicate_of_isSome (h : (f a).isSome) : findSome? f (replicate n a) = if n = 0 then none else f a := by
-  simp [findSome?_replicate, h]
+-- Argument is unused, but used to decide whether `simp` should unfold.
+@[simp] theorem find?_replicate_of_isSome (_ : (f a).isSome) : findSome? f (replicate n a) = if n = 0 then none else f a := by
+  simp [findSome?_replicate]
 
 @[simp] theorem find?_replicate_of_isNone (h : (f a).isNone) : findSome? f (replicate n a) = none := by
   rw [Option.isNone_iff_eq_none] at h

src/Init/Data/List/TakeDrop.lean

@@ -383,6 +383,29 @@ theorem minimum?_eq_some_iff' {xs : List Nat} :
     (min_eq_or := fun _ _ => by omega)
     (le_min_iff := fun _ _ _ => by omega)
 
+-- This could be generalized,
+-- but will first require further work on order typeclasses in the core repository.
+theorem minimum?_cons' {a : Nat} {l : List Nat} :
+    (a :: l).minimum? = some (match l.minimum? with
+    | none => a
+    | some m => min a m) := by
+  rw [minimum?_eq_some_iff']
+  split <;> rename_i h m
+  · simp_all
+  · rw [minimum?_eq_some_iff'] at m
+    obtain ⟨m, le⟩ := m
+    rw [Nat.min_def]
+    constructor
+    · split
+      · exact mem_cons_self a l
+      · exact mem_cons_of_mem a m
+    · intro b m
+      cases List.mem_cons.1 m with
+      | inl => split <;> omega
+      | inr h =>
+        specialize le b h
+        split <;> omega
+
 /-! ### maximum? -/
 
 -- A specialization of `maximum?_eq_some_iff` to Nat.
@@ -393,4 +416,27 @@ theorem maximum?_eq_some_iff' {xs : List Nat} :
     (max_eq_or := fun _ _ => by omega)
     (max_le_iff := fun _ _ _ => by omega)
 
+-- This could be generalized,
+-- but will first require further work on order typeclasses in the core repository.
+theorem maximum?_cons' {a : Nat} {l : List Nat} :
+    (a :: l).maximum? = some (match l.maximum? with
+    | none => a
+    | some m => max a m) := by
+  rw [maximum?_eq_some_iff']
+  split <;> rename_i h m
+  · simp_all
+  · rw [maximum?_eq_some_iff'] at m
+    obtain ⟨m, le⟩ := m
+    rw [Nat.max_def]
+    constructor
+    · split
+      · exact mem_cons_of_mem a m
+      · exact mem_cons_self a l
+    · intro b m
+      cases List.mem_cons.1 m with
+      | inl => split <;> omega
+      | inr h =>
+        specialize le b h
+        split <;> omega
+
 end List

src/Init/Data/Nat/Basic.lean

@@ -100,6 +100,7 @@ def blt (a b : Nat) : Bool :=
   ble a.succ b
 
 attribute [simp] Nat.zero_le
+attribute [simp] Nat.not_lt_zero
 
 /-! # Helper "packing" theorems -/
 

src/Init/Data/Option/Basic.lean

@@ -19,6 +19,7 @@ def getM [Alternative m] : Option α → m α
   | some a   => pure a
 
 @[deprecated getM (since := "2024-04-17")]
+-- `[Monad m]` is not needed here.
 def toMonad [Monad m] [Alternative m] : Option α → m α := getM
 
 /-- Returns `true` on `some x` and `false` on `none`. -/

src/Init/Data/Option/Lemmas.lean

@@ -82,7 +82,7 @@ theorem isSome_iff_exists : isSome x ↔ ∃ a, x = some a := by cases x <;> sim
   cases a <;> simp
 
 theorem eq_some_iff_get_eq : o = some a ↔ ∃ h : o.isSome, o.get h = a := by
-  cases o <;> simp; nofun
+  cases o <;> simp
 
 theorem eq_some_of_isSome : ∀ {o : Option α} (h : o.isSome), o = some (o.get h)
   | some _, _ => rfl

src/Init/Ext.lean

@@ -10,58 +10,38 @@ import Init.RCases
 
 namespace Lean
 namespace Parser.Attr
-/-- Registers an extensionality theorem.
+
+/--
+The flag `(iff := false)` prevents `ext` from generating an `ext_iff` lemma.
+-/
+syntax extIff := atomic("(" &"iff" " := " &"false" ")")
+
+/--
+The flag `(flat := false)` causes `ext` to not flatten parents' fields when generating an `ext` lemma.
+-/
+syntax extFlat := atomic("(" &"flat" " := " &"false" ")")
+
+/--
+Registers an extensionality theorem.
 
 * When `@[ext]` is applied to a structure, it generates `.ext` and `.ext_iff` theorems and registers
   them for the `ext` tactic.
 
-* When `@[ext]` is applied to a theorem, the theorem is registered for the `ext` tactic.
+* When `@[ext]` is applied to a theorem, the theorem is registered for the `ext` tactic, and it generates an `ext_iff` theorem.
+  The name of the theorem is from adding the suffix `_iff` to the theorem name.
 
 * An optional natural number argument, e.g. `@[ext 9000]`, specifies a priority for the lemma. Higher-priority lemmas are chosen first, and the default is `1000`.
 
+* The flag `@[ext (iff := false)]` prevents it from generating an `ext_iff` theorem.
+
 * The flag `@[ext (flat := false)]` causes generated structure extensionality theorems to show inherited fields based on their representation,
   rather than flattening the parents' fields into the lemma's equality hypotheses.
-  structures in the generated extensionality theorems. -/
-syntax (name := ext) "ext" (" (" &"flat" " := " term ")")? (ppSpace prio)? : attr
+-/
+syntax (name := ext) "ext" (ppSpace extIff)? (ppSpace extFlat)? (ppSpace prio)? : attr
 end Parser.Attr
 
 -- TODO: rename this namespace?
--- Remark: `ext` has scoped syntax, Mathlib may depend on the actual namespace name.
 namespace Elab.Tactic.Ext
-/--
-Creates the type of the extensionality theorem for the given structure,
-elaborating to `x.1 = y.1 → x.2 = y.2 → x = y`, for example.
--/
-scoped syntax (name := extType) "ext_type% " term:max ppSpace ident : term
-
-/--
-Creates the type of the iff-variant of the extensionality theorem for the given structure,
-elaborating to `x = y ↔ x.1 = y.1 ∧ x.2 = y.2`, for example.
--/
-scoped syntax (name := extIffType) "ext_iff_type% " term:max ppSpace ident : term
-
-/--
-`declare_ext_theorems_for A` declares the extensionality theorems for the structure `A`.
-
-These theorems state that two expressions with the structure type are equal if their fields are equal.
--/
-syntax (name := declareExtTheoremFor) "declare_ext_theorems_for " ("(" &"flat" " := " term ") ")? ident (ppSpace prio)? : command
-
-macro_rules | `(declare_ext_theorems_for $[(flat := $f)]? $struct:ident $(prio)?) => do
-  let flat := f.getD (mkIdent `true)
-  let names ← Macro.resolveGlobalName struct.getId.eraseMacroScopes
-  let name ← match names.filter (·.2.isEmpty) with
-    | [] => Macro.throwError s!"unknown constant {struct.getId}"
-    | [(name, _)] => pure name
-    | _ => Macro.throwError s!"ambiguous name {struct.getId}"
-  let extName := mkIdentFrom struct (canonical := true) <| name.mkStr "ext"
-  let extIffName := mkIdentFrom struct (canonical := true) <| name.mkStr "ext_iff"
-  `(@[ext $(prio)?] protected theorem $extName:ident : ext_type% $flat $struct:ident :=
-      fun {..} {..} => by intros; subst_eqs; rfl
-    protected theorem $extIffName:ident : ext_iff_type% $flat $struct:ident :=
-      fun {..} {..} =>
-        ⟨fun h => by cases h; and_intros <;> rfl,
-         fun _ => by (repeat cases ‹_ ∧ _›); subst_eqs; rfl⟩)
 
 /--
 Applies extensionality lemmas that are registered with the `@[ext]` attribute.
@@ -96,19 +76,8 @@ macro "ext1" xs:(colGt ppSpace rintroPat)* : tactic =>
 end Elab.Tactic.Ext
 end Lean
 
+attribute [ext] Prod PProd Sigma PSigma
 attribute [ext] funext propext Subtype.eq
 
-@[ext] theorem Prod.ext : {x y : Prod α β} → x.fst = y.fst → x.snd = y.snd → x = y
-  | ⟨_,_⟩, ⟨_,_⟩, rfl, rfl => rfl
-
-@[ext] theorem PProd.ext : {x y : PProd α β} → x.fst = y.fst → x.snd = y.snd → x = y
-  | ⟨_,_⟩, ⟨_,_⟩, rfl, rfl => rfl
-
-@[ext] theorem Sigma.ext : {x y : Sigma β} → x.fst = y.fst → HEq x.snd y.snd → x = y
-  | ⟨_,_⟩, ⟨_,_⟩, rfl, .rfl => rfl
-
-@[ext] theorem PSigma.ext : {x y : PSigma β} → x.fst = y.fst → HEq x.snd y.snd → x = y
-  | ⟨_,_⟩, ⟨_,_⟩, rfl, .rfl => rfl
-
 @[ext] protected theorem PUnit.ext (x y : PUnit) : x = y := rfl
 protected theorem Unit.ext (x y : Unit) : x = y := rfl

src/Init/GetElem.lean

@@ -179,11 +179,9 @@ instance [GetElem? cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] :
 @[simp] theorem getElem_fin [GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
     a[i] = a[i.1] := rfl
 
-@[simp] theorem getElem?_fin [h : GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n)
-    [Decidable (Dom a i)] : a[i]? = a[i.1]? := by rfl
+@[simp] theorem getElem?_fin [h : GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) : a[i]? = a[i.1]? := by rfl
 
-@[simp] theorem getElem!_fin [GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n)
-    [Decidable (Dom a i)] [Inhabited Elem] : a[i]! = a[i.1]! := rfl
+@[simp] theorem getElem!_fin [GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) [Inhabited Elem] : a[i]! = a[i.1]! := rfl
 
 macro_rules
   | `(tactic| get_elem_tactic_trivial) => `(tactic| apply Fin.val_lt_of_le; get_elem_tactic_trivial; done)

src/Init/Omega/LinearCombo.lean

@@ -38,6 +38,10 @@ theorem ext {a b : LinearCombo} (w₁ : a.const = b.const) (w₂ : a.coeffs = b.
   subst w₁; subst w₂
   congr
 
+/-- Check if a linear combination is an atom, i.e. the constant term is zero and there is exactly one nonzero coefficient, which is one. -/
+def isAtom (a : LinearCombo) : Bool :=
+  a.const == 0 && (a.coeffs.filter (· == 1)).length == 1 && a.coeffs.all fun c => c == 0 || c == 1
+
 /--
 Evaluate a linear combination `⟨r, [c_1, …, c_k]⟩` at values `[v_1, …, v_k]` to obtain
 `r + (c_1 * x_1 + (c_2 * x_2 + ... (c_k * x_k + 0))))`.

src/Init/PropLemmas.lean

@@ -253,6 +253,9 @@ end forall_congr
 
 @[simp] theorem not_exists : (¬∃ x, p x) ↔ ∀ x, ¬p x := exists_imp
 
+theorem forall_not_of_not_exists (h : ¬∃ x, p x) : ∀ x, ¬p x := not_exists.mp h
+theorem not_exists_of_forall_not (h : ∀ x, ¬p x) : ¬∃ x, p x := not_exists.mpr h
+
 theorem forall_and : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x) :=
   ⟨fun h => ⟨fun x => (h x).1, fun x => (h x).2⟩, fun ⟨h₁, h₂⟩ x => ⟨h₁ x, h₂ x⟩⟩
 

src/Init/SimpLemmas.lean

@@ -129,6 +129,7 @@ instance : Std.LawfulIdentity Or False where
 @[simp] theorem iff_false (p : Prop) : (p ↔ False) = ¬p := propext ⟨(·.1), (⟨·, False.elim⟩)⟩
 @[simp] theorem false_iff (p : Prop) : (False ↔ p) = ¬p := propext ⟨(·.2), (⟨False.elim, ·⟩)⟩
 @[simp] theorem false_implies (p : Prop) : (False → p) = True := eq_true False.elim
+@[simp] theorem forall_false (p : False → Prop) : (∀ h : False, p h) = True := eq_true (False.elim ·)
 @[simp] theorem implies_true (α : Sort u) : (α → True) = True := eq_true fun _ => trivial
 @[simp] theorem true_implies (p : Prop) : (True → p) = p := propext ⟨(· trivial), (fun _ => ·)⟩
 @[simp] theorem not_false_eq_true : (¬ False) = True := eq_true False.elim

src/Init/System/IO.lean

@@ -712,8 +712,17 @@ structure Child (cfg : StdioConfig) where
 
 @[extern "lean_io_process_spawn"] opaque spawn (args : SpawnArgs) : IO (Child args.toStdioConfig)
 
+/--
+Block until the child process has exited and return its exit code.
+-/
 @[extern "lean_io_process_child_wait"] opaque Child.wait {cfg : @& StdioConfig} : @& Child cfg → IO UInt32
 
+/--
+Check whether the child has exited yet. If it hasn't return none, otherwise its exit code.
+-/
+@[extern "lean_io_process_child_try_wait"] opaque Child.tryWait {cfg : @& StdioConfig} : @& Child cfg →
+    IO (Option UInt32)
+
 /-- Terminates the child process using the SIGTERM signal or a platform analogue.
     If the process was started using `SpawnArgs.setsid`, terminates the entire process group instead. -/
 @[extern "lean_io_process_child_kill"] opaque Child.kill {cfg : @& StdioConfig} : @& Child cfg → IO Unit

src/Lean/Data/SMap.lean

@@ -87,6 +87,11 @@ def switch (m : SMap α β) : SMap α β :=
 @[inline] def foldStage2 {σ : Type w} (f : σ → α → β → σ) (s : σ) (m : SMap α β) : σ :=
   m.map₂.foldl f s
 
+/-- Monadic fold over a staged map. -/
+def foldM {m : Type w → Type w} [Monad m]
+    (f : σ → α → β → m σ) (init : σ) (map : SMap α β) : m σ := do
+  map.map₂.foldlM f (← map.map₁.foldM f init)
+
 def fold {σ : Type w} (f : σ → α → β → σ) (init : σ) (m : SMap α β) : σ :=
   m.map₂.foldl f $ m.map₁.fold f init
 

src/Lean/Declaration.lean

@@ -239,6 +239,10 @@ structure InductiveVal extends ConstantVal where
   all : List Name
   /-- List of the names of the constructors for this inductive datatype. -/
   ctors : List Name
+  /-- Number of auxillary data types produced from nested occurrences.
+  An inductive definition `T` is nested when there is a constructor with an argument `x : F T`,
+   where `F : Type → Type` is some suitably behaved (ie strictly positive) function (Eg `Array T`, `List T`, `T × T`, ...).  -/
+  numNested : Nat
   /-- `true` when recursive (that is, the inductive type appears as an argument in a constructor). -/
   isRec : Bool
   /-- Whether the definition is flagged as unsafe. -/
@@ -257,14 +261,12 @@ structure InductiveVal extends ConstantVal where
   Section 2.2, Definition 3
   -/
   isReflexive : Bool
-  /-- An inductive definition `T` is nested when there is a constructor with an argument `x : F T`,
-   where `F : Type → Type` is some suitably behaved (ie strictly positive) function (Eg `Array T`, `List T`, `T × T`, ...). -/
-  isNested : Bool
+
   deriving Inhabited
 
 @[export lean_mk_inductive_val]
 def mkInductiveValEx (name : Name) (levelParams : List Name) (type : Expr) (numParams numIndices : Nat)
-    (all ctors : List Name) (isRec isUnsafe isReflexive isNested : Bool) : InductiveVal := {
+    (all ctors : List Name) (numNested : Nat) (isRec isUnsafe isReflexive : Bool) : InductiveVal := {
   name := name
   levelParams := levelParams
   type := type
@@ -272,18 +274,18 @@ def mkInductiveValEx (name : Name) (levelParams : List Name) (type : Expr) (numP
   numIndices := numIndices
   all := all
   ctors := ctors
+  numNested := numNested
   isRec := isRec
   isUnsafe := isUnsafe
   isReflexive := isReflexive
-  isNested := isNested
 }
 
 @[export lean_inductive_val_is_rec] def InductiveVal.isRecEx (v : InductiveVal) : Bool := v.isRec
 @[export lean_inductive_val_is_unsafe] def InductiveVal.isUnsafeEx (v : InductiveVal) : Bool := v.isUnsafe
 @[export lean_inductive_val_is_reflexive] def InductiveVal.isReflexiveEx (v : InductiveVal) : Bool := v.isReflexive
-@[export lean_inductive_val_is_nested] def InductiveVal.isNestedEx (v : InductiveVal) : Bool := v.isNested
 
 def InductiveVal.numCtors (v : InductiveVal) : Nat := v.ctors.length
+def InductiveVal.isNested (v : InductiveVal) : Bool := v.numNested > 0
 
 structure ConstructorVal extends ConstantVal where
   /-- Inductive type this constructor is a member of -/

src/Lean/Elab/MutualDef.lean

@@ -168,13 +168,8 @@ private def elabHeaders (views : Array DefView)
           reuseBody := false
 
       let mut (newHeader, newState) ← withRestoreOrSaveFull reusableResult? none do
-        withRef view.headerRef do
-        addDeclarationRanges declName view.ref  -- NOTE: this should be the full `ref`
+        withReuseContext view.headerRef do
         applyAttributesAt declName view.modifiers.attrs .beforeElaboration
-        -- do not hide header errors on partial body syntax as these two elaboration parts are
-        -- sufficiently independent
-        withTheReader Core.Context ({ · with suppressElabErrors :=
-          view.headerRef.hasMissing && !Command.showPartialSyntaxErrors.get (← getOptions) }) do
         withDeclName declName <| withAutoBoundImplicit <| withLevelNames levelNames <|
           elabBindersEx view.binders.getArgs fun xs => do
             let refForElabFunType := view.value
@@ -340,6 +335,7 @@ private def elabFunValues (headers : Array DefViewElabHeader) : TermElabM (Array
           reusableResult? := some (old.value, old.state)
 
     let (val, state) ← withRestoreOrSaveFull reusableResult? header.tacSnap? do
+      withReuseContext header.value do
       withDeclName header.declName <| withLevelNames header.levelNames do
       let valStx ← liftMacroM <| declValToTerm header.value
       forallBoundedTelescope header.type header.numParams fun xs type => do
@@ -933,6 +929,11 @@ where
           checkForHiddenUnivLevels allUserLevelNames preDefs
           addPreDefinitions preDefs
           processDeriving headers
+      for view in views, header in headers do
+        -- NOTE: this should be the full `ref`, and thus needs to be done after any snapshotting
+        -- that depends only on a part of the ref
+        addDeclarationRanges header.declName view.ref
+
 
   processDeriving (headers : Array DefViewElabHeader) := do
     for header in headers, view in views do

src/Lean/Elab/PreDefinition/Basic.lean

@@ -183,16 +183,31 @@ def addAndCompilePartialRec (preDefs : Array PreDefinition) : TermElabM Unit :=
             | _ => none
           modifiers := {} }
 
-private def containsRecFn (recFnName : Name) (e : Expr) : Bool :=
-  (e.find? fun e => e.isConstOf recFnName).isSome
+private def containsRecFn (recFnNames : Array Name) (e : Expr) : Bool :=
+  (e.find? fun e => e.isConst && recFnNames.contains e.constName!).isSome
 
-def ensureNoRecFn (recFnName : Name) (e : Expr) : MetaM Expr := do
-  if containsRecFn recFnName e then
+def ensureNoRecFn (recFnNames : Array Name) (e : Expr) : MetaM Unit := do
+  if containsRecFn recFnNames e then
     Meta.forEachExpr e fun e => do
-      if e.isAppOf recFnName then
+      if e.getAppFn.isConst && recFnNames.contains e.getAppFn.constName! then
         throwError "unexpected occurrence of recursive application{indentExpr e}"
-    pure e
-  else
-    pure e
+
+/--
+Checks that all codomains have the same level, throws an error otherwise.
+-/
+def checkCodomainsLevel (preDefs : Array PreDefinition) : MetaM Unit := do
+  if preDefs.size = 1 then return
+  let arities ← preDefs.mapM fun preDef =>
+    lambdaTelescope preDef.value fun xs _ => return xs.size
+  forallBoundedTelescope preDefs[0]!.type arities[0]!  fun _ type₀ => do
+    let u₀ ← getLevel type₀
+    for i in [1:preDefs.size] do
+      forallBoundedTelescope preDefs[i]!.type arities[i]! fun _ typeᵢ =>
+      unless ← isLevelDefEq u₀ (← getLevel typeᵢ) do
+        withOptions (fun o => pp.sanitizeNames.set o false) do
+          throwError m!"invalid mutual definition, result types must be in the same universe " ++
+            m!"level, resulting type " ++
+            m!"for `{preDefs[0]!.declName}` is{indentExpr type₀} : {← inferType type₀}\n" ++
+            m!"and for `{preDefs[i]!.declName}` is{indentExpr typeᵢ} : {← inferType typeᵢ}"
 
 end Lean.Elab

src/Lean/Elab/PreDefinition/Main.lean

@@ -186,6 +186,7 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
     else
       ensureFunIndReservedNamesAvailable preDefs
       try
+        checkCodomainsLevel preDefs
         checkTerminationByHints preDefs
         let termArgs ← elabTerminationByHints preDefs
         if shouldUseStructural preDefs then

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

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
+Authors: Leonardo de Moura, Joachim Breitner
 -/
 prelude
 import Lean.Util.HasConstCache
@@ -9,6 +9,7 @@ import Lean.Meta.Match.MatcherApp.Transform
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Structural.Basic
+import Lean.Elab.PreDefinition.Structural.FunPacker
 
 namespace Lean.Elab.Structural
 open Meta
@@ -41,23 +42,43 @@ private partial def toBelowAux (C : Expr) (belowDict : Expr) (arg : Expr) (F : E
       unless belowDictFun.getAppFn == C do throwToBelowFailed
       unless ← isDefEq belowDictArg arg do throwToBelowFailed
       pure (mkAppN F argTailArgs)
-    | _ => throwToBelowFailed
+    | _ =>
+      trace[Elab.definition.structural] "belowDict not an app: {belowDict}"
+      throwToBelowFailed
 
 /-- See `toBelow` -/
-private def withBelowDict (below : Expr) (numIndParams : Nat) (k : Expr → Expr → MetaM α) : MetaM α := do
+private def withBelowDict [Inhabited α] (below : Expr) (numIndParams : Nat)
+    (positions : Positions) (k : Array Expr → Expr → MetaM α) : MetaM α := do
+  let numIndAll := positions.size
   let belowType ← inferType below
   trace[Elab.definition.structural] "belowType: {belowType}"
+  unless (← isTypeCorrect below) do
+    trace[Elab.definition.structural] "not type correct!"
   belowType.withApp fun f args => do
-    let motivePos := numIndParams + 1
-    unless motivePos < args.size do throwError "unexpected 'below' type{indentExpr belowType}"
-    let pre := mkAppN f (args.extract 0 numIndParams)
-    let preType ← inferType pre
-    forallBoundedTelescope preType (some 1) fun x _ => do
-      let motiveType ← inferType x[0]!
-      withLocalDeclD (← mkFreshUserName `C) motiveType fun C =>
-        let belowDict := mkApp pre C
-        let belowDict := mkAppN belowDict (args.extract (numIndParams + 1) args.size)
-        k C belowDict
+    unless numIndParams + numIndAll < args.size do
+      trace[Elab.definition.structural] "unexpected 'below' type{indentExpr belowType}"
+      throwToBelowFailed
+    let params := args[:numIndParams]
+    let finalArgs := args[numIndParams+numIndAll:]
+    let pre := mkAppN f params
+    let motiveTypes ← inferArgumentTypesN numIndAll pre
+    let numMotives : Nat := positions.numIndices
+    trace[Elab.definition.structural] "numMotives: {numMotives}"
+    let mut CTypes := Array.mkArray numMotives (.sort 37) -- dummy value
+    for poss in positions, motiveType in motiveTypes do
+      for pos in poss do
+        CTypes := CTypes.set! pos motiveType
+    let CDecls : Array (Name × (Array Expr → MetaM Expr)) ← CTypes.mapM fun t => do
+        return ((← mkFreshUserName `C), fun _ => pure t)
+    withLocalDeclsD CDecls fun Cs => do
+      -- We have to pack these canary motives like we packed the real motives
+      let packedCs ← positions.mapMwith packMotives motiveTypes Cs
+      let belowDict := mkAppN pre packedCs
+      let belowDict := mkAppN belowDict finalArgs
+      trace[Elab.definition.structural] "initial belowDict for {Cs}:{indentExpr belowDict}"
+      unless (← isTypeCorrect belowDict) do
+        trace[Elab.definition.structural] "not type correct!"
+      k Cs belowDict
 
 /--
   `below` is a free variable with type of the form `I.below indParams motive indices major`,
@@ -79,14 +100,16 @@ private def withBelowDict (below : Expr) (numIndParams : Nat) (k : Expr → Expr
   We search this dictionary using the auxiliary function `toBelowAux`.
   The dictionary is built using the `PProd` (`And` for inductive predicates).
   We keep searching it until we find `C recArg`, where `C` is the auxiliary fresh variable created at `withBelowDict`.  -/
-private partial def toBelow (below : Expr) (numIndParams : Nat) (recArg : Expr) : MetaM Expr := do
-  withBelowDict below numIndParams fun C belowDict =>
-    toBelowAux C belowDict recArg below
+private partial def toBelow (below : Expr) (numIndParams : Nat) (positions : Positions) (fnIndex : Nat) (recArg : Expr) : MetaM Expr := do
+  withBelowDict below numIndParams positions fun Cs belowDict =>
+    toBelowAux Cs[fnIndex]! belowDict recArg below
 
-private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo) (below : Expr) (e : Expr) : M Expr :=
-  let containsRecFn (e : Expr) : StateRefT (HasConstCache recFnName) M Bool :=
+private partial def replaceRecApps (recArgInfos : Array RecArgInfo) (positions : Positions)
+    (below : Expr) (e : Expr) : M Expr :=
+  let recFnNames := recArgInfos.map (·.fnName)
+  let containsRecFn (e : Expr) : StateRefT (HasConstCache recFnNames) M Bool :=
     modifyGet (·.contains e)
-  let rec loop (below : Expr) (e : Expr) : StateRefT (HasConstCache recFnName) M Expr := do
+  let rec loop (below : Expr) (e : Expr) : StateRefT (HasConstCache recFnNames) M Expr := do
     if !(← containsRecFn e) then
       return e
     match e with
@@ -106,32 +129,36 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo)
         return mkMData d (← loop below b)
     | Expr.proj n i e => return mkProj n i (← loop below e)
     | Expr.app _ _ =>
-      let processApp (e : Expr) : StateRefT (HasConstCache recFnName) M Expr :=
+      let processApp (e : Expr) : StateRefT (HasConstCache recFnNames) M Expr :=
         e.withApp fun f args => do
-          if f.isConstOf recFnName then
-            let numFixed  := recArgInfo.fixedParams.size
-            let recArgPos := recArgInfo.fixedParams.size + recArgInfo.pos
+          if let .some fnIdx := recArgInfos.findIdx? (f.isConstOf ·.fnName) then
+            let recArgInfo := recArgInfos[fnIdx]!
+            let numFixed  := recArgInfo.numFixed
+            let recArgPos := recArgInfo.recArgPos
             if recArgPos >= args.size then
               throwError "insufficient number of parameters at recursive application {indentExpr e}"
             let recArg := args[recArgPos]!
             -- For reflexive type, we may have nested recursive applications in recArg
             let recArg ← loop below recArg
-            let f ← try toBelow below recArgInfo.indParams.size recArg catch  _ => throwError "failed to eliminate recursive application{indentExpr e}"
+            let f ←
+              try toBelow below recArgInfo.indParams.size positions fnIdx recArg
+              catch _ => throwError "failed to eliminate recursive application{indentExpr e}"
             -- Recall that the fixed parameters are not in the scope of the `brecOn`. So, we skip them.
             let argsNonFixed := args.extract numFixed args.size
             -- The function `f` does not explicitly take `recArg` and its indices as arguments. So, we skip them too.
             let mut fArgs := #[]
             for i in [:argsNonFixed.size] do
-              if recArgInfo.pos != i && !recArgInfo.indicesPos.contains i then
+              let j := i + numFixed
+              if recArgInfo.recArgPos != j && !recArgInfo.indicesPos.contains j then
                 let arg := argsNonFixed[i]!
-                let arg ← replaceRecApps recFnName recArgInfo below arg
+                let arg ← replaceRecApps recArgInfos positions below arg
                 fArgs := fArgs.push arg
             return mkAppN f fArgs
           else
             return mkAppN (← loop below f) (← args.mapM (loop below))
       match (← matchMatcherApp? (alsoCasesOn := true) e) with
       | some matcherApp =>
-        if !recArgHasLooseBVarsAt recFnName recArgInfo.recArgPos e then
+        if recArgInfos.all (fun recArgInfo => !recArgHasLooseBVarsAt recArgInfo.fnName recArgInfo.recArgPos e) then
           processApp e
         else
           /- Here is an example we currently do not handle
@@ -163,49 +190,114 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo)
           else
             processApp e
       | none => processApp e
-    | e => ensureNoRecFn recFnName e
+    | e =>
+      ensureNoRecFn recFnNames e
+      pure e
   loop below e |>.run' {}
 
-def mkBRecOn (recFnName : Name) (recArgInfo : RecArgInfo) (value : Expr) : M Expr := do
-  trace[Elab.definition.structural] "mkBRecOn: {value}"
-  let type  := (← inferType value).headBeta
-  let major := recArgInfo.ys[recArgInfo.pos]!
-  let otherArgs := recArgInfo.ys.filter fun y => y != major && !recArgInfo.indIndices.contains y
-  trace[Elab.definition.structural] "fixedParams: {recArgInfo.fixedParams}, otherArgs: {otherArgs}"
-  let motive ← mkForallFVars otherArgs type
-  let mut brecOnUniv ← getLevel motive
-  trace[Elab.definition.structural] "brecOn univ: {brecOnUniv}"
-  let useBInductionOn := recArgInfo.reflexive && brecOnUniv == levelZero
-  if recArgInfo.reflexive && brecOnUniv != levelZero then
-    brecOnUniv ← decLevel brecOnUniv
-  let motive ← mkLambdaFVars (recArgInfo.indIndices.push major) motive
-  trace[Elab.definition.structural] "brecOn motive: {motive}"
-  let brecOn :=
-    if useBInductionOn then
-      Lean.mkConst (mkBInductionOnName recArgInfo.indName) recArgInfo.indLevels
-    else
-      Lean.mkConst (mkBRecOnName recArgInfo.indName) (brecOnUniv :: recArgInfo.indLevels)
-  let brecOn := mkAppN brecOn recArgInfo.indParams
-  let brecOn := mkApp brecOn motive
-  let brecOn := mkAppN brecOn recArgInfo.indIndices
-  let brecOn := mkApp brecOn major
-  check brecOn
-  let brecOnType ← inferType brecOn
-  trace[Elab.definition.structural] "brecOn     {brecOn}"
-  trace[Elab.definition.structural] "brecOnType {brecOnType}"
-  forallBoundedTelescope brecOnType (some 1) fun F _ => do
-    let F := F[0]!
-    let FType ← inferType F
-    trace[Elab.definition.structural] "FType: {FType}"
-    let FType ← instantiateForall FType recArgInfo.indIndices
-    let FType ← instantiateForall FType #[major]
+/--
+Calculates the `.brecOn` motive corresponding to one structural recursive function.
+The `value` is the function with (only) the fixed parameters moved into the context.
+-/
+def mkBRecOnMotive (recArgInfo : RecArgInfo) (value : Expr) : M Expr := do
+  lambdaTelescope value fun xs value => do
+    let type  := (← inferType value).headBeta
+    let (indexMajorArgs, otherArgs) := recArgInfo.pickIndicesMajor xs
+    let motive ← mkForallFVars otherArgs type
+    mkLambdaFVars indexMajorArgs motive
+
+/--
+Calculates the `.brecOn` functional argument corresponding to one structural recursive function.
+The `value` is the function with (only) the fixed parameters moved into the context,
+The `type` is the expected type of the argument.
+The `recArgInfos` is used to transform the body of the function to replace recursive calls with
+uses of the `below` induction hypothesis.
+-/
+def mkBRecOnF (recArgInfos : Array RecArgInfo) (positions : Positions)
+    (recArgInfo : RecArgInfo) (value : Expr) (FType : Expr) : M Expr := do
+  lambdaTelescope value fun xs value => do
+    let (indexMajorArgs, otherArgs) := recArgInfo.pickIndicesMajor xs
+    let FType ← instantiateForall FType indexMajorArgs
     forallBoundedTelescope FType (some 1) fun below _ => do
       -- TODO: `below` user name is `f`, and it will make a global `f` to be pretty printed as `_root_.f` in error messages.
       -- We should add an option to `forallBoundedTelescope` to ensure fresh names are used.
       let below := below[0]!
-      let valueNew     ← replaceRecApps recFnName recArgInfo below value
-      let Farg         ← mkLambdaFVars (recArgInfo.indIndices ++ #[major, below] ++ otherArgs) valueNew
-      let brecOn       := mkApp brecOn Farg
-      return mkAppN brecOn otherArgs
+      let valueNew   ← replaceRecApps recArgInfos positions below value
+      mkLambdaFVars (indexMajorArgs ++ #[below] ++ otherArgs) valueNew
+
+
+/--
+Given the `motives`, figures out whether to use `.brecOn` or `.binductionOn`, pass
+the right universe levels, the parameters, and the motives.
+It was already checked earlier in `checkCodomainsLevel` that the functions live in the same universe.
+-/
+def mkBRecOnConst (recArgInfos : Array RecArgInfo) (positions : Positions)
+   (motives : Array Expr) : MetaM (Name → Expr) := do
+  -- For now, just look at the first
+  let recArgInfo := recArgInfos[0]!
+  let motive := motives[0]!
+  let brecOnUniv ← lambdaTelescope motive fun _ type => getLevel type
+  let indInfo ← getConstInfoInduct recArgInfo.indName
+  let useBInductionOn := indInfo.isReflexive && brecOnUniv == levelZero
+  let brecOnUniv ←
+    if indInfo.isReflexive && brecOnUniv != levelZero then
+      decLevel brecOnUniv
+    else
+      pure brecOnUniv
+  let brecOnCons := fun n =>
+    let brecOn :=
+      if useBInductionOn then .const (mkBInductionOnName n) recArgInfo.indLevels
+      else                    .const (mkBRecOnName n) (brecOnUniv :: recArgInfo.indLevels)
+    mkAppN brecOn recArgInfo.indParams
+
+  -- Pick one as a prototype
+  let brecOnAux := brecOnCons recArgInfo.indName
+  -- Infer the type of the packed motive arguments
+  let packedMotiveTypes ← inferArgumentTypesN recArgInfo.indAll.size brecOnAux
+  let packedMotives ← positions.mapMwith packMotives packedMotiveTypes motives
+
+  return fun n => mkAppN (brecOnCons n) packedMotives
+
+/--
+Given the `recArgInfos` and the `motives`, infer the types of the `F` arguments to the `.brecOn`
+combinators. This assumes that all `.brecOn` functions of a mutual inductive have the same structure.
+
+It also undoes the permutation and packing done by `packMotives`
+-/
+def inferBRecOnFTypes (recArgInfos : Array RecArgInfo) (positions : Positions)
+    (brecOnConst : Name → Expr) : MetaM (Array Expr) := do
+  let recArgInfo := recArgInfos[0]! -- pick an arbitrary one
+  let brecOn := brecOnConst recArgInfo.indName
+  check brecOn
+  let brecOnType ← inferType brecOn
+  -- Skip the indices and major argument
+  let packedFTypes ← forallBoundedTelescope brecOnType (some (recArgInfo.indicesPos.size + 1)) fun _ brecOnType =>
+    -- And return the types of of the next arguments
+    arrowDomainsN recArgInfo.indAll.size brecOnType
+
+  let mut FTypes := Array.mkArray recArgInfos.size (Expr.sort 0)
+  for packedFType in packedFTypes, poss in positions do
+    for pos in poss do
+      FTypes := FTypes.set! pos packedFType
+  return FTypes
+
+/--
+Completes the `.brecOn` for the given function.
+The `value` is the function with (only) the fixed parameters moved into the context.
+-/
+def mkBrecOnApp (positions : Positions) (fnIdx : Nat) (brecOnConst : Name → Expr)
+    (FArgs : Array Expr) (recArgInfo : RecArgInfo) (value : Expr) : MetaM Expr := do
+  lambdaTelescope value fun ys _value => do
+    let (indexMajorArgs, otherArgs) := recArgInfo.pickIndicesMajor ys
+    let brecOn := brecOnConst recArgInfo.indName
+    let brecOn := mkAppN brecOn indexMajorArgs
+    let packedFTypes ← inferArgumentTypesN positions.size brecOn
+    let packedFArgs ← positions.mapMwith packFArgs packedFTypes FArgs
+    let brecOn := mkAppN brecOn packedFArgs
+    let some poss := positions.find? (·.contains fnIdx)
+      | throwError "mkBrecOnApp: Could not find {fnIdx} in {positions}"
+    let brecOn ← if poss.size = 1 then pure brecOn else
+      mkPProdProjN (poss.getIdx? fnIdx).get! brecOn
+    mkLambdaFVars ys (mkAppN brecOn otherArgs)
 
 end Lean.Elab.Structural

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

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
+Authors: Leonardo de Moura, Joachim Breitner
 -/
 prelude
 import Lean.Meta.Basic
@@ -9,14 +9,21 @@ import Lean.Meta.ForEachExpr
 
 namespace Lean.Elab.Structural
 
+/--
+Information about the argument of interest of a structurally recursive function.
+
+The `Expr`s in this data structure expect the `fixedParams` to be in scope, but not the other
+parameters of the function. This ensures that this data structure makes sense in the other functions
+of a mutually recursive group.
+-/
 structure RecArgInfo where
-  /-- `fixedParams ++ ys` are the arguments of the function we are trying to justify termination using structural recursion. -/
-  fixedParams : Array Expr
-  /-- recursion arguments -/
-  ys          : Array Expr
-  /-- position in `ys` of the argument we are recursing on -/
-  pos         : Nat
-  /-- position in `ys` of the inductive datatype indices we are recursing on -/
+  /-- the name of the recursive function -/
+  fnName      : Name
+  /-- the fixed prefix of arguments of the function we are trying to justify termination using structural recursion. -/
+  numFixed    : Nat
+  /-- position of the argument (counted including fixed prefix) we are recursing on -/
+  recArgPos   : Nat
+  /-- position of the indices (counted including fixed prefix) of the inductive datatype indices we are recursing on -/
   indicesPos  : Array Nat
   /-- inductive datatype name of the argument we are recursing on -/
   indName     : Name
@@ -24,15 +31,23 @@ structure RecArgInfo where
   indLevels   : List Level
   /-- inductive datatype parameters of the argument we are recursing on -/
   indParams   : Array Expr
-  /-- inductive datatype indices of the argument we are recursing on, it is equal to `indicesPos.map fun i => ys.get! i` -/
-  indIndices  : Array Expr
-  /-- true if we are recursing over a reflexive inductive datatype -/
-  reflexive   : Bool
-  /-- true if the type is an inductive predicate -/
-  indPred     : Bool
-
-def RecArgInfo.recArgPos (info : RecArgInfo) : Nat :=
-  info.fixedParams.size + info.pos
+  /-- The types mutually inductive with indName -/
+  indAll      : Array Name
+deriving Inhabited
+/--
+If `xs` are the parameters of the functions (excluding fixed prefix), partitions them
+into indices and major arguments, and other parameters.
+-/
+def RecArgInfo.pickIndicesMajor (info : RecArgInfo) (xs : Array Expr) : (Array Expr × Array Expr) := Id.run do
+  let mut indexMajorArgs := #[]
+  let mut otherArgs := #[]
+  for h : i in [:xs.size] do
+    let j := i + info.numFixed
+    if j = info.recArgPos || info.indicesPos.contains j then
+      indexMajorArgs := indexMajorArgs.push xs[i]
+    else
+      otherArgs := otherArgs.push xs[i]
+  return (indexMajorArgs, otherArgs)
 
 structure State where
   /-- As part of the inductive predicates case, we keep adding more and more discriminants from the
@@ -64,4 +79,51 @@ def recArgHasLooseBVarsAt (recFnName : Name) (recArgPos : Nat) (e : Expr) : Bool
      e.isAppOf recFnName && e.getAppNumArgs > recArgPos && (e.getArg! recArgPos).hasLooseBVars
   app?.isSome
 
+
+/--
+Lets say we have `n` mutually recursive functions whose recursive arguments are from a group
+of `m` mutually inductive data types. This mapping does not have to be one-to-one: for one type
+there can be zero, one or more functions. We use the logic in the `FunPacker` modules to combine
+the bodies (and motives) of multiple such functions.
+
+Therefore we have to take the `n` functions, group them by their recursive argument's type,
+and for each such type, keep track of the order of the functions.
+
+We represent these positions as an `Array (Array Nat)`. We have that
+
+* `positions.size = indInfo.all.length`
+* `positions.flatten` is a permutation of `[0:n]`, so each of the `n` functions has exactly one
+  position, and each position refers to one of the `n` functions.
+* if `k ∈ positions[i]` then the recursive argument of function `k` is has type `indInfo.all[i]`
+
+-/
+abbrev Positions := Array (Array Nat)
+
+/--
+The number of indices in the array.
+-/
+def Positions.numIndices (positions : Positions) : Nat :=
+    positions.foldl (fun s poss => s + poss.size) 0
+
+/--
+Groups the `xs` by their `f` value, and puts these groups into the order given by `ys`.
+-/
+def Positions.groupAndSort {α β} [Inhabited α] [DecidableEq β]
+    (f : α → β) (xs : Array α) (ys : Array β) : Positions :=
+  let positions := ys.map fun y => (Array.range xs.size).filter fun i => f xs[i]! = y
+  -- Sanity check: is this really a grouped permutation of all the indices?
+  assert! Array.range xs.size == positions.flatten.qsort Nat.blt
+  positions
+
+/--
+Let `positions.size = ys.size` and `positions.numIndices = xs.size`. Maps `f` over each `y` in `ys`,
+also passing in those elements `xs` that belong to that are those elements of `xs` that belong to
+`y` according to `positions`.
+-/
+def Positions.mapMwith {α β m} [Monad m] [Inhabited β] (f : α → Array β → m γ)
+    (positions : Positions) (ys : Array α) (xs : Array β) : m (Array γ) := do
+  assert! positions.size = ys.size
+  assert! positions.numIndices = xs.size
+  (Array.zip ys positions).mapM fun ⟨y, poss⟩ => f y (poss.map (xs[·]!))
+
 end Lean.Elab.Structural

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

@@ -63,12 +63,12 @@ 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 (tryRefl := true) #[info.declName] goal.mvarId!
+    mkEqnTypes (tryRefl := true) info.declNames goal.mvarId!
   let baseName := info.declName
   let mut thmNames := #[]
   for i in [: eqnTypes.size] do
     let type := eqnTypes[i]!
-    trace[Elab.definition.structural.eqns] "{eqnTypes[i]!}"
+    trace[Elab.definition.structural.eqns] "eqnType {i}: {type}"
     let name := (Name.str baseName eqnThmSuffixBase).appendIndexAfter (i+1)
     thmNames := thmNames.push name
     let value ← mkProof info.declName type

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

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
+Authors: Leonardo de Moura, Joachim Breitner
 -/
 prelude
 import Lean.Elab.PreDefinition.Structural.Basic
@@ -29,20 +29,16 @@ private def hasBadIndexDep? (ys : Array Expr) (indices : Array Expr) : MetaM (Op
 -- Inductive datatype parameters cannot depend on ys
 private def hasBadParamDep? (ys : Array Expr) (indParams : Array Expr) : MetaM (Option (Expr × Expr)) := do
   for p in indParams do
-    let pType ← inferType p
     for y in ys do
-      if ← dependsOn pType y.fvarId! then
+      if ← dependsOn p y.fvarId! then
         return some (p, y)
   return none
 
 /--
-Pass to `k` the `RecArgInfo` for the `i`th parameter in the parameter list `xs`. This performs
+Assemble the `RecArgInfo` for the `i`th parameter in the parameter list `xs`. This performs
 various sanity checks on the argument (is it even an inductive type etc).
-Also wraps all errors in a common “argument cannot be used” header
 -/
-def withRecArgInfo (numFixed : Nat) (xs : Array Expr) (i : Nat) (k : RecArgInfo → M α) : M α := do
-  mapError
-    (f := fun msg => m!"argument #{i+1} cannot be used for structural recursion{indentD msg}") do
+def getRecArgInfo (fnName : Name) (numFixed : Nat) (xs : Array Expr) (i : Nat) : MetaM RecArgInfo := do
   if h : i < xs.size then
     if i < numFixed then
       throwError "it is unchanged in the recursive calls"
@@ -53,76 +49,79 @@ def withRecArgInfo (numFixed : Nat) (xs : Array Expr) (i : Nat) (k : RecArgInfo
     let xType ← whnfD localDecl.type
     matchConstInduct xType.getAppFn (fun _ => throwError "its type is not an inductive") fun indInfo us => do
     if !(← hasConst (mkBRecOnName indInfo.name)) then
-      throwError "its type does not have a recursor"
+      throwError "its type {indInfo.name} does not have a recursor"
     else if indInfo.isReflexive && !(← hasConst (mkBInductionOnName indInfo.name)) && !(← isInductivePredicate indInfo.name) then
-      throwError "its type is a reflexive inductive, but {mkBInductionOnName indInfo.name} does not exist and it is not an inductive predicate"
+      throwError "its type {indInfo.name} is a reflexive inductive, but {mkBInductionOnName indInfo.name} does not exist and it is not an inductive predicate"
     else
-      let indArgs    := xType.getAppArgs
-      let indParams  := indArgs.extract 0 indInfo.numParams
-      let indIndices := indArgs.extract indInfo.numParams indArgs.size
+      let indArgs    : Array Expr := xType.getAppArgs
+      let indParams  : Array Expr := indArgs[0:indInfo.numParams]
+      let indIndices : Array Expr := indArgs[indInfo.numParams:]
       if !indIndices.all Expr.isFVar then
-        throwError "its type is an inductive family and indices are not variables{indentExpr xType}"
+        throwError "its type {indInfo.name} is an inductive family and indices are not variables{indentExpr xType}"
       else if !indIndices.allDiff then
-        throwError " its type is an inductive family and indices are not pairwise distinct{indentExpr xType}"
+        throwError " its type {indInfo.name} is an inductive family and indices are not pairwise distinct{indentExpr xType}"
       else
         let indexMinPos := getIndexMinPos xs indIndices
         let numFixed    := if indexMinPos < numFixed then indexMinPos else numFixed
-        let fixedParams := xs.extract 0 numFixed
-        let ys          := xs.extract numFixed xs.size
+        let ys          := xs[numFixed:]
         match (← hasBadIndexDep? ys indIndices) with
         | some (index, y) =>
-          throwError "its type is an inductive family{indentExpr xType}\nand index{indentExpr index}\ndepends on the non index{indentExpr y}"
+          throwError "its type {indInfo.name} is an inductive family{indentExpr xType}\nand index{indentExpr index}\ndepends on the non index{indentExpr y}"
         | none =>
           match (← hasBadParamDep? ys indParams) with
           | some (indParam, y) =>
-            throwError "its type is an inductive datatype{indentExpr xType}\nand parameter{indentExpr indParam}\ndepends on{indentExpr y}"
+            throwError "its type is an inductive datatype{indentExpr xType}\nand the datatype parameter{indentExpr indParam}\ndepends on the function parameter{indentExpr y}\nwhich does not come before the varying parameters and before the indices of the recursion parameter."
           | none =>
-            let indicesPos := indIndices.map fun index => match ys.indexOf? index with | some i => i.val | none => unreachable!
-            k { fixedParams := fixedParams
-                ys          := ys
-                pos         := i - fixedParams.size
-                indicesPos  := indicesPos
-                indName     := indInfo.name
-                indLevels   := us
-                indParams   := indParams
-                indIndices  := indIndices
-                reflexive   := indInfo.isReflexive
-                indPred     := ←isInductivePredicate indInfo.name }
+            let indicesPos := indIndices.map fun index => match xs.indexOf? index with | some i => i.val | none => unreachable!
+            return { fnName      := fnName
+                     numFixed    := numFixed
+                     recArgPos   := i
+                     indicesPos  := indicesPos
+                     indName     := indInfo.name
+                     indLevels   := us
+                     indParams   := indParams
+                     indAll      := indInfo.all.toArray }
     else
       throwError "the index #{i+1} exceeds {xs.size}, the number of parameters"
 
 /--
-  Try to find an argument that is structurally smaller in every recursive application.
+  Runs `k` on all argument indices, until it succeeds.
   We use this argument to justify termination using the auxiliary `brecOn` construction.
 
   We give preference for arguments that are *not* indices of inductive types of other arguments.
   See issue #837 for an example where we can show termination using the index of an inductive family, but
   we don't get the desired definitional equalities.
+
+  `value` is the function value (including fixed parameters)
 -/
-partial def findRecArg (numFixed : Nat) (xs : Array Expr) (k : RecArgInfo → M α) : M α := do
-  /- Collect arguments that are indices. See comment above. -/
-  let indicesRef : IO.Ref (Array Nat) ← IO.mkRef {}
-  for x in xs do
-    let xType ← inferType x
-    /- Traverse all sub-expressions in the type of `x` -/
-    forEachExpr xType fun e =>
-      /- If `e` is an inductive family, we store in `indicesRef` all variables in `xs` that occur in "index positions". -/
-      matchConstInduct e.getAppFn (fun _ => pure ()) fun info _ => do
-        if info.numIndices > 0 && info.numParams + info.numIndices == e.getAppNumArgs then
-          for arg in e.getAppArgs[info.numParams:] do
-            forEachExpr arg fun e => do
-              if let .some idx := xs.getIdx? e then
-                indicesRef.modify fun indices => indices.push idx
-  let indices ← indicesRef.get
-  let nonIndices := (Array.range xs.size).filter (fun i => !(indices.contains i))
-  let mut errors : Array MessageData := Array.mkArray xs.size m!""
+partial def tryAllArgs (value : Expr) (k : Nat → M α) : M α := do
+  -- It's improtant to keep the call to `k` outside the scope of `lambdaTelescope`:
+  -- The tactics in the IndPred construction search the full local context, so we must not have
+  -- extra FVars there
+  let (indices, nonIndices) ← lambdaTelescope value fun xs _ => do
+    let indicesRef : IO.Ref (Array Nat) ← IO.mkRef {}
+    for x in xs do
+      let xType ← inferType x
+      /- Traverse all sub-expressions in the type of `x` -/
+      forEachExpr xType fun e =>
+        /- If `e` is an inductive family, we store in `indicesRef` all variables in `xs` that occur in "index positions". -/
+        matchConstInduct e.getAppFn (fun _ => pure ()) fun info _ => do
+          if info.numIndices > 0 && info.numParams + info.numIndices == e.getAppNumArgs then
+            for arg in e.getAppArgs[info.numParams:] do
+              forEachExpr arg fun e => do
+                if let .some idx := xs.getIdx? e then
+                  indicesRef.modify (·.push idx)
+    let indices ← indicesRef.get
+    let nonIndices := (Array.range xs.size).filter (fun i => !(indices.contains i))
+    return (indices, nonIndices)
+
+  let mut errors : Array MessageData := Array.mkArray (indices.size  + nonIndices.size) m!""
   let saveState ← get -- backtrack the state for each argument
   for i in id (nonIndices ++ indices) do
-    let x := xs[i]!
-    trace[Elab.definition.structural] "findRecArg x: {x}"
+    trace[Elab.definition.structural] "findRecArg i: {i}"
     try
       set saveState
-      return (← withRecArgInfo numFixed xs i k)
+      return (← k i)
     catch e => errors := errors.set! i e.toMessageData
   throwError
     errors.foldl

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

@@ -0,0 +1,126 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+prelude
+import Lean.Meta.InferType
+
+/-!
+This module contains the logic that packs the motives and FArgs of multiple functions into one,
+to allow structural mutual recursion where the number of functions is not exactly the same
+as the number of inductive data types in the mutual inductive group.
+
+The private helper functions related to `PProd` here should at some point be moved to their own
+module, so that they can be used elsewhere (e.g. `FunInd`), and possibly unified with the similar
+constructions for well-founded recursion (see `ArgsPacker` module).
+-/
+
+namespace Lean.Elab.Structural
+open Meta
+
+private def mkPUnit : Level → Expr
+  | .zero => .const ``True []
+  | lvl   => .const ``PUnit [lvl]
+
+private def mkPProd (e1 e2 : Expr) : MetaM Expr := do
+  let lvl1 ← getLevel e1
+  let lvl2 ← getLevel e2
+  if lvl1 matches .zero && lvl2 matches .zero then
+    return mkApp2 (.const `And []) e1 e2
+  else
+    return mkApp2 (.const ``PProd [lvl1, lvl2]) e1 e2
+
+private def mkNProd (lvl : Level) (es : Array Expr) : MetaM Expr :=
+  es.foldrM (init := mkPUnit lvl) mkPProd
+
+private def mkPUnitMk : Level → Expr
+  | .zero => .const ``True.intro []
+  | lvl   => .const ``PUnit.unit [lvl]
+
+private def mkPProdMk (e1 e2 : Expr) : MetaM Expr := do
+  let t1 ← inferType e1
+  let t2 ← inferType e2
+  let lvl1 ← getLevel t1
+  let lvl2 ← getLevel t2
+  if lvl1 matches .zero && lvl2 matches .zero then
+    return mkApp4 (.const ``And.intro []) t1 t2 e1 e2
+  else
+    return mkApp4 (.const ``PProd.mk [lvl1, lvl2]) t1 t2 e1 e2
+
+private def mkNProdMk (lvl : Level) (es : Array Expr) : MetaM Expr :=
+  es.foldrM (init := mkPUnitMk lvl) mkPProdMk
+
+/-- `PProd.fst` or `And.left` (as projections) -/
+private def mkPProdFst (e : Expr) : MetaM Expr := do
+  let t ← whnf (← inferType e)
+  match_expr t with
+  | PProd _ _ => return .proj ``PProd 0 e
+  | And _ _ =>   return .proj ``And 0 e
+  | _ => throwError "Cannot project .1 out of{indentExpr e}\nof type{indentExpr t}"
+
+/-- `PProd.snd` or `And.right` (as projections) -/
+private def mkPProdSnd (e : Expr) : MetaM Expr := do
+  let t ← whnf (← inferType e)
+  match_expr t with
+  | PProd _ _ => return .proj ``PProd 1 e
+  | And _ _ =>   return .proj ``And 1 e
+  | _ => throwError "Cannot project .2 out of{indentExpr e}\nof type{indentExpr t}"
+
+/-- Given a proof of `P₁ ∧ … ∧ Pᵢ ∧ … ∧ Pₙ ∧ True`, return the proof of `Pᵢ` -/
+def mkPProdProjN (i : Nat) (e : Expr) : MetaM Expr := do
+  let mut value := e
+  for _ in [:i] do
+      value ← mkPProdSnd value
+  value ← mkPProdFst value
+  return value
+
+/--
+Combines motives from different functions that recurse on the same parameter type into a single
+function returning a `PProd` type.
+
+For example
+```
+packMotives (Nat → Sort u) #[(fun (n : Nat) => Nat), (fun (n : Nat) => Fin n -> Fin n )]
+```
+will return
+```
+fun (n : Nat) (PProd Nat (Fin n → Fin n))
+```
+
+It is the identity if `motives.size = 1`.
+
+It returns a dummy motive `(xs : ) → PUnit` or `(xs : … ) → True` if no motive is given.
+(this is the reason we need the expected type in the `motiveType` parameter).
+
+-/
+def packMotives (motiveType : Expr) (motives : Array Expr) : MetaM Expr := do
+  if motives.size = 1 then
+    return motives[0]!
+  trace[Elab.definition.structural] "packing Motives\nexpected: {motiveType}\nmotives: {motives}"
+  forallTelescope motiveType fun xs sort => do
+    unless sort.isSort do
+      throwError "packMotives: Unexpected motiveType {motiveType}"
+    -- NB: Use beta, not instantiateLambda; when constructing the belowDict below
+    -- we pass `C`, a plain FVar, here
+    let motives := motives.map (·.beta xs)
+    let packedMotives ← mkNProd sort.sortLevel! motives
+    mkLambdaFVars xs packedMotives
+
+/--
+Combines the F-args from different functions that recurse on the same parameter type into a single
+function returning a `PProd` value. See `packMotives`
+
+It is the identity if `motives.size = 1`.
+-/
+def packFArgs (FArgType : Expr) (FArgs : Array Expr) : MetaM Expr := do
+  if FArgs.size = 1 then
+    return FArgs[0]!
+  forallTelescope FArgType fun xs body => do
+    let lvl ← getLevel body
+    let FArgs := FArgs.map (·.beta xs)
+    let packedFArgs ← mkNProdMk lvl FArgs
+    mkLambdaFVars xs packedFArgs
+
+
+end Lean.Elab.Structural

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

@@ -11,7 +11,7 @@ import Lean.Elab.PreDefinition.Structural.Basic
 namespace Lean.Elab.Structural
 open Meta
 
-private partial def replaceIndPredRecApps (recFnName : Name) (recArgInfo : RecArgInfo) (motive : Expr) (e : Expr) : M Expr := do
+private partial def replaceIndPredRecApps (recArgInfo : RecArgInfo) (motive : Expr) (e : Expr) : M Expr := do
   let maxDepth := IndPredBelow.maxBackwardChainingDepth.get (← getOptions)
   let rec loop (e : Expr) : M Expr := do
     match e with
@@ -33,7 +33,7 @@ private partial def replaceIndPredRecApps (recFnName : Name) (recArgInfo : RecAr
     | Expr.app _ _ =>
       let processApp (e : Expr) : M Expr := do
         e.withApp fun f args => do
-          if f.isConstOf recFnName then
+          if f.isConstOf recArgInfo.fnName then
             let ty ← inferType e
             let main ← mkFreshExprSyntheticOpaqueMVar ty
             if (← IndPredBelow.backwardsChaining main.mvarId! maxDepth) then
@@ -44,7 +44,7 @@ private partial def replaceIndPredRecApps (recFnName : Name) (recArgInfo : RecAr
             return mkAppN (← loop f) (← args.mapM loop)
       match (← matchMatcherApp? e) with
       | some matcherApp =>
-        if !recArgHasLooseBVarsAt recFnName recArgInfo.recArgPos e then
+        if !recArgHasLooseBVarsAt recArgInfo.fnName recArgInfo.recArgPos e then
           processApp e
         else
           trace[Elab.definition.structural] "matcherApp before adding below transformation:\n{matcherApp.toExpr}"
@@ -63,42 +63,48 @@ private partial def replaceIndPredRecApps (recFnName : Name) (recArgInfo : RecAr
             trace[Elab.definition.structural] "modified matcher:\n{newApp}"
             processApp newApp
       | none => processApp e
-    | e => ensureNoRecFn recFnName e
+    | e =>
+      ensureNoRecFn #[recArgInfo.fnName] e
+      pure e
   loop e
 
-def mkIndPredBRecOn (recFnName : Name) (recArgInfo : RecArgInfo) (value : Expr) : M Expr := do
-  let type  := (← inferType value).headBeta
-  let major := recArgInfo.ys[recArgInfo.pos]!
-  let otherArgs := recArgInfo.ys.filter fun y => y != major && !recArgInfo.indIndices.contains y
-  trace[Elab.definition.structural] "fixedParams: {recArgInfo.fixedParams}, otherArgs: {otherArgs}"
-  let motive ← mkForallFVars otherArgs type
-  let motive ← mkLambdaFVars (recArgInfo.indIndices.push major) motive
-  trace[Elab.definition.structural] "brecOn motive: {motive}"
-  let brecOn := Lean.mkConst (mkBRecOnName recArgInfo.indName) recArgInfo.indLevels
-  let brecOn := mkAppN brecOn recArgInfo.indParams
-  let brecOn := mkApp brecOn motive
-  let brecOn := mkAppN brecOn recArgInfo.indIndices
-  let brecOn := mkApp brecOn major
-  check brecOn
-  let brecOnType ← inferType brecOn
-  trace[Elab.definition.structural] "brecOn     {brecOn}"
-  trace[Elab.definition.structural] "brecOnType {brecOnType}"
-  -- we need to close the telescope here, because the local context is used:
-  -- The root cause was, that this copied code puts an ih : FType into the
-  -- local context and later, when we use the local context to build the recursive
-  -- call, it uses this ih. But that ih doesn't exist in the actual brecOn call.
-  -- That's why it must go.
-  let FType ← forallBoundedTelescope brecOnType (some 1) fun F _ => do
-    let F := F[0]!
-    let FType ← inferType F
-    trace[Elab.definition.structural] "FType: {FType}"
-    let FType ← instantiateForall FType recArgInfo.indIndices
-    instantiateForall FType #[major]
-  forallBoundedTelescope FType (some 1) fun below _ => do
-    let below := below[0]!
-    let valueNew     ← replaceIndPredRecApps recFnName recArgInfo motive value
-    let Farg         ← mkLambdaFVars (recArgInfo.indIndices ++ #[major, below] ++ otherArgs) valueNew
-    let brecOn       := mkApp brecOn Farg
-    return mkAppN brecOn otherArgs
+/--
+Transform the body of a recursive function into a non-recursive one.
+
+The `value` is the function with (only) the fixed parameters instantiated.
+-/
+def mkIndPredBRecOn (recArgInfo : RecArgInfo) (value : Expr) : M Expr := do
+  lambdaTelescope value fun ys value => do
+    let type  := (← inferType value).headBeta
+    let (indexMajorArgs, otherArgs) := recArgInfo.pickIndicesMajor ys
+    trace[Elab.definition.structural] "numFixed: {recArgInfo.numFixed}, indexMajorArgs: {indexMajorArgs}, otherArgs: {otherArgs}"
+    let motive ← mkForallFVars otherArgs type
+    let motive ← mkLambdaFVars indexMajorArgs motive
+    trace[Elab.definition.structural] "brecOn motive: {motive}"
+    let brecOn := Lean.mkConst (mkBRecOnName recArgInfo.indName) recArgInfo.indLevels
+    let brecOn := mkAppN brecOn recArgInfo.indParams
+    let brecOn := mkApp brecOn motive
+    let brecOn := mkAppN brecOn indexMajorArgs
+    check brecOn
+    let brecOnType ← inferType brecOn
+    trace[Elab.definition.structural] "brecOn     {brecOn}"
+    trace[Elab.definition.structural] "brecOnType {brecOnType}"
+    -- we need to close the telescope here, because the local context is used:
+    -- The root cause was, that this copied code puts an ih : FType into the
+    -- local context and later, when we use the local context to build the recursive
+    -- call, it uses this ih. But that ih doesn't exist in the actual brecOn call.
+    -- That's why it must go.
+    let FType ← forallBoundedTelescope brecOnType (some 1) fun F _ => do
+      let F := F[0]!
+      let FType ← inferType F
+      trace[Elab.definition.structural] "FType: {FType}"
+      instantiateForall FType indexMajorArgs
+    forallBoundedTelescope FType (some 1) fun below _ => do
+      let below := below[0]!
+      let valueNew     ← replaceIndPredRecApps recArgInfo motive value
+      let Farg         ← mkLambdaFVars (indexMajorArgs ++ #[below] ++ otherArgs) valueNew
+      let brecOn       := mkApp brecOn Farg
+      let brecOn       := mkAppN brecOn otherArgs
+      mkLambdaFVars ys brecOn
 
 end Lean.Elab.Structural

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

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
+Authors: Leonardo de Moura, Joachim Breitner
 -/
 prelude
 import Lean.Elab.PreDefinition.TerminationArgument
@@ -59,55 +59,158 @@ private def getFixedPrefix (declName : Name) (xs : Array Expr) (value : Expr) :
       return true
   numFixedRef.get
 
-private def elimRecursion (preDef : PreDefinition) (termArg? : Option TerminationArgument) : M (Nat × PreDefinition) := do
-  trace[Elab.definition.structural] "{preDef.declName} := {preDef.value}"
-  withoutModifyingEnv do lambdaTelescope preDef.value fun xs value => do
-    addAsAxiom preDef
-    let value ← preprocess value preDef.declName
-    trace[Elab.definition.structural] "{preDef.declName} {xs} :=\n{value}"
-    let numFixed ← getFixedPrefix preDef.declName xs value
-    trace[Elab.definition.structural] "numFixed: {numFixed}"
-    let go := fun recArgInfo => do
-      let valueNew ← if recArgInfo.indPred then
-        mkIndPredBRecOn preDef.declName recArgInfo value
-      else
-        mkBRecOn preDef.declName recArgInfo value
-      let valueNew ← mkLambdaFVars xs valueNew
-      trace[Elab.definition.structural] "result: {valueNew}"
-      -- Recursive applications may still occur in expressions that were not visited by replaceRecApps (e.g., in types)
-      let valueNew ← ensureNoRecFn preDef.declName valueNew
-      let recArgPos := recArgInfo.fixedParams.size + recArgInfo.pos
-      return (recArgPos, { preDef with value := valueNew })
-    -- Use termination_by annotation to find argument to recurse on, or just try all
-    match termArg? with
-    | .some termArg =>
-        assert! termArg.structural
-        withRecArgInfo numFixed xs (← termArg.structuralArg) go
-    | .none => findRecArg numFixed xs go
+partial def withCommonTelescope (preDefs : Array PreDefinition) (k : Array Expr → Array Expr → M α) : M α :=
+  go #[] (preDefs.map (·.value))
+where
+  go (fvars : Array Expr) (vals : Array Expr) : M α := do
+    if !(vals.all fun val => val.isLambda) then
+      k fvars vals
+    else if !(← vals.allM fun val => return val.bindingName! == vals[0]!.bindingName! && val.binderInfo == vals[0]!.binderInfo && (← isDefEq val.bindingDomain! vals[0]!.bindingDomain!)) then
+      k fvars vals
+    else
+      withLocalDecl vals[0]!.bindingName! vals[0]!.binderInfo vals[0]!.bindingDomain! fun x =>
+        go (fvars.push x) (vals.map fun val => val.bindingBody!.instantiate1 x)
+
+def getMutualFixedPrefix (preDefs : Array PreDefinition) : M Nat :=
+  withCommonTelescope preDefs fun xs vals => do
+    let resultRef ← IO.mkRef xs.size
+    for val in vals do
+      if (← resultRef.get) == 0 then return 0
+      forEachExpr' val fun e => do
+        if preDefs.any fun preDef => e.isAppOf preDef.declName then
+          let args := e.getAppArgs
+          resultRef.modify (min args.size ·)
+          for arg in args, x in xs do
+            if !(← withoutProofIrrelevance <| withReducible <| isDefEq arg x) then
+              -- We continue searching if e's arguments are not a prefix of `xs`
+              return true
+          return false
+        else
+          return true
+    resultRef.get
+
+/-- Checks that all parameter types are mutually inductive -/
+private def checkAllFromSameClique (recArgInfos : Array RecArgInfo) : MetaM Unit := do
+  for recArgInfo in recArgInfos do
+    unless recArgInfos[0]!.indAll.contains recArgInfo.indName do
+      throwError m!"Cannot use structural mutual recursion: The recursive argument of " ++
+        m!"{recArgInfos[0]!.fnName} is of type {recArgInfos[0]!.indName}, " ++
+        m!"the recursive argument of {recArgInfo.fnName} is of type " ++
+            m!"{recArgInfo.indName}, and these are not mutually recursive."
+
+private def elimMutualRecursion (preDefs : Array PreDefinition) (recArgPoss : Array Nat) : M (Array PreDefinition) := do
+  withoutModifyingEnv do
+    preDefs.forM (addAsAxiom ·)
+    let names := preDefs.map (·.declName)
+    let preDefs ← preDefs.mapM fun preDef =>
+      return { preDef with value := (← preprocess preDef.value names) }
+
+    -- The syntactically fixed arguments
+    let maxNumFixed ← getMutualFixedPrefix preDefs
+
+    -- We do two passes to get the RecArgInfo values.
+    -- From the first pass, we only keep the  mininum of the `numFixed` reported.
+    let numFixed ← lambdaBoundedTelescope preDefs[0]!.value maxNumFixed fun xs _ => do
+      assert! xs.size = maxNumFixed
+      let values ← preDefs.mapM (instantiateLambda ·.value xs)
+
+      let recArgInfos ← preDefs.mapIdxM fun i preDef => do
+        let recArgPos := recArgPoss[i]!
+        let value := values[i]!
+        lambdaTelescope value fun ys _value => do
+          getRecArgInfo preDef.declName maxNumFixed (xs ++ ys) recArgPos
+
+      return (recArgInfos.map (·.numFixed)).foldl Nat.min maxNumFixed
+
+    if numFixed < maxNumFixed then
+      trace[Elab.definition.structural] "Reduced numFixed from {maxNumFixed} to {numFixed}"
+
+    -- Now we bring exactly that `numFixed` parameter into scope.
+    lambdaBoundedTelescope preDefs[0]!.value numFixed fun xs _ => do
+      assert! xs.size = numFixed
+      let values ← preDefs.mapM (instantiateLambda ·.value xs)
+
+      let recArgInfos ← preDefs.mapIdxM fun i preDef => do
+        let recArgPos := recArgPoss[i]!
+        let value := values[i]!
+        lambdaTelescope value fun ys _value => do
+          getRecArgInfo preDef.declName numFixed (xs ++ ys) recArgPos
+
+      -- Two passes should suffice
+      assert! recArgInfos.all (·.numFixed = numFixed)
+
+      let indInfo ← getConstInfoInduct recArgInfos[0]!.indName
+      if ← isInductivePredicate indInfo.name then
+        -- Here we branch off to the IndPred construction, but only for non-mutual functions
+        unless preDefs.size = 1 do
+          throwError "structural mutual recursion over inductive predicates is not supported"
+        trace[Elab.definition.structural] "Using mkIndPred construction"
+        let preDef := preDefs[0]!
+        let recArgInfo := recArgInfos[0]!
+        let value := values[0]!
+        let valueNew ← mkIndPredBRecOn recArgInfo value
+        let valueNew ← mkLambdaFVars xs valueNew
+        trace[Elab.definition.structural] "Nonrecursive value:{indentExpr valueNew}"
+        check valueNew
+        return #[{ preDef with value := valueNew }]
+
+      checkAllFromSameClique recArgInfos
+      -- Sort the (indices of the) definitions by their position in indInfo.all
+      let positions : Positions := .groupAndSort (·.indName) recArgInfos indInfo.all.toArray
+
+      -- Construct the common `.brecOn` arguments
+      let motives ← (Array.zip recArgInfos values).mapM fun (r, v) => mkBRecOnMotive r v
+      let brecOnConst ← mkBRecOnConst recArgInfos positions motives
+      let FTypes ← inferBRecOnFTypes recArgInfos positions brecOnConst
+      let FArgs ← (recArgInfos.zip  (values.zip FTypes)).mapM fun (r, (v, t)) =>
+        mkBRecOnF recArgInfos positions r v t
+      -- Assemble the individual `.brecOn` applications
+      let valuesNew ← (Array.zip recArgInfos values).mapIdxM fun i (r, v) =>
+        mkBrecOnApp positions i brecOnConst FArgs r v
+      -- Abstract over the fixed prefixed
+      let valuesNew ← valuesNew.mapM (mkLambdaFVars xs ·)
+      return (Array.zip preDefs valuesNew).map fun ⟨preDef, valueNew⟩ => { preDef with value := valueNew }
 
 def reportTermArg (preDef : PreDefinition) (recArgPos : Nat) : MetaM Unit := do
   if let some ref := preDef.termination.terminationBy?? then
     let fn ← lambdaTelescope preDef.value fun xs _ => mkLambdaFVars xs xs[recArgPos]!
-    let termArg : TerminationArgument := {ref := .missing, structural := true, fn}
+    let termArg : TerminationArgument:= {ref := .missing, structural := true, fn}
     let arity ← lambdaTelescope preDef.value fun xs _ => pure xs.size
     let stx ← termArg.delab arity (extraParams := preDef.termination.extraParams)
     Tactic.TryThis.addSuggestion ref stx
 
-def structuralRecursion (preDefs : Array PreDefinition) (termArgs? : Option TerminationArguments) : TermElabM Unit :=
-  if preDefs.size != 1 then
-    throwError "structural recursion does not handle mutually recursive functions"
-  else do
-    let termArg? := termArgs?.map (·[0]!)
-    let ((recArgPos, preDefNonRec), state) ← run <| elimRecursion preDefs[0]! termArg?
-    reportTermArg preDefNonRec recArgPos
+private def inferRecArgPos (preDefs : Array PreDefinition)
+    (termArgs? : Option TerminationArguments) : M (Array Nat × Array PreDefinition) := do
+  withoutModifyingEnv do
+    if let some termArgs := termArgs? then
+      let recArgPoss ← termArgs.mapM (·.structuralArg)
+      let preDefsNew ← elimMutualRecursion preDefs recArgPoss
+      return (recArgPoss, preDefsNew)
+    else
+      let #[preDef] := preDefs
+        | throwError "mutual structural recursion requires explicit `termination_by` clauses"
+      -- Use termination_by annotation to find argument to recurse on, or just try all
+      tryAllArgs preDef.value fun i =>
+        mapError (f := fun msg => m!"argument #{i+1} cannot be used for structural recursion{indentD msg}") do
+          let preDefsNew ← elimMutualRecursion #[preDef] #[i]
+          return (#[i], preDefsNew)
+
+def structuralRecursion (preDefs : Array PreDefinition) (termArgs? : Option TerminationArguments) : TermElabM Unit := do
+  let ((recArgPoss, preDefsNonRec), state) ← run <| inferRecArgPos preDefs termArgs?
+  for recArgPos in recArgPoss, preDef in preDefs do
+    reportTermArg preDef recArgPos
+  state.addMatchers.forM liftM
+  preDefsNonRec.forM fun preDefNonRec => do
     let preDefNonRec ← eraseRecAppSyntax preDefNonRec
-    let mut preDef ← eraseRecAppSyntax preDefs[0]!
-    state.addMatchers.forM liftM
+    -- state.addMatchers.forM liftM
     mapError (addNonRec preDefNonRec (applyAttrAfterCompilation := false)) fun msg =>
       m!"structural recursion failed, produced type incorrect term{indentD msg}"
     -- We create the `_unsafe_rec` before we abstract nested proofs.
     -- Reason: the nested proofs may be referring to the _unsafe_rec.
-    addAndCompilePartialRec #[preDef]
+  let preDefs ← preDefs.mapM (eraseRecAppSyntax ·)
+  addAndCompilePartialRec preDefs
+  for preDef in preDefs, recArgPos in recArgPoss do
+    let mut preDef := preDef
     unless preDef.kind.isTheorem do
       unless (← isProp preDef.type) do
         preDef ← abstractNestedProofs preDef
@@ -119,7 +222,7 @@ def structuralRecursion (preDefs : Array PreDefinition) (termArgs? : Option Term
         registerEqnsInfo preDef (preDefs.map (·.declName)) recArgPos
     addSmartUnfoldingDef preDef recArgPos
     markAsRecursive preDef.declName
-    applyAttributesOf #[preDefNonRec] AttributeApplicationTime.afterCompilation
+  applyAttributesOf preDefsNonRec AttributeApplicationTime.afterCompilation
 
 builtin_initialize
   registerTraceClass `Elab.definition.structural

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

@@ -10,9 +10,9 @@ import Lean.Elab.RecAppSyntax
 namespace Lean.Elab.Structural
 open Meta
 
-private def shouldBetaReduce (e : Expr) (recFnName : Name) : Bool :=
+private def shouldBetaReduce (e : Expr) (recFnNames : Array Name) : Bool :=
   if e.isHeadBetaTarget then
-    e.getAppFn.find? (·.isConstOf recFnName) |>.isSome
+    e.getAppFn.find? (fun e => e.isConst && recFnNames.contains e.constName!) |>.isSome
   else
     false
 
@@ -35,10 +35,10 @@ Preprocesses the expessions to improve the effectiveness of `elimRecursion`.
     | i+1 => (f x) i
   ```
 -/
-def preprocess (e : Expr) (recFnName : Name) : CoreM Expr :=
+def preprocess (e : Expr) (recFnNames : Array Name) : CoreM Expr :=
   Core.transform e
     (pre := fun e =>
-      if shouldBetaReduce e recFnName then
+      if shouldBetaReduce e recFnNames then
         return .visit e.headBeta
       else
         return .continue)

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

@@ -37,7 +37,7 @@ private partial def replaceRecApps (recFnName : Name) (fixedPrefixSize : Nat) (F
   trace[Elab.definition.wf] "{F} : {← inferType F}"
   loop F e |>.run' {}
 where
-  processRec (F : Expr) (e : Expr) : StateRefT (HasConstCache recFnName) TermElabM Expr := do
+  processRec (F : Expr) (e : Expr) : StateRefT (HasConstCache #[recFnName]) TermElabM Expr := do
     if e.getAppNumArgs < fixedPrefixSize + 1 then
       loop F (← etaExpand e)
     else
@@ -47,16 +47,16 @@ where
       let r := mkApp r (← mkDecreasingProof decreasingProp)
       return mkAppN r (← args[fixedPrefixSize+1:].toArray.mapM (loop F))
 
-  processApp (F : Expr) (e : Expr) : StateRefT (HasConstCache recFnName) TermElabM Expr := do
+  processApp (F : Expr) (e : Expr) : StateRefT (HasConstCache #[recFnName]) TermElabM Expr := do
     if e.isAppOf recFnName then
       processRec F e
     else
       e.withApp fun f args => return mkAppN (← loop F f) (← args.mapM (loop F))
 
-  containsRecFn (e : Expr) : StateRefT (HasConstCache recFnName) TermElabM Bool := do
+  containsRecFn (e : Expr) : StateRefT (HasConstCache #[recFnName]) TermElabM Bool := do
     modifyGet (·.contains e)
 
-  loop (F : Expr) (e : Expr) : StateRefT (HasConstCache recFnName) TermElabM Expr := do
+  loop (F : Expr) (e : Expr) : StateRefT (HasConstCache #[recFnName]) TermElabM Expr := do
     if !(← containsRecFn e) then
       return e
     match e with
@@ -90,7 +90,9 @@ where
         else
           processApp F e
       | none => processApp F e
-    | e => ensureNoRecFn recFnName e
+    | e =>
+      ensureNoRecFn #[recFnName] e
+      pure e
 
 /-- Refine `F` over `PSum.casesOn` -/
 private partial def processSumCasesOn (x F val : Expr) (k : (x : Expr) → (F : Expr) → (val : Expr) → TermElabM Expr) : TermElabM Expr := do

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

@@ -192,7 +192,7 @@ def simpleMeasures (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)
 
 /-- Internal monad used by `withRecApps` -/
 abbrev M (recFnName : Name) (α β : Type) : Type :=
-  StateRefT (Array α) (StateRefT (HasConstCache recFnName) MetaM) β
+  StateRefT (Array α) (StateRefT (HasConstCache #[recFnName]) MetaM) β
 
 /--
 Traverses the given expression `e`, and invokes the continuation `k`
@@ -223,7 +223,7 @@ where
         loop param f
 
   containsRecFn (e : Expr) : M recFnName α Bool := do
-    modifyGetThe (HasConstCache recFnName) (·.contains e)
+    modifyGetThe (HasConstCache #[recFnName]) (·.contains e)
 
   loop (param : Expr) (e : Expr) : M recFnName α Unit := do
     if !(← containsRecFn e) then
@@ -266,7 +266,7 @@ where
           processApp param e
       | none => processApp param e
     | e => do
-      let _ ← ensureNoRecFn recFnName e
+      ensureNoRecFn #[recFnName] e
 
 /--
 A `SavedLocalContext` captures the state and local context of a `MetaM`, to be continued later.

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

@@ -10,23 +10,6 @@ import Lean.Elab.PreDefinition.Basic
 namespace Lean.Elab.WF
 open Meta
 
-
-/--
-Checks that all codomians have the same level, throws an error otherwise.
--/
-private def checkCodomainsLevel (fixedPrefixSize : Nat) (arities : Array Nat)
-    (preDefs : Array PreDefinition) : MetaM Unit := do
-  forallBoundedTelescope preDefs[0]!.type  (fixedPrefixSize + arities[0]!)  fun _ type₀ => do
-    let u₀ ← getLevel type₀
-    for i in [1:preDefs.size] do
-      forallBoundedTelescope preDefs[i]!.type  (fixedPrefixSize + arities[i]!) fun _ typeᵢ =>
-      unless ← isLevelDefEq u₀ (← getLevel typeᵢ) do
-        withOptions (fun o => pp.sanitizeNames.set o false) do
-          throwError m!"invalid mutual definition, result types must be in the same universe " ++
-            m!"level, resulting type " ++
-            m!"for `{preDefs[0]!.declName}` is{indentExpr type₀} : {← inferType type₀}\n" ++
-            m!"and for `{preDefs[i]!.declName}` is{indentExpr typeᵢ} : {← inferType typeᵢ}"
-
 /--
   Pass the first `n` arguments of `e` to the continuation, and apply the result to the
   remaining arguments. If `e` does not have enough arguments, it is eta-expanded as needed.
@@ -75,8 +58,6 @@ def packMutual (fixedPrefix : Nat) (argsPacker : ArgsPacker) (preDefs : Array Pr
   if let #[1] := arities then return preDefs[0]!
   let newFn := if argsPacker.numFuncs > 1 then preDefs[0]!.declName ++ `_mutual
                                           else preDefs[0]!.declName ++ `_unary
-
-  checkCodomainsLevel fixedPrefix argsPacker.arities preDefs
   -- Bring the fixed Prefix into scope
   forallBoundedTelescope preDefs[0]!.type (some fixedPrefix) fun ys _ => do
     let types ← preDefs.mapM (instantiateForall ·.type ys)

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -93,7 +93,8 @@ where
             let (_, state) ← withRestoreOrSaveFull reusableResult?
                 -- set up nested reuse; `evalTactic` will check for `isIncrementalElab`
                 (tacSnap? := some { old? := oldInner?, new := inner }) do
-              evalTactic tac
+              Term.withReuseContext tac do
+                evalTactic tac
             finished.resolve { state? := state }
 
         withTheReader Term.Context ({ · with tacSnap? := some {

src/Lean/Elab/Tactic/Ext.lean

@@ -5,14 +5,164 @@ Authors: Gabriel Ebner, Mario Carneiro
 -/
 prelude
 import Init.Ext
+import Lean.Elab.DeclarationRange
 import Lean.Elab.Tactic.RCases
 import Lean.Elab.Tactic.Repeat
 import Lean.Elab.Tactic.BuiltinTactic
 import Lean.Elab.Command
 import Lean.Linter.Util
 
+/-!
+# Implementation of the `@[ext]` attribute
+-/
+
 namespace Lean.Elab.Tactic.Ext
 open Meta Term
+
+/-!
+### Meta code for creating ext theorems
+-/
+
+/--
+Constructs the hypotheses for the structure extensionality theorem that
+states that two structures are equal if their fields are equal.
+
+Calls the continuation `k` with the list of parameters to the structure,
+two structure variables `x` and `y`, and a list of pairs `(field, ty)`
+where each `ty` is of the form `x.field = y.field` or `HEq x.field y.field`.
+
+If `flat` parses to `true`, any fields inherited from parent structures
+are treated as fields of the given structure type.
+If it is `false`, then the behind-the-scenes encoding of inherited fields
+is visible in the extensionality lemma.
+-/
+def withExtHyps (struct : Name) (flat : Bool)
+    (k : Array Expr → (x y : Expr) → Array (Name × Expr) → MetaM α) : MetaM α := do
+  unless isStructure (← getEnv) struct do throwError "not a structure: {struct}"
+  let structC ← mkConstWithLevelParams struct
+  forallTelescope (← inferType structC) fun params _ => do
+  withNewBinderInfos (params.map (·.fvarId!, BinderInfo.implicit)) do
+  withLocalDecl `x .implicit (mkAppN structC params) fun x => do
+  withLocalDecl `y .implicit (mkAppN structC params) fun y => do
+    let mut hyps := #[]
+    let fields ← if flat then
+      pure <| getStructureFieldsFlattened (← getEnv) struct (includeSubobjectFields := false)
+    else
+      pure <| getStructureFields (← getEnv) struct
+    for field in fields do
+      let x_f ← mkProjection x field
+      let y_f ← mkProjection y field
+      unless ← isProof x_f do
+        hyps := hyps.push (field, ← mkEqHEq x_f y_f)
+    k params x y hyps
+
+/--
+Creates the type of the extensionality theorem for the given structure,
+returning `∀ {x y : Struct}, x.1 = y.1 → x.2 = y.2 → x = y`, for example.
+-/
+def mkExtType (structName : Name) (flat : Bool) : MetaM Expr := withLCtx {} {} do
+  withExtHyps structName flat fun params x y hyps => do
+    let ty := hyps.foldr (init := ← mkEq x y) fun (f, h) ty => .forallE f h ty .default
+    mkForallFVars (params |>.push x |>.push y) ty
+
+/--
+Derives the type of the `iff` form of an ext theorem.
+-/
+def mkExtIffType (extThmName : Name) : MetaM Expr := withLCtx {} {} do
+  forallTelescopeReducing (← getConstInfo extThmName).type fun args ty => do
+    let failNotEq := throwError "expecting a theorem proving x = y, but instead it proves{indentD ty}"
+    let some (_, x, y) := ty.eq? | failNotEq
+    let some xIdx := args.findIdx? (· == x) | failNotEq
+    let some yIdx := args.findIdx? (· == y) | failNotEq
+    unless xIdx == yIdx + 1 || xIdx + 1 == yIdx do
+      throwError "expecting {x} and {y} to be consecutive arguments"
+    let startIdx := max xIdx yIdx + 1
+    let toRevert := args[startIdx:].toArray
+    let fvars ← toRevert.foldlM (init := {}) (fun st e => return collectFVars st (← inferType e))
+    for fvar in toRevert do
+      unless ← Meta.isProof fvar do
+        throwError "argument {fvar} is not a proof, which is not supported"
+      if fvars.fvarSet.contains fvar.fvarId! then
+        throwError "argument {fvar} is depended upon, which is not supported"
+    let conj := mkAndN (← toRevert.mapM (inferType ·)).toList
+    withNewBinderInfos (args |>.extract 0 startIdx |>.map (·.fvarId!, .implicit)) do
+      mkForallFVars args[:startIdx] <| mkIff ty conj
+
+/--
+Ensures that the given structure has an ext theorem, without validating any pre-existing theorems.
+Returns the name of the ext theorem.
+
+See `Lean.Elab.Tactic.Ext.withExtHyps` for an explanation of the `flat` argument.
+-/
+def realizeExtTheorem (structName : Name) (flat : Bool) : Elab.Command.CommandElabM Name := do
+  unless isStructure (← getEnv) structName do
+    throwError "'{structName}' is not a structure"
+  let extName := structName.mkStr "ext"
+  unless (← getEnv).contains extName do
+    Elab.Command.liftTermElabM <| withoutErrToSorry <| withDeclName extName do
+      let type ← mkExtType structName flat
+      let pf ← withSynthesize do
+        let indVal ← getConstInfoInduct structName
+        let params := Array.mkArray indVal.numParams (← `(_))
+        Elab.Term.elabTermEnsuringType (expectedType? := type) (implicitLambda := false)
+          -- introduce the params, do cases on 'x' and 'y', and then substitute each equation
+          (← `(by intro $params* {..} {..}; intros; subst_eqs; rfl))
+      let pf ← instantiateMVars pf
+      if pf.hasMVar then throwError "(internal error) synthesized ext proof contains metavariables{indentD pf}"
+      let info ← getConstInfo structName
+      addDecl <| Declaration.thmDecl {
+        name := extName
+        type
+        value := pf
+        levelParams := info.levelParams
+      }
+      modifyEnv fun env => addProtected env extName
+      Lean.addDeclarationRanges extName {
+        range := ← getDeclarationRange (← getRef)
+        selectionRange := ← getDeclarationRange (← getRef) }
+  return extName
+
+/--
+Given an 'ext' theorem, ensures that there is an iff version of the theorem (if possible),
+without validating any pre-existing theorems.
+Returns the name of the 'ext_iff' theorem.
+-/
+def realizeExtIffTheorem (extName : Name) : Elab.Command.CommandElabM Name := do
+  let extIffName : Name :=
+    match extName with
+    | .str n s => .str n (s ++ "_iff")
+    | _ => .str extName "ext_iff"
+  unless (← getEnv).contains extIffName do
+    let info ← getConstInfo extName
+    Elab.Command.liftTermElabM <| withoutErrToSorry <| withDeclName extIffName do
+      let type ← mkExtIffType extName
+      let pf ← withSynthesize do
+        Elab.Term.elabTermEnsuringType (expectedType? := type) <| ← `(by
+          intros
+          refine ⟨?_, ?_⟩
+          · intro h; cases h; and_intros <;> (intros; first | rfl | simp | fail "Failed to prove converse of ext theorem")
+          · intro; (repeat cases ‹_ ∧ _›); apply $(mkCIdent extName) <;> assumption)
+      let pf ← instantiateMVars pf
+      if pf.hasMVar then throwError "(internal error) synthesized ext_iff proof contains metavariables{indentD pf}"
+      addDecl <| Declaration.thmDecl {
+        name := extIffName
+        type
+        value := pf
+        levelParams := info.levelParams
+      }
+      -- Only declarations in a namespace can be protected:
+      unless extIffName.isAtomic do
+        modifyEnv fun env => addProtected env extIffName
+      Lean.addDeclarationRanges extIffName {
+        range := ← getDeclarationRange (← getRef)
+        selectionRange := ← getDeclarationRange (← getRef) }
+  return extIffName
+
+
+/-!
+### Attribute
+-/
+
 /-- Information about an extensionality theorem, stored in the environment extension. -/
 structure ExtTheorem where
   /-- Declaration name of the extensionality theorem. -/
@@ -66,9 +216,9 @@ def ExtTheorems.eraseCore (d : ExtTheorems) (declName : Name) : ExtTheorems :=
  { d with erased := d.erased.insert declName }
 
 /--
-  Erases a name marked as a `ext` attribute.
-  Check that it does in fact have the `ext` attribute by making sure it names a `ExtTheorem`
-  found somewhere in the state's tree, and is not erased.
+Erases a name marked as a `ext` attribute.
+Check that it does in fact have the `ext` attribute by making sure it names a `ExtTheorem`
+found somewhere in the state's tree, and is not erased.
 -/
 def ExtTheorems.erase [Monad m] [MonadError m] (d : ExtTheorems) (declName : Name) :
     m ExtTheorems := do
@@ -79,97 +229,40 @@ def ExtTheorems.erase [Monad m] [MonadError m] (d : ExtTheorems) (declName : Nam
 builtin_initialize registerBuiltinAttribute {
   name := `ext
   descr := "Marks a theorem as an extensionality theorem"
-  add := fun declName stx kind => do
-    let `(attr| ext $[(flat := $f)]? $(prio)?) := stx
-      | throwError "unexpected @[ext] attribute {stx}"
+  add := fun declName stx kind => MetaM.run' do
+    let `(attr| ext $[(iff := false%$iffFalse?)]? $[(flat := false%$flatFalse?)]? $(prio)?) := stx
+      | throwError "invalid syntax for 'ext' attribute"
+    let iff := iffFalse?.isNone
+    let flat := flatFalse?.isNone
+    let mut declName := declName
     if isStructure (← getEnv) declName then
-      liftCommandElabM <| Elab.Command.elabCommand <|
-        ← `(declare_ext_theorems_for $[(flat := $f)]? $(mkCIdentFrom stx declName) $[$prio]?)
-    else MetaM.run' do
-      if let some flat := f then
-        throwErrorAt flat "unexpected 'flat' config on @[ext] theorem"
-      let declTy := (← getConstInfo declName).type
-      let (_, _, declTy) ← withDefault <| forallMetaTelescopeReducing declTy
-      let failNotEq := throwError
-        "@[ext] attribute only applies to structures or theorems proving x = y, got {declTy}"
-      let some (ty, lhs, rhs) := declTy.eq? | failNotEq
-      unless lhs.isMVar && rhs.isMVar do failNotEq
-      let keys ← withReducible <| DiscrTree.mkPath ty extExt.config
-      let priority ← liftCommandElabM do Elab.liftMacroM do
-        evalPrio (prio.getD (← `(prio| default)))
-      extExtension.add {declName, keys, priority} kind
+      declName ← liftCommandElabM <| withRef stx <| realizeExtTheorem declName flat
+    else if let some stx := flatFalse? then
+      throwErrorAt stx "unexpected 'flat' configuration on @[ext] theorem"
+    -- Validate and add theorem to environment extension
+    let declTy := (← getConstInfo declName).type
+    let (_, _, declTy) ← withDefault <| forallMetaTelescopeReducing declTy
+    let failNotEq := throwError "\
+      @[ext] attribute only applies to structures and to theorems proving 'x = y' where 'x' and 'y' are variables, \
+      but this theorem proves{indentD declTy}"
+    let some (ty, lhs, rhs) := declTy.eq? | failNotEq
+    unless lhs.isMVar && rhs.isMVar do failNotEq
+    let keys ← withReducible <| DiscrTree.mkPath ty extExt.config
+    let priority ← liftCommandElabM <| Elab.liftMacroM do evalPrio (prio.getD (← `(prio| default)))
+    extExtension.add {declName, keys, priority} kind
+    -- Realize iff theorem
+    if iff then
+      discard <| liftCommandElabM <| withRef stx <| realizeExtIffTheorem declName
   erase := fun declName => do
     let s := extExtension.getState (← getEnv)
     let s ← s.erase declName
     modifyEnv fun env => extExtension.modifyState env fun _ => s
 }
 
-/--
-Constructs the hypotheses for the structure extensionality theorem that
-states that two structures are equal if their fields are equal.
 
-Calls the continuation `k` with the list of parameters to the structure,
-two structure variables `x` and `y`, and a list of pairs `(field, ty)`
-where `ty` is `x.field = y.field` or `HEq x.field y.field`.
-
-If `flat` parses to `true`, any fields inherited from parent structures
-are treated fields of the given structure type.
-If it is `false`, then the behind-the-scenes encoding of inherited fields
-is visible in the extensionality lemma.
+/-!
+### Implementation of `ext` tactic
 -/
--- TODO: this is probably the wrong place to have this function
-def withExtHyps (struct : Name) (flat : Term)
-    (k : Array Expr → (x y : Expr) → Array (Name × Expr) → MetaM α) : MetaM α := do
-  let flat ← match flat with
-  | `(true) => pure true
-  | `(false) => pure false
-  | _ => throwErrorAt flat "expected 'true' or 'false'"
-  unless isStructure (← getEnv) struct do throwError "not a structure: {struct}"
-  let structC ← mkConstWithLevelParams struct
-  forallTelescope (← inferType structC) fun params _ => do
-  withNewBinderInfos (params.map (·.fvarId!, BinderInfo.implicit)) do
-  withLocalDeclD `x (mkAppN structC params) fun x => do
-  withLocalDeclD `y (mkAppN structC params) fun y => do
-    let mut hyps := #[]
-    let fields ← if flat then
-      pure <| getStructureFieldsFlattened (← getEnv) struct (includeSubobjectFields := false)
-    else
-      pure <| getStructureFields (← getEnv) struct
-    for field in fields do
-      let x_f ← mkProjection x field
-      let y_f ← mkProjection y field
-      if ← isProof x_f then
-        pure ()
-      else if ← isDefEq (← inferType x_f) (← inferType y_f) then
-        hyps := hyps.push (field, ← mkEq x_f y_f)
-      else
-        hyps := hyps.push (field, ← mkHEq x_f y_f)
-    k params x y hyps
-
-/--
-Creates the type of the extensionality theorem for the given structure,
-elaborating to `x.1 = y.1 → x.2 = y.2 → x = y`, for example.
--/
-@[builtin_term_elab extType] def elabExtType : TermElab := fun stx _ => do
-  match stx with
-  | `(ext_type%  $flat:term $struct:ident) => do
-    withExtHyps (← realizeGlobalConstNoOverloadWithInfo struct) flat fun params x y hyps => do
-      let ty := hyps.foldr (init := ← mkEq x y) fun (f, h) ty =>
-        mkForall f BinderInfo.default h ty
-      mkForallFVars (params |>.push x |>.push y) ty
-  | _ => throwUnsupportedSyntax
-
-/--
-Creates the type of the iff-variant of the extensionality theorem for the given structure,
-elaborating to `x = y ↔ x.1 = y.1 ∧ x.2 = y.2`, for example.
--/
-@[builtin_term_elab extIffType] def elabExtIffType : TermElab := fun stx _ => do
-  match stx with
-  | `(ext_iff_type% $flat:term $struct:ident) => do
-    withExtHyps (← realizeGlobalConstNoOverloadWithInfo struct) flat fun params x y hyps => do
-      mkForallFVars (params |>.push x |>.push y) <|
-        mkIff (← mkEq x y) <| mkAndN (hyps.map (·.2)).toList
-  | _ => throwUnsupportedSyntax
 
 /-- Apply a single extensionality theorem to `goal`. -/
 def applyExtTheoremAt (goal : MVarId) : MetaM (List MVarId) := goal.withContext do

src/Lean/Elab/Tactic/Omega/Frontend.lean

@@ -254,7 +254,17 @@ where
     | _ => match n.getAppFnArgs with
     | (``Nat.succ, #[n]) => rewrite e (.app (.const ``Int.ofNat_succ []) n)
     | (``HAdd.hAdd, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_add []) a b)
-    | (``HMul.hMul, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_mul []) a b)
+    | (``HMul.hMul, #[_, _, _, _, a, b]) =>
+      -- Don't push the cast into a multiplication unless it produces a non-trivial linear combination.
+      let r? ← commitWhen do
+        let (lc, prf, r) ← rewrite e (mkApp2 (.const ``Int.ofNat_mul []) a b)
+        if lc.isAtom then
+          pure (none, false)
+        else
+          pure (some (lc, prf, r), true)
+      match r? with
+      | some r => pure r
+      | none => mkAtomLinearCombo e
     | (``HDiv.hDiv, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_ediv []) a b)
     | (``OfNat.ofNat, #[_, n, _]) => rewrite e (.app (.const ``Int.natCast_ofNat []) n)
     | (``HMod.hMod, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_emod []) a b)

src/Lean/Elab/Term.lean

@@ -360,21 +360,39 @@ instance : MonadBacktrack SavedState TermElabM where
   saveState      := Term.saveState
   restoreState b := b.restore
 
+/--
+Incremental elaboration helper. Avoids leakage of data from outside syntax via the monadic context
+when running `act` on `stx` by
+* setting `stx` as the `ref` and
+* deactivating `suppressElabErrors` if `stx` is `missing`-free, which also helps with not hiding
+  useful errors in this part of the input. Note that if `stx` has `missing`, this should always be
+  true for the outer syntax as well, so taking the old value of `suppressElabErrors` into account
+  should not introduce data leakage.
+
+This combinator should always be used when narrowing reuse to a syntax subtree, usually (in the case
+of tactics, to be generalized) via `withNarrowed(Arg)TacticReuse`.
+-/
+def withReuseContext [Monad m] [MonadWithReaderOf Core.Context m] (stx : Syntax) (act : m α) :
+    m α := do
+  withTheReader Core.Context (fun ctx => { ctx with
+      ref := stx
+      suppressElabErrors := ctx.suppressElabErrors && stx.hasMissing }) act
+
 /--
 Manages reuse information for nested tactics by `split`ting given syntax into an outer and inner
 part. `act` is then run on the inner part but with reuse information adjusted as following:
 * If the old (from `tacSnap?`'s `SyntaxGuarded.stx`) and new (from `stx`) outer syntax are not
   identical according to `Syntax.eqWithInfo`, reuse is disabled.
 * Otherwise, the old syntax as stored in `tacSnap?` is updated to the old *inner* syntax.
-* In any case, we also use `withRef` on the inner syntax to avoid leakage of the outer syntax into
-  `act` via this route.
+* In any case, `withReuseContext` is used on the new inner syntax to further prepare the monadic
+  context.
 
 For any tactic that participates in reuse, `withNarrowedTacticReuse` should be applied to the
 tactic's syntax and `act` should be used to do recursive tactic evaluation of nested parts.
 -/
-def withNarrowedTacticReuse [Monad m] [MonadWithReaderOf Context m]
-    [MonadOptions m] [MonadRef m] (split : Syntax → Syntax × Syntax) (act : Syntax → m α)
-    (stx : Syntax) : m α := do
+def withNarrowedTacticReuse [Monad m] [MonadWithReaderOf Core.Context m]
+    [MonadWithReaderOf Context m] [MonadOptions m] (split : Syntax → Syntax × Syntax)
+    (act : Syntax → m α) (stx : Syntax) : m α := do
   let (outer, inner) := split stx
   let opts ← getOptions
   withTheReader Term.Context (fun ctx => { ctx with tacSnap? := ctx.tacSnap?.map fun tacSnap =>
@@ -384,8 +402,7 @@ def withNarrowedTacticReuse [Monad m] [MonadWithReaderOf Context m]
       return { old with stx := oldInner }
     }
   }) do
-    withRef inner do
-      act inner
+    withReuseContext inner (act inner)
 
 /--
 A variant of `withNarrowedTacticReuse` that uses `stx[argIdx]` as the inner syntax and all `stx`
@@ -396,8 +413,8 @@ NOTE: child nodes after `argIdx` are not tested (which would almost always disab
 necessarily shifted by changes at `argIdx`) so it must be ensured that the result of `arg` does not
 depend on them (i.e. they should not be inspected beforehand).
 -/
-def withNarrowedArgTacticReuse [Monad m] [MonadWithReaderOf Context m]
-    [MonadOptions m] [MonadRef m] (argIdx : Nat) (act : Syntax → m α) (stx : Syntax) : m α :=
+def withNarrowedArgTacticReuse [Monad m] [MonadWithReaderOf Core.Context m] [MonadWithReaderOf Context m]
+    [MonadOptions m] (argIdx : Nat) (act : Syntax → m α) (stx : Syntax) : m α :=
   withNarrowedTacticReuse (fun stx => (mkNullNode stx.getArgs[:argIdx], stx[argIdx])) act stx
 
 /--

src/Lean/Environment.lean

@@ -868,9 +868,9 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
           -- Recall that the map has not been modified when `cinfoPrev? = some _`.
           unless equivInfo cinfoPrev cinfo do
             throwAlreadyImported s const2ModIdx modIdx cname
-      const2ModIdx := const2ModIdx.insert cname modIdx
+      const2ModIdx := const2ModIdx.insertIfNew cname modIdx |>.1
     for cname in mod.extraConstNames do
-      const2ModIdx := const2ModIdx.insert cname modIdx
+      const2ModIdx := const2ModIdx.insertIfNew cname modIdx |>.1
   let constants : ConstMap := SMap.fromHashMap constantMap false
   let exts ← mkInitialExtensionStates
   let mut env : Environment := {

src/Lean/Exception.lean

@@ -105,7 +105,7 @@ class MonadRecDepth (m : Type → Type) where
   getRecDepth      : m Nat
   getMaxRecDepth   : m Nat
 
-instance [Monad m] [MonadRecDepth m] : MonadRecDepth (ReaderT ρ m) where
+instance [MonadRecDepth m] : MonadRecDepth (ReaderT ρ m) where
   withRecDepth d x := fun ctx => MonadRecDepth.withRecDepth d (x ctx)
   getRecDepth      := fun _ => MonadRecDepth.getRecDepth
   getMaxRecDepth   := fun _ => MonadRecDepth.getMaxRecDepth

src/Lean/Meta/InferType.lean

@@ -420,4 +420,26 @@ Remark: it subsumes `isType`
 def isTypeFormer (e : Expr) : MetaM Bool := do
   isTypeFormerType (← inferType e)
 
+
+/--
+Given `n` and a non-dependent function type `α₁ → α₂ → ... → αₙ → Sort u`, returns the
+types `α₁, α₂, ..., αₙ`. Throws an error if there are not at least `n` argument types or if a
+later argument type depends on a prior one (i.e., it's a dependent function type).
+
+This can be used to infer the expected type of the alternatives when constructing a `MatcherApp`.
+-/
+def arrowDomainsN (n : Nat) (type : Expr) : MetaM (Array Expr) := do
+  forallBoundedTelescope type n fun xs _ => do
+    let types ← xs.mapM (inferType ·)
+    for t in types do
+      if t.hasAnyFVar (fun fvar => xs.contains (.fvar fvar)) then
+        throwError "unexpected dependent type {t} in {type}"
+    return types
+
+/--
+Infers the types of the next `n` parameters that `e` expects. See `arrowDomainsN`.
+-/
+def inferArgumentTypesN (n : Nat) (e : Expr) : MetaM (Array Expr) := do
+  arrowDomainsN n (← inferType e)
+
 end Lean.Meta

src/Lean/Meta/Match/MatcherApp/Transform.lean

@@ -159,25 +159,6 @@ def refineThrough? (matcherApp : MatcherApp) (e : Expr) :
     return none
 
 
-/--
-Given `n` and a non-dependent function type `α₁ → α₂ → ... → αₙ → Sort u`, returns the
-types `α₁, α₂, ..., αₙ`. Throws an error if there are not at least `n` argument types or if a
-later argument type depends on a prior one (i.e., it's a dependent function type).
-
-This can be used to infer the expected type of the alternatives when constructing a `MatcherApp`.
--/
--- TODO: Which is the natural module for this?
-def arrowDomainsN (n : Nat) (type : Expr) : MetaM (Array Expr) := do
-  let mut type := type
-  let mut ts := #[]
-  for i in [:n] do
-    type ← whnfForall type
-    let Expr.forallE _ α β _ ← pure type | throwError "expected {n} arguments, got {i}"
-    if β.hasLooseBVars then throwError "unexpected dependent type"
-    ts := ts.push α
-    type := β
-  return ts
-
 private def withUserNamesImpl {α} (fvars : Array Expr) (names : Array Name) (k : MetaM α) : MetaM α := do
   let lctx := (Array.zip fvars names).foldl (init := ← (getLCtx)) fun lctx (fvar, name) =>
     lctx.setUserName fvar.fvarId! name
@@ -295,7 +276,7 @@ def transform
     unless (← isTypeCorrect aux1) do
       logError m!"failed to transform matcher, type error when constructing new pre-splitter motive:{indentExpr aux1}"
       check aux1
-    let origAltTypes ← arrowDomainsN matcherApp.alts.size (← inferType aux1)
+    let origAltTypes ← inferArgumentTypesN matcherApp.alts.size aux1
 
     let aux2 := mkAppN (mkConst splitter matcherLevels.toList) params'
     let aux2 := mkApp aux2 motive'
@@ -303,7 +284,7 @@ def transform
     unless (← isTypeCorrect aux2) do
       logError m!"failed to transform matcher, type error when constructing splitter motive:{indentExpr aux2}"
       check aux2
-    let altTypes ← arrowDomainsN matcherApp.alts.size (← inferType aux2)
+    let altTypes ← inferArgumentTypesN matcherApp.alts.size aux2
 
     let mut alts' := #[]
     for alt in matcherApp.alts,
@@ -343,7 +324,7 @@ def transform
     unless (← isTypeCorrect aux) do
       logError m!"failed to transform matcher, type error when constructing new motive:{indentExpr aux}"
       check aux
-    let altTypes ← arrowDomainsN matcherApp.alts.size (← inferType aux)
+    let altTypes ← inferArgumentTypesN matcherApp.alts.size aux
 
     let mut alts' := #[]
     for alt in matcherApp.alts,

src/Lean/Meta/Tactic/FunInd.lean

@@ -741,6 +741,12 @@ def findRecursor {α} (name : Name) (varNames : Array Name) (e : Expr)
     MatcherApp.withUserNames params varNames do
       if not f.isConst then err else
       if isBRecOnRecursor (← getEnv) f.constName! then
+        -- Bail out on mutual or nested inductives
+        let .str indName _ := f.constName! | unreachable!
+        let indInfo ← getConstInfoInduct indName
+        if indInfo.all.length > 1 then
+          throwError "functional induction: cannot handle mutual inductives"
+
         let elimInfo ← getElimExprInfo f
         let targets : Array Expr := elimInfo.targetsPos.map (args[·]!)
         let body := args[elimInfo.motivePos + 1 + elimInfo.targetsPos.size]!

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs.lean

@@ -12,3 +12,4 @@ import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.String
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.List

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/List.lean

@@ -0,0 +1,21 @@
+/-
+Copyright (c) 2024 Lean FRO. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Lean.Meta.LitValues
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
+
+namespace List
+open Lean Meta Simp
+
+/-- Simplification procedure for `List.replicate` applied to a `Nat` literal. -/
+-- We don't always want `List.replicate_succ` as a `simp` lemma,
+-- so we use this `dsimproc` to unfold `List.replicate` applied to literals.
+builtin_dsimproc [simp, seval] reduceReplicate (replicate _ _) := fun e => do
+  let_expr replicate α n x ← e | return .continue
+  let some n ← Nat.fromExpr? n | return .continue
+  return .done <| (← mkListLit α (List.replicate n x))
+
+end List

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -438,19 +438,19 @@ private def doNotVisit (pred : Expr → Bool) (declName : Name) : DSimproc := fu
     return .continue e
 
 /--
-Auliliary `dsimproc` for not visiting `OfNat.ofNat` application subterms.
+Auxiliary `dsimproc` for not visiting `OfNat.ofNat` application subterms.
 This is the `dsimp` equivalent of the approach used at `visitApp`.
 Recall that we fold orphan raw Nat literals.
 -/
 private def doNotVisitOfNat : DSimproc := doNotVisit isOfNatNatLit ``OfNat.ofNat
 
 /--
-Auliliary `dsimproc` for not visiting `OfScientific.ofScientific` application subterms.
+Auxiliary `dsimproc` for not visiting `OfScientific.ofScientific` application subterms.
 -/
 private def doNotVisitOfScientific : DSimproc := doNotVisit isOfScientificLit ``OfScientific.ofScientific
 
 /--
-Auliliary `dsimproc` for not visiting `Char` literal subterms.
+Auxiliary `dsimproc` for not visiting `Char` literal subterms.
 -/
 private def doNotVisitCharLit : DSimproc := doNotVisit isCharLit ``Char.ofNat
 

src/Lean/ResolveName.lean

@@ -314,7 +314,7 @@ def ensureNoOverload [Monad m] [MonadError m] (n : Name) (cs : List Name) : m Na
 def resolveGlobalConstNoOverloadCore [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (n : Name) : m Name := do
   ensureNoOverload n (← resolveGlobalConstCore n)
 
-def preprocessSyntaxAndResolve [Monad m] [MonadEnv m] [MonadError m] (stx : Syntax) (k : Name → m (List Name)) : m (List Name) := do
+def preprocessSyntaxAndResolve [Monad m] [MonadError m] (stx : Syntax) (k : Name → m (List Name)) : m (List Name) := do
   match stx with
   | .ident _ _ n pre => do
     let pre := pre.filterMap fun

src/Lean/ToExpr.lean

@@ -106,6 +106,10 @@ instance : ToExpr Unit where
   toExpr     := fun _ => mkConst `Unit.unit
   toTypeExpr := mkConst ``Unit
 
+instance : ToExpr System.FilePath where
+  toExpr p := mkApp (mkConst ``System.FilePath.mk) (toExpr p.toString)
+  toTypeExpr := mkConst ``System.FilePath
+
 private def Name.toExprAux (n : Name) : Expr :=
   if isSimple n 0 then
     mkStr n 0 #[]

src/Lean/Util.lean

@@ -29,4 +29,5 @@ import Lean.Util.OccursCheck
 import Lean.Util.HasConstCache
 import Lean.Util.FileSetupInfo
 import Lean.Util.Heartbeats
+import Lean.Util.SearchPath
 import Lean.Util.SafeExponentiation

src/Lean/Util/HasConstCache.lean

@@ -8,15 +8,15 @@ import Lean.Expr
 
 namespace Lean
 
-structure HasConstCache (declName : Name) where
+structure HasConstCache (declNames : Array Name) where
   cache : HashMapImp Expr Bool := mkHashMapImp
 
-unsafe def HasConstCache.containsUnsafe (e : Expr) : StateM (HasConstCache declName) Bool := do
+unsafe def HasConstCache.containsUnsafe (e : Expr) : StateM (HasConstCache declNames) Bool := do
   if let some r := (← get).cache.find? (beq := ⟨ptrEq⟩) e then
     return r
   else
     match e with
-    | .const n ..        => return n == declName
+    | .const n ..        => return declNames.contains n
     | .app f a           => cache e (← containsUnsafe f <||> containsUnsafe a)
     | .lam _ d b _       => cache e (← containsUnsafe d <||> containsUnsafe b)
     | .forallE _ d b _   => cache e (← containsUnsafe d <||> containsUnsafe b)
@@ -25,7 +25,7 @@ unsafe def HasConstCache.containsUnsafe (e : Expr) : StateM (HasConstCache declN
     | .proj _ _ b        => cache e (← containsUnsafe b)
     | _                  => return false
 where
-  cache (e : Expr) (r : Bool) : StateM (HasConstCache declName) Bool := do
+  cache (e : Expr) (r : Bool) : StateM (HasConstCache declNames) Bool := do
     modify fun ⟨cache⟩ => ⟨cache.insert (beq := ⟨ptrEq⟩) e r |>.1⟩
     return r
 
@@ -33,6 +33,6 @@ where
   Return true iff `e` contains the constant `declName`.
   Remark: the results for visited expressions are stored in the state cache. -/
 @[implemented_by HasConstCache.containsUnsafe]
-opaque HasConstCache.contains (e : Expr) : StateM (HasConstCache declName) Bool
+opaque HasConstCache.contains (e : Expr) : StateM (HasConstCache declNames) Bool
 
 end Lean

src/Lean/Util/SearchPath.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Lean.ToExpr
+import Lean.Util.Path
+import Lean.Elab.Term
+
+open Lean
+
+/--
+Term elaborator that retrieves the current `SearchPath`.
+
+Typical usage is `searchPathRef.set compile_time_search_path%`.
+
+This must not be used in files that are potentially compiled on another machine and then imported.
+(That is, if used in an imported file it will embed the search path from whichever machine
+compiled the `.olean`.)
+-/
+elab "compile_time_search_path%" : term =>
+  return toExpr (← searchPathRef.get)

src/Std/Data.lean

@@ -7,3 +7,10 @@ prelude
 import Std.Data.DHashMap
 import Std.Data.HashMap
 import Std.Data.HashSet
+
+-- The three imports above only import the modules needed to work with the version which bundles
+-- the well-formedness invariant, so we need to additionally import the files that deal with the
+-- unbundled version
+import Std.Data.DHashMap.RawLemmas
+import Std.Data.HashMap.RawLemmas
+import Std.Data.HashSet.RawLemmas

src/Std/Data/DHashMap.lean

@@ -5,6 +5,5 @@ Authors: Markus Himmel
 -/
 prelude
 import Std.Data.DHashMap.Basic
-import Std.Data.DHashMap.RawLemmas
 import Std.Data.DHashMap.Lemmas
 import Std.Data.DHashMap.AdditionalOperations

src/Std/Data/DHashMap/Basic.lean

@@ -63,6 +63,9 @@ namespace DHashMap
 instance [BEq α] [Hashable α] : EmptyCollection (DHashMap α β) where
   emptyCollection := empty
 
+instance [BEq α] [Hashable α] : Inhabited (DHashMap α β) where
+  default := ∅
+
 @[inline, inherit_doc Raw.insert] def insert [BEq α] [Hashable α] (m : DHashMap α β) (a : α)
     (b : β a) : DHashMap α β :=
   ⟨Raw₀.insert ⟨m.1, m.2.size_buckets_pos⟩ a b, .insert₀ m.2⟩

src/Std/Data/DHashMap/Raw.lean

@@ -54,6 +54,9 @@ capacity.
 instance : EmptyCollection (Raw α β) where
   emptyCollection := empty
 
+instance : Inhabited (Raw α β) where
+  default := ∅
+
 /--
 Inserts the given mapping into the map, replacing an existing mapping for the key if there is one.
 -/

src/Std/Data/HashMap/Basic.lean

@@ -66,6 +66,9 @@ namespace HashMap
 instance [BEq α] [Hashable α] : EmptyCollection (HashMap α β) where
   emptyCollection := empty
 
+instance [BEq α] [Hashable α] : Inhabited (HashMap α β) where
+  default := ∅
+
 @[inline, inherit_doc DHashMap.insert] def insert [BEq α] [Hashable α] (m : HashMap α β) (a : α)
     (b : β) : HashMap α β :=
   ⟨m.inner.insert a b⟩

src/Std/Data/HashMap/Raw.lean

@@ -63,6 +63,9 @@ namespace Raw
 instance : EmptyCollection (Raw α β) where
   emptyCollection := empty
 
+instance : Inhabited (Raw α β) where
+  default := ∅
+
 @[inline, inherit_doc DHashMap.Raw.insert] def insert [BEq α] [Hashable α] (m : Raw α β) (a : α)
     (b : β) : Raw α β :=
   ⟨m.inner.insert a b⟩

src/Std/Data/HashSet/Basic.lean

@@ -64,6 +64,9 @@ capacity.
 instance [BEq α] [Hashable α] : EmptyCollection (HashSet α) where
   emptyCollection := empty
 
+instance [BEq α] [Hashable α] : Inhabited (HashSet α) where
+  default := ∅
+
 /--
 Inserts the given element into the set. If the hash set already contains an element that is
 equal (with regard to `==`) to the given element, then the hash set is returned unchanged.

src/Std/Data/HashSet/Raw.lean

@@ -65,6 +65,9 @@ the empty collection notations `∅` and `{}` to create an empty hash set with t
 instance : EmptyCollection (Raw α) where
   emptyCollection := empty
 
+instance : Inhabited (Raw α) where
+  default := ∅
+
 /--
 Inserts the given element into the set. If the hash set already contains an element that is
 equal (with regard to `==`) to the given element, then the hash set is returned unchanged.

src/kernel/declaration.cpp

@@ -100,22 +100,22 @@ recursor_rule::recursor_rule(name const & cnstr, unsigned nfields, expr const &
 }
 
 extern "C" object * lean_mk_inductive_val(object * n, object * lparams, object * type, object * nparams, object * nindices,
-                                          object * all, object * cnstrs, uint8 rec, uint8 unsafe, uint8 is_refl, uint8 is_nested);
+                                          object * all, object * cnstrs, object * nnested, uint8 rec, uint8 unsafe, uint8 is_refl);
 extern "C" uint8 lean_inductive_val_is_rec(object * v);
 extern "C" uint8 lean_inductive_val_is_unsafe(object * v);
 extern "C" uint8 lean_inductive_val_is_reflexive(object * v);
-extern "C" uint8 lean_inductive_val_is_nested(object * v);
 
 inductive_val::inductive_val(name const & n, names const & lparams, expr const & type, unsigned nparams,
-                             unsigned nindices, names const & all, names const & cnstrs, bool rec, bool unsafe, bool is_refl, bool is_nested):
+                             unsigned nindices, names const & all, names const & cnstrs, unsigned nnested,
+                             bool rec, bool unsafe, bool is_refl):
     object_ref(lean_mk_inductive_val(n.to_obj_arg(), lparams.to_obj_arg(), type.to_obj_arg(), nat(nparams).to_obj_arg(),
-                                     nat(nindices).to_obj_arg(), all.to_obj_arg(), cnstrs.to_obj_arg(), rec, unsafe, is_refl, is_nested)) {
+                                     nat(nindices).to_obj_arg(), all.to_obj_arg(), cnstrs.to_obj_arg(),
+                                     nat(nnested).to_obj_arg(), rec, unsafe, is_refl)) {
 }
 
 bool inductive_val::is_rec() const { return lean_inductive_val_is_rec(to_obj_arg()); }
 bool inductive_val::is_unsafe() const { return lean_inductive_val_is_unsafe(to_obj_arg()); }
 bool inductive_val::is_reflexive() const { return lean_inductive_val_is_reflexive(to_obj_arg()); }
-bool inductive_val::is_nested() const { return lean_inductive_val_is_nested(to_obj_arg()); }
 
 extern "C" object * lean_mk_constructor_val(object * n, object * lparams, object * type, object * induct,
                                             object * cidx, object * nparams, object * nfields, uint8 unsafe);

src/kernel/declaration.h

@@ -12,10 +12,10 @@ Author: Leonardo de Moura
 
 namespace lean {
 /**
-inductive reducibility_hints
-| opaque  : reducibility_hints
-| abbrev  : reducibility_hints
-| regular : nat → reducibility_hints
+inductive ReducibilityHints where
+  | opaque  : ReducibilityHints
+  | abbrev  : ReducibilityHints
+  | regular : UInt32 → ReducibilityHints
 
 Reducibility hints are used in the convertibility checker (aka is_def_eq predicate),
 whenever checking a constraint such as
@@ -54,8 +54,10 @@ public:
 int compare(reducibility_hints const & h1, reducibility_hints const & h2);
 
 /*
-structure constant_val :=
-(id : name) (lparams : list name) (type : expr)
+structure ConstantVal where
+  name : Name
+  levelParams : List Name
+  type : Expr
 */
 class constant_val : public object_ref {
 public:
@@ -70,8 +72,8 @@ public:
 };
 
 /*
-structure axiom_val extends constant_val :=
-(is_unsafe : bool)
+structure AxiomVal extends ConstantVal where
+  isUnsafe : Bool
 */
 class axiom_val : public object_ref {
 public:
@@ -87,11 +89,17 @@ public:
     bool is_unsafe() const;
 };
 
+/*
+inductive DefinitionSafety where
+  | «unsafe» | safe | «partial»
+*/
 enum class definition_safety { unsafe, safe, partial };
 
 /*
-structure definition_val extends constant_val :=
-(value : expr) (hints : reducibility_hints) (is_unsafe : bool)
+structure DefinitionVal extends ConstantVal where
+  value  : Expr
+  hints  : ReducibilityHints
+  safety : DefinitionSafety
 */
 class definition_val : public object_ref {
 public:
@@ -131,8 +139,10 @@ public:
 };
 
 /*
-structure opaque_val extends constant_val :=
-(value : expr)
+structure OpaqueVal extends ConstantVal where
+  value : Expr
+  isUnsafe : Bool
+  all : List Name := [name]
 */
 class opaque_val : public object_ref {
 public:
@@ -150,8 +160,9 @@ public:
 };
 
 /*
-structure constructor :=
-(id : name) (type : expr)
+structure Constructor where
+  name : Name
+  type : Expr
 */
 typedef pair_ref<name, expr> constructor;
 inline name const & constructor_name(constructor const & c) { return c.fst(); }
@@ -159,8 +170,10 @@ inline expr const & constructor_type(constructor const & c) { return c.snd(); }
 typedef list_ref<constructor> constructors;
 
 /**
-structure inductive_type where
-(id : name) (type : expr) (cnstrs : list constructor)
+structure InductiveType where
+  name : Name
+  type : Expr
+  ctors : List Constructor
 */
 class inductive_type : public object_ref {
 public:
@@ -176,14 +189,14 @@ public:
 typedef list_ref<inductive_type> inductive_types;
 
 /*
-inductive declaration
-| axiom_decl       (val : axiom_val)
-| defn_decl        (val : definition_val)
-| thm_decl         (val : theorem_val)
-| opaque_decl      (val : opaque_val)
-| quot_decl        (id : name)
-| mutual_defn_decl (defns : list definition_val) -- All definitions must be marked as `unsafe`
-| induct_decl      (lparams : list name) (nparams : nat) (types : list inductive_type) (is_unsafe : bool)
+inductive Declaration where
+  | axiomDecl       (val : AxiomVal)
+  | defnDecl        (val : DefinitionVal)
+  | thmDecl         (val : TheoremVal)
+  | opaqueDecl      (val : OpaqueVal)
+  | quotDecl
+  | mutualDefnDecl  (defns : List DefinitionVal) -- All definitions must be marked as `unsafe` or `partial`
+  | inductDecl      (lparams : List Name) (nparams : Nat) (types : List InductiveType) (isUnsafe : Bool)
 */
 enum class declaration_kind { Axiom, Definition, Theorem, Opaque, Quot, MutualDefinition, Inductive };
 class declaration : public object_ref {
@@ -261,19 +274,21 @@ public:
 };
 
 /*
-structure inductive_val extends constant_val where
-(nparams : nat)       -- Number of parameters
-(nindices : nat)      -- Number of indices
-(all : list name)     -- List of all (including this one) inductive datatypes in the mutual declaration containing this one
-(cnstrs : list name)  -- List of all constructors for this inductive datatype
-(is_rec : bool)       -- `tt` iff it is recursive
-(is_unsafe : bool)
-(is_reflexive : bool)
+structure InductiveVal extends ConstantVal where
+  numParams : Nat
+  numIndices : Nat
+  all : List Name    -- List of all (including this one) inductive datatypes in the mutual
+                        declaration containing this one
+  ctors : List Name  -- List of the names of the constructors for this inductive datatype
+  numNested : Nat
+  isRec : Bool
+  isUnsafe : Bool
+  isReflexive : Bool
 */
 class inductive_val : public object_ref {
 public:
     inductive_val(name const & n, names const & lparams, expr const & type, unsigned nparams,
-                  unsigned nindices, names const & all, names const & cnstrs, bool is_rec, bool is_unsafe, bool is_reflexive, bool is_nested);
+                  unsigned nindices, names const & all, names const & cnstrs, unsigned nnested, bool is_rec, bool is_unsafe, bool is_reflexive);
     inductive_val(inductive_val const & other):object_ref(other) {}
     inductive_val(inductive_val && other):object_ref(other) {}
     inductive_val & operator=(inductive_val const & other) { object_ref::operator=(other); return *this; }
@@ -284,19 +299,19 @@ public:
     names const & get_all() const { return static_cast<names const &>(cnstr_get_ref(*this, 3)); }
     names const & get_cnstrs() const { return static_cast<names const &>(cnstr_get_ref(*this, 4)); }
     unsigned get_ncnstrs() const { return length(get_cnstrs()); }
+    unsigned get_nnested() const { return static_cast<nat const &>(cnstr_get_ref(*this, 5)).get_small_value(); }
     bool is_rec() const;
     bool is_unsafe() const;
     bool is_reflexive() const;
-    bool is_nested() const;
 };
 
 /*
-structure constructor_val extends constant_val :=
-(induct  : name)  -- Inductive type this constructor is a member of
-(cidx    : nat)   -- Constructor index (i.e., position in the inductive declaration)
-(nparams : nat)   -- Number of parameters in inductive datatype `induct`
-(nfields : nat)   -- Number of fields (i.e., arity - nparams)
-(is_unsafe : bool)
+structure ConstructorVal extends ConstantVal where
+  induct  : Name  -- Inductive type this constructor is a member of
+  cidx    : Nat   -- Constructor index (i.e., Position in the inductive declaration)
+  numParams : Nat -- Number of parameters in inductive datatype
+  numFields : Nat -- Number of fields (i.e., arity - nparams)
+  isUnsafe : Bool
 */
 class constructor_val : public object_ref {
 public:
@@ -314,10 +329,10 @@ public:
 };
 
 /*
-structure recursor_rule :=
-(cnstr : name)  -- Reduction rule for this constructor
-(nfields : nat) -- Number of fields (i.e., without counting inductive datatype parameters)
-(rhs : expr)    -- Right hand side of the reduction rule
+structure RecursorRule where
+  ctor : Name   -- Reduction rule for this Constructor
+  nfields : Nat -- Number of fields (i.e., without counting inductive datatype parameters)
+  rhs : Expr    -- Right hand side of the reduction rule
 */
 class recursor_rule : public object_ref {
 public:
@@ -334,15 +349,15 @@ public:
 typedef list_ref<recursor_rule> recursor_rules;
 
 /*
-structure recursor_val extends constant_val :=
-(all : list name)            -- List of all inductive datatypes in the mutual declaration that generated this recursor
-(nparams : nat)              -- Number of parameters
-(nindices : nat)             -- Number of indices
-(nmotives : nat)             -- Number of motives
-(nminors : nat)              -- Number of minor premises
-(rules : list recursor_rule) -- A reduction for each constructor
-(k : bool)                   -- It supports K-like reduction
-(is_unsafe : bool)
+structure RecursorVal extends ConstantVal where
+  all : List Name  -- List of all inductive datatypes in the mutual declaration that generated this recursor
+  numParams : Nat
+  numIndices : Nat
+  numMotives : Nat
+  numMinors : Nat
+  rules : List RecursorRule
+  k : Bool         -- It supports K-like reduction.
+  isUnsafe : Bool
 */
 class recursor_val : public object_ref {
 public:
@@ -370,14 +385,14 @@ public:
 enum class quot_kind { Type, Mk, Lift, Ind };
 
 /*
-inductive quot_kind
-| type  -- `quot`
-| cnstr -- `quot.mk`
-| lift  -- `quot.lift`
-| ind   -- `quot.ind`
+inductive QuotKind where
+  | type  -- `Quot`
+  | ctor  -- `Quot.mk`
+  | lift  -- `Quot.lift`
+  | ind   -- `Quot.ind`
 
-structure quot_val extends constant_val :=
-(kind : quot_kind)
+structure QuotVal extends ConstantVal where
+  kind : QuotKind
 */
 class quot_val : public object_ref {
 public:
@@ -395,15 +410,15 @@ public:
 
 /*
 /-- Information associated with constant declarations. -/
-inductive constant_info
-| axiom_info    (val : axiom_val)
-| defn_info     (val : definition_val)
-| thm_info      (val : theorem_val)
-| opaque_info   (val : opaque_val)
-| quot_info     (val : quot_val)
-| induct_info   (val : inductive_val)
-| cnstr_info    (val : constructor_val)
-| rec_info      (val : recursor_val)
+inductive ConstantInfo where
+  | axiomInfo    (val : AxiomVal)
+  | defnInfo     (val : DefinitionVal)
+  | thmInfo      (val : TheoremVal)
+  | opaqueInfo   (val : OpaqueVal)
+  | quotInfo     (val : QuotVal)
+  | inductInfo   (val : InductiveVal)
+  | ctorInfo     (val : ConstructorVal)
+  | recInfo      (val : RecursorVal)l)
 */
 enum class constant_info_kind { Axiom, Definition, Theorem, Opaque, Quot, Inductive, Constructor, Recursor };
 class constant_info : public object_ref {

src/kernel/inductive.cpp

@@ -145,7 +145,7 @@ class add_inductive_fn {
     level                  m_elim_level;
     bool                   m_K_target;
 
-    bool                   m_is_nested;
+    unsigned               m_nnested;
 
     struct rec_info {
         expr         m_C;        /* free variable for "main" motive */
@@ -159,9 +159,9 @@ class add_inductive_fn {
     buffer<rec_info>       m_rec_infos;
 
 public:
-    add_inductive_fn(environment const & env, diagnostics * diag, inductive_decl const & decl, bool is_nested):
+    add_inductive_fn(environment const & env, diagnostics * diag, inductive_decl const & decl, unsigned nnested):
         m_env(env), m_ngen(*g_ind_fresh), m_diag(diag), m_lparams(decl.get_lparams()), m_is_unsafe(decl.is_unsafe()),
-        m_is_nested(is_nested) {
+        m_nnested(nnested) {
         if (!decl.get_nparams().is_small())
             throw kernel_exception(env, "invalid inductive datatype, number of parameters is too big");
         m_nparams = decl.get_nparams().get_small_value();
@@ -326,7 +326,7 @@ public:
                 cnstr_names.push_back(constructor_name(cnstr));
             }
             m_env.add_core(constant_info(inductive_val(n, m_lparams, ind_type.get_type(), m_nparams, m_nindices[idx],
-                                                       all, names(cnstr_names), rec, m_is_unsafe, reflexive, m_is_nested)));
+                                                       all, names(cnstr_names), m_nnested, rec, m_is_unsafe, reflexive)));
         }
     }
 
@@ -1112,10 +1112,10 @@ static pair<names, name_map<name>> mk_aux_rec_name_map(environment const & aux_e
 
 environment environment::add_inductive(declaration const & d) const {
     elim_nested_inductive_result res = elim_nested_inductive_fn(*this, d)();
-    bool is_nested = !res.m_aux2nested.empty();
+    unsigned nnested = res.m_aux2nested.size();
     scoped_diagnostics diag(*this, true);
-    environment aux_env = add_inductive_fn(*this, diag.get(), inductive_decl(res.m_aux_decl), is_nested)();
-    if (!is_nested) {
+    environment aux_env = add_inductive_fn(*this, diag.get(), inductive_decl(res.m_aux_decl), nnested)();
+    if (!nnested) {
         /* `d` did not contain nested inductive types. */
         return diag.update(aux_env);
     } else {
@@ -1157,8 +1157,8 @@ environment environment::add_inductive(declaration const & d) const {
                Remark: if we decide to store the recursor names, we will also need to fix it. */
             new_env.add_core(constant_info(inductive_val(ind_info.get_name(), ind_info.get_lparams(), ind_info.get_type(),
                                                          ind_val.get_nparams(), ind_val.get_nindices(),
-                                                         all_ind_names, ind_val.get_cnstrs(),
-                                                         ind_val.is_rec(), ind_val.is_unsafe(), ind_val.is_reflexive(), ind_val.is_nested())));
+                                                         all_ind_names, ind_val.get_cnstrs(), ind_val.get_nnested(),
+                                                         ind_val.is_rec(), ind_val.is_unsafe(), ind_val.is_reflexive())));
             for (name const & cnstr_name : ind_val.get_cnstrs()) {
                 constant_info   cnstr_info = aux_env.get(cnstr_name);
                 constructor_val cnstr_val  = cnstr_info.to_constructor_val();

src/lake/Lake/CLI/Translate/Lean.lean

@@ -169,7 +169,14 @@ protected def Dependency.mkSyntax (cfg : Dependency) : RequireDecl := Unhygienic
       `(fromSource|$(quote dir):term)
     | .git url rev? subDir? =>
       `(fromSource|git $(quote url) $[@ $(rev?.map quote)]? $[/ $(subDir?.map quote)]?)
-  let ver? := cfg.version?.map quote
+  let ver? ←
+    if let some ver := cfg.version? then
+      if ver.startsWith "git#" then
+        some <$> `(verSpec|git $(quote <| ver.drop 4))
+      else
+        some <$> `(verSpec|$(quote ver):term)
+    else
+      pure none
   let scope? := if cfg.scope.isEmpty then none else some (quote cfg.scope)
   let opts? := if cfg.opts.isEmpty then none else some <| Unhygienic.run do
     cfg.opts.foldM (init := mkCIdent ``NameMap.empty) fun stx opt val =>

src/lake/Lake/DSL/Require.lean

@@ -56,24 +56,31 @@ subdirectory is specified).
 syntax fromClause :=
   " from " fromSource
 
+/-
+A `NameMap String` of Lake options used to configure the dependency.
+This is equivalent to passing `-K` options to the dependency on the command line.
+-/
 syntax withClause :=
   " with " term
 
+syntax verSpec :=
+  &"git "? term:max
+
 /--
 The version of the package to lookup in Lake's package index.
-A Git revision can be specified via `"git#<rev>"`.
+A Git revision can be specified via `@ git "<rev>"`.
 -/
-syntax verSpec :=
-  " @ " term:max
+syntax verClause :=
+  " @ " verSpec
 
 syntax depName :=
   atomic(str " / ")? identOrStr
 
 syntax depSpec :=
-  depName (verSpec)? (fromClause)? (withClause)?
+  depName (verClause)? (fromClause)? (withClause)?
 
 @[inline] private def quoteOptTerm [Monad m] [MonadQuotation m] (term? : Option Term) : m Term :=
-  if let some term := term? then withRef term `(some $term) else `(none)
+  if let some term := term? then withRef term ``(some $term) else ``(none)
 
 def expandDepSpec (stx : TSyntax ``depSpec) (doc? : Option DocComment) : MacroM Command := do
   let `(depSpec| $fullNameStx $[@ $ver?]? $[from $src?]? $[with $opts?]?) := stx
@@ -93,11 +100,19 @@ def expandDepSpec (stx : TSyntax ``depSpec) (doc? : Option DocComment) : MacroM
     match scope? with
     | some scope => scope
     | none => Syntax.mkStrLit "" (.fromRef fullNameStx)
+  let ver ←
+    if let some ver := ver? then withRef ver do
+      match ver with
+      | `(verSpec|git $ver) => ``(some ("git#" ++ $ver))
+      | `(verSpec|$ver:term) => ``(some $ver)
+      | _ => Macro.throwErrorAt ver "ill-formed version syntax"
+    else
+      ``(none)
   let name := expandIdentOrStrAsIdent nameStx
   `($[$doc?:docComment]? @[package_dep] def $name : $(mkCIdent ``Dependency) := {
     name :=  $(quote name.getId),
     scope := $scope,
-    version? := $(← quoteOptTerm ver?),
+    version? := $ver,
     src? := $(← quoteOptTerm src?),
     opts := $(opts?.getD <| ← `({})),
   })

src/lake/Lake/Util/FilePath.lean

@@ -22,7 +22,3 @@ def mkRelPathString (path : FilePath) : String :=
 
 scoped instance : ToJson FilePath where
   toJson path := toJson <| mkRelPathString path
-
-scoped instance : ToExpr FilePath where
-  toExpr p := mkApp (mkConst ``System.FilePath.mk) (toExpr p.toString)
-  toTypeExpr := mkConst ``System.FilePath

src/lake/tests/translateConfig/out.expected.lean

@@ -9,7 +9,7 @@ package test where
   lintDriver := "b"
   platformIndependent := true
 
-require "foo" / baz @ "git#abcdef"
+require "foo" / baz @ git "abcdef"
 
 require foo from "-" with Lake.NameMap.empty |>.insert `foo "bar"
 

src/runtime/process.cpp

@@ -92,6 +92,22 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_child_wait(b_obj_arg, b_obj_arg c
     return lean_io_result_mk_ok(box_uint32(exit_code));
 }
 
+extern "C" LEAN_EXPORT obj_res lean_io_process_child_try_wait(b_obj_arg, b_obj_arg child, obj_arg) {
+    HANDLE h = static_cast<HANDLE>(lean_get_external_data(cnstr_get(child, 3)));
+    DWORD exit_code;
+    DWORD ret = WaitForSingleObject(h, 0);
+    if (ret == WAIT_FAILED) {
+        return io_result_mk_error((sstream() << GetLastError()).str());
+    } else if (ret == WAIT_TIMEOUT) {
+        return io_result_mk_ok(mk_option_none());
+    } else {
+        if (!GetExitCodeProcess(h, &exit_code)) {
+            return io_result_mk_error((sstream() << GetLastError()).str());
+        }
+        return lean_io_result_mk_ok(mk_option_some(box_uint32(exit_code)));
+    }
+}
+
 extern "C" LEAN_EXPORT obj_res lean_io_process_child_kill(b_obj_arg, b_obj_arg child, obj_arg) {
     HANDLE h = static_cast<HANDLE>(lean_get_external_data(cnstr_get(child, 3)));
     if (!TerminateProcess(h, 1)) {
@@ -309,6 +325,28 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_child_wait(b_obj_arg, b_obj_arg c
     }
 }
 
+extern "C" LEAN_EXPORT obj_res lean_io_process_child_try_wait(b_obj_arg, b_obj_arg child, obj_arg) {
+    static_assert(sizeof(pid_t) == sizeof(uint32), "pid_t is expected to be a 32-bit type"); // NOLINT
+    pid_t pid = cnstr_get_uint32(child, 3 * sizeof(object *));
+    int status;
+    int ret = waitpid(pid, &status, WNOHANG);
+    if (ret == -1) {
+        return io_result_mk_error(decode_io_error(errno, nullptr));
+    } else if (ret == 0) {
+        return io_result_mk_ok(mk_option_none());
+    } else {
+        if (WIFEXITED(status)) {
+            obj_res output = box_uint32(static_cast<unsigned>(WEXITSTATUS(status)));
+            return lean_io_result_mk_ok(mk_option_some(output));
+        } else {
+            lean_assert(WIFSIGNALED(status));
+            // use bash's convention
+            obj_res output = box_uint32(128 + static_cast<unsigned>(WTERMSIG(status)));
+            return lean_io_result_mk_ok(mk_option_some(output));
+        }
+    }
+}
+
 extern "C" LEAN_EXPORT obj_res lean_io_process_child_kill(b_obj_arg, b_obj_arg child, obj_arg) {
     static_assert(sizeof(pid_t) == sizeof(uint32), "pid_t is expected to be a 32-bit type"); // NOLINT
     pid_t pid = cnstr_get_uint32(child, 3 * sizeof(object *));