fix

This PR fixes a bug in the pattern selection in the `grind`.

doc/dev/ffi.md

@@ -49,8 +49,9 @@ In the case of `@[extern]` all *irrelevant* types are removed first; see next se
   is represented by the representation of that parameter's type.
 
   For example, `{ x : α // p }`, the `Subtype` structure of a value of type `α` and an irrelevant proof, is represented by the representation of `α`.
-* `Nat` is represented by `lean_object *`.
-  Its runtime value is either a pointer to an opaque bignum object or, if the lowest bit of the "pointer" is 1 (`lean_is_scalar`), an encoded unboxed natural number (`lean_box`/`lean_unbox`).
+  Similarly, the signed integer types `Int8`, ..., `Int64`, `ISize` are also represented by the unsigned C types `uint8_t`, ..., `uint64_t`, `size_t`, respectively, because they have a trivial structure.
+* `Nat` and `Int` are represented by `lean_object *`.
+  Their runtime values is either a pointer to an opaque bignum object or, if the lowest bit of the "pointer" is 1 (`lean_is_scalar`), an encoded unboxed natural number or integer (`lean_box`/`lean_unbox`).
 * A universe `Sort u`, type constructor `... → Sort u`, or proposition `p : Prop` is *irrelevant* and is either statically erased (see above) or represented as a `lean_object *` with the runtime value `lean_box(0)`
 * Any other type is represented by `lean_object *`.
   Its runtime value is a pointer to an object of a subtype of `lean_object` (see the "Inductive types" section below) or the unboxed value `lean_box(cidx)` for the `cidx`th constructor of an inductive type if this constructor does not have any relevant parameters.

doc/dev/release_checklist.md

@@ -37,16 +37,32 @@ We'll use `v4.6.0` as the intended release version as a running example.
     - Create the tag `v4.6.0` from `master`/`main` and push it.
     - Merge the tag `v4.6.0` into the `stable` branch and push it.
   - We do this for the repositories:
