.

This PR makes `IntCast` a field of `Lean.Grind.CommRing`, along with
additional axioms relating it to negation of `OfNat`. This allows use to
use existing instances which are not definitionally equal to the
previously given construction.

---------

Co-authored-by: Leonardo de Moura <leomoura@amazon.com>

.github/workflows/ci.yml

@@ -139,20 +139,21 @@ jobs:
             let large = ${{ github.repository == 'leanprover/lean4' }};
             const isPr = "${{ github.event_name }}" == "pull_request";
             let matrix = [
+              /* TODO: to be updated to new LLVM
               {
                 "name": "Linux LLVM",
                 "os": "ubuntu-latest",
                 "release": false,
                 "check-level": 2,
                 "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
                 "binary-check": "ldd -v",
                 // foreign code may be linked against more recent glibc
                 // reverse-ffi needs to be updated to link to LLVM libraries
                 "CTEST_OPTIONS": "-E 'foreign|leanlaketest_reverse-ffi'",
                 "CMAKE_OPTIONS": "-DLLVM=ON -DLLVM_CONFIG=${GITHUB_WORKSPACE}/build/llvm-host/bin/llvm-config"
-              },
+              }, */
               {
                 // portable release build: use channel with older glibc (2.26)
                 "name": "Linux release",
@@ -160,14 +161,12 @@ jobs:
                 "release": true,
                 "check-level": 0,
                 "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
                 "binary-check": "ldd -v",
                 // foreign code may be linked against more recent glibc
                 "CTEST_OPTIONS": "-E 'foreign'"
               },
-              // deactivated due to bugs
-              /*
               {
                 "name": "Linux Lake",
                 "os": large ? "nscloud-ubuntu-22.04-amd64-4x8" : "ubuntu-latest",
@@ -178,7 +177,6 @@ jobs:
                 // TODO: why does this fail?
                 "CTEST_OPTIONS": "-E 'scopedMacros'"
               },
-              */
               {
                 "name": "Linux",
                 "os": large ? "nscloud-ubuntu-22.04-amd64-4x8" : "ubuntu-latest",
@@ -210,7 +208,7 @@ jobs:
                 "release": true,
                 "check-level": 2,
                 "shell": "bash -euxo pipefail {0}",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-apple-darwin.tar.zst",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-apple-darwin.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
                 "binary-check": "otool -L",
                 "tar": "gtar" // https://github.com/actions/runner-images/issues/2619
@@ -221,7 +219,7 @@ jobs:
                 "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
                 "release": true,
                 "shell": "bash -euxo pipefail {0}",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-apple-darwin.tar.zst",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-aarch64-apple-darwin.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
                 "binary-check": "otool -L",
                 "tar": "gtar", // https://github.com/actions/runner-images/issues/2619
@@ -242,7 +240,7 @@ jobs:
                 "CMAKE_OPTIONS": "-G \"Unix Makefiles\"",
                 // for reasons unknown, interactivetests are flaky on Windows
                 "CTEST_OPTIONS": "--repeat until-pass:2",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-mingw.sh lean-llvm*",
                 "binary-check": "ldd"
               },
@@ -253,7 +251,7 @@ jobs:
                 "release": true,
                 "check-level": 2,
                 "shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-linux-gnu.tar.zst",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-aarch64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*"
               },
               // Started running out of memory building expensive modules, a 2GB heap is just not that much even before fragmentation

.github/workflows/nix-ci.yml

@@ -73,7 +73,7 @@ jobs:
         with:
           extra-conf: |
             extra-sandbox-paths = /nix/var/cache/ccache?
-            substituters = file://${{ github.workspace }}/nix-store-cache-copy?priority=10&trusted=true https://cache.nixos.org  
+            substituters = file://${{ github.workspace }}/nix-store-cache-copy?priority=10&trusted=true https://cache.nixos.org
       - name: Prepare CCache Cache
         run: |
           sudo mkdir -m0770 -p /nix/var/cache/ccache
@@ -103,40 +103,10 @@ jobs:
           paths: push-test/test-results.xml
         if: always()
         continue-on-error: true
-      - name: Build manual
-        run: |
-          nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc#{lean-mdbook,leanInk,alectryon,inked} -o push-doc
-          nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc
-          # https://github.com/netlify/cli/issues/1809
-          cp -r --dereference ./result ./dist
-        if: matrix.name == 'Nix Linux'
       - name: Rebuild Nix Store Cache
         run: |
           rm -rf nix-store-cache || true
           nix copy ./push-* --to file://$PWD/nix-store-cache?compression=none
-      - id: deploy-info
-        name: Compute Deployment Metadata
-        run: |
-          set -e
-          python3 -c 'import base64; print("alias="+base64.urlsafe_b64encode(bytes.fromhex("${{github.sha}}")).decode("utf-8").rstrip("="))' >> "$GITHUB_OUTPUT"
-          echo "message=`git log -1 --pretty=format:"%s"`" >> "$GITHUB_OUTPUT"
-      - name: Publish manual to Netlify
-        uses: nwtgck/actions-netlify@v3.0
-        id: publish-manual
-        with:
-          publish-dir: ./dist
-          production-branch: master
-          github-token: ${{ secrets.GITHUB_TOKEN }}
-          deploy-message: |
-            ${{ github.event_name == 'pull_request' && format('pr#{0}: {1}', github.event.number, github.event.pull_request.title) || format('ref/{0}: {1}', github.ref_name, steps.deploy-info.outputs.message) }}
-          alias: ${{ steps.deploy-info.outputs.alias }}
-          enable-commit-comment: false
-          enable-pull-request-comment: false
-          github-deployment-environment: "lean-lang.org/lean4/doc"
-          fails-without-credentials: false
-        env:
-          NETLIFY_AUTH_TOKEN: ${{ secrets.NETLIFY_AUTH_TOKEN }}
-          NETLIFY_SITE_ID: "b8e805d2-7e9b-4f80-91fb-a84d72fc4a68"
       - name: Fixup CCache Cache
         run: |
           sudo chown -R $USER /nix/var/cache

nix/buildLeanPackage.nix

@@ -194,7 +194,7 @@ with builtins; let
   modCandidates = mapAttrs (mod: header:
     let
       deps = if header.errors == []
-             then map (m: m.module) header.imports
+             then map (m: m.module) header.result.imports
              else abort "errors while parsing imports of ${mod}:\n${lib.concatStringsSep "\n" header.errors}";
     in mkMod mod (map (dep: if modDepsMap ? ${dep} then modCandidates.${dep} else externalModMap.${dep}) deps)) modDepsMap;
   expandGlob = g:
@@ -206,7 +206,7 @@ with builtins; let
   # subset of `modCandidates` that is transitively reachable from `roots`
   mods' = listToAttrs (map (e: { name = e.key; value = modCandidates.${e.key}; }) (genericClosure {
     startSet = map (m: { key = m; }) (concatMap expandGlob roots);
-    operator = e: if modDepsMap ? ${e.key} then map (m: { key = m.module; }) (filter (m: modCandidates ? ${m.module}) modDepsMap.${e.key}.imports) else [];
+    operator = e: if modDepsMap ? ${e.key} then map (m: { key = m.module; }) (filter (m: modCandidates ? ${m.module}) modDepsMap.${e.key}.result.imports) else [];
   }));
   allLinkFlags = lib.foldr (shared: acc: acc ++ [ "-L${shared}" "-l${shared.linkName or shared.name}" ]) linkFlags allNativeSharedLibs;
 

script/prepare-llvm-linux.sh

@@ -1,5 +1,5 @@
 #!/usr/bin/env bash
-set -uo pipefail
+set -euxo pipefail
 
 # run from root build directory (from inside nix-shell or otherwise defining GLIBC/ZLIB/GMP) as in
 # ```
@@ -14,6 +14,7 @@ set -uo pipefail
 else
   ln -s llvm llvm-host
 fi
+mkdir -p stage0/lib
 mkdir -p stage1/{bin,lib,lib/glibc,include/clang}
 CP="cp -d"  # preserve symlinks
 # a C compiler!
@@ -25,6 +26,8 @@ cp -L llvm/bin/llvm-ar stage1/bin/
 # dependencies of the above
 $CP llvm/lib/lib{clang-cpp,LLVM}*.so* stage1/lib/
 $CP $ZLIB/lib/libz.so* stage1/lib/
+# also copy USE_LLVM deps into stage 0
+$CP llvm/lib/libLLVM*.so* $ZLIB/lib/libz.so* stage0/lib/
 # general clang++ dependency, breaks cross-library C++ exceptions if linked statically
 $CP $GCC_LIB/lib/libgcc_s.so* stage1/lib/
 # bundle libatomic (referenced by LLVM >= 15, and required by the lean executable to run)
@@ -39,18 +42,18 @@ $CP $GLIBC/lib/*crt* stage1/lib/
 # runtime
 (cd llvm; $CP --parents lib/clang/*/lib/*/{clang_rt.*.o,libclang_rt.builtins*} ../stage1)
 $CP llvm/lib/*/lib{c++,c++abi,unwind}.* $GMP/lib/libgmp.a $LIBUV/lib/libuv.a stage1/lib/
-# LLVM 15 appears to ship the dependencies in 'llvm/lib/<target-triple>/' and 'llvm/include/<target-triple>/'
-# but clang-15 that we use to compile is linked against 'llvm/lib/' and 'llvm/include'
+# LLVM 19 appears to ship the dependencies in 'llvm/lib/<target-triple>/' and 'llvm/include/<target-triple>/'
+# but clang-19 that we use to compile is linked against 'llvm/lib/' and 'llvm/include'
 # https://github.com/llvm/llvm-project/issues/54955
 $CP llvm/lib/*/lib{c++,c++abi,unwind}.* llvm/lib/
 $CP llvm-host/lib/*/lib{c++,c++abi,unwind}.* llvm-host/lib/
 # libc++ headers are looked up in the host compiler's root, so copy over target-specific includes
-$CP -r llvm/include/*-*-* llvm-host/include/
+$CP -r llvm/include/*-*-* llvm-host/include/ || true
 # glibc: use for linking (so Lean programs don't embed newer symbol versions), but not for running (because libc.so, librt.so, and ld.so must be compatible)!
 $CP $GLIBC/lib/libc_nonshared.a stage1/lib/glibc
 # libpthread_nonshared.a must be linked in order to be able to use `pthread_atfork(3)`. LibUV uses this function.
 $CP $GLIBC/lib/libpthread_nonshared.a stage1/lib/glibc
-for f in $GLIBC/lib/lib{c,dl,m,rt,pthread}-*; do b=$(basename $f); cp $f stage1/lib/glibc/${b%-*}.so; done
+for f in $GLIBC/lib/{ld,lib{c,dl,m,rt,pthread}}-*; do b=$(basename $f); cp $f stage1/lib/glibc/${b%-*}.so; done
 OPTIONS=()
 echo -n " -DLEAN_STANDALONE=ON"
 echo -n " -DCMAKE_CXX_COMPILER=$PWD/llvm-host/bin/clang++ -DLEAN_CXX_STDLIB='-Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic'"
@@ -64,7 +67,8 @@ 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='--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'"
+# ld.so is usually included by the libc.so linker script but we discard those
+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 ROOT/lib/glibc/ld.so -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

src/CMakeLists.txt

@@ -365,8 +365,8 @@ if(LLVM)
   execute_process(COMMAND ${LLVM_CONFIG} --version COMMAND_ERROR_IS_FATAL ANY OUTPUT_VARIABLE LLVM_CONFIG_VERSION ECHO_OUTPUT_VARIABLE OUTPUT_STRIP_TRAILING_WHITESPACE)
   string(REGEX MATCH "^[0-9]*" LLVM_CONFIG_MAJOR_VERSION ${LLVM_CONFIG_VERSION})
   message(STATUS "Found 'llvm-config' at '${LLVM_CONFIG}' with version '${LLVM_CONFIG_VERSION}', major version '${LLVM_CONFIG_MAJOR_VERSION}'")
-  if (NOT LLVM_CONFIG_MAJOR_VERSION STREQUAL "15")
-    message(FATAL_ERROR "Unable to find llvm-config version 15. Found invalid version '${LLVM_CONFIG_MAJOR_VERSION}'")
+  if (NOT LLVM_CONFIG_MAJOR_VERSION STREQUAL "19")
+    message(FATAL_ERROR "Unable to find llvm-config version 19. Found invalid version '${LLVM_CONFIG_MAJOR_VERSION}'")
   endif()
   # -DLEAN_LLVM is used to conditionally compile Lean features that depend on LLVM
   string(APPEND CMAKE_CXX_FLAGS " -D LEAN_LLVM")

src/Init/Conv.lean

@@ -318,6 +318,25 @@ syntax "repeat " convSeq : conv
 macro_rules
   | `(conv| repeat $seq) => `(conv| first | ($seq); repeat $seq | skip)
 
+/--
+Extracts `let` and `let_fun` expressions from within the target expression.
+This is the conv mode version of the `extract_lets` tactic.
+
+- `extract_lets` extracts all the lets from the target.
+- `extract_lets x y z` extracts all the lets from the target and uses `x`, `y`, and `z` for the first names.
+  Using `_` for a name leaves it unnamed.
+
+Limitation: the extracted local declarations do not persist outside of the `conv` goal.
+See also `lift_lets`, which does not extract lets as local declarations.
+-/
+syntax (name := extractLets) "extract_lets " optConfig (ppSpace colGt (ident <|> hole))* : conv
+
+/--
+Lifts `let` and `let_fun` expressions within the target expression as far out as possible.
+This is the conv mode version of the `lift_lets` tactic.
+-/
+syntax (name := liftLets) "lift_lets " optConfig : conv
+
 /--
 `conv => ...` allows the user to perform targeted rewriting on a goal or hypothesis,
 by focusing on particular subexpressions.

src/Init/Data/Array/Find.lean

@@ -21,6 +21,13 @@ open Nat
 
 /-! ### findSome? -/
 
+@[simp] theorem findSome?_empty : (#[] : Array α).findSome? f = none := rfl
+@[simp] theorem findSome?_push {xs : Array α} : (xs.push a).findSome? f = (xs.findSome? f).or (f a) := by
+  cases xs; simp [List.findSome?_append]
+
+theorem findSome?_singleton {a : α} {f : α → Option β} : #[a].findSome? f = f a := by
+  simp
+
 @[simp] theorem findSomeRev?_push_of_isSome {xs : Array α} (h : (f a).isSome) : (xs.push a).findSomeRev? f = f a := by
   cases xs; simp_all
 
@@ -129,6 +136,8 @@ abbrev findSome?_mkArray_of_isNone := @findSome?_replicate_of_isNone
 
 /-! ### find? -/
 
+@[simp] theorem find?_empty : find? p #[] = none := rfl
+
 @[simp] theorem find?_singleton {a : α} {p : α → Bool} :
     #[a].find? p = if p a then some a else none := by
   simp [singleton_eq_toArray_singleton]
@@ -157,6 +166,9 @@ theorem find?_eq_some_iff_append {xs : Array α} :
     exact ⟨as.toList, ⟨l, by simpa using congrArg Array.toList h'⟩,
       by simpa using h⟩
 
+theorem find?_push {xs : Array α} : (xs.push a).find? p = (xs.find? p).or (if p a then some a else none) := by
+  cases xs; simp
+
 @[simp]
 theorem find?_push_eq_some {xs : Array α} :
     (xs.push a).find? p = some b ↔ xs.find? p = some b ∨ (xs.find? p = none ∧ (p a ∧ a = b)) := by
@@ -331,6 +343,11 @@ theorem find?_eq_some_iff_getElem {xs : Array α} {p : α → Bool} {b : α} :
 
 /-! ### findIdx -/
 
+@[simp] theorem findIdx_empty : findIdx p #[] = 0 := rfl
+theorem findIdx_singleton {a : α} {p : α → Bool} :
+    #[a].findIdx p = if p a then 0 else 1 := by
+  simp
+
 theorem findIdx_of_getElem?_eq_some {xs : Array α} (w : xs[xs.findIdx p]? = some y) : p y := by
   rcases xs with ⟨xs⟩
   exact List.findIdx_of_getElem?_eq_some (by simpa using w)
@@ -411,6 +428,13 @@ theorem findIdx_append {p : α → Bool} {xs ys : Array α} :
   rcases ys with ⟨ys⟩
   simp [List.findIdx_append]
 
+theorem findIdx_push {xs : Array α} {a : α} {p : α → Bool} :
+    (xs.push a).findIdx p = if xs.findIdx p < xs.size then xs.findIdx p else xs.size + if p a then 0 else 1 := by
+  simp only [push_eq_append, findIdx_append]
+  split <;> rename_i h
+  · rfl
+  · simp [findIdx_singleton, Nat.add_comm]
+
 theorem findIdx_le_findIdx {xs : Array α} {p q : α → Bool} (h : ∀ x ∈ xs, p x → q x) : xs.findIdx q ≤ xs.findIdx p := by
   rcases xs with ⟨xs⟩
   simp_all [List.findIdx_le_findIdx]
@@ -439,6 +463,9 @@ theorem false_of_mem_extract_findIdx {xs : Array α} {p : α → Bool} (h : x
 /-! ### findIdx? -/
 
 @[simp] theorem findIdx?_empty : (#[] : Array α).findIdx? p = none := by simp
+theorem findIdx?_singleton {a : α} {p : α → Bool} :
+    #[a].findIdx? p = if p a then some 0 else none := by
+  simp
 
 @[simp]
 theorem findIdx?_eq_none_iff {xs : Array α} {p : α → Bool} :
@@ -506,6 +533,13 @@ theorem of_findIdx?_eq_none {xs : Array α} {p : α → Bool} (w : xs.findIdx? p
   rcases ys with ⟨ys⟩
   simp [List.findIdx?_append]
 
+theorem findIdx?_push {xs : Array α} {a : α} {p : α → Bool} :
+    (xs.push a).findIdx? p = (xs.findIdx? p).or (if p a then some xs.size else none) := by
+  simp only [push_eq_append, findIdx?_append]
+  split <;> rename_i h
+  · simp only [findIdx?_singleton, if_pos h, Option.map_some, Nat.zero_add]
+  · simp only [findIdx?_singleton, if_neg h, Option.map_none]
+
 theorem findIdx?_flatten {xss : Array (Array α)} {p : α → Bool} :
     xss.flatten.findIdx? p =
       (xss.findIdx? (·.any p)).map
@@ -563,6 +597,9 @@ theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : Array α} {p q : α → Bo
 /-! ### findFinIdx? -/
 
 @[simp] theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := by simp
+theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
+    #[a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by
+  simp
 
 -- We can't mark this as a `@[congr]` lemma since the head of the RHS is not `findFinIdx?`.
 theorem findFinIdx?_congr {p : α → Bool} {xs ys : Array α} (w : xs = ys) :
@@ -593,6 +630,21 @@ theorem findFinIdx?_eq_some_iff {xs : Array α} {p : α → Bool} {i : Fin xs.si
   · rintro ⟨h, w⟩
     exact ⟨i, ⟨i.2, h, fun j hji => w ⟨j, by omega⟩ hji⟩, rfl⟩
 
+theorem findFinIdx?_push {xs : Array α} {a : α} {p : α → Bool} :
+    (xs.push a).findFinIdx? p =
+      ((xs.findFinIdx? p).map (Fin.castLE (by simp))).or (if p a then some ⟨xs.size, by simp⟩ else none) := by
+  simp only [findFinIdx?_eq_pmap_findIdx?, findIdx?_push, Option.pmap_or]
+  split <;> rename_i h _ <;> split <;> simp [h]
+
+theorem findFinIdx?_append {xs ys : Array α} {p : α → Bool} :
+    (xs ++ ys).findFinIdx? p =
+      ((xs.findFinIdx? p).map (Fin.castLE (by simp))).or
+        ((ys.findFinIdx? p).map (Fin.natAdd xs.size) |>.map (Fin.cast (by simp))) := by
+  simp only [findFinIdx?_eq_pmap_findIdx?, findIdx?_append, Option.pmap_or]
+  split <;> rename_i h _
+  · simp [h, Option.pmap_map, Option.map_pmap, Nat.add_comm]
+  · simp [h]
+
 @[simp]
 theorem isSome_findFinIdx? {xs : Array α} {p : α → Bool} :
     (xs.findFinIdx? p).isSome = xs.any p := by

src/Init/Data/BitVec/Lemmas.lean

@@ -21,6 +21,9 @@ set_option linter.missingDocs true
 
 namespace BitVec
 
+@[simp] theorem mk_zero : BitVec.ofFin (w := w) ⟨0, h⟩ = 0#w := rfl
+@[simp] theorem ofNatLT_zero : BitVec.ofNatLT (w := w) 0 h = 0#w := rfl
+
 @[simp] theorem getLsbD_ofFin (x : Fin (2^n)) (i : Nat) :
     getLsbD (BitVec.ofFin x) i = x.val.testBit i := rfl
 
@@ -136,6 +139,8 @@ theorem toNat_ne_iff_ne {n} {x y : BitVec n} : x.toNat ≠ y.toNat ↔ x ≠ y :
 @[bitvec_to_nat] theorem toNat_eq {x y : BitVec n} : x = y ↔ x.toNat = y.toNat :=
   Iff.intro (congrArg BitVec.toNat) eq_of_toNat_eq
 
+theorem toNat_inj {x y : BitVec n} : x.toNat = y.toNat ↔ x = y := toNat_eq.symm
+
 @[bitvec_to_nat] theorem toNat_ne {x y : BitVec n} : x ≠ y ↔ x.toNat ≠ y.toNat := by
   rw [Ne, toNat_eq]
 
@@ -637,7 +642,7 @@ theorem toInt_nonneg_of_msb_false {x : BitVec w} (h : x.msb = false) : 0 ≤ x.t
   apply Nat.mod_eq_of_lt
   apply Nat.one_lt_two_pow (by omega)
 
-/-- Prove equality of bitvectors in terms of nat operations. -/
+/-- Prove equality of bitvectors in terms of integer operations. -/
 theorem eq_of_toInt_eq {x y : BitVec n} : x.toInt = y.toInt → x = y := by
   intro eq
   simp only [toInt_eq_toNat_cond] at eq

src/Init/Data/Fin/Lemmas.lean

@@ -410,6 +410,14 @@ theorem succ_succ_ne_one (a : Fin n) : Fin.succ (Fin.succ a) ≠ 1 :=
 
 @[simp] theorem coe_cast (h : n = m) (i : Fin n) : (i.cast h : Nat) = i := rfl
 
+@[simp] theorem cast_castLE {k m n} (km : k ≤ m) (mn : m = n) (i : Fin k) :
+    Fin.cast mn (i.castLE km) = i.castLE (mn ▸ km) :=
+  Fin.ext (by simp)
+
+@[simp] theorem cast_castLT {k m n} (i : Fin k) (h : (i : Nat) < m) (mn : m = n) :
+    Fin.cast mn (i.castLT h) = i.castLT (mn ▸ h) :=
+  Fin.ext (by simp)
+
 @[simp] theorem cast_zero [NeZero n] [NeZero m] (h : n = m) : Fin.cast h 0 = 0 := rfl
 
 @[simp] theorem cast_last {n' : Nat} {h : n + 1 = n' + 1} : (last n).cast h  = last n' :=

src/Init/Data/Int/Pow.lean

@@ -67,4 +67,10 @@ theorem pow_lt_pow_of_lt {a : Int} {b c : Nat} (ha : 1 < a) (hbc : b < c):
   | 0 => rfl
   | k + 1 => by rw [Int.pow_succ, natAbs_mul, natAbs_pow, Nat.pow_succ]
 
+theorem toNat_pow_of_nonneg {x : Int} (h : 0 ≤ x) (k : Nat) : (x ^ k).toNat = x.toNat ^ k := by
+  induction k with
+  | zero => simp
+  | succ k ih =>
+    rw [Int.pow_succ, Int.toNat_mul (Int.pow_nonneg h) h, ih, Nat.pow_succ]
+
 end Int

src/Init/Data/List/Find.lean

@@ -25,6 +25,10 @@ open Nat
 
 /-! ### findSome? -/
 
+@[simp] theorem findSome?_singleton {a : α} {f : α → Option β} : [a].findSome? f = f a := by
+  simp only [findSome?]
+  split <;> simp_all
+
 @[simp] theorem findSome?_cons_of_isSome {l} (h : (f a).isSome) : findSome? f (a :: l) = f a := by
   simp only [findSome?]
   split <;> simp_all
@@ -510,10 +514,13 @@ private theorem findIdx?_go_eq {p : α → Bool} {xs : List α} {i : Nat} :
 
 @[simp] theorem findIdx?_nil : ([] : List α).findIdx? p = none := rfl
 
-@[simp] theorem findIdx?_cons :
+theorem findIdx?_cons :
     (x :: xs).findIdx? p = if p x then some 0 else (xs.findIdx? p).map fun i => i + 1 := by
   simp [findIdx?, findIdx?_go_eq]
 
+@[simp] theorem findIdx?_singleton {a : α} {p : α → Bool} : [a].findIdx? p = if p a then some 0 else none := by
+  simp [findIdx?_cons, findIdx?_nil]
+
 /-! ### findIdx -/
 
 theorem findIdx_cons {p : α → Bool} {b : α} {l : List α} :
@@ -531,6 +538,9 @@ where
       cases p hd <;> simp only [cond_false, cond_true]
       exact findIdx_go_succ p tl (n + 1)
 
+@[simp] theorem findIdx_singleton {a : α} {p : α → Bool} : [a].findIdx p = if p a then 0 else 1 := by
+  simp [findIdx_cons, findIdx_nil]
+
 theorem findIdx_of_getElem?_eq_some {xs : List α} (w : xs[xs.findIdx p]? = some y) : p y := by
   induction xs with
   | nil => simp_all
@@ -825,7 +835,7 @@ abbrev findIdx?_of_eq_none := @of_findIdx?_eq_none
 @[simp] theorem findIdx?_append :
     (xs ++ ys : List α).findIdx? p =
       (xs.findIdx? p).or ((ys.findIdx? p).map fun i => i + xs.length) := by
-  induction xs with simp
+  induction xs with simp [findIdx?_cons]
   | cons _ _ _ => split <;> simp_all [Option.map_or, Option.map_map]; rfl
 
 theorem findIdx?_flatten {l : List (List α)} {p : α → Bool} :
@@ -960,7 +970,7 @@ theorem findFinIdx?_eq_pmap_findIdx? {xs : List α} {p : α → Bool} :
         (fun i h => h) := by
   simp [findIdx?_eq_map_findFinIdx?_val, Option.pmap_map]
 
-@[simp] theorem findFinIdx?_cons {p : α → Bool} {x : α} {xs : List α} :
+theorem findFinIdx?_cons {p : α → Bool} {x : α} {xs : List α} :
     findFinIdx? p (x :: xs) = if p x then some 0 else (findFinIdx? p xs).map Fin.succ := by
   rw [← Option.map_inj_right (f := Fin.val) (fun a b => Fin.eq_of_val_eq)]
   rw [← findIdx?_eq_map_findFinIdx?_val]
@@ -970,6 +980,19 @@ theorem findFinIdx?_eq_pmap_findIdx? {xs : List α} {p : α → Bool} :
   · rw [findIdx?_eq_map_findFinIdx?_val]
     simp [Function.comp_def]
 
+theorem findFinIdx?_append {xs ys : List α} {p : α → Bool} :
+    (xs ++ ys).findFinIdx? p =
+      ((xs.findFinIdx? p).map (Fin.castLE (by simp))).or
+        ((ys.findFinIdx? p).map (Fin.natAdd xs.length) |>.map (Fin.cast (by simp))) := by
+  simp only [findFinIdx?_eq_pmap_findIdx?, findIdx?_append, Option.pmap_or]
+  split <;> rename_i h _
+  · simp [h, Option.pmap_map, Option.map_pmap, Nat.add_comm]
+  · simp [h]
+
+@[simp] theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
+    [a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by
+  simp [findFinIdx?_cons, findFinIdx?_nil]
+
 @[simp] theorem findFinIdx?_eq_none_iff {l : List α} {p : α → Bool} :
     l.findFinIdx? p = none ↔ ∀ x ∈ l, ¬ p x := by
   simp [findFinIdx?_eq_pmap_findIdx?]
@@ -1086,10 +1109,10 @@ theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : List α} {a : α} :
 
 @[simp] theorem finIdxOf?_nil [BEq α] : ([] : List α).finIdxOf? a = none := rfl
 
-@[simp] theorem finIdxOf?_cons [BEq α] {a : α} {xs : List α} :
+theorem finIdxOf?_cons [BEq α] {a : α} {xs : List α} :
     (a :: xs).finIdxOf? b =
       if a == b then some ⟨0, by simp⟩ else (xs.finIdxOf? b).map (·.succ) := by
-  simp [finIdxOf?]
+  simp [finIdxOf?, findFinIdx?_cons]
 
 @[simp] theorem finIdxOf?_eq_none_iff [BEq α] [LawfulBEq α] {l : List α} {a : α} :
     l.finIdxOf? a = none ↔ a ∉ l := by
@@ -1132,7 +1155,10 @@ The lemmas below should be made consistent with those for `findIdx?` (and proved
 
 theorem idxOf?_cons [BEq α] {a : α} {xs : List α} {b : α} :
     (a :: xs).idxOf? b = if a == b then some 0 else (xs.idxOf? b).map (· + 1) := by
-  simp [idxOf?]
+  simp [idxOf?, findIdx?_cons]
+
+@[simp] theorem idxOf?_singleton [BEq α] {a b : α} : [a].idxOf? b = if a == b then some 0 else none := by
+  simp [idxOf?_cons, idxOf?_nil]
 
 @[simp] theorem idxOf?_eq_none_iff [BEq α] [LawfulBEq α] {l : List α} {a : α} :
     l.idxOf? a = none ↔ a ∉ l := by
@@ -1174,6 +1200,10 @@ variable [BEq α] [LawfulBEq α]
 @[simp] theorem lookup_cons_self  {k : α} : ((k,b) :: es).lookup k = some b := by
   simp [lookup_cons]
 
+@[simp] theorem lookup_singleton {a b : α} : [(a,b)].lookup c = if c == a then some b else none := by
+  simp [lookup_cons, lookup_nil]
+  split <;> simp_all
+
 theorem lookup_eq_findSome? {l : List (α × β)} {k : α} :
     l.lookup k = l.findSome? fun p => if k == p.1 then some p.2 else none := by
   induction l with

src/Init/Data/List/Nat/Find.lean

@@ -58,4 +58,4 @@ theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : List α} {p q : α → Boo
     rw [findIdx?_eq_some_iff_findIdx_eq] at h
     omega
   | none =>
-    refine ⟨l₁'.length, by simp, by simp_all⟩
+    refine ⟨l₁'.length, by simp, by simp_all [findIdx?_cons]⟩

src/Init/Data/Option/Lemmas.lean

@@ -895,6 +895,13 @@ theorem pmap_map (o : Option α) (f : α → β) {p : β → Prop} (g : ∀ b, p
       pmap (fun a h => g (f a) h) o (fun a m => H (f a) (map_eq_some_iff.2 ⟨_, m, rfl⟩)) := by
   cases o <;> simp
 
+theorem pmap_or {p : α → Prop} {f : ∀ (a : α), p a → β} {o o' : Option α} {h} :
+    (or o o').pmap f h =
+      match o with
+      | none => o'.pmap f (fun a h' => h a h')
+      | some a => f a (h a rfl) := by
+  cases o <;> simp
+
 theorem pmap_pred_congr {α : Type u}
     {p p' : α → Prop} (hp : ∀ x, p x ↔ p' x)
     {o o' : Option α} (ho : o = o')

src/Init/Data/RArray.lean

@@ -22,9 +22,6 @@ tree implementing `Nat → α`.
 
 See `RArray.ofFn` and `RArray.ofArray` in module `Lean.Data.RArray` for functions that construct an
 `RArray`.
-
-It is not universe-polymorphic. ; smaller proof objects and no complication with the `ToExpr` type
-class.
 -/
 inductive RArray (α : Type u) : Type u where
   | leaf : α → RArray α

src/Init/Data/Vector/Find.lean

@@ -24,6 +24,13 @@ open Nat
 
 /-! ### findSome? -/
 
+@[simp] theorem findSome?_empty : (#v[] : Vector α 0).findSome? f = none := rfl
+@[simp] theorem findSome?_push {xs : Vector α n} : (xs.push a).findSome? f = (xs.findSome? f).or (f a) := by
+  cases xs; simp [List.findSome?_append]
+
+theorem findSome?_singleton {a : α} {f : α → Option β} : #v[a].findSome? f = f a := by
+  simp
+
 @[simp] theorem findSomeRev?_push_of_isSome {xs : Vector α n} {h : (f a).isSome} : (xs.push a).findSomeRev? f = f a := by
   rcases xs with ⟨xs, rfl⟩
   simp only [push_mk, findSomeRev?_mk, Array.findSomeRev?_push_of_isSome, h]
@@ -130,6 +137,8 @@ abbrev findSome?_mkVector_of_isNone := @findSome?_replicate_of_isNone
 
 /-! ### find? -/
 
+@[simp] theorem find?_empty : find? p #v[] = none := rfl
+
 @[simp] theorem find?_singleton {a : α} {p : α → Bool} :
     #v[a].find? p = if p a then some a else none := by
   simp
@@ -158,6 +167,10 @@ theorem find?_eq_some_iff_append {xs : Vector α n} :
   · rintro ⟨h, k₁, k₂, w, as, bs, h', w'⟩
     exact ⟨h, as.toArray, bs.toArray, by simp [h'], by simpa using w'⟩
 
+theorem find?_push {xs : Vector α n} : (xs.push a).find? p = (xs.find? p).or (if p a then some a else none) := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.find?_push]
+
 @[simp]
 theorem find?_push_eq_some {xs : Vector α n} :
     (xs.push a).find? p = some b ↔ xs.find? p = some b ∨ (xs.find? p = none ∧ (p a ∧ a = b)) := by
@@ -288,12 +301,30 @@ theorem find?_eq_some_iff_getElem {xs : Vector α n} {p : α → Bool} {b : α}
 /-! ### findFinIdx? -/
 
 @[simp] theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p (#v[] : Vector α 0) = none := by simp
+theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
+    #[a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by
+  simp
 
 @[congr] theorem findFinIdx?_congr {p : α → Bool} {xs : Vector α n} {ys : Vector α n} (w : xs = ys) :
     findFinIdx? p xs = findFinIdx? p ys := by
   subst w
   simp
 
+theorem findFinIdx?_push {xs : Vector α n} {a : α} {p : α → Bool} :
+    (xs.push a).findFinIdx? p =
+      ((xs.findFinIdx? p).map Fin.castSucc).or (if p a then some ⟨n, by simp⟩ else none) := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.findFinIdx?_push, Option.map_or, Function.comp_def]
+  congr
+
+theorem findFinIdx?_append {xs : Vector α n₁} {ys : Vector α n₂} {p : α → Bool} :
+    (xs ++ ys).findFinIdx? p =
+      ((xs.findFinIdx? p).map (Fin.castLE (by simp))).or
+        ((ys.findFinIdx? p).map (Fin.natAdd xs.size) |>.map (Fin.cast (by simp))) := by
+  rcases xs with ⟨xs, rfl⟩
+  rcases ys with ⟨ys, rfl⟩
+  simp [Array.findFinIdx?_append, Option.map_or, Function.comp_def]
+
 @[simp]
 theorem isSome_findFinIdx? {xs : Vector α n} {p : α → Bool} :
     (xs.findFinIdx? p).isSome = xs.any p := by

src/Init/Grind/CommRing.lean

@@ -9,3 +9,4 @@ import Init.Grind.CommRing.Int
 import Init.Grind.CommRing.UInt
 import Init.Grind.CommRing.SInt
 import Init.Grind.CommRing.BitVec
+import Init.Grind.CommRing.Poly

src/Init/Grind/CommRing/Basic.lean

@@ -30,6 +30,7 @@ namespace Lean.Grind
 
 class CommRing (α : Type u) extends Add α, Mul α, Neg α, Sub α, HPow α Nat α where
   [ofNat : ∀ n, OfNat α n]
+  [intCast : IntCast α]
   add_assoc : ∀ a b c : α, a + b + c = a + (b + c)
   add_comm : ∀ a b : α, a + b = b + a
   add_zero : ∀ a : α, a + 0 = a
@@ -43,6 +44,8 @@ class CommRing (α : Type u) extends Add α, Mul α, Neg α, Sub α, HPow α Nat
   pow_zero : ∀ a : α, a ^ 0 = 1
   pow_succ : ∀ a : α, ∀ n : Nat, a ^ (n + 1) = (a ^ n) * a
   ofNat_succ : ∀ a : Nat, OfNat.ofNat (α := α) (a + 1) = OfNat.ofNat a + 1 := by intros; rfl
+  intCast_ofNat : ∀ n : Nat, Int.cast (OfNat.ofNat (α := Int) n) = OfNat.ofNat (α := α) n := by intros; rfl
+  intCast_neg : ∀ i : Int, Int.cast (R := α) (-i) = -Int.cast i := by intros; rfl
 
 -- We reduce the priority of these parent instances,
 -- so that in downstream libraries with their own `CommRing` class,
@@ -53,11 +56,14 @@ attribute [instance 100] CommRing.toAdd CommRing.toMul CommRing.toNeg CommRing.t
 -- This is a low-priority instance, to avoid conflicts with existing `OfNat` instances.
 attribute [instance 100] CommRing.ofNat
 
+-- This is a low-priority instance, to avoid conflicts with existing `IntCast` instances.
+attribute [instance 100] CommRing.intCast
+
 namespace CommRing
 
 variable {α : Type u} [CommRing α]
 
-instance : NatCast α where
+instance natCastInst : NatCast α where
   natCast n := OfNat.ofNat n
 
 theorem natCast_zero : ((0 : Nat) : α) = 0 := rfl
@@ -69,6 +75,7 @@ theorem ofNat_add (a b : Nat) : OfNat.ofNat (α := α) (a + b) = OfNat.ofNat a +
   | succ b ih => rw [Nat.add_succ, ofNat_succ, ih, ofNat_succ b, add_assoc]
 
 theorem natCast_succ (n : Nat) : ((n + 1 : Nat) : α) = ((n : α) + 1) := ofNat_add _ _
+theorem natCast_add (a b : Nat) : ((a + b : Nat) : α) = ((a : α) + (b : α)) := ofNat_add _ _
 
 theorem zero_add (a : α) : 0 + a = a := by
   rw [add_comm, add_zero]
@@ -96,6 +103,9 @@ theorem ofNat_mul (a b : Nat) : OfNat.ofNat (α := α) (a * b) = OfNat.ofNat a *
   | zero => simp [Nat.mul_zero, mul_zero]
   | succ a ih => rw [Nat.mul_succ, ofNat_add, ih, ofNat_add, left_distrib, mul_one]
 
+theorem natCast_mul (a b : Nat) : ((a * b : Nat) : α) = ((a : α) * (b : α)) := by
+  rw [← ofNat_eq_natCast, ofNat_mul, ofNat_eq_natCast, ofNat_eq_natCast]
+
 theorem add_left_inj {a b : α} (c : α) : a + c = b + c ↔ a = b :=
   ⟨fun h => by simpa [add_assoc, add_neg_cancel, add_zero] using (congrArg (· + -c) h),
    fun g => congrArg (· + c) g⟩
@@ -125,25 +135,25 @@ theorem neg_sub (a b : α) : -(a - b) = b - a := by
 theorem sub_self (a : α) : a - a = 0 := by
   rw [sub_eq_add_neg, add_neg_cancel]
 
-instance : IntCast α where
-  intCast n := match n with
-  | Int.ofNat n => OfNat.ofNat n
-  | Int.negSucc n => -OfNat.ofNat (n + 1)
+theorem sub_eq_iff {a b c : α} : a - b = c ↔ a = c + b := by
+  rw [sub_eq_add_neg]
+  constructor
+  next => intro; subst c; rw [add_assoc, neg_add_cancel, add_zero]
+  next => intro; subst a; rw [add_assoc, add_comm b, neg_add_cancel, add_zero]
 
-theorem intCast_zero : ((0 : Int) : α) = 0 := rfl
-theorem intCast_one : ((1 : Int) : α) = 1 := rfl
-theorem intCast_neg_one : ((-1 : Int) : α) = -1 := rfl
-theorem intCast_ofNat (n : Nat) : ((n : Int) : α) = (n : α) := rfl
-theorem intCast_ofNat_add_one (n : Nat) : ((n + 1 : Int) : α) = (n : α) + 1 := ofNat_add _ _
-theorem intCast_negSucc (n : Nat) : ((-(n + 1) : Int) : α) = -((n : α) + 1) := congrArg (- ·) (ofNat_add _ _)
-theorem intCast_neg (x : Int) : ((-x : Int) : α) = - (x : α) :=
-  match x with
-  | (0 : Nat) => neg_zero.symm
-  | (n + 1 : Nat) => by
-    rw [Int.natCast_add, Int.cast_ofNat_Int, intCast_negSucc, intCast_ofNat_add_one]
-  | -((n : Nat) + 1) => by
-    rw [Int.neg_neg, intCast_ofNat_add_one, intCast_negSucc, neg_neg]
-theorem intCast_nat_add {x y : Nat} : ((x + y : Int) : α) = ((x : α) + (y : α)) := ofNat_add _ _
+theorem sub_eq_zero_iff {a b : α} : a - b = 0 ↔ a = b := by
+  simp [sub_eq_iff, zero_add]
+
+theorem intCast_zero : ((0 : Int) : α) = 0 := intCast_ofNat 0
+theorem intCast_one : ((1 : Int) : α) = 1 := intCast_ofNat 1
+theorem intCast_neg_one : ((-1 : Int) : α) = -1 := by rw [intCast_neg, intCast_ofNat]
+theorem intCast_natCast (n : Nat) : ((n : Int) : α) = (n : α) := intCast_ofNat n
+theorem intCast_natCast_add_one (n : Nat) : ((n + 1 : Int) : α) = (n : α) + 1 := by
+  rw [← Int.natCast_succ, intCast_natCast, natCast_add, ofNat_eq_natCast]
+theorem intCast_negSucc (n : Nat) : ((-(n + 1) : Int) : α) = -((n : α) + 1) := by
+  rw [intCast_neg, ← Int.natCast_succ, intCast_natCast, ofNat_eq_natCast, natCast_add]
+theorem intCast_nat_add {x y : Nat} : ((x + y : Int) : α) = ((x : α) + (y : α)) := by
+  rw [Int.ofNat_add_ofNat, intCast_natCast, natCast_add]
 theorem intCast_nat_sub {x y : Nat} (h : x ≥ y) : (((x - y : Nat) : Int) : α) = ((x : α) - (y : α)) := by
   induction x with
   | zero =>
@@ -153,29 +163,30 @@ theorem intCast_nat_sub {x y : Nat} (h : x ≥ y) : (((x - y : Nat) : Int) : α)
     by_cases h : x + 1 = y
     · simp [h, intCast_zero, sub_self]
     · have : ((x + 1 - y : Nat) : Int) = (x - y : Nat) + 1 := by omega
-      rw [this, intCast_ofNat_add_one]
+      rw [this, intCast_natCast_add_one]
       specialize ih (by omega)
-      rw [intCast_ofNat] at ih
+      rw [intCast_natCast] at ih
       rw [ih, natCast_succ, sub_eq_add_neg, sub_eq_add_neg, add_assoc, add_comm _ 1, ← add_assoc]
 theorem intCast_add (x y : Int) : ((x + y : Int) : α) = ((x : α) + (y : α)) :=
   match x, y with
-  | (x : Nat), (y : Nat) => ofNat_add _ _
+  | (x : Nat), (y : Nat) => by
+    rw [intCast_nat_add, intCast_natCast, intCast_natCast]
   | (x : Nat), (-(y + 1 : Nat)) => by
     by_cases h : x ≥ y + 1
     · have : (x + -(y+1 : Nat) : Int) = ((x - (y + 1) : Nat) : Int) := by omega
-      rw [this, intCast_neg, intCast_nat_sub h, intCast_ofNat, intCast_ofNat, sub_eq_add_neg]
+      rw [this, intCast_neg, intCast_nat_sub h, intCast_natCast, intCast_natCast, sub_eq_add_neg]
     · have : (x + -(y+1 : Nat) : Int) = (-(y + 1 - x : Nat) : Int) := by omega
-      rw [this, intCast_neg, intCast_nat_sub (by omega), intCast_ofNat, intCast_neg, intCast_ofNat,
+      rw [this, intCast_neg, intCast_nat_sub (by omega), intCast_natCast, intCast_neg, intCast_natCast,
         neg_sub, sub_eq_add_neg]
   | (-(x + 1 : Nat)), (y : Nat) => by
     by_cases h : y ≥ x+ 1
     · have : (-(x+1 : Nat) + y : Int) = ((y - (x + 1) : Nat) : Int) := by omega
-      rw [this, intCast_neg, intCast_nat_sub h, intCast_ofNat, intCast_ofNat, sub_eq_add_neg, add_comm]
+      rw [this, intCast_neg, intCast_nat_sub h, intCast_natCast, intCast_natCast, sub_eq_add_neg, add_comm]
     · have : (-(x+1 : Nat) + y : Int) = (-(x + 1 - y : Nat) : Int) := by omega
-      rw [this, intCast_neg, intCast_nat_sub (by omega), intCast_ofNat, intCast_neg, intCast_ofNat,
+      rw [this, intCast_neg, intCast_nat_sub (by omega), intCast_natCast, intCast_neg, intCast_natCast,
         neg_sub, sub_eq_add_neg, add_comm]
   | (-(x + 1 : Nat)), (-(y + 1 : Nat)) => by
-    rw [← Int.neg_add, intCast_neg, intCast_nat_add, neg_add, intCast_neg, intCast_neg, intCast_ofNat, intCast_ofNat]
+    rw [← Int.neg_add, intCast_neg, intCast_nat_add, neg_add, intCast_neg, intCast_neg, intCast_natCast, intCast_natCast]
 theorem intCast_sub (x y : Int) : ((x - y : Int) : α) = ((x : α) - (y : α)) := by
   rw [Int.sub_eq_add_neg, intCast_add, intCast_neg, sub_eq_add_neg]
 
@@ -191,17 +202,20 @@ theorem neg_mul (a b : α) : (-a) * b = -(a * b) := by
 theorem mul_neg (a b : α) : a * (-b) = -(a * b) := by
   rw [mul_comm, neg_mul, mul_comm]
 
-theorem intCast_nat_mul (x y : Nat) : ((x * y : Int) : α) = ((x : α) * (y : α)) := ofNat_mul _ _
+theorem intCast_nat_mul (x y : Nat) : ((x * y : Int) : α) = ((x : α) * (y : α)) := by
+  rw [Int.ofNat_mul_ofNat, intCast_natCast, natCast_mul]
+
 theorem intCast_mul (x y : Int) : ((x * y : Int) : α) = ((x : α) * (y : α)) :=
   match x, y with
-  | (x : Nat), (y : Nat) => ofNat_mul _ _
+  | (x : Nat), (y : Nat) => by
+    rw [intCast_nat_mul, intCast_natCast, intCast_natCast]
   | (x : Nat), (-(y + 1 : Nat)) => by
-    rw [Int.mul_neg, intCast_neg, intCast_nat_mul, intCast_neg, mul_neg, intCast_ofNat, intCast_ofNat]
+    rw [Int.mul_neg, intCast_neg, intCast_nat_mul, intCast_neg, mul_neg, intCast_natCast, intCast_natCast]
   | (-(x + 1 : Nat)), (y : Nat) => by
-    rw [Int.neg_mul, intCast_neg, intCast_nat_mul, intCast_neg, neg_mul, intCast_ofNat, intCast_ofNat]
+    rw [Int.neg_mul, intCast_neg, intCast_nat_mul, intCast_neg, neg_mul, intCast_natCast, intCast_natCast]
   | (-(x + 1 : Nat)), (-(y + 1 : Nat)) => by
     rw [Int.neg_mul_neg, intCast_neg, intCast_neg, neg_mul, mul_neg, neg_neg, intCast_nat_mul,
-      intCast_ofNat, intCast_ofNat]
+      intCast_natCast, intCast_natCast]
 
 theorem intCast_pow (x : Int) (k : Nat) : ((x ^ k : Int) : α) = (x : α) ^ k := by
   induction k
@@ -217,7 +231,7 @@ end CommRing
 
 open CommRing
 
-class IsCharP (α : Type u) [CommRing α] (p : Nat) where
+class IsCharP (α : Type u) [CommRing α] (p : outParam Nat) where
   ofNat_eq_zero_iff (p) : ∀ (x : Nat), OfNat.ofNat (α := α) x = 0 ↔ x % p = 0
 
 namespace IsCharP
@@ -231,10 +245,10 @@ theorem intCast_eq_zero_iff (x : Int) : (x : α) = 0 ↔ x % p = 0 :=
   match x with
   | (x : Nat) => by
     have := ofNat_eq_zero_iff (α := α) p (x := x)
-    rw [Int.ofNat_mod_ofNat]
+    rw [Int.ofNat_mod_ofNat, intCast_natCast]
     norm_cast
   | -(x + 1 : Nat) => by
-    rw [Int.neg_emod, Int.ofNat_mod_ofNat, intCast_neg, intCast_ofNat, neg_eq_zero]
+    rw [Int.neg_emod, Int.ofNat_mod_ofNat, intCast_neg, intCast_natCast, neg_eq_zero]
     have := ofNat_eq_zero_iff (α := α) p (x := x + 1)
     rw [ofNat_eq_natCast] at this
     rw [this]
@@ -264,7 +278,7 @@ theorem intCast_ext_iff {x y : Int} : (x : α) = (y : α) ↔ x % p = y % p := b
 
 theorem ofNat_ext_iff {x y : Nat} : OfNat.ofNat (α := α) x = OfNat.ofNat (α := α) y ↔ x % p = y % p := by
   have := intCast_ext_iff (α := α) p (x := x) (y := y)
-  simp only [intCast_ofNat, ← Int.ofNat_emod] at this
+  simp only [intCast_natCast, ← Int.ofNat_emod] at this
   simp only [ofNat_eq_natCast]
   norm_cast at this
 
@@ -279,7 +293,7 @@ theorem intCast_emod (x : Int) : ((x % p : Int) : α) = (x : α) := by
   rw [intCast_ext_iff p, Int.emod_emod]
 
 theorem natCast_emod (x : Nat) : ((x % p : Nat) : α) = (x : α) := by
-  simp only [← intCast_ofNat]
+  simp only [← intCast_natCast]
   rw [Int.ofNat_emod, intCast_emod]
 
 theorem ofNat_emod (x : Nat) : OfNat.ofNat (α := α) (x % p) = OfNat.ofNat x :=

src/Init/Grind/CommRing/BitVec.lean

@@ -23,6 +23,7 @@ instance : CommRing (BitVec w) where
   pow_zero _ := BitVec.pow_zero
   pow_succ _ _ := BitVec.pow_succ
   ofNat_succ x := BitVec.ofNat_add x 1
+  intCast_neg _ := BitVec.ofInt_neg
 
 instance : IsCharP (BitVec w) (2 ^ w) where
   ofNat_eq_zero_iff {x} := by simp [BitVec.ofInt, BitVec.toNat_eq]

src/Init/Grind/CommRing/Poly.lean

@@ -5,7 +5,9 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Nat.Lemmas
+import Init.Data.Hashable
 import Init.Data.Ord
+import Init.Data.RArray
 import Init.Grind.CommRing.Basic
 
 namespace Lean.Grind
@@ -23,34 +25,34 @@ inductive Expr where
   | pow (a : Expr) (k : Nat)
   deriving Inhabited, BEq
 
--- TODO: add support for universes to Lean.RArray
-inductive RArray (α : Type u) : Type u where
-  | leaf : α → RArray α
-  | branch : Nat → RArray α → RArray α → RArray α
-
-def RArray.get (a : RArray α) (n : Nat) : α :=
-  match a with
-  | .leaf x => x
-  | .branch p l r => if n < p then l.get n else r.get n
-
 abbrev Context (α : Type u) := RArray α
 
 def Var.denote {α} (ctx : Context α) (v : Var) : α :=
   ctx.get v
 
+def denoteInt {α} [CommRing α] (k : Int) : α :=
+  bif k < 0 then
+    - OfNat.ofNat (α := α) k.natAbs
+  else
+    OfNat.ofNat (α := α) k.natAbs
+
 def Expr.denote {α} [CommRing α] (ctx : Context α) : Expr → α
   | .add a b  => denote ctx a + denote ctx b
   | .sub a b  => denote ctx a - denote ctx b
   | .mul a b  => denote ctx a * denote ctx b
   | .neg a    => -denote ctx a
-  | .num k    => k
+  | .num k    => denoteInt k
   | .var v    => v.denote ctx
   | .pow a k  => denote ctx a ^ k
 
 structure Power where
   x : Var
   k : Nat
-  deriving BEq, Repr
+  deriving BEq, Repr, Inhabited
+
+instance : LawfulBEq Power where
+  eq_of_beq {a} := by cases a <;> intro b <;> cases b <;> simp_all! [BEq.beq]
+  rfl := by intro a; cases a <;> simp! [BEq.beq]
 
 def Power.varLt (p₁ p₂ : Power) : Bool :=
   p₁.x.blt p₂.x
@@ -63,50 +65,48 @@ def Power.denote {α} [CommRing α] (ctx : Context α) : Power → α
     | k => x.denote ctx ^ k
 
 inductive Mon where
-  | leaf (p : Power)
-  | cons (p : Power) (m : Mon)
-  deriving BEq, Repr
+  | unit
+  | mult (p : Power) (m : Mon)
+  deriving BEq, Repr, Inhabited
+
+instance : LawfulBEq Mon where
+  eq_of_beq {a} := by
+    induction a <;> intro b <;> cases b <;> simp_all! [BEq.beq]
+    next p₁ m₁ p₂ m₂ ih =>
+      cases p₁ <;> cases p₂ <;> simp <;> intros <;> simp [*]
+      next h => exact ih h
+  rfl := by
+    intro a
+    induction a <;> simp! [BEq.beq]
+    assumption
 
 def Mon.denote {α} [CommRing α] (ctx : Context α) : Mon → α
-  | .leaf p => p.denote ctx
-  | .cons p m => p.denote ctx * denote ctx m
-
-def Mon.denote' {α} [CommRing α] (ctx : Context α) : Mon → α
-  | .leaf p => p.denote ctx
-  | .cons p m => go (p.denote ctx) m
-where
-  go (acc : α) : Mon → α
-    | .leaf p => acc * p.denote ctx
-    | .cons p m => go (acc * p.denote ctx) m
+  | unit => 1
+  | .mult p m => p.denote ctx * denote ctx m
 
 def Mon.ofVar (x : Var) : Mon :=
-  .leaf { x, k := 1 }
+  .mult { x, k := 1 } .unit
 
 def Mon.concat (m₁ m₂ : Mon) : Mon :=
   match m₁ with
-  | .leaf p => .cons p m₂
-  | .cons p m₁ => .cons p (concat m₁ m₂)
+  | .unit => m₂
+  | .mult pw m₁ => .mult pw (concat m₁ m₂)
 
-def Mon.mulPow (p : Power) (m : Mon) : Mon :=
+def Mon.mulPow (pw : Power) (m : Mon) : Mon :=
   match m with
-  | .leaf p' =>
-    bif p.varLt p' then
-      .cons p m
-    else bif p'.varLt p then
-      .cons p' (.leaf p)
+  | .unit =>
+    .mult pw .unit
+  | .mult pw' m =>
+    bif pw.varLt pw' then
+      .mult pw (.mult pw' m)
+    else bif pw'.varLt pw then
+      .mult pw' (mulPow pw m)
     else
-      .leaf { x := p.x, k := p.k + p'.k }
-  | .cons p' m =>
-    bif p.varLt p' then
-      .cons p (.cons p' m)
-    else bif p'.varLt p then
-      .cons p' (mulPow p m)
-    else
-      .cons { x := p.x, k := p.k + p'.k } m
+      .mult { x := pw.x, k := pw.k + pw'.k } m
 
 def Mon.length : Mon → Nat
-  | .leaf _ => 1
-  | .cons _ m => 1 + length m
+  | .unit => 0
+  | .mult _ m => 1 + length m
 
 def hugeFuel := 1000000
 
@@ -119,19 +119,19 @@ where
     | 0 => concat m₁ m₂
     | fuel + 1 =>
       match m₁, m₂ with
-      | m₁, .leaf p => m₁.mulPow p
-      | .leaf p, m₂ => m₂.mulPow p
-      | .cons p₁ m₁, .cons p₂ m₂ =>
-        bif p₁.varLt p₂ then
-          .cons p₁ (go fuel m₁ (.cons p₂ m₂))
-        else bif p₂.varLt p₁ then
-          .cons p₂ (go fuel (.cons p₁ m₁) m₂)
+      | m₁, .unit => m₁
+      | .unit, m₂ => m₂
+      | .mult pw₁ m₁, .mult pw₂ m₂ =>
+        bif pw₁.varLt pw₂ then
+          .mult pw₁ (go fuel m₁ (.mult pw₂ m₂))
+        else bif pw₂.varLt pw₁ then
+          .mult pw₂ (go fuel (.mult pw₁ m₁) m₂)
         else
-          .cons { x := p₁.x, k := p₁.k + p₂.k } (go fuel m₁ m₂)
+          .mult { x := pw₁.x, k := pw₁.k + pw₂.k } (go fuel m₁ m₂)
 
 def Mon.degree : Mon → Nat
-  | .leaf p => p.k
-  | .cons p m => p.k + degree m
+  | .unit => 0
+  | .mult pw m => pw.k + degree m
 
 def Var.revlex (x y : Var) : Ordering :=
   bif x.blt y then .gt
@@ -148,24 +148,16 @@ def Power.revlex (p₁ p₂ : Power) : Ordering :=
 
 def Mon.revlexWF (m₁ m₂ : Mon) : Ordering :=
   match m₁, m₂ with
-  | .leaf p₁, .leaf p₂ => p₁.revlex p₂
-  | .leaf p₁, .cons p₂ m₂ =>
-    bif p₁.x.ble p₂.x  then
-      .gt
+  | .unit, .unit => .eq
+  | .unit, .mult .. => .gt
+  | .mult .., .unit => .lt
+  | .mult pw₁ m₁, .mult pw₂ m₂ =>
+    bif pw₁.x == pw₂.x then
+      revlexWF m₁ m₂ |>.then (powerRevlex pw₁.k pw₂.k)
+    else bif pw₁.x.blt pw₂.x then
+      revlexWF m₁ (.mult pw₂ m₂) |>.then .gt
     else
-      revlexWF (.leaf p₁) m₂ |>.then .gt
-  | .cons p₁ m₁, .leaf p₂ =>
-    bif p₂.x.ble p₁.x then
-      .lt
-    else
-      revlexWF m₁ (.leaf p₂) |>.then .lt
-  | .cons p₁ m₁, .cons p₂ m₂ =>
-    bif p₁.x == p₂.x then
-      revlexWF m₁ m₂ |>.then (powerRevlex p₁.k p₂.k)
-    else bif p₁.x.blt p₂.x then
-      revlexWF m₁ (.cons p₂ m₂) |>.then .gt
-    else
-      revlexWF (.cons p₁ m₁) m₂ |>.then .lt
+      revlexWF (.mult pw₁ m₁) m₂ |>.then .lt
 
 def Mon.revlexFuel (fuel : Nat) (m₁ m₂ : Mon) : Ordering :=
   match fuel with
@@ -175,24 +167,16 @@ def Mon.revlexFuel (fuel : Nat) (m₁ m₂ : Mon) : Ordering :=
     revlexWF m₁ m₂
   | fuel + 1 =>
     match m₁, m₂ with
-    | .leaf p₁, .leaf p₂ => p₁.revlex p₂
-    | .leaf p₁, .cons p₂ m₂ =>
-      bif p₁.x.ble p₂.x  then
-        .gt
+    | .unit, .unit => .eq
+    | .unit, .mult ..  => .gt
+    | .mult .., .unit => .lt
+    | .mult pw₁ m₁, .mult pw₂ m₂ =>
+      bif pw₁.x == pw₂.x then
+        revlexFuel fuel m₁ m₂ |>.then (powerRevlex pw₁.k pw₂.k)
+      else bif pw₁.x.blt pw₂.x then
+        revlexFuel fuel m₁ (.mult pw₂ m₂) |>.then .gt
       else
-        revlexFuel fuel (.leaf p₁) m₂ |>.then .gt
-    | .cons p₁ m₁, .leaf p₂ =>
-      bif p₂.x.ble p₁.x then
-        .lt
-      else
-        revlexFuel fuel m₁ (.leaf p₂) |>.then .lt
-    | .cons p₁ m₁, .cons p₂ m₂ =>
-      bif p₁.x == p₂.x then
-        revlexFuel fuel m₁ m₂ |>.then (powerRevlex p₁.k p₂.k)
-      else bif p₁.x.blt p₂.x then
-        revlexFuel fuel m₁ (.cons p₂ m₂) |>.then .gt
-      else
-        revlexFuel fuel (.cons p₁ m₁) m₂ |>.then .lt
+        revlexFuel fuel (.mult pw₁ m₁) m₂ |>.then .lt
 
 def Mon.revlex (m₁ m₂ : Mon) : Ordering :=
   revlexFuel hugeFuel m₁ m₂
@@ -203,7 +187,21 @@ def Mon.grevlex (m₁ m₂ : Mon) : Ordering :=
 inductive Poly where
   | num (k : Int)
   | add (k : Int) (v : Mon) (p : Poly)
-  deriving BEq
+  deriving BEq, Inhabited
+
+instance : LawfulBEq Poly where
+  eq_of_beq {a} := by
+    induction a <;> intro b <;> cases b <;> simp_all! [BEq.beq]
+    intro h₁ h₂ h₃
+    next m₁ p₁ _ m₂ p₂ ih =>
+    replace h₂ : m₁ == m₂ := h₂
+    simp [ih h₃, eq_of_beq h₂]
+  rfl := by
+    intro a
+    induction a <;> simp! [BEq.beq]
+    next k m p ih =>
+    show m == m ∧ p == p
+    simp [ih]
 
 def Poly.denote [CommRing α] (ctx : Context α) (p : Poly) : α :=
   match p with
@@ -216,14 +214,26 @@ def Poly.ofMon (m : Mon) : Poly :=
 def Poly.ofVar (x : Var) : Poly :=
   ofMon (Mon.ofVar x)
 
+def Poly.isSorted : Poly → Bool
+  | .num _ => true
+  | .add _ _ (.num _) => true
+  | .add _ m₁ (.add k m₂ p) => m₁.grevlex m₂ == .gt && (Poly.add k m₂ p).isSorted
+
 def Poly.addConst (p : Poly) (k : Int) : Poly :=
-  match p with
+  bif k == 0 then
+    p
+  else
+    go p
+where
+  go : Poly → Poly
   | .num k' => .num (k' + k)
-  | .add k' m p => .add k' m (addConst p k)
+  | .add k' m p => .add k' m (go p)
 
 def Poly.insert (k : Int) (m : Mon) (p : Poly) : Poly :=
   bif k == 0 then
     p
+  else bif m == .unit then
+    p.addConst k
   else
     go p
 where
@@ -232,13 +242,13 @@ where
     | .add k' m' p =>
       match m.grevlex m' with
       | .eq =>
-        let k'' := k + k'
-        bif k'' == 0 then
+        let k := k + k'
+        bif k == 0 then
           p
         else
-          .add k'' m p
-      | .lt => .add k m (.add k' m' p)
-      | .gt => .add k' m' (go p)
+          .add k m p
+      | .gt => .add k m (.add k' m' p)
+      | .lt => .add k' m' (go p)
 
 def Poly.concat (p₁ p₂ : Poly) : Poly :=
   match p₁ with
@@ -260,11 +270,17 @@ where
 def Poly.mulMon (k : Int) (m : Mon) (p : Poly) : Poly :=
   bif k == 0 then
     .num 0
+  else bif m == .unit then
+    p.mulConst k
   else
     go p
 where
   go : Poly → Poly
-   | .num k' => .add (k*k') m (.num 0)
+   | .num k' =>
+     bif k' == 0 then
+       .num 0
+     else
+       .add (k*k') m (.num 0)
    | .add k' m' p => .add (k*k') (m.mul m') (go p)
 
 def Poly.combine (p₁ p₂ : Poly) : Poly :=
@@ -285,8 +301,8 @@ where
             go fuel p₁ p₂
           else
             .add k m₁ (go fuel p₁ p₂)
-        | .lt => .add k₁ m₁ (go fuel p₁ (.add k₂ m₂ p₂))
-        | .gt => .add k₂ m₂ (go fuel (.add k₁ m₁ p₁) p₂)
+        | .gt => .add k₁ m₁ (go fuel p₁ (.add k₂ m₂ p₂))
+        | .lt => .add k₂ m₂ (go fuel (.add k₁ m₁ p₁) p₂)
 
 def Poly.mul (p₁ : Poly) (p₂ : Poly) : Poly :=
   go p₁ (.num 0)
@@ -312,15 +328,17 @@ def Expr.toPoly : Expr → Poly
   | .pow a k =>
     match a with
     | .num n => .num (n^k)
-    | .var x => Poly.ofMon (.leaf {x, k})
+    | .var x => Poly.ofMon (.mult {x, k} .unit)
     | _ => a.toPoly.pow k
 
 /-!
 **Definitions for the `IsCharP` case**
 
-We considered using a single set of definitions parameterized by `Option c`, but decided against it to avoid
-unnecessary kernel‑reduction overhead. Once we can specialize definitions before they reach the kernel,
+We considered using a single set of definitions parameterized by `Option c` or simply set `c = 0` since
+`n % 0 = n` in Lean, but decided against it to avoid unnecessary kernel‑reduction overhead.
+Once we can specialize definitions before they reach the kernel,
 we can merge the two versions. Until then, the `IsCharP` definitions will carry the `C` suffix.
+We use them whenever we can infer the characteristic using type class instance synthesis.
 -/
 def Poly.addConstC (p : Poly) (k : Int) (c : Nat) : Poly :=
   match p with
@@ -344,8 +362,8 @@ where
           p
         else
           .add k'' m p
-      | .lt => .add k m (.add k' m' p)
-      | .gt => .add k' m' (go k p)
+      | .gt => .add k m (.add k' m' p)
+      | .lt => .add k' m' (go k p)
 
 def Poly.mulConstC (k : Int) (p : Poly) (c : Nat) : Poly :=
   let k := k % c
@@ -404,8 +422,8 @@ where
             go fuel p₁ p₂
           else
             .add k m₁ (go fuel p₁ p₂)
-        | .lt => .add k₁ m₁ (go fuel p₁ (.add k₂ m₂ p₂))
-        | .gt => .add k₂ m₂ (go fuel (.add k₁ m₁ p₁) p₂)
+        | .gt => .add k₁ m₁ (go fuel p₁ (.add k₂ m₂ p₂))
+        | .lt => .add k₂ m₂ (go fuel (.add k₁ m₁ p₁) p₂)
 
 def Poly.mulC (p₁ : Poly) (p₂ : Poly) (c : Nat) : Poly :=
   go p₁ (.num 0)
@@ -434,36 +452,74 @@ where
     | .pow a k =>
       match a with
       | .num n => .num ((n^k) % c)
-      | .var x => Poly.ofMon (.leaf {x, k})
+      | .var x => Poly.ofMon (.mult {x, k} .unit)
       | _ => (go a).powC k c
 
+/--
+A Nullstellensatz certificate.
+```
+lhs₁ = rh₁ → ... → lhsₙ = rhₙ → q₁*(lhs₁ - rhs₁) + ... + qₙ*(lhsₙ - rhsₙ) = 0
+```
+-/
+inductive NullCert where
+  | empty
+  | add (q : Poly) (lhs : Expr) (rhs : Expr) (s : NullCert)
+
+/--
+```
+q₁*(lhs₁ - rhs₁) + ... + qₙ*(lhsₙ - rhsₙ)
+```
+-/
+def NullCert.denote {α} [CommRing α] (ctx : Context α) : NullCert → α
+  | .empty => 0
+  | .add q lhs rhs nc => (q.denote ctx)*(lhs.denote ctx - rhs.denote ctx) + nc.denote ctx
+
+/--
+```
+lhs₁ = rh₁ → ... → lhsₙ = rhₙ → p
+```
+-/
+def NullCert.eqsImplies {α} [CommRing α] (ctx : Context α) (nc : NullCert) (p : Prop) : Prop :=
+  match nc with
+  | .empty           => p
+  | .add _ lhs rhs nc => lhs.denote ctx = rhs.denote ctx → eqsImplies ctx nc p
+
+/--
+A polynomial representing
+```
+q₁*(lhs₁ - rhs₁) + ... + qₙ*(lhsₙ - rhsₙ)
+```
+-/
+def NullCert.toPoly (nc : NullCert) : Poly :=
+  match nc with
+  | .empty => .num 0
+  | .add q lhs rhs nc => (q.mul (lhs.sub rhs).toPoly).combine nc.toPoly
+
+def NullCert.toPolyC (nc : NullCert) (c : Nat) : Poly :=
+  match nc with
+  | .empty => .num 0
+  | .add q lhs rhs nc => (q.mulC ((lhs.sub rhs).toPolyC c) c).combineC (nc.toPolyC c) c
+
 /-!
 Theorems for justifying the procedure for commutative rings in `grind`.
 -/
 
+theorem denoteInt_eq {α} [CommRing α] (k : Int) : denoteInt (α := α) k = k := by
+  simp [denoteInt, cond_eq_if] <;> split
+  next h => rw [ofNat_eq_natCast, ← intCast_natCast, ← intCast_neg, ← Int.eq_neg_natAbs_of_nonpos (Int.le_of_lt h)]
+  next h => rw [ofNat_eq_natCast, ← intCast_natCast, ← Int.eq_natAbs_of_nonneg (Int.le_of_not_gt h)]
+
 theorem Power.denote_eq {α} [CommRing α] (ctx : Context α) (p : Power)
     : p.denote ctx = p.x.denote ctx ^ p.k := by
   cases p <;> simp [Power.denote] <;> split <;> simp [pow_zero, pow_succ, one_mul]
 
-theorem Mon.denote'_go_eq_denote {α} [CommRing α] (ctx : Context α) (a : α) (m : Mon)
-    : denote'.go ctx a m = a * denote ctx m := by
-  induction m generalizing a <;> simp [Mon.denote, Mon.denote'.go]
-  next p' m ih =>
-    simp [Mon.denote] at ih
-    rw [ih, mul_assoc]
-
-theorem Mon.denote'_eq_denote {α} [CommRing α] (ctx : Context α) (m : Mon)
-    : denote' ctx m = denote ctx m := by
-  cases m <;> simp [Mon.denote, Mon.denote']
-  next p m => apply denote'_go_eq_denote
-
 theorem Mon.denote_ofVar {α} [CommRing α] (ctx : Context α) (x : Var)
     : denote ctx (ofVar x) = x.denote ctx := by
-  simp [denote, ofVar, Power.denote_eq, pow_succ, pow_zero, one_mul]
+  simp [denote, ofVar, Power.denote_eq, pow_succ, pow_zero, one_mul, mul_one]
 
 theorem Mon.denote_concat {α} [CommRing α] (ctx : Context α) (m₁ m₂ : Mon)
     : denote ctx (concat m₁ m₂) = m₁.denote ctx * m₂.denote ctx := by
-  induction m₁ <;> simp [concat, denote, *]
+  induction m₁ <;> simp [concat, denote, one_mul, *]
   next p₁ m₁ ih => rw [mul_assoc]
 
 private theorem le_of_blt_false {a b : Nat} : a.blt b = false → b ≤ a := by
@@ -478,14 +534,7 @@ private theorem eq_of_blt_false {a b : Nat} : a.blt b = false → b.blt a = fals
 
 theorem Mon.denote_mulPow {α} [CommRing α] (ctx : Context α) (p : Power) (m : Mon)
     : denote ctx (mulPow p m) = p.denote ctx * m.denote ctx := by
-  fun_induction mulPow <;> simp [mulPow, *]
-  next => simp [denote]
-  next => simp [denote]; rw [mul_comm]
-  next p' h₁ h₂ =>
-    have := eq_of_blt_false h₁ h₂
-    simp [denote, Power.denote_eq, this, pow_add]
-  next => simp [denote]
-  next => simp [denote, mul_assoc, mul_comm, mul_left_comm, *]
+  fun_induction mulPow <;> simp [mulPow, denote, mul_assoc, mul_comm, mul_left_comm, *]
   next h₁ h₂ =>
     have := eq_of_blt_false h₁ h₂
     simp [denote, Power.denote_eq, pow_add, this, mul_assoc]
@@ -494,10 +543,9 @@ theorem Mon.denote_mul {α} [CommRing α] (ctx : Context α) (m₁ m₂ : Mon)
     : denote ctx (mul m₁ m₂) = m₁.denote ctx * m₂.denote ctx := by
   unfold mul
   generalize hugeFuel = fuel
-  fun_induction mul.go <;> simp [mul.go, denote, denote_concat, denote_mulPow, *]
-  next => rw [mul_comm]
-  next => simp [mul_assoc]
-  next => simp [mul_assoc, mul_left_comm, mul_comm]
+  fun_induction mul.go
+    <;> simp [mul.go, denote, denote_concat, denote_mulPow, one_mul, mul_one,
+      mul_assoc, mul_left_comm, mul_comm, *]
   next h₁ h₂ _ =>
     have := eq_of_blt_false h₁ h₂
     simp [Power.denote_eq, pow_add, mul_assoc, mul_left_comm, mul_comm, this]
@@ -526,7 +574,6 @@ private theorem then_eq (o₁ o₂ : Ordering) : o₁.then o₂ = .eq ↔ o₁ =
 
 theorem Mon.eq_of_revlexWF {m₁ m₂ : Mon} : m₁.revlexWF m₂ = .eq → m₁ = m₂ := by
   fun_induction revlexWF <;> simp [revlexWF, *, then_gt, then_lt, then_eq]
-  next => apply Power.eq_of_revlex
   next p₁ m₁ p₂ m₂ h ih =>
     cases p₁; cases p₂; intro h₁ h₂; simp [ih h₁, h]
     simp at h h₂
@@ -535,7 +582,6 @@ theorem Mon.eq_of_revlexWF {m₁ m₂ : Mon} : m₁.revlexWF m₂ = .eq → m₁
 theorem Mon.eq_of_revlexFuel {fuel : Nat} {m₁ m₂ : Mon} : revlexFuel fuel m₁ m₂ = .eq → m₁ = m₂ := by
   fun_induction revlexFuel <;> simp [revlexFuel, *, then_gt, then_lt, then_eq]
   next => apply eq_of_revlexWF
-  next => apply Power.eq_of_revlex
   next p₁ m₁ p₂ m₂ h ih =>
     cases p₁; cases p₂; intro h₁ h₂; simp [ih h₁, h]
     simp at h h₂
@@ -556,22 +602,29 @@ theorem Poly.denote_ofVar {α} [CommRing α] (ctx : Context α) (x : Var)
   simp [ofVar, denote_ofMon, Mon.denote_ofVar]
 
 theorem Poly.denote_addConst {α} [CommRing α] (ctx : Context α) (p : Poly) (k : Int) : (addConst p k).denote ctx = p.denote ctx + k := by
-  fun_induction addConst <;> simp [addConst, denote, *]
-  next => rw [intCast_add]
-  next => simp [add_comm, add_left_comm, add_assoc]
+  simp [addConst, cond_eq_if]; split
+  next => simp [*, intCast_zero, add_zero]
+  next =>
+    fun_induction addConst.go <;> simp [addConst.go, denote, *]
+    next => rw [intCast_add]
+    next => simp [add_comm, add_left_comm, add_assoc]
 
 theorem Poly.denote_insert {α} [CommRing α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
     : (insert k m p).denote ctx = k * m.denote ctx + p.denote ctx := by
   simp [insert, cond_eq_if] <;> split
   next => simp [*, intCast_zero, zero_mul, zero_add]
   next =>
-    fun_induction insert.go <;> simp_all +zetaDelta [insert.go, denote, cond_eq_if]
-    next h₁ _ h₂ =>
-      rw [← add_assoc, Mon.eq_of_grevlex h₁, ← right_distrib, ← intCast_add, h₂, intCast_zero, zero_mul, zero_add]
-    next h₁ _ _ =>
-      rw [intCast_add, right_distrib, add_assoc, Mon.eq_of_grevlex h₁]
+    split
+    next h =>
+      simp at h <;> simp [*, Mon.denote, denote_addConst, mul_one, add_comm]
     next =>
-      rw [add_left_comm]
+      fun_induction insert.go <;> simp_all +zetaDelta [insert.go, denote, cond_eq_if]
+      next h₁ h₂ =>
+        rw [← add_assoc, Mon.eq_of_grevlex h₁, ← right_distrib, ← intCast_add, h₂, intCast_zero, zero_mul, zero_add]
+      next h₁ _ =>
+        rw [intCast_add, right_distrib, add_assoc, Mon.eq_of_grevlex h₁]
+      next =>
+        rw [add_left_comm]
 
 theorem Poly.denote_concat {α} [CommRing α] (ctx : Context α) (p₁ p₂ : Poly)
     : (concat p₁ p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by
@@ -594,9 +647,14 @@ theorem Poly.denote_mulMon {α} [CommRing α] (ctx : Context α) (k : Int) (m :
   simp [mulMon, cond_eq_if] <;> split
   next => simp [denote, *, intCast_zero, zero_mul]
   next =>
-    fun_induction mulMon.go <;> simp [mulMon.go, denote, *]
-    next => simp [intCast_mul, intCast_zero, add_zero, mul_comm, mul_left_comm, mul_assoc]
-    next => simp [Mon.denote_mul, intCast_mul, left_distrib, mul_comm, mul_left_comm, mul_assoc]
+    split
+    next h =>
+      simp at h; simp [*, Mon.denote, mul_one, denote_mulConst]
+    next =>
+      fun_induction mulMon.go <;> simp [mulMon.go, denote, *]
+      next h => simp +zetaDelta at h; simp [*, intCast_zero, mul_zero]
+      next => simp [intCast_mul, intCast_zero, add_zero, mul_comm, mul_left_comm, mul_assoc]
+      next => simp [Mon.denote_mul, intCast_mul, left_distrib, mul_comm, mul_left_comm, mul_assoc]
 
 theorem Poly.denote_combine {α} [CommRing α] (ctx : Context α) (p₁ p₂ : Poly)
     : (combine p₁ p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by
@@ -629,11 +687,69 @@ theorem Expr.denote_toPoly {α} [CommRing α] (ctx : Context α) (e : Expr)
    : e.toPoly.denote ctx = e.denote ctx := by
   fun_induction toPoly
     <;> simp [toPoly, denote, Poly.denote, Poly.denote_ofVar, Poly.denote_combine,
-          Poly.denote_mul, Poly.denote_mulConst, Poly.denote_pow, *]
-  next => rw [intCast_neg, neg_mul, intCast_one, one_mul]
-  next => rw [intCast_neg, neg_mul, intCast_one, one_mul, sub_eq_add_neg]
-  next => rw [intCast_pow]
-  next => simp [Poly.denote_ofMon, Mon.denote, Power.denote_eq]
+          Poly.denote_mul, Poly.denote_mulConst, Poly.denote_pow, intCast_pow, intCast_neg, intCast_one,
+          neg_mul, one_mul, sub_eq_add_neg, denoteInt_eq, *]
+  next => simp [Poly.denote_ofMon, Mon.denote, Power.denote_eq, mul_one]
+
+theorem Expr.eq_of_toPoly_eq {α} [CommRing α] (ctx : Context α) (a b : Expr) (h : a.toPoly == b.toPoly) : a.denote ctx = b.denote ctx := by
+  have h := congrArg (Poly.denote ctx) (eq_of_beq h)
+  simp [denote_toPoly] at h
+  assumption
+
+def ne_unsat_cert (a b : Expr) : Bool :=
+  (a.sub b).toPoly == .num 0
+
+theorem ne_unsat {α} [CommRing α] (ctx : Context α) (a b : Expr)
+    : ne_unsat_cert a b → a.denote ctx ≠ b.denote ctx → False := by
+  simp [ne_unsat_cert]
+  intro h
+  replace h := congrArg (Poly.denote ctx .) h
+  simp [Poly.denote, Expr.denote, Expr.denote_toPoly, intCast_zero, sub_eq_zero_iff] at h
+  assumption
+
+def eq_unsat_cert (a b : Expr) (k : Int) : Bool :=
+  k != 0 && (a.sub b).toPoly == .num k
+
+-- Remark: `[IsCharP α 0]` after `(ctx : Context α)` is not a mistake.
+-- The `grind` procedure assumes that support theorems start with `{α} [CommRing α] (ctx : Context α)`
+theorem eq_unsat {α} [CommRing α] (ctx : Context α) [IsCharP α 0] (a b : Expr) (k : Int)
+    : eq_unsat_cert a b k → a.denote ctx = b.denote ctx → False := by
+  simp [eq_unsat_cert]
+  intro h₁ h₂
+  replace h₂ := congrArg (Poly.denote ctx .) h₂
+  simp [Poly.denote, Expr.denote, Expr.denote_toPoly, intCast_zero, sub_eq_iff] at h₂
+  have := IsCharP.intCast_eq_zero_iff (α := α) 0 k
+  simp [h₁] at this
+  rw [h₂, Eq.comm, ← sub_eq_iff, sub_self, Eq.comm]
+  assumption
+
+/-- Helper theorem for proving `NullCert` theorems. -/
+theorem NullCert.eqsImplies_helper {α} [CommRing α] (ctx : Context α) (nc : NullCert) (p : Prop) : (nc.denote ctx = 0 → p) → nc.eqsImplies ctx p := by
+  induction nc <;> simp [denote, eqsImplies]
+  next ih =>
+    intro h₁ h₂
+    apply ih
+    simp [h₂, sub_self, mul_zero, zero_add] at h₁
+    assumption
+
+theorem NullCert.denote_toPoly {α} [CommRing α] (ctx : Context α) (nc : NullCert) : nc.toPoly.denote ctx = nc.denote ctx := by
+  induction nc <;> simp [toPoly, denote, Poly.denote, intCast_zero, Poly.denote_combine, Poly.denote_mul, Expr.denote_toPoly, Expr.denote, *]
+
+def NullCert.eq_cert (nc : NullCert) (lhs rhs : Expr) :=
+  (lhs.sub rhs).toPoly == nc.toPoly
+
+theorem NullCert.eq {α} [CommRing α] (ctx : Context α) (nc : NullCert) (lhs rhs : Expr)
+    : nc.eq_cert lhs rhs → nc.eqsImplies ctx (lhs.denote ctx = rhs.denote ctx) := by
+  simp [eq_cert]; intro h₁
+  apply eqsImplies_helper
+  intro h₂
+  replace h₁ := congrArg (Poly.denote ctx) h₁
+  simp [Expr.denote_toPoly, denote_toPoly, h₂, Expr.denote, sub_eq_zero_iff] at h₁
+  assumption
+
+/-!
+Theorems for justifying the procedure for commutative rings with a characteristic in `grind`.
+-/
 
 theorem Poly.denote_addConstC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (p : Poly) (k : Int) : (addConstC p k c).denote ctx = p.denote ctx + k := by
   fun_induction addConstC <;> simp [addConstC, denote, *]
@@ -740,12 +856,58 @@ theorem Expr.denote_toPolyC {α c} [CommRing α] [IsCharP α c] (ctx : Context
   unfold toPolyC
   fun_induction toPolyC.go
     <;> simp [toPolyC.go, denote, Poly.denote, Poly.denote_ofVar, Poly.denote_combineC,
-          Poly.denote_mulC, Poly.denote_mulConstC, Poly.denote_powC, *]
+          Poly.denote_mulC, Poly.denote_mulConstC, Poly.denote_powC, denoteInt_eq, *]
   next => rw [IsCharP.intCast_emod]
   next => rw [intCast_neg, neg_mul, intCast_one, one_mul]
   next => rw [intCast_neg, neg_mul, intCast_one, one_mul, sub_eq_add_neg]
   next => rw [IsCharP.intCast_emod, intCast_pow]
-  next => simp [Poly.denote_ofMon, Mon.denote, Power.denote_eq]
+  next => simp [Poly.denote_ofMon, Mon.denote, Power.denote_eq, mul_one]
+
+theorem Expr.eq_of_toPolyC_eq {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (a b : Expr)
+    (h : a.toPolyC c == b.toPolyC c) : a.denote ctx = b.denote ctx := by
+  have h := congrArg (Poly.denote ctx) (eq_of_beq h)
+  simp [denote_toPolyC] at h
+  assumption
+
+def ne_unsatC_cert (a b : Expr) (c : Nat) : Bool :=
+  (a.sub b).toPolyC c == .num 0
+
+theorem ne_unsatC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (a b : Expr)
+    : ne_unsatC_cert a b c → a.denote ctx ≠ b.denote ctx → False := by
+  simp [ne_unsatC_cert]
+  intro h
+  replace h := congrArg (Poly.denote ctx .) h
+  simp [Poly.denote, Expr.denote, Expr.denote_toPolyC, intCast_zero, sub_eq_zero_iff] at h
+  assumption
+
+def eq_unsatC_cert (a b : Expr) (c : Nat) (k : Int) : Bool :=
+  k != 0 && k % c != 0 && (a.sub b).toPolyC c == .num k
+
+theorem eq_unsatC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (a b : Expr) (k : Int)
+    : eq_unsatC_cert a b c k → a.denote ctx = b.denote ctx → False := by
+  simp [eq_unsatC_cert]
+  intro h₁ h₂ h₃
+  replace h₃ := congrArg (Poly.denote ctx .) h₃
+  simp [Poly.denote, Expr.denote, Expr.denote_toPolyC, intCast_zero, sub_eq_iff] at h₃
+  have := IsCharP.intCast_eq_zero_iff (α := α) c k
+  simp [h₁, h₂] at this
+  rw [h₃, Eq.comm, ← sub_eq_iff, sub_self, Eq.comm]
+  assumption
+
+theorem NullCert.denote_toPolyC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (nc : NullCert) : (nc.toPolyC c).denote ctx = nc.denote ctx := by
+  induction nc <;> simp [toPolyC, denote, Poly.denote, intCast_zero, Poly.denote_combineC, Poly.denote_mulC, Expr.denote_toPolyC, Expr.denote, *]
+
+def NullCert.eq_certC (nc : NullCert) (lhs rhs : Expr) (c : Nat) :=
+  (lhs.sub rhs).toPolyC c == nc.toPoly
+
+theorem NullCert.eqC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (nc : NullCert) (lhs rhs : Expr)
+    : nc.eq_certC lhs rhs c → nc.eqsImplies ctx (lhs.denote ctx = rhs.denote ctx) := by
+  simp [eq_certC]; intro h₁
+  apply eqsImplies_helper
+  intro h₂
+  replace h₁ := congrArg (Poly.denote ctx) h₁
+  simp [Expr.denote_toPolyC, denote_toPoly, h₂, Expr.denote, sub_eq_zero_iff] at h₁
+  assumption
 
 end CommRing
 end Lean.Grind

src/Init/Grind/CommRing/SInt.lean

@@ -26,6 +26,7 @@ instance : CommRing Int8 where
   pow_zero := Int8.pow_zero
   pow_succ := Int8.pow_succ
   ofNat_succ x := Int8.ofNat_add x 1
+  intCast_neg := Int8.ofInt_neg
 
 instance : IsCharP Int8 (2 ^ 8) where
   ofNat_eq_zero_iff {x} := by
@@ -51,7 +52,7 @@ instance : CommRing Int16 where
   pow_zero := Int16.pow_zero
   pow_succ := Int16.pow_succ
   ofNat_succ x := Int16.ofNat_add x 1
-
+  intCast_neg := Int16.ofInt_neg
 instance : IsCharP Int16 (2 ^ 16) where
   ofNat_eq_zero_iff {x} := by
     have : OfNat.ofNat x = Int16.ofInt x := rfl
@@ -76,7 +77,7 @@ instance : CommRing Int32 where
   pow_zero := Int32.pow_zero
   pow_succ := Int32.pow_succ
   ofNat_succ x := Int32.ofNat_add x 1
-
+  intCast_neg := Int32.ofInt_neg
 instance : IsCharP Int32 (2 ^ 32) where
   ofNat_eq_zero_iff {x} := by
     have : OfNat.ofNat x = Int32.ofInt x := rfl
@@ -101,7 +102,7 @@ instance : CommRing Int64 where
   pow_zero := Int64.pow_zero
   pow_succ := Int64.pow_succ
   ofNat_succ x := Int64.ofNat_add x 1
-
+  intCast_neg := Int64.ofInt_neg
 instance : IsCharP Int64 (2 ^ 64) where
   ofNat_eq_zero_iff {x} := by
     have : OfNat.ofNat x = Int64.ofInt x := rfl
@@ -126,7 +127,7 @@ instance : CommRing ISize where
   pow_zero := ISize.pow_zero
   pow_succ := ISize.pow_succ
   ofNat_succ x := ISize.ofNat_add x 1
-
+  intCast_neg := ISize.ofInt_neg
 open System.Platform (numBits)
 
 instance : IsCharP ISize (2 ^ numBits) where

src/Init/Grind/CommRing/UInt.lean

@@ -7,7 +7,6 @@ prelude
 import Init.Grind.CommRing.Basic
 import Init.Data.UInt.Lemmas
 
-
 namespace UInt8
 
 /-- Variant of `UInt8.ofNat_mod_size` replacing `2 ^ 8` with `256`.-/
@@ -16,6 +15,16 @@ theorem ofNat_mod_size' : ofNat (x % 256) = ofNat x := ofNat_mod_size
 instance : IntCast UInt8 where
   intCast x := UInt8.ofInt x
 
+theorem intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : UInt8) = OfNat.ofNat x := by
+    -- A better proof would be welcome!
+    simp only [Int.cast, IntCast.intCast]
+    rw [UInt8.ofInt]
+    rw [Int.toNat_emod (Int.zero_le_ofNat x) (by decide)]
+    erw [Int.toNat_natCast]
+    rw [Int.toNat_pow_of_nonneg (by decide)]
+    simp only [ofNat, BitVec.ofNat, Fin.ofNat', Int.reduceToNat, Nat.dvd_refl,
+      Nat.mod_mod_of_dvd, instOfNat]
+
 end UInt8
 
 namespace UInt16
@@ -26,6 +35,16 @@ theorem ofNat_mod_size' : ofNat (x % 65536) = ofNat x := ofNat_mod_size
 instance : IntCast UInt16 where
   intCast x := UInt16.ofInt x
 
+theorem intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : UInt16) = OfNat.ofNat x := by
+    -- A better proof would be welcome!
+    simp only [Int.cast, IntCast.intCast]
+    rw [UInt16.ofInt]
+    rw [Int.toNat_emod (Int.zero_le_ofNat x) (by decide)]
+    erw [Int.toNat_natCast]
+    rw [Int.toNat_pow_of_nonneg (by decide)]
+    simp only [ofNat, BitVec.ofNat, Fin.ofNat', Int.reduceToNat, Nat.dvd_refl,
+      Nat.mod_mod_of_dvd, instOfNat]
+
 end UInt16
 
 namespace UInt32
@@ -36,6 +55,16 @@ theorem ofNat_mod_size' : ofNat (x % 4294967296) = ofNat x := ofNat_mod_size
 instance : IntCast UInt32 where
   intCast x := UInt32.ofInt x
 
+theorem intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : UInt32) = OfNat.ofNat x := by
+    -- A better proof would be welcome!
+    simp only [Int.cast, IntCast.intCast]
+    rw [UInt32.ofInt]
+    rw [Int.toNat_emod (Int.zero_le_ofNat x) (by decide)]
+    erw [Int.toNat_natCast]
+    rw [Int.toNat_pow_of_nonneg (by decide)]
+    simp only [ofNat, BitVec.ofNat, Fin.ofNat', Int.reduceToNat, Nat.dvd_refl,
+      Nat.mod_mod_of_dvd, instOfNat]
+
 end UInt32
 
 namespace UInt64
@@ -46,6 +75,16 @@ theorem ofNat_mod_size' : ofNat (x % 18446744073709551616) = ofNat x := ofNat_mo
 instance : IntCast UInt64 where
   intCast x := UInt64.ofInt x
 
+theorem intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : UInt64) = OfNat.ofNat x := by
+    -- A better proof would be welcome!
+    simp only [Int.cast, IntCast.intCast]
+    rw [UInt64.ofInt]
+    rw [Int.toNat_emod (Int.zero_le_ofNat x) (by decide)]
+    erw [Int.toNat_natCast]
+    rw [Int.toNat_pow_of_nonneg (by decide)]
+    simp only [ofNat, BitVec.ofNat, Fin.ofNat', Int.reduceToNat, Nat.dvd_refl,
+      Nat.mod_mod_of_dvd, instOfNat]
+
 end UInt64
 
 namespace USize
@@ -53,9 +92,21 @@ namespace USize
 instance : IntCast USize where
   intCast x := USize.ofInt x
 
+theorem intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : USize) = OfNat.ofNat x := by
+    -- A better proof would be welcome!
+    simp only [Int.cast, IntCast.intCast]
+    rw [USize.ofInt]
+    rw [Int.toNat_emod (Int.zero_le_ofNat x)]
+    · erw [Int.toNat_natCast]
+      rw [Int.toNat_pow_of_nonneg (by decide)]
+      simp only [ofNat, BitVec.ofNat, Fin.ofNat', Int.reduceToNat, Nat.dvd_refl,
+        Nat.mod_mod_of_dvd, instOfNat]
+    · obtain _ | _ := System.Platform.numBits_eq <;> simp_all
+
 end USize
 namespace Lean.Grind
 
+
 instance : CommRing UInt8 where
   add_assoc := UInt8.add_assoc
   add_comm := UInt8.add_comm
@@ -70,8 +121,10 @@ instance : CommRing UInt8 where
   pow_zero := UInt8.pow_zero
   pow_succ := UInt8.pow_succ
   ofNat_succ x := UInt8.ofNat_add x 1
+  intCast_neg := UInt8.ofInt_neg
+  intCast_ofNat := UInt8.intCast_ofNat
 
-instance : IsCharP UInt8 (2 ^ 8) where
+instance : IsCharP UInt8 256 where
   ofNat_eq_zero_iff {x} := by
     have : OfNat.ofNat x = UInt8.ofNat x := rfl
     simp [this, UInt8.ofNat_eq_iff_mod_eq_toNat]
@@ -90,8 +143,10 @@ instance : CommRing UInt16 where
   pow_zero := UInt16.pow_zero
   pow_succ := UInt16.pow_succ
   ofNat_succ x := UInt16.ofNat_add x 1
+  intCast_neg := UInt16.ofInt_neg
+  intCast_ofNat := UInt16.intCast_ofNat
 
-instance : IsCharP UInt16 (2 ^ 16) where
+instance : IsCharP UInt16 65536 where
   ofNat_eq_zero_iff {x} := by
     have : OfNat.ofNat x = UInt16.ofNat x := rfl
     simp [this, UInt16.ofNat_eq_iff_mod_eq_toNat]
@@ -110,8 +165,10 @@ instance : CommRing UInt32 where
   pow_zero := UInt32.pow_zero
   pow_succ := UInt32.pow_succ
   ofNat_succ x := UInt32.ofNat_add x 1
+  intCast_neg := UInt32.ofInt_neg
+  intCast_ofNat := UInt32.intCast_ofNat
 
-instance : IsCharP UInt32 (2 ^ 32) where
+instance : IsCharP UInt32 4294967296 where
   ofNat_eq_zero_iff {x} := by
     have : OfNat.ofNat x = UInt32.ofNat x := rfl
     simp [this, UInt32.ofNat_eq_iff_mod_eq_toNat]
@@ -130,8 +187,10 @@ instance : CommRing UInt64 where
   pow_zero := UInt64.pow_zero
   pow_succ := UInt64.pow_succ
   ofNat_succ x := UInt64.ofNat_add x 1
+  intCast_neg := UInt64.ofInt_neg
+  intCast_ofNat := UInt64.intCast_ofNat
 
-instance : IsCharP UInt64 (2 ^ 64) where
+instance : IsCharP UInt64 18446744073709551616 where
   ofNat_eq_zero_iff {x} := by
     have : OfNat.ofNat x = UInt64.ofNat x := rfl
     simp [this, UInt64.ofNat_eq_iff_mod_eq_toNat]
@@ -150,6 +209,8 @@ instance : CommRing USize where
   pow_zero := USize.pow_zero
   pow_succ := USize.pow_succ
   ofNat_succ x := USize.ofNat_add x 1
+  intCast_neg := USize.ofInt_neg
+  intCast_ofNat := USize.intCast_ofNat
 
 open System.Platform
 

src/Init/Grind/Tactics.lean

@@ -112,6 +112,10 @@ structure Config where
   That is, `let x := v; e[x]` reduces to `e[v]`. See also `zetaDelta`.
   -/
   zeta := true
+  /--
+  When `true` (default: `false`), uses procedure for handling equalities over commutative rings.
+  -/
+  ring := false
   deriving Inhabited, BEq
 
 end Lean.Grind

src/Init/MetaTypes.lean

@@ -286,4 +286,44 @@ inductive Occurrences where
 
 instance : Coe (List Nat) Occurrences := ⟨.pos⟩
 
+/--
+Configuration for the `extract_lets` tactic.
+-/
+structure ExtractLetsConfig where
+  /-- If true (default: false), extract lets from subterms that are proofs.
+  Top-level lets are always extracted. -/
+  proofs : Bool := false
+  /-- If true (default: true), extract lets from subterms that are types.
+  Top-level lets are always extracted. -/
+  types : Bool := true
+  /-- If true (default: false), extract lets from subterms that are implicit arguments. -/
+  implicits : Bool := false
+  /-- If false (default: true), extracts only top-level lets, otherwise allows descending into subterms.
+  When false, `proofs` and `types` are ignored, and lets appearing in the types or values of the
+  top-level lets are not themselves extracted. -/
+  descend : Bool := true
+  /-- If true (default: true), descend into forall/lambda/let bodies when extracting. Only relevant when `descend` is true. -/
+  underBinder : Bool := true
+  /-- If true (default: false), eliminate unused lets rather than extract them. -/
+  usedOnly : Bool := false
+  /-- If true (default: true), reuse local declarations that have syntactically equal values.
+  Note that even when false, the caching strategy for `extract_let`s may result in fewer extracted let bindings than expected. -/
+  merge : Bool := true
+  /-- When merging is enabled, if true (default: true), make use of pre-existing local definitions in the local context. -/
+  useContext : Bool := true
+  /-- If true (default: false), then once `givenNames` is exhausted, stop extracting lets. Otherwise continue extracting lets. -/
+  onlyGivenNames : Bool := false
+  /-- If true (default: false), then when no name is provided for a 'let' expression, the name is used as-is without making it be inaccessible.
+  The name still might be inaccessible if the binder name was. -/
+  preserveBinderNames : Bool := false
+  /-- If true (default: false), lift non-extractable `let`s as far out as possible. -/
+  lift : Bool := false
+
+/--
+Configuration for the `lift_lets` tactic.
+-/
+structure LiftLetsConfig extends ExtractLetsConfig where
+  lift := true
+  preserveBinderNames := true
+
 end Lean.Meta

src/Init/Prelude.lean

@@ -2037,23 +2037,23 @@ structure BitVec (w : Nat) where
 /--
 Bitvectors have decidable equality.
 
-This should be used via the instance `DecidableEq (BitVec n)`.
+This should be used via the instance `DecidableEq (BitVec w)`.
 -/
 -- We manually derive the `DecidableEq` instances for `BitVec` because
 -- we want to have builtin support for bit-vector literals, and we
 -- need a name for this function to implement `canUnfoldAtMatcher` at `WHNF.lean`.
-def BitVec.decEq (x y : BitVec n) : Decidable (Eq x y) :=
+def BitVec.decEq (x y : BitVec w) : Decidable (Eq x y) :=
   match x, y with
   | ⟨n⟩, ⟨m⟩ =>
     dite (Eq n m)
       (fun h => isTrue (h ▸ rfl))
       (fun h => isFalse (fun h' => BitVec.noConfusion h' (fun h' => absurd h' h)))
 
-instance : DecidableEq (BitVec n) := BitVec.decEq
+instance : DecidableEq (BitVec w) := BitVec.decEq
 
-/-- The `BitVec` with value `i`, given a proof that `i < 2^n`. -/
+/-- The `BitVec` with value `i`, given a proof that `i < 2^w`. -/
 @[match_pattern]
-protected def BitVec.ofNatLT {n : Nat} (i : Nat) (p : LT.lt i (hPow 2 n)) : BitVec n where
+protected def BitVec.ofNatLT {w : Nat} (i : Nat) (p : LT.lt i (hPow 2 w)) : BitVec w where
   toFin := ⟨i, p⟩
 
 /--
@@ -2061,14 +2061,14 @@ Return the underlying `Nat` that represents a bitvector.
 
 This is O(1) because `BitVec` is a (zero-cost) wrapper around a `Nat`.
 -/
-protected def BitVec.toNat (x : BitVec n) : Nat := x.toFin.val
+protected def BitVec.toNat (x : BitVec w) : Nat := x.toFin.val
 
-instance : LT (BitVec n) where lt := (LT.lt ·.toNat ·.toNat)
-instance (x y : BitVec n) : Decidable (LT.lt x y) :=
+instance : LT (BitVec w) where lt := (LT.lt ·.toNat ·.toNat)
+instance (x y : BitVec w) : Decidable (LT.lt x y) :=
   inferInstanceAs (Decidable (LT.lt x.toNat y.toNat))
 
-instance : LE (BitVec n) where le := (LE.le ·.toNat ·.toNat)
-instance (x y : BitVec n) : Decidable (LE.le x y) :=
+instance : LE (BitVec w) where le := (LE.le ·.toNat ·.toNat)
+instance (x y : BitVec w) : Decidable (LE.le x y) :=
   inferInstanceAs (Decidable (LE.le x.toNat y.toNat))
 
 /-- The number of distinct values representable by `UInt8`, that is, `2^8 = 256`. -/

src/Init/Tactics.lean

@@ -496,6 +496,38 @@ syntax (name := change) "change " term (location)? : tactic
 -/
 syntax (name := changeWith) "change " term " with " term (location)? : tactic
 
+/--
+Extracts `let` and `let_fun` expressions from within the target or a local hypothesis,
+introducing new local definitions.
+
+- `extract_lets` extracts all the lets from the target.
+- `extract_lets x y z` extracts all the lets from the target and uses `x`, `y`, and `z` for the first names.
+  Using `_` for a name leaves it unnamed.
+- `extract_lets x y z at h` operates on the local hypothesis `h` instead of the target.
+
+For example, given a local hypotheses if the form `h : let x := v; b x`, then `extract_lets z at h`
+introduces a new local definition `z := v` and changes `h` to be `h : b z`.
+-/
+syntax (name := extractLets) "extract_lets " optConfig (ppSpace colGt (ident <|> hole))* (location)? : tactic
+
+/--
+Lifts `let` and `let_fun` expressions within a term as far out as possible.
+It is like `extract_lets +lift`, but the top-level lets at the end of the procedure
+are not extracted as local hypotheses.
+
+- `lift_lets` lifts let expressions in the target.
+- `lift_lets at h` lifts let expressions at the given local hypothesis.
+
+For example,
+```lean
+example : (let x := 1; x) = 1 := by
+  lift_lets
+  -- ⊢ let x := 1; x = 1
+  ...
+```
+-/
+syntax (name := liftLets) "lift_lets " optConfig (location)? : tactic
+
 /--
 If `thm` is a theorem `a = b`, then as a rewrite rule,
 * `thm` means to replace `a` with `b`, and

src/Lean/AddDecl.lean

@@ -52,7 +52,7 @@ def addDecl (decl : Declaration) : CoreM Unit := do
   modifyEnv (decl.getNames.foldl registerNamePrefixes)
 
   if !Elab.async.get (← getOptions) then
-    return (← doAdd)
+    return (← addSynchronously)
 
   -- convert `Declaration` to `ConstantInfo` to use as a preliminary value in the environment until
   -- kernel checking has finished; not all cases are supported yet
@@ -61,7 +61,7 @@ def addDecl (decl : Declaration) : CoreM Unit := do
     | .defnDecl defn => pure (defn.name, .defnInfo defn, .defn)
     | .mutualDefnDecl [defn] => pure (defn.name, .defnInfo defn, .defn)
     | .axiomDecl ax => pure (ax.name, .axiomInfo ax, .axiom)
-    | _ => return (← doAdd)
+    | _ => return (← addSynchronously)
 
   let env ← getEnv
   -- no environment extension changes to report after kernel checking; ensures we do not
@@ -81,6 +81,19 @@ def addDecl (decl : Declaration) : CoreM Unit := do
   let endRange? := (← getRef).getTailPos?.map fun pos => ⟨pos, pos⟩
   Core.logSnapshotTask { stx? := none, reportingRange? := endRange?, task := t, cancelTk? := cancelTk }
 where
+  addSynchronously := do
+    doAdd
+    -- make constants known to the elaborator; in the synchronous case, we can simply read them from
+    -- the kernel env
+    for n in decl.getNames do
+      let env ← getEnv
+      let some info := env.checked.get.find? n | unreachable!
+      -- do *not* report extensions in synchronous case at this point as they are usually set only
+      -- after adding the constant itself
+      let res ← env.addConstAsync (reportExts := false) n (.ofConstantInfo info)
+      res.commitConst env (info? := info)
+      res.commitCheckEnv res.asyncEnv
+      setEnv res.mainEnv
   doAdd := do
     profileitM Exception "type checking" (← getOptions) do
       withTraceNode `Kernel (fun _ => return m!"typechecking declarations {decl.getTopLevelNames}") do

src/Lean/Compiler/IR/ElimDeadBranches.lean

@@ -165,6 +165,7 @@ structure InterpContext where
 structure InterpState where
   assignments : Array Assignment
   funVals     : PArray Value -- we take snapshots during fixpoint computations
+  visitedJps  : Array (Std.HashSet JoinPointId)
 
 abbrev M := ReaderT InterpContext (StateM InterpState)
 
@@ -223,11 +224,18 @@ def updateCurrFnSummary (v : Value) : M Unit := do
   let currFnIdx := ctx.currFnIdx
   modify fun s => { s with funVals := s.funVals.modify currFnIdx (fun v' => widening ctx.env v v') }
 
+def markJPVisited (j : JoinPointId) : M Bool := do
+  let currFnIdx := (← read).currFnIdx
+  modifyGet fun s =>
+    ⟨!(s.visitedJps[currFnIdx]!.contains j),
+     { s with visitedJps := s.visitedJps.modify currFnIdx fun a => a.insert j }⟩
+
 /-- Return true if the assignment of at least one parameter has been updated. -/
-def updateJPParamsAssignment (ys : Array Param) (xs : Array Arg) : M Bool := do
+def updateJPParamsAssignment (j : JoinPointId) (ys : Array Param) (xs : Array Arg) : M Bool := do
   let ctx ← read
   let currFnIdx := ctx.currFnIdx
-  ys.size.foldM (init := false) fun i _ r => do
+  let isFirstVisit ← markJPVisited j
+  ys.size.foldM (init := isFirstVisit) fun i _ r => do
     let y := ys[i]
     let x := xs[i]!
     let yVal ← findVarValue y.x
@@ -272,7 +280,7 @@ partial def interpFnBody : FnBody → M Unit
     let ctx ← read
     let ys := (ctx.lctx.getJPParams j).get!
     let b  := (ctx.lctx.getJPBody j).get!
-    let updated ← updateJPParamsAssignment ys xs
+    let updated ← updateJPParamsAssignment j ys xs
     if updated then
       -- We must reset the value of nested join-point parameters since they depend on `ys` values
       resetNestedJPParams b
@@ -283,7 +291,8 @@ partial def interpFnBody : FnBody → M Unit
 
 def inferStep : M Bool := do
   let ctx ← read
-  modify fun s => { s with assignments := ctx.decls.map fun _ => {} }
+  modify fun s => { s with assignments := ctx.decls.map fun _ => {},
+                           visitedJps := ctx.decls.map fun _ => {} }
   ctx.decls.size.foldM (init := false) fun idx _ modified => do
     match ctx.decls[idx] with
     | .fdecl (xs := ys) (body := b) .. => do
@@ -295,7 +304,11 @@ def inferStep : M Bool := do
         let s ← get
         let newVals := s.funVals[idx]!
         pure (modified || currVals != newVals)
-    | .extern .. => pure modified
+    | .extern .. => do
+      let currVals := (← get).funVals[idx]!
+      updateCurrFnSummary .top
+      let newVals := (← get).funVals[idx]!
+      pure (modified || currVals != newVals)
 
 partial def inferMain : M Unit := do
   let modified ← inferStep
@@ -332,8 +345,9 @@ def elimDeadBranches (decls : Array Decl) : CompilerM (Array Decl) := do
   let env := s.env
   let assignments : Array Assignment := decls.map fun _ => {}
   let funVals := mkPArray decls.size Value.bot
+  let visitedJps := decls.map fun _ => {}
   let ctx : InterpContext := { decls := decls, env := env }
-  let s : InterpState := { assignments := assignments, funVals := funVals }
+  let s : InterpState := { assignments, funVals, visitedJps }
   let (_, s) := (inferMain ctx).run s
   let funVals := s.funVals
   let assignments := s.assignments

src/Lean/Compiler/IR/ExpandResetReuse.lean

@@ -49,11 +49,23 @@ partial def consumed (x : VarId) : FnBody → Bool
   | e => !e.isTerminal && consumed x e.body
 
 abbrev Mask := Array (Option VarId)
+abbrev ProjCounts := Std.HashMap (VarId × Nat) Nat
+
+partial def computeProjCounts (bs : Array FnBody) : ProjCounts :=
+  let incrementCountIfProj r b :=
+    if let .vdecl _ _ (.proj i v) _ := b then
+      r.alter (v, i) fun
+      | some n => some (n + 1)
+      | none => some 1
+    else
+      r
+  bs.foldl incrementCountIfProj Std.HashMap.emptyWithCapacity
 
 /-- Auxiliary function for eraseProjIncFor -/
-partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (keep : Array FnBody) : Array FnBody × Mask :=
+partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (projCounts : ProjCounts)
+    (mask : Mask) (keep : Array FnBody) : Array FnBody × Mask :=
   let done (_ : Unit)        := (bs ++ keep.reverse, mask)
-  let keepInstr (b : FnBody) := eraseProjIncForAux y bs.pop mask (keep.push b)
+  let keepInstr (b : FnBody) := eraseProjIncForAux y bs.pop projCounts mask (keep.push b)
   if h : bs.size < 2 then done ()
   else
     let b := bs.back!
@@ -65,7 +77,10 @@ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (ke
       let b' := bs[bs.size - 2]
       match b' with
       | .vdecl w _ (.proj i x) _ =>
-        if w == z && y == x then
+        -- We disable the inc optimization if there are multiple projections with the same base
+        -- and index, because the downstream transformations are incapable of correctly handling
+        -- the aliasing.
+        if w == z && y == x && projCounts[(x, i)]! == 1 then
           /- Found
              ```
              let z := proj[i] y
@@ -77,7 +92,7 @@ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (ke
           let mask := mask.set! i (some z)
           let keep := keep.push b'
           let keep := if n == 1 then keep else keep.push (FnBody.inc z (n-1) c p FnBody.nil)
-          eraseProjIncForAux y bs mask keep
+          eraseProjIncForAux y bs projCounts mask keep
         else done ()
       | _ => done ()
     | _ => done ()
@@ -85,7 +100,7 @@ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (ke
 /-- Try to erase `inc` instructions on projections of `y` occurring in the tail of `bs`.
    Return the updated `bs` and a bit mask specifying which `inc`s have been removed. -/
 def eraseProjIncFor (n : Nat) (y : VarId) (bs : Array FnBody) : Array FnBody × Mask :=
-  eraseProjIncForAux y bs (.replicate n none) #[]
+  eraseProjIncForAux y bs (computeProjCounts bs) (.replicate n none) #[]
 
 /-- Replace `reuse x ctor ...` with `ctor ...`, and remove `dec x` -/
 partial def reuseToCtor (x : VarId) : FnBody → FnBody

src/Lean/Compiler/IR/LLVMBindings.lean

@@ -63,6 +63,7 @@ structure Module (ctx : Context) where
   private mk :: ptr : USize
 instance : Nonempty (Module ctx) := ⟨{ ptr := default }⟩
 
+/-
 structure PassManager (ctx : Context) where
   private mk :: ptr : USize
 instance : Nonempty (PassManager ctx) := ⟨{ ptr := default }⟩
@@ -70,6 +71,7 @@ instance : Nonempty (PassManager ctx) := ⟨{ ptr := default }⟩
 structure PassManagerBuilder (ctx : Context) where
   private mk :: ptr : USize
 instance : Nonempty (PassManagerBuilder ctx) := ⟨{ ptr := default }⟩
+-/
 
 structure Target (ctx : Context) where
   private mk :: ptr : USize
@@ -313,6 +315,7 @@ opaque createTargetMachine (target : Target ctx) (tripleStr : @&String) (cpu : @
 @[extern "lean_llvm_target_machine_emit_to_file"]
 opaque targetMachineEmitToFile (targetMachine : TargetMachine ctx) (module : Module ctx) (filepath : @&String) (codegenType : LLVM.CodegenFileType) : BaseIO Unit
 
+/-
 @[extern "lean_llvm_create_pass_manager"]
 opaque createPassManager : BaseIO (PassManager ctx)
 
@@ -333,6 +336,7 @@ opaque PassManagerBuilder.setOptLevel (pmb : PassManagerBuilder ctx) (optLevel :
 
 @[extern "lean_llvm_pass_manager_builder_populate_module_pass_manager"]
 opaque PassManagerBuilder.populateModulePassManager (pmb : PassManagerBuilder ctx) (pm : PassManager ctx): BaseIO Unit
+-/
 
 @[extern "lean_llvm_dispose_target_machine"]
 opaque disposeTargetMachine (tm : TargetMachine ctx) : BaseIO Unit

src/Lean/Elab/Frontend.lean

@@ -132,6 +132,11 @@ def process (input : String) (env : Environment) (opts : Options) (fileName : Op
   let s ← IO.processCommands inputCtx { : Parser.ModuleParserState } (Command.mkState env {} opts)
   pure (s.commandState.env, s.commandState.messages)
 
+register_builtin_option experimental.module : Bool := {
+  defValue := false
+  descr := "Allow use of module system (experimental)"
+}
+
 @[export lean_run_frontend]
 def runFrontend
     (input : String)
@@ -151,7 +156,10 @@ def runFrontend
   let opts := Elab.async.setIfNotSet opts true
   let ctx := { inputCtx with }
   let processor := Language.Lean.process
-  let snap ← processor (fun _ => pure <| .ok { mainModuleName, opts, trustLevel, plugins }) none ctx
+  let snap ← processor (fun header => do
+    if !header.raw[0].isNone && !experimental.module.get opts then
+      throw <| IO.Error.userError "`module` keyword is experimental and not enabled here"
+    pure <| .ok { mainModuleName, opts, trustLevel, plugins }) none ctx
   let snaps := Language.toSnapshotTree snap
   let severityOverrides := errorOnKinds.foldl (·.insert · .error) {}
   let hasErrors ← snaps.runAndReport opts jsonOutput severityOverrides

src/Lean/Elab/Import.lean

@@ -10,19 +10,18 @@ import Lean.CoreM
 
 namespace Lean.Elab
 
-def headerToImports (header : Syntax) : Array Import :=
-  let imports := if header[0].isNone then #[{ module := `Init : Import }] else #[]
-  imports ++ header[1].getArgs.map fun stx =>
-    -- `stx` is of the form `(Module.import "import" "runtime"? id)
-    let runtime := !stx[1].isNone
-    let id      := stx[2].getId
-    { module := id, runtimeOnly := runtime }
+def headerToImports : TSyntax ``Parser.Module.header → Array Import
+  | `(Parser.Module.header| $[module%$moduleTk]? $[prelude%$preludeTk]? $[import $ns]*) =>
+    let imports := if preludeTk.isNone then #[{ module := `Init : Import }] else #[]
+    imports ++ ns.map ({ module := ·.getId })
+  | _ => unreachable!
 
-def processHeader (header : Syntax) (opts : Options) (messages : MessageLog)
+def processHeader (header : TSyntax ``Parser.Module.header) (opts : Options) (messages : MessageLog)
     (inputCtx : Parser.InputContext) (trustLevel : UInt32 := 0)
     (plugins : Array System.FilePath := #[]) (leakEnv := false)
     : IO (Environment × MessageLog) := do
-  let level := if experimental.module.get opts then
+  let isModule := !header.raw[0].isNone
+  let level := if isModule then
     if Elab.inServer.get opts then
       .server
     else
@@ -35,7 +34,7 @@ def processHeader (header : Syntax) (opts : Options) (messages : MessageLog)
     pure (env, messages)
   catch e =>
     let env ← mkEmptyEnvironment
-    let spos := header.getPos?.getD 0
+    let spos := header.raw.getPos?.getD 0
     let pos  := inputCtx.fileMap.toPosition spos
     pure (env, messages.add { fileName := inputCtx.fileName, data := toString e, pos := pos })
 

src/Lean/Elab/ParseImportsFast.lean

@@ -10,9 +10,10 @@ namespace Lean
 namespace ParseImports
 
 structure State where
-  imports : Array Import := #[]
-  pos     : String.Pos := 0
-  error?  : Option String := none
+  imports  : Array Import := #[]
+  pos      : String.Pos := 0
+  error?   : Option String := none
+  isModule : Bool := false
   deriving Inhabited
 
 def Parser := String → State → State
@@ -132,8 +133,8 @@ partial def whitespace : Parser := fun input s =>
   else
     false
 
-def State.pushModule (module : Name) (runtimeOnly : Bool) (s : State) : State :=
-  { s with imports := s.imports.push { module, runtimeOnly } }
+def State.pushModule (module : Name) (s : State) : State :=
+  { s with imports := s.imports.push { module } }
 
 @[inline] def isIdRestCold (c : Char) : Bool :=
   c = '_' || c = '\'' || c == '!' || c == '?' || isLetterLike c || isSubScriptAlnum c
@@ -141,7 +142,7 @@ def State.pushModule (module : Name) (runtimeOnly : Bool) (s : State) : State :=
 @[inline] def isIdRestFast (c : Char) : Bool :=
   c.isAlphanum || (c != '.' && c != '\n' && c != ' ' && isIdRestCold c)
 
-partial def moduleIdent (runtimeOnly : Bool) : Parser := fun input s =>
+partial def moduleIdent : Parser := fun input s =>
   let rec parse (module : Name) (s : State) :=
     let i := s.pos
     if h : input.atEnd i then
@@ -161,7 +162,7 @@ partial def moduleIdent (runtimeOnly : Bool) : Parser := fun input s =>
             let s := s.next input s.pos
             parse module s
           else
-            whitespace input (s.pushModule module runtimeOnly)
+            whitespace input (s.pushModule module)
       else if isIdFirst curr then
         let startPart := i
         let s         := takeWhile isIdRestFast input (s.next' input i h)
@@ -171,7 +172,7 @@ partial def moduleIdent (runtimeOnly : Bool) : Parser := fun input s =>
           let s := s.next input s.pos
           parse module s
         else
-          whitespace input (s.pushModule module runtimeOnly)
+          whitespace input (s.pushModule module)
       else
         s.mkError "expected identifier"
   parse .anonymous s
@@ -184,28 +185,31 @@ partial def moduleIdent (runtimeOnly : Bool) : Parser := fun input s =>
   | none => many p input s
   | some _ => { pos, error? := none, imports := s.imports.shrink size }
 
-@[inline] partial def preludeOpt (k : String) : Parser :=
-  keywordCore k (fun _ s => s.pushModule `Init false) (fun _ s => s)
-
 def main : Parser :=
-  preludeOpt "prelude" >>
-  many (keyword "import" >> keywordCore "runtime" (moduleIdent false) (moduleIdent true))
+  keywordCore "module" (fun _ s => { s with isModule := true }) (fun _ s => s) >>
+  keywordCore "prelude" (fun _ s => s.pushModule `Init) (fun _ s => s) >>
+  many (keyword "import" >> moduleIdent)
 
 end ParseImports
 
+deriving instance ToJson for Import
+
+structure ParseImportsResult where
+  imports  : Array Import
+  isModule : Bool
+  deriving ToJson
+
 /--
 Simpler and faster version of `parseImports`. We use it to implement Lake.
 -/
-def parseImports' (input : String) (fileName : String) : IO (Array Lean.Import) := do
+def parseImports' (input : String) (fileName : String) : IO ParseImportsResult := do
   let s := ParseImports.main input (ParseImports.whitespace input {})
   match s.error? with
-  | none => return s.imports
+  | none => return { s with }
   | some err => throw <| IO.userError s!"{fileName}: {err}"
 
-deriving instance ToJson for Import
-
 structure PrintImportResult where
-  imports? : Option (Array Import) := none
+  result?  : Option ParseImportsResult := none
   errors   : Array String := #[]
   deriving ToJson
 
@@ -217,8 +221,8 @@ structure PrintImportsResult where
 def printImportsJson (fileNames : Array String) : IO Unit := do
   let rs ← fileNames.mapM fun fn => do
     try
-      let deps ← parseImports' (← IO.FS.readFile ⟨fn⟩) fn
-      return { imports? := some deps }
+      let res ← parseImports' (← IO.FS.readFile ⟨fn⟩) fn
+      return { result? := some res }
     catch e => return { errors := #[e.toString] }
   IO.println (toJson { imports := rs : PrintImportsResult } |>.compress)
 

src/Lean/Elab/Tactic.lean

@@ -50,3 +50,4 @@ import Lean.Elab.Tactic.AsAuxLemma
 import Lean.Elab.Tactic.TreeTacAttr
 import Lean.Elab.Tactic.ExposeNames
 import Lean.Elab.Tactic.SimpArith
+import Lean.Elab.Tactic.Lets

src/Lean/Elab/Tactic/Conv.lean

@@ -8,6 +8,7 @@ import Lean.Elab.Tactic.Conv.Basic
 import Lean.Elab.Tactic.Conv.Congr
 import Lean.Elab.Tactic.Conv.Rewrite
 import Lean.Elab.Tactic.Conv.Change
+import Lean.Elab.Tactic.Conv.Lets
 import Lean.Elab.Tactic.Conv.Simp
 import Lean.Elab.Tactic.Conv.Pattern
 import Lean.Elab.Tactic.Conv.Delta

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

@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+prelude
+import Lean.Elab.Tactic.Lets
+import Lean.Elab.Tactic.Conv.Basic
+
+/-!
+# Conv tactics to manipulate `let` expressions
+-/
+
+open Lean Meta
+
+namespace Lean.Elab.Tactic.Conv
+
+/-!
+### `extract_lets`
+-/
+
+@[builtin_tactic Lean.Parser.Tactic.Conv.extractLets] elab_rules : tactic
+  | `(conv| extract_lets $cfg:optConfig $ids*) => do
+    let mut config ← elabExtractLetsConfig cfg
+    let givenNames := (ids.map getNameOfIdent').toList
+    let (lhs, rhs) ← getLhsRhs
+    let fvars ← liftMetaTacticAux fun mvarId => do
+      mvarId.checkNotAssigned `extract_lets
+      Meta.extractLets #[lhs] givenNames (config := config) fun fvarIds es _ => do
+        let lhs' := es[0]!
+        if fvarIds.isEmpty && lhs == lhs' then
+          throwTacticEx `extract_lets mvarId m!"made no progress"
+        let (rhs', g) ← mkConvGoalFor lhs' (← mvarId.getTag)
+        let fvars := fvarIds.map .fvar
+        let assign (mvar : MVarId) (e : Expr) : MetaM Unit := do
+          let e ← mkLetFVars (usedLetOnly := false) fvars e
+          mvar.withContext do
+            unless ← isDefEq (.mvar mvar) e do
+              throwTacticEx `extract_lets mvarId m!"(internal error) non-defeq in assignment"
+            mvar.assign e
+        assign rhs'.mvarId! rhs
+        assign mvarId g
+        return (fvarIds, [g.mvarId!])
+    extractLetsAddVarInfo ids fvars
+
+/-!
+### `lift_lets`
+-/
+
+@[builtin_tactic Lean.Parser.Tactic.Conv.liftLets] elab_rules : tactic
+  | `(conv| lift_lets $cfg:optConfig) => do
+    let mut config ← elabLiftLetsConfig cfg
+    withMainContext do
+      let lhs ← getLhs
+      let lhs' ← Meta.liftLets lhs config
+      if lhs == lhs' then
+        throwTacticEx `lift_lets (← getMainGoal) m!"made no progress"
+      changeLhs lhs'
+
+end Lean.Elab.Tactic.Conv

src/Lean/Elab/Tactic/Lets.lean

@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+prelude
+import Lean.Meta.Tactic.Lets
+import Lean.Elab.Tactic.Location
+
+/-!
+# Tactics to manipulate `let` expressions
+-/
+
+open Lean Meta
+
+namespace Lean.Elab.Tactic
+
+register_builtin_option linter.tactic.unusedName : Bool := {
+  defValue := true,
+  descr := "enable the 'unused name' tactic linter"
+}
+
+/-!
+### `extract_lets`
+-/
+
+def extractLetsAddVarInfo (ids : Array Syntax) (fvars : Array FVarId) : TacticM Unit :=
+  withMainContext do
+    for h : i in [0:ids.size] do
+      if h' : i < fvars.size then
+        Term.addLocalVarInfo ids[i] (mkFVar fvars[i])
+      else
+        Linter.logLintIf linter.tactic.unusedName ids[i] m!"unused name"
+
+declare_config_elab elabExtractLetsConfig ExtractLetsConfig
+
+@[builtin_tactic extractLets] elab_rules : tactic
+  | `(tactic| extract_lets $cfg:optConfig $ids* $[$loc?:location]?) => do
+    let mut config ← elabExtractLetsConfig cfg
+    let givenNames := (ids.map getNameOfIdent').toList
+    withLocation (expandOptLocation (Lean.mkOptionalNode loc?))
+      (atLocal := fun h => do
+        let fvars ← liftMetaTacticAux fun mvarId => do
+          let ((fvars, _), mvarId) ← mvarId.extractLetsLocalDecl h givenNames config
+          return (fvars, [mvarId])
+        extractLetsAddVarInfo ids fvars)
+      (atTarget := do
+        let fvars ← liftMetaTacticAux fun mvarId => do
+          let ((fvars, _), mvarId) ← mvarId.extractLets givenNames config
+          return (fvars, [mvarId])
+        extractLetsAddVarInfo ids fvars)
+      (failed := fun _ => throwError "'extract_lets' tactic failed")
+
+/-!
+### `lift_lets`
+-/
+
+declare_config_elab elabLiftLetsConfig LiftLetsConfig
+
+@[builtin_tactic liftLets] elab_rules : tactic
+  | `(tactic| lift_lets $cfg:optConfig $[$loc?:location]?) => do
+    let mut config ← elabLiftLetsConfig cfg
+    withLocation (expandOptLocation (Lean.mkOptionalNode loc?))
+      (atLocal := fun h => liftMetaTactic1 fun mvarId => mvarId.liftLetsLocalDecl h config)
+      (atTarget := liftMetaTactic1 fun mvarId => mvarId.liftLets config)
+      (failed := fun _ => throwError "'lift_lets' tactic failed")
+
+end Lean.Elab.Tactic

src/Lean/Environment.lean

@@ -95,12 +95,11 @@ abbrev ConstMap := SMap Name ConstantInfo
 
 structure Import where
   module      : Name
-  runtimeOnly : Bool := false
   deriving Repr, Inhabited
 
 instance : Coe Name Import := ⟨({module := ·})⟩
 
-instance : ToString Import := ⟨fun imp => toString imp.module ++ if imp.runtimeOnly then " (runtime)" else ""⟩
+instance : ToString Import := ⟨fun imp => toString imp.module⟩
 
 /--
   A compacted region holds multiple Lean objects in a contiguous memory region, which can be read/written to/from disk.
@@ -123,6 +122,8 @@ instance : Nonempty EnvExtensionEntry := EnvExtensionEntrySpec.property
 /-- Content of a .olean file.
    We use `compact.cpp` to generate the image of this object in disk. -/
 structure ModuleData where
+  /-- Participating in the module system? -/
+  isModule        : Bool
   imports         : Array Import
   /--
   `constNames` contains all constant names in `constants`.
@@ -152,6 +153,8 @@ structure EnvironmentHeader where
   Name of the module being compiled.
   -/
   mainModule   : Name         := default
+  /-- Participating in the module system? -/
+  isModule     : Bool         := false
   /-- Direct imports -/
   imports      : Array Import := #[]
   /-- Compacted regions for all imported modules. Objects in compacted memory regions do no require any memory management. -/
@@ -518,9 +521,9 @@ structure Environment where
   -/
   checked             : Task Kernel.Environment := .pure base
   /--
-  Container of asynchronously elaborated declarations. For consistency, `updateBaseAfterKernelAdd`
-  makes sure this contains constants added even synchronously, i.e. `base ⨃ asyncConsts` is the set
-  of constants known on the current environment branch, which is a subset of `checked`.
+  Container of asynchronously elaborated declarations. For consistency, `Lean.addDecl` makes sure
+  this contains constants added even synchronously, i.e. `base ⨃ asyncConsts` is the set of
+  constants known on the current environment branch, which is a subset of `checked`.
   -/
   private asyncConsts : AsyncConsts := default
   /-- Information about this asynchronous branch of the environment, if any. -/
@@ -1581,17 +1584,11 @@ def mkModuleData (env : Environment) (level : OLeanLevel := .private) : IO Modul
   -- TODO: does not include cstage* constants from the old codegen
   --let constants := constNames.filterMap env.find?
   let constNames := constants.map (·.name)
-  return {
-    imports         := env.header.imports
+  return { env.header with
     extraConstNames := env.checked.get.extraConstNames.toArray
     constNames, constants, entries
   }
 
-register_builtin_option experimental.module : Bool := {
-  defValue := false
-  descr := "Enable module system (experimental)"
-}
-
 @[export lean_write_module]
 def writeModule (env : Environment) (fname : System.FilePath) (split := false) : IO Unit := do
   if split then
@@ -1699,7 +1696,7 @@ abbrev ImportStateM := StateRefT ImportState IO
 partial def importModulesCore (imports : Array Import) (level := OLeanLevel.private) :
     ImportStateM Unit := do
   for i in imports do
-    if i.runtimeOnly || (← get).moduleNameSet.contains i.module then
+    if (← get).moduleNameSet.contains i.module then
       continue
     modify fun s => { s with moduleNameSet := s.moduleNameSet.insert i.module }
     let mFile ← findOLean i.module
@@ -1756,7 +1753,7 @@ Constructs environment from `importModulesCore` results.
 See also `importModules` for parameter documentation.
 -/
 def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (trustLevel : UInt32 := 0)
-    (leakEnv loadExts : Bool) : IO Environment := do
+    (leakEnv loadExts : Bool) (isModule := false) : IO Environment := do
   let numConsts := s.moduleData.foldl (init := 0) fun numConsts mod =>
     numConsts + mod.constants.size + mod.extraConstNames.size
   let mut const2ModIdx : Std.HashMap Name ModuleIdx := Std.HashMap.emptyWithCapacity (capacity := numConsts)
@@ -1783,7 +1780,7 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
       extraConstNames := {}
       extensions      := exts
       header     := {
-        trustLevel, imports
+        trustLevel, isModule, imports
         regions      := s.parts.flatMap (·.map (·.2))
         moduleNames  := s.moduleNames
         moduleData   := s.moduleData
@@ -1847,7 +1844,8 @@ def importModules (imports : Array Import) (opts : Options) (trustLevel : UInt32
   withImporting do
     plugins.forM Lean.loadPlugin
     let (_, s) ← importModulesCore (level := level) imports |>.run
-    finalizeImport (leakEnv := leakEnv) (loadExts := loadExts) s imports opts trustLevel
+    finalizeImport (leakEnv := leakEnv) (loadExts := loadExts) (isModule := !level matches .private)
+      s imports opts trustLevel
 
 /--
 Creates environment object from imports and frees compacted regions after calling `act`. No live
@@ -1878,13 +1876,18 @@ def Kernel.setDiagnostics (env : Lean.Environment) (diag : Diagnostics) : Lean.E
 
 namespace Environment
 
+private def looksLikeOldCodegenName : Name → Bool
+  | .str _ s => s.startsWith "_cstage" || s.startsWith "_spec_"
+  | _        => false
+
 @[export lean_elab_environment_update_base_after_kernel_add]
 private def updateBaseAfterKernelAdd (env : Environment) (kenv : Kernel.Environment) (decl : Declaration) : Environment :=
   { env with
     checked := .pure kenv
-    -- make constants available in `asyncConsts` as well; see its docstring
+    -- HACK: the old codegen adds some helper constants directly to the kernel environment, we need
+    -- to add them to the async consts as well in order to be able to replay them
     asyncConsts := decl.getNames.foldl (init := env.asyncConsts) fun asyncConsts n =>
-      if asyncConsts.find? n |>.isNone then
+      if looksLikeOldCodegenName n then
         asyncConsts.add {
           constInfo := .ofConstantInfo (kenv.find? n |>.get!)
           exts? := none

src/Lean/Language/Lean.lean

@@ -361,7 +361,7 @@ General notes:
   the `sync` parameter on `parseCmd` and spawn an elaboration task when we leave it.
 -/
 partial def process
-    (setupImports : Syntax → ProcessingT IO (Except HeaderProcessedSnapshot SetupImportsResult))
+    (setupImports : TSyntax ``Parser.Module.header → ProcessingT IO (Except HeaderProcessedSnapshot SetupImportsResult))
     (old? : Option InitialSnapshot) : ProcessingM InitialSnapshot := do
   parseHeader old? |>.run (old?.map (·.ictx))
 where
@@ -423,7 +423,7 @@ where
           result? := none
         }
 
-      let trimmedStx := stx.unsetTrailing
+      let trimmedStx := stx.raw.unsetTrailing
       -- semi-fast path: go to next snapshot if syntax tree is unchanged
       -- NOTE: We compare modulo `unsetTrailing` in order to ensure that changes in trailing
       -- whitespace do not invalidate the header. This is safe because we only pass the trimmed
@@ -443,11 +443,11 @@ where
         diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog)
         result? := some {
           parserState
-          processedSnap := (← processHeader trimmedStx parserState)
+          processedSnap := (← processHeader ⟨trimmedStx⟩ parserState)
         }
       }
 
-  processHeader (stx : Syntax) (parserState : Parser.ModuleParserState) :
+  processHeader (stx : TSyntax ``Parser.Module.header) (parserState : Parser.ModuleParserState) :
       LeanProcessingM (SnapshotTask HeaderProcessedSnapshot) := do
     let ctx ← read
     SnapshotTask.ofIO stx none (some ⟨0, ctx.input.endPos⟩) <|
@@ -489,7 +489,7 @@ where
             ngen    := { namePrefix := `_import }
           }) (Elab.InfoTree.node
               (Elab.Info.ofCommandInfo { elaborator := `header, stx })
-              (stx[1].getArgs.toList.map (fun importStx =>
+              (stx.raw[2].getArgs.toList.map (fun importStx =>
                 Elab.InfoTree.node (Elab.Info.ofCommandInfo {
                   elaborator := `import
                   stx := importStx

src/Lean/Meta/AppBuilder.lean

@@ -27,13 +27,17 @@ def mkExpectedTypeHint (e : Expr) (expectedType : Expr) : MetaM Expr := do
 /--
 `mkLetFun x v e` creates the encoding for the `let_fun x := v; e` expression.
 The expression `x` can either be a free variable or a metavariable, and the function suitably abstracts `x` in `e`.
-NB: `x` must not be a let-bound free variable.
 -/
 def mkLetFun (x : Expr) (v : Expr) (e : Expr) : MetaM Expr := do
-  let f ← mkLambdaFVars #[x] e
+  -- If `x` is an `ldecl`, then the result of `mkLambdaFVars` is a let expression.
+  let ensureLambda : Expr → Expr
+    | .letE n t _ b _ => .lam n t b .default
+    | e@(.lam ..)     => e
+    | _               => unreachable!
+  let f ← ensureLambda <$> mkLambdaFVars (usedLetOnly := false) #[x] e
   let ety ← inferType e
   let α ← inferType x
-  let β ← mkLambdaFVars #[x] ety
+  let β ← ensureLambda <$> mkLambdaFVars (usedLetOnly := false) #[x] ety
   let u1 ← getLevel α
   let u2 ← getLevel ety
   return mkAppN (.const ``letFun [u1, u2]) #[α, β, v, f]
@@ -304,7 +308,7 @@ private partial def mkAppMArgs (f : Expr) (fType : Expr) (xs : Array Expr) : Met
         | _ =>
           let x := xs[i]
           let xType ← inferType x
-          if (← isDefEq d xType) then
+          if (← withAtLeastTransparency .default (isDefEq d xType)) then
             loop b (i+1) j (args.push x) instMVars
           else
             throwAppTypeMismatch (mkAppN f args) x

src/Lean/Meta/Basic.lean

@@ -604,6 +604,9 @@ export Core (instantiateTypeLevelParams instantiateValueLevelParams)
 @[inline] def map2MetaM [MonadControlT MetaM m] [Monad m] (f : forall {α}, (β → γ → MetaM α) → MetaM α) {α} (k : β → γ → m α) : m α :=
   controlAt MetaM fun runInBase => f fun b c => runInBase <| k b c
 
+@[inline] def map3MetaM [MonadControlT MetaM m] [Monad m] (f : forall {α}, (β → γ → δ → MetaM α) → MetaM α) {α} (k : β → γ → δ → m α) : m α :=
+  controlAt MetaM fun runInBase => f fun b c d => runInBase <| k b c d
+
 section Methods
 variable [MonadControlT MetaM n] [Monad n]
 
@@ -1926,6 +1929,76 @@ private partial def instantiateLambdaAux (ps : Array Expr) (i : Nat) (e : Expr)
 def instantiateLambda (e : Expr) (ps : Array Expr) : MetaM Expr :=
   instantiateLambdaAux ps 0 e
 
+/--
+A simpler version of `ParamInfo` for information about the parameter of a forall or lambda.
+-/
+structure ExprParamInfo where
+  /-- The name of the parameter. -/
+  name : Name
+  /-- The type of the parameter. -/
+  type : Expr
+  /-- The binder annotation for the parameter. -/
+  binderInfo : BinderInfo := BinderInfo.default
+  deriving Inhabited
+
+/--
+Given `e` of the form `∀ (p₁ : P₁) … (p₁ : P₁), B[p_1,…,p_n]` and `arg₁ : P₁, …, argₙ : Pₙ`, returns
+* the names `p₁, …, pₙ`,
+* the binder infos,
+* the binder types `P₁, P₂[arg₁], …, P[arg₁,…,argₙ₋₁]`, and
+* the type `B[arg₁,…,argₙ]`.
+
+It uses `whnf` to reduce `e` if it is not a forall.
+
+See also `Lean.Meta.instantiateForall`.
+-/
+def instantiateForallWithParamInfos (e : Expr) (args : Array Expr) (cleanupAnnotations : Bool := false) :
+    MetaM (Array ExprParamInfo × Expr) := do
+  let mut e := e
+  let mut res := Array.mkEmpty args.size
+  let mut j := 0
+  for i in [0:args.size] do
+    unless e.isForall do
+      e ← whnf (e.instantiateRevRange j i args)
+      j := i
+    match e with
+    | .forallE name type e' binderInfo =>
+      let type := type.instantiateRevRange j i args
+      let type := if cleanupAnnotations then type.cleanupAnnotations else type
+      res := res.push { name, type, binderInfo }
+      e := e'
+    | _ => throwError "invalid `instantiateForallWithParams`, too many parameters{indentExpr e}"
+  return (res, e)
+
+/--
+Given `e` of the form `fun (p₁ : P₁) … (p₁ : P₁) => t[p_1,…,p_n]` and `arg₁ : P₁, …, argₙ : Pₙ`, returns
+* the names `p₁, …, pₙ`,
+* the binder infos,
+* the binder types `P₁, P₂[arg₁], …, P[arg₁,…,argₙ₋₁]`, and
+* the term `t[arg₁,…,argₙ]`.
+
+It uses `whnf` to reduce `e` if it is not a lambda.
+
+See also `Lean.Meta.instantiateLambda`.
+-/
+def instantiateLambdaWithParamInfos (e : Expr) (args : Array Expr) (cleanupAnnotations : Bool := false) :
+    MetaM (Array ExprParamInfo × Expr) := do
+  let mut e := e
+  let mut res := Array.mkEmpty args.size
+  let mut j := 0
+  for i in [0:args.size] do
+    unless e.isLambda do
+      e ← whnf (e.instantiateRevRange j i args)
+      j := i
+    match e with
+    | .forallE name type e' binderInfo =>
+      let type := type.instantiateRevRange j i args
+      let type := if cleanupAnnotations then type.cleanupAnnotations else type
+      res := res.push { name, type, binderInfo }
+      e := e'
+    | _ => throwError "invalid `instantiateForallWithParams`, too many parameters{indentExpr e}"
+  return (res, e)
+
 /-- Pretty-print the given expression. -/
 def ppExprWithInfos (e : Expr) : MetaM FormatWithInfos := do
   let ctxCore  ← readThe Core.Context

src/Lean/Meta/Tactic.lean

@@ -14,6 +14,7 @@ import Lean.Meta.Tactic.Assert
 import Lean.Meta.Tactic.Rewrite
 import Lean.Meta.Tactic.Generalize
 import Lean.Meta.Tactic.Replace
+import Lean.Meta.Tactic.Lets
 import Lean.Meta.Tactic.Induction
 import Lean.Meta.Tactic.Cases
 import Lean.Meta.Tactic.ElimInfo

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

@@ -9,3 +9,4 @@ import Lean.Meta.Tactic.Grind.Arith.Types
 import Lean.Meta.Tactic.Grind.Arith.Main
 import Lean.Meta.Tactic.Grind.Arith.Offset
 import Lean.Meta.Tactic.Grind.Arith.Cutsat
+import Lean.Meta.Tactic.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing.lean

@@ -0,0 +1,31 @@
+/-
+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.Util.Trace
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
+import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Internalize
+import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Var
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
+import Lean.Meta.Tactic.Grind.Arith.CommRing.EqCnstr
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
+import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
+
+namespace Lean
+
+builtin_initialize registerTraceClass `grind.ring
+builtin_initialize registerTraceClass `grind.ring.internalize
+builtin_initialize registerTraceClass `grind.ring.assert
+builtin_initialize registerTraceClass `grind.ring.assert.unsat (inherited := true)
+builtin_initialize registerTraceClass `grind.ring.assert.trivial (inherited := true)
+builtin_initialize registerTraceClass `grind.ring.assert.store (inherited := true)
+builtin_initialize registerTraceClass `grind.ring.assert.discard (inherited := true)
+builtin_initialize registerTraceClass `grind.ring.simp
+
+
+end Lean

src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.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.Arith.CommRing.Util
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Var
+
+namespace Lean.Meta.Grind.Arith.CommRing
+/-!
+Helper functions for converting reified terms back into their denotations.
+-/
+
+private def denoteNum (k : Int) : RingM Expr := do
+  let ring ← getRing
+  let n := mkRawNatLit k.natAbs
+  let ofNatInst := mkApp3 (mkConst ``Grind.CommRing.ofNat [ring.u]) ring.type ring.commRingInst n
+  let n := mkApp3 (mkConst ``OfNat.ofNat [ring.u]) ring.type n ofNatInst
+  if k < 0 then
+    return mkApp ring.negFn n
+  else
+    return n
+
+def _root_.Lean.Grind.CommRing.Power.denoteExpr (pw : Power) : RingM Expr := do
+  let x := (← getRing).vars[pw.x]!
+  if pw.k == 1 then
+    return x
+  else
+    return mkApp2 (← getRing).powFn x (toExpr pw.k)
+
+def _root_.Lean.Grind.CommRing.Mon.denoteExpr (m : Mon) : RingM Expr := do
+  match m with
+  | .unit => denoteNum 1
+  | .mult pw m => go m (← pw.denoteExpr)
+where
+  go (m : Mon) (acc : Expr) : RingM Expr := do
+    match m with
+    | .unit => return acc
+    | .mult pw m => go m (mkApp2 (← getRing).mulFn acc (← pw.denoteExpr))
+
+def _root_.Lean.Grind.CommRing.Poly.denoteExpr (p : Poly) : RingM Expr := do
+  match p with
+  | .num k => denoteNum k
+  | .add k m p => go p (← denoteTerm k m)
+where
+  denoteTerm (k : Int) (m : Mon) : RingM Expr := do
+    if k == 1 then
+      m.denoteExpr
+    else
+      return mkApp2 (← getRing).mulFn (← denoteNum k) (← m.denoteExpr)
+
+  go (p : Poly) (acc : Expr) : RingM Expr := do
+    match p with
+    | .num 0 => return acc
+    | .num k => return mkApp2 (← getRing).addFn acc (← denoteNum k)
+    | .add k m p => go p (mkApp2 (← getRing).addFn acc (← denoteTerm k m))
+
+def _root_.Lean.Grind.CommRing.Expr.denoteExpr (e : RingExpr) : RingM Expr := do
+  go e
+where
+  go : RingExpr → RingM Expr
+  | .num k => denoteNum k
+  | .var x => return (← getRing).vars[x]!
+  | .add a b => return mkApp2 (← getRing).addFn (← go a) (← go b)
+  | .sub a b => return mkApp2 (← getRing).subFn (← go a) (← go b)
+  | .mul a b => return mkApp2 (← getRing).mulFn (← go a) (← go b)
+  | .pow a k => return mkApp2 (← getRing).powFn (← go a) (toExpr k)
+  | .neg a => return mkApp (← getRing).negFn (← go a)
+
+end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean

@@ -0,0 +1,125 @@
+/-
+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.Arith.CommRing.RingId
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
+import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
+
+namespace Lean.Meta.Grind.Arith.CommRing
+/-- Returns `some ringId` if `a` and `b` are elements of the same ring. -/
+private def inSameRing? (a b : Expr) : GoalM (Option Nat) := do
+  let some ringId ← getTermRingId? a | return none
+  let some ringId' ← getTermRingId? b | return none
+  unless ringId == ringId' do return none -- This can happen when we have heterogeneous equalities
+  return ringId
+
+def mkEqCnstr (p : Poly) (h : EqCnstrProof) : RingM EqCnstr := do
+  let id := (← getRing).nextId
+  let sugar := p.degree
+  modifyRing fun s => { s with nextId := s.nextId + 1 }
+  return { sugar, p, h, id }
+
+/--
+Returns the ring expression denoting the given Lean expression.
+Recall that we compute the ring expressions during internalization.
+-/
+private def toRingExpr? (e : Expr) : RingM (Option RingExpr) := do
+  let ring ← getRing
+  if let some re := ring.denote.find? { expr := e } then
+    return some re
+  else if let some x := ring.varMap.find? { expr := e } then
+    return some (.var x)
+  else
+    reportIssue! "failed to convert to ring expression{indentExpr e}"
+    return none
+
+/--
+Returns `some c`, where `c` is an equation from the basis whose leading monomial divides `m`.
+If `unitOnly` is true, only equations with a unit leading coefficient are considered.
+-/
+def _root_.Lean.Grind.CommRing.Mon.findSimp? (m : Mon) (unitOnly : Bool := false) : RingM (Option EqCnstr) :=
+  go m
+where
+  go : Mon → RingM (Option EqCnstr)
+    | .unit => return none
+    | .mult pw m' => do
+      for c in (← getRing).varToBasis[pw.x]! do
+        if !unitOnly || c.p.lc.natAbs == 1 then
+        if c.p.divides m then
+          return some c
+      go m'
+
+/--
+Returns `some c`, where `c` is an equation from the basis whose leading monomial divides some
+monomial in `p`.
+If `unitOnly` is true, only equations with a unit leading coefficient are considered.
+-/
+def _root_.Lean.Grind.CommRing.Poly.findSimp? (p : Poly) (unitOnly : Bool := false) : RingM (Option EqCnstr) := do
+  match p with
+  | .num _ => return none
+  | .add _ m p =>
+    match (← m.findSimp? unitOnly) with
+    | some c => return some c
+    | none => p.findSimp? unitOnly
+
+/-- Simplify the given equation constraint using the current basis. -/
+def simplify (c : EqCnstr) : RingM EqCnstr := do
+  let mut c := c
+  repeat
+    checkSystem "ring"
+    let some c' ← c.p.findSimp? | return c
+    let some r := c'.p.simp? c.p | unreachable!
+    c := { c with
+      p := r.p
+      h := .simp c' c r.k₁ r.k₂ r.m
+    }
+    trace_goal[grind.ring.simp] "{← c.p.denoteExpr}"
+  return c
+
+@[export lean_process_ring_eq]
+def processNewEqImpl (a b : Expr) : GoalM Unit := do
+  if isSameExpr a b then return () -- TODO: check why this is needed
+  let some ringId ← inSameRing? a b | return ()
+  RingM.run ringId do
+    trace_goal[grind.ring.assert] "{← mkEq a b}"
+    let some ra ← toRingExpr? a | return ()
+    let some rb ← toRingExpr? b | return ()
+    let p ← (ra.sub rb).toPolyM
+    if let .num k := p then
+      if k == 0 then
+        trace_goal[grind.ring.assert.trivial] "{← p.denoteExpr} = 0"
+      else if (← hasChar) then
+        trace_goal[grind.ring.assert.unsat] "{← p.denoteExpr} = 0"
+        setEqUnsat k a b ra rb
+      else
+        -- Remark: we currently don't do anything if the characteristic is not known.
+        trace_goal[grind.ring.assert.discard] "{← p.denoteExpr} = 0"
+      return ()
+
+    trace_goal[grind.ring.assert.store] "{← p.denoteExpr} = 0"
+  -- TODO: save equality
+
+@[export lean_process_ring_diseq]
+def processNewDiseqImpl (a b : Expr) : GoalM Unit := do
+  let some ringId ← inSameRing? a b | return ()
+  RingM.run ringId do
+    trace_goal[grind.ring.assert] "{mkNot (← mkEq a b)}"
+    let some ra ← toRingExpr? a | return ()
+    let some rb ← toRingExpr? b | return ()
+    let p ← (ra.sub rb).toPolyM
+    if let .num k := p then
+      if k == 0 then
+        trace_goal[grind.ring.assert.unsat] "{← p.denoteExpr} ≠ 0"
+        setNeUnsat a b ra rb
+      else
+        -- Remark: if the characteristic is known, it is trivial.
+        -- Otherwise, we don't do anything.
+        trace_goal[grind.ring.assert.trivial] "{← p.denoteExpr} ≠ 0"
+      return ()
+    trace_goal[grind.ring.assert.store] "{← p.denoteExpr} ≠ 0"
+    -- TODO: save disequalitys
+
+end Lean.Meta.Grind.Arith.CommRing

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

@@ -0,0 +1,46 @@
+/-
+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.Simp
+import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
+
+namespace Lean.Meta.Grind.Arith.CommRing
+
+/-- If `e` is a function application supported by the `CommRing` module, return its type. -/
+private def getType? (e : Expr) : Option Expr :=
+  match_expr e with
+  | HAdd.hAdd α _ _ _ _ _ => some α
+  | HSub.hSub α _ _ _ _ _ => some α
+  | HMul.hMul α _ _ _ _ _ => some α
+  | HPow.hPow α β _ _ _ _ =>
+    let_expr Nat := β | none
+    some α
+  | Neg.neg α _ _ => some α
+  | OfNat.ofNat α _ _ => some α
+  | NatCast.natCast α _ _ => some α
+  | IntCast.intCast α _ _ => some α
+  | _ => none
+
+private def isForbiddenParent (parent? : Option Expr) : Bool :=
+  if let some parent := parent? then
+    getType? parent |>.isSome
+  else
+    false
+
+def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
+  unless (← getConfig).ring do return ()
+  let some type := getType? e | return ()
+  if isForbiddenParent parent? then return ()
+  let some ringId ← getRingId? type | return ()
+  RingM.run ringId do
+    let some re ← reify? e | return ()
+    trace_goal[grind.ring.internalize] "[{ringId}]: {e}"
+    setTermRingId e
+    markAsCommRingTerm e
+    modifyRing fun s => { s with denote := s.denote.insert { expr := e } re }
+
+end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean

@@ -0,0 +1,166 @@
+/-
+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.Grind.CommRing.Poly
+namespace Lean.Grind.CommRing
+
+/-- `lcm m₁ m₂` returns the least common multiple of the given monomials. -/
+def Mon.lcm : Mon → Mon → Mon
+  | .unit, m₂ => m₂
+  | m₁, .unit => m₁
+  | .mult pw₁ m₁, .mult pw₂ m₂ =>
+    match compare pw₁.x pw₂.x with
+    | .eq => .mult { x := pw₁.x, k := max pw₁.k pw₂.k } (lcm m₁ m₂)
+    | .lt => .mult pw₁ (lcm m₁ (.mult pw₂ m₂))
+    | .gt => .mult pw₂ (lcm (.mult pw₁ m₁) m₂)
+
+/--
+`divides m₁ m₂` returns `true` if monomial `m₁` divides `m₂`
+Example: `x^2.z` divides `w.x^3.y^2.z`
+-/
+def Mon.divides : Mon → Mon → Bool
+  | .unit, _ => true
+  | _, .unit => false
+  | .mult pw₁ m₁, .mult pw₂ m₂ =>
+    match compare pw₁.x pw₂.x with
+    | .eq => pw₁.k ≤ pw₂.k && divides m₁ m₂
+    | .lt => false
+    | .gt => divides (.mult pw₁ m₁) m₂
+
+/--
+Given `m₁` and `m₂` such that `m₂.divides m₁`, then
+`m₁.div m₂` returns the result.
+Example `w.x^3.y^2.z` div `x^2.z` returns `w.x.y^2`
+-/
+def Mon.div : Mon → Mon → Mon
+  | m₁, .unit => m₁
+  | .unit, _  => .unit -- reachable only if pre-condition does not hold
+  | .mult pw₁ m₁, .mult pw₂ m₂ =>
+    match compare pw₁.x pw₂.x with
+    | .eq =>
+      let k := pw₁.k - pw₂.k
+      if k == 0 then
+        div m₁ m₂
+      else
+        .mult { x := pw₁.x, k } (div m₁ m₂)
+    | .lt => .mult pw₁ (div m₁ (.mult pw₂ m₂))
+    | .gt => .unit -- reachable only if pre-condition does not hold
+
+/--
+`coprime m₁ m₂` returns `true` if the given monomials
+do not have any variable in common.
+-/
+def Mon.coprime : Mon → Mon → Bool
+  | .unit, _ => true
+  | _, .unit => true
+  | .mult pw₁ m₁, .mult pw₂ m₂ =>
+    match compare pw₁.x pw₂.x with
+    | .eq => false
+    | .lt => coprime m₁ (.mult pw₂ m₂)
+    | .gt => coprime (.mult pw₁ m₁) m₂
+
+/--
+Contains the S-polynomial resulting from superposing two polynomials `p₁` and `p₂`,
+along with coefficients and monomials used in their construction.
+-/
+structure SPolResult where
+  /-- The computed S-polynomial. -/
+  spol : Poly := .num 0
+  /-- Coefficient applied to polynomial `p₁`. -/
+  c₁   : Int  := 0
+  /-- Monomial factor applied to polynomial `p₁`. -/
+  m₁   : Mon  := .unit
+  /-- Coefficient applied to polynomial `p₂`. -/
+  c₂   : Int  := 0
+  /-- Monomial factor applied to polynomial `p₂`. -/
+  m₂   : Mon  := .unit
+
+/--
+Returns the S-polynomial of polynomials `p₁` and `p₂`, and coefficients&terms used to construct it.
+Given polynomials with leading terms `k₁*m₁` and `k₂*m₂`, the S-polynomial is defined as:
+```
+S(p₁, p₂) = (k₂/gcd(k₁, k₂)) * (lcm(m₁, m₂)/m₁) * p₁ - (k₁/gcd(k₁, k₂)) * (lcm(m₁, m₂)/m₂) * p₂
+```
+-/
+def Poly.spol (p₁ p₂ : Poly) : SPolResult  :=
+  match p₁, p₂ with
+  | .add k₁ m₁ p₁, .add k₂ m₂ p₂ =>
+    let m    := m₁.lcm m₂
+    let m₁   := m.div m₁
+    let m₂   := m.div m₂
+    let g    := Nat.gcd k₁.natAbs k₂.natAbs
+    let c₁   := k₂/g
+    let c₂   := -k₁/g
+    let p₁   := p₁.mulMon c₁ m₁
+    let p₂   := p₂.mulMon c₂ m₂
+    let spol := p₁.combine p₂
+    { spol, c₁, m₁, c₂, m₂ }
+  | _, _ => {}
+
+/--
+Result of simplifying a polynomial `p₂` using a polynomial `p₁`.
+
+The simplification rewrites the first monomial of `p₂` that can be divided
+by the leading monomial of `p₁`.
+-/
+structure SimpResult where
+  /-- The resulting simplified polynomial after rewriting. -/
+  p  : Poly := .num 0
+  /-- The integer coefficient multiplied with polynomial `p₁` in the rewriting step. -/
+  k₁ : Int  := 0
+  /-- The integer coefficient multiplied with polynomial `p₂` during rewriting. -/
+  k₂ : Int  := 0
+  /-- The monomial factor applied to polynomial `p₁`. -/
+  m  : Mon  := .unit
+
+/--
+Simplifies polynomial `p₂` using polynomial `p₁` by rewriting.
+
+This function attempts to rewrite `p₂` by eliminating the first occurrence of
+the leading monomial of `p₁`.
+-/
+def Poly.simp? (p₁ p₂ : Poly) : Option SimpResult :=
+  match p₁ with
+  | .add k₁' m₁ p₁ =>
+    let rec go? (p₂ : Poly) : Option SimpResult :=
+      match p₂ with
+      | .add k₂' m₂ p₂ =>
+        if m₁.divides m₂ then
+          let m  := m₂.div m₁
+          let g  := Nat.gcd k₁'.natAbs k₂'.natAbs
+          let k₁ := -k₂'/g
+          let k₂ := k₁'/g
+          let p  := (p₁.mulMon k₁ m).combine (p₂.mulConst k₂)
+          some { p, k₁, k₂, m }
+        else if let some r := go? p₂ then
+          some { r with p := .add (k₂'*r.k₂) m₂ r.p }
+        else
+          none
+      | .num _ => none
+    go? p₂
+  | _ => none
+
+def Poly.degree : Poly → Nat
+  | .num _ => 0
+  | .add _ m _ => m.degree
+
+/-- Returns `true` if the leading monomial of `p` divides `m`. -/
+def Poly.divides (p : Poly) (m : Mon) : Bool :=
+  match p with
+  | .num _ => true -- should be unreachable
+  | .add _ m' _ => m'.divides m
+
+/-- Returns the leading coefficient of the given polynomial -/
+def Poly.lc : Poly → Int
+ | .num k => k
+ | .add k _ _ => k
+
+/-- Returns the leading monomial of the given polynomial. -/
+def Poly.lm : Poly → Mon
+ | .num _ => .unit
+ | .add _ m _ => m
+
+end Lean.Grind.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean

@@ -0,0 +1,43 @@
+/-
+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.Diseq
+import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
+import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
+
+namespace Lean.Meta.Grind.Arith.CommRing
+
+/--
+Returns a context of type `RArray α` containing the variables of the given ring.
+`α` is the type of the ring.
+-/
+def toContextExpr : RingM Expr := do
+  let ring ← getRing
+  if h : 0 < ring.vars.size then
+    RArray.toExpr ring.type id (RArray.ofFn (ring.vars[·]) h)
+  else
+    RArray.toExpr ring.type id (RArray.leaf (mkApp ring.natCastFn (toExpr 0)))
+
+private def mkLemmaPrefix (declName declNameC : Name) : RingM Expr := do
+  let ring ← getRing
+  let ctx ← toContextExpr
+  if let some (charInst, c) ← nonzeroCharInst? then
+    return mkApp5 (mkConst declNameC [ring.u]) ring.type (toExpr c) ring.commRingInst charInst ctx
+  else
+    return mkApp3 (mkConst declName [ring.u]) ring.type ring.commRingInst ctx
+
+def setNeUnsat (a b : Expr) (ra rb : RingExpr) : RingM Unit := do
+  let h ← mkLemmaPrefix ``Grind.CommRing.ne_unsat ``Grind.CommRing.ne_unsatC
+  closeGoal <| mkApp4 h (toExpr ra) (toExpr rb) reflBoolTrue (← mkDiseqProof a b)
+
+def setEqUnsat (k : Int) (a b : Expr) (ra rb : RingExpr) : RingM Unit := do
+  let mut h ← mkLemmaPrefix ``Grind.CommRing.eq_unsat ``Grind.CommRing.eq_unsatC
+  let (charInst, c) ← getCharInst
+  if c == 0 then
+    h := mkApp h charInst
+  closeGoal <| mkApp5 h (toExpr ra) (toExpr rb) (toExpr k) reflBoolTrue (← mkEqProof a b)
+
+end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Reify.lean

@@ -0,0 +1,108 @@
+/-
+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.Simp
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Util
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Var
+
+namespace Lean.Meta.Grind.Arith.CommRing
+
+def isAddInst (ring : Ring) (inst : Expr) : Bool :=
+  isSameExpr ring.addFn.appArg! inst
+def isMulInst (ring : Ring) (inst : Expr) : Bool :=
+  isSameExpr ring.mulFn.appArg! inst
+def isSubInst (ring : Ring) (inst : Expr) : Bool :=
+  isSameExpr ring.subFn.appArg! inst
+def isNegInst (ring : Ring) (inst : Expr) : Bool :=
+  isSameExpr ring.negFn.appArg! inst
+def isPowInst (ring : Ring) (inst : Expr) : Bool :=
+  isSameExpr ring.powFn.appArg! inst
+def isIntCastInst (ring : Ring) (inst : Expr) : Bool :=
+  isSameExpr ring.intCastFn.appArg! inst
+def isNatCastInst (ring : Ring) (inst : Expr) : Bool :=
+  isSameExpr ring.natCastFn.appArg! inst
+
+private def reportAppIssue (e : Expr) : GoalM Unit := do
+  reportIssue! "comm ring term with unexpected instance{indentExpr e}"
+
+/--
+Converts a Lean expression `e` in the `CommRing` with id `ringId` into
+a `CommRing.Expr` object.
+-/
+partial def reify? (e : Expr) : RingM (Option RingExpr) := do
+  let toVar (e : Expr) : RingM RingExpr := do
+    return .var (← mkVar e)
+  let asVar (e : Expr) : RingM RingExpr := do
+    reportAppIssue e
+    return .var (← mkVar e)
+  let rec go (e : Expr) : RingM RingExpr := do
+    match_expr e with
+    | HAdd.hAdd _ _ _ i a b =>
+      if isAddInst (← getRing) i then return .add (← go a) (← go b) else asVar e
+    | HMul.hMul _ _ _ i a b =>
+      if isMulInst (← getRing) i then return .mul (← go a) (← go b) else asVar e
+    | HSub.hSub _ _ _ i a b =>
+      if isSubInst (← getRing) i then return .sub (← go a) (← go b) else asVar e
+    | HPow.hPow _ _ _ i a b =>
+      let some k ← getNatValue? b | toVar e
+      if isPowInst (← getRing) i then return .pow (← go a) k else asVar e
+    | Neg.neg _ i a =>
+      if isNegInst (← getRing) i then return .neg (← go a) else asVar e
+    | IntCast.intCast _ i e =>
+      if isIntCastInst (← getRing) i then
+        let some k ← getIntValue? e | toVar e
+        return .num k
+      else
+        asVar e
+    | NatCast.natCast _ i e =>
+      if isNatCastInst (← getRing) i then
+        let some k ← getNatValue? e | toVar e
+        return .num k
+      else
+        asVar e
+    | OfNat.ofNat _ n _ =>
+      let some k ← getNatValue? n | toVar e
+      if (← withDefault <| isDefEq e (mkApp (← getRing).natCastFn n)) then
+        return .num k
+      else
+        asVar e
+    | _ => toVar e
+  let asNone (e : Expr) : GoalM (Option RingExpr) := do
+    reportAppIssue e
+    return none
+  match_expr e with
+  | HAdd.hAdd _ _ _ i a b =>
+    if isAddInst (← getRing) i then return some (.add (← go a) (← go b)) else asNone e
+  | HMul.hMul _ _ _ i a b =>
+    if isMulInst (← getRing) i then return some (.mul (← go a) (← go b)) else asNone e
+  | HSub.hSub _ _ _ i a b =>
+    if isSubInst (← getRing) i then return some (.sub (← go a) (← go b)) else asNone e
+  | HPow.hPow _ _ _ i a b =>
+    let some k ← getNatValue? b | return none
+    if isPowInst (← getRing) i then return some (.pow (← go a) k) else asNone e
+  | Neg.neg _ i a =>
+    if isNegInst (← getRing) i then return some (.neg (← go a)) else asNone e
+  | IntCast.intCast _ i e =>
+    if isIntCastInst (← getRing) i then
+      let some k ← getIntValue? e | return none
+      return some (.num k)
+    else
+      asNone e
+  | NatCast.natCast _ i e =>
+    if isNatCastInst (← getRing) i then
+      let some k ← getNatValue? e | return none
+      return some (.num k)
+    else
+      asNone e
+  | OfNat.ofNat _ n _ =>
+    let some k ← getNatValue? n | return none
+    if (← withDefault <| isDefEq e (mkApp (← getRing).natCastFn n)) then
+      return some (.num k)
+    else
+      asNone e
+  | _ => return none
+
+end  Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean

@@ -0,0 +1,120 @@
+/-
+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.Simp
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Util
+
+namespace Lean.Meta.Grind.Arith.CommRing
+
+private def internalizeFn (fn : Expr) : GoalM Expr := do
+  shareCommon (← canon fn)
+
+private def getAddFn (type : Expr) (u : Level) (commRingInst : Expr) : GoalM Expr := do
+  let instType := mkApp3 (mkConst ``HAdd [u, u, u]) type type type
+  let .some inst ← trySynthInstance instType |
+    throwError "failed to find instance for ring addition{indentExpr instType}"
+  let inst' := mkApp2 (mkConst ``instHAdd [u]) type <| mkApp2 (mkConst ``Grind.CommRing.toAdd [u]) type commRingInst
+  unless (← withDefault <| isDefEq inst inst') do
+    throwError "instance for addition{indentExpr inst}\nis not definitionally equal to the `Grind.CommRing` one{indentExpr inst'}"
+  internalizeFn <| mkApp4 (mkConst ``HAdd.hAdd [u, u, u]) type type type inst
+
+private def getMulFn (type : Expr) (u : Level) (commRingInst : Expr) : GoalM Expr := do
+  let instType := mkApp3 (mkConst ``HMul [u, u, u]) type type type
+  let .some inst ← trySynthInstance instType |
+    throwError "failed to find instance for ring multiplication{indentExpr instType}"
+  let inst' := mkApp2 (mkConst ``instHMul [u]) type <| mkApp2 (mkConst ``Grind.CommRing.toMul [u]) type commRingInst
+  unless (← withDefault <| isDefEq inst inst') do
+    throwError "instance for multiplication{indentExpr inst}\nis not definitionally equal to the `Grind.CommRing` one{indentExpr inst'}"
+  internalizeFn <| mkApp4 (mkConst ``HMul.hMul [u, u, u]) type type type inst
+
+private def getSubFn (type : Expr) (u : Level) (commRingInst : Expr) : GoalM Expr := do
+  let instType := mkApp3 (mkConst ``HSub [u, u, u]) type type type
+  let .some inst ← trySynthInstance instType |
+    throwError "failed to find instance for ring subtraction{indentExpr instType}"
+  let inst' := mkApp2 (mkConst ``instHSub [u]) type <| mkApp2 (mkConst ``Grind.CommRing.toSub [u]) type commRingInst
+  unless (← withDefault <| isDefEq inst inst') do
+    throwError "instance for subtraction{indentExpr inst}\nis not definitionally equal to the `Grind.CommRing` one{indentExpr inst'}"
+  internalizeFn <| mkApp4 (mkConst ``HSub.hSub [u, u, u]) type type type inst
+
+private def getNegFn (type : Expr) (u : Level) (commRingInst : Expr) : GoalM Expr := do
+  let instType := mkApp (mkConst ``Neg [u]) type
+  let .some inst ← trySynthInstance instType |
+    throwError "failed to find instance for ring negation{indentExpr instType}"
+  let inst' := mkApp2 (mkConst ``Grind.CommRing.toNeg [u]) type commRingInst
+  unless (← withDefault <| isDefEq inst inst') do
+    throwError "instance for negation{indentExpr inst}\nis not definitionally equal to the `Grind.CommRing` one{indentExpr inst'}"
+  internalizeFn <| mkApp2 (mkConst ``Neg.neg [u]) type inst
+
+private def getPowFn (type : Expr) (u : Level) (commRingInst : Expr) : GoalM Expr := do
+  let instType := mkApp3 (mkConst ``HPow [u, 0, u]) type Nat.mkType type
+  let .some inst ← trySynthInstance instType |
+    throwError "failed to find instance for ring power operator{indentExpr instType}"
+  let inst' := mkApp2 (mkConst ``Grind.CommRing.toHPow [u]) type commRingInst
+  unless (← withDefault <| isDefEq inst inst') do
+    throwError "instance for power operator{indentExpr inst}\nis not definitionally equal to the `Grind.CommRing` one{indentExpr inst'}"
+  internalizeFn <| mkApp4 (mkConst ``HPow.hPow [u, 0, u]) type Nat.mkType type inst
+
+private def getIntCastFn (type : Expr) (u : Level) (commRingInst : Expr) : GoalM Expr := do
+  let instType := mkApp (mkConst ``IntCast [u]) type
+  let .some inst ← trySynthInstance instType |
+    throwError "failed to find instance for ring intCast{indentExpr instType}"
+  let inst' := mkApp2 (mkConst ``Grind.CommRing.intCast [u]) type commRingInst
+  unless (← withDefault <| isDefEq inst inst') do
+    throwError "instance for intCast{indentExpr inst}\nis not definitionally equal to the `Grind.CommRing` one{indentExpr inst'}"
+  internalizeFn <| mkApp2 (mkConst ``IntCast.intCast [u]) type inst
+
+private def getNatCastFn (type : Expr) (u : Level) (commRingInst : Expr) : GoalM Expr := do
+  let instType := mkApp (mkConst ``NatCast [u]) type
+  let .some inst ← trySynthInstance instType |
+    throwError "failed to find instance for ring natCast{indentExpr instType}"
+  let inst' := mkApp2 (mkConst ``Grind.CommRing.natCastInst [u]) type commRingInst
+  unless (← withDefault <| isDefEq inst inst') do
+    throwError "instance for natCast{indentExpr inst}\nis not definitionally equal to the `Grind.CommRing` one{indentExpr inst'}"
+  internalizeFn <| mkApp2 (mkConst ``NatCast.natCast [u]) type inst
+
+/--
+Returns the ring id for the given type if there is a `CommRing` instance for it.
+
+This function will also perform sanity-checks
+(e.g., the `Add` instance for `type` must be definitionally equal to the `CommRing.toAdd` one.)
+
+It also caches the functions representing `+`, `*`, `-`, `^`, and `intCast`.
+-/
+def getRingId? (type : Expr) : GoalM (Option Nat) := do
+  if let some id? := (← get').typeIdOf.find? { expr := type } then
+    return id?
+  else
+    let id? ← go?
+    modify' fun s => { s with typeIdOf := s.typeIdOf.insert { expr := type } id? }
+    return id?
+where
+  go? : GoalM (Option Nat) := do
+    let u ← getDecLevel type
+    let ring := mkApp (mkConst ``Grind.CommRing [u]) type
+    let .some commRingInst ← trySynthInstance ring | return none
+    trace_goal[grind.ring] "new ring: {type}"
+    let charInst? ← withNewMCtxDepth do
+      let n ← mkFreshExprMVar (mkConst ``Nat)
+      let charType := mkApp3 (mkConst ``Grind.IsCharP [u]) type commRingInst n
+      let .some charInst ← trySynthInstance charType | pure none
+      let n ← instantiateMVars n
+      let some n ← evalNat n |>.run
+        | trace_goal[grind.ring] "found instance for{indentExpr charType}\nbut characteristic is not a natural number"; pure none
+      trace_goal[grind.ring] "characteristic: {n}"
+      pure <| some (charInst, n)
+    let addFn ← getAddFn type u commRingInst
+    let mulFn ← getMulFn type u commRingInst
+    let subFn ← getSubFn type u commRingInst
+    let negFn ← getNegFn type u commRingInst
+    let powFn ← getPowFn type u commRingInst
+    let intCastFn ← getIntCastFn type u commRingInst
+    let natCastFn ← getNatCastFn type u commRingInst
+    let id := (← get').rings.size
+    let ring : Ring := { id, type, u, commRingInst, charInst?, addFn, mulFn, subFn, negFn, powFn, intCastFn, natCastFn }
+    modify' fun s => { s with rings := s.rings.push ring }
+    return some id
+
+end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/ToExpr.lean

@@ -0,0 +1,57 @@
+/-
+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.Grind.CommRing.Poly
+import Lean.ToExpr
+
+namespace Lean.Meta.Grind.Arith.CommRing
+open Grind.CommRing
+/-!
+`ToExpr` instances for `CommRing.Poly` types.
+-/
+
+def ofPower (p : Power) : Expr :=
+  mkApp2 (mkConst ``Power.mk) (toExpr p.x) (toExpr p.k)
+
+instance : ToExpr Power where
+  toExpr := ofPower
+  toTypeExpr := mkConst ``Power
+
+def ofMon (m : Mon) : Expr :=
+  match m with
+  | .unit => mkConst ``Mon.unit
+  | .mult pw m => mkApp2 (mkConst ``Mon.mult) (toExpr pw) (ofMon m)
+
+instance : ToExpr Mon where
+  toExpr := ofMon
+  toTypeExpr := mkConst ``Mon
+
+def ofPoly (p : Poly) : Expr :=
+  match p with
+  | .num k => mkApp (mkConst ``Poly.num) (toExpr k)
+  | .add k m p => mkApp3 (mkConst ``Poly.add) (toExpr k) (toExpr m) (ofPoly p)
+
+instance : ToExpr Poly where
+  toExpr := ofPoly
+  toTypeExpr := mkConst ``Poly
+
+open Lean.Grind
+
+def ofRingExpr (e : CommRing.Expr) : Expr :=
+  match e with
+  | .num k => mkApp (mkConst ``CommRing.Expr.num) (toExpr k)
+  | .var x => mkApp (mkConst ``CommRing.Expr.var) (toExpr x)
+  | .add a b => mkApp2 (mkConst ``CommRing.Expr.add) (ofRingExpr a) (ofRingExpr b)
+  | .mul a b => mkApp2 (mkConst ``CommRing.Expr.mul) (ofRingExpr a) (ofRingExpr b)
+  | .sub a b => mkApp2 (mkConst ``CommRing.Expr.sub) (ofRingExpr a) (ofRingExpr b)
+  | .neg a => mkApp (mkConst ``CommRing.Expr.neg) (ofRingExpr a)
+  | .pow a k => mkApp2 (mkConst ``CommRing.Expr.pow) (ofRingExpr a) (toExpr k)
+
+instance : ToExpr CommRing.Expr where
+  toExpr := ofRingExpr
+  toTypeExpr := mkConst ``CommRing.Expr
+
+end Lean.Meta.Grind.Arith.CommRing

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

@@ -0,0 +1,103 @@
+/-
+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.Data.PersistentArray
+import Lean.Data.RBTree
+import Lean.Meta.Tactic.Grind.ENodeKey
+import Lean.Meta.Tactic.Grind.Arith.Util
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
+
+namespace Lean.Meta.Grind.Arith.CommRing
+export Lean.Grind.CommRing (Var Power Mon Poly)
+abbrev RingExpr := Grind.CommRing.Expr
+
+deriving instance Repr for Power, Mon, Poly
+
+mutual
+
+structure EqCnstr where
+  p     : Poly
+  h     : EqCnstrProof
+  sugar : Nat
+  id    : Nat
+
+inductive EqCnstrProof where
+  | core (a b : Expr)
+  | superpose (c₁ c₂ : EqCnstr)
+  | simp (c₁ c₂ : EqCnstr) (k₁ k₂ : Int) (m : Mon)
+  | mul (k : Int) (e : EqCnstr)
+  | div (k : Int) (e : EqCnstr)
+
+end
+
+instance : Inhabited EqCnstrProof where
+  default := .core default default
+
+instance : Inhabited EqCnstr where
+  default := { p := default, h := default, sugar := 0, id := 0 }
+
+protected def EqCnstr.compare (c₁ c₂ : EqCnstr) : Ordering :=
+  (compare c₁.sugar c₂.sugar) |>.then
+  (compare c₁.p.degree c₂.p.degree) |>.then
+  (compare c₁.id c₂.id)
+
+abbrev Queue : Type := RBTree EqCnstr EqCnstr.compare
+
+/-- State for each `CommRing` processed by this module. -/
+structure Ring where
+  id           : Nat
+  type         : Expr
+  /-- Cached `getDecLevel type` -/
+  u            : Level
+  /-- `CommRing` instance for `type` -/
+  commRingInst : Expr
+  /-- `IsCharP` instance for `type` if available. -/
+  charInst?    : Option (Expr × Nat) := .none
+  addFn        : Expr
+  mulFn        : Expr
+  subFn        : Expr
+  negFn        : Expr
+  powFn        : Expr
+  intCastFn    : Expr
+  natCastFn    : Expr
+  /--
+  Mapping from variables to their denotations.
+  Remark each variable can be in only one ring.
+  -/
+  vars         : PArray Expr := {}
+  /-- Mapping from `Expr` to a variable representing it. -/
+  varMap       : PHashMap ENodeKey Var := {}
+  /-- Mapping from Lean expressions to their representations as `RingExpr` -/
+  denote       : PHashMap ENodeKey RingExpr := {}
+  /-- Next unique id for `EqCnstr`s. -/
+  nextId       : Nat := 0
+  /-- Number of "steps": simplification and superposition. -/
+  steps        : Nat := 0
+  /-- Equations to process. -/
+  queue        : Queue := {}
+  /--
+  Mapping from variables `x` to equations such that the smallest variable
+  in the leading monomial is `x`.
+  -/
+  varToBasis   : PArray (List EqCnstr) := {}
+  deriving Inhabited
+
+/-- State for all `CommRing` types detected by `grind`. -/
+structure State where
+  /--
+  Commutative rings.
+  We expect to find a small number of rings in a given goal. Thus, using `Array` is fine here.
+  -/
+  rings : Array Ring := {}
+  /--
+  Mapping from types to its "ring id". We cache failures using `none`.
+  `typeIdOf[type]` is `some id`, then `id < rings.size`. -/
+  typeIdOf : PHashMap ENodeKey (Option Nat) := {}
+  /- Mapping from expressions/terms to their ring ids. -/
+  exprToRingId : PHashMap ENodeKey Nat := {}
+  deriving Inhabited
+
+end Lean.Meta.Grind.Arith.CommRing

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

@@ -0,0 +1,85 @@
+/-
+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.Arith.CommRing
+
+def get' : GoalM State := do
+  return (← get).arith.ring
+
+@[inline] def modify' (f : State → State) : GoalM Unit := do
+  modify fun s => { s with arith.ring := f s.arith.ring }
+
+/-- We don't want to keep carrying the `RingId` around. -/
+abbrev RingM := ReaderT Nat GoalM
+
+abbrev RingM.run (ringId : Nat) (x : RingM α) : GoalM α :=
+  x ringId
+
+abbrev getRingId : RingM Nat :=
+  read
+
+def getRing : RingM Ring := do
+  let s ← get'
+  let ringId ← getRingId
+  if h : ringId < s.rings.size then
+    return s.rings[ringId]
+  else
+    throwError "`grind` internal error, invalid ringId"
+
+@[inline] def modifyRing (f : Ring → Ring) : RingM Unit := do
+  let ringId ← getRingId
+  modify' fun s => { s with rings := s.rings.modify ringId f }
+
+def getTermRingId? (e : Expr) : GoalM (Option Nat) := do
+  return (← get').exprToRingId.find? { expr := e }
+
+def setTermRingId (e : Expr) : RingM Unit := do
+  let ringId ← getRingId
+  if let some ringId' ← getTermRingId? e then
+    unless ringId' == ringId do
+      reportIssue! "expression in two different rings{indentExpr e}"
+    return ()
+  modify' fun s => { s with exprToRingId := s.exprToRingId.insert { expr := e } ringId }
+
+/-- Returns `some c` if the current ring has a nonzero characteristic `c`. -/
+def nonzeroChar? : RingM (Option Nat) := do
+  if let some (_, c) := (← getRing).charInst? then
+    if c != 0 then
+      return some c
+  return none
+
+/-- Returns `some (charInst, c)` if the current ring has a nonzero characteristic `c`. -/
+def nonzeroCharInst? : RingM (Option (Expr × Nat)) := do
+  if let some (inst, c) := (← getRing).charInst? then
+    if c != 0 then
+      return some (inst, c)
+  return none
+
+/-- Returns `true` if the current ring has a `IsCharP` instance. -/
+def hasChar  : RingM Bool := do
+  return (← getRing).charInst?.isSome
+
+/--
+Returns the pair `(charInst, c)`. If the ring does not have a `IsCharP` instance, then throws internal error.
+-/
+def getCharInst : RingM (Expr × Nat) := do
+  let some c := (← getRing).charInst?
+    | throwError "`grind` internal error, ring does not have a characteristic"
+  return c
+
+/--
+Converts the given ring expression into a multivariate polynomial.
+If the ring has a nonzero characteristic, it is used during normalization.
+-/
+def _root_.Lean.Grind.CommRing.Expr.toPolyM (e : RingExpr) : RingM Poly := do
+  if let some c ← nonzeroChar? then
+    return e.toPolyC c
+  else
+    return e.toPoly
+
+end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Var.lean

@@ -0,0 +1,25 @@
+/-
+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.Arith.CommRing.Util
+
+namespace Lean.Meta.Grind.Arith.CommRing
+
+def mkVar (e : Expr) : RingM Var := do
+  let s ← getRing
+  if let some var := s.varMap.find? { expr := e } then
+    return var
+  let var : Var := s.vars.size
+  modifyRing fun s => { s with
+    vars       := s.vars.push e
+    varMap     := s.varMap.insert { expr := e } var
+    varToBasis := s.varToBasis.push []
+  }
+  setTermRingId e
+  markAsCommRingTerm e
+  return var
+
+end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean

@@ -64,11 +64,6 @@ def mkNatExprDecl (e : Int.OfNat.Expr) : ProofM Expr := do
   modify fun s => { s with natExprMap := s.natExprMap.insert e x }
   return x
 
-private def mkDiseqProof (a b : Expr) : GoalM Expr := do
- let some h ← mkDiseqProof? a b
-   | throwError "internal `grind` error, failed to build disequality proof for{indentExpr a}\nand{indentExpr b}"
-  return h
-
 private def mkLetOfMap {_ : Hashable α} {_ : BEq α} (m : Std.HashMap α Expr) (e : Expr)
     (varPrefix : Name) (varType : Expr) (toExpr : α → Expr) : GoalM Expr := do
   if m.isEmpty then

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

@@ -26,17 +26,6 @@ where
 end Int.Linear
 
 namespace Lean.Meta.Grind.Arith.Cutsat
-/--
-`gcdExt a b` returns the triple `(g, α, β)` such that
-- `g = gcd a b` (with `g ≥ 0`), and
-- `g = α * a + β * β`.
--/
-partial def gcdExt (a b : Int) : Int × Int × Int :=
-  if b = 0 then
-    (a.natAbs, if a = 0 then 0 else a / a.natAbs, 0)
-  else
-    let (g, α, β) := gcdExt b (a % b)
-    (g, β, α - (a / b) * β)
 
 def get' : GoalM State := do
   return (← get).arith.cutsat

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

@@ -6,11 +6,13 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Meta.Tactic.Grind.Arith.Offset
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.EqCnstr
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Internalize
 
 namespace Lean.Meta.Grind.Arith
 
 def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
   Offset.internalize e parent?
   Cutsat.internalize e parent?
+  CommRing.internalize e parent?
 
 end Lean.Meta.Grind.Arith

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

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Meta.Tactic.Grind.Arith.Offset.Types
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
 
 namespace Lean.Meta.Grind.Arith
 
@@ -13,6 +14,7 @@ namespace Lean.Meta.Grind.Arith
 structure State where
   offset : Offset.State := {}
   cutsat : Cutsat.State := {}
+  ring   : CommRing.State := {}
   deriving Inhabited
 
 end Lean.Meta.Grind.Arith

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

@@ -82,5 +82,16 @@ def quoteIfArithTerm (e : Expr) : MessageData :=
     aquote e
   else
     e
+/--
+`gcdExt a b` returns the triple `(g, α, β)` such that
+- `g = gcd a b` (with `g ≥ 0`), and
+- `g = α * a + β * β`.
+-/
+partial def gcdExt (a b : Int) : Int × Int × Int :=
+  if b = 0 then
+    (a.natAbs, if a = 0 then 0 else a / a.natAbs, 0)
+  else
+    let (g, α, β) := gcdExt b (a % b)
+    (g, β, α - (a / b) * β)
 
 end Lean.Meta.Grind.Arith

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

@@ -111,7 +111,7 @@ private def propagateOffsetEq (rhsRoot lhsRoot : ENode) : GoalM Unit := do
 
 /--
 Helper function for combining `ENode.cutsat?` fields and propagating equalities
-to the offset constraint module.
+to the cutsat module.
 It returns a set of parents that should be traversed for disequality propagation.
 -/
 private def propagateCutsatEq (rhsRoot lhsRoot : ENode) : GoalM ParentSet := do
@@ -138,6 +138,28 @@ private def propagateCutsatEq (rhsRoot lhsRoot : ENode) : GoalM ParentSet := do
     else
       return {}
 
+/--
+Helper function for combining `ENode.ring?` fields and propagating equalities
+to the commutative ring module.
+It returns a set of parents that should be traversed for disequality propagation.
+-/
+private def propagateCommRingEq (rhsRoot lhsRoot : ENode) : GoalM ParentSet := do
+  match lhsRoot.ring? with
+  | some lhsRing =>
+    if let some rhsRing := rhsRoot.ring? then
+      Arith.CommRing.processNewEq lhsRing rhsRing
+      return {}
+    else
+      -- We have to retrieve the node because other fields have been updated
+      let rhsRoot ← getENode rhsRoot.self
+      setENode rhsRoot.self { rhsRoot with ring? := lhsRing }
+      getParents rhsRoot.self
+  | none =>
+    if rhsRoot.ring?.isSome then
+      getParents lhsRoot.self
+    else
+      return {}
+
 /--
 Tries to apply beta-reductiong using the parent applications of the functions in `fns` with
 the lambda expressions in `lams`.
@@ -241,7 +263,8 @@ where
     propagateBeta lams₁ fns₁
     propagateBeta lams₂ fns₂
     propagateOffsetEq rhsRoot lhsRoot
-    let parentsToPropagateDiseqs ← propagateCutsatEq rhsRoot lhsRoot
+    let parentsToPropagateCutsatDiseqs ← propagateCutsatEq rhsRoot lhsRoot
+    let parentsToPropagateRingDiseqs ← propagateCommRingEq rhsRoot lhsRoot
     resetParentsOf lhsRoot.self
     copyParentsTo parents rhsNode.root
     unless (← isInconsistent) do
@@ -251,8 +274,8 @@ where
         propagateUp parent
       for e in toPropagateDown do
         propagateDown e
-      propagateCutsatDiseqs parentsToPropagateDiseqs
-
+      propagateCutsatDiseqs parentsToPropagateCutsatDiseqs
+      propagateCommRingDiseqs parentsToPropagateRingDiseqs
   updateRoots (lhs : Expr) (rootNew : Expr) : GoalM Unit := do
     traverseEqc lhs fun n =>
       setENode n.self { n with root := rootNew }

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

@@ -78,4 +78,9 @@ def mkDiseqProof? (a b : Expr) : GoalM (Option Expr) := do
   else
     return mkApp6 (mkConst ``Grind.ne_of_ne_of_eq_right u) α b a d (← mkEqProof b d) h
 
+def mkDiseqProof (a b : Expr) : GoalM Expr := do
+ let some h ← mkDiseqProof? a b
+   | throwError "internal `grind` error, failed to build disequality proof for{indentExpr a}\nand{indentExpr b}"
+  return h
+
 end Lean.Meta.Grind

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

@@ -160,6 +160,7 @@ builtin_grind_propagator propagateEqDown ↓Eq := fun e => do
       propagateBoolDiseq lhs
       propagateBoolDiseq rhs
     propagateCutsatDiseq lhs rhs
+    propagateCommRingDiseq lhs rhs
     let thms ← getExtTheorems α
     if !thms.isEmpty then
       /-

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

@@ -323,6 +323,11 @@ structure ENode where
   to the cutsat module. Its implementation is similar to the `offset?` field.
   -/
   cutsat? : Option Expr := none
+  /--
+  The `ring?` field is used to propagate equalities from the `grind` congruence closure module
+  to the comm ring module. Its implementation is similar to the `offset?` field.
+  -/
+  ring? : Option Expr := none
   -- Remark: we expect to have builtin support for offset constraints, cutsat, and comm ring.
   -- If the number of satellite solvers increases, we may add support for an arbitrary solvers like done in Z3.
   deriving Inhabited, Repr
@@ -1015,6 +1020,53 @@ def markAsCutsatTerm (e : Expr) : GoalM Unit := do
     setENode root.self { root with cutsat? := some e }
     propagateCutsatDiseqs (← getParents root.self)
 
+/--
+Notifies the comm ring module that `a = b` where
+`a` and `b` are terms that have been internalized by this module.
+-/
+@[extern "lean_process_ring_eq"] -- forward definition
+opaque Arith.CommRing.processNewEq (a b : Expr) : GoalM Unit
+
+/--
+Notifies the comm ring module that `a ≠ b` where
+`a` and `b` are terms that have been internalized by this module.
+-/
+@[extern "lean_process_ring_diseq"] -- forward definition
+opaque Arith.CommRing.processNewDiseq (a b : Expr) : GoalM Unit
+
+/--
+Given `lhs` and `rhs` that are known to be disequal, checks whether
+`lhs` and `rhs` have ring terms `e₁` and `e₂` attached to them,
+and invokes process `Arith.CommRing.processNewDiseq e₁ e₂`
+-/
+def propagateCommRingDiseq (lhs rhs : Expr) : GoalM Unit := do
+  let some lhs ← get? lhs | return ()
+  let some rhs ← get? rhs | return ()
+  Arith.CommRing.processNewDiseq lhs rhs
+where
+  get? (a : Expr) : GoalM (Option Expr) := do
+    return (← getRootENode a).ring?
+
+/--
+Traverses disequalities in `parents`, and propagate the ones relevant to the
+comm ring module.
+-/
+def propagateCommRingDiseqs (parents : ParentSet) : GoalM Unit := do
+  forEachDiseq parents propagateCommRingDiseq
+
+/--
+Marks `e` as a term of interest to the ring module.
+If the root of `e`s equivalence class has already a term of interest,
+a new equality is propagated to the ring module.
+-/
+def markAsCommRingTerm (e : Expr) : GoalM Unit := do
+  let root ← getRootENode e
+  if let some e' := root.ring? then
+    Arith.CommRing.processNewEq e e'
+  else
+    setENode root.self { root with ring? := some e }
+    propagateCommRingDiseqs (← getParents root.self)
+
 /-- Returns `true` is `e` is the root of its congruence class. -/
 def isCongrRoot (e : Expr) : GoalM Bool := do
   return (← getENode e).isCongrRoot

src/Lean/Meta/Tactic/Lets.lean

@@ -0,0 +1,437 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+prelude
+import Lean.Meta.Tactic.Replace
+
+/-!
+# Tactics to manipulate `let` expressions
+-/
+
+open Lean Meta
+
+namespace Lean.Meta
+
+/-!
+### `let` extraction
+
+Extracting `let`s means to locate `let`/`letFun`s in a term and to extract them
+from the term, extending the local context with new declarations in the process.
+A related process is lifting `lets`, which means to move `let`/`letFun`s toward the root of a term.
+-/
+
+namespace ExtractLets
+
+structure LocalDecl' where
+  decl : LocalDecl
+  /--
+  If true, is a `let`, if false, is a `letFun`.
+  Used in `lift` mode.
+  -/
+  isLet : Bool
+
+structure State where
+  /-- Names to use for local definitions for the extracted lets. -/
+  givenNames : List Name
+  /-- Saved declarations for the extracted `let`s. -/
+  decls : Array LocalDecl' := #[]
+  /-- Map from `let` values to fvars. To support the `merge` option. -/
+  valueMap : ExprStructMap FVarId := {}
+  deriving Inhabited
+
+-- The `Bool` in the cache key is whether we are looking at a "top-level" expression.
+abbrev M := ReaderT ExtractLetsConfig <| MonadCacheT (Bool × ExprStructEq) Expr <| StateRefT State MetaM
+
+/-- Returns `true` if `nextName?` would return a name. -/
+def hasNextName : M Bool := do
+  return !(← read).onlyGivenNames || !(← get).givenNames.isEmpty
+
+/-- Gets the next name to use for extracted `let`s -/
+def nextName? : M (Option Name) := do
+  let s ← get
+  match s.givenNames, (← read).onlyGivenNames with
+  | n :: ns, _      => set { s with givenNames := ns }; return n
+  | []     , true   => return none
+  | []     , false  => return `_
+
+/--
+Generate a name to use for a new local declaration, derived possibly from the given binder name.
+Returns `none` iff `hasNextName` is false.
+-/
+def nextNameForBinderName? (binderName : Name) : M (Option Name) := do
+  if let some n ← nextName? then
+    if n != `_ then
+      return n
+    else
+      if binderName.isAnonymous then
+        -- Use a nicer binder name than `[anonymous]`, which can appear for example in `letFun x f` when `f` is not a lambda expression.
+        mkFreshUserName `a
+      else if (← read).preserveBinderNames || n.hasMacroScopes then
+        return n
+      else
+        mkFreshUserName binderName
+  else
+    return none
+
+/--
+Returns 'true' if `e` does not depend on any of the fvars in `fvars`.
+-/
+def extractable (fvars : List Expr) (e : Expr) : Bool :=
+  !e.hasAnyFVar (fvars.contains <| .fvar ·)
+
+/--
+Returns whether a let-like expression with the given type and value is extractable,
+given the list `fvars` of binders that inhibit extraction.
+-/
+def isExtractableLet (fvars : List Expr) (n : Name) (t v : Expr) : M (Bool × Name) := do
+  if (← hasNextName) && extractable fvars t && extractable fvars v then
+    if let some n ← nextNameForBinderName? n then
+      return (true, n)
+  -- In lift mode, we temporarily extract non-extractable lets, but we do not make use of `givenNames` for them.
+  -- These will be flushed as let/letFun expressions, and we wish to preserve the original binder name.
+  if (← read).lift then
+    return (true, n)
+  return (false, n)
+
+/--
+Adds the `decl` to the `decls` list. Assumes that `decl` is an ldecl.
+-/
+def addDecl (decl : LocalDecl) (isLet : Bool) : M Unit := do
+  let cfg ← read
+  modify fun s => { s with
+    decls := s.decls.push { decl, isLet }
+    valueMap := if cfg.merge then s.valueMap.insert decl.value decl.fvarId else s.valueMap
+  }
+
+/--
+Removes and returns all local declarations that (transitively) depend on `fvar`.
+-/
+def flushDecls (fvar : FVarId) : M (Array LocalDecl') := do
+  let mut fvarSet : FVarIdSet := {}
+  fvarSet := fvarSet.insert fvar
+  let mut toSave := #[]
+  let mut toFlush := #[]
+  for ldecl in (← get).decls do
+    if ldecl.decl.type.hasAnyFVar (fvarSet.contains ·) || ldecl.decl.value.hasAnyFVar (fvarSet.contains ·) then
+      toFlush := toFlush.push ldecl
+      fvarSet := fvarSet.insert ldecl.decl.fvarId
+    else
+      toSave := toSave.push ldecl
+  modify fun s => { s with decls := toSave }
+  return toFlush
+
+/--
+Ensures that the given local declarations are in context. Runs `k` in that context.
+-/
+def withEnsuringDeclsInContext [Monad m] [MonadControlT MetaM m] [MonadLCtx m] (decls : Array LocalDecl') (k : m α) : m α := do
+  let lctx ← getLCtx
+  let decls := decls |>.filter (!lctx.contains ·.decl.fvarId) |>.map (·.decl)
+  withExistingLocalDecls decls.toList k
+
+/--
+Closes all the local declarations in `e`, creating `let` and `letFun` expressions.
+Does not require that any of the declarations are in context.
+Assumes that `e` contains no metavariables with local contexts that contain any of these metavariables
+(the extraction procedure creates no new metavariables, so this is the case).
+
+This should *not* be used when closing lets for new goal metavariables, since
+1. The goal contains the decls in its local context, violating the assumption.
+2. We need to use true `let`s in that case, since tactics may zeta-delta reduce these declarations.
+-/
+def mkLetDecls (decls : Array LocalDecl') (e : Expr) : MetaM Expr := do
+  withEnsuringDeclsInContext decls do
+    decls.foldrM (init := e) fun { decl, isLet } e => do
+      if isLet then
+        return .letE decl.userName decl.type decl.value (e.abstract #[decl.toExpr]) false
+      else
+        mkLetFun decl.toExpr decl.value e
+
+/--
+Makes sure the declaration for `fvarId` is marked with `isLet := true`.
+Used in `lift + merge` mode to ensure that, after merging, if any version was a `let` then it's a `let` rather than a `letFun`.
+-/
+def ensureIsLet (fvarId : FVarId) : M Unit := do
+  modify fun s => { s with
+    decls := s.decls.map fun d =>
+      if d.decl.fvarId == fvarId then { d with isLet := true } else d
+  }
+
+/--
+Ensures that the given `fvarId` is in context by adding `decls` from the state.
+Simplification: since we are not recording which decls depend on which, but we do know all dependencies
+come before a particular decl, we add all the decls up to and including `fvarId`.
+
+Used for `merge` feature.
+-/
+def withDeclInContext (fvarId : FVarId) (k : M α) : M α := do
+  let decls := (← get).decls
+  if (← getLCtx).contains fvarId then
+    -- Is either pre-existing or already added.
+    k
+  else if let some idx := decls.findIdx? (·.decl.fvarId == fvarId) then
+    withEnsuringDeclsInContext decls[0:idx+1] k
+  else
+    k
+
+/--
+Initializes the `valueMap` with all the local definitions that aren't implementation details.
+Used for `merge` feature when `useContext` is enabled.
+-/
+def initializeValueMap : M Unit := do
+  let lctx ← getLCtx
+  lctx.forM fun decl => do
+    if decl.isLet && !decl.isImplementationDetail then
+      let value ← instantiateMVars decl.value
+      modify fun s => { s with valueMap := s.valueMap.insert value decl.fvarId }
+
+/--
+Returns `true` if the expression contains a `let` expression or a `letFun`
+(this does not verify that the `letFun`s are well-formed).
+Its purpose is to be a check for whether a subexpression can be skipped.
+-/
+def containsLet (e : Expr) : Bool :=
+  Option.isSome <| e.find? fun e' => e'.isLet || e'.isConstOf ``letFun
+
+/--
+Extracts lets from `e`.
+- `fvars` is an array of all the local variables from going under binders,
+  used to detect whether an expression is extractable. Extracted `let`s do not have their fvarids in this list.
+  This is not part of the cache key since it's an optimization and in principle derivable.
+- `topLevel` is whether we are still looking at the top-level expression.
+  The body of an extracted top-level let is also considered to be top-level.
+  This is part of the cache key since it affects what is extracted.
+
+Note: the return value may refer to fvars that are not in the current local context, but they are in the `decls` list.
+-/
+partial def extractCore (fvars : List Expr) (e : Expr) (topLevel : Bool := false) : M Expr := do
+  let cfg ← read
+  if e.isAtomic then
+    return e
+  else if !cfg.descend && !topLevel then
+    return e
+  else
+    checkCache (topLevel, (e : ExprStructEq)) fun _ => do
+      if !containsLet e then
+        return e
+      -- Don't honor `proofs := false` or `types := false` for top-level lets, since it's confusing not having them be extracted.
+      unless topLevel && (e.isLet || e.isLetFun || e.isMData) do
+        if !cfg.proofs then
+          if ← isProof e then
+            return e
+        if !cfg.types then
+          if ← isType e then
+            return e
+      let whenDescend (k : M Expr) : M Expr := do if cfg.descend then k else pure e
+      match e with
+      | .bvar .. | .fvar .. | .mvar .. | .sort .. | .const .. | .lit .. => unreachable!
+      | .mdata _ e'      => return e.updateMData! (← extractCore fvars e' (topLevel := topLevel))
+      | .letE n t v b _  => extractLetLike true n t v b (fun t v b => pure <| e.updateLet! t v b) (topLevel := topLevel)
+      | .app ..          =>
+        if e.isLetFun then
+          extractLetFun e (topLevel := topLevel)
+        else
+          whenDescend do extractApp e.getAppFn e.getAppArgs
+      | .proj _ _ s      => whenDescend do return e.updateProj! (← extractCore fvars s)
+      | .lam n t b i     => whenDescend do extractBinder n t b i (fun t b => e.updateLambda! i t b)
+      | .forallE n t b i => whenDescend do extractBinder n t b i (fun t b => e.updateForall! i t b)
+where
+  extractBinder (n : Name) (t b : Expr) (i : BinderInfo) (mk : Expr → Expr → Expr) : M Expr := do
+    let t ← extractCore fvars t
+    if (← read).underBinder then
+      withLocalDecl n i t fun x => do
+        let b ← extractCore (x :: fvars) (b.instantiate1 x)
+        if (← read).lift then
+          let toFlush ← flushDecls x.fvarId!
+          let b ← mkLetDecls toFlush b
+          return mk t (b.abstract #[x])
+        else
+          return mk t (b.abstract #[x])
+    else
+      return mk t b
+  extractLetLike (isLet : Bool) (n : Name) (t v b : Expr) (mk : Expr → Expr → Expr → M Expr) (topLevel : Bool) : M Expr := do
+    let cfg ← read
+    let t ← extractCore fvars t
+    let v ← extractCore fvars v
+    if cfg.usedOnly && !b.hasLooseBVars then
+      return ← extractCore fvars b (topLevel := topLevel)
+    if cfg.merge then
+      if let some fvarId := (← get).valueMap.get? v then
+        if isLet && cfg.lift then ensureIsLet fvarId
+        return ← withDeclInContext fvarId <|
+          extractCore fvars (b.instantiate1 (.fvar fvarId)) (topLevel := topLevel)
+    let (extract, n) ← isExtractableLet fvars n t v
+    if !extract && (!cfg.underBinder || !cfg.descend) then
+      return ← mk t v b
+    withLetDecl n t v fun x => do
+      if extract then
+        addDecl (← x.fvarId!.getDecl) isLet
+        extractCore fvars (b.instantiate1 x) (topLevel := topLevel)
+      else
+        let b ← extractCore (x :: fvars) (b.instantiate1 x)
+        mk t v (b.abstract #[x])
+  /-- `e` is the letFun expression -/
+  extractLetFun (e : Expr) (topLevel : Bool) : M Expr := do
+    let letFunE := e.getAppFn
+    let β := e.getArg! 1
+    let (n, t, v, b) := e.letFun?.get!
+    extractLetLike false n t v b (topLevel := topLevel)
+      (fun t v b =>
+        -- Strategy: construct letFun directly rather than use `mkLetFun`.
+        -- We don't update the `β` argument.
+        return mkApp4 letFunE t β v (.lam n t b .default))
+  extractApp (f : Expr) (args : Array Expr) : M Expr := do
+    let cfg ← read
+    if f.isConstOf ``letFun && args.size ≥ 4 then
+      extractApp (mkAppN f args[0:4]) args[4:]
+    else
+      let f' ← extractCore fvars f
+      if cfg.implicits then
+        return mkAppN f' (← args.mapM (extractCore fvars))
+      else
+        let (paramInfos, _) ← instantiateForallWithParamInfos (← inferType f) args
+        let mut args := args
+        for i in [0:args.size] do
+          if paramInfos[i]!.binderInfo.isExplicit then
+            args := args.set! i (← extractCore fvars args[i]!)
+        return mkAppN f' args
+
+def extractTopLevel (e : Expr) : M Expr := do
+  let e ← instantiateMVars e
+  extractCore [] e (topLevel := true)
+
+/--
+Main entry point for extracting lets.
+-/
+def extract (es : Array Expr) : M (Array Expr) := do
+  let cfg ← read
+  if cfg.merge && cfg.useContext then
+    initializeValueMap
+  es.mapM extractTopLevel
+
+end ExtractLets
+
+/--
+Implementation of the `extractLets` function.
+- `es` is an array of terms that are valid in the current local context.
+- `k` is a callback that is run in the updated local context with all relevant `let`s extracted
+  and with the post-extraction expressions, and the remaining names from `givenNames`.
+-/
+private def extractLetsImp (es : Array Expr) (givenNames : List Name)
+    (k : Array FVarId → Array Expr → List Name → MetaM α) (config : ExtractLetsConfig) : MetaM α := do
+  let (es, st) ← ExtractLets.extract es |>.run config |>.run' {} |>.run { givenNames }
+  let givenNames' := st.givenNames
+  let decls := st.decls.map (·.decl)
+  withExistingLocalDecls decls.toList <| k (decls.map (·.fvarId)) es givenNames'
+
+/--
+Extracts `let` and `letFun` expressions into local definitions,
+evaluating `k` at the post-extracted expressions and the extracted fvarids, within a context containing those local declarations.
+- The `givenNames` is a list of explicit names to use for extracted local declarations.
+  If a name is `_` (or if there is no provided given name and `config.onlyGivenNames` is true) then uses a hygienic name
+  based on the existing binder name.
+-/
+def extractLets [Monad m] [MonadControlT MetaM m] (es : Array Expr) (givenNames : List Name)
+    (k : Array FVarId → Array Expr → List Name → m α) (config : ExtractLetsConfig := {}) : m α :=
+  map3MetaM (fun k => extractLetsImp es givenNames k config) k
+
+/--
+Lifts `let` and `letFun` expressions in the given expression as far out as possible.
+-/
+def liftLets (e : Expr) (config : LiftLetsConfig := {}) : MetaM Expr := do
+  let (es, st) ← ExtractLets.extract #[e] |>.run { config with onlyGivenNames := true } |>.run' {} |>.run { givenNames := [] }
+  ExtractLets.mkLetDecls st.decls es[0]!
+
+end Lean.Meta
+
+private def throwMadeNoProgress (tactic : Name) (mvarId : MVarId) : MetaM α :=
+  throwTacticEx tactic mvarId m!"made no progress"
+
+/--
+Extracts `let` and `letFun` expressions from the target,
+returning `FVarId`s for the extracted let declarations along with the new goal.
+- The `givenNames` is a list of explicit names to use for extracted local declarations.
+  If a name is `_` (or if there is no provided given name and `config.onlyGivenNames` is true) then uses a hygienic name
+  based on the existing binder name.
+-/
+def Lean.MVarId.extractLets (mvarId : MVarId) (givenNames : List Name) (config : ExtractLetsConfig := {}) :
+    MetaM ((Array FVarId × List Name) × MVarId) :=
+  mvarId.withContext do
+    mvarId.checkNotAssigned `extract_lets
+    let ty ← mvarId.getType
+    Meta.extractLets #[ty] givenNames (config := config) fun fvarIds es givenNames' => do
+      let ty' := es[0]!
+      if fvarIds.isEmpty && ty == ty' then
+        throwMadeNoProgress `extract_lets mvarId
+      let g ← mkFreshExprSyntheticOpaqueMVar ty' (← mvarId.getTag)
+      mvarId.assign <| ← mkLetFVars (usedLetOnly := false) (fvarIds.map .fvar) g
+      return ((fvarIds, givenNames'), g.mvarId!)
+
+/--
+Like `Lean.MVarId.extractLets` but extracts lets from a local declaration.
+If the local declaration has a value, then both its type and value are modified.
+-/
+def Lean.MVarId.extractLetsLocalDecl (mvarId : MVarId) (fvarId : FVarId) (givenNames : List Name) (config : ExtractLetsConfig := {}) :
+    MetaM ((Array FVarId × List Name) × MVarId) := do
+  mvarId.checkNotAssigned `extract_lets
+  mvarId.withReverted #[fvarId] fun mvarId fvars => mvarId.withContext do
+    let finalize (fvarIds : Array FVarId) (givenNames' : List Name) (targetNew : Expr) := do
+      let g ← mkFreshExprSyntheticOpaqueMVar targetNew (← mvarId.getTag)
+      mvarId.assign <| ← mkLetFVars (usedLetOnly := false) (fvarIds.map .fvar) g
+      return ((fvarIds, givenNames'), fvars.map .some, g.mvarId!)
+    match ← mvarId.getType with
+    | .forallE n t b i =>
+      Meta.extractLets #[t] givenNames (config := config) fun fvarIds es givenNames' => do
+        let t' := es[0]!
+        if fvarIds.isEmpty && t == t' then
+          throwMadeNoProgress `extract_lets mvarId
+        finalize fvarIds givenNames' (.forallE n t' b i)
+    | .letE n t v b ndep =>
+      Meta.extractLets #[t, v] givenNames (config := config) fun fvarIds es givenNames' => do
+        let t' := es[0]!
+        let v' := es[1]!
+        if fvarIds.isEmpty && t == t' && v == v' then
+          throwMadeNoProgress `extract_lets mvarId
+        finalize fvarIds givenNames' (.letE n t' v' b ndep)
+    | _ => throwTacticEx `extract_lets mvarId "unexpected auxiliary target"
+
+/--
+Lifts `let` and `letFun` expressions in target as far out as possible.
+Throws an exception if nothing is lifted.
+
+Like `Lean.MVarId.extractLets`, but top-level lets are not added to the local context.
+-/
+def Lean.MVarId.liftLets (mvarId : MVarId) (config : LiftLetsConfig := {}) : MetaM MVarId :=
+  mvarId.withContext do
+    mvarId.checkNotAssigned `lift_lets
+    let ty ← mvarId.getType
+    let ty' ← Meta.liftLets ty (config := config)
+    if ty == ty' then
+      throwMadeNoProgress `lift_lets mvarId
+    mvarId.replaceTargetDefEq ty'
+
+/--
+Like `Lean.MVarId.liftLets` but lifts lets in a local declaration.
+If the local declaration has a value, then both its type and value are modified.
+-/
+def Lean.MVarId.liftLetsLocalDecl (mvarId : MVarId) (fvarId : FVarId) (config : LiftLetsConfig := {}) : MetaM MVarId := do
+  mvarId.checkNotAssigned `lift_lets
+  -- Revert to make sure the resulting type/value refers fvars that come after `fvarId`.
+  -- (Note: reverting isn't necessary unless both `merge := true` and `useContext := true`.)
+  Prod.snd <$> mvarId.withReverted #[fvarId] fun mvarId fvars => mvarId.withContext do
+    let finalize (targetNew : Expr) := do
+      return ((), fvars.map .some, ← mvarId.replaceTargetDefEq targetNew)
+    match ← mvarId.getType with
+    | .forallE n t b i =>
+      let t' ← Meta.liftLets t (config := config)
+      if t == t' then
+        throwMadeNoProgress `lift_lets mvarId
+      finalize (.forallE n t' b i)
+    | .letE n t v b ndep =>
+      let t' ← Meta.liftLets t (config := config)
+      let v' ← Meta.liftLets v (config := config)
+      if t == t' && v == v' then
+        throwMadeNoProgress `lift_lets mvarId
+      finalize (.letE n t' v' b ndep)
+    | _ => throwTacticEx `lift_lets mvarId "unexpected auxiliary target"

src/Lean/Parser/Module.lean

@@ -11,9 +11,14 @@ namespace Lean
 namespace Parser
 
 namespace Module
+def moduleTk   := leading_parser "module"
 def «prelude»  := leading_parser "prelude"
-def «import»   := leading_parser "import " >> optional "runtime" >> identWithPartialTrailingDot
-def header     := leading_parser optional («prelude» >> ppLine) >> many («import» >> ppLine) >> ppLine
+def «import»   := leading_parser "import " >> identWithPartialTrailingDot
+def header     := leading_parser optional (moduleTk >> ppLine >> ppLine) >>
+  optional («prelude» >> ppLine) >>
+  many («import» >> ppLine) >>
+  ppLine
+
 /--
   Parser for a Lean module. We never actually run this parser but instead use the imperative definitions below that
   return the same syntax tree structure, but add error recovery. Still, it is helpful to have a `Parser` definition
@@ -64,7 +69,7 @@ where
       if let .original (trailing := trailing) .. := stx.getTailInfo then pure (some trailing)
         else none
 
-def parseHeader (inputCtx : InputContext) : IO (Syntax × ModuleParserState × MessageLog) := do
+def parseHeader (inputCtx : InputContext) : IO (TSyntax ``Module.header × ModuleParserState × MessageLog) := do
   let dummyEnv ← mkEmptyEnvironment
   let p   := andthenFn whitespace Module.header.fn
   let tokens := Module.updateTokens (getTokenTable dummyEnv)
@@ -73,7 +78,7 @@ def parseHeader (inputCtx : InputContext) : IO (Syntax × ModuleParserState × M
   let mut messages : MessageLog := {}
   for (pos, stk, err) in s.allErrors do
     messages := messages.add <| mkErrorMessage inputCtx pos stk err
-  pure (stx, {pos := s.pos, recovering := s.hasError}, messages)
+  pure (⟨stx⟩, {pos := s.pos, recovering := s.hasError}, messages)
 
 private def mkEOI (pos : String.Pos) : Syntax :=
   let atom := mkAtom (SourceInfo.original "".toSubstring pos "".toSubstring pos) ""

src/Lean/PrettyPrinter.lean

@@ -34,7 +34,7 @@ def ppTerm (stx : Term) : CoreM Format := ppCategory `term stx
 
 def ppUsing (e : Expr) (delab : Expr → MetaM Term) : MetaM Format := do
   let lctx := (← getLCtx).sanitizeNames.run' { options := (← getOptions) }
-  Meta.withLCtx lctx #[] do
+  Meta.withLCtx' lctx do
     ppTerm (← delab e)
 
 register_builtin_option pp.exprSizes : Bool := {
@@ -58,7 +58,7 @@ to `Elab.Info` nodes produced by the delaborator at various subexpressions of `e
 def ppExprWithInfos (e : Expr) (optsPerPos : Delaborator.OptionsPerPos := {}) (delab := Delaborator.delab)
     : MetaM FormatWithInfos := do
   let lctx := (← getLCtx).sanitizeNames.run' { options := (← getOptions) }
-  Meta.withLCtx lctx #[] do
+  Meta.withLCtx' lctx do
     let (stx, infos) ← delabCore e optsPerPos delab
     let fmt ← ppTerm stx >>= maybePrependExprSizes e
     return ⟨fmt, infos⟩

src/Lean/Server/FileWorker.lean

@@ -368,7 +368,7 @@ def setupImports
     (meta        : DocumentMeta)
     (cmdlineOpts : Options)
     (chanOut     : Std.Channel JsonRpc.Message)
-    (stx         : Syntax)
+    (stx         : TSyntax ``Parser.Module.header)
     : Language.ProcessingT IO (Except Language.Lean.HeaderProcessedSnapshot SetupImportsResult) := do
   let importsAlreadyLoaded ← importsLoadedRef.modifyGet ((·, true))
   if importsAlreadyLoaded then

src/Std/Data/HashSet/Basic.lean

@@ -283,3 +283,54 @@ end Unverified
 end HashSet
 
 end Std
+
+open Std
+
+namespace List
+
+/--
+Deduplicate an `List α`, keeping the first of each class of `==` elements.
+Uses the `Hashable α` instance for the type,
+for O(n * log n) performance for good hash hash functions.
+
+See `List.eraseDupsWithHash_eq : xs.eraseDupsWithHash = xs.eraseDups`.
+-/
+def eraseDupsWithHash [BEq α] [Hashable α] (xs : List α) : List α := Id.run do
+  let mut result := #[]
+  let mut seen : HashSet α := ∅
+  for x in xs do
+    if ¬ x ∈ seen then
+      result := result.push x
+      seen := seen.insert x
+  return result.toList
+
+def eraseDupsWithHash' [BEq α] [Hashable α] (xs : List α) (seen : HashSet α := ∅) : List α :=
+  match xs with
+  | nil => []
+  | x :: xs =>
+    if seen.contains x then
+      eraseDupsWithHash' xs seen
+    else
+      x :: eraseDupsWithHash' xs (seen.insert x)
+
+end List
+
+namespace Array
+
+/--
+Deduplicate an `Array α`, keeping the first of each class of `==` elements.
+Uses the `Hashable α` instance for the type,
+for O(n * log n) performance for good hash hash functions.
+
+See `Array.eraseDupsWithHash_eq : xs.eraseDupsWithHash = xs.eraseDups`.
+-/
+def eraseDupsWithHash [BEq α] [Hashable α] (xs : Array α) : Array α := Id.run do
+  let mut result := #[]
+  let mut seen : HashSet α := ∅
+  for x in xs do
+    if ¬ x ∈ seen then
+      result := result.push x
+      seen := seen.insert x
+  return result
+
+end Array

src/Std/Data/HashSet/Lemmas.lean

@@ -908,3 +908,42 @@ theorem getD_filter [EquivBEq α] [LawfulHashable α]
 end filter
 
 end Std.HashSet
+
+open Std
+
+namespace List
+
+theorem eraseDupsWithHash'_eq {xs : List α} {seen : HashSet α} :
+    xs.eraseDupsWithHash' seen = (xs.filter fun x => !seen.contains x).eraseDupsWithHash' := by
+  fun_induction eraseDupsWithHash'
+  case case1 =>
+    unfold eraseDupsWithHash'
+    simp
+  case case2 h ih =>
+    unfold eraseDupsWithHash'
+    simp_all [filter_cons]
+  case case3 =>
+    unfold eraseDupsWithHash'
+    simp
+
+@[simp] theorem eraseDupWithHash_nil : ([] : List α).eraseDupsWithHash = [] := by
+  simp [eraseDupsWithHash, Id.run]
+
+@[simp] theorem eraseDupsWithHash_cons {x : α} {xs : List α} :
+    (x :: xs).eraseDupsWithHash = x :: (xs.filter (· != x)).eraseDupsWithHash := by
+  simp [eraseDupsWithHash]
+
+
+theorem eraseDupsWithHash_eq {xs : List α} : xs.eraseDupsWithHash = xs.eraseDups := by
+  cases xs with
+  | nil => simp
+  | cons x xs => simp
+
+end List
+
+namespace Array
+
+theorem eraseDupsWithHash_eq {xs : Array α} : xs.eraseDupsWithHash = xs.toList.eraseDups.toArray := by
+  sorry
+
+end Array

src/Std/Data/TreeMap.lean

@@ -6,3 +6,4 @@ Authors: Paul Reichert
 prelude
 import Std.Data.TreeMap.Basic
 import Std.Data.TreeMap.AdditionalOperations
+import Std.Data.TreeMap.Raw.AdditionalOperations

src/Std/Sat/AIG/RefVecOperator/Fold.lean

@@ -15,29 +15,18 @@ namespace RefVec
 
 variable {α : Type} [Hashable α] [DecidableEq α] {aig : AIG α}
 
-structure FoldTarget (aig : AIG α) where
-  {len : Nat}
-  vec : RefVec aig len
-  func : (aig : AIG α) → BinaryInput aig → Entrypoint α
-  [lawful : LawfulOperator α BinaryInput func]
-
-attribute [instance] FoldTarget.lawful
-
-@[inline]
-def FoldTarget.mkAnd {aig : AIG α} (vec : RefVec aig w) : FoldTarget aig where
-  vec := vec
-  func := mkAndCached
-
 @[specialize]
-def fold (aig : AIG α) (target : FoldTarget aig) : Entrypoint α :=
+def fold (aig : AIG α) (vec : RefVec aig len)
+    (func : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput func] :
+    Entrypoint α :=
   let res := aig.mkConstCached true
   let aig := res.aig
   let acc := res.ref
-  let input := target.vec.cast <| by
+  let input := vec.cast <| by
     intros
     apply LawfulOperator.le_size_of_le_aig_size (f := mkConstCached)
     omega
-  go aig acc 0 target.len input target.func
+  go aig acc 0 len input func
 where
   @[specialize]
   go (aig : AIG α) (acc : Ref aig) (idx : Nat) (len : Nat) (input : RefVec aig len)
@@ -68,8 +57,10 @@ theorem fold.go_le_size {aig : AIG α} (acc : Ref aig) (idx : Nat) (s : RefVec a
   · simp
   termination_by len - idx
 
-theorem fold_le_size {aig : AIG α} (target : FoldTarget aig) :
-    aig.decls.size ≤ (fold aig target).1.decls.size := by
+theorem fold_le_size {aig : AIG α} (vec : RefVec aig len)
+    (func : (aig : AIG α) → BinaryInput aig → Entrypoint α)
+    [LawfulOperator α BinaryInput func] :
+    aig.decls.size ≤ (fold aig vec func).1.decls.size := by
   unfold fold
   dsimp only
   refine Nat.le_trans ?_ (by apply fold.go_le_size)
@@ -94,9 +85,10 @@ theorem fold.go_decl_eq {aig : AIG α} (acc : Ref aig) (i : Nat) (s : RefVec aig
     simp
 termination_by len - i
 
-theorem fold_decl_eq {aig : AIG α} (target : FoldTarget aig) :
+theorem fold_decl_eq {aig : AIG α} (vec : RefVec aig len)
+    (func : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput func] :
     ∀ idx (h1 : idx < aig.decls.size) (h2),
-      (fold aig target).1.decls[idx]'h2
+      (fold aig vec func).1.decls[idx]'h2
         =
       aig.decls[idx]'h1 := by
   intros
@@ -107,14 +99,26 @@ theorem fold_decl_eq {aig : AIG α} (target : FoldTarget aig) :
   apply LawfulOperator.lt_size_of_lt_aig_size (f := mkConstCached)
   assumption
 
-instance : LawfulOperator α FoldTarget fold where
-  le_size := by intros; apply fold_le_size
-  decl_eq := by intros; apply fold_decl_eq
+theorem fold_lt_size_of_lt_aig_size (aig : AIG α) (vec : RefVec aig len)
+    (func : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput func]
+    (h : x < aig.decls.size) :
+    x < (fold aig vec func).aig.decls.size := by
+  apply Nat.lt_of_lt_of_le
+  · exact h
+  · apply fold_le_size
+
+theorem fold_le_size_of_le_aig_size (aig : AIG α) (vec : RefVec aig len)
+    (func : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput func]
+    (h : x ≤ aig.decls.size) :
+    x ≤ (fold aig vec func).aig.decls.size := by
+  apply Nat.le_trans
+  · exact h
+  · apply fold_le_size
 
 namespace fold
 
-theorem denote_go_and {aig : AIG α} (acc : AIG.Ref aig) (curr : Nat) (hcurr : curr ≤ len)
-    (input : RefVec aig len) :
+theorem denote_go_and {aig : AIG α} (acc : AIG.Ref aig) (curr : Nat)
+    (hcurr : curr ≤ len) (input : RefVec aig len) :
     ⟦
       (go aig acc curr len input mkAndCached).aig,
       (go aig acc curr len input mkAndCached).ref,
@@ -168,11 +172,10 @@ end fold
 
 @[simp]
 theorem denote_fold_and {aig : AIG α} (s : RefVec aig len) :
-    ⟦(fold aig (FoldTarget.mkAnd s)), assign⟧
+    ⟦(fold aig s AIG.mkAndCached), assign⟧
       ↔
     (∀ (idx : Nat) (hidx : idx < len), ⟦aig, s.get idx hidx, assign⟧) := by
   unfold fold
-  simp only [FoldTarget.mkAnd]
   rw [fold.denote_go_and]
   · simp only [denote_projected_entry, mkConstCached_eval_eq_mkConst_eval, denote_mkConst,
     Nat.zero_le, get_cast, Ref.cast_eq, true_implies, true_and]

src/Std/Sat/AIG/RefVecOperator/Zip.lean

@@ -70,18 +70,12 @@ instance : LawfulZipOperator α mkImpCached where
 
 end LawfulZipOperator
 
-structure ZipTarget (aig : AIG α) (len : Nat) where
-  input : BinaryRefVec aig len
-  func : (aig : AIG α) → BinaryInput aig → Entrypoint α
-  [lawful : LawfulOperator α BinaryInput func]
-  [chainable : LawfulZipOperator α func]
-
-attribute [instance] ZipTarget.lawful
-attribute [instance] ZipTarget.chainable
-
 @[specialize]
-def zip (aig : AIG α) (target : ZipTarget aig len) : RefVecEntry α len :=
-  go aig 0 (.emptyWithCapacity len) (by omega) target.input.lhs target.input.rhs target.func
+def zip (aig : AIG α) (input : BinaryRefVec aig len)
+    (func : (aig : AIG α) → BinaryInput aig → Entrypoint α)
+    [LawfulOperator α BinaryInput func] [LawfulZipOperator α func] :
+    RefVecEntry α len :=
+  go aig 0 (.emptyWithCapacity len) (by omega) input.lhs input.rhs func
 where
   @[specialize]
   go (aig : AIG α) (idx : Nat) (s : RefVec aig idx) (hidx : idx ≤ len)
@@ -107,7 +101,7 @@ where
 theorem zip.go_le_size {aig : AIG α} (idx : Nat) (hidx) (s : RefVec aig idx)
     (lhs rhs : RefVec aig len)
     (f : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput f]
-    [chainable : LawfulZipOperator α f] :
+    [LawfulZipOperator α f] :
     aig.decls.size ≤ (go aig idx s hidx lhs rhs f).1.decls.size := by
   unfold go
   split
@@ -117,14 +111,16 @@ theorem zip.go_le_size {aig : AIG α} (idx : Nat) (hidx) (s : RefVec aig idx)
   · simp
   termination_by len - idx
 
-theorem zip_le_size {aig : AIG α} (target : ZipTarget aig len) :
-    aig.decls.size ≤ (zip aig target).1.decls.size := by
+theorem zip_le_size (aig : AIG α) (input : BinaryRefVec aig len)
+    (func : (aig : AIG α) → BinaryInput aig → Entrypoint α)
+    [LawfulOperator α BinaryInput func] [LawfulZipOperator α func] :
+    aig.decls.size ≤ (zip aig input func).1.decls.size := by
   unfold zip
   apply zip.go_le_size
 
 theorem zip.go_decl_eq {aig : AIG α} (i) (hi) (lhs rhs : RefVec aig len)
     (s : RefVec aig i) (f : (aig : AIG α) → BinaryInput aig → Entrypoint α)
-    [LawfulOperator α BinaryInput f] [chainable : LawfulZipOperator α f] :
+    [LawfulOperator α BinaryInput f] [LawfulZipOperator α f] :
     ∀ (idx : Nat) (h1) (h2), (go aig i s hi lhs rhs f).1.decls[idx]'h2 = aig.decls[idx]'h1 := by
   generalize hgo : go aig i s hi lhs rhs f = res
   unfold go at hgo
@@ -143,22 +139,48 @@ theorem zip.go_decl_eq {aig : AIG α} (i) (hi) (lhs rhs : RefVec aig len)
     simp
 termination_by len - i
 
-theorem zip_decl_eq {aig : AIG α} (target : ZipTarget aig len) :
+theorem zip_decl_eq {aig : AIG α} (input : BinaryRefVec aig len)
+    (func : (aig : AIG α) → BinaryInput aig → Entrypoint α)
+    [LawfulOperator α BinaryInput func] [LawfulZipOperator α func] :
     ∀ idx (h1 : idx < aig.decls.size) (h2),
-      (zip aig target).1.decls[idx]'h2 = aig.decls[idx]'h1 := by
+      (zip aig input func).1.decls[idx]'h2 = aig.decls[idx]'h1 := by
   intros
   unfold zip
   apply zip.go_decl_eq
 
-instance : LawfulVecOperator α ZipTarget zip where
-  le_size := by intros; apply zip_le_size
-  decl_eq := by intros; apply zip_decl_eq
+theorem zip_lt_size_of_lt_aig_size (aig : AIG α) (input : BinaryRefVec aig len)
+    (func : (aig : AIG α) → BinaryInput aig → Entrypoint α)
+    [LawfulOperator α BinaryInput func] [LawfulZipOperator α func] (h : x < aig.decls.size) :
+    x < (zip aig input func).aig.decls.size := by
+  apply Nat.lt_of_lt_of_le
+  · exact h
+  · apply zip_le_size
+
+theorem zip_le_size_of_le_aig_size (aig : AIG α) (input : BinaryRefVec aig len)
+    (func : (aig : AIG α) → BinaryInput aig → Entrypoint α)
+    [LawfulOperator α BinaryInput func] [LawfulZipOperator α func] (h : x ≤ aig.decls.size) :
+    x ≤ (zip aig input func).aig.decls.size := by
+  apply Nat.le_trans
+  · exact h
+  · apply zip_le_size
+
+theorem IsPrefix_zip {aig : AIG α} (input : BinaryRefVec aig len)
+    (func : (aig : AIG α) → BinaryInput aig → Entrypoint α)
+    [LawfulOperator α BinaryInput func] [LawfulZipOperator α func] :
+    AIG.IsPrefix aig.decls (zip aig input func).aig.decls := by
+  intros
+  unfold zip
+  apply IsPrefix.of
+  · intros
+    apply zip_decl_eq
+  · intros
+    apply zip_le_size
 
 namespace zip
 
 theorem go_get_aux {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefVec aig curr)
     (lhs rhs : RefVec aig len) (f : (aig : AIG α) → BinaryInput aig → Entrypoint α)
-    [LawfulOperator α BinaryInput f] [chainable : LawfulZipOperator α f] :
+    [LawfulOperator α BinaryInput f] [LawfulZipOperator α f] :
     -- The hfoo here is a trick to make the dependent type gods happy
     ∀ (idx : Nat) (hidx : idx < curr) (hfoo),
       (go aig curr s hcurr lhs rhs f).vec.get idx (by omega)
@@ -188,7 +210,7 @@ termination_by len - curr
 
 theorem go_get {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefVec aig curr)
     (lhs rhs : RefVec aig len) (f : (aig : AIG α) → BinaryInput aig → Entrypoint α)
-    [LawfulOperator α BinaryInput f] [chainable : LawfulZipOperator α f] :
+    [LawfulOperator α BinaryInput f] [LawfulZipOperator α f] :
     ∀ (idx : Nat) (hidx : idx < curr),
       (go aig curr s hcurr lhs rhs f).vec.get idx (by omega)
         =
@@ -199,7 +221,7 @@ theorem go_get {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefVec ai
 theorem go_denote_mem_prefix {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len)
     (s : RefVec aig curr) (lhs rhs : RefVec aig len)
     (f : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput f]
-    [chainable : LawfulZipOperator α f] (start : Nat) (hstart) :
+    [LawfulZipOperator α f] (start : Nat) (hstart) :
     ⟦
       (go aig curr s hcurr lhs rhs f).aig,
       ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
@@ -217,7 +239,7 @@ theorem go_denote_mem_prefix {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len)
 attribute [local simp] LawfulZipOperator.denote_prefix_cast_ref in
 theorem denote_go {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefVec aig curr)
     (lhs rhs : RefVec aig len) (f : (aig : AIG α) → BinaryInput aig → Entrypoint α)
-    [LawfulOperator α BinaryInput f] [chainable : LawfulZipOperator α f] :
+    [LawfulOperator α BinaryInput f] [LawfulZipOperator α f] :
     ∀ (idx : Nat) (hidx1 : idx < len),
       curr ≤ idx
         →
@@ -254,11 +276,13 @@ termination_by len - curr
 end zip
 
 @[simp]
-theorem denote_zip {aig : AIG α} (target : ZipTarget aig len) :
+theorem denote_zip {aig : AIG α} (input : BinaryRefVec aig len)
+    (func : (aig : AIG α) → BinaryInput aig → Entrypoint α)
+    [LawfulOperator α BinaryInput func] [LawfulZipOperator α func] :
     ∀ (idx : Nat) (hidx : idx < len),
-      ⟦(zip aig target).aig, (zip aig target).vec.get idx hidx, assign⟧
+      ⟦(zip aig input func).aig, (zip aig input func).vec.get idx hidx, assign⟧
         =
-      ⟦target.func aig ⟨target.input.lhs.get idx hidx, target.input.rhs.get idx hidx⟩, assign⟧ := by
+      ⟦func aig ⟨input.lhs.get idx hidx, input.rhs.get idx hidx⟩, assign⟧ := by
   intros
   apply zip.denote_go
   omega

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean

@@ -139,26 +139,26 @@ where
         omega
       match op with
       | .and =>
-         let res := AIG.RefVec.zip aig ⟨⟨lhs, rhs⟩, AIG.mkAndCached⟩
+         let res := AIG.RefVec.zip aig ⟨lhs, rhs⟩ AIG.mkAndCached
          have := by
-           apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := AIG.RefVec.zip)
+           apply AIG.RefVec.zip_le_size_of_le_aig_size
            dsimp only at hlaig hraig
            omega
-         ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := AIG.RefVec.zip) ..)⟩
+         ⟨⟨res, this⟩, cache.cast (AIG.RefVec.zip_le_size ..)⟩
       | .or =>
-         let res := AIG.RefVec.zip aig ⟨⟨lhs, rhs⟩, AIG.mkOrCached⟩
+         let res := AIG.RefVec.zip aig ⟨lhs, rhs⟩ AIG.mkOrCached
          have := by
-           apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := AIG.RefVec.zip)
+           apply AIG.RefVec.zip_le_size_of_le_aig_size
            dsimp only at hlaig hraig
            omega
-         ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := AIG.RefVec.zip) ..)⟩
+         ⟨⟨res, this⟩, cache.cast (AIG.RefVec.zip_le_size ..)⟩
       | .xor =>
-         let res := AIG.RefVec.zip aig ⟨⟨lhs, rhs⟩, AIG.mkXorCached⟩
+         let res := AIG.RefVec.zip aig ⟨lhs, rhs⟩ AIG.mkXorCached
          have := by
-           apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := AIG.RefVec.zip)
+           apply AIG.RefVec.zip_le_size_of_le_aig_size
            dsimp only at hlaig hraig
            omega
-         ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := AIG.RefVec.zip) ..)⟩
+         ⟨⟨res, this⟩, cache.cast (AIG.RefVec.zip_le_size ..)⟩
       | .add =>
         let res := bitblast.blastAdd aig ⟨lhs, rhs⟩
         have := by
@@ -310,10 +310,17 @@ theorem go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) :
   · rw [AIG.LawfulVecOperator.decl_eq (f := blastVar)]
   · rw [AIG.LawfulVecOperator.decl_eq (f := blastConst)]
   · next op lhsExpr rhsExpr =>
+    have hl := (goCache aig lhsExpr cache).result.property
+    have hr := (goCache (goCache aig lhsExpr cache).1.1.aig rhsExpr (goCache aig lhsExpr cache).cache).result.property
     match op with
-    | .and | .or | .xor | .add | .mul | .udiv | .umod =>
-      have hl := (goCache aig lhsExpr cache).result.property
-      have hr := (goCache (goCache aig lhsExpr cache).1.1.aig rhsExpr (goCache aig lhsExpr cache).cache).result.property
+    | .and | .or | .xor =>
+      rw [AIG.RefVec.zip_decl_eq]
+      rw [goCache_decl_eq, goCache_decl_eq]
+      · omega
+      · apply Nat.lt_of_lt_of_le
+        · exact h1
+        · apply Nat.le_trans <;> assumption
+    | .add | .mul | .udiv | .umod =>
       rw [AIG.LawfulVecOperator.decl_eq]
       rw [goCache_decl_eq, goCache_decl_eq]
       · omega

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Eq.lean

@@ -21,25 +21,25 @@ namespace BVPred
 variable [Hashable α] [DecidableEq α]
 
 def mkEq (aig : AIG α) (pair : AIG.BinaryRefVec aig w) : AIG.Entrypoint α :=
-  let res := AIG.RefVec.zip aig ⟨pair, AIG.mkBEqCached⟩
+  let res := AIG.RefVec.zip aig pair AIG.mkBEqCached
   let aig := res.aig
   let bits := res.vec
-  AIG.RefVec.fold aig (.mkAnd bits)
+  AIG.RefVec.fold aig bits AIG.mkAndCached
 
 instance {w : Nat} : AIG.LawfulOperator α (AIG.BinaryRefVec · w) mkEq where
   le_size := by
     intros
     unfold mkEq
     dsimp only
-    apply AIG.LawfulOperator.le_size_of_le_aig_size (f := AIG.RefVec.fold)
-    apply AIG.LawfulVecOperator.le_size (f := AIG.RefVec.zip)
+    apply AIG.RefVec.fold_le_size_of_le_aig_size
+    apply AIG.RefVec.zip_le_size
   decl_eq := by
     intros
     unfold mkEq
     dsimp only
-    rw [AIG.LawfulOperator.decl_eq (f := AIG.RefVec.fold)]
-    rw [AIG.LawfulVecOperator.decl_eq (f := AIG.RefVec.zip)]
-    apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := AIG.RefVec.zip)
+    rw [AIG.RefVec.fold_decl_eq]
+    rw [AIG.RefVec.zip_decl_eq]
+    apply AIG.RefVec.zip_lt_size_of_lt_aig_size
     assumption
 
 end BVPred

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean

@@ -196,11 +196,20 @@ theorem go_Inv_of_Inv (cache : Cache aig) (hinv : Cache.Inv assign aig cache) :
     apply Cache.Inv_cast
     · apply LawfulVecOperator.isPrefix_aig (f := blastConst)
     · exact hinv
-  · dsimp only at hres
-    split at hres
-    all_goals
+  · next op lhsExpr rhsExpr =>
+    dsimp only at hres
+    match op with
+    | .and | .or | .xor =>
+      dsimp only at hres
+      rw [← hres]
+      apply Cache.Inv_cast
+      · apply RefVec.IsPrefix_zip
+      · apply goCache_Inv_of_Inv
+        apply goCache_Inv_of_Inv
+        exact hinv
+    | .add | .mul | .udiv | .umod =>
+      dsimp only at hres
       rw [← hres]
-      dsimp only
       apply Cache.Inv_cast
       · apply LawfulVecOperator.isPrefix_aig
       · apply goCache_Inv_of_Inv

src/lake/Lake/Build/Imports.lean

@@ -33,7 +33,7 @@ def buildImportsAndDeps
     let precompileImports ← (← computePrecompileImportsAux leanFile imports).await
     let pkgs := precompileImports.foldl (·.insert ·.pkg) OrdPackageSet.empty |>.toArray
     let externLibsJob ← fetchExternLibs pkgs
-    let impLibsJob ← fetchImportLibs imports
+    let impLibsJob ← fetchImportLibs precompileImports
     let dynlibsJob ← root.dynlibs.fetchIn root
     let pluginsJob ← root.plugins.fetchIn root
     modJob.bindM fun _ =>

src/lake/Lake/Build/Module.lean

@@ -35,8 +35,8 @@ building an `Array` product of its direct local imports.
 -/
 def Module.recParseImports (mod : Module) : FetchM (Job (Array Module)) := Job.async do
   let contents ← IO.FS.readFile mod.leanFile
-  let imports ← Lean.parseImports' contents mod.leanFile.toString
-  let mods ← imports.foldlM (init := OrdModuleSet.empty) fun set imp =>
+  let res ← Lean.parseImports' contents mod.leanFile.toString
+  let mods ← res.imports.foldlM (init := OrdModuleSet.empty) fun set imp =>
     findModule? imp.module <&> fun | some mod => set.insert mod | none => set
   return mods.toArray
 
@@ -208,8 +208,15 @@ def Module.recBuildDeps (mod : Module) : FetchM (Job ModuleDeps) := ensureJob do
       logError s!"{mod.leanFile}: module imports itself"
     imp.olean.fetch
   let importJob := Job.mixArray importJobs "import oleans"
+  /-
+  Remark: It should be possible to avoid transitive imports here when the module
+  itself is precompiled, but they are currently kept to perserve the "bad import" errors.
+  -/
+  let precompileImports ← if mod.shouldPrecompile then
+    mod.transImports.fetch else mod.precompileImports.fetch
+  let precompileImports ← precompileImports.await
   let impLibsJob ← Job.collectArray (traceCaption := "import dynlibs") <$>
-    mod.fetchImportLibs directImports mod.shouldPrecompile
+    mod.fetchImportLibs precompileImports mod.shouldPrecompile
   let externLibsJob ← Job.collectArray (traceCaption := "package external libraries") <$>
     mod.pkg.externLibs.mapM (·.dynlib.fetch)
   let dynlibsJob ← mod.dynlibs.fetchIn mod.pkg "module dynlibs"

src/lake/Lake/CLI/Main.lean

@@ -539,11 +539,11 @@ private def evalLeanFile
     | error s!"file not found: {leanFile}"
   let spawnArgs ← id do
     if let some mod := ws.findModuleBySrc? path then
-      let deps ← ws.runBuild mod.deps.fetch buildConfig
+      let deps ← ws.runBuild (withRegisterJob s!"setup ({mod.name})" do mod.deps.fetch) buildConfig
       return mkSpawnArgs ws path deps (some mod.rootDir) mod.leanArgs
     else
-      let imports ← Lean.parseImports' (← IO.FS.readFile path) leanFile.toString
-      let imports := imports.filterMap (ws.findModule? ·.module)
+      let res ← Lean.parseImports' (← IO.FS.readFile path) leanFile.toString
+      let imports := res.imports.filterMap (ws.findModule? ·.module)
       let deps ← ws.runBuild (buildImportsAndDeps leanFile imports) buildConfig
       return mkSpawnArgs ws path deps none ws.root.moreLeanArgs
   logVerbose (mkCmdLog spawnArgs)

src/lake/Lake/CLI/Serve.lean

@@ -62,7 +62,7 @@ def setupFile
     let some ws ← loadWorkspace loadConfig |>.toBaseIO buildConfig.outLv buildConfig.ansiMode
       | error "failed to load workspace"
     if let some mod := ws.findModuleBySrc? path then
-      let deps ← ws.runBuild mod.deps.fetch buildConfig
+      let deps ← ws.runBuild (withRegisterJob s!"setup ({mod.name})" do mod.deps.fetch) buildConfig
       let opts := mod.serverOptions.foldl (init := {}) fun opts opt =>
         opts.insert opt.name opt.value
       let info : FileSetupInfo := {

src/lake/Lake/Load/Lean/Elab.lean

@@ -35,13 +35,13 @@ def importModulesUsingCache (imports : Array Import) (opts : Options) (trustLeve
   return env
 
 /-- Like `Lean.Elab.processHeader`, but using `importEnvCache`. -/
-def processHeader (header : Syntax) (opts : Options)
+def processHeader (header : TSyntax ``Parser.Module.header) (opts : Options)
 (inputCtx : Parser.InputContext) : StateT MessageLog IO Environment := do
   try
     let imports := Elab.headerToImports header
     importModulesUsingCache imports opts 1024
   catch e =>
-    let pos := inputCtx.fileMap.toPosition <| header.getPos?.getD 0
+    let pos := inputCtx.fileMap.toPosition <| header.raw.getPos?.getD 0
     modify (·.add { fileName := inputCtx.fileName, data := toString e, pos })
     mkEmptyEnvironment
 

src/lake/tests/badImport/test.sh

@@ -14,13 +14,16 @@ source ../common.sh
 test_err "Building Etc" build Lib.U Etc
 # Test importing a missing module from outside the workspace
 test_err "U.lean:2:0: unknown module prefix 'Bogus'" build +Lib.U
-test_run setup-file . Bogus # Lake ignores the file (the server will error)
+test_err "U.lean:2:0: error: unknown module prefix 'Bogus'" lean ./Lib/U.lean
+test_run setup-file ./Lib/U.lean # Lake ignores the unknown import (the server will error)
 # Test importing onself
 test_err "S.lean: module imports itself" build +Lib.S
-test_err "S.lean: module imports itself" setup-file ./Lib/S.lean Lib.S
+test_err "S.lean: module imports itself" lean ./Lib/S.lean
+test_err "S.lean: module imports itself" setup-file ./Lib/S.lean
 # Test importing a missing module from within the workspace
 test_err "B.lean: bad import 'Lib.Bogus'" build +Lib.B
-test_err "B.lean: bad import 'Lib.Bogus'" setup-file ./Lib/B.lean Lib.Bogus
+test_err "B.lean: bad import 'Lib.Bogus'" lean ./Lib/B.lean
+test_err "B.lean: bad import 'Lib.Bogus'" setup-file ./Lib/B.lean
 # Test a vanishing import within the workspace (lean4#3551)
 echo "[Test: Vanishing Import]"
 set -x
@@ -29,10 +32,12 @@ $LAKE build +Lib.B
 rm Lib/Bogus.lean
 set +x
 test_err "B.lean: bad import 'Lib.Bogus'" build +Lib.B
-test_err "B.lean: bad import 'Lib.Bogus'" setup-file . Lib.B
+test_err "B.lean: bad import 'Lib.Bogus'" lean ./Lib/B.lean
+test_err "B.lean: bad import 'Lib.Bogus'" setup-file ./Lib/B.lean
 # Test a module which imports a module containing a bad import
 test_err "B1.lean: bad import 'Lib.B'" build +Lib.B1
-test_err "B1.lean: bad import 'Lib.B'" setup-file ./Lib/B1.lean Lib.B
+test_err "B1.lean: bad import 'Lib.B'" lean ./Lib/B1.lean
+test_err "B1.lean: bad import 'Lib.B'" setup-file ./Lib/B1.lean
 # Test an executable with a bad import does not kill the whole build
 test_err "Building Etc" build X Etc
 # Test an executable which imports a missing module from within the workspace

src/lake/tests/common.sh

@@ -72,6 +72,8 @@ test_err() {
       echo "Lake unexpectedly succeeded."
       return 1
     fi
+  else
+    return 1
   fi
 }
 

src/lake/tests/precompileLink/Downstream.lean

@@ -0,0 +1,3 @@
+import Downstream.Import
+
+#eval greetingRef.get

src/lake/tests/precompileLink/Downstream/Import.lean

@@ -0,0 +1 @@
+import Foo

src/lake/tests/precompileLink/Foo/Baz.lean

@@ -1,3 +1,3 @@
 import FooDep
 
-initialize greetingRef : IO.Ref String ← IO.mkRef greeting
+builtin_initialize greetingRef : IO.Ref String ← IO.mkRef greeting

src/lake/tests/precompileLink/Indirect.lean

@@ -0,0 +1 @@
+import Foo

src/lake/tests/precompileLink/lakefile.lean

@@ -12,3 +12,5 @@ lean_lib Foo where
 lean_lib FooDep
 lean_lib FooDepDep
 lean_exe orderTest
+
+lean_lib Downstream

src/lake/tests/precompileLink/test.sh

@@ -7,6 +7,11 @@ source ../common.sh
 # https://github.com/leanprover/lean4/issues/7790
 test_run -v exe orderTest
 
+# Test that transitively importing a precompiled module
+# from a non-precompiled module works
+test_not_out '"pluginPaths":[]' -v setup-file bogus Downstream
+test_run -v build Downstream
+
 # Test that `moreLinkArgs` are included when linking precompiled modules
 ./clean.sh
 test_maybe_err "-lBogus" build -KlinkArgs=-lBogus

src/library/compiler/llvm.cpp

@@ -26,8 +26,8 @@ Lean's IR.
 #include "llvm-c/Target.h"
 #include "llvm-c/TargetMachine.h"
 #include "llvm-c/Types.h"
-#include "llvm-c/Transforms/PassBuilder.h"
-#include "llvm-c/Transforms/PassManagerBuilder.h"
+//#include "llvm-c/Transforms/PassBuilder.h"
+//#include "llvm-c/Transforms/PassManagerBuilder.h"
 #endif
 
 // This is mostly boilerplate, suppress warnings
@@ -135,6 +135,8 @@ static inline LLVMBasicBlockRef lean_to_BasicBlock(size_t s) {
     return reinterpret_cast<LLVMBasicBlockRef>(s);
 }
 
+/* TODO: update to new pass manager
+
 // == LLVM <-> Lean: PassManagerRef ==
 static inline size_t PassManager_to_lean(LLVMPassManagerRef s) {
     return reinterpret_cast<size_t>(s);
@@ -152,6 +154,7 @@ static inline size_t PassManagerBuilder_to_lean(LLVMPassManagerBuilderRef s) {
 static inline LLVMPassManagerBuilderRef lean_to_PassManagerBuilder(size_t s) {
     return reinterpret_cast<LLVMPassManagerBuilderRef>(s);
 }
+*/
 
 // == LLVM <-> Lean: AttributeRef ==
 static inline size_t Attribute_to_lean(LLVMAttributeRef s) {
@@ -1184,90 +1187,90 @@ extern "C" LEAN_EXPORT lean_object *lean_llvm_target_machine_emit_to_file(size_t
 #endif  // LEAN_LLVM
 }
 
-extern "C" LEAN_EXPORT lean_object *lean_llvm_create_pass_manager(size_t ctx,
-    lean_object * /* w */) {
-#ifndef LEAN_LLVM
-    lean_always_assert(
-        false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
-                  "the LLVM backend function."));
-#else
-    return lean_io_result_mk_ok(lean_box_usize(PassManager_to_lean(LLVMCreatePassManager())));
-#endif  // LEAN_LLVM
-}
-
-extern "C" LEAN_EXPORT lean_object *lean_llvm_run_pass_manager(size_t ctx, size_t pm, size_t mod,
-    lean_object * /* w */) {
-#ifndef LEAN_LLVM
-    lean_always_assert(
-        false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
-                  "the LLVM backend function."));
-#else
-    int is_error = LLVMRunPassManager(lean_to_PassManager(pm), lean_to_Module(mod));
-    return lean_io_result_mk_ok(lean_box(0));
-#endif  // LEAN_LLVM
-}
-
-extern "C" LEAN_EXPORT lean_object *lean_llvm_dispose_pass_manager(size_t ctx, size_t pm,
-    lean_object * /* w */) {
-#ifndef LEAN_LLVM
-    lean_always_assert(
-        false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
-                  "the LLVM backend function."));
-#else
-    LLVMDisposePassManager(lean_to_PassManager(pm));
-    return lean_io_result_mk_ok(lean_box(0));
-#endif  // LEAN_LLVM
-}
-
-extern "C" LEAN_EXPORT lean_object *lean_llvm_create_pass_manager_builder(size_t ctx,
-    lean_object * /* w */) {
-#ifndef LEAN_LLVM
-    lean_always_assert(
-        false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
-                  "the LLVM backend function."));
-#else
-    return lean_io_result_mk_ok(lean_box_usize(PassManagerBuilder_to_lean(LLVMPassManagerBuilderCreate())));
-#endif  // LEAN_LLVM
-}
-
-
-extern "C" LEAN_EXPORT lean_object *lean_llvm_dispose_pass_manager_builder(size_t ctx, size_t pmb,
-    lean_object * /* w */) {
-#ifndef LEAN_LLVM
-    lean_always_assert(
-        false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
-                  "the LLVM backend function."));
-#else
-    LLVMPassManagerBuilderDispose(lean_to_PassManagerBuilder(pmb));
-    return lean_io_result_mk_ok(lean_box(0));
-#endif  // LEAN_LLVM
-}
-
-
-extern "C" LEAN_EXPORT lean_object *lean_llvm_pass_manager_builder_set_opt_level(size_t ctx, size_t pmb, unsigned opt_level,
-    lean_object * /* w */) {
-#ifndef LEAN_LLVM
-    lean_always_assert(
-        false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
-                  "the LLVM backend function."));
-#else
-    LLVMPassManagerBuilderSetOptLevel(lean_to_PassManagerBuilder(pmb), opt_level);
-    return lean_io_result_mk_ok(lean_box(0));
-#endif  // LEAN_LLVM
-}
-
-
-extern "C" LEAN_EXPORT lean_object *lean_llvm_pass_manager_builder_populate_module_pass_manager(size_t ctx, size_t pmb, size_t pm,
-    lean_object * /* w */) {
-#ifndef LEAN_LLVM
-    lean_always_assert(
-        false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
-                  "the LLVM backend function."));
-#else
-    LLVMPassManagerBuilderPopulateModulePassManager(lean_to_PassManagerBuilder(pmb), lean_to_PassManager(pm));
-    return lean_io_result_mk_ok(lean_box(0));
-#endif  // LEAN_LLVM
-}
+//extern "C" LEAN_EXPORT lean_object *lean_llvm_create_pass_manager(size_t ctx,
+//    lean_object * /* w */) {
+//#ifndef LEAN_LLVM
+//    lean_always_assert(
+//        false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
+//                  "the LLVM backend function."));
+//#else
+//    return lean_io_result_mk_ok(lean_box_usize(PassManager_to_lean(LLVMCreatePassManager())));
+//#endif  // LEAN_LLVM
+//}
+//
+//extern "C" LEAN_EXPORT lean_object *lean_llvm_run_pass_manager(size_t ctx, size_t pm, size_t mod,
+//    lean_object * /* w */) {
+//#ifndef LEAN_LLVM
+//    lean_always_assert(
+//        false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
+//                  "the LLVM backend function."));
+//#else
+//    int is_error = LLVMRunPassManager(lean_to_PassManager(pm), lean_to_Module(mod));
+//    return lean_io_result_mk_ok(lean_box(0));
+//#endif  // LEAN_LLVM
+//}
+//
+//extern "C" LEAN_EXPORT lean_object *lean_llvm_dispose_pass_manager(size_t ctx, size_t pm,
+//    lean_object * /* w */) {
+//#ifndef LEAN_LLVM
+//    lean_always_assert(
+//        false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
+//                  "the LLVM backend function."));
+//#else
+//    LLVMDisposePassManager(lean_to_PassManager(pm));
+//    return lean_io_result_mk_ok(lean_box(0));
+//#endif  // LEAN_LLVM
+//}
+//
+//extern "C" LEAN_EXPORT lean_object *lean_llvm_create_pass_manager_builder(size_t ctx,
+//    lean_object * /* w */) {
+//#ifndef LEAN_LLVM
+//    lean_always_assert(
+//        false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
+//                  "the LLVM backend function."));
+//#else
+//    return lean_io_result_mk_ok(lean_box_usize(PassManagerBuilder_to_lean(LLVMPassManagerBuilderCreate())));
+//#endif  // LEAN_LLVM
+//}
+//
+//
+//extern "C" LEAN_EXPORT lean_object *lean_llvm_dispose_pass_manager_builder(size_t ctx, size_t pmb,
+//    lean_object * /* w */) {
+//#ifndef LEAN_LLVM
+//    lean_always_assert(
+//        false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
+//                  "the LLVM backend function."));
+//#else
+//    LLVMPassManagerBuilderDispose(lean_to_PassManagerBuilder(pmb));
+//    return lean_io_result_mk_ok(lean_box(0));
+//#endif  // LEAN_LLVM
+//}
+//
+//
+//extern "C" LEAN_EXPORT lean_object *lean_llvm_pass_manager_builder_set_opt_level(size_t ctx, size_t pmb, unsigned opt_level,
+//    lean_object * /* w */) {
+//#ifndef LEAN_LLVM
+//    lean_always_assert(
+//        false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
+//                  "the LLVM backend function."));
+//#else
+//    LLVMPassManagerBuilderSetOptLevel(lean_to_PassManagerBuilder(pmb), opt_level);
+//    return lean_io_result_mk_ok(lean_box(0));
+//#endif  // LEAN_LLVM
+//}
+//
+//
+//extern "C" LEAN_EXPORT lean_object *lean_llvm_pass_manager_builder_populate_module_pass_manager(size_t ctx, size_t pmb, size_t pm,
+//    lean_object * /* w */) {
+//#ifndef LEAN_LLVM
+//    lean_always_assert(
+//        false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
+//                  "the LLVM backend function."));
+//#else
+//    LLVMPassManagerBuilderPopulateModulePassManager(lean_to_PassManagerBuilder(pmb), lean_to_PassManager(pm));
+//    return lean_io_result_mk_ok(lean_box(0));
+//#endif  // LEAN_LLVM
+//}
 
 extern "C" LEAN_EXPORT lean_object *lean_llvm_dispose_target_machine(size_t ctx, size_t tm,
     lean_object * /* w */) {

src/shell/CMakeLists.txt

@@ -185,12 +185,11 @@ ENDFOREACH(T)
 # bootstrap: too slow
 # toolchain: requires elan to download toolchain
 # online: downloads remote repositories
-# badImport/buildArgs: flaky for unknown reasons
 file(GLOB_RECURSE LEANLAKETESTS
   #"${LEAN_SOURCE_DIR}/lake/tests/test.sh"
   "${LEAN_SOURCE_DIR}/lake/examples/test.sh")
 FOREACH(T ${LEANLAKETESTS})
-  if(NOT T MATCHES ".*(lake-packages|bootstrap|toolchain|online|buildArgs|badImport).*")
+  if(NOT T MATCHES ".*(lake-packages|bootstrap|toolchain|online).*")
     GET_FILENAME_COMPONENT(T_DIR ${T} DIRECTORY)
     GET_FILENAME_COMPONENT(DIR_NAME ${T_DIR} NAME)
     add_test(NAME "leanlaketest_${DIR_NAME}"