-    - [lean4checker](https://github.com/leanprover/lean4checker)
-      - No dependencies
-      - Toolchain bump PR
-      - Create and push the tag
-      - Merge the tag into `stable`
     - [Batteries](https://github.com/leanprover-community/batteries)
       - No dependencies
       - Toolchain bump PR
       - Create and push the tag
       - Merge the tag into `stable`
+    - [lean4checker](https://github.com/leanprover/lean4checker)
+      - No dependencies
+      - Toolchain bump PR
+      - Create and push the tag
+      - Merge the tag into `stable`
+    - [doc-gen4](https://github.com/leanprover/doc-gen4)
+      - Dependencies: exist, but they're not part of the release workflow
+      - Toolchain bump PR including updated Lake manifest
+      - Create and push the tag
+      - There is no `stable` branch; skip this step
+    - [Verso](https://github.com/leanprover/verso)
+      - Dependencies: exist, but they're not part of the release workflow
+      - The `SubVerso` dependency should be compatible with _every_ Lean release simultaneously, rather than following this workflow
+      - Toolchain bump PR including updated Lake manifest
+      - Create and push the tag
+      - There is no `stable` branch; skip this step
+    - [Cli](https://github.com/leanprover/lean4-cli)
+      - No dependencies
+      - Toolchain bump PR
+      - Create and push the tag
+      - There is no `stable` branch; skip this step
     - [ProofWidgets4](https://github.com/leanprover-community/ProofWidgets4)
       - Dependencies: `Batteries`
       - Note on versions and branches:
@@ -61,17 +77,6 @@ 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`
-    - [doc-gen4](https://github.com/leanprover/doc-gen4)
-      - Dependencies: exist, but they're not part of the release workflow
-      - Toolchain bump PR including updated Lake manifest
-      - Create and push the tag
-      - There is no `stable` branch; skip this step
-    - [Verso](https://github.com/leanprover/verso)
-      - Dependencies: exist, but they're not part of the release workflow
-      - The `SubVerso` dependency should be compatible with _every_ Lean release simultaneously, rather than following this workflow
-      - Toolchain bump PR including updated Lake manifest
-      - Create and push the tag
-      - There is no `stable` branch; skip this step
     - [import-graph](https://github.com/leanprover-community/import-graph)
       - Toolchain bump PR including updated Lake manifest
       - Create and push the tag
@@ -97,6 +102,7 @@ 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`
+- Run `scripts/release_checklist.py v4.6.0` to check that everything is in order.
 - 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`

script/prepare-llvm-linux.sh

@@ -63,8 +63,8 @@ else
 fi
 # use `-nostdinc` to make sure headers are not visible by default (in particular, not to `#include_next` in the clang headers),
 # but do not change sysroot so users can still link against system libs
-echo -n " -DLEANC_INTERNAL_FLAGS='-nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang"
-echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a ROOT/lib/glibc/libpthread_nonshared.a -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'"
+echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang"
+echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a ROOT/lib/glibc/libpthread_nonshared.a -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'"
 # when not using the above flags, link GMP dynamically/as usual
 echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-Wl,--as-needed -lgmp -luv -lpthread -ldl -lrt -Wl,--no-as-needed'"
 # do not set `LEAN_CC` for tests

script/prepare-llvm-macos.sh

@@ -48,12 +48,11 @@ if [[ -L llvm-host ]]; then
   echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang"
   gcp $GMP/lib/libgmp.a stage1/lib/
   gcp $LIBUV/lib/libuv.a stage1/lib/
-  echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/libc -fuse-ld=lld'"
   echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp -luv'"
 else
   echo -n " -DCMAKE_C_COMPILER=$PWD/llvm-host/bin/clang -DLEANC_OPTS='--sysroot $PWD/stage1 -resource-dir $PWD/stage1/lib/clang/15.0.1 ${EXTRA_FLAGS:-}'"
-  echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/libc -fuse-ld=lld'"
 fi
-echo -n " -DLEANC_INTERNAL_FLAGS='-nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang"
+echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang"
+echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -L ROOT/lib/libc -fuse-ld=lld'"
 # do not set `LEAN_CC` for tests
 echo -n " -DLEAN_TEST_VARS=''"

script/prepare-llvm-mingw.sh

@@ -43,7 +43,7 @@ echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang.exe -DCMAKE_C_COMPILER_WORKS=
 echo -n " -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_CXX_COMPILER=clang++"
 echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm -idirafter /clang64/include/'"
 echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang.exe"
-echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -static-libgcc -Wl,-Bstatic -lgmp $(pkg-config --static --libs libuv) -lunwind -Wl,-Bdynamic -fuse-ld=lld'"
+echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -Wl,-Bstatic -lgmp $(pkg-config --static --libs libuv) -lunwind -Wl,-Bdynamic -fuse-ld=lld'"
 # when not using the above flags, link GMP dynamically/as usual. Always link ICU dynamically.
 echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp $(pkg-config --libs libuv) -lucrtbase'"
 # do not set `LEAN_CC` for tests

script/release_checklist.py

@@ -0,0 +1,132 @@
+#!/usr/bin/env python3
+
+import argparse
+import yaml
+import requests
+import base64
+import subprocess
+import sys
+import os
+
+def parse_repos_config(file_path):
+    with open(file_path, "r") as f:
+        return yaml.safe_load(f)["repositories"]
+
+def get_github_token():
+    try:
+        import subprocess
+        result = subprocess.run(['gh', 'auth', 'token'], capture_output=True, text=True)
+        if result.returncode == 0:
+            return result.stdout.strip()
+    except FileNotFoundError:
+        print("Warning: 'gh' CLI not found. Some API calls may be rate-limited.")
+    return None
+
+def get_branch_content(repo_url, branch, file_path, github_token):
+    api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + f"/contents/{file_path}?ref={branch}"
+    headers = {'Authorization': f'token {github_token}'} if github_token else {}
+    response = requests.get(api_url, headers=headers)
+    if response.status_code == 200:
+        content = response.json().get("content", "")
+        content = content.replace("\n", "")
+        try:
+            return base64.b64decode(content).decode('utf-8').strip()
+        except Exception:
+            return None
+    return None
+
+def tag_exists(repo_url, tag_name, github_token):
+    api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + f"/git/refs/tags/{tag_name}"
+    headers = {'Authorization': f'token {github_token}'} if github_token else {}
+    response = requests.get(api_url, headers=headers)
+    return response.status_code == 200
+
+def is_merged_into_stable(repo_url, tag_name, stable_branch, github_token):
+    # First get the commit SHA for the tag
+    api_base = repo_url.replace("https://github.com/", "https://api.github.com/repos/")
+    headers = {'Authorization': f'token {github_token}'} if github_token else {}
+
+    # Get tag's commit SHA
+    tag_response = requests.get(f"{api_base}/git/refs/tags/{tag_name}", headers=headers)
+    if tag_response.status_code != 200:
+        return False
+    tag_sha = tag_response.json()['object']['sha']
+
+    # Get commits on stable branch containing this SHA
+    commits_response = requests.get(
+        f"{api_base}/commits?sha={stable_branch}&per_page=100",
+        headers=headers
+    )
+    if commits_response.status_code != 200:
+        return False
+
+    # Check if any commit in stable's history matches our tag's SHA
+    stable_commits = [commit['sha'] for commit in commits_response.json()]
+    return tag_sha in stable_commits
+
+def parse_version(version_str):
+    # Remove 'v' prefix and split into components
+    # Handle Lean toolchain format (leanprover/lean4:v4.x.y)
+    if ':' in version_str:
+        version_str = version_str.split(':')[1]
+    version = version_str.lstrip('v')
+    # Handle release candidates by removing -rc part for comparison
+    version = version.split('-')[0]
+    return tuple(map(int, version.split('.')))
+
+def is_version_gte(version1, version2):
+    """Check if version1 >= version2"""
+    return parse_version(version1) >= parse_version(version2)
+
+def is_release_candidate(version):
+    return "-rc" in version
+
+def main():
+    github_token = get_github_token()
+
+    if len(sys.argv) != 2:
+        print("Usage: python3 release_checklist.py <toolchain>")
+        sys.exit(1)
+
+    toolchain = sys.argv[1]
+
+    with open(os.path.join(os.path.dirname(__file__), "release_repos.yml")) as f:
+        repos = yaml.safe_load(f)["repositories"]
+
+    for repo in repos:
+        name = repo["name"]
+        url = repo["url"]
+        branch = repo["branch"]
+        check_stable = repo["stable-branch"]
+        check_tag = repo.get("toolchain-tag", True)
+
+        print(f"\nRepository: {name}")
+
+        # Check if branch is on at least the target toolchain
+        lean_toolchain_content = get_branch_content(url, branch, "lean-toolchain", github_token)
+        if lean_toolchain_content is None:
+            print(f"  ❌ No lean-toolchain file found in {branch} branch")
+            continue
+
+        on_target_toolchain = is_version_gte(lean_toolchain_content.strip(), toolchain)
+        if not on_target_toolchain:
+            print(f"  ❌ Not on target toolchain (needs ≥ {toolchain}, but {branch} is on {lean_toolchain_content.strip()})")
+            continue
+        print(f"  ✅ On compatible toolchain (>= {toolchain})")
+
+        # Only check for tag if toolchain-tag is true
+        if check_tag:
+            if not tag_exists(url, toolchain, github_token):
+                print(f"  ❌ Tag {toolchain} does not exist")
+                continue
+            print(f"  ✅ Tag {toolchain} exists")
+
+        # Only check merging into stable if stable-branch is true and not a release candidate
+        if check_stable and not is_release_candidate(toolchain):
+            if not is_merged_into_stable(url, toolchain, "stable", github_token):
+                print(f"  ❌ Tag {toolchain} is not merged into stable")
+                continue
+            print(f"  ✅ Tag {toolchain} is merged into stable")
+
+if __name__ == "__main__":
+    main()

script/release_repos.yml

@@ -0,0 +1,86 @@
+repositories:
+  - name: Batteries
+    url: https://github.com/leanprover-community/batteries
+    toolchain-tag: true
+    stable-branch: true
+    branch: main
+    dependencies: []
+
+  - name: lean4checker
+    url: https://github.com/leanprover/lean4checker
+    toolchain-tag: true
+    stable-branch: true
+    branch: master
+    dependencies: []
+
+  - name: doc-gen4
+    url: https://github.com/leanprover/doc-gen4
+    toolchain-tag: true
+    stable-branch: false
+    branch: main
+    dependencies: []
+
+  - name: Verso
+    url: https://github.com/leanprover/verso
+    toolchain-tag: true
+    stable-branch: false
+    branch: main
+    dependencies: []
+
+  - name: Cli
+    url: https://github.com/leanprover/lean4-cli
+    toolchain-tag: true
+    stable-branch: false
+    branch: main
+    dependencies: []
+
+  - name: ProofWidgets4
+    url: https://github.com/leanprover-community/ProofWidgets4
+    toolchain-tag: false
+    stable-branch: false
+    branch: main
+    dependencies:
+      - Batteries
+
+  - name: Aesop
+    url: https://github.com/leanprover-community/aesop
+    toolchain-tag: true
+    stable-branch: true
+    branch: master
+    dependencies:
+      - Batteries
+
+  - name: import-graph
+    url: https://github.com/leanprover-community/import-graph
+    toolchain-tag: true
+    stable-branch: false
+    branch: main
+    dependencies: []
+
+  - name: plausible
+    url: https://github.com/leanprover-community/plausible
+    toolchain-tag: true
+    stable-branch: false
+    branch: main
+    dependencies: []
+
+  - name: Mathlib
+    url: https://github.com/leanprover-community/mathlib4
+    toolchain-tag: true
+    stable-branch: true
+    branch: master
+    dependencies:
+      - Aesop
+      - ProofWidgets4
+      - lean4checker
+      - Batteries
+      - doc-gen4
+      - import-graph
+
+  - name: REPL
+    url: https://github.com/leanprover-community/repl
+    toolchain-tag: true
+    stable-branch: true
+    branch: master
+    dependencies:
+      - Mathlib

src/Init/Conv.lean

@@ -150,6 +150,10 @@ See the `simp` tactic for more information. -/
 syntax (name := simp) "simp" optConfig (discharger)? (&" only")?
   (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*) "]")? : conv
 
+/-- `simp?` takes the same arguments as `simp`, but reports an equivalent call to `simp only`
+that would be sufficient to close the goal. See the `simp?` tactic for more information. -/
+syntax (name := simpTrace) "simp?" optConfig (discharger)? (&" only")? (simpArgs)? : conv
+
 /--
 `dsimp` is the definitional simplifier in `conv`-mode. It differs from `simp` in that it only
 applies theorems that hold by reflexivity.
@@ -167,6 +171,9 @@ example (a : Nat): (0 + 0) = a - a := by
 syntax (name := dsimp) "dsimp" optConfig (discharger)? (&" only")?
   (" [" withoutPosition((simpErase <|> simpLemma),*) "]")? : conv
 
+@[inherit_doc simpTrace]
+syntax (name := dsimpTrace) "dsimp?" optConfig (&" only")? (dsimpArgs)? : conv
+
 /-- `simp_match` simplifies match expressions. For example,
 ```
 match [a, b] with

src/Init/Data/Array/Basic.lean

@@ -244,8 +244,7 @@ def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
 def range (n : Nat) : Array Nat :=
   ofFn fun (i : Fin n) => i
 
-def singleton (v : α) : Array α :=
-  mkArray 1 v
+@[inline] protected def singleton (v : α) : Array α := #[v]
 
 def back! [Inhabited α] (a : Array α) : α :=
   a[a.size - 1]!

src/Init/Data/BitVec/Lemmas.lean

@@ -9,7 +9,9 @@ import Init.Data.Bool
 import Init.Data.BitVec.Basic
 import Init.Data.Fin.Lemmas
 import Init.Data.Nat.Lemmas
+import Init.Data.Nat.Div.Lemmas
 import Init.Data.Nat.Mod
+import Init.Data.Nat.Div.Lemmas
 import Init.Data.Int.Bitwise.Lemmas
 import Init.Data.Int.Pow
 
@@ -98,6 +100,12 @@ theorem ofFin_eq_ofNat : @BitVec.ofFin w (Fin.mk x lt) = BitVec.ofNat w x := by
 theorem eq_of_toNat_eq {n} : ∀ {x y : BitVec n}, x.toNat = y.toNat → x = y
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 
+/-- Prove nonequality of bitvectors in terms of nat operations. -/
+theorem toNat_ne_iff_ne {n} {x y : BitVec n} : x.toNat ≠ y.toNat ↔ x ≠ y := by
+  constructor
+  · rintro h rfl; apply h rfl
+  · intro h h_eq; apply h <| eq_of_toNat_eq h_eq
+
 @[simp] theorem val_toFin (x : BitVec w) : x.toFin.val = x.toNat := rfl
 
 @[bv_toNat] theorem toNat_eq {x y : BitVec n} : x = y ↔ x.toNat = y.toNat :=
@@ -442,6 +450,10 @@ theorem toInt_eq_toNat_cond (x : BitVec n) :
         (x.toNat : Int) - (2^n : Nat) :=
   rfl
 
+theorem toInt_eq_toNat_of_lt {x : BitVec n} (h : 2 * x.toNat < 2^n) :
+    x.toInt = x.toNat := by
+  simp [toInt_eq_toNat_cond, h]
+
 theorem msb_eq_false_iff_two_mul_lt {x : BitVec w} : x.msb = false ↔ 2 * x.toNat < 2^w := by
   cases w <;> simp [Nat.pow_succ, Nat.mul_comm _ 2, msb_eq_decide, toNat_of_zero_length]
 
@@ -454,6 +466,9 @@ theorem toInt_eq_msb_cond (x : BitVec w) :
   simp only [BitVec.toInt, ← msb_eq_false_iff_two_mul_lt]
   cases x.msb <;> rfl
 
+theorem toInt_eq_toNat_of_msb {x : BitVec w} (h : x.msb = false) :
+    x.toInt = x.toNat := by
+  simp [toInt_eq_msb_cond, h]
 
 theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n) := by
   simp only [toInt_eq_toNat_cond]
@@ -785,6 +800,19 @@ theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h
   unfold allOnes
   simp
 
+@[simp] theorem toInt_allOnes : (allOnes w).toInt = if 0 < w then -1 else 0 := by
+  norm_cast
+  by_cases h : w = 0
+  · subst h
+    simp
+  · have : 1 < 2 ^ w := by simp [h]
+    simp [BitVec.toInt]
+    omega
+
+@[simp] theorem toFin_allOnes : (allOnes w).toFin = Fin.ofNat' (2^w) (2^w - 1) := by
+  ext
+  simp
+
 @[simp] theorem getLsbD_allOnes : (allOnes v).getLsbD i = decide (i < v) := by
   simp [allOnes]
 
@@ -1142,11 +1170,16 @@ theorem getMsb_not {x : BitVec w} :
 /-! ### shiftLeft -/
 
 @[simp, bv_toNat] theorem toNat_shiftLeft {x : BitVec v} :
-    BitVec.toNat (x <<< n) = BitVec.toNat x <<< n % 2^v :=
+    (x <<< n).toNat = x.toNat <<< n % 2^v :=
   BitVec.toNat_ofNat _ _
 
+@[simp] theorem toInt_shiftLeft {x : BitVec w} :
+    (x <<< n).toInt = (x.toNat <<< n : Int).bmod (2^w) := by
+  rw [toInt_eq_toNat_bmod, toNat_shiftLeft, Nat.shiftLeft_eq]
+  simp
+
 @[simp] theorem toFin_shiftLeft {n : Nat} (x : BitVec w) :
-    BitVec.toFin (x <<< n) = Fin.ofNat' (2^w) (x.toNat <<< n) := rfl
+    (x <<< n).toFin = Fin.ofNat' (2^w) (x.toNat <<< n) := rfl
 
 @[simp]
 theorem shiftLeft_zero (x : BitVec w) : x <<< 0 = x := by
@@ -2282,6 +2315,12 @@ theorem ofNat_sub_ofNat {n} (x y : Nat) : BitVec.ofNat n x - BitVec.ofNat n y =
 @[simp, bv_toNat] theorem toNat_neg (x : BitVec n) : (- x).toNat = (2^n - x.toNat) % 2^n := by
   simp [Neg.neg, BitVec.neg]
 
+theorem toNat_neg_of_pos {x : BitVec n} (h : 0#n < x) :
+    (- x).toNat = 2^n - x.toNat := by
+  change 0 < x.toNat at h
+  rw [toNat_neg, Nat.mod_eq_of_lt]
+  omega
+
 theorem toInt_neg {x : BitVec w} :
     (-x).toInt = (-x.toInt).bmod (2 ^ w) := by
   rw [← BitVec.zero_sub, toInt_sub]
@@ -2377,6 +2416,54 @@ theorem not_neg (x : BitVec w) : ~~~(-x) = x + -1#w := by
         show (_ - x.toNat) % _ = _ by rw [Nat.mod_eq_of_lt (by omega)]]
       omega
 
+/-! ### fill -/
+
+@[simp]
+theorem getLsbD_fill {w i : Nat} {v : Bool} :
+    (fill w v).getLsbD i = (v && decide (i < w)) := by
+  by_cases h : v
+  <;> simp [h, BitVec.fill, BitVec.negOne_eq_allOnes]
+
+@[simp]
+theorem getMsbD_fill {w i : Nat} {v : Bool} :
+    (fill w v).getMsbD i = (v && decide (i < w)) := by
+  by_cases h : v
+  <;> simp [h, BitVec.fill, BitVec.negOne_eq_allOnes]
+
+@[simp]
+theorem getElem_fill {w i : Nat} {v : Bool} (h : i < w) :
+    (fill w v)[i] = v := by
+  by_cases h : v
+  <;> simp [h, BitVec.fill, BitVec.negOne_eq_allOnes]
+
+@[simp]
+theorem msb_fill {w : Nat} {v : Bool} :
+    (fill w v).msb = (v && decide (0 < w)) := by
+  simp [BitVec.msb]
+
+theorem fill_eq {w : Nat} {v : Bool} : fill w v = if v = true then allOnes w else 0#w := by
+  by_cases h : v <;> (simp only [h] ; ext ; simp)
+
+@[simp]
+theorem fill_true {w : Nat} : fill w true = allOnes w := by
+  simp [fill_eq]
+
+@[simp]
+theorem fill_false {w : Nat} : fill w false = 0#w := by
+  simp [fill_eq]
+
+@[simp] theorem fill_toNat {w : Nat} {v : Bool} :
+    (fill w v).toNat = if v = true then 2^w - 1 else 0 := by
+  by_cases h : v <;> simp [h]
+
+@[simp] theorem fill_toInt {w : Nat} {v : Bool} :
+    (fill w v).toInt = if v = true && 0 < w then -1 else 0 := by
+  by_cases h : v <;> simp [h]
+
+@[simp] theorem fill_toFin {w : Nat} {v : Bool} :
+    (fill w v).toFin = if v = true then (allOnes w).toFin else Fin.ofNat' (2 ^ w) 0 := by
+  by_cases h : v <;> simp [h]
+
 /-! ### mul -/
 
 theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := by rfl
@@ -2520,13 +2607,13 @@ theorem udiv_def {x y : BitVec n} : x / y = BitVec.ofNat n (x.toNat / y.toNat) :
   rw [← udiv_eq]
   simp [udiv, bv_toNat, h, Nat.mod_eq_of_lt]
 
+@[simp]
+theorem toFin_udiv {x y : BitVec n} : (x / y).toFin = x.toFin / y.toFin := by
+  rfl
+
 @[simp, bv_toNat]
 theorem toNat_udiv {x y : BitVec n} : (x / y).toNat = x.toNat / y.toNat := by
-  rw [udiv_def]
-  by_cases h : y = 0
-  · simp [h]
-  · rw [toNat_ofNat, Nat.mod_eq_of_lt]
-    exact Nat.lt_of_le_of_lt (Nat.div_le_self ..) (by omega)
+  rfl
 
 @[simp]
 theorem zero_udiv {x : BitVec w} : (0#w) / x = 0#w := by
@@ -2562,6 +2649,45 @@ theorem udiv_self {x : BitVec w} :
       ↓reduceIte, toNat_udiv]
     rw [Nat.div_self (by omega), Nat.mod_eq_of_lt (by omega)]
 
+theorem msb_udiv (x y : BitVec w) :
+    (x / y).msb = (x.msb && y == 1#w) := by
+  cases msb_x : x.msb
+  · suffices x.toNat / y.toNat < 2 ^ (w - 1) by simpa [msb_eq_decide]
+    calc
+      x.toNat / y.toNat ≤ x.toNat     := by apply Nat.div_le_self
+                      _ < 2 ^ (w - 1) := by simpa [msb_eq_decide] using msb_x
+  . rcases w with _|w
+    · contradiction
+    · have : (y == 1#_) = decide (y.toNat = 1) := by
+        simp [(· == ·), toNat_eq]
+      simp only [this, Bool.true_and]
+      match hy : y.toNat with
+      | 0 =>
+        obtain rfl : y = 0#_ := eq_of_toNat_eq hy
+        simp
+      | 1 =>
+        obtain rfl : y = 1#_ := eq_of_toNat_eq (by simp [hy])
+        simpa using msb_x
+      | y + 2 =>
+        suffices x.toNat / (y + 2) < 2 ^ w by
+          simp_all [msb_eq_decide, hy]
+        calc
+          x.toNat / (y + 2)
+            ≤ x.toNat / 2 := by apply Nat.div_add_le_right (by omega)
+          _ < 2 ^ w       := by omega
+
+theorem msb_udiv_eq_false_of {x : BitVec w} (h : x.msb = false) (y : BitVec w) :
+    (x / y).msb = false := by
+  simp [msb_udiv, h]
+
+/--
+If `x` is nonnegative (i.e., does not have its msb set),
+then `x / y` is nonnegative, thus `toInt` and `toNat` coincide.
+-/
+theorem toInt_udiv_of_msb {x : BitVec w} (h : x.msb = false) (y : BitVec w) :
+    (x / y).toInt = x.toNat / y.toNat := by
+  simp [toInt_eq_msb_cond, msb_udiv_eq_false_of h]
+
 /-! ### umod -/
 
 theorem umod_def {x y : BitVec n} :
@@ -2574,6 +2700,10 @@ theorem umod_def {x y : BitVec n} :
 theorem toNat_umod {x y : BitVec n} :
     (x % y).toNat = x.toNat % y.toNat := rfl
 
+@[simp]
+theorem toFin_umod {x y : BitVec w} :
+    (x % y).toFin = x.toFin % y.toFin := rfl
+
 @[simp]
 theorem umod_zero {x : BitVec n} : x % 0#n = x := by
   simp [umod_def]
@@ -2601,6 +2731,55 @@ theorem umod_eq_and {x y : BitVec 1} : x % y = x &&& (~~~y) := by
     rcases hy with rfl | rfl <;>
       rfl
 
+theorem umod_eq_of_lt {x y : BitVec w} (h : x < y) :
+    x % y = x := by
+  apply eq_of_toNat_eq
+  simp [Nat.mod_eq_of_lt h]
+
+@[simp]
+theorem msb_umod {x y : BitVec w} :
+    (x % y).msb = (x.msb && (x < y || y == 0#w)) := by
+  rw [msb_eq_decide, toNat_umod]
+  cases msb_x : x.msb
+  · suffices x.toNat % y.toNat < 2 ^ (w - 1) by simpa
+    calc
+      x.toNat % y.toNat ≤ x.toNat     := by apply Nat.mod_le
+                      _ < 2 ^ (w - 1) := by simpa [msb_eq_decide] using msb_x
+  . by_cases hy : y = 0
+    · simp_all [msb_eq_decide]
+    · suffices 2 ^ (w - 1) ≤ x.toNat % y.toNat ↔ x < y by simp_all
+      by_cases x_lt_y : x < y
+      . simp_all [Nat.mod_eq_of_lt x_lt_y, msb_eq_decide]
+      · suffices x.toNat % y.toNat < 2 ^ (w - 1) by
+          simpa [x_lt_y]
+        have y_le_x : y.toNat ≤ x.toNat := by
+          simpa using x_lt_y
+        replace hy : y.toNat ≠ 0 :=
+          toNat_ne_iff_ne.mpr hy
+        by_cases msb_y : y.toNat < 2 ^ (w - 1)
+        · have : x.toNat % y.toNat < y.toNat := Nat.mod_lt _ (by omega)
+          omega
+        · rcases w with _|w
+          · contradiction
+          simp only [Nat.add_one_sub_one]
+          replace msb_y : 2 ^ w ≤ y.toNat := by
+            simpa using msb_y
+          have : y.toNat ≤ y.toNat * (x.toNat / y.toNat) := by
+              apply Nat.le_mul_of_pos_right
+              apply Nat.div_pos y_le_x
+              omega
+          have : x.toNat % y.toNat ≤ x.toNat - y.toNat := by
+            rw [Nat.mod_eq_sub]; omega
+          omega
+
+theorem toInt_umod {x y : BitVec w} :
+    (x % y).toInt = (x.toNat % y.toNat : Int).bmod (2 ^ w) := by
+  simp [toInt_eq_toNat_bmod]
+
+theorem toInt_umod_of_msb {x y : BitVec w} (h : x.msb = false) :
+    (x % y).toInt = x.toInt % y.toNat := by
+  simp [toInt_eq_msb_cond, h]
+
 /-! ### smtUDiv -/
 
 theorem smtUDiv_eq (x y : BitVec w) : smtUDiv x y = if y = 0#w then allOnes w else x / y := by
@@ -2757,7 +2936,12 @@ theorem smod_zero {x : BitVec n} : x.smod 0#n = x := by
 
 /-! # Rotate Left -/
 
-/-- rotateLeft is invariant under `mod` by the bitwidth. -/
+/--`rotateLeft` is defined in terms of left and right shifts. -/
+theorem rotateLeft_def {x : BitVec w} {r : Nat} :
+    x.rotateLeft r = (x <<< (r % w)) ||| (x >>> (w - r % w)) := by
+  simp only [rotateLeft, rotateLeftAux]
+
+/-- `rotateLeft` is invariant under `mod` by the bitwidth. -/
 @[simp]
 theorem rotateLeft_mod_eq_rotateLeft {x : BitVec w} {r : Nat} :
     x.rotateLeft (r % w) = x.rotateLeft r := by
@@ -2901,8 +3085,18 @@ theorem msb_rotateLeft {m w : Nat} {x : BitVec w} :
   · simp
     omega
 
+@[simp]
+theorem toNat_rotateLeft {x : BitVec w} {r : Nat} :
+    (x.rotateLeft r).toNat = (x.toNat <<< (r % w)) % (2^w) ||| x.toNat >>> (w - r % w) := by
+  simp only [rotateLeft_def, toNat_shiftLeft, toNat_ushiftRight, toNat_or]
+
 /-! ## Rotate Right -/
 
+/-- `rotateRight` is defined in terms of left and right shifts. -/
+theorem rotateRight_def {x : BitVec w} {r : Nat} :
+    x.rotateRight r = (x >>> (r % w)) ||| (x <<< (w - r % w)) := by
+  simp only [rotateRight, rotateRightAux]
+
 /--
 Accessing bits in `x.rotateRight r` the range `[0, w-r)` is equal to
 accessing bits `x` in the range `[r, w)`.
@@ -3038,6 +3232,11 @@ theorem msb_rotateRight {r w : Nat} {x : BitVec w} :
     simp [h₁]
   · simp [show w = 0 by omega]
 
+@[simp]
+theorem toNat_rotateRight {x : BitVec w} {r : Nat} :
+    (x.rotateRight r).toNat = (x.toNat >>> (r % w)) ||| x.toNat <<< (w - r % w) % (2^w) := by
+  simp only [rotateRight_def, toNat_shiftLeft, toNat_ushiftRight, toNat_or]
+
 /- ## twoPow -/
 
 theorem twoPow_eq (w : Nat) (i : Nat) : twoPow w i = 1#w <<< i := by

src/Init/Data/Int/DivModLemmas.lean

@@ -534,6 +534,13 @@ theorem mul_emod (a b n : Int) : (a * b) % n = (a % n) * (b % n) % n := by
 @[simp] theorem emod_emod (a b : Int) : (a % b) % b = a % b := by
   conv => rhs; rw [← emod_add_ediv a b, add_mul_emod_self_left]
 
+@[simp] theorem emod_sub_emod (m n k : Int) : (m % n - k) % n = (m - k) % n :=
+  Int.emod_add_emod m n (-k)
+
+@[simp] theorem sub_emod_emod (m n k : Int) : (m - n % k) % k = (m - n) % k := by
+  apply (emod_add_cancel_right (n % k)).mp
+  rw [Int.sub_add_cancel, Int.add_emod_emod, Int.sub_add_cancel]
+
 theorem sub_emod (a b n : Int) : (a - b) % n = (a % n - b % n) % n := by
   apply (emod_add_cancel_right b).mp
   rw [Int.sub_add_cancel, ← Int.add_emod_emod, Int.sub_add_cancel, emod_emod]

src/Init/Data/List/Lemmas.lean

@@ -1,7 +1,8 @@
 /-
 Copyright (c) 2014 Parikshit Khanna. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
+Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro,
+  Kim Morrison
 -/
 prelude
 import Init.Data.Bool
@@ -757,207 +758,6 @@ theorem length_eq_of_beq [BEq α] {l₁ l₂ : List α} (h : l₁ == l₂) : l
     | nil => simp
     | cons b l₂ => simp [isEqv, ih]
 
-/-! ### foldlM and foldrM -/
-
-@[simp] theorem foldlM_reverse [Monad m] (l : List α) (f : β → α → m β) (b) :
-    l.reverse.foldlM f b = l.foldrM (fun x y => f y x) b := rfl
-
-@[simp] theorem foldlM_append [Monad m] [LawfulMonad m] (f : β → α → m β) (b) (l l' : List α) :
-    (l ++ l').foldlM f b = l.foldlM f b >>= l'.foldlM f := by
-  induction l generalizing b <;> simp [*]
-
-@[simp] theorem foldrM_cons [Monad m] [LawfulMonad m] (a : α) (l) (f : α → β → m β) (b) :
-    (a :: l).foldrM f b = l.foldrM f b >>= f a := by
-  simp only [foldrM]
-  induction l <;> simp_all
-
-theorem foldl_eq_foldlM (f : β → α → β) (b) (l : List α) :
-    l.foldl f b = l.foldlM (m := Id) f b := by
-  induction l generalizing b <;> simp [*, foldl]
-
-theorem foldr_eq_foldrM (f : α → β → β) (b) (l : List α) :
-    l.foldr f b = l.foldrM (m := Id) f b := by
-  induction l <;> simp [*, foldr]
-
-@[simp] theorem id_run_foldlM (f : β → α → Id β) (b) (l : List α) :
-    Id.run (l.foldlM f b) = l.foldl f b := (foldl_eq_foldlM f b l).symm
-
-@[simp] theorem id_run_foldrM (f : α → β → Id β) (b) (l : List α) :
-    Id.run (l.foldrM f b) = l.foldr f b := (foldr_eq_foldrM f b l).symm
-
-/-! ### foldl and foldr -/
-
-@[simp] theorem foldr_cons_eq_append (l : List α) : l.foldr cons l' = l ++ l' := by
-  induction l <;> simp [*]
-
-@[deprecated foldr_cons_eq_append (since := "2024-08-22")] abbrev foldr_self_append := @foldr_cons_eq_append
-
-@[simp] theorem foldl_flip_cons_eq_append (l : List α) : l.foldl (fun x y => y :: x) l' = l.reverse ++ l' := by
-  induction l generalizing l' <;> simp [*]
-
-theorem foldr_cons_nil (l : List α) : l.foldr cons [] = l := by simp
-
-@[deprecated foldr_cons_nil (since := "2024-09-04")] abbrev foldr_self := @foldr_cons_nil
-
-theorem foldl_map (f : β₁ → β₂) (g : α → β₂ → α) (l : List β₁) (init : α) :
-    (l.map f).foldl g init = l.foldl (fun x y => g x (f y)) init := by
-  induction l generalizing init <;> simp [*]
-
-theorem foldr_map (f : α₁ → α₂) (g : α₂ → β → β) (l : List α₁) (init : β) :
-    (l.map f).foldr g init = l.foldr (fun x y => g (f x) y) init := by
-  induction l generalizing init <;> simp [*]
-
-theorem foldl_filterMap (f : α → Option β) (g : γ → β → γ) (l : List α) (init : γ) :
-    (l.filterMap f).foldl g init = l.foldl (fun x y => match f y with | some b => g x b | none => x) init := by
-  induction l generalizing init with
-  | nil => rfl
-  | cons a l ih =>
-    simp only [filterMap_cons, foldl_cons]
-    cases f a <;> simp [ih]
-
-theorem foldr_filterMap (f : α → Option β) (g : β → γ → γ) (l : List α) (init : γ) :
-    (l.filterMap f).foldr g init = l.foldr (fun x y => match f x with | some b => g b y | none => y) init := by
-  induction l generalizing init with
-  | nil => rfl
-  | cons a l ih =>
-    simp only [filterMap_cons, foldr_cons]
-    cases f a <;> simp [ih]
-
-theorem foldl_map' (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : List α)
-    (h : ∀ x y, f' (g x) (g y) = g (f x y)) :
-    (l.map g).foldl f' (g a) = g (l.foldl f a) := by
-  induction l generalizing a
-  · simp
-  · simp [*, h]
-
-theorem foldr_map' (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : List α)
-    (h : ∀ x y, f' (g x) (g y) = g (f x y)) :
-    (l.map g).foldr f' (g a) = g (l.foldr f a) := by
-  induction l generalizing a
-  · simp
-  · simp [*, h]
-
-theorem foldl_assoc {op : α → α → α} [ha : Std.Associative op] :
-    ∀ {l : List α} {a₁ a₂}, l.foldl op (op a₁ a₂) = op a₁ (l.foldl op a₂)
-  | [], a₁, a₂ => rfl
-  | a :: l, a₁, a₂ => by
-    simp only [foldl_cons, ha.assoc]
-    rw [foldl_assoc]
-
-theorem foldr_assoc {op : α → α → α} [ha : Std.Associative op] :
-    ∀ {l : List α} {a₁ a₂}, l.foldr op (op a₁ a₂) = op (l.foldr op a₁) a₂
-  | [], a₁, a₂ => rfl
-  | a :: l, a₁, a₂ => by
-    simp only [foldr_cons, ha.assoc]
-    rw [foldr_assoc]
-
-theorem foldl_hom (f : α₁ → α₂) (g₁ : α₁ → β → α₁) (g₂ : α₂ → β → α₂) (l : List β) (init : α₁)
-    (H : ∀ x y, g₂ (f x) y = f (g₁ x y)) : l.foldl g₂ (f init) = f (l.foldl g₁ init) := by
-  induction l generalizing init <;> simp [*, H]
-
-theorem foldr_hom (f : β₁ → β₂) (g₁ : α → β₁ → β₁) (g₂ : α → β₂ → β₂) (l : List α) (init : β₁)
-    (H : ∀ x y, g₂ x (f y) = f (g₁ x y)) : l.foldr g₂ (f init) = f (l.foldr g₁ init) := by
-  induction l <;> simp [*, H]
-
-/--
-Prove a proposition about the result of `List.foldl`,
-by proving it for the initial data,
-and the implication that the operation applied to any element of the list preserves the property.
-
-The motive can take values in `Sort _`, so this may be used to construct data,
-as well as to prove propositions.
--/
-def foldlRecOn {motive : β → Sort _} : ∀ (l : List α) (op : β → α → β) (b : β) (_ : motive b)
-    (_ : ∀ (b : β) (_ : motive b) (a : α) (_ : a ∈ l), motive (op b a)), motive (List.foldl op b l)
-  | [], _, _, hb, _ => hb
-  | hd :: tl, op, b, hb, hl =>
-    foldlRecOn tl op (op b hd) (hl b hb hd (mem_cons_self hd tl))
-      fun y hy x hx => hl y hy x (mem_cons_of_mem hd hx)
-
-@[simp] theorem foldlRecOn_nil {motive : β → Sort _} (hb : motive b)
-    (hl : ∀ (b : β) (_ : motive b) (a : α) (_ : a ∈ []), motive (op b a)) :
-    foldlRecOn [] op b hb hl = hb := rfl
-
-@[simp] theorem foldlRecOn_cons {motive : β → Sort _} (hb : motive b)
-    (hl : ∀ (b : β) (_ : motive b) (a : α) (_ : a ∈ x :: l), motive (op b a)) :
-    foldlRecOn (x :: l) op b hb hl =
-      foldlRecOn l op (op b x) (hl b hb x (mem_cons_self x l))
-        (fun b c a m => hl b c a (mem_cons_of_mem x m)) :=
-  rfl
-
-/--
-Prove a proposition about the result of `List.foldr`,
-by proving it for the initial data,
-and the implication that the operation applied to any element of the list preserves the property.
-
-The motive can take values in `Sort _`, so this may be used to construct data,
-as well as to prove propositions.
--/
-def foldrRecOn {motive : β → Sort _} : ∀ (l : List α) (op : α → β → β) (b : β) (_ : motive b)
-    (_ : ∀ (b : β) (_ : motive b) (a : α) (_ : a ∈ l), motive (op a b)), motive (List.foldr op b l)
-  | nil, _, _, hb, _ => hb
-  | x :: l, op, b, hb, hl =>
-    hl (foldr op b l)
-      (foldrRecOn l op b hb fun b c a m => hl b c a (mem_cons_of_mem x m)) x (mem_cons_self x l)
-
-@[simp] theorem foldrRecOn_nil {motive : β → Sort _} (hb : motive b)
-    (hl : ∀ (b : β) (_ : motive b) (a : α) (_ : a ∈ []), motive (op a b)) :
-    foldrRecOn [] op b hb hl = hb := rfl
-
-@[simp] theorem foldrRecOn_cons {motive : β → Sort _} (hb : motive b)
-    (hl : ∀ (b : β) (_ : motive b) (a : α) (_ : a ∈ x :: l), motive (op a b)) :
-    foldrRecOn (x :: l) op b hb hl =
-      hl _ (foldrRecOn l op b hb fun b c a m => hl b c a (mem_cons_of_mem x m))
-        x (mem_cons_self x l) :=
-  rfl
-
-/--
-We can prove that two folds over the same list are related (by some arbitrary relation)
-if we know that the initial elements are related and the folding function, for each element of the list,
-preserves the relation.
--/
-theorem foldl_rel {l : List α} {f g : β → α → β} {a b : β} (r : β → β → Prop)
-    (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)) :
-    r (l.foldl (fun acc a => f acc a) a) (l.foldl (fun acc a => g acc a) b) := by
-  induction l generalizing a b with
-  | nil => simp_all
-  | cons a l ih =>
-    simp only [foldl_cons]
-    apply ih
-    · simp_all
-    · exact fun a m c c' h => h' _ (by simp_all) _ _ h
-
-/--
-We can prove that two folds over the same list are related (by some arbitrary relation)
-if we know that the initial elements are related and the folding function, for each element of the list,
-preserves the relation.
--/
-theorem foldr_rel {l : List α} {f g : α → β → β} {a b : β} (r : β → β → Prop)
-    (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')) :
-    r (l.foldr (fun a acc => f a acc) a) (l.foldr (fun a acc => g a acc) b) := by
-  induction l generalizing a b with
-  | nil => simp_all
-  | cons a l ih =>
-    simp only [foldr_cons]
-    apply h'
-    · simp
-    · exact ih h fun a m c c' h => h' _ (by simp_all) _ _ h
-
-@[simp] theorem foldl_add_const (l : List α) (a b : Nat) :
-    l.foldl (fun x _ => x + a) b = b + a * l.length := by
-  induction l generalizing b with
-  | nil => simp
-  | cons y l ih =>
-    simp only [foldl_cons, ih, length_cons, Nat.mul_add, Nat.mul_one, Nat.add_assoc,
-      Nat.add_comm a]
-
-@[simp] theorem foldr_add_const (l : List α) (a b : Nat) :
-    l.foldr (fun _ x => x + a) b = b + a * l.length := by
-  induction l generalizing b with
-  | nil => simp
-  | cons y l ih =>
-    simp only [foldr_cons, ih, length_cons, Nat.mul_add, Nat.mul_one, Nat.add_assoc]
-
 /-! ### getLast -/
 
 theorem getLast_eq_getElem : ∀ (l : List α) (h : l ≠ []),
@@ -1216,27 +1016,6 @@ theorem getLast?_tail (l : List α) : (tail l).getLast? = if l.length = 1 then n
 
 /-! ### map -/
 
-@[simp] theorem map_id_fun : map (id : α → α) = id := by
-  funext l
-  induction l <;> simp_all
-
-/-- `map_id_fun'` differs from `map_id_fun` by representing the identity function as a lambda, rather than `id`. -/
-@[simp] theorem map_id_fun' : map (fun (a : α) => a) = id := map_id_fun
-
--- This is not a `@[simp]` lemma because `map_id_fun` will apply.
-theorem map_id (l : List α) : map (id : α → α) l = l := by
-  induction l <;> simp_all
-
-/-- `map_id'` differs from `map_id` by representing the identity function as a lambda, rather than `id`. -/
--- This is not a `@[simp]` lemma because `map_id_fun'` will apply.
-theorem map_id' (l : List α) : map (fun (a : α) => a) l = l := map_id l
-
-/-- Variant of `map_id`, with a side condition that the function is pointwise the identity. -/
-theorem map_id'' {f : α → α} (h : ∀ x, f x = x) (l : List α) : map f l = l := by
-  simp [show f = id from funext h]
-
-theorem map_singleton (f : α → β) (a : α) : map f [a] = [f a] := rfl
-
 @[simp] theorem length_map (as : List α) (f : α → β) : (as.map f).length = as.length := by
   induction as with
   | nil => simp [List.map]
@@ -1262,6 +1041,27 @@ theorem get_map (f : α → β) {l i} :
     get (map f l) i = f (get l ⟨i, length_map l f ▸ i.2⟩) := by
   simp
 
+@[simp] theorem map_id_fun : map (id : α → α) = id := by
+  funext l
+  induction l <;> simp_all
+
+/-- `map_id_fun'` differs from `map_id_fun` by representing the identity function as a lambda, rather than `id`. -/
+@[simp] theorem map_id_fun' : map (fun (a : α) => a) = id := map_id_fun
+
+-- This is not a `@[simp]` lemma because `map_id_fun` will apply.
+theorem map_id (l : List α) : map (id : α → α) l = l := by
+  induction l <;> simp_all
+
+/-- `map_id'` differs from `map_id` by representing the identity function as a lambda, rather than `id`. -/
+-- This is not a `@[simp]` lemma because `map_id_fun'` will apply.
+theorem map_id' (l : List α) : map (fun (a : α) => a) l = l := map_id l
+
+/-- Variant of `map_id`, with a side condition that the function is pointwise the identity. -/
+theorem map_id'' {f : α → α} (h : ∀ x, f x = x) (l : List α) : map f l = l := by
+  simp [show f = id from funext h]
+
+theorem map_singleton (f : α → β) (a : α) : map f [a] = [f a] := rfl
+
 @[simp] theorem mem_map {f : α → β} : ∀ {l : List α}, b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b
   | [] => by simp
   | _ :: l => by simp [mem_map (l := l), eq_comm (a := b)]
@@ -1315,6 +1115,10 @@ theorem map_eq_cons_iff' {f : α → β} {l : List α} :
 
 @[deprecated map_eq_cons' (since := "2024-09-05")] abbrev map_eq_cons' := @map_eq_cons_iff'
 
+@[simp] theorem map_eq_singleton_iff {f : α → β} {l : List α} {b : β} :
+    map f l = [b] ↔ ∃ a, l = [a] ∧ f a = b := by
+  simp [map_eq_cons_iff]
+
 theorem map_eq_map_iff : map f l = map g l ↔ ∀ a ∈ l, f a = g a := by
   induction l <;> simp
 
@@ -1481,7 +1285,7 @@ theorem map_filter_eq_foldr (f : α → β) (p : α → Bool) (as : List α) :
 @[simp] theorem filter_append {p : α → Bool} :
     ∀ (l₁ l₂ : List α), filter p (l₁ ++ l₂) = filter p l₁ ++ filter p l₂
   | [], _ => rfl
-  | a :: l₁, l₂ => by simp [filter]; split <;> simp [filter_append l₁]
+  | a :: l₁, l₂ => by simp only [cons_append, filter]; split <;> simp [filter_append l₁]
 
 theorem filter_eq_cons_iff {l} {a} {as} :
     filter p l = a :: as ↔
@@ -1961,16 +1765,6 @@ theorem set_append {s t : List α} :
     (s ++ t).set i x = s ++ t.set (i - s.length) x := by
   rw [set_append, if_neg (by simp_all)]
 
-@[simp] theorem foldrM_append [Monad m] [LawfulMonad m] (f : α → β → m β) (b) (l l' : List α) :
-    (l ++ l').foldrM f b = l'.foldrM f b >>= l.foldrM f := by
-  induction l <;> simp [*]
-
-@[simp] theorem foldl_append {β : Type _} (f : β → α → β) (b) (l l' : List α) :
-    (l ++ l').foldl f b = l'.foldl f (l.foldl f b) := by simp [foldl_eq_foldlM]
-
-@[simp] theorem foldr_append (f : α → β → β) (b) (l l' : List α) :
-    (l ++ l').foldr f b = l.foldr f (l'.foldr f b) := by simp [foldr_eq_foldrM]
-
 theorem filterMap_eq_append_iff {f : α → Option β} :
     filterMap f l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂ := by
   constructor
@@ -2119,14 +1913,6 @@ theorem head?_flatten {L : List (List α)} : (flatten L).head? = L.findSome? fun
 -- `getLast?_flatten` is proved later, after the `reverse` section.
 -- `head_flatten` and `getLast_flatten` are proved in `Init.Data.List.Find`.
 
-theorem foldl_flatten (f : β → α → β) (b : β) (L : List (List α)) :
-    (flatten L).foldl f b = L.foldl (fun b l => l.foldl f b) b := by
-  induction L generalizing b <;> simp_all
-
-theorem foldr_flatten (f : α → β → β) (b : β) (L : List (List α)) :
-    (flatten L).foldr f b = L.foldr (fun l b => l.foldr f b) b := by
-  induction L <;> simp_all
-
 @[simp] theorem map_flatten (f : α → β) (L : List (List α)) : map f (flatten L) = flatten (map (map f) L) := by
   induction L <;> simp_all
 
@@ -2699,10 +2485,114 @@ theorem flatMap_reverse {β} (l : List α) (f : α → List β) : (l.reverse.fla
 @[simp] theorem reverseAux_eq (as bs : List α) : reverseAux as bs = reverse as ++ bs :=
   reverseAux_eq_append ..
 
+@[simp] theorem reverse_replicate (n) (a : α) : reverse (replicate n a) = replicate n a :=
+  eq_replicate_iff.2
+    ⟨by rw [length_reverse, length_replicate],
+     fun _ h => eq_of_mem_replicate (mem_reverse.1 h)⟩
+
+
+/-! ### foldlM and foldrM -/
+
+@[simp] theorem foldlM_append [Monad m] [LawfulMonad m] (f : β → α → m β) (b) (l l' : List α) :
+    (l ++ l').foldlM f b = l.foldlM f b >>= l'.foldlM f := by
+  induction l generalizing b <;> simp [*]
+
+@[simp] theorem foldrM_cons [Monad m] [LawfulMonad m] (a : α) (l) (f : α → β → m β) (b) :
+    (a :: l).foldrM f b = l.foldrM f b >>= f a := by
+  simp only [foldrM]
+  induction l <;> simp_all
+
+theorem foldl_eq_foldlM (f : β → α → β) (b) (l : List α) :
+    l.foldl f b = l.foldlM (m := Id) f b := by
+  induction l generalizing b <;> simp [*, foldl]
+
+theorem foldr_eq_foldrM (f : α → β → β) (b) (l : List α) :
+    l.foldr f b = l.foldrM (m := Id) f b := by
+  induction l <;> simp [*, foldr]
+
+@[simp] theorem id_run_foldlM (f : β → α → Id β) (b) (l : List α) :
+    Id.run (l.foldlM f b) = l.foldl f b := (foldl_eq_foldlM f b l).symm
+
+@[simp] theorem id_run_foldrM (f : α → β → Id β) (b) (l : List α) :
+    Id.run (l.foldrM f b) = l.foldr f b := (foldr_eq_foldrM f b l).symm
+
+@[simp] theorem foldlM_reverse [Monad m] (l : List α) (f : β → α → m β) (b) :
+    l.reverse.foldlM f b = l.foldrM (fun x y => f y x) b := rfl
+
 @[simp] theorem foldrM_reverse [Monad m] (l : List α) (f : α → β → m β) (b) :
     l.reverse.foldrM f b = l.foldlM (fun x y => f y x) b :=
   (foldlM_reverse ..).symm.trans <| by simp
 
+/-! ### foldl and foldr -/
+
+@[simp] theorem foldr_cons_eq_append (l : List α) : l.foldr cons l' = l ++ l' := by
+  induction l <;> simp [*]
+
+@[deprecated foldr_cons_eq_append (since := "2024-08-22")] abbrev foldr_self_append := @foldr_cons_eq_append
+
+@[simp] theorem foldl_flip_cons_eq_append (l : List α) : l.foldl (fun x y => y :: x) l' = l.reverse ++ l' := by
+  induction l generalizing l' <;> simp [*]
+
+theorem foldr_cons_nil (l : List α) : l.foldr cons [] = l := by simp
+
+@[deprecated foldr_cons_nil (since := "2024-09-04")] abbrev foldr_self := @foldr_cons_nil
+
+theorem foldl_map (f : β₁ → β₂) (g : α → β₂ → α) (l : List β₁) (init : α) :
+    (l.map f).foldl g init = l.foldl (fun x y => g x (f y)) init := by
+  induction l generalizing init <;> simp [*]
+
+theorem foldr_map (f : α₁ → α₂) (g : α₂ → β → β) (l : List α₁) (init : β) :
+    (l.map f).foldr g init = l.foldr (fun x y => g (f x) y) init := by
+  induction l generalizing init <;> simp [*]
+
+theorem foldl_filterMap (f : α → Option β) (g : γ → β → γ) (l : List α) (init : γ) :
+    (l.filterMap f).foldl g init = l.foldl (fun x y => match f y with | some b => g x b | none => x) init := by
+  induction l generalizing init with
+  | nil => rfl
+  | cons a l ih =>
+    simp only [filterMap_cons, foldl_cons]
+    cases f a <;> simp [ih]
+
+theorem foldr_filterMap (f : α → Option β) (g : β → γ → γ) (l : List α) (init : γ) :
+    (l.filterMap f).foldr g init = l.foldr (fun x y => match f x with | some b => g b y | none => y) init := by
+  induction l generalizing init with
+  | nil => rfl
+  | cons a l ih =>
+    simp only [filterMap_cons, foldr_cons]
+    cases f a <;> simp [ih]
+
+theorem foldl_map' (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : List α)
+    (h : ∀ x y, f' (g x) (g y) = g (f x y)) :
+    (l.map g).foldl f' (g a) = g (l.foldl f a) := by
+  induction l generalizing a
+  · simp
+  · simp [*, h]
+
+theorem foldr_map' (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : List α)
+    (h : ∀ x y, f' (g x) (g y) = g (f x y)) :
+    (l.map g).foldr f' (g a) = g (l.foldr f a) := by
+  induction l generalizing a
+  · simp
+  · simp [*, h]
+
+@[simp] theorem foldrM_append [Monad m] [LawfulMonad m] (f : α → β → m β) (b) (l l' : List α) :
+    (l ++ l').foldrM f b = l'.foldrM f b >>= l.foldrM f := by
+  induction l <;> simp [*]
+
+@[simp] theorem foldl_append {β : Type _} (f : β → α → β) (b) (l l' : List α) :
+    (l ++ l').foldl f b = l'.foldl f (l.foldl f b) := by simp [foldl_eq_foldlM]
+
+@[simp] theorem foldr_append (f : α → β → β) (b) (l l' : List α) :
+    (l ++ l').foldr f b = l.foldr f (l'.foldr f b) := by simp [foldr_eq_foldrM]
+
+theorem foldl_flatten (f : β → α → β) (b : β) (L : List (List α)) :
+    (flatten L).foldl f b = L.foldl (fun b l => l.foldl f b) b := by
+  induction L generalizing b <;> simp_all
+
+theorem foldr_flatten (f : α → β → β) (b : β) (L : List (List α)) :
+    (flatten L).foldr f b = L.foldr (fun l b => l.foldr f b) b := by
+  induction L <;> simp_all
+
 @[simp] theorem foldl_reverse (l : List α) (f : β → α → β) (b) :
     l.reverse.foldl f b = l.foldr (fun x y => f y x) b := by simp [foldl_eq_foldlM, foldr_eq_foldrM]
 
@@ -2716,10 +2606,127 @@ theorem foldl_eq_foldr_reverse (l : List α) (f : β → α → β) (b) :
 theorem foldr_eq_foldl_reverse (l : List α) (f : α → β → β) (b) :
     l.foldr f b = l.reverse.foldl (fun x y => f y x) b := by simp
 
-@[simp] theorem reverse_replicate (n) (a : α) : reverse (replicate n a) = replicate n a :=
-  eq_replicate_iff.2
-    ⟨by rw [length_reverse, length_replicate],
-     fun _ h => eq_of_mem_replicate (mem_reverse.1 h)⟩
+theorem foldl_assoc {op : α → α → α} [ha : Std.Associative op] :
+    ∀ {l : List α} {a₁ a₂}, l.foldl op (op a₁ a₂) = op a₁ (l.foldl op a₂)
+  | [], a₁, a₂ => rfl
+  | a :: l, a₁, a₂ => by
+    simp only [foldl_cons, ha.assoc]
+    rw [foldl_assoc]
+
+theorem foldr_assoc {op : α → α → α} [ha : Std.Associative op] :
+    ∀ {l : List α} {a₁ a₂}, l.foldr op (op a₁ a₂) = op (l.foldr op a₁) a₂
+  | [], a₁, a₂ => rfl
+  | a :: l, a₁, a₂ => by
+    simp only [foldr_cons, ha.assoc]
+    rw [foldr_assoc]
+
+theorem foldl_hom (f : α₁ → α₂) (g₁ : α₁ → β → α₁) (g₂ : α₂ → β → α₂) (l : List β) (init : α₁)
+    (H : ∀ x y, g₂ (f x) y = f (g₁ x y)) : l.foldl g₂ (f init) = f (l.foldl g₁ init) := by
+  induction l generalizing init <;> simp [*, H]
+
+theorem foldr_hom (f : β₁ → β₂) (g₁ : α → β₁ → β₁) (g₂ : α → β₂ → β₂) (l : List α) (init : β₁)
+    (H : ∀ x y, g₂ x (f y) = f (g₁ x y)) : l.foldr g₂ (f init) = f (l.foldr g₁ init) := by
+  induction l <;> simp [*, H]
+
+/--
+Prove a proposition about the result of `List.foldl`,
+by proving it for the initial data,
+and the implication that the operation applied to any element of the list preserves the property.
+
+The motive can take values in `Sort _`, so this may be used to construct data,
+as well as to prove propositions.
+-/
+def foldlRecOn {motive : β → Sort _} : ∀ (l : List α) (op : β → α → β) (b : β) (_ : motive b)
+    (_ : ∀ (b : β) (_ : motive b) (a : α) (_ : a ∈ l), motive (op b a)), motive (List.foldl op b l)
+  | [], _, _, hb, _ => hb
+  | hd :: tl, op, b, hb, hl =>
+    foldlRecOn tl op (op b hd) (hl b hb hd (mem_cons_self hd tl))
+      fun y hy x hx => hl y hy x (mem_cons_of_mem hd hx)
+
+@[simp] theorem foldlRecOn_nil {motive : β → Sort _} (hb : motive b)
+    (hl : ∀ (b : β) (_ : motive b) (a : α) (_ : a ∈ []), motive (op b a)) :
+    foldlRecOn [] op b hb hl = hb := rfl
+
+@[simp] theorem foldlRecOn_cons {motive : β → Sort _} (hb : motive b)
+    (hl : ∀ (b : β) (_ : motive b) (a : α) (_ : a ∈ x :: l), motive (op b a)) :
+    foldlRecOn (x :: l) op b hb hl =
+      foldlRecOn l op (op b x) (hl b hb x (mem_cons_self x l))
+        (fun b c a m => hl b c a (mem_cons_of_mem x m)) :=
+  rfl
+
+/--
+Prove a proposition about the result of `List.foldr`,
+by proving it for the initial data,
+and the implication that the operation applied to any element of the list preserves the property.
+
+The motive can take values in `Sort _`, so this may be used to construct data,
+as well as to prove propositions.
+-/
+def foldrRecOn {motive : β → Sort _} : ∀ (l : List α) (op : α → β → β) (b : β) (_ : motive b)
+    (_ : ∀ (b : β) (_ : motive b) (a : α) (_ : a ∈ l), motive (op a b)), motive (List.foldr op b l)
+  | nil, _, _, hb, _ => hb
+  | x :: l, op, b, hb, hl =>
+    hl (foldr op b l)
+      (foldrRecOn l op b hb fun b c a m => hl b c a (mem_cons_of_mem x m)) x (mem_cons_self x l)
+
+@[simp] theorem foldrRecOn_nil {motive : β → Sort _} (hb : motive b)
+    (hl : ∀ (b : β) (_ : motive b) (a : α) (_ : a ∈ []), motive (op a b)) :
+    foldrRecOn [] op b hb hl = hb := rfl
+
+@[simp] theorem foldrRecOn_cons {motive : β → Sort _} (hb : motive b)
+    (hl : ∀ (b : β) (_ : motive b) (a : α) (_ : a ∈ x :: l), motive (op a b)) :
+    foldrRecOn (x :: l) op b hb hl =
+      hl _ (foldrRecOn l op b hb fun b c a m => hl b c a (mem_cons_of_mem x m))
+        x (mem_cons_self x l) :=
+  rfl
+
+/--
+We can prove that two folds over the same list are related (by some arbitrary relation)
+if we know that the initial elements are related and the folding function, for each element of the list,
+preserves the relation.
+-/
+theorem foldl_rel {l : List α} {f g : β → α → β} {a b : β} (r : β → β → Prop)
+    (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)) :
+    r (l.foldl (fun acc a => f acc a) a) (l.foldl (fun acc a => g acc a) b) := by
+  induction l generalizing a b with
+  | nil => simp_all
+  | cons a l ih =>
+    simp only [foldl_cons]
+    apply ih
+    · simp_all
+    · exact fun a m c c' h => h' _ (by simp_all) _ _ h
+
+/--
+We can prove that two folds over the same list are related (by some arbitrary relation)
+if we know that the initial elements are related and the folding function, for each element of the list,
+preserves the relation.
+-/
+theorem foldr_rel {l : List α} {f g : α → β → β} {a b : β} (r : β → β → Prop)
+    (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')) :
+    r (l.foldr (fun a acc => f a acc) a) (l.foldr (fun a acc => g a acc) b) := by
+  induction l generalizing a b with
+  | nil => simp_all
+  | cons a l ih =>
+    simp only [foldr_cons]
+    apply h'
+    · simp
+    · exact ih h fun a m c c' h => h' _ (by simp_all) _ _ h
+
+@[simp] theorem foldl_add_const (l : List α) (a b : Nat) :
+    l.foldl (fun x _ => x + a) b = b + a * l.length := by
+  induction l generalizing b with
+  | nil => simp
+  | cons y l ih =>
+    simp only [foldl_cons, ih, length_cons, Nat.mul_add, Nat.mul_one, Nat.add_assoc,
+      Nat.add_comm a]
+
+@[simp] theorem foldr_add_const (l : List α) (a b : Nat) :
+    l.foldr (fun _ x => x + a) b = b + a * l.length := by
+  induction l generalizing b with
+  | nil => simp
+  | cons y l ih =>
+    simp only [foldr_cons, ih, length_cons, Nat.mul_add, Nat.mul_one, Nat.add_assoc]
+
 
 /-! #### Further results about `getLast` and `getLast?` -/
 

src/Init/Data/List/ToArray.lean

@@ -46,7 +46,7 @@ theorem toArray_cons (a : α) (l : List α) : (a :: l).toArray = #[a] ++ l.toArr
 @[simp] theorem isEmpty_toArray (l : List α) : l.toArray.isEmpty = l.isEmpty := by
   cases l <;> simp [Array.isEmpty]
 
-@[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = singleton a := rfl
+@[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = Array.singleton a := rfl
 
 @[simp] theorem back!_toArray [Inhabited α] (l : List α) : l.toArray.back! = l.getLast! := by
   simp only [back!, size_toArray, Array.get!_eq_getElem!, getElem!_toArray, getLast!_eq_getElem!]

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

@@ -49,4 +49,17 @@ theorem lt_div_mul_self (h : 0 < k) (w : k ≤ x) : x - k < x / k * k := by
   have : x % k < k := mod_lt x h
   omega
 
+theorem div_pos (hba : b ≤ a) (hb : 0 < b) : 0 < a / b := by
+  cases b
+  · contradiction
+  · simp [Nat.pos_iff_ne_zero, div_eq_zero_iff_lt, hba]
+
+theorem div_le_div_left (hcb : c ≤ b) (hc : 0 < c) : a / b ≤ a / c :=
+  (Nat.le_div_iff_mul_le hc).2 <|
+    Nat.le_trans (Nat.mul_le_mul_left _ hcb) (Nat.div_mul_le_self a b)
+
+theorem div_add_le_right {z : Nat} (h : 0 < z) (x y : Nat) :
+    x / (y + z) ≤ x / z :=
+  div_le_div_left (Nat.le_add_left z y) h
+
 end Nat

src/Init/Data/UInt/Basic.lean

@@ -159,6 +159,8 @@ def UInt32.xor (a b : UInt32) : UInt32 := ⟨a.toBitVec ^^^ b.toBitVec⟩
 def UInt32.shiftLeft (a b : UInt32) : UInt32 := ⟨a.toBitVec <<< (mod b 32).toBitVec⟩
 @[extern "lean_uint32_shift_right"]
 def UInt32.shiftRight (a b : UInt32) : UInt32 := ⟨a.toBitVec >>> (mod b 32).toBitVec⟩
+def UInt32.lt (a b : UInt32) : Prop := a.toBitVec < b.toBitVec
+def UInt32.le (a b : UInt32) : Prop := a.toBitVec ≤ b.toBitVec
 
 instance : Add UInt32       := ⟨UInt32.add⟩
 instance : Sub UInt32       := ⟨UInt32.sub⟩
@@ -169,6 +171,8 @@ set_option linter.deprecated false in
 instance : HMod UInt32 Nat UInt32 := ⟨UInt32.modn⟩
 
 instance : Div UInt32       := ⟨UInt32.div⟩
+instance : LT UInt32        := ⟨UInt32.lt⟩
+instance : LE UInt32        := ⟨UInt32.le⟩
 
 @[extern "lean_uint32_complement"]
 def UInt32.complement (a : UInt32) : UInt32 := ⟨~~~a.toBitVec⟩

src/Init/Data/Vector/Basic.lean

@@ -103,7 +103,7 @@ of bounds.
 @[inline] def head [NeZero n] (v : Vector α n) := v[0]'(Nat.pos_of_neZero n)
 
 /-- Push an element `x` to the end of a vector. -/
-@[inline] def push (x : α) (v : Vector α n)  : Vector α (n + 1) :=
+@[inline] def push (v : Vector α n) (x : α) : Vector α (n + 1) :=
   ⟨v.toArray.push x, by simp⟩
 
 /-- Remove the last element of a vector. -/
@@ -136,6 +136,18 @@ This will perform the update destructively provided that the vector has a refere
 @[inline] def set! (v : Vector α n) (i : Nat) (x : α) : Vector α n :=
   ⟨v.toArray.set! i x, by simp⟩
 
+@[inline] def foldlM [Monad m] (f : β → α → m β) (b : β) (v : Vector α n) : m β :=
+  v.toArray.foldlM f b
+
+@[inline] def foldrM [Monad m] (f : α → β → m β) (b : β) (v : Vector α n) : m β :=
+  v.toArray.foldrM f b
+
+@[inline] def foldl (f : β → α → β) (b : β) (v : Vector α n) : β :=
+  v.toArray.foldl f b
+
+@[inline] def foldr (f : α → β → β) (b : β) (v : Vector α n) : β :=
+  v.toArray.foldr f b
+
 /-- Append two vectors. -/
 @[inline] def append (v : Vector α n) (w : Vector α m) : Vector α (n + m) :=
   ⟨v.toArray ++ w.toArray, by simp⟩

src/Init/Data/Vector/Lemmas.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Shreyas Srinivas. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Shreyas Srinivas, Francois Dorais
+Authors: Shreyas Srinivas, Francois Dorais, Kim Morrison
 -/
 prelude
 import Init.Data.Vector.Basic
@@ -66,6 +66,18 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
 @[simp] theorem back?_mk (a : Array α) (h : a.size = n) :
     (Vector.mk a h).back? = a.back? := rfl
 
+@[simp] theorem foldlM_mk [Monad m] (f : β → α → m β) (b : β) (a : Array α) (h : a.size = n) :
+    (Vector.mk a h).foldlM f b = a.foldlM f b := rfl
+
+@[simp] theorem foldrM_mk [Monad m] (f : α → β → m β) (b : β) (a : Array α) (h : a.size = n) :
+    (Vector.mk a h).foldrM f b = a.foldrM f b := rfl
+
+@[simp] theorem foldl_mk (f : β → α → β) (b : β) (a : Array α) (h : a.size = n) :
+    (Vector.mk a h).foldl f b = a.foldl f b := rfl
+
+@[simp] theorem foldr_mk (f : α → β → β) (b : β) (a : Array α) (h : a.size = n) :
+    (Vector.mk a h).foldr f b = a.foldr f b := rfl
+
 @[simp] theorem drop_mk (a : Array α) (h : a.size = n) (m) :
     (Vector.mk a h).drop m = Vector.mk (a.extract m a.size) (by simp [h]) := rfl
 
@@ -141,6 +153,14 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
 @[simp] theorem all_mk (p : α → Bool) (a : Array α) (h : a.size = n) :
     (Vector.mk a h).all p = a.all p := rfl
 
+@[simp] theorem eq_mk : v = Vector.mk a h ↔ v.toArray = a := by
+  cases v
+  simp
+
+@[simp] theorem mk_eq : Vector.mk a h = v ↔ a = v.toArray := by
+  cases v
+  simp
+
 /-! ### toArray lemmas -/
 
 @[simp] theorem getElem_toArray {α n} (xs : Vector α n) (i : Nat) (h : i < xs.toArray.size) :
@@ -1023,11 +1043,12 @@ theorem mem_setIfInBounds (v : Vector α n) (i : Nat) (hi : i < n) (a : α) :
   cases l₂
   simp
 
-/-! Content below this point has not yet been aligned with `List` and `Array`. -/
+/-! ### map -/
 
-@[simp] theorem getElem_ofFn {α n} (f : Fin n → α) (i : Nat) (h : i < n) :
-    (Vector.ofFn f)[i] = f ⟨i, by simpa using h⟩ := by
-  simp [ofFn]
+@[simp] theorem getElem_map (f : α → β) (a : Vector α n) (i : Nat) (hi : i < n) :
+    (a.map f)[i] = f a[i] := by
+  cases a
+  simp
 
 /-- The empty vector maps to the empty vector. -/
 @[simp]
@@ -1035,6 +1056,123 @@ theorem map_empty (f : α → β) : map f #v[] = #v[] := by
   rw [map, mk.injEq]
   exact Array.map_empty f
 
+@[simp] theorem map_push {f : α → β} {as : Vector α n} {x : α} :
+    (as.push x).map f = (as.map f).push (f x) := by
+  cases as
+  simp
+
+@[simp] theorem map_id_fun : map (n := n) (id : α → α) = id := by
+  funext l
+  induction l <;> simp_all
+
+/-- `map_id_fun'` differs from `map_id_fun` by representing the identity function as a lambda, rather than `id`. -/
+@[simp] theorem map_id_fun' : map (n := n) (fun (a : α) => a) = id := map_id_fun
+
+-- This is not a `@[simp]` lemma because `map_id_fun` will apply.
+theorem map_id (l : Vector α n) : map (id : α → α) l = l := by
+  cases l <;> simp_all
+
+/-- `map_id'` differs from `map_id` by representing the identity function as a lambda, rather than `id`. -/
+-- This is not a `@[simp]` lemma because `map_id_fun'` will apply.
+theorem map_id' (l : Vector α n) : map (fun (a : α) => a) l = l := map_id l
+
+/-- Variant of `map_id`, with a side condition that the function is pointwise the identity. -/
+theorem map_id'' {f : α → α} (h : ∀ x, f x = x) (l : Vector α n) : map f l = l := by
+  simp [show f = id from funext h]
+
+theorem map_singleton (f : α → β) (a : α) : map f #v[a] = #v[f a] := rfl
+
+@[simp] theorem mem_map {f : α → β} {l : Vector α n} : b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b := by
+  cases l
+  simp
+
+theorem exists_of_mem_map (h : b ∈ map f l) : ∃ a, a ∈ l ∧ f a = b := mem_map.1 h
+
+theorem mem_map_of_mem (f : α → β) (h : a ∈ l) : f a ∈ map f l := mem_map.2 ⟨_, h, rfl⟩
+
+theorem forall_mem_map {f : α → β} {l : Vector α n} {P : β → Prop} :
+    (∀ (i) (_ : i ∈ l.map f), P i) ↔ ∀ (j) (_ : j ∈ l), P (f j) := by
+  simp
+
+@[simp] theorem map_inj_left {f g : α → β} : map f l = map g l ↔ ∀ a ∈ l, f a = g a := by
+  cases l <;> simp_all
+
+theorem map_congr_left (h : ∀ a ∈ l, f a = g a) : map f l = map g l :=
+  map_inj_left.2 h
+
+theorem map_inj [NeZero n] : map (n := n) f = map g ↔ f = g := by
+  constructor
+  · intro h
+    ext a
+    replace h := congrFun h (mkVector n a)
+    simp only [mkVector, map_mk, mk.injEq, Array.map_inj_left, Array.mem_mkArray,  and_imp,
+      forall_eq_apply_imp_iff] at h
+    exact h (NeZero.ne n)
+  · intro h; subst h; rfl
+
+theorem map_eq_push_iff {f : α → β} {l : Vector α (n + 1)} {l₂ : Vector β n} {b : β} :
+    map f l = l₂.push b ↔ ∃ l₁ a, l = l₁.push a ∧ map f l₁ = l₂ ∧ f a = b := by
+  rcases l with ⟨l, h⟩
+  rcases l₂ with ⟨l₂, rfl⟩
+  simp only [map_mk, push_mk, mk.injEq, Array.map_eq_push_iff]
+  constructor
+  · rintro ⟨l₁, a, rfl, rfl, rfl⟩
+    refine ⟨⟨l₁, by simp⟩, a, by simp⟩
+  · rintro ⟨l₁, a, h₁, h₂, rfl⟩
+    refine ⟨l₁.toArray, a, by simp_all⟩
+
+@[simp] theorem map_eq_singleton_iff {f : α → β} {l : Vector α 1} {b : β} :
+    map f l = #v[b] ↔ ∃ a, l = #v[a] ∧ f a = b := by
+  cases l
+  simp
+
+theorem map_eq_map_iff {f g : α → β} {l : Vector α n} :
+    map f l = map g l ↔ ∀ a ∈ l, f a = g a := by
+  cases l <;> simp_all
+
+theorem map_eq_iff {f : α → β} {l : Vector α n} {l' : Vector β n} :
+    map f l = l' ↔ ∀ i (h : i < n), l'[i] = f l[i] := by
+  rcases l with ⟨l, rfl⟩
+  rcases l' with ⟨l', h'⟩
+  simp only [map_mk, eq_mk, Array.map_eq_iff, getElem_mk]
+  constructor
+  · intro w i h
+    simpa [h, h'] using w i
+  · intro w i
+    if h : i < l.size then
+      simpa [h, h'] using w i h
+    else
+      rw [getElem?_neg, getElem?_neg, Option.map_none'] <;> omega
+
+@[simp] theorem map_set {f : α → β} {l : Vector α n} {i : Nat} {h : i < n} {a : α} :
+    (l.set i a).map f = (l.map f).set i (f a) (by simpa using h) := by
+  cases l
+  simp
+
+@[simp] theorem map_setIfInBounds {f : α → β} {l : Vector α n} {i : Nat} {a : α} :
+    (l.setIfInBounds i a).map f = (l.map f).setIfInBounds i (f a) := by
+  cases l
+  simp
+
+@[simp] theorem map_pop {f : α → β} {l : Vector α n} : l.pop.map f = (l.map f).pop := by
+  cases l
+  simp
+
+@[simp] theorem back?_map {f : α → β} {l : Vector α n} : (l.map f).back? = l.back?.map f := by
+  cases l
+  simp
+
+@[simp] theorem map_map {f : α → β} {g : β → γ} {as : Vector α n} :
+    (as.map f).map g = as.map (g ∘ f) := by
+  cases as
+  simp
+
+/-! Content below this point has not yet been aligned with `List` and `Array`. -/
+
+@[simp] theorem getElem_ofFn {α n} (f : Fin n → α) (i : Nat) (h : i < n) :
+    (Vector.ofFn f)[i] = f ⟨i, by simpa using h⟩ := by
+  simp [ofFn]
+
 @[simp] theorem getElem_push_last {v : Vector α n} {x : α} : (v.push x)[n] = x := by
   rcases v with ⟨data, rfl⟩
   simp
@@ -1088,13 +1226,6 @@ theorem getElem_append_right {a : Vector α n} {b : Vector α m} {i : Nat} (h :
   cases a
   simp
 
-/-! ### map -/
-
-@[simp] theorem getElem_map (f : α → β) (a : Vector α n) (i : Nat) (hi : i < n) :
-    (a.map f)[i] = f a[i] := by
-  cases a
-  simp
-
 /-! ### zipWith -/
 
 @[simp] theorem getElem_zipWith (f : α → β → γ) (a : Vector α n) (b : Vector β n) (i : Nat)
@@ -1103,6 +1234,37 @@ theorem getElem_append_right {a : Vector α n} {b : Vector α m} {i : Nat} (h :
   cases b
   simp
 
+/-! ### foldlM and foldrM -/
+
+@[simp] theorem foldlM_append [Monad m] [LawfulMonad m] (f : β → α → m β) (b) (l : Vector α n) (l' : Vector α n') :
+    (l ++ l').foldlM f b = l.foldlM f b >>= l'.foldlM f := by
+  cases l
+  cases l'
+  simp
+
+@[simp] theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (l : Vector α n) (a : α) :
+    (l.push a).foldrM f init = f a init >>= l.foldrM f := by
+  cases l
+  simp
+
+theorem foldl_eq_foldlM (f : β → α → β) (b) (l : Vector α n) :
+    l.foldl f b = l.foldlM (m := Id) f b := by
+  cases l
+  simp [Array.foldl_eq_foldlM]
+
+theorem foldr_eq_foldrM (f : α → β → β) (b) (l : Vector α n) :
+    l.foldr f b = l.foldrM (m := Id) f b := by
+  cases l
+  simp [Array.foldr_eq_foldrM]
+
+@[simp] theorem id_run_foldlM (f : β → α → Id β) (b) (l : Vector α n) :
+    Id.run (l.foldlM f b) = l.foldl f b := (foldl_eq_foldlM f b l).symm
+
+@[simp] theorem id_run_foldrM (f : α → β → Id β) (b) (l : Vector α n) :
+    Id.run (l.foldrM f b) = l.foldr f b := (foldr_eq_foldrM f b l).symm
+
+/-! ### foldl and foldr -/
+
 /-! ### take -/
 
 @[simp] theorem take_size (a : Vector α n) : a.take n = a.cast (by simp) := by

src/Init/Grind.lean

@@ -10,3 +10,4 @@ import Init.Grind.Lemmas
 import Init.Grind.Cases
 import Init.Grind.Propagator
 import Init.Grind.Util
+import Init.Grind.Offset

src/Init/Grind/Lemmas.lean

@@ -25,6 +25,9 @@ theorem and_eq_of_eq_false_right {a b : Prop} (h : b = False) : (a ∧ b) = Fals
 theorem eq_true_of_and_eq_true_left {a b : Prop} (h : (a ∧ b) = True) : a = True := by simp_all
 theorem eq_true_of_and_eq_true_right {a b : Prop} (h : (a ∧ b) = True) : b = True := by simp_all
 
+theorem or_of_and_eq_false {a b : Prop} (h : (a ∧ b) = False) : (¬a ∨ ¬b) := by
+  by_cases a <;> by_cases b <;> simp_all
+
 /-! Or -/
 
 theorem or_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a ∨ b) = True := by simp [h]
@@ -35,6 +38,15 @@ theorem or_eq_of_eq_false_right {a b : Prop} (h : b = False) : (a ∨ b) = a :=
 theorem eq_false_of_or_eq_false_left {a b : Prop} (h : (a ∨ b) = False) : a = False := by simp_all
 theorem eq_false_of_or_eq_false_right {a b : Prop} (h : (a ∨ b) = False) : b = False := by simp_all
 
+/-! Implies -/
+
+theorem imp_eq_of_eq_false_left {a b : Prop} (h : a = False) : (a → b) = True := by simp [h]
+theorem imp_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a → b) = True := by simp [h]
+theorem imp_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a → b) = b := by simp [h]
+
+theorem eq_true_of_imp_eq_false {a b : Prop} (h : (a → b) = False) : a = True := by simp_all
+theorem eq_false_of_imp_eq_false {a b : Prop} (h : (a → b) = False) : b = False := by simp_all
+
 /-! Not -/
 
 theorem not_eq_of_eq_true {a : Prop} (h : a = True) : (Not a) = False := by simp [h]
@@ -61,9 +73,28 @@ theorem forall_propagator (p : Prop) (q : p → Prop) (q' : Prop) (h₁ : p = Tr
   · intro h'; exact Eq.mp h₂ (h' (of_eq_true h₁))
   · intro h'; intros; exact Eq.mpr h₂ h'
 
+theorem of_forall_eq_false (α : Sort u) (p : α → Prop) (h : (∀ x : α, p x) = False) : ∃ x : α, ¬ p x := by simp_all
+
 /-! dite -/
 
 theorem dite_cond_eq_true' {α : Sort u} {c : Prop} {_ : Decidable c} {a : c → α} {b : ¬ c → α} {r : α} (h₁ : c = True) (h₂ : a (of_eq_true h₁) = r) : (dite c a b) = r := by simp [h₁, h₂]
 theorem dite_cond_eq_false' {α : Sort u} {c : Prop} {_ : Decidable c} {a : c → α} {b : ¬ c → α} {r : α} (h₁ : c = False) (h₂ : b (of_eq_false h₁) = r) : (dite c a b) = r := by simp [h₁, h₂]
 
+/-! Casts -/
+
+theorem eqRec_heq.{u_1, u_2} {α : Sort u_2} {a : α}
+        {motive : (x : α) → a = x → Sort u_1} (v : motive a (Eq.refl a)) {b : α} (h : a = b)
+        : HEq (@Eq.rec α a motive v b h) v := by
+ subst h; rfl
+
+theorem eqRecOn_heq.{u_1, u_2} {α : Sort u_2} {a : α}
+        {motive : (x : α) → a = x → Sort u_1} {b : α} (h : a = b) (v : motive a (Eq.refl a))
+        : HEq (@Eq.recOn α a motive b h v) v := by
+ subst h; rfl
+
+theorem eqNDRec_heq.{u_1, u_2} {α : Sort u_2} {a : α}
+        {motive : α → Sort u_1} (v : motive a) {b : α} (h : a = b)
+        : HEq (@Eq.ndrec α a motive v b h) v := by
+ subst h; rfl
+
 end Lean.Grind

src/Init/Grind/Norm.lean

@@ -41,8 +41,9 @@ attribute [grind_norm] not_true
 -- False
 attribute [grind_norm] not_false_eq_true
 
+-- Remark: we disabled the following normalization rule because we want this information when implementing splitting heuristics
 -- Implication as a clause
-@[grind_norm↓] theorem imp_eq (p q : Prop) : (p → q) = (¬ p ∨ q) := by
+theorem imp_eq (p q : Prop) : (p → q) = (¬ p ∨ q) := by
   by_cases p <;> by_cases q <;> simp [*]
 
 -- And

src/Init/Grind/Offset.lean

@@ -0,0 +1,165 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Core
+import Init.Omega
+
+namespace Lean.Grind.Offset
+
+abbrev Var := Nat
+abbrev Context := Lean.RArray Nat
+
+def fixedVar := 100000000 -- Any big number should work here
+
+def Var.denote (ctx : Context) (v : Var) : Nat :=
+  bif v == fixedVar then 1 else ctx.get v
+
+structure Cnstr where
+  x : Var
+  y : Var
+  k : Nat  := 0
+  l : Bool := true
+  deriving Repr, DecidableEq, Inhabited
+
+def Cnstr.denote (c : Cnstr) (ctx : Context) : Prop :=
+  if c.l then
+    c.x.denote ctx + c.k ≤ c.y.denote ctx
+  else
+    c.x.denote ctx ≤ c.y.denote ctx + c.k
+
+def trivialCnstr : Cnstr := { x := 0, y := 0, k := 0, l := true }
+
+@[simp] theorem denote_trivial (ctx : Context) : trivialCnstr.denote ctx := by
+  simp [Cnstr.denote, trivialCnstr]
+
+def Cnstr.trans (c₁ c₂ : Cnstr) : Cnstr :=
+  if c₁.y = c₂.x then
+    let { x, k := k₁, l := l₁, .. } := c₁
+    let { y, k := k₂, l := l₂, .. } := c₂
+    match l₁, l₂ with
+    | false, false =>
+      { x, y, k := k₁ + k₂, l := false }
+    | false, true =>
+      if k₁ < k₂ then
+        { x, y, k := k₂ - k₁, l := true }
+      else
+        { x, y, k := k₁ - k₂, l := false }
+    | true, false =>
+      if k₁ < k₂ then
+        { x, y, k := k₂ - k₁, l := false }
+      else
+        { x, y, k := k₁ - k₂, l := true }
+    | true, true =>
+      { x, y, k := k₁ + k₂, l := true }
+  else
+    trivialCnstr
+
+@[simp] theorem Cnstr.denote_trans_easy (ctx : Context) (c₁ c₂ : Cnstr) (h : c₁.y ≠ c₂.x) : (c₁.trans c₂).denote ctx := by
+  simp [*, Cnstr.trans]
+
+@[simp] theorem Cnstr.denote_trans (ctx : Context) (c₁ c₂ : Cnstr) : c₁.denote ctx → c₂.denote ctx → (c₁.trans c₂).denote ctx := by
+  by_cases c₁.y = c₂.x
+  case neg => simp [*]
+  simp [trans, *]
+  let { x, k := k₁, l := l₁, .. } := c₁
+  let { y, k := k₂, l := l₂, .. } := c₂
+  simp_all; split
+  · simp [denote]; omega
+  · split <;> simp [denote] <;> omega
+  · split <;> simp [denote] <;> omega
+  · simp [denote]; omega
+
+def Cnstr.isTrivial (c : Cnstr) : Bool := c.x == c.y && c.k == 0
+
+theorem Cnstr.of_isTrivial (ctx : Context) (c : Cnstr) : c.isTrivial = true → c.denote ctx := by
+  cases c; simp [isTrivial]; intros; simp [*, denote]
+
+def Cnstr.isFalse (c : Cnstr) : Bool := c.x == c.y && c.k != 0 && c.l == true
+
+theorem Cnstr.of_isFalse (ctx : Context) {c : Cnstr} : c.isFalse = true → ¬c.denote ctx := by
+  cases c; simp [isFalse]; intros; simp [*, denote]; omega
+
+def Cnstrs := List Cnstr
+
+def Cnstrs.denoteAnd' (ctx : Context) (c₁ : Cnstr) (c₂ : Cnstrs) : Prop :=
+  match c₂ with
+  | [] => c₁.denote ctx
+  | c::cs => c₁.denote ctx ∧ Cnstrs.denoteAnd' ctx c cs
+
+theorem Cnstrs.denote'_trans (ctx : Context) (c₁ c : Cnstr) (cs : Cnstrs) : c₁.denote ctx → denoteAnd' ctx c cs → denoteAnd' ctx (c₁.trans c) cs := by
+  induction cs
+  next => simp [denoteAnd', *]; apply Cnstr.denote_trans
+  next c cs ih => simp [denoteAnd']; intros; simp [*]
+
+def Cnstrs.trans' (c₁ : Cnstr) (c₂ : Cnstrs) : Cnstr :=
+  match c₂ with
+  | [] => c₁
+  | c::c₂ => trans' (c₁.trans c) c₂
+
+@[simp] theorem Cnstrs.denote'_trans' (ctx : Context) (c₁ : Cnstr) (c₂ : Cnstrs) : denoteAnd' ctx c₁ c₂ → (trans' c₁ c₂).denote ctx := by
+  induction c₂ generalizing c₁
+  next => intros; simp_all [trans', denoteAnd']
+  next c cs ih => simp [denoteAnd']; intros; simp [trans']; apply ih; apply denote'_trans <;> assumption
+
+def Cnstrs.denoteAnd (ctx : Context) (c : Cnstrs) : Prop :=
+  match c with
+  | [] => True
+  | c::cs => denoteAnd' ctx c cs
+
+def Cnstrs.trans (c : Cnstrs) : Cnstr :=
+  match c with
+  | []    => trivialCnstr
+  | c::cs => trans' c cs
+
+theorem Cnstrs.of_denoteAnd_trans {ctx : Context} {c : Cnstrs} : c.denoteAnd ctx → c.trans.denote ctx := by
+  cases c <;> simp [*, trans, denoteAnd] <;> intros <;> simp [*]
+
+def Cnstrs.isFalse (c : Cnstrs) : Bool :=
+  c.trans.isFalse
+
+theorem Cnstrs.unsat' (ctx : Context) (c : Cnstrs) : c.isFalse = true → ¬ c.denoteAnd ctx := by
+  simp [isFalse]; intro h₁ h₂
+  have := of_denoteAnd_trans h₂
+  have := Cnstr.of_isFalse ctx h₁
+  contradiction
+
+/-- `denote ctx [c_1, ..., c_n] C` is `c_1.denote ctx → ... → c_n.denote ctx → C` -/
+def Cnstrs.denote (ctx : Context) (cs : Cnstrs) (C : Prop) : Prop :=
+  match cs with
+  | [] => C
+  | c::cs => c.denote ctx → denote ctx cs C
+
+theorem Cnstrs.not_denoteAnd'_eq (ctx : Context) (c : Cnstr) (cs : Cnstrs) (C : Prop) : (denoteAnd' ctx c cs → C) = denote ctx (c::cs) C := by
+  simp [denote]
+  induction cs generalizing c
+  next => simp [denoteAnd', denote]
+  next c' cs ih =>
+    simp [denoteAnd', denote, *]
+
+theorem Cnstrs.not_denoteAnd_eq (ctx : Context) (cs : Cnstrs) (C : Prop) : (denoteAnd ctx cs → C) = denote ctx cs C := by
+  cases cs
+  next => simp [denoteAnd, denote]
+  next c cs => apply not_denoteAnd'_eq
+
+def Cnstr.isImpliedBy (cs : Cnstrs) (c : Cnstr) : Bool :=
+  cs.trans == c
+
+/-! Main theorems used by `grind`. -/
+
+/-- Auxiliary theorem used by `grind` to prove that a system of offset inequalities is unsatisfiable. -/
+theorem Cnstrs.unsat (ctx : Context) (cs : Cnstrs) : cs.isFalse = true → cs.denote ctx False := by
+  intro h
+  rw [← not_denoteAnd_eq]
+  apply unsat'
+  assumption
+
+/-- Auxiliary theorem used by `grind` to prove an implied offset inequality. -/
+theorem Cnstrs.imp (ctx : Context) (cs : Cnstrs) (c : Cnstr) (h : c.isImpliedBy cs = true)  : cs.denote ctx (c.denote ctx) := by
+  rw [← eq_of_beq h]
+  rw [← not_denoteAnd_eq]
+  apply of_denoteAnd_trans
+
+end Lean.Grind.Offset

src/Init/Grind/Tactics.lean

@@ -6,20 +6,27 @@ Authors: Leonardo de Moura
 prelude
 import Init.Tactics
 
+namespace Lean.Parser.Attr
+
+syntax grindEq     := "="
+syntax grindEqBoth := atomic("_" "=" "_")
+syntax grindEqRhs  := atomic("=" "_")
+syntax grindBwd    := "←"
+syntax grindFwd    := "→"
+
+syntax (name := grind) "grind" (grindEqBoth <|> grindEqRhs <|> grindEq <|> grindBwd <|> grindFwd)? : attr
+
+end Lean.Parser.Attr
+
 namespace Lean.Grind
 /--
 The configuration for `grind`.
-Passed to `grind` using, for example, the `grind (config := { eager := true })` syntax.
+Passed to `grind` using, for example, the `grind (config := { matchEqs := true })` syntax.
 -/
 structure Config where
-  /-- When `eager` is true (default: `false`), `grind` eagerly splits `if-then-else` and `match` expressions during internalization. -/
-  eager : Bool := false
-  /-- Maximum number of branches (i.e., case-splits) in the proof search tree. -/
-  splits : Nat := 100
-  /--
-  Maximum number of E-matching (aka heuristic theorem instantiation)
-  in a proof search tree branch.
-  -/
+  /-- Maximum number of case-splits in a proof search branch. It does not include splits performed during normalization. -/
+  splits : Nat := 5
+  /-- Maximum number of E-matching (aka heuristic theorem instantiation) rounds before each case split. -/
   ematch : Nat := 5
   /--
   Maximum term generation.
@@ -30,6 +37,14 @@ structure Config where
   instances : Nat := 1000
   /-- If `matchEqs` is `true`, `grind` uses `match`-equations as E-matching theorems. -/
   matchEqs : Bool := true
+  /-- If `splitMatch` is `true`, `grind` performs case-splitting on `match`-expressions during the search. -/
+  splitMatch : Bool := true
+  /-- If `splitIte` is `true`, `grind` performs case-splitting on `if-then-else` expressions during the search. -/
+  splitIte : Bool := true
+  /--
+  If `splitIndPred` is `true`, `grind` performs case-splitting on inductive predicates.
+  Otherwise, it performs case-splitting only on types marked with `[grind_split]` attribute. -/
+  splitIndPred : Bool := true
   deriving Inhabited, BEq
 
 end Lean.Grind

src/Init/Grind/Util.lean

@@ -21,7 +21,12 @@ def doNotSimp {α : Sort u} (a : α) : α := a
 /-- Gadget for representing offsets `t+k` in patterns. -/
 def offset (a b : Nat) : Nat := a + b
 
-set_option pp.proofs true
+/--
+Gadget for annotating the equalities in `match`-equations conclusions.
+`_origin` is the term used to instantiate the `match`-equation using E-matching.
+When `EqMatch a b origin` is `True`, we mark `origin` as a resolved case-split.
+-/
+def EqMatch (a b : α) {_origin : α} : Prop := a = b
 
 theorem nestedProof_congr (p q : Prop) (h : p = q) (hp : p) (hq : q) : HEq (nestedProof p hp) (nestedProof q hq) := by
   subst h; apply HEq.refl

src/Init/Prelude.lean

@@ -4170,6 +4170,16 @@ def withRef [Monad m] [MonadRef m] {α} (ref : Syntax) (x : m α) : m α :=
   let ref := replaceRef ref oldRef
   MonadRef.withRef ref x
 
+/--
+If `ref? = some ref`, run `x : m α` with a modified value for the `ref` by calling `withRef`.
+Otherwise, run `x` directly.
+-/
+@[always_inline, inline]
+def withRef? [Monad m] [MonadRef m] {α} (ref? : Option Syntax) (x : m α) : m α :=
+  match ref? with
+  | some ref => withRef ref x
+  | _        => x
+
 /-- A monad that supports syntax quotations. Syntax quotations (in term
     position) are monadic values that when executed retrieve the current "macro
     scope" from the monad and apply it to every identifier they introduce

src/Init/Tactics.lean

@@ -818,7 +818,7 @@ syntax inductionAlt  := ppDedent(ppLine) inductionAltLHS+ " => " (hole <|> synth
 After `with`, there is an optional tactic that runs on all branches, and
 then a list of alternatives.
 -/
-syntax inductionAlts := " with" (ppSpace colGt tactic)? withPosition((colGe inductionAlt)+)
+syntax inductionAlts := " with" (ppSpace colGt tactic)? withPosition((colGe inductionAlt)*)
 
 /--
 Assuming `x` is a variable in the local context with an inductive type,

src/Lean/Data/Json/Printer.lean

@@ -11,6 +11,22 @@ import Init.Data.List.Impl
 namespace Lean
 namespace Json
 
+set_option maxRecDepth 1024 in
+/--
+This table contains for each UTF-8 byte whether we need to escape a string that contains it.
+-/
+private def escapeTable : { xs : ByteArray // xs.size = 256 } :=
+  ⟨ByteArray.mk #[
+    1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, 1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,
+    0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,1, 0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,
+    0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0, 0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,
+    0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0, 0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,
+    1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, 1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,
+    1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, 1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,
+    1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, 1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,
+    1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, 1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1
+  ], by rfl⟩
+
 private def escapeAux (acc : String) (c : Char) : String :=
   -- escape ", \, \n and \r, keep all other characters ≥ 0x20 and render characters < 0x20 with \u
   if c = '"' then -- hack to prevent emacs from regarding the rest of the file as a string: "
@@ -39,8 +55,27 @@ private def escapeAux (acc : String) (c : Char) : String :=
     let d4 := Nat.digitChar (n % 16)
     acc ++ "\\u" |>.push d1 |>.push d2 |>.push d3 |>.push d4
 
+private def needEscape (s : String) : Bool :=
+  go s 0
+where
+  go (s : String) (i : Nat) : Bool :=
+    if h : i < s.utf8ByteSize then
+      let byte := s.getUtf8Byte i h
+      have h1 : byte.toNat < 256 := UInt8.toNat_lt_size byte
+      have h2 : escapeTable.val.size = 256 := escapeTable.property
+      if escapeTable.val.get byte.toNat (Nat.lt_of_lt_of_eq h1 h2.symm) == 0 then
+        go s (i + 1)
+      else
+        true
+    else
+      false
+
 def escape (s : String) (acc : String := "") : String :=
-  s.foldl escapeAux acc
+  -- If we don't have any characters that need to be escaped we can just append right away.
+  if needEscape s then
+    s.foldl escapeAux acc
+  else
+    acc ++ s
 
 def renderString (s : String) (acc : String := "") : String :=
   let acc := acc ++ "\""

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -362,9 +362,9 @@ partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit :=
   | `(tactic| intro $h:term $hs:term*) => evalTactic (← `(tactic| intro $h:term; intro $hs:term*))
   | _ => throwUnsupportedSyntax
 where
-  introStep (ref : Option Syntax) (n : Name) (typeStx? : Option Syntax := none) : TacticM Unit := do
+  introStep (ref? : Option Syntax) (n : Name) (typeStx? : Option Syntax := none) : TacticM Unit := do
     let fvarId ← liftMetaTacticAux fun mvarId => do
-      let (fvarId, mvarId) ← mvarId.intro n
+      let (fvarId, mvarId) ← withRef? ref? <| mvarId.intro n
       pure (fvarId, [mvarId])
     if let some typeStx := typeStx? then
       withMainContext do
@@ -374,9 +374,9 @@ where
         unless (← isDefEqGuarded type fvarType) do
           throwError "type mismatch at `intro {fvar}`{← mkHasTypeButIsExpectedMsg fvarType type}"
         liftMetaTactic fun mvarId => return [← mvarId.replaceLocalDeclDefEq fvarId type]
-    if let some stx := ref then
+    if let some ref := ref? then
       withMainContext do
-        Term.addLocalVarInfo stx (mkFVar fvarId)
+        Term.addLocalVarInfo ref (mkFVar fvarId)
 
 @[builtin_tactic Lean.Parser.Tactic.introMatch] def evalIntroMatch : Tactic := fun stx => do
   let matchAlts := stx[1]

src/Lean/Elab/Tactic/Classical.lean

@@ -24,11 +24,8 @@ def classical [Monad m] [MonadEnv m] [MonadFinally m] [MonadLiftT MetaM m] (t :
   finally
     modifyEnv Meta.instanceExtension.popScope
 
-@[builtin_tactic Lean.Parser.Tactic.classical]
-def evalClassical : Tactic := fun stx => do
-  match stx with
-  | `(tactic| classical $tacs:tacticSeq) =>
-     classical <| Elab.Tactic.evalTactic tacs
-  | _ => throwUnsupportedSyntax
+@[builtin_tactic Lean.Parser.Tactic.classical, builtin_incremental]
+def evalClassical : Tactic := fun stx =>
+  classical <| Term.withNarrowedArgTacticReuse (argIdx := 1) Elab.Tactic.evalTactic stx
 
 end Lean.Elab.Tactic

src/Lean/Elab/Tactic/Conv/Simp.lean

@@ -7,9 +7,10 @@ prelude
 import Lean.Elab.Tactic.Simp
 import Lean.Elab.Tactic.Split
 import Lean.Elab.Tactic.Conv.Basic
+import Lean.Elab.Tactic.SimpTrace
 
 namespace Lean.Elab.Tactic.Conv
-open Meta
+open Meta Tactic TryThis
 
 def applySimpResult (result : Simp.Result) : TacticM Unit := do
   if result.proof?.isNone then
@@ -23,6 +24,19 @@ def applySimpResult (result : Simp.Result) : TacticM Unit := do
   let (result, _) ← dischargeWrapper.with fun d? => simp lhs ctx (simprocs := simprocs) (discharge? := d?)
   applySimpResult result
 
+@[builtin_tactic Lean.Parser.Tactic.Conv.simpTrace] def evalSimpTrace : Tactic := fun stx => withMainContext do
+  match stx with
+  | `(conv| simp?%$tk $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]?) => do
+    let stx ← `(tactic| simp%$tk $cfg:optConfig $[$discharger]? $[only%$o]? $[[$args,*]]?)
+    let { ctx, simprocs, dischargeWrapper, .. } ← mkSimpContext stx (eraseLocal := false)
+    let lhs ← getLhs
+    let (result, stats) ← dischargeWrapper.with fun d? =>
+      simp lhs ctx (simprocs := simprocs) (discharge? := d?)
+    applySimpResult result
+    let stx ← mkSimpCallStx stx stats.usedTheorems
+    addSuggestion tk stx (origSpan? := ← getRef)
+  | _ => throwUnsupportedSyntax
+
 @[builtin_tactic Lean.Parser.Tactic.Conv.simpMatch] def evalSimpMatch : Tactic := fun _ => withMainContext do
   applySimpResult (← Split.simpMatch (← getLhs))
 
@@ -30,4 +44,15 @@ def applySimpResult (result : Simp.Result) : TacticM Unit := do
   let { ctx, .. } ← mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
   changeLhs (← Lean.Meta.dsimp (← getLhs) ctx).1
 
+@[builtin_tactic Lean.Parser.Tactic.Conv.dsimpTrace] def evalDSimpTrace : Tactic := fun stx => withMainContext do
+  match stx with
+  | `(conv| dsimp?%$tk $cfg:optConfig $[only%$o]? $[[$args,*]]?) =>
+    let stx ← `(tactic| dsimp%$tk $cfg:optConfig $[only%$o]? $[[$args,*]]?)
+    let { ctx, .. } ← mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
+    let (result, stats) ← Lean.Meta.dsimp (← getLhs) ctx
+    changeLhs result
+    let stx ← mkSimpCallStx stx stats.usedTheorems
+    addSuggestion tk stx (origSpan? := ← getRef)
+  | _ => throwUnsupportedSyntax
+
 end Lean.Elab.Tactic.Conv

src/Lean/Elab/Tactic/Induction.lean

@@ -258,11 +258,11 @@ private def saveAltVarsInfo (altMVarId : MVarId) (altStx : Syntax) (fvarIds : Ar
           i := i + 1
 
 open Language in
-def evalAlts (elimInfo : ElimInfo) (alts : Array Alt) (optPreTac : Syntax) (altStxs : Array Syntax)
+def evalAlts (elimInfo : ElimInfo) (alts : Array Alt) (optPreTac : Syntax) (altStxs? : Option (Array Syntax))
     (initialInfo : Info)
     (numEqs : Nat := 0) (numGeneralized : Nat := 0) (toClear : Array FVarId := #[])
     (toTag : Array (Ident × FVarId) := #[]) : TacticM Unit := do
-  let hasAlts := altStxs.size > 0
+  let hasAlts := altStxs?.isSome
   if hasAlts then
     -- default to initial state outside of alts
     -- HACK: because this node has the same span as the original tactic,
@@ -274,9 +274,7 @@ def evalAlts (elimInfo : ElimInfo) (alts : Array Alt) (optPreTac : Syntax) (altS
 where
   -- continuation in the correct info context
   goWithInfo := do
-    let hasAlts := altStxs.size > 0
-
-    if hasAlts then
+    if let some altStxs := altStxs? then
       if let some tacSnap := (← readThe Term.Context).tacSnap? then
         -- incrementality: create a new promise for each alternative, resolve current snapshot to
         -- them, eventually put each of them back in `Context.tacSnap?` in `applyAltStx`
@@ -309,7 +307,8 @@ where
 
   -- continuation in the correct incrementality context
   goWithIncremental (tacSnaps : Array (SnapshotBundle TacticParsedSnapshot)) := do
-    let hasAlts := altStxs.size > 0
+    let hasAlts := altStxs?.isSome
+    let altStxs := altStxs?.getD #[]
     let mut alts := alts
 
     -- initial sanity checks: named cases should be known, wildcards should be last
@@ -343,12 +342,12 @@ where
       let altName := getAltName altStx
       if let some i := alts.findFinIdx? (·.1 == altName) then
         -- cover named alternative
-        applyAltStx tacSnaps altStxIdx altStx alts[i]
+        applyAltStx tacSnaps altStxs altStxIdx altStx alts[i]
         alts := alts.eraseIdx i
       else if !alts.isEmpty && isWildcard altStx then
         -- cover all alternatives
         for alt in alts do
-          applyAltStx tacSnaps altStxIdx altStx alt
+          applyAltStx tacSnaps altStxs altStxIdx altStx alt
         alts := #[]
       else
         throwErrorAt altStx "unused alternative '{altName}'"
@@ -379,7 +378,7 @@ where
         altMVarIds.forM fun mvarId => admitGoal mvarId
 
   /-- Applies syntactic alternative to alternative goal. -/
-  applyAltStx tacSnaps altStxIdx altStx alt := withRef altStx do
+  applyAltStx tacSnaps altStxs altStxIdx altStx alt := withRef altStx do
     let { name := altName, info, mvarId := altMVarId } := alt
     -- also checks for unknown alternatives
     let numFields ← getAltNumFields elimInfo altName
@@ -476,7 +475,7 @@ private def generalizeVars (mvarId : MVarId) (stx : Syntax) (targets : Array Exp
 /--
 Given `inductionAlts` of the form
 ```
-syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)+)
+syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)*)
 ```
 Return an array containing its alternatives.
 -/
@@ -486,21 +485,30 @@ private def getAltsOfInductionAlts (inductionAlts : Syntax) : Array Syntax :=
 /--
 Given `inductionAlts` of the form
 ```
-syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)+)
+syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)*)
 ```
-runs `cont alts` where `alts` is an array containing all `inductionAlt`s while disabling incremental
-reuse if any other syntax changed.
+runs `cont (some alts)` where `alts` is an array containing all `inductionAlt`s while disabling incremental
+reuse if any other syntax changed. If there's no `with` clause, then runs `cont none`.
 -/
 private def withAltsOfOptInductionAlts (optInductionAlts : Syntax)
-    (cont : Array Syntax → TacticM α) : TacticM α :=
+    (cont : Option (Array Syntax) → TacticM α) : TacticM α :=
   Term.withNarrowedTacticReuse (stx := optInductionAlts) (fun optInductionAlts =>
     if optInductionAlts.isNone then
       -- if there are no alternatives, what to compare is irrelevant as there will be no reuse
       (mkNullNode #[], mkNullNode #[])
     else
+      -- if there are no alts, then use the `with` token for `inner` for a ref for messages
+      let altStxs := optInductionAlts[0].getArg 2
+      let inner := if altStxs.getNumArgs > 0 then altStxs else optInductionAlts[0][0]
       -- `with` and tactic applied to all branches must be unchanged for reuse
-      (mkNullNode optInductionAlts[0].getArgs[:2], optInductionAlts[0].getArg 2))
-    (fun alts => cont alts.getArgs)
+      (mkNullNode optInductionAlts[0].getArgs[:2], inner))
+    (fun alts? =>
+      if optInductionAlts.isNone then      -- no `with` clause
+        cont none
+      else if alts?.isOfKind nullKind then -- has alts
+        cont (some alts?.getArgs)
+      else                                 -- has `with` clause, but no alts
+        cont (some #[]))
 
 private def getOptPreTacOfOptInductionAlts (optInductionAlts : Syntax) : Syntax :=
   if optInductionAlts.isNone then mkNullNode else optInductionAlts[0][1]
@@ -518,7 +526,7 @@ private def expandMultiAlt? (alt : Syntax) : Option (Array Syntax) := Id.run do
 /--
 Given `inductionAlts` of the form
 ```
-syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)+)
+syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)*)
 ```
 Return `some inductionAlts'` if one of the alternatives have multiple LHSs, in the new `inductionAlts'`
 all alternatives have a single LHS.
@@ -700,10 +708,10 @@ def evalInduction : Tactic := fun stx =>
         -- unchanged
         -- everything up to the alternatives must be unchanged for reuse
         Term.withNarrowedArgTacticReuse (stx := stx) (argIdx := 4) fun optInductionAlts => do
-        withAltsOfOptInductionAlts optInductionAlts fun alts => do
+        withAltsOfOptInductionAlts optInductionAlts fun alts? => do
           let optPreTac := getOptPreTacOfOptInductionAlts optInductionAlts
           mvarId.assign result.elimApp
-          ElimApp.evalAlts elimInfo result.alts optPreTac alts initInfo (numGeneralized := n) (toClear := targetFVarIds)
+          ElimApp.evalAlts elimInfo result.alts optPreTac alts? initInfo (numGeneralized := n) (toClear := targetFVarIds)
           appendGoals result.others.toList
 where
   checkTargets (targets : Array Expr) : MetaM Unit := do

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

@@ -680,7 +680,7 @@ def omegaTactic (cfg : OmegaConfig) : TacticM Unit := do
 
 /-- The `omega` tactic, for resolving integer and natural linear arithmetic problems. This
 `TacticM Unit` frontend with default configuration can be used as an Aesop rule, for example via
-the tactic call `aesop (add 50% tactic Lean.Omega.omegaDefault)`. -/
+the tactic call `aesop (add 50% tactic Lean.Elab.Tactic.Omega.omegaDefault)`. -/
 def omegaDefault : TacticM Unit := omegaTactic {}
 
 @[builtin_tactic Lean.Parser.Tactic.omega]

src/Lean/Elab/Tactic/RCases.lean

@@ -507,7 +507,7 @@ partial def rintroCore (g : MVarId) (fs : FVarSubst) (clears : Array FVarId) (a
   match pat with
   | `(rintroPat| $pat:rcasesPat) =>
     let pat := (← RCasesPatt.parse pat).typed? ref ty?
-    let (v, g) ← g.intro (pat.name?.getD `_)
+    let (v, g) ← withRef pat.ref <| g.intro (pat.name?.getD `_)
     rcasesCore g fs clears (.fvar v) a pat cont
   | `(rintroPat| ($(pats)* $[: $ty?']?)) =>
     let ref := if pats.size == 1 then pat.raw else .missing

src/Lean/Meta/Tactic/Cases.lean

@@ -33,7 +33,7 @@ private def mkEqAndProof (lhs rhs : Expr) : MetaM (Expr × Expr) := do
   else
     pure (mkApp4 (mkConst ``HEq [u]) lhsType lhs rhsType rhs, mkApp2 (mkConst ``HEq.refl [u]) lhsType lhs)
 
-private partial def withNewEqs (targets targetsNew : Array Expr) (k : Array Expr → Array Expr → MetaM α) : MetaM α :=
+partial def withNewEqs (targets targetsNew : Array Expr) (k : Array Expr → Array Expr → MetaM α) : MetaM α :=
   let rec loop (i : Nat) (newEqs : Array Expr) (newRefls : Array Expr) := do
     if i < targets.size then
       let (newEqType, newRefl) ← mkEqAndProof targets[i]! targetsNew[i]!

src/Lean/Meta/Tactic/Grind.lean

@@ -23,7 +23,7 @@ import Lean.Meta.Tactic.Grind.Parser
 import Lean.Meta.Tactic.Grind.EMatchTheorem
 import Lean.Meta.Tactic.Grind.EMatch
 import Lean.Meta.Tactic.Grind.Main
-
+import Lean.Meta.Tactic.Grind.CasesMatch
 
 namespace Lean
 
@@ -34,10 +34,14 @@ builtin_initialize registerTraceClass `grind.eqc
 builtin_initialize registerTraceClass `grind.internalize
 builtin_initialize registerTraceClass `grind.ematch
 builtin_initialize registerTraceClass `grind.ematch.pattern
+builtin_initialize registerTraceClass `grind.ematch.pattern.search
 builtin_initialize registerTraceClass `grind.ematch.instance
 builtin_initialize registerTraceClass `grind.ematch.instance.assignment
 builtin_initialize registerTraceClass `grind.issues
 builtin_initialize registerTraceClass `grind.simp
+builtin_initialize registerTraceClass `grind.split
+builtin_initialize registerTraceClass `grind.split.candidate
+builtin_initialize registerTraceClass `grind.split.resolved
 
 /-! Trace options for `grind` developers -/
 builtin_initialize registerTraceClass `grind.debug
@@ -48,5 +52,6 @@ builtin_initialize registerTraceClass `grind.debug.proj
 builtin_initialize registerTraceClass `grind.debug.parent
 builtin_initialize registerTraceClass `grind.debug.final
 builtin_initialize registerTraceClass `grind.debug.forallPropagator
-
+builtin_initialize registerTraceClass `grind.debug.split
+builtin_initialize registerTraceClass `grind.debug.canon
 end Lean

src/Lean/Meta/Tactic/Grind/Canon.lean

@@ -22,7 +22,7 @@ to detect when two structurally different atoms are definitionally equal.
 The `grind` tactic, on the other hand, uses congruence closure. Moreover, types, type formers, proofs, and instances
 are considered supporting elements and are not factored into congruence detection.
 
-This module minimizes the number of `isDefEq` checks by comparing two terms `a` and `b` only if they instances,
+This module minimizes the number of `isDefEq` checks by comparing two terms `a` and `b` only if they are instances,
 types, or type formers and are the `i`-th arguments of two different `f`-applications. This approach is
 sufficient for the congruence closure procedure used by the `grind` tactic.
 
@@ -46,15 +46,35 @@ structure State where
   proofCanon : PHashMap Expr Expr := {}
   deriving Inhabited
 
+inductive CanonElemKind where
+  | /--
+    Type class instances are canonicalized using `TransparencyMode.instances`.
+    -/
+    instance
+  | /--
+    Types and Type formers are canonicalized using `TransparencyMode.default`.
+    Remark: propositions are just visited. We do not invoke `canonElemCore` for them.
+    -/
+    type
+  | /--
+    Implicit arguments that are not types, type formers, or instances, are canonicalized
+    using `TransparencyMode.reducible`
+    -/
+    implicit
+  deriving BEq
+
+def CanonElemKind.explain : CanonElemKind → String
+  | .instance => "type class instances"
+  | .type => "types (or type formers)"
+  | .implicit => "implicit arguments (which are not type class instances or types)"
+
 /--
 Helper function for canonicalizing `e` occurring as the `i`th argument of an `f`-application.
-`isInst` is true if `e` is an type class instance.
 
-Recall that we use `TransparencyMode.instances` for checking whether two instances are definitionally equal or not.
-Thus, if diagnostics are enabled, we also check them using `TransparencyMode.default`. If the result is different
+Thus, if diagnostics are enabled, we also re-check them using `TransparencyMode.default`. If the result is different
 we report to the user.
 -/
-def canonElemCore (f : Expr) (i : Nat) (e : Expr) (isInst : Bool) : StateT State MetaM Expr := do
+def canonElemCore (f : Expr) (i : Nat) (e : Expr) (kind : CanonElemKind) : StateT State MetaM Expr := do
   let s ← get
   if let some c := s.canon.find? e then
     return c
@@ -66,16 +86,19 @@ def canonElemCore (f : Expr) (i : Nat) (e : Expr) (isInst : Bool) : StateT State
       -- in general safe to replace `e` with `c` if `c` has more free variables than `e`.
       -- However, we don't revert previously canonicalized elements in the `grind` tactic.
       modify fun s => { s with canon := s.canon.insert e c }
+      trace[grind.debug.canon] "found {e} ===> {c}"
       return c
-    if isInst then
-      if (← isDiagnosticsEnabled <&&> pure (c.fvarsSubset e) <&&> (withDefault <| isDefEq e c)) then
+    if kind != .type then
+      if (← isTracingEnabledFor `grind.issues <&&> (withDefault <| isDefEq e c)) then
         -- TODO: consider storing this information in some structure that can be browsed later.
-        trace[grind.issues] "the following `grind` static elements are definitionally equal with `default` transparency, but not with `instances` transparency{indentExpr e}\nand{indentExpr c}"
+        trace[grind.issues] "the following {kind.explain} are definitionally equal with `default` transparency but not with a more restrictive transparency{indentExpr e}\nand{indentExpr c}"
+  trace[grind.debug.canon] "({f}, {i}) ↦ {e}"
   modify fun s => { s with canon := s.canon.insert e e, argMap := s.argMap.insert key (e::cs) }
   return e
 
-abbrev canonType (f : Expr) (i : Nat) (e : Expr) := withDefault <| canonElemCore f i e false
-abbrev canonInst (f : Expr) (i : Nat) (e : Expr) := withReducibleAndInstances <| canonElemCore f i e true
+abbrev canonType (f : Expr) (i : Nat) (e : Expr) := withDefault <| canonElemCore f i e .type
+abbrev canonInst (f : Expr) (i : Nat) (e : Expr) := withReducibleAndInstances <| canonElemCore f i e .instance
+abbrev canonImplicit (f : Expr) (i : Nat) (e : Expr) := withReducible <| canonElemCore f i e .implicit
 
 /--
 Return type for the `shouldCanon` function.
@@ -85,6 +108,8 @@ private inductive ShouldCanonResult where
     canonType
   | /- Nested instances are canonicalized. -/
     canonInst
+  | /- Implicit argument that is not an instance nor a type. -/
+    canonImplicit
   | /-
     Term is not a proof, type (former), nor an instance.
     Thus, it must be recursively visited by the canonizer.
@@ -92,6 +117,13 @@ private inductive ShouldCanonResult where
     visit
   deriving Inhabited
 
+instance : Repr ShouldCanonResult where
+  reprPrec r _ := match r with
+    | .canonType => "canonType"
+    | .canonInst => "canonInst"
+    | .canonImplicit => "canonImplicit"
+    | .visit => "visit"
+
 /--
 See comments at `ShouldCanonResult`.
 -/
@@ -102,7 +134,14 @@ def shouldCanon (pinfos : Array ParamInfo) (i : Nat) (arg : Expr) : MetaM Should
       return .canonInst
     else if pinfo.isProp then
       return .visit
-  if (← isTypeFormer arg) then
+    else if pinfo.isImplicit then
+      if (← isTypeFormer arg) then
+        return .canonType
+      else
+        return .canonImplicit
+  if (← isProp arg) then
+    return .visit
+  else if (← isTypeFormer arg) then
     return .canonType
   else
     return .visit
@@ -129,17 +168,19 @@ where
         else
           let pinfos := (← getFunInfo f).paramInfo
           let mut modified := false
-          let mut args := args
-          for i in [:args.size] do
-            let arg := args[i]!
+          let mut args := args.toVector
+          for h : i in [:args.size] do
+            let arg := args[i]
+            trace[grind.debug.canon] "[{repr (← shouldCanon pinfos i arg)}]: {arg} : {← inferType arg}"
             let arg' ← match (← shouldCanon pinfos i arg) with
             | .canonType  => canonType f i arg
             | .canonInst  => canonInst f i arg
+            | .canonImplicit => canonImplicit f i (← visit arg)
             | .visit      => visit arg
             unless ptrEq arg arg' do
-              args := args.set! i arg'
+              args := args.set i arg'
               modified := true
-          pure <| if modified then mkAppN f args else e
+          pure <| if modified then mkAppN f args.toArray else e
       | .forallE _ d b _ =>
         -- Recall that we have `ForallProp.lean`.
         let d' ← visit d
@@ -151,7 +192,8 @@ where
     return e'
 
 /-- Canonicalizes nested types, type formers, and instances in `e`. -/
-def canon (e : Expr) : StateT State MetaM Expr :=
+def canon (e : Expr) : StateT State MetaM Expr := do
+  trace[grind.debug.canon] "{e}"
   unsafe canonImpl e
 
 end Canon

src/Lean/Meta/Tactic/Grind/Cases.lean

@@ -36,14 +36,17 @@ def cases (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := mvarId.withConte
     let mut recursor := mkApp (mkAppN recursor indicesExpr) (mkFVar fvarId)
     let mut recursorType ← inferType recursor
     let mut mvarIdsNew := #[]
+    let mut idx := 1
     for _ in [:recursorInfo.numMinors] do
       let .forallE _ targetNew recursorTypeNew _ ← whnf recursorType
         | throwTacticEx `grind.cases mvarId "unexpected recursor type"
       recursorType := recursorTypeNew
-      let mvar ← mkFreshExprSyntheticOpaqueMVar targetNew tag
+      let tagNew := if recursorInfo.numMinors > 1 then Name.num tag idx else tag
+      let mvar ← mkFreshExprSyntheticOpaqueMVar targetNew tagNew
       recursor := mkApp recursor mvar
       let mvarIdNew ← mvar.mvarId!.tryClearMany (indices.push fvarId)
       mvarIdsNew := mvarIdsNew.push mvarIdNew
+      idx := idx + 1
     mvarId.assign recursor
     return mvarIdsNew.toList
   if recursorInfo.numIndices > 0 then

src/Lean/Meta/Tactic/Grind/CasesMatch.lean

@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Util
+import Lean.Meta.Tactic.Cases
+import Lean.Meta.Match.MatcherApp
+
+namespace Lean.Meta.Grind
+
+def casesMatch (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := mvarId.withContext do
+  let some app ← matchMatcherApp? e
+    | throwTacticEx `grind.casesMatch mvarId m!"`match`-expression expected{indentExpr e}"
+  let (motive, eqRefls) ← mkMotiveAndRefls app
+  let target ← mvarId.getType
+  let mut us := app.matcherLevels
+  if let some i := app.uElimPos? then
+    us := us.set! i (← getLevel target)
+  let splitterName := (← Match.getEquationsFor app.matcherName).splitterName
+  let splitterApp := mkConst splitterName us.toList
+  let splitterApp := mkAppN splitterApp app.params
+  let splitterApp := mkApp splitterApp motive
+  let splitterApp := mkAppN splitterApp app.discrs
+  let (mvars, _, _) ← forallMetaBoundedTelescope (← inferType splitterApp) app.alts.size (kind := .syntheticOpaque)
+  let splitterApp := mkAppN splitterApp mvars
+  let val := mkAppN splitterApp eqRefls
+  mvarId.assign val
+  updateTags mvars
+  return mvars.toList.map (·.mvarId!)
+where
+  mkMotiveAndRefls (app : MatcherApp) : MetaM (Expr × Array Expr) := do
+    let dummy := mkSort 0
+    let aux := mkApp (mkAppN e.getAppFn app.params) dummy
+    forallBoundedTelescope (← inferType aux) app.discrs.size fun xs _ => do
+    withNewEqs app.discrs xs fun eqs eqRefls => do
+      let type ← mvarId.getType
+      let type ← mkForallFVars eqs type
+      let motive ← mkLambdaFVars xs type
+      return (motive, eqRefls)
+
+  updateTags (mvars : Array Expr) : MetaM Unit := do
+    let tag ← mvarId.getTag
+    if mvars.size == 1 then
+      mvars[0]!.mvarId!.setTag tag
+    else
+      let mut idx := 1
+      for mvar in mvars do
+        mvar.mvarId!.setTag (Name.num tag idx)
+        idx := idx + 1
+
+end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Combinators.lean

@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Types
+
+namespace Lean.Meta.Grind
+
+/-!
+Combinators for manipulating `GrindTactic`s.
+TODO: a proper tactic language for `grind`.
+-/
+
+def GrindTactic := Goal → GrindM (Option (List Goal))
+
+def GrindTactic.try (x : GrindTactic) : GrindTactic := fun g => do
+  let some gs ← x g | return some [g]
+  return some gs
+
+def applyToAll (x : GrindTactic)  (goals : List Goal) : GrindM (List Goal) := do
+  go goals []
+where
+  go (goals : List Goal) (acc : List Goal) : GrindM (List Goal) := do
+    match goals with
+    | [] => return acc.reverse
+    | goal :: goals => match (← x goal) with
+      | none => go goals (goal :: acc)
+      | some goals' => go goals (goals' ++ acc)
+
+partial def GrindTactic.andThen (x y : GrindTactic) : GrindTactic := fun goal => do
+  let some goals ← x goal | return none
+  applyToAll y goals
+
+instance : AndThen GrindTactic where
+  andThen a b := GrindTactic.andThen a (b ())
+
+partial def GrindTactic.iterate (x : GrindTactic) : GrindTactic := fun goal => do
+  go [goal] []
+where
+  go (todo : List Goal) (result : List Goal) : GrindM (List Goal) := do
+    match todo with
+    | [] => return result
+    | goal :: todo =>
+      if let some goalsNew ← x goal then
+        go (goalsNew ++ todo) result
+      else
+        go todo (goal :: result)
+
+partial def GrindTactic.orElse (x y : GrindTactic) : GrindTactic := fun goal => do
+  let some goals ← x goal | y goal
+  return goals
+
+instance : OrElse GrindTactic where
+  orElse a b := GrindTactic.andThen a (b ())
+
+def toGrindTactic (f : GoalM Unit) : GrindTactic := fun goal => do
+  let goal ← GoalM.run' goal f
+  if goal.inconsistent then
+    return some []
+  else
+    return some [goal]
+
+def GrindTactic' := Goal → GrindM (List Goal)
+
+def GrindTactic'.toGrindTactic (x : GrindTactic') : GrindTactic := fun goal => do
+  let goals ← x goal
+  return some goals
+
+end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Core.lean

@@ -43,7 +43,7 @@ private def removeParents (root : Expr) : GoalM ParentSet := do
   for parent in parents do
     -- Recall that we may have `Expr.forallE` in `parents` because of `ForallProp.lean`
     if (← pure parent.isApp <&&> isCongrRoot parent) then
-      trace[grind.debug.parent] "remove: {parent}"
+      trace_goal[grind.debug.parent] "remove: {parent}"
       modify fun s => { s with congrTable := s.congrTable.erase { e := parent } }
   return parents
 
@@ -54,7 +54,7 @@ This is an auxiliary function performed while merging equivalence classes.
 private def reinsertParents (parents : ParentSet) : GoalM Unit := do
   for parent in parents do
     if (← pure parent.isApp <&&> isCongrRoot parent) then
-      trace[grind.debug.parent] "reinsert: {parent}"
+      trace_goal[grind.debug.parent] "reinsert: {parent}"
       addCongrTable parent
 
 /-- Closes the goal when `True` and `False` are in the same equivalence class. -/
@@ -91,9 +91,9 @@ private partial def addEqStep (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit
   let rhsNode ← getENode rhs
   if isSameExpr lhsNode.root rhsNode.root then
     -- `lhs` and `rhs` are already in the same equivalence class.
-    trace[grind.debug] "{← ppENodeRef lhs} and {← ppENodeRef rhs} are already in the same equivalence class"
+    trace_goal[grind.debug] "{← ppENodeRef lhs} and {← ppENodeRef rhs} are already in the same equivalence class"
     return ()
-  trace[grind.eqc] "{← if isHEq then mkHEq lhs rhs else mkEq lhs rhs}"
+  trace_goal[grind.eqc] "{← if isHEq then mkHEq lhs rhs else mkEq lhs rhs}"
   let lhsRoot ← getENode lhsNode.root
   let rhsRoot ← getENode rhsNode.root
   let mut valueInconsistency := false
@@ -118,11 +118,11 @@ private partial def addEqStep (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit
   unless (← isInconsistent) do
     if valueInconsistency then
       closeGoalWithValuesEq lhsRoot.self rhsRoot.self
-  trace[grind.debug] "after addEqStep, {← ppState}"
+  trace_goal[grind.debug] "after addEqStep, {← ppState}"
   checkInvariants
 where
   go (lhs rhs : Expr) (lhsNode rhsNode lhsRoot rhsRoot : ENode) (flipped : Bool) : GoalM Unit := do
-    trace[grind.debug] "adding {← ppENodeRef lhs} ↦ {← ppENodeRef rhs}"
+    trace_goal[grind.debug] "adding {← ppENodeRef lhs} ↦ {← ppENodeRef rhs}"
     /-
     We have the following `target?/proof?`
     `lhs -> ... -> lhsNode.root`
@@ -139,7 +139,7 @@ where
     }
     let parents ← removeParents lhsRoot.self
     updateRoots lhs rhsNode.root
-    trace[grind.debug] "{← ppENodeRef lhs} new root {← ppENodeRef rhsNode.root}, {← ppENodeRef (← getRoot lhs)}"
+    trace_goal[grind.debug] "{← ppENodeRef lhs} new root {← ppENodeRef rhsNode.root}, {← ppENodeRef (← getRoot lhs)}"
     reinsertParents parents
     setENode lhsNode.root { (← getENode lhsRoot.self) with -- We must retrieve `lhsRoot` since it was updated.
       next := rhsRoot.next
@@ -208,7 +208,7 @@ def addNewEq (lhs rhs proof : Expr) (generation : Nat) : GoalM Unit := do
 
 /-- Adds a new `fact` justified by the given proof and using the given generation. -/
 def add (fact : Expr) (proof : Expr) (generation := 0) : GoalM Unit := do
-  trace[grind.assert] "{fact}"
+  trace_goal[grind.assert] "{fact}"
   if (← isInconsistent) then return ()
   resetNewEqs
   let_expr Not p := fact

src/Lean/Meta/Tactic/Grind/Ctor.lean

@@ -9,14 +9,18 @@ import Lean.Meta.Tactic.Grind.Types
 namespace Lean.Meta.Grind
 
 private partial def propagateInjEqs (eqs : Expr) (proof : Expr) : GoalM Unit := do
+  -- Remark: we must use `shareCommon` before using `pushEq` and `pushHEq`.
+  -- This is needed because the result type of the injection theorem may allocate
   match_expr eqs with
   | And left right =>
     propagateInjEqs left (.proj ``And 0 proof)
     propagateInjEqs right (.proj ``And 1 proof)
-  | Eq _ lhs rhs    => pushEq lhs rhs proof
-  | HEq _ lhs _ rhs => pushHEq lhs rhs proof
+  | Eq _ lhs rhs    =>
+    pushEq (← shareCommon lhs) (← shareCommon rhs) proof
+  | HEq _ lhs _ rhs =>
+    pushHEq (← shareCommon lhs) (← shareCommon rhs) proof
   | _ =>
-   trace[grind.issues] "unexpected injectivity theorem result type{indentExpr eqs}"
+   trace_goal[grind.issues] "unexpected injectivity theorem result type{indentExpr eqs}"
    return ()
 
 /--

src/Lean/Meta/Tactic/Grind/EMatch.lean

@@ -51,6 +51,8 @@ structure Context where
   useMT : Bool := true
   /-- `EMatchTheorem` being processed. -/
   thm   : EMatchTheorem := default
+  /-- Initial application used to start E-matching -/
+  initApp : Expr := default
   deriving Inhabited
 
 /-- State for the E-matching monad -/
@@ -64,6 +66,9 @@ abbrev M := ReaderT Context $ StateRefT State GoalM
 def M.run' (x : M α) : GoalM α :=
   x {} |>.run' {}
 
+@[inline] private abbrev withInitApp (e : Expr) (x : M α) : M α :=
+  withReader (fun ctx => { ctx with initApp := e }) x
+
 /--
 Assigns `bidx := e` in `c`. If `bidx` is already assigned in `c`, we check whether
 `e` and `c.assignment[bidx]` are in the same equivalence class.
@@ -137,7 +142,8 @@ private partial def processMatch (c : Choice) (p : Expr) (e : Expr) : M Unit :=
   let mut curr := e
   repeat
     let n ← getENode curr
-    if n.generation <= maxGeneration
+    -- Remark: we use `<` because the instance generation is the maximum term generation + 1
+    if n.generation < maxGeneration
        -- uses heterogeneous equality or is the root of its congruence class
        && (n.heqProofs || n.isCongrRoot)
        && eqvFunctions pFn curr.getAppFn
@@ -155,7 +161,7 @@ private partial def processOffset (c : Choice) (pArg : Expr) (k : Nat) (e : Expr
   let mut curr := e
   repeat
     let n ← getENode curr
-    if n.generation <= maxGeneration then
+    if n.generation < maxGeneration then
       if let some (eArg, k') ← isOffset? curr |>.run then
         if k' < k then
           let c := c.updateGen n.generation
@@ -166,14 +172,14 @@ private partial def processOffset (c : Choice) (pArg : Expr) (k : Nat) (e : Expr
         else if k' > k then
           let eArg' := mkNatAdd eArg (mkNatLit (k' - k))
           let eArg' ← shareCommon (← canon eArg')
-          internalize eArg' n.generation
+          internalize eArg' (n.generation+1)
           if let some c ← matchArg? c pArg eArg' |>.run then
             pushChoice (c.updateGen n.generation)
       else if let some k' ← evalNat curr |>.run then
         if k' >= k then
           let eArg' := mkNatLit (k' - k)
           let eArg' ← shareCommon (← canon eArg')
-          internalize eArg' n.generation
+          internalize eArg' (n.generation+1)
           if let some c ← matchArg? c pArg eArg' |>.run then
             pushChoice (c.updateGen n.generation)
     curr ← getNext curr
@@ -186,21 +192,25 @@ private def processContinue (c : Choice) (p : Expr) : M Unit := do
   let maxGeneration ← getMaxGeneration
   for app in apps do
     let n ← getENode app
-    if n.generation <= maxGeneration
+    if n.generation < maxGeneration
        && (n.heqProofs || n.isCongrRoot) then
       if let some c ← matchArgs? c p app |>.run then
         let gen := n.generation
         let c := { c with gen := Nat.max gen c.gen }
         modify fun s => { s with choiceStack := c :: s.choiceStack }
 
-/-- Helper function for marking parts of `match`-equation theorem as "do-not-simplify" -/
-private partial def annotateMatchEqnType (prop : Expr) : M Expr := do
+/--
+Helper function for marking parts of `match`-equation theorem as "do-not-simplify"
+`initApp` is the match-expression used to instantiate the `match`-equation.
+-/
+private partial def annotateMatchEqnType (prop : Expr) (initApp : Expr) : M Expr := do
   if let .forallE n d b bi := prop then
     withLocalDecl n bi (← markAsDoNotSimp d) fun x => do
-      mkForallFVars #[x] (← annotateMatchEqnType (b.instantiate1 x))
+      mkForallFVars #[x] (← annotateMatchEqnType (b.instantiate1 x) initApp)
   else
     let_expr f@Eq α lhs rhs := prop | return prop
-    return mkApp3 f α (← markAsDoNotSimp lhs) rhs
+    -- See comment at `Grind.EqMatch`
+    return mkApp4 (mkConst ``Grind.EqMatch f.constLevels!) α (← markAsDoNotSimp lhs) rhs initApp
 
 /--
 Stores new theorem instance in the state.
@@ -212,9 +222,9 @@ private def addNewInstance (origin : Origin) (proof : Expr) (generation : Nat) :
     check proof
   let mut prop ← inferType proof
   if Match.isMatchEqnTheorem (← getEnv) origin.key then
-    prop ← annotateMatchEqnType prop
-  trace[grind.ematch.instance] "{← origin.pp}: {prop}"
-  addTheoremInstance proof prop generation
+    prop ← annotateMatchEqnType prop (← read).initApp
+  trace_goal[grind.ematch.instance] "{← origin.pp}: {prop}"
+  addTheoremInstance proof prop (generation+1)
 
 /--
 After processing a (multi-)pattern, use the choice assignment to instantiate the proof.
@@ -224,28 +234,30 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w
   let thm := (← read).thm
   unless (← markTheoremInstance thm.proof c.assignment) do
     return ()
-  trace[grind.ematch.instance.assignment] "{← thm.origin.pp}: {assignmentToMessageData c.assignment}"
+  trace_goal[grind.ematch.instance.assignment] "{← thm.origin.pp}: {assignmentToMessageData c.assignment}"
   let proof ← thm.getProofWithFreshMVarLevels
   let numParams := thm.numParams
   assert! c.assignment.size == numParams
   let (mvars, bis, _) ← forallMetaBoundedTelescope (← inferType proof) numParams
   if mvars.size != thm.numParams then
-    trace[grind.issues] "unexpected number of parameters at {← thm.origin.pp}"
+    trace_goal[grind.issues] "unexpected number of parameters at {← thm.origin.pp}"
     return ()
   -- Apply assignment
   for h : i in [:mvars.size] do
     let v := c.assignment[numParams - i - 1]!
     unless isSameExpr v unassigned do
       let mvarId := mvars[i].mvarId!
-      unless (← isDefEq (← mvarId.getType) (← inferType v) <&&> mvarId.checkedAssign v) do
-        trace[grind.issues] "type error constructing proof for {← thm.origin.pp}\nwhen assigning metavariable {mvars[i]} with {indentExpr v}"
+      let mvarIdType ← mvarId.getType
+      let vType ← inferType v
+      unless (← isDefEq mvarIdType vType <&&> mvarId.checkedAssign v) do
+        trace_goal[grind.issues] "type error constructing proof for {← thm.origin.pp}\nwhen assigning metavariable {mvars[i]} with {indentExpr v}\n{← mkHasTypeButIsExpectedMsg vType mvarIdType}"
         return ()
   -- Synthesize instances
   for mvar in mvars, bi in bis do
     if bi.isInstImplicit && !(← mvar.mvarId!.isAssigned) then
       let type ← inferType mvar
       unless (← synthesizeInstance mvar type) do
-        trace[grind.issues] "failed to synthesize instance when instantiating {← thm.origin.pp}{indentExpr type}"
+        trace_goal[grind.issues] "failed to synthesize instance when instantiating {← thm.origin.pp}{indentExpr type}"
         return ()
   let proof := mkAppN proof mvars
   if (← mvars.allM (·.mvarId!.isAssigned)) then
@@ -253,7 +265,7 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w
   else
     let mvars ← mvars.filterM fun mvar => return !(← mvar.mvarId!.isAssigned)
     if let some mvarBad ← mvars.findM? fun mvar => return !(← isProof mvar) then
-      trace[grind.issues] "failed to instantiate {← thm.origin.pp}, failed to instantiate non propositional argument with type{indentExpr (← inferType mvarBad)}"
+      trace_goal[grind.issues] "failed to instantiate {← thm.origin.pp}, failed to instantiate non propositional argument with type{indentExpr (← inferType mvarBad)}"
     let proof ← mkLambdaFVars (binderInfoForMVars := .default) mvars (← instantiateMVars proof)
     addNewInstance thm.origin proof c.gen
 where
@@ -262,17 +274,18 @@ where
     isDefEq x val
 
 /-- Process choice stack until we don't have more choices to be processed. -/
-private partial def processChoices : M Unit := do
-  unless (← get).choiceStack.isEmpty do
+private def processChoices : M Unit := do
+  let maxGeneration ← getMaxGeneration
+  while !(← get).choiceStack.isEmpty do
     checkSystem "ematch"
     if (← checkMaxInstancesExceeded) then return ()
     let c ← modifyGet fun s : State => (s.choiceStack.head!, { s with choiceStack := s.choiceStack.tail! })
-    match c.cnstrs with
-    | [] => instantiateTheorem c
-    | .match p e :: cnstrs => processMatch { c with cnstrs } p e
-    | .offset p k e :: cnstrs => processOffset { c with cnstrs } p k e
-    | .continue p :: cnstrs => processContinue { c with cnstrs } p
-    processChoices
+    if c.gen < maxGeneration then
+      match c.cnstrs with
+      | [] => instantiateTheorem c
+      | .match p e :: cnstrs => processMatch { c with cnstrs } p e
+      | .offset p k e :: cnstrs => processOffset { c with cnstrs } p k e
+      | .continue p :: cnstrs => processContinue { c with cnstrs } p
 
 private def main (p : Expr) (cnstrs : List Cnstr) : M Unit := do
   let some apps := (← getThe Goal).appMap.find? p.toHeadIndex
@@ -286,9 +299,10 @@ private def main (p : Expr) (cnstrs : List Cnstr) : M Unit := do
     let n ← getENode app
     if (n.heqProofs || n.isCongrRoot) &&
        (!useMT || n.mt == gmt) then
-      if let some c ← matchArgs? { cnstrs, assignment, gen := n.generation } p app |>.run then
-        modify fun s => { s with choiceStack := [c] }
-        processChoices
+      withInitApp app do
+        if let some c ← matchArgs? { cnstrs, assignment, gen := n.generation } p app |>.run then
+          modify fun s => { s with choiceStack := [c] }
+          processChoices
 
 def ematchTheorem (thm : EMatchTheorem) : M Unit := do
   if (← checkMaxInstancesExceeded) then return ()
@@ -327,7 +341,7 @@ def ematch : GoalM Unit := do
   let go (thms newThms : PArray EMatchTheorem) : EMatch.M Unit := do
     withReader (fun ctx => { ctx with useMT := true }) <| ematchTheorems thms
     withReader (fun ctx => { ctx with useMT := false }) <| ematchTheorems newThms
-  if (← checkMaxInstancesExceeded) then
+  if (← checkMaxInstancesExceeded <||> checkMaxEmatchExceeded) then
     return ()
   else
     go (← get).thms (← get).newThms |>.run'
@@ -335,17 +349,18 @@ def ematch : GoalM Unit := do
       thms         := s.thms ++ s.newThms
       newThms      := {}
       gmt          := s.gmt + 1
+      numEmatch    := s.numEmatch + 1
     }
 
 /-- Performs one round of E-matching, and assert new instances. -/
-def ematchAndAssert? (goal : Goal) : GrindM (Option (List Goal)) := do
+def ematchAndAssert : GrindTactic := fun goal => do
   let numInstances := goal.numInstances
   let goal ← GoalM.run' goal ematch
   if goal.numInstances == numInstances then
     return none
   assertAll goal
 
-def ematchStar (goal : Goal) : GrindM (List Goal) := do
-  iterate goal ematchAndAssert?
+def ematchStar : GrindTactic :=
+  ematchAndAssert.iterate
 
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean

@@ -5,12 +5,14 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Grind.Util
+import Init.Grind.Tactics
 import Lean.HeadIndex
 import Lean.PrettyPrinter
 import Lean.Util.FoldConsts
 import Lean.Util.CollectFVars
 import Lean.Meta.Basic
 import Lean.Meta.InferType
+import Lean.Meta.Eqns
 import Lean.Meta.Tactic.Grind.Util
 
 namespace Lean.Meta.Grind
@@ -37,9 +39,10 @@ def isOffsetPattern? (pat : Expr) : Option (Expr × Nat) := Id.run do
   let .lit (.natVal k) := k | none
   return some (pat, k)
 
-def preprocessPattern (pat : Expr) : MetaM Expr := do
+def preprocessPattern (pat : Expr) (normalizePattern := true) : MetaM Expr := do
   let pat ← instantiateMVars pat
   let pat ← unfoldReducible pat
+  let pat ← if normalizePattern then normalize pat else pure pat
   let pat ← detectOffsets pat
   let pat ← foldProjs pat
   return pat
@@ -54,22 +57,29 @@ inductive Origin where
   is the provided grind argument. The `id` is a unique identifier for the call.
   -/
   | stx (id : Name) (ref : Syntax)
-  | other
-  deriving Inhabited, Repr
+  /-- It is local, but we don't have a local hypothesis for it. -/
+  | local (id : Name)
+  deriving Inhabited, Repr, BEq
 
 /-- A unique identifier corresponding to the origin. -/
 def Origin.key : Origin → Name
   | .decl declName => declName
   | .fvar fvarId   => fvarId.name
   | .stx id _      => id
-  | .other         => `other
+  | .local id      => id
 
 def Origin.pp [Monad m] [MonadEnv m] [MonadError m] (o : Origin) : m MessageData := do
   match o with
   | .decl declName => return MessageData.ofConst (← mkConstWithLevelParams declName)
   | .fvar fvarId   => return mkFVar fvarId
   | .stx _ ref     => return ref
-  | .other         => return "[unknown]"
+  | .local id      => return id
+
+instance : BEq Origin where
+  beq a b := a.key == b.key
+
+instance : Hashable Origin where
+  hash a := hash a.key
 
 /-- A theorem for heuristic instantiation based on E-matching. -/
 structure EMatchTheorem where
@@ -91,8 +101,10 @@ structure EMatchTheorem where
 structure EMatchTheorems where
   /-- The key is a symbol from `EMatchTheorem.symbols`. -/
   private map : PHashMap Name (List EMatchTheorem) := {}
-  /-- Set of theorem names that have been inserted using `insert`. -/
-  private thmNames : PHashSet Name := {}
+  /-- Set of theorem ids that have been inserted using `insert`. -/
+  private origins : PHashSet Origin := {}
+  /-- Theorems that have been marked as erased -/
+  private erased  : PHashSet Origin := {}
   deriving Inhabited
 
 /--
@@ -107,12 +119,25 @@ def EMatchTheorems.insert (s : EMatchTheorems) (thm : EMatchTheorem) : EMatchThe
   let .const declName :: syms := thm.symbols
     | unreachable!
   let thm := { thm with symbols := syms }
-  let { map, thmNames } := s
-  let thmNames := thmNames.insert thm.origin.key
+  let { map, origins, erased } := s
+  let origins := origins.insert thm.origin
+  let erased := erased.erase thm.origin
   if let some thms := map.find? declName then
-    return { map := map.insert declName (thm::thms), thmNames }
+    return { map := map.insert declName (thm::thms), origins, erased }
   else
-    return { map := map.insert declName [thm], thmNames }
+    return { map := map.insert declName [thm], origins, erased }
+
+/-- Returns `true` if `s` contains a theorem with the given origin. -/
+def EMatchTheorems.contains (s : EMatchTheorems) (origin : Origin) : Bool :=
+  s.origins.contains origin
+
+/-- Mark the theorm with the given origin as `erased` -/
+def EMatchTheorems.erase (s : EMatchTheorems) (origin : Origin) : EMatchTheorems :=
+  { s with erased := s.erased.insert origin, origins := s.origins.erase origin }
+
+/-- Returns true if the theorem has been marked as erased. -/
+def EMatchTheorems.isErased (s : EMatchTheorems) (origin : Origin) : Bool :=
+  s.erased.contains origin
 
 /--
 Retrieves theorems from `s` associated with the given symbol. See `EMatchTheorem.insert`.
@@ -125,10 +150,6 @@ def EMatchTheorems.retrieve? (s : EMatchTheorems) (sym : Name) : Option (List EM
   else
     none
 
-/-- Returns `true` if `declName` is the name of a theorem that was inserted using `insert`. -/
-def EMatchTheorems.containsTheoremName (s : EMatchTheorems) (declName : Name) : Bool :=
-  s.thmNames.contains declName
-
 def EMatchTheorem.getProofWithFreshMVarLevels (thm : EMatchTheorem) : MetaM Expr := do
   if thm.proof.isConst && thm.levelParams.isEmpty then
     let declName := thm.proof.constName!
@@ -215,17 +236,19 @@ private def getPatternFn? (pattern : Expr) : Option Expr :=
     | _ => none
 
 /--
-Returns a bit-mask `mask` s.t. `mask[i]` is true if the the corresponding argument is
-- a type or type former, or
+Returns a bit-mask `mask` s.t. `mask[i]` is true if the corresponding argument is
+- a type (that is not a proposition) or type former, or
 - a proof, or
 - an instance implicit argument
 
 When `mask[i]`, we say the corresponding argument is a "support" argument.
 -/
-private def getPatternFunMask (f : Expr) (numArgs : Nat) : MetaM (Array Bool) := do
+def getPatternSupportMask (f : Expr) (numArgs : Nat) : MetaM (Array Bool) := do
   forallBoundedTelescope (← inferType f) numArgs fun xs _ => do
     xs.mapM fun x => do
-      if (← isTypeFormer x <||> isProof x) then
+      if (← isProp x) then
+        return false
+      else if (← isTypeFormer x <||> isProof x) then
         return true
       else
         return (← x.fvarId!.getDecl).binderInfo matches .instImplicit
@@ -240,16 +263,16 @@ private partial def go (pattern : Expr) (root := false) : M Expr := do
     else
       return mkOffsetPattern e k
   let some f := getPatternFn? pattern
-    | throwError "invalid pattern, (non-forbidden) application expected"
+    | throwError "invalid pattern, (non-forbidden) application expected{indentExpr pattern}"
   assert! f.isConst || f.isFVar
   saveSymbol f.toHeadIndex
-  let mut args := pattern.getAppArgs
-  let supportMask ← getPatternFunMask f args.size
-  for i in [:args.size] do
-    let arg := args[i]!
+  let mut args := pattern.getAppArgs.toVector
+  let supportMask ← getPatternSupportMask f args.size
+  for h : i in [:args.size] do
+    let arg := args[i]
     let isSupport := supportMask[i]?.getD false
-    args := args.set! i (← goArg arg isSupport)
-  return mkAppN f args
+    args := args.set i (← goArg arg isSupport)
+  return mkAppN f args.toArray
 where
   goArg (arg : Expr) (isSupport : Bool) : M Expr := do
     if !arg.hasLooseBVars then
@@ -276,6 +299,9 @@ def main (patterns : List Expr) : MetaM (List Expr × List HeadIndex × Std.Hash
   let (patterns, s) ← patterns.mapM go |>.run {}
   return (patterns, s.symbols.toList, s.bvarsFound)
 
+def normalizePattern (e : Expr) : M Expr := do
+  go e
+
 end NormalizePattern
 
 /--
@@ -400,38 +426,60 @@ private def ppParamsAt (proof : Expr) (numParams : Nat) (paramPos : List Nat) :
         msg := msg ++ m!"{x} : {← inferType x}"
     addMessageContextFull msg
 
+/--
+Creates an E-matching theorem for a theorem with proof `proof`, `numParams` parameters, and the given set of patterns.
+Pattern variables are represented using de Bruijn indices.
+-/
+def mkEMatchTheoremCore (origin : Origin) (levelParams : Array Name) (numParams : Nat) (proof : Expr) (patterns : List Expr) : MetaM EMatchTheorem := do
+  let (patterns, symbols, bvarFound) ← NormalizePattern.main patterns
+  trace[grind.ematch.pattern] "{MessageData.ofConst proof}: {patterns.map ppPattern}"
+  if let .missing pos ← checkCoverage proof numParams bvarFound then
+     let pats : MessageData := m!"{patterns.map ppPattern}"
+     throwError "invalid pattern(s) for `{← origin.pp}`{indentD pats}\nthe following theorem parameters cannot be instantiated:{indentD (← ppParamsAt proof numParams pos)}"
+  return {
+    proof, patterns, numParams, symbols
+    levelParams, origin
+  }
+
+private def getProofFor (declName : Name) : CoreM Expr := do
+  let .thmInfo info ← getConstInfo declName
+    | throwError "`{declName}` is not a theorem"
+  let us := info.levelParams.map mkLevelParam
+  return mkConst declName us
+
 /--
 Creates an E-matching theorem for `declName` with `numParams` parameters, and the given set of patterns.
 Pattern variables are represented using de Bruijn indices.
 -/
 def mkEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) : MetaM EMatchTheorem := do
-  let .thmInfo info ← getConstInfo declName
-    | throwError "`{declName}` is not a theorem, you cannot assign patterns to non-theorems for the `grind` tactic"
-  let us := info.levelParams.map mkLevelParam
-  let proof := mkConst declName us
-  let (patterns, symbols, bvarFound) ← NormalizePattern.main patterns
-  assert! symbols.all fun s => s matches .const _
-  trace[grind.ematch.pattern] "{MessageData.ofConst proof}: {patterns.map ppPattern}"
-  if let .missing pos ← checkCoverage proof numParams bvarFound then
-     let pats : MessageData := m!"{patterns.map ppPattern}"
-     throwError "invalid pattern(s) for `{declName}`{indentD pats}\nthe following theorem parameters cannot be instantiated:{indentD (← ppParamsAt proof numParams pos)}"
-  return {
-    proof, patterns, numParams, symbols
-    levelParams := #[]
-    origin      := .decl declName
-  }
+  mkEMatchTheoremCore (.decl declName) #[] numParams (← getProofFor declName) patterns
+
+/--
+Given a theorem with proof `proof` and type of the form `∀ (a_1 ... a_n), lhs = rhs`,
+creates an E-matching pattern for it using `addEMatchTheorem n [lhs]`
+If `normalizePattern` is true, it applies the `grind` simplification theorems and simprocs to the pattern.
+-/
+def mkEMatchEqTheoremCore (origin : Origin) (levelParams : Array Name) (proof : Expr) (normalizePattern : Bool) (useLhs : Bool) : MetaM EMatchTheorem := do
+  let (numParams, patterns) ← forallTelescopeReducing (← inferType proof) fun xs type => do
+    let (lhs, rhs) ← match_expr type with
+      | Eq _ lhs rhs => pure (lhs, rhs)
+      | Iff lhs rhs => pure (lhs, rhs)
+      | HEq _ lhs _ rhs => pure (lhs, rhs)
+      | _ => throwError "invalid E-matching equality theorem, conclusion must be an equality{indentExpr type}"
+    let pat := if useLhs then lhs else rhs
+    let pat ← preprocessPattern pat normalizePattern
+    return (xs.size, [pat.abstract xs])
+  mkEMatchTheoremCore origin levelParams numParams proof patterns
 
 /--
 Given theorem with name `declName` and type of the form `∀ (a_1 ... a_n), lhs = rhs`,
 creates an E-matching pattern for it using `addEMatchTheorem n [lhs]`
+
+If `normalizePattern` is true, it applies the `grind` simplification theorems and simprocs to the
+pattern.
 -/
-def mkEMatchEqTheorem (declName : Name) : MetaM EMatchTheorem := do
-  let info ← getConstInfo declName
-  let (numParams, patterns) ← forallTelescopeReducing info.type fun xs type => do
-    let_expr Eq _ lhs _ := type | throwError "invalid E-matching equality theorem, conclusion must be an equality{indentExpr type}"
-    let lhs ← preprocessPattern lhs
-    return (xs.size, [lhs.abstract xs])
-  mkEMatchTheorem declName numParams patterns
+def mkEMatchEqTheorem (declName : Name) (normalizePattern := true) (useLhs : Bool := true) : MetaM EMatchTheorem := do
+  mkEMatchEqTheoremCore (.decl declName) #[] (← getProofFor declName) normalizePattern useLhs
 
 /--
 Adds an E-matching theorem to the environment.
@@ -451,4 +499,227 @@ def addEMatchEqTheorem (declName : Name) : MetaM Unit := do
 def getEMatchTheorems : CoreM EMatchTheorems :=
   return ematchTheoremsExt.getState (← getEnv)
 
+inductive TheoremKind where
+  | eqLhs | eqRhs | eqBoth | fwd | bwd | default
+  deriving Inhabited, BEq
+
+private def TheoremKind.toAttribute : TheoremKind → String
+  | .eqLhs   => "[grind =]"
+  | .eqRhs   => "[grind =_]"
+  | .eqBoth  => "[grind _=_]"
+  | .fwd     => "[grind →]"
+  | .bwd     => "[grind ←]"
+  | .default => "[grind]"
+
+private def TheoremKind.explainFailure : TheoremKind → String
+  | .eqLhs   => "failed to find pattern in the left-hand side of the theorem's conclusion"
+  | .eqRhs   => "failed to find pattern in the right-hand side of the theorem's conclusion"
+  | .eqBoth  => unreachable! -- eqBoth is a macro
+  | .fwd     => "failed to find patterns in the antecedents of the theorem"
+  | .bwd     => "failed to find patterns in the theorem's conclusion"
+  | .default => "failed to find patterns"
+
+/-- Returns the types of `xs` that are propositions. -/
+private def getPropTypes (xs : Array Expr) : MetaM (Array Expr) :=
+  xs.filterMapM fun x => do
+    let type ← inferType x
+    if (← isProp type) then return some type else return none
+
+/-- State for the (pattern) `CollectorM` monad -/
+private structure Collector.State where
+  /-- Pattern found so far. -/
+  patterns  : Array Expr := #[]
+  done      : Bool := false
+
+private structure Collector.Context where
+  proof : Expr
+  xs    : Array Expr
+
+/-- Monad for collecting patterns for a theorem. -/
+private abbrev CollectorM := ReaderT Collector.Context $ StateRefT Collector.State NormalizePattern.M
+
+/-- Similar to `getPatternFn?`, but operates on expressions that do not contain loose de Bruijn variables. -/
+private def isPatternFnCandidate (f : Expr) : CollectorM Bool := do
+  match f with
+  | .const declName _ => return !isForbidden declName
+  | .fvar .. => return !(← read).xs.contains f
+  | _ => return false
+
+private def addNewPattern (p : Expr) : CollectorM Unit := do
+  trace[grind.ematch.pattern.search] "found pattern: {ppPattern p}"
+  let bvarsFound := (← getThe NormalizePattern.State).bvarsFound
+  let done := (← checkCoverage (← read).proof (← read).xs.size bvarsFound) matches .ok
+  if done then
+    trace[grind.ematch.pattern.search] "found full coverage"
+  modify fun s => { s with patterns := s.patterns.push p, done }
+
+private partial def collect (e : Expr) : CollectorM Unit := do
+  if (← get).done then return ()
+  match e with
+  | .app .. =>
+    let f := e.getAppFn
+    if (← isPatternFnCandidate f) then
+      let saved ← getThe NormalizePattern.State
+      try
+        trace[grind.ematch.pattern.search] "candidate: {e}"
+        let p := e.abstract (← read).xs
+        unless p.hasLooseBVars do
+          trace[grind.ematch.pattern.search] "skip, does not contain pattern variables"
+          return ()
+        let p ← NormalizePattern.normalizePattern p
+        if saved.bvarsFound.size < (← getThe NormalizePattern.State).bvarsFound.size then
+          addNewPattern p
+          return ()
+        trace[grind.ematch.pattern.search] "skip, no new variables covered"
+        -- restore state and continue search
+        set saved
+      catch _ =>
+        trace[grind.ematch.pattern.search] "skip, exception during normalization"
+        -- restore state and continue search
+        set saved
+    let args := e.getAppArgs
+    for arg in args, flag in (← NormalizePattern.getPatternSupportMask f args.size) do
+      unless flag do
+        collect arg
+  | .forallE _ d b _ =>
+    if (← pure e.isArrow <&&> isProp d <&&> isProp b) then
+      collect d
+      collect b
+  | _ => return ()
+
+private def collectPatterns? (proof : Expr) (xs : Array Expr) (searchPlaces : Array Expr) : MetaM (Option (List Expr × List HeadIndex)) := do
+  let go : CollectorM (Option (List Expr)) := do
+    for place in searchPlaces do
+      let place ← preprocessPattern place
+      collect place
+      if (← get).done then
+        return some ((← get).patterns.toList)
+    return none
+  let (some ps, s) ← go { proof, xs } |>.run' {} |>.run {}
+    | return none
+  return some (ps, s.symbols.toList)
+
+def mkEMatchTheoremWithKind? (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : TheoremKind) : MetaM (Option EMatchTheorem) := do
+  if kind == .eqLhs then
+    return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := false) (useLhs := true))
+  else if kind == .eqRhs then
+    return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := false) (useLhs := false))
+  let type ← inferType proof
+  forallTelescopeReducing type fun xs type => do
+    let searchPlaces ← match kind with
+      | .fwd =>
+        let ps ← getPropTypes xs
+        if ps.isEmpty then
+          throwError "invalid `grind` forward theorem, theorem `{← origin.pp}` does not have propositional hypotheses"
+        pure ps
+      | .bwd => pure #[type]
+      | .default => pure <| #[type] ++ (← getPropTypes xs)
+      | _ => unreachable!
+    go xs searchPlaces
+where
+  go (xs : Array Expr) (searchPlaces : Array Expr) : MetaM (Option EMatchTheorem) := do
+    let some (patterns, symbols) ← collectPatterns? proof xs searchPlaces
+      | return none
+    let numParams := xs.size
+    trace[grind.ematch.pattern] "{← origin.pp}: {patterns.map ppPattern}"
+    return some {
+      proof, patterns, numParams, symbols
+      levelParams, origin
+    }
+
+private def getKind (stx : Syntax) : TheoremKind :=
+  if stx[1].isNone then
+    .default
+  else if stx[1][0].getKind == ``Parser.Attr.grindEq then
+    .eqLhs
+  else if stx[1][0].getKind == ``Parser.Attr.grindFwd then
+    .fwd
+  else if stx[1][0].getKind == ``Parser.Attr.grindEqRhs then
+    .eqRhs
+  else if stx[1][0].getKind == ``Parser.Attr.grindEqBoth then
+    .eqBoth
+  else
+    .bwd
+
+private def addGrindEqAttr (declName : Name) (attrKind : AttributeKind) (thmKind : TheoremKind) (useLhs := true) : MetaM Unit := do
+  if (← getConstInfo declName).isTheorem then
+    ematchTheoremsExt.add (← mkEMatchEqTheorem declName (normalizePattern := true) (useLhs := useLhs)) attrKind
+  else if let some eqns ← getEqnsFor? declName then
+    unless useLhs do
+      throwError "`{declName}` is a definition, you must only use the left-hand side for extracting patterns"
+    for eqn in eqns do
+      ematchTheoremsExt.add (← mkEMatchEqTheorem eqn) attrKind
+  else
+    throwError s!"`{thmKind.toAttribute}` attribute can only be applied to equational theorems or function definitions"
+
+private def addGrindAttr (declName : Name) (attrKind : AttributeKind) (thmKind : TheoremKind) : MetaM Unit := do
+  if thmKind == .eqLhs then
+    addGrindEqAttr declName attrKind thmKind (useLhs := true)
+  else if thmKind == .eqRhs then
+    addGrindEqAttr declName attrKind thmKind (useLhs := false)
+  else if thmKind == .eqBoth then
+    addGrindEqAttr declName attrKind thmKind (useLhs := true)
+    addGrindEqAttr declName attrKind thmKind (useLhs := false)
+  else if !(← getConstInfo declName).isTheorem then
+    addGrindEqAttr declName attrKind thmKind
+  else
+    let some thm ← mkEMatchTheoremWithKind? (.decl declName) #[] (← getProofFor declName) thmKind
+      | throwError "`@{thmKind.toAttribute} theorem {declName}` {thmKind.explainFailure}, consider using different options or the `grind_pattern` command"
+    ematchTheoremsExt.add thm attrKind
+
+builtin_initialize
+  registerBuiltinAttribute {
+    name := `grind
+    descr :=
+      "The `[grind]` attribute is used to annotate declarations.\
+      \
+      When applied to an equational theorem, `[grind =]`, `[grind =_]`, or `[grind _=_]`\
+      will mark the theorem for use in heuristic instantiations by the `grind` tactic,
+      using respectively the left-hand side, the right-hand side, or both sides of the theorem.\
+      When applied to a function, `[grind =]` automatically annotates the equational theorems associated with that function.\
+      When applied to a theorem `[grind ←]` will instantiate the theorem whenever it encounters the conclusion of the theorem
+      (that is, it will use the theorem for backwards reasoning).\
+      When applied to a theorem `[grind →]` will instantiate the theorem whenever it encounters sufficiently many of the propositional hypotheses
+      (that is, it will use the theorem for forwards reasoning).\
+      \
+      The attribute `[grind]` by itself will effectively try `[grind ←]` (if the conclusion is sufficient for instantiation) and then `[grind →]`.\
+      \
+      The `grind` tactic utilizes annotated theorems to add instances of matching patterns into the local context during proof search.\
+      For example, if a theorem `@[grind =] theorem foo_idempotent : foo (foo x) = foo x` is annotated,\
+      `grind` will add an instance of this theorem to the local context whenever it encounters the pattern `foo (foo x)`."
+    applicationTime := .afterCompilation
+    add := fun declName stx attrKind => do
+      addGrindAttr declName attrKind (getKind stx) |>.run' {}
+    erase := fun declName => MetaM.run' do
+      /-
+      Remark: consider the following example
+      ```
+      attribute [grind] foo  -- ok
+      attribute [-grind] foo.eqn_2  -- ok
+      attribute [-grind] foo  -- error
+      ```
+      One may argue that the correct behavior should be
+      ```
+      attribute [grind] foo  -- ok
+      attribute [-grind] foo.eqn_2  -- error
+      attribute [-grind] foo  -- ok
+      ```
+      -/
+      let throwErr := throwError "`{declName}` is not marked with the `[grind]` attribute"
+      let info ← getConstInfo declName
+      if !info.isTheorem then
+        if let some eqns ← getEqnsFor? declName then
+           let s := ematchTheoremsExt.getState (← getEnv)
+           unless eqns.all fun eqn => s.contains (.decl eqn) do
+             throwErr
+           modifyEnv fun env => ematchTheoremsExt.modifyState env fun s =>
+             eqns.foldl (init := s) fun s eqn => s.erase (.decl eqn)
+        else
+          throwErr
+      else
+        unless ematchTheoremsExt.getState (← getEnv) |>.contains (.decl declName) do
+          throwErr
+        modifyEnv fun env => ematchTheoremsExt.modifyState env fun s => s.erase (.decl declName)
+  }
+
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/ForallProp.lean

@@ -15,20 +15,88 @@ If `parent` is a projection-application `proj_i c`,
 check whether the root of the equivalence class containing `c` is a constructor-application `ctor ... a_i ...`.
 If so, internalize the term `proj_i (ctor ... a_i ...)` and add the equality `proj_i (ctor ... a_i ...) = a_i`.
 -/
-def propagateForallProp (parent : Expr) : GoalM Unit := do
-  let .forallE n p q bi := parent | return ()
-  trace[grind.debug.forallPropagator] "{parent}"
-  unless (← isEqTrue p) do return ()
-  trace[grind.debug.forallPropagator] "isEqTrue, {parent}"
-  let h₁ ← mkEqTrueProof p
-  let qh₁ := q.instantiate1 (mkApp2 (mkConst ``of_eq_true) p h₁)
-  let r ← simp qh₁
-  let q := mkLambda n bi p q
-  let q' := r.expr
-  internalize q' (← getGeneration parent)
-  trace[grind.debug.forallPropagator] "q': {q'} for{indentExpr parent}"
-  let h₂ ← r.getProof
-  let h := mkApp5 (mkConst ``Lean.Grind.forall_propagator) p q q' h₁ h₂
-  pushEq parent q' h
+def propagateForallPropUp (e : Expr) : GoalM Unit := do
+  let .forallE n p q bi := e | return ()
+  trace_goal[grind.debug.forallPropagator] "{e}"
+  if !q.hasLooseBVars then
+    propagateImpliesUp p q
+  else
+    unless (← isEqTrue p) do return
+    trace_goal[grind.debug.forallPropagator] "isEqTrue, {e}"
+    let h₁ ← mkEqTrueProof p
+    let qh₁ := q.instantiate1 (mkApp2 (mkConst ``of_eq_true) p h₁)
+    let r ← simp qh₁
+    let q := mkLambda n bi p q
+    let q' := r.expr
+    internalize q' (← getGeneration e)
+    trace_goal[grind.debug.forallPropagator] "q': {q'} for{indentExpr e}"
+    let h₂ ← r.getProof
+    let h := mkApp5 (mkConst ``Lean.Grind.forall_propagator) p q q' h₁ h₂
+    pushEq e q' h
+where
+  propagateImpliesUp (a b : Expr) : GoalM Unit := do
+    unless (← alreadyInternalized b) do return ()
+    if (← isEqFalse a) then
+      -- a = False → (a → b) = True
+      pushEqTrue e <| mkApp3 (mkConst ``Grind.imp_eq_of_eq_false_left) a b (← mkEqFalseProof a)
+    else if (← isEqTrue a) then
+      -- a = True → (a → b) = b
+      pushEq e b <| mkApp3 (mkConst ``Grind.imp_eq_of_eq_true_left) a b (← mkEqTrueProof a)
+    else if (← isEqTrue b) then
+      -- b = True → (a → b) = True
+      pushEqTrue e <| mkApp3 (mkConst ``Grind.imp_eq_of_eq_true_right) a b (← mkEqTrueProof b)
+
+private def isEqTrueHyp? (proof : Expr) : Option FVarId := Id.run do
+  let_expr eq_true _ p := proof | return none
+  let .fvar fvarId := p | return none
+  return some fvarId
+
+/-- Similar to `mkEMatchTheoremWithKind?`, but swallow any exceptions. -/
+private def mkEMatchTheoremWithKind'? (origin : Origin) (proof : Expr) (kind : TheoremKind) : MetaM (Option EMatchTheorem) := do
+  try
+    mkEMatchTheoremWithKind? origin #[] proof kind
+  catch _ =>
+    return none
+
+private def addLocalEMatchTheorems (e : Expr) : GoalM Unit := do
+  let proof ← mkEqTrueProof e
+  let origin ← if let some fvarId := isEqTrueHyp? proof then
+    pure <| .fvar fvarId
+  else
+    let idx ← modifyGet fun s => (s.nextThmIdx, { s with nextThmIdx := s.nextThmIdx + 1 })
+    pure <| .local ((`local).appendIndexAfter idx)
+  let proof := mkApp2 (mkConst ``of_eq_true) e proof
+  let size := (← get).newThms.size
+  let gen ← getGeneration e
+  -- TODO: we should have a flag for collecting all unary patterns in a local theorem
+  if let some thm ← mkEMatchTheoremWithKind'? origin proof .fwd then
+    activateTheorem thm gen
+  if let some thm ← mkEMatchTheoremWithKind'? origin proof .bwd then
+    activateTheorem thm gen
+  if (← get).newThms.size == size then
+    if let some thm ← mkEMatchTheoremWithKind'? origin proof .default then
+      activateTheorem thm gen
+  if (← get).newThms.size == size then
+    trace[grind.issues] "failed to create E-match local theorem for{indentExpr e}"
+
+def propagateForallPropDown (e : Expr) : GoalM Unit := do
+  let .forallE n a b bi := e | return ()
+  if (← isEqFalse e) then
+    if b.hasLooseBVars then
+      let α := a
+      let p := b
+      -- `e` is of the form `∀ x : α, p x`
+      -- Add fact `∃ x : α, ¬ p x`
+      let u ← getLevel α
+      let prop := mkApp2 (mkConst ``Exists [u]) α (mkLambda n bi α (mkNot p))
+      let proof := mkApp3 (mkConst ``Grind.of_forall_eq_false [u]) α (mkLambda n bi α p) (← mkEqFalseProof e)
+      addNewFact proof prop (← getGeneration e)
+    else
+      let h ← mkEqFalseProof e
+      pushEqTrue a <| mkApp3 (mkConst ``Grind.eq_true_of_imp_eq_false) a b h
+      pushEqFalse b <| mkApp3 (mkConst ``Grind.eq_false_of_imp_eq_false) a b h
+  else if (← isEqTrue e) then
+    if b.hasLooseBVars then
+      addLocalEMatchTheorems e
 
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Internalize.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Grind.Util
+import Init.Grind.Lemmas
 import Lean.Meta.LitValues
 import Lean.Meta.Match.MatcherInfo
 import Lean.Meta.Match.MatchEqsExt
@@ -22,15 +23,19 @@ def addCongrTable (e : Expr) : GoalM Unit := do
     let g := e'.getAppFn
     unless isSameExpr f g do
       unless (← hasSameType f g) do
-        trace[grind.issues] "found congruence between{indentExpr e}\nand{indentExpr e'}\nbut functions have different types"
+        trace_goal[grind.issues] "found congruence between{indentExpr e}\nand{indentExpr e'}\nbut functions have different types"
         return ()
-    trace[grind.debug.congr] "{e} = {e'}"
+    trace_goal[grind.debug.congr] "{e} = {e'}"
     pushEqHEq e e' congrPlaceholderProof
     let node ← getENode e
     setENode e { node with congr := e' }
   else
     modify fun s => { s with congrTable := s.congrTable.insert { e } }
 
+/--
+Given an application `e` of the form `f a_1 ... a_n`,
+adds entry `f ↦ e` to `appMap`. Recall that `appMap` is a multi-map.
+-/
 private def updateAppMap (e : Expr) : GoalM Unit := do
   let key := e.toHeadIndex
   modify fun s => { s with
@@ -40,6 +45,50 @@ private def updateAppMap (e : Expr) : GoalM Unit := do
       s.appMap.insert key [e]
   }
 
+/-- Inserts `e` into the list of case-split candidates. -/
+private def addSplitCandidate (e : Expr) : GoalM Unit := do
+  trace_goal[grind.split.candidate] "{e}"
+  modify fun s => { s with splitCandidates := e :: s.splitCandidates }
+
+-- TODO: add attribute to make this extensible
+private def forbiddenSplitTypes := [``Eq, ``HEq, ``True, ``False]
+
+/-- Inserts `e` into the list of case-split candidates if applicable. -/
+private def checkAndAddSplitCandidate (e : Expr) : GoalM Unit := do
+  unless e.isApp do return ()
+  if (← getConfig).splitIte && (e.isIte || e.isDIte) then
+    addSplitCandidate e
+    return ()
+  if (← getConfig).splitMatch then
+    if (← isMatcherApp e) then
+      if let .reduced _ ← reduceMatcher? e then
+        -- When instantiating `match`-equations, we add `match`-applications that can be reduced,
+        -- and consequently don't need to be splitted.
+        return ()
+      else
+        addSplitCandidate e
+        return ()
+  let .const declName _  := e.getAppFn | return ()
+    if forbiddenSplitTypes.contains declName then return ()
+    -- We should have a mechanism for letting users to select types to case-split.
+    -- Right now, we just consider inductive predicates that are not in the forbidden list
+    if (← getConfig).splitIndPred then
+      if (← isInductivePredicate declName) then
+        addSplitCandidate e
+
+/--
+If `e` is a `cast`-like term (e.g., `cast h a`), add `HEq e a` to the to-do list.
+It could be an E-matching theorem, but we want to ensure it is always applied since
+we want to rely on the fact that `cast h a` and `a` are in the same equivalence class.
+-/
+private def pushCastHEqs (e : Expr) : GoalM Unit := do
+  match_expr e with
+  | f@cast α β h a => pushHEq e a (mkApp4 (mkConst ``cast_heq f.constLevels!) α β h a)
+  | f@Eq.rec α a motive v b h => pushHEq e v (mkApp6 (mkConst ``Grind.eqRec_heq f.constLevels!) α a motive v b h)
+  | f@Eq.ndrec α a motive v b h => pushHEq e v (mkApp6 (mkConst ``Grind.eqNDRec_heq f.constLevels!) α a motive v b h)
+  | f@Eq.recOn α a motive b h v => pushHEq e v (mkApp6 (mkConst ``Grind.eqRecOn_heq f.constLevels!) α a motive b h v)
+  | _ => return ()
+
 mutual
 /-- Internalizes the nested ground terms in the given pattern. -/
 private partial def internalizePattern (pattern : Expr) (generation : Nat) : GoalM Expr := do
@@ -52,12 +101,12 @@ private partial def internalizePattern (pattern : Expr) (generation : Nat) : Goa
   else pattern.withApp fun f args => do
     return mkAppN f (← args.mapM (internalizePattern · generation))
 
-private partial def activateTheorem (thm : EMatchTheorem) (generation : Nat) : GoalM Unit := do
+partial def activateTheorem (thm : EMatchTheorem) (generation : Nat) : GoalM Unit := do
   -- Recall that we use the proof as part of the key for a set of instances found so far.
   -- We don't want to use structural equality when comparing keys.
   let proof ← shareCommon thm.proof
   let thm := { thm with proof, patterns := (← thm.patterns.mapM (internalizePattern · generation)) }
-  trace[grind.ematch] "activated `{thm.origin.key}`, {thm.patterns.map ppPattern}"
+  trace_goal[grind.ematch] "activated `{thm.origin.key}`, {thm.patterns.map ppPattern}"
   modify fun s => { s with newThms := s.newThms.push thm }
 
 /--
@@ -71,47 +120,54 @@ private partial def addMatchEqns (f : Expr) (generation : Nat) : GoalM Unit := d
   if (← get).matchEqNames.contains declName then return ()
   modify fun s => { s with matchEqNames := s.matchEqNames.insert declName }
   for eqn in (← Match.getEquationsFor declName).eqnNames do
-    activateTheorem (← mkEMatchEqTheorem eqn) generation
+    -- We disable pattern normalization to prevent the `match`-expression to be reduced.
+    activateTheorem (← mkEMatchEqTheorem eqn (normalizePattern := false)) generation
 
 private partial def activateTheoremPatterns (fName : Name) (generation : Nat) : GoalM Unit := do
   if let some (thms, thmMap) := (← get).thmMap.retrieve? fName then
     modify fun s => { s with thmMap }
     let appMap := (← get).appMap
     for thm in thms do
-      let symbols := thm.symbols.filter fun sym => !appMap.contains sym
-      let thm := { thm with symbols }
-      match symbols with
-      | [] => activateTheorem thm generation
-      | _ =>
-        trace[grind.ematch] "reinsert `{thm.origin.key}`"
-        modify fun s => { s with thmMap := s.thmMap.insert thm }
+      unless (← get).thmMap.isErased thm.origin do
+        let symbols := thm.symbols.filter fun sym => !appMap.contains sym
+        let thm := { thm with symbols }
+        match symbols with
+        | [] => activateTheorem thm generation
+        | _ =>
+          trace_goal[grind.ematch] "reinsert `{thm.origin.key}`"
+          modify fun s => { s with thmMap := s.thmMap.insert thm }
 
 partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do
   if (← alreadyInternalized e) then return ()
-  trace[grind.internalize] "{e}"
+  trace_goal[grind.internalize] "{e}"
   match e with
   | .bvar .. => unreachable!
   | .sort .. => return ()
   | .fvar .. | .letE .. | .lam .. =>
     mkENodeCore e (ctor := false) (interpreted := false) (generation := generation)
-  | .forallE _ d _ _ =>
+  | .forallE _ d b _ =>
     mkENodeCore e (ctor := false) (interpreted := false) (generation := generation)
     if (← isProp d <&&> isProp e) then
       internalize d generation
       registerParent e d
+      unless b.hasLooseBVars do
+        internalize b generation
+        registerParent e b
       propagateUp e
   | .lit .. | .const .. =>
     mkENode e generation
   | .mvar ..
   | .mdata ..
   | .proj .. =>
-    trace[grind.issues] "unexpected term during internalization{indentExpr e}"
+    trace_goal[grind.issues] "unexpected term during internalization{indentExpr e}"
     mkENodeCore e (ctor := false) (interpreted := false) (generation := generation)
   | .app .. =>
     if (← isLitValue e) then
       -- We do not want to internalize the components of a literal value.
       mkENode e generation
     else e.withApp fun f args => do
+      checkAndAddSplitCandidate e
+      pushCastHEqs e
       addMatchEqns f generation
       if f.isConstOf ``Lean.Grind.nestedProof && args.size == 2 then
         -- We only internalize the proposition. We can skip the proof because of

src/Lean/Meta/Tactic/Grind/Intro.lean

@@ -11,6 +11,7 @@ import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Cases
 import Lean.Meta.Tactic.Grind.Injection
 import Lean.Meta.Tactic.Grind.Core
+import Lean.Meta.Tactic.Grind.Combinators
 
 namespace Lean.Meta.Grind
 
@@ -88,7 +89,7 @@ private def applyInjection? (goal : Goal) (fvarId : FVarId) : MetaM (Option Goal
     return none
 
 /-- Introduce new hypotheses (and apply `by_contra`) until goal is of the form `... ⊢ False` -/
-partial def intros (goal : Goal) (generation : Nat) : GrindM (List Goal) := do
+partial def intros  (generation : Nat) : GrindTactic' := fun goal => do
   let rec go (goal : Goal) : StateRefT (Array Goal) GrindM Unit := do
     if goal.inconsistent then
       return ()
@@ -116,11 +117,11 @@ partial def intros (goal : Goal) (generation : Nat) : GrindM (List Goal) := do
   return goals.toList
 
 /-- Asserts a new fact `prop` with proof `proof` to the given `goal`. -/
-def assertAt (goal : Goal) (proof : Expr) (prop : Expr) (generation : Nat) : GrindM (List Goal) := do
+def assertAt (proof : Expr) (prop : Expr) (generation : Nat) : GrindTactic' := fun goal => do
   if (← isCasesCandidate prop) then
     let mvarId ← goal.mvarId.assert (← mkFreshUserName `h) prop proof
     let goal := { goal with mvarId }
-    intros goal generation
+    intros generation goal
   else
     let goal ← GoalM.run' goal do
       let r ← simp prop
@@ -130,25 +131,13 @@ def assertAt (goal : Goal) (proof : Expr) (prop : Expr) (generation : Nat) : Gri
     if goal.inconsistent then return [] else return [goal]
 
 /-- Asserts next fact in the `goal` fact queue. -/
-def assertNext? (goal : Goal) : GrindM (Option (List Goal)) := do
+def assertNext : GrindTactic := fun goal => do
   let some (fact, newFacts) := goal.newFacts.dequeue?
     | return none
-  assertAt { goal with newFacts } fact.proof fact.prop fact.generation
-
-partial def iterate (goal : Goal) (f : Goal → GrindM (Option (List Goal))) : GrindM (List Goal) := do
-  go [goal] []
-where
-  go (todo : List Goal) (result : List Goal) : GrindM (List Goal) := do
-    match todo with
-    | [] => return result
-    | goal :: todo =>
-      if let some goalsNew ← f goal then
-        go (goalsNew ++ todo) result
-      else
-        go todo (goal :: result)
+  assertAt fact.proof fact.prop fact.generation { goal with newFacts }
 
 /-- Asserts all facts in the `goal` fact queue. -/
-partial def assertAll (goal : Goal) : GrindM (List Goal) := do
-  iterate goal assertNext?
+partial def assertAll : GrindTactic :=
+  assertNext.iterate
 
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Inv.lean

@@ -85,9 +85,9 @@ private def checkProofs : GoalM Unit := do
       for b in eqc do
         unless isSameExpr a b do
           let p ← mkEqHEqProof a b
-          trace[grind.debug.proofs] "{a} = {b}"
+          trace_goal[grind.debug.proofs] "{a} = {b}"
           check p
-          trace[grind.debug.proofs] "checked: {← inferType p}"
+          trace_goal[grind.debug.proofs] "checked: {← inferType p}"
 
 /--
 Checks basic invariants if `grind.debug` is enabled.

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

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 prelude
 import Init.Grind.Lemmas
 import Lean.Meta.Tactic.Util
-import Lean.Meta.Tactic.Simp.Simproc
 import Lean.Meta.Tactic.Grind.RevertAll
 import Lean.Meta.Tactic.Grind.PropagatorAttr
 import Lean.Meta.Tactic.Grind.Proj
@@ -15,7 +14,8 @@ import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.Inv
 import Lean.Meta.Tactic.Grind.Intro
 import Lean.Meta.Tactic.Grind.EMatch
-import Lean.Meta.Tactic.Grind.DoNotSimp
+import Lean.Meta.Tactic.Grind.Split
+import Lean.Meta.Tactic.Grind.SimpUtil
 
 namespace Lean.Meta.Grind
 
@@ -24,32 +24,24 @@ def mkMethods (fallback : Fallback) : CoreM Methods := do
   return {
     fallback
     propagateUp := fun e => do
-     propagateForallProp e
+     propagateForallPropUp e
      let .const declName _ := e.getAppFn | return ()
      propagateProjEq e
      if let some prop := builtinPropagators.up[declName]? then
        prop e
     propagateDown := fun e => do
+     propagateForallPropDown e
      let .const declName _ := e.getAppFn | return ()
      if let some prop := builtinPropagators.down[declName]? then
        prop e
   }
 
-private def getGrindSimprocs : MetaM Simprocs := do
-  let s ← grindNormSimprocExt.getSimprocs
-  let s ← addDoNotSimp s
-  return s
-
 def GrindM.run (x : GrindM α) (mainDeclName : Name) (config : Grind.Config) (fallback : Fallback) : MetaM α := do
   let scState := ShareCommon.State.mk _
   let (falseExpr, scState) := ShareCommon.State.shareCommon scState (mkConst ``False)
   let (trueExpr, scState)  := ShareCommon.State.shareCommon scState (mkConst ``True)
-  let thms ← grindNormExt.getTheorems
-  let simprocs := #[(← getGrindSimprocs), (← Simp.getSEvalSimprocs)]
-  let simp ← Simp.mkContext
-    (config := { arith := true })
-    (simpTheorems := #[thms])
-    (congrTheorems := (← getSimpCongrTheorems))
+  let simprocs ← Grind.getSimprocs
+  let simp ← Grind.getSimpContext
   x (← mkMethods fallback).toMethodsRef { mainDeclName, config, simprocs, simp } |>.run' { scState, trueExpr, falseExpr }
 
 private def mkGoal (mvarId : MVarId) : GrindM Goal := do
@@ -68,6 +60,7 @@ private def initCore (mvarId : MVarId) : GrindM (List Goal) := do
   let mvarId ← mvarId.revertAll
   let mvarId ← mvarId.unfoldReducible
   let mvarId ← mvarId.betaReduce
+  appendTagSuffix mvarId `grind
   let goals ← intros (← mkGoal mvarId) (generation := 0)
   goals.forM (·.checkInvariants (expensive := true))
   return goals.filter fun goal => !goal.inconsistent
@@ -77,7 +70,7 @@ def all (goals : List Goal) (f : Goal → GrindM (List Goal)) : GrindM (List Goa
 
 /-- A very simple strategy -/
 private def simple (goals : List Goal) : GrindM (List Goal) := do
-  all goals ematchStar
+  applyToAll (assertAll >> ematchStar >> (splitNext >> assertAll >> ematchStar).iterate) goals
 
 def main (mvarId : MVarId) (config : Grind.Config) (mainDeclName : Name) (fallback : Fallback) : MetaM (List MVarId) := do
   let go : GrindM (List MVarId) := do

src/Lean/Meta/Tactic/Grind/Proj.lean

@@ -30,7 +30,7 @@ def propagateProjEq (parent : Expr) : GoalM Unit := do
     let parentNew ← shareCommon (mkApp parent.appFn! ctor)
     internalize parentNew (← getGeneration parent)
     pure parentNew
-  trace[grind.debug.proj] "{parentNew}"
+  trace_goal[grind.debug.proj] "{parentNew}"
   let idx := info.numParams + info.i
   unless idx < ctor.getAppNumArgs do return ()
   let v := ctor.getArg! idx

src/Lean/Meta/Tactic/Grind/Propagate.lean

@@ -134,6 +134,13 @@ builtin_grind_propagator propagateEqDown ↓Eq := fun e => do
     let_expr Eq _ a b := e | return ()
     pushEq a b <| mkApp2 (mkConst ``of_eq_true) e (← mkEqTrueProof e)
 
+/-- Propagates `EqMatch` downwards -/
+builtin_grind_propagator propagateEqMatchDown ↓Grind.EqMatch := fun e => do
+  if (← isEqTrue e) then
+    let_expr Grind.EqMatch _ a b origin := e | return ()
+    markCaseSplitAsResolved origin
+    pushEq a b <| mkApp2 (mkConst ``of_eq_true) e (← mkEqTrueProof e)
+
 /-- Propagates `HEq` downwards -/
 builtin_grind_propagator propagateHEqDown ↓HEq := fun e => do
   if (← isEqTrue e) then

src/Lean/Meta/Tactic/Grind/SimpUtil.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Simp.Simproc
+import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.DoNotSimp
+
+namespace Lean.Meta.Grind
+
+/-- Returns the array of simprocs used by `grind`. -/
+protected def getSimprocs : MetaM (Array Simprocs) := do
+  let s ← grindNormSimprocExt.getSimprocs
+  let s ← addDoNotSimp s
+  return #[s, (← Simp.getSEvalSimprocs)]
+
+/-- Returns the simplification context used by `grind`. -/
+protected def getSimpContext : MetaM Simp.Context := do
+  let thms ← grindNormExt.getTheorems
+  Simp.mkContext
+    (config := { arith := true })
+    (simpTheorems := #[thms])
+    (congrTheorems := (← getSimpCongrTheorems))
+
+@[export lean_grind_normalize]
+def normalizeImp (e : Expr) : MetaM Expr := do
+  let (r, _) ← Meta.simp e (← Grind.getSimpContext) (← Grind.getSimprocs)
+  return r.expr
+
+end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Split.lean

@@ -0,0 +1,126 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.Intro
+import Lean.Meta.Tactic.Grind.Cases
+import Lean.Meta.Tactic.Grind.CasesMatch
+
+namespace Lean.Meta.Grind
+
+inductive CaseSplitStatus where
+  | resolved
+  | notReady
+  | ready
+  deriving Inhabited, BEq
+
+private def checkCaseSplitStatus (e : Expr) : GoalM CaseSplitStatus := do
+  match_expr e with
+  | Or a b =>
+    if (← isEqTrue e) then
+      if (← isEqTrue a <||> isEqTrue b) then
+        return .resolved
+      else
+        return .ready
+    else if (← isEqFalse e) then
+      return .resolved
+    else
+      return .notReady
+  | And a b =>
+    if (← isEqTrue e) then
+      return .resolved
+    else if (← isEqFalse e) then
+      if (← isEqFalse a <||> isEqFalse b) then
+        return .resolved
+      else
+        return .ready
+    else
+      return .notReady
+  | ite _ c _ _ _ =>
+    if (← isEqTrue c <||> isEqFalse c) then
+      return .resolved
+    else
+      return .ready
+  | dite _ c _ _ _ =>
+    if (← isEqTrue c <||> isEqFalse c) then
+      return .resolved
+    else
+      return .ready
+  | _ =>
+    if (← isResolvedCaseSplit e) then
+      trace[grind.debug.split] "split resolved: {e}"
+      return .resolved
+    if (← isMatcherApp e) then
+      return .ready
+    let .const declName .. := e.getAppFn | unreachable!
+    if (← isInductivePredicate declName <&&> isEqTrue e) then
+      return .ready
+    return .notReady
+
+/-- Returns the next case-split to be performed. It uses a very simple heuristic. -/
+private def selectNextSplit? : GoalM (Option Expr) := do
+  if (← isInconsistent) then return none
+  if (← checkMaxCaseSplit) then return none
+  go (← get).splitCandidates none []
+where
+  go (cs : List Expr) (c? : Option Expr) (cs' : List Expr) : GoalM (Option Expr) := do
+    match cs with
+    | [] =>
+      modify fun s => { s with splitCandidates := cs'.reverse }
+      if c?.isSome then
+        -- Remark: we reset `numEmatch` after each case split.
+        -- We should consider other strategies in the future.
+        modify fun s => { s with numSplits := s.numSplits + 1, numEmatch := 0 }
+      return c?
+    | c::cs =>
+    match (← checkCaseSplitStatus c) with
+    | .notReady => go cs c? (c::cs')
+    | .resolved => go cs c? cs'
+    | .ready =>
+    match c? with
+    | none => go cs (some c) cs'
+    | some c' =>
+      if (← getGeneration c) < (← getGeneration c') then
+        go cs (some c) (c'::cs')
+      else
+        go cs c? (c::cs')
+
+/-- Constructs a major premise for the `cases` tactic used by `grind`. -/
+private def mkCasesMajor (c : Expr) : GoalM Expr := do
+  match_expr c with
+  | And a b => return mkApp3 (mkConst ``Grind.or_of_and_eq_false) a b (← mkEqFalseProof c)
+  | ite _ c _ _ _ => return mkEM c
+  | dite _ c _ _ _ => return mkEM c
+  | _ => return mkApp2 (mkConst ``of_eq_true) c (← mkEqTrueProof c)
+
+/-- Introduces new hypotheses in each goal. -/
+private def introNewHyp (goals : List Goal) (acc : List Goal) (generation : Nat) : GrindM (List Goal) := do
+  match goals with
+  | [] => return acc.reverse
+  | goal::goals => introNewHyp goals ((← intros generation goal) ++ acc) generation
+
+/--
+Selects a case-split from the list of candidates,
+and returns a new list of goals if successful.
+-/
+def splitNext : GrindTactic := fun goal => do
+  let (goals?, _) ← GoalM.run goal do
+    let some c ← selectNextSplit?
+      | return none
+    let gen ← getGeneration c
+    trace_goal[grind.split] "{c}, generation: {gen}"
+    let mvarIds ← if (← isMatcherApp c) then
+      casesMatch (← get).mvarId c
+    else
+      let major ← mkCasesMajor c
+      cases (← get).mvarId major
+    let goal ← get
+    let goals := mvarIds.map fun mvarId => { goal with mvarId }
+    let goals ← introNewHyp goals [] (gen+1)
+    return some goals
+  return goals?
+
+end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -29,7 +29,7 @@ def congrPlaceholderProof := mkConst (Name.mkSimple "[congruence]")
 
 /--
 Returns `true` if `e` is `True`, `False`, or a literal value.
-See `LitValues` for supported literals.
+See `Lean.Meta.LitValues` for supported literals.
 -/
 def isInterpreted (e : Expr) : MetaM Bool := do
   if e.isTrue || e.isFalse then return true
@@ -59,16 +59,16 @@ structure CongrTheoremCacheKey where
   f       : Expr
   numArgs : Nat
 
--- We manually define `BEq` because we wannt to use pointer equality.
+-- We manually define `BEq` because we want to use pointer equality.
 instance : BEq CongrTheoremCacheKey where
   beq a b := isSameExpr a.f b.f && a.numArgs == b.numArgs
 
--- We manually define `Hashable` because we wannt to use pointer equality.
+-- We manually define `Hashable` because we want to use pointer equality.
 instance : Hashable CongrTheoremCacheKey where
   hash a := mixHash (unsafe ptrAddrUnsafe a.f).toUInt64 (hash a.numArgs)
 
 /-- State for the `GrindM` monad. -/
-structure CoreState where
+structure State where
   canon      : Canon.State := {}
   /-- `ShareCommon` (aka `Hashconsing`) state. -/
   scState    : ShareCommon.State.{0} ShareCommon.objectFactory := ShareCommon.State.mk _
@@ -83,12 +83,17 @@ structure CoreState where
   simpStats  : Simp.Stats := {}
   trueExpr   : Expr
   falseExpr  : Expr
+  /--
+  Used to generate trace messages of the for `[grind] working on <tag>`,
+  and implement the macro `trace_goal`.
+  -/
+  lastTag    : Name := .anonymous
 
 private opaque MethodsRefPointed : NonemptyType.{0}
 private def MethodsRef : Type := MethodsRefPointed.type
 instance : Nonempty MethodsRef := MethodsRefPointed.property
 
-abbrev GrindM := ReaderT MethodsRef $ ReaderT Context $ StateRefT CoreState MetaM
+abbrev GrindM := ReaderT MethodsRef $ ReaderT Context $ StateRefT State MetaM
 
 /-- Returns the user-defined configuration options -/
 def getConfig : GrindM Grind.Config :=
@@ -123,12 +128,12 @@ def abstractNestedProofs (e : Expr) : GrindM Expr := do
 
 /--
 Applies hash-consing to `e`. Recall that all expressions in a `grind` goal have
-been hash-consing. We perform this step before we internalize expressions.
+been hash-consed. We perform this step before we internalize expressions.
 -/
 def shareCommon (e : Expr) : GrindM Expr := do
-  modifyGet fun { canon, scState, nextThmIdx, congrThms, trueExpr, falseExpr, simpStats } =>
+  modifyGet fun { canon, scState, nextThmIdx, congrThms, trueExpr, falseExpr, simpStats, lastTag } =>
     let (e, scState) := ShareCommon.State.shareCommon scState e
-    (e, { canon, scState, nextThmIdx, congrThms, trueExpr, falseExpr, simpStats })
+    (e, { canon, scState, nextThmIdx, congrThms, trueExpr, falseExpr, simpStats, lastTag })
 
 /--
 Canonicalizes nested types, type formers, and instances in `e`.
@@ -193,7 +198,7 @@ structure ENode where
   interpreted : Bool := false
   /-- `ctor := true` if the head symbol is a constructor application. -/
   ctor : Bool := false
-  /-- `hasLambdas := true` if equivalence class contains lambda expressions. -/
+  /-- `hasLambdas := true` if the equivalence class contains lambda expressions. -/
   hasLambdas : Bool := false
   /--
   If `heqProofs := true`, then some proofs in the equivalence class are based
@@ -207,7 +212,6 @@ structure ENode where
   generation : Nat := 0
   /-- Modification time -/
   mt : Nat := 0
-  -- TODO: see Lean 3 implementation
   deriving Inhabited, Repr
 
 def ENode.isCongrRoot (n : ENode) :=
@@ -375,12 +379,22 @@ structure Goal where
   thmMap       : EMatchTheorems
   /-- Number of theorem instances generated so far -/
   numInstances : Nat := 0
+  /-- Number of E-matching rounds performed in this goal since the last case-split. -/
+  numEmatch    : Nat := 0
   /-- (pre-)instances found so far. It includes instances that failed to be instantiated. -/
   preInstances : PreInstanceSet := {}
   /-- new facts to be processed. -/
   newFacts     : Std.Queue NewFact := ∅
   /-- `match` auxiliary functions whose equations have already been created and activated. -/
   matchEqNames : PHashSet Name := {}
+  /-- Case-split candidates. -/
+  splitCandidates : List Expr := []
+  /-- Number of splits performed to get to this goal. -/
+  numSplits : Nat := 0
+  /-- Case-splits that do not have to be performed anymore. -/
+  resolvedSplits : PHashSet ENodeKey := {}
+  /-- Next local E-match theorem idx. -/
+  nextThmIdx : Nat := 0
   deriving Inhabited
 
 def Goal.admit (goal : Goal) : MetaM Unit :=
@@ -394,6 +408,25 @@ abbrev GoalM := StateRefT Goal GrindM
 @[inline] def GoalM.run' (goal : Goal) (x : GoalM Unit) : GrindM Goal :=
   goal.mvarId.withContext do StateRefT'.run' (x *> get) goal
 
+def updateLastTag : GoalM Unit := do
+  if (← isTracingEnabledFor `grind) then
+    let currTag ← (← get).mvarId.getTag
+    if currTag != (← getThe Grind.State).lastTag then
+      trace[grind] "working on goal `{currTag}`"
+      modifyThe Grind.State fun s => { s with lastTag := currTag }
+
+/--
+Macro similar to `trace[...]`, but it includes the trace message `trace[grind] "working on <current goal>"`
+if the tag has changed since the last trace message.
+-/
+macro "trace_goal[" id:ident "]" s:(interpolatedStr(term) <|> term) : doElem => do
+  let msg ← if s.raw.getKind == interpolatedStrKind then `(m! $(⟨s⟩)) else `(($(⟨s⟩) : MessageData))
+  `(doElem| do
+    let cls := $(quote id.getId.eraseMacroScopes)
+    if (← Lean.isTracingEnabledFor cls) then
+      updateLastTag
+      Lean.addTrace cls $msg)
+
 /--
 A helper function used to mark a theorem instance found by the E-matching module.
 It returns `true` if it is a new instance and `false` otherwise.
@@ -418,6 +451,14 @@ def addTheoremInstance (proof : Expr) (prop : Expr) (generation : Nat) : GoalM U
 def checkMaxInstancesExceeded : GoalM Bool := do
   return (← get).numInstances >= (← getConfig).instances
 
+/-- Returns `true` if the maximum number of case-splits has been reached. -/
+def checkMaxCaseSplit : GoalM Bool := do
+  return (← get).numSplits >= (← getConfig).splits
+
+/-- Returns `true` if the maximum number of E-matching rounds has been reached. -/
+def checkMaxEmatchExceeded : GoalM Bool := do
+  return (← get).numEmatch >= (← getConfig).ematch
+
 /--
 Returns `some n` if `e` has already been "internalized" into the
 Otherwise, returns `none`s.
@@ -637,7 +678,9 @@ def mkEqFalseProof (a : Expr) : GoalM Expr := do
 
 /-- Marks current goal as inconsistent without assigning `mvarId`. -/
 def markAsInconsistent : GoalM Unit := do
-  modify fun s => { s with inconsistent := true }
+  unless (← get).inconsistent do
+    trace[grind] "closed `{← (← get).mvarId.getTag}`"
+    modify fun s => { s with inconsistent := true }
 
 /--
 Closes the current goal using the given proof of `False` and
@@ -726,4 +769,17 @@ partial def getEqcs : GoalM (List (List Expr)) := do
       r := (← getEqc node.self) :: r
   return r
 
+/-- Returns `true` if `e` is a case-split that does not need to be performed anymore. -/
+def isResolvedCaseSplit (e : Expr) : GoalM Bool :=
+  return (← get).resolvedSplits.contains { expr := e }
+
+/--
+Mark `e` as a case-split that does not need to be performed anymore.
+Remark: we currently use this feature to disable `match`-case-splits
+-/
+def markCaseSplitAsResolved (e : Expr) : GoalM Unit := do
+  unless (← isResolvedCaseSplit e) do
+    trace_goal[grind.split.resolved] "{e}"
+    modify fun s => { s with resolvedSplits := s.resolvedSplits.insert { expr := e } }
+
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Util.lean

@@ -140,4 +140,11 @@ def normalizeLevels (e : Expr) : CoreM Expr := do
     | _ => return .continue
   Core.transform e (pre := pre)
 
+/--
+Normalizes the given expression using the `grind` simplification theorems and simprocs.
+This function is used for normalzing E-matching patterns. Note that it does not return a proof.
+-/
+@[extern "lean_grind_normalize"] -- forward definition
+opaque normalize (e : Expr) : MetaM Expr
+
 end Lean.Meta.Grind

src/Lean/Util/Trace.lean

@@ -293,13 +293,16 @@ def registerTraceClass (traceClassName : Name) (inherited := false) (ref : Name
   if inherited then
     inheritedTraceOptions.modify (·.insert optionName)
 
-macro "trace[" id:ident "]" s:(interpolatedStr(term) <|> term) : doElem => do
-  let msg ← if s.raw.getKind == interpolatedStrKind then `(m! $(⟨s⟩)) else `(($(⟨s⟩) : MessageData))
+def expandTraceMacro (id : Syntax) (s : Syntax) : MacroM (TSyntax `doElem) := do
+  let msg ← if s.getKind == interpolatedStrKind then `(m! $(⟨s⟩)) else `(($(⟨s⟩) : MessageData))
   `(doElem| do
     let cls := $(quote id.getId.eraseMacroScopes)
     if (← Lean.isTracingEnabledFor cls) then
       Lean.addTrace cls $msg)
 
+macro "trace[" id:ident "]" s:(interpolatedStr(term) <|> term) : doElem => do
+  expandTraceMacro id s.raw
+
 def bombEmoji := "💥️"
 def checkEmoji := "✅️"
 def crossEmoji := "❌️"

src/Std.lean

@@ -10,3 +10,4 @@ import Std.Sync
 import Std.Time
 import Std.Tactic
 import Std.Internal
+import Std.Net

src/Std/Net.lean

@@ -0,0 +1,7 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Std.Net.Addr

src/Std/Net/Addr.lean

@@ -0,0 +1,197 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Init.Data.Vector.Basic
+
+/-!
+This module contains Lean representations of IP and socket addresses:
+- `IPv4Addr`: Representing IPv4 addresses.
+- `SocketAddressV4`: Representing a pair of IPv4 address and port.
+- `IPv6Addr`: Representing IPv6 addresses.
+- `SocketAddressV6`: Representing a pair of IPv6 address and port.
+- `IPAddr`: Can either be an `IPv4Addr` or an `IPv6Addr`.
+- `SocketAddress`: Can either be a `SocketAddressV4` or `SocketAddressV6`.
+-/
+
+namespace Std
+namespace Net
+
+/--
+Representation of an IPv4 address.
+-/
+structure IPv4Addr where
+  /--
+  This structure represents the address: `octets[0].octets[1].octets[2].octets[3]`.
+  -/
+  octets : Vector UInt8 4
+  deriving Inhabited, DecidableEq
+
+/--
+A pair of an `IPv4Addr` and a port.
+-/
+structure SocketAddressV4 where
+  addr : IPv4Addr
+  port : UInt16
+  deriving Inhabited, DecidableEq
+
+/--
+Representation of an IPv6 address.
+-/
+structure IPv6Addr where
+  /--
+  This structure represents the address: `segments[0]:segments[1]:...`.
+  -/
+  segments : Vector UInt16 8
+  deriving Inhabited, DecidableEq
+
+/--
+A pair of an `IPv6Addr` and a port.
+-/
+structure SocketAddressV6 where
+  addr : IPv6Addr
+  port : UInt16
+  deriving Inhabited, DecidableEq
+
+/--
+An IP address, either IPv4 or IPv6.
+-/
+inductive IPAddr where
+  | v4 (addr : IPv4Addr)
+  | v6 (addr : IPv6Addr)
+  deriving Inhabited, DecidableEq
+
+/--
+Either a `SocketAddressV4` or `SocketAddressV6`.
+-/
+inductive SocketAddress where
+  | v4 (addr : SocketAddressV4)
+  | v6 (addr : SocketAddressV6)
+  deriving Inhabited, DecidableEq
+
+/--
+The kinds of address families supported by Lean, currently only IP variants.
+-/
+inductive AddressFamily where
+  | ipv4
+  | ipv6
+  deriving Inhabited, DecidableEq
+
+namespace IPv4Addr
+
+/--
+Build the IPv4 address `a.b.c.d`.
+-/
+def ofParts (a b c d : UInt8) : IPv4Addr :=
+  { octets := #v[a, b, c, d] }
+
+/--
+Try to parse `s` as an IPv4 address, returning `none` on failure.
+-/
+@[extern "lean_uv_pton_v4"]
+opaque ofString (s : @&String) : Option IPv4Addr
+
+/--
+Turn `addr` into a `String` in the usual IPv4 format.
+-/
+@[extern "lean_uv_ntop_v4"]
+opaque toString (addr : @&IPv4Addr) : String
+
+instance : ToString IPv4Addr where
+  toString := toString
+
+instance : Coe IPv4Addr IPAddr where
+  coe addr := .v4 addr
+
+end IPv4Addr
+
+namespace SocketAddressV4
+
+instance : Coe SocketAddressV4 SocketAddress where
+  coe addr := .v4 addr
+
+end SocketAddressV4
+
+namespace IPv6Addr
+
+/--
+Build the IPv6 address `a:b:c:d:e:f:g:h`.
+-/
+def ofParts (a b c d e f g h : UInt16) : IPv6Addr :=
+  { segments := #v[a, b, c, d, e, f, g, h] }
+
+/--
+Try to parse `s` as an IPv6 address according to
+[RFC 2373](https://datatracker.ietf.org/doc/html/rfc2373), returning `none` on failure.
+-/
+@[extern "lean_uv_pton_v6"]
+opaque ofString (s : @&String) : Option IPv6Addr
+
+/--
+Turn `addr` into a `String` in the IPv6 format described in
+[RFC 2373](https://datatracker.ietf.org/doc/html/rfc2373).
+-/
+@[extern "lean_uv_ntop_v6"]
+opaque toString (addr : @&IPv6Addr) : String
+
+instance : ToString IPv6Addr where
+  toString := toString
+
+instance : Coe IPv6Addr IPAddr where
+  coe addr := .v6 addr
+
+end IPv6Addr
+
+namespace SocketAddressV6
+
+instance : Coe SocketAddressV6 SocketAddress where
+  coe addr := .v6 addr
+
+end SocketAddressV6
+
+namespace IPAddr
+
+/--
+Obtain the `AddressFamily` associated with an `IPAddr`.
+-/
+def family : IPAddr → AddressFamily
+  | .v4 .. => .ipv4
+  | .v6 .. => .ipv6
+
+def toString : IPAddr → String
+  | .v4 addr => addr.toString
+  | .v6 addr => addr.toString
+
+instance : ToString IPAddr where
+  toString := toString
+
+end IPAddr
+
+namespace SocketAddress
+
+/--
+Obtain the `AddressFamily` associated with a `SocketAddress`.
+-/
+def family : SocketAddress → AddressFamily
+  | .v4 .. => .ipv4
+  | .v6 .. => .ipv6
+
+/--
+Obtain the `IPAddr` contained in a `SocketAddress`.
+-/
+def ipAddr : SocketAddress → IPAddr
+  | .v4 sa  => .v4 sa.addr
+  | .v6 sa  => .v6 sa.addr
+
+/--
+Obtain the port contained in a `SocketAddress`.
+-/
+def port : SocketAddress → UInt16
+  | .v4 sa | .v6 sa => sa.port
+
+end SocketAddress
+
+end Net
+end Std

src/Std/Time/Date/Unit/Month.lean

@@ -39,6 +39,12 @@ instance {x y : Ordinal} : Decidable (x < y) :=
 def Offset : Type := Int
   deriving Repr, BEq, Inhabited, Add, Sub, Mul, Div, Neg, ToString, LT, LE, DecidableEq
 
+instance {x y : Offset} : Decidable (x ≤ y) :=
+  Int.decLe x y
+
+instance {x y : Offset} : Decidable (x < y) :=
+  Int.decLt x y
+
 instance : OfNat Offset n :=
   ⟨Int.ofNat n⟩
 

src/Std/Time/Date/Unit/Week.lean

@@ -39,6 +39,12 @@ instance : Inhabited Ordinal where
 def Offset : Type := UnitVal (86400 * 7)
   deriving Repr, BEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
 
+instance {x y : Offset} : Decidable (x ≤ y) :=
+  inferInstanceAs (Decidable (x.val ≤ y.val))
+
+instance {x y : Offset} : Decidable (x < y) :=
+  inferInstanceAs (Decidable (x.val < y.val))
+
 instance : OfNat Offset n := ⟨UnitVal.ofNat n⟩
 
 namespace Ordinal

src/Std/Time/Time/Unit/Hour.lean

@@ -40,7 +40,13 @@ instance {x y : Ordinal} : Decidable (x < y) :=
 or differences in hours.
 -/
 def Offset : Type := UnitVal 3600
-  deriving Repr, BEq, Inhabited, Add, Sub, Neg, ToString
+  deriving Repr, BEq, Inhabited, Add, Sub, Neg, ToString, LT, LE
+
+instance { x y : Offset } : Decidable (x ≤ y) :=
+  inferInstanceAs (Decidable (x.val ≤ y.val))
+
+instance { x y : Offset } : Decidable (x < y) :=
+  inferInstanceAs (Decidable (x.val < y.val))
 
 instance : OfNat Offset n :=
   ⟨UnitVal.ofNat n⟩

src/Std/Time/Time/Unit/Millisecond.lean

@@ -40,6 +40,12 @@ instance {x y : Ordinal} : Decidable (x < y) :=
 def Offset : Type := UnitVal (1 / 1000)
   deriving Repr, BEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
 
+instance { x y : Offset } : Decidable (x ≤ y) :=
+  inferInstanceAs (Decidable (x.val ≤ y.val))
+
+instance { x y : Offset } : Decidable (x < y) :=
+  inferInstanceAs (Decidable (x.val < y.val))
+
 instance : OfNat Offset n :=
   ⟨UnitVal.ofNat n⟩
 

src/Std/Time/Time/Unit/Minute.lean

@@ -38,7 +38,13 @@ instance {x y : Ordinal} : Decidable (x < y) :=
 `Offset` represents a duration offset in minutes.
 -/
 def Offset : Type := UnitVal 60
-  deriving Repr, BEq, Inhabited, Add, Sub, Neg, ToString
+  deriving Repr, BEq, Inhabited, Add, Sub, Neg, ToString, LT, LE
+
+instance { x y : Offset } : Decidable (x ≤ y) :=
+  inferInstanceAs (Decidable (x.val ≤ y.val))
+
+instance { x y : Offset } : Decidable (x < y) :=
+  inferInstanceAs (Decidable (x.val < y.val))
 
 instance : OfNat Offset n :=
   ⟨UnitVal.ofInt <| Int.ofNat n⟩

src/Std/Time/Time/Unit/Nanosecond.lean

@@ -42,6 +42,9 @@ def Offset : Type := UnitVal (1 / 1000000000)
 instance { x y : Offset } : Decidable (x ≤ y) :=
   inferInstanceAs (Decidable (x.val ≤ y.val))
 
+instance { x y : Offset } : Decidable (x < y) :=
+  inferInstanceAs (Decidable (x.val < y.val))
+
 instance : OfNat Offset n :=
   ⟨UnitVal.ofNat n⟩
 

src/Std/Time/Time/Unit/Second.lean

@@ -51,6 +51,12 @@ instance {x y : Ordinal l} : Decidable (x < y) :=
 def Offset : Type := UnitVal 1
   deriving Repr, BEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
 
+instance { x y : Offset } : Decidable (x ≤ y) :=
+  inferInstanceAs (Decidable (x.val ≤ y.val))
+
+instance { x y : Offset } : Decidable (x < y) :=
+  inferInstanceAs (Decidable (x.val < y.val))
+
 instance : OfNat Offset n :=
   ⟨UnitVal.ofNat n⟩
 

src/runtime/CMakeLists.txt

@@ -2,7 +2,7 @@ set(RUNTIME_OBJS debug.cpp thread.cpp mpz.cpp utf8.cpp
 object.cpp apply.cpp exception.cpp interrupt.cpp memory.cpp
 stackinfo.cpp compact.cpp init_module.cpp load_dynlib.cpp io.cpp hash.cpp
 platform.cpp alloc.cpp allocprof.cpp sharecommon.cpp stack_overflow.cpp
-process.cpp object_ref.cpp mpn.cpp mutex.cpp libuv.cpp)
+process.cpp object_ref.cpp mpn.cpp mutex.cpp libuv.cpp uv/net_addr.cpp)
 add_library(leanrt_initial-exec STATIC ${RUNTIME_OBJS})
 set_target_properties(leanrt_initial-exec PROPERTIES
   ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR})

src/runtime/uv/net_addr.cpp

@@ -0,0 +1,131 @@
+/*
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Henrik Böving
+*/
+
+#include "runtime/uv/net_addr.h"
+#include <cstring>
+
+namespace lean {
+
+#ifndef LEAN_EMSCRIPTEN
+
+void lean_ipv4_addr_to_in_addr(b_obj_arg ipv4_addr, in_addr* out) {
+    out->s_addr = 0;
+    for (int i = 0; i < 4; i++) {
+        uint32_t octet = (uint32_t)(uint8_t)lean_unbox(array_uget(ipv4_addr, i));
+        out->s_addr |= octet << (3 - i) * 8;
+    }
+    out->s_addr = htonl(out->s_addr);
+}
+
+void lean_ipv6_addr_to_in6_addr(b_obj_arg ipv6_addr, in6_addr* out) {
+    for (int i = 0; i < 8; i++) {
+        uint16_t segment = htons((uint16_t)lean_unbox(array_uget(ipv6_addr, i)));
+        out->s6_addr[2 * i] = (uint8_t)segment;
+        out->s6_addr[2 * i + 1] = (uint8_t)(segment >> 8);
+    }
+}
+
+lean_obj_res lean_in_addr_to_ipv4_addr(const in_addr* ipv4_addr) {
+    obj_res ret = alloc_array(0, 4);
+    uint32_t hostaddr = ntohl(ipv4_addr->s_addr);
+
+    for (int i = 0; i < 4; i++) {
+        uint8_t octet = (uint8_t)(hostaddr >> (3 - i) * 8);
+        array_push(ret, lean_box(octet));
+    }
+
+    lean_assert(array_size(ret) == 4);
+    return ret;
+}
+
+lean_obj_res lean_in6_addr_to_ipv6_addr(const in6_addr* ipv6_addr) {
+    obj_res ret = alloc_array(0, 8);
+
+    for (int i = 0; i < 16; i += 2) {
+        uint16_t part1 = (uint16_t)ipv6_addr->s6_addr[i];
+        uint16_t part2 = (uint16_t)ipv6_addr->s6_addr[i + 1];
+        uint16_t segment = ntohs((part2 << 8) | part1);
+        array_push(ret, lean_box(segment));
+    }
+
+    lean_assert(array_size(ret) == 8);
+    return ret;
+}
+
+/* Std.Net.IPV4Addr.ofString (s : @&String) : Option IPV4Addr */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v4(b_obj_arg str_obj) {
+    const char* str = string_cstr(str_obj);
+    in_addr internal;
+    if (uv_inet_pton(AF_INET, str, &internal) == 0) {
+        return mk_option_some(lean_in_addr_to_ipv4_addr(&internal));
+    } else {
+        return mk_option_none();
+    }
+}
+
+/* Std.Net.IPV4Addr.toString (addr : @&IPV4Addr) : String */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v4(b_obj_arg ipv4_addr) {
+    in_addr internal;
+    lean_ipv4_addr_to_in_addr(ipv4_addr, &internal);
+    char dst[INET_ADDRSTRLEN];
+    int ret = uv_inet_ntop(AF_INET, &internal, dst, sizeof(dst));
+    lean_always_assert(ret == 0);
+    return lean_mk_string(dst);
+}
+
+/* Std.Net.IPV6Addr.ofString (s : @&String) : Option IPV6Addr */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v6(b_obj_arg str_obj) {
+    const char* str = string_cstr(str_obj);
+    in6_addr internal;
+    if (uv_inet_pton(AF_INET6, str, &internal) == 0) {
+        return mk_option_some(lean_in6_addr_to_ipv6_addr(&internal));
+    } else {
+        return mk_option_none();
+    }
+}
+
+/* Std.Net.IPV6Addr.toString (addr : @&IPV6Addr) : String */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v6(b_obj_arg ipv6_addr) {
+    in6_addr internal;
+    lean_ipv6_addr_to_in6_addr(ipv6_addr, &internal);
+    char dst[INET6_ADDRSTRLEN];
+    int ret = uv_inet_ntop(AF_INET6, &internal, dst, sizeof(dst));
+    lean_always_assert(ret == 0);
+    return lean_mk_string(dst);
+}
+
+#else
+
+/* Std.Net.IPV4Addr.ofString (s : @&String) : Option IPV4Addr */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v4(b_obj_arg str_obj) {
+    lean_always_assert(
+        false && ("Please build a version of Lean4 with libuv to invoke this.")
+    );
+}
+
+/* Std.Net.IPV4Addr.toString (addr : @&IPV4Addr) : String */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v4(b_obj_arg ipv4_addr) {
+    lean_always_assert(
+        false && ("Please build a version of Lean4 with libuv to invoke this.")
+    );
+}
+
+/* Std.Net.IPV6Addr.ofString (s : @&String) : Option IPV6Addr */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v6(b_obj_arg str_obj) {
+    lean_always_assert(
+        false && ("Please build a version of Lean4 with libuv to invoke this.")
+    );
+}
+
+/* Std.Net.IPV6Addr.toString (addr : @&IPV6Addr) : String */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v6(b_obj_arg ipv6_addr) {
+    lean_always_assert(
+        false && ("Please build a version of Lean4 with libuv to invoke this.")
+    );
+}
+
+#endif
+}

src/runtime/uv/net_addr.h

@@ -0,0 +1,28 @@
+/*
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Henrik Böving
+*/
+#pragma once
+#include <lean/lean.h>
+#include "runtime/object.h"
+
+
+namespace lean {
+
+#ifndef LEAN_EMSCRIPTEN
+#include <uv.h>
+
+void lean_ipv4_addr_to_in_addr(b_obj_arg ipv4_addr, struct in_addr* out);
+void lean_ipv6_addr_to_in6_addr(b_obj_arg ipv6_addr, struct in6_addr* out);
+lean_obj_res lean_in_addr_to_ipv4_addr(const struct in_addr* ipv4_addr);
+lean_obj_res lean_in6_addr_to_ipv6_addr(const struct in6_addr* ipv6_addr);
+
+#endif
+
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v4(b_obj_arg str_obj);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v4(b_obj_arg ipv4_addr);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v6(b_obj_arg str_obj);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v6(b_obj_arg ipv6_addr);
+
+}