fix: realizer for matcher equation theorems

"alteration pattern" -> "alternation pattern"

.github/workflows/ci.yml

@@ -62,7 +62,7 @@ jobs:
                 "os": "ubuntu-latest",
                 "release": false,
                 "quick": false,
-                "shell": "nix-shell --arg pkgsDist \"import (fetchTarball \\\"channel:nixos-19.03\\\") {{}}\" --run \"bash -euxo pipefail {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",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
                 "binary-check": "ldd -v",
@@ -76,7 +76,7 @@ jobs:
                 "os": "ubuntu-latest",
                 "release": true,
                 "quick": true,
-                "shell": "nix-shell --arg pkgsDist \"import (fetchTarball \\\"channel:nixos-19.03\\\") {{}}\" --run \"bash -euxo pipefail {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",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
                 "binary-check": "ldd -v",
@@ -154,7 +154,7 @@ jobs:
                 "quick": false,
                 "cross": true,
                 "cross_target": "aarch64-unknown-linux-gnu",
-                "shell": "nix-shell --arg pkgsDist \"import (fetchTarball \\\"channel:nixos-19.03\\\") {{ localSystem.config = \\\"aarch64-unknown-linux-gnu\\\"; }}\" --run \"bash -euxo pipefail {0}\"",
+                "shell": "nix develop .#oldGlibcAArch -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 https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm-aarch64-* lean-llvm-x86_64-*"
               },
@@ -252,7 +252,7 @@ jobs:
     runs-on: ${{ matrix.os }}
     defaults:
       run:
-        shell: ${{ matrix.shell || 'nix-shell --run "bash -euxo pipefail {0}"' }}
+        shell: ${{ matrix.shell || 'nix develop -c bash -euxo pipefail {0}' }}
     name: ${{ matrix.name }}
     env:
       # must be inside workspace
@@ -383,8 +383,14 @@ jobs:
           cd build/stage1
           ulimit -c unlimited # coredumps
           # exclude nonreproducible test
-          ctest -j4 --output-on-failure ${{ matrix.CTEST_OPTIONS }} < /dev/null
+          ctest -j4 --progress --output-junit test-results.xml --output-on-failure ${{ matrix.CTEST_OPTIONS }} < /dev/null
         if: (matrix.wasm || !matrix.cross) && needs.configure.outputs.quick == 'false'
+      - name: Test Summary
+        uses: test-summary/action@v2
+        with:
+          paths: build/stage1/test-results.xml
+        # prefix `if` above with `always` so it's run even if tests failed
+        if: always() && (matrix.wasm || !matrix.cross) && needs.configure.outputs.quick == 'false'
       - name: Check Test Binary
         run: ${{ matrix.binary-check }} tests/compiler/534.lean.out
         if: ${{ !matrix.cross && needs.configure.outputs.quick == 'false' }}

.github/workflows/nix-ci.yml

@@ -77,7 +77,13 @@ jobs:
           nix build $NIX_BUILD_ARGS .#cacheRoots -o push-build
       - name: Test
         run: |
-          nix build $NIX_BUILD_ARGS .#test -o push-test
+          nix build --keep-failed $NIX_BUILD_ARGS .#test -o push-test || (ln -s /tmp/nix-build-*/source/src/build/ ./push-test; false)
+      - name: Test Summary
+        uses: test-summary/action@v2
+        with:
+          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,test,inked} -o push-doc

.github/workflows/pr-release.yml

@@ -126,24 +126,22 @@ jobs:
           if [ "$NIGHTLY_SHA" = "$MERGE_BASE_SHA" ]; then
             echo "The merge base of this PR coincides with the nightly release"
 
+            STD_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover/std4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
             MATHLIB_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/mathlib4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
 
-            if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then
-              echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
+            if [[ -n "$STD_REMOTE_TAGS" ]]; then
+              echo "... and Std has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
+              MESSAGE=""
 
-              STD_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover/std4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
-
-              if [[ -n "$STD_REMOTE_TAGS" ]]; then
-                echo "... and Std has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
-                MESSAGE=""
+              if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then
+                echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."    
               else
-                echo "... but Std does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
-                MESSAGE="- ❗ Std CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Std CI should run now."
+                echo "... but Mathlib does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
+                MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Mathlib CI should run now."
               fi
-    
             else
-              echo "... but Mathlib does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
-              MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Mathlib CI should run now."
+              echo "... but Std does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
+              MESSAGE="- ❗ Std CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Std CI should run now."
             fi
 
           else
@@ -151,7 +149,8 @@ jobs:
             echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA"
             git -C lean4.git log -10 origin/master
 
-            MESSAGE="- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_SHA\`."
+            NIGHTLY_WITH_MATHLIB_SHA="$(git -C lean4.git rev-parse "nightly-with-mathlib")"
+            MESSAGE="- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MATHLIB_SHA\`."
           fi
 
           if [[ -n "$MESSAGE" ]]; then

RELEASES.md

@@ -21,17 +21,16 @@ v4.8.0 (development in progress)
 
 * Importing two different files containing proofs of the same theorem is no longer considered an error. This feature is particularly useful for theorems that are automatically generated on demand (e.g., equational theorems).
 
-* New command `derive_functinal_induction`:
+* Funcitonal induction principles.
 
-  Derived from the definition of a (possibly mutually) recursive function
-  defined by well-founded recursion, a **functional induction principle** is
-  tailored to proofs about that function. For example from:
+  Derived from the definition of a (possibly mutually) recursive function, a **functional induction principle** is created that is tailored to proofs about that function.
+
+  For example from:
   ```
   def ackermann : Nat → Nat → Nat
     | 0, m => m + 1
     | n+1, 0 => ackermann n 1
     | n+1, m+1 => ackermann n (ackermann (n + 1) m)
-  derive_functional_induction ackermann
   ```
   we get
   ```
@@ -41,8 +40,13 @@ v4.8.0 (development in progress)
     (x x : Nat) : motive x x
   ```
 
+  It can be used in the `induction` tactic using the `using` syntax:
+  ```
+  induction n, m using ackermann.induct
+  ```
+
 * The termination checker now recognizes more recursion patterns without an
-  explicit `terminatin_by`. In particular the idiom of counting up to an upper
+  explicit `termination_by`. In particular the idiom of counting up to an upper
   bound, as in
   ```
   def Array.sum (arr : Array Nat) (i acc : Nat) : Nat :=
@@ -53,6 +57,25 @@ v4.8.0 (development in progress)
   ```
   is recognized without having to say `termination_by arr.size - i`.
 
+* Attribute `@[pp_using_anonymous_constructor]` to make structures pretty print like `⟨x, y, z⟩`
+  rather than `{a := x, b := y, c := z}`.
+  This attribute is applied to `Sigma`, `PSigma`, `PProd`, `Subtype`, `And`, and `Fin`.
+
+* Now structure instances pretty print with parent structures' fields inlined.
+  That is, if `B` extends `A`, then `{ toA := { x := 1 }, y := 2 }` now pretty prints as `{ x := 1, y := 2 }`.
+  Setting option `pp.structureInstances.flatten` to false turns this off.
+
+* Option `pp.structureProjections` is renamed to `pp.fieldNotation`, and there is now a suboption `pp.fieldNotation.generalized`
+  to enable pretty printing function applications using generalized field notation (defaults to true).
+  Field notation can be disabled on a function-by-function basis using the `@[pp_nodot]` attribute.
+
+* Added `@[induction_eliminator]` and `@[cases_eliminator]` attributes to be able to define custom eliminators
+  for the `induction` and `cases` tactics, replacing the `@[eliminator]` attribute.
+  Gives custom eliminators for `Nat` so that `induction` and `cases` put goal states into terms of `0` and `n + 1`
+  rather than `Nat.zero` and `Nat.succ n`.
+  Added option `tactic.customEliminators` to control whether to use custom eliminators.
+  [#3629](https://github.com/leanprover/lean4/pull/3629) and
+  [#3655](https://github.com/leanprover/lean4/pull/3655).
 
 Breaking changes:
 
@@ -81,6 +104,8 @@ fact.def :
 -/
 ```
 
+* The coercion from `String` to `Name` was removed. Previously, it was `Name.mkSimple`, which does not separate strings at dots, but experience showed that this is not always the desired coercion. For the previous behavior, manually insert a call to `Name.mkSimple`.
+
 v4.7.0
 ---------
 

default.nix

@@ -1,9 +0,0 @@
-# used for `nix-shell https://github.com/leanprover/lean4/archive/master.tar.gz -A nix`
-{ nix = (import ./shell.nix {}).nix; } //
-(import (
-  fetchTarball {
-    url = "https://github.com/edolstra/flake-compat/archive/c75e76f80c57784a6734356315b306140646ee84.tar.gz";
-    sha256 = "071aal00zp2m9knnhddgr2wqzlx6i6qa1263lv1y7bdn2w20h10h"; }
-) {
-  src =  ./.;
-}).defaultNix

doc/flake.nix

@@ -27,7 +27,7 @@
         src = inputs.mdBook;
         cargoDeps = drv.cargoDeps.overrideAttrs (_: {
           inherit src;
-          outputHash = "sha256-1YlPS6cqgxE4fjy9G8pWrpP27YrrbCDnfeyIsX81ZNw=";
+          outputHash = "sha256-CO3A9Kpp4sIvkT9X3p+GTidazk7Fn4jf0AP2PINN44A=";
         });
         doCheck = false;
       });

doc/make/index.md

@@ -12,7 +12,7 @@ Platform-Specific Setup
 - [Windows (msys2)](msys2.md)
 - [Windows (WSL)](wsl.md)
 - [macOS (homebrew)](osx-10.9.md)
-- Linux/macOS/WSL via [Nix](https://nixos.org/nix/): Call `nix-shell` in the project root. That's it.
+- Linux/macOS/WSL via [Nix](https://nixos.org/nix/): Call `nix develop` in the project root. That's it.
 
 Generic Build Instructions
 --------------------------

flake.lock

@@ -1,12 +1,31 @@
 {
   "nodes": {
-    "flake-utils": {
+    "flake-compat": {
+      "flake": false,
       "locked": {
-        "lastModified": 1656928814,
-        "narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=",
+        "lastModified": 1673956053,
+        "narHash": "sha256-4gtG9iQuiKITOjNQQeQIpoIB6b16fm+504Ch3sNKLd8=",
+        "owner": "edolstra",
+        "repo": "flake-compat",
+        "rev": "35bb57c0c8d8b62bbfd284272c928ceb64ddbde9",
+        "type": "github"
+      },
+      "original": {
+        "owner": "edolstra",
+        "repo": "flake-compat",
+        "type": "github"
+      }
+    },
+    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
+      "locked": {
+        "lastModified": 1710146030,
+        "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249",
+        "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
         "type": "github"
       },
       "original": {
@@ -18,11 +37,11 @@
     "lean4-mode": {
       "flake": false,
       "locked": {
-        "lastModified": 1676498134,
-        "narHash": "sha256-u3WvyKxOViZG53hkb8wd2/Og6muTecbh+NdflIgVeyk=",
+        "lastModified": 1709737301,
+        "narHash": "sha256-uT9JN2kLNKJK9c/S/WxLjiHmwijq49EgLb+gJUSDpz0=",
         "owner": "leanprover",
         "repo": "lean4-mode",
-        "rev": "2c6ef33f476fdf5eb5e4fa4fa023ba8b11372440",
+        "rev": "f1f24c15134dee3754b82c9d9924866fe6bc6b9f",
         "type": "github"
       },
       "original": {
@@ -31,34 +50,35 @@
         "type": "github"
       }
     },
-    "lowdown-src": {
+    "libgit2": {
       "flake": false,
       "locked": {
-        "lastModified": 1633514407,
-        "narHash": "sha256-Dw32tiMjdK9t3ETl5fzGrutQTzh2rufgZV4A/BbxuD4=",
-        "owner": "kristapsdz",
-        "repo": "lowdown",
-        "rev": "d2c2b44ff6c27b936ec27358a2653caaef8f73b8",
+        "lastModified": 1697646580,
+        "narHash": "sha256-oX4Z3S9WtJlwvj0uH9HlYcWv+x1hqp8mhXl7HsLu2f0=",
+        "owner": "libgit2",
+        "repo": "libgit2",
+        "rev": "45fd9ed7ae1a9b74b957ef4f337bc3c8b3df01b5",
         "type": "github"
       },
       "original": {
-        "owner": "kristapsdz",
-        "repo": "lowdown",
+        "owner": "libgit2",
+        "repo": "libgit2",
         "type": "github"
       }
     },
     "nix": {
       "inputs": {
-        "lowdown-src": "lowdown-src",
+        "flake-compat": "flake-compat",
+        "libgit2": "libgit2",
         "nixpkgs": "nixpkgs",
         "nixpkgs-regression": "nixpkgs-regression"
       },
       "locked": {
-        "lastModified": 1657097207,
-        "narHash": "sha256-SmeGmjWM3fEed3kQjqIAO8VpGmkC2sL1aPE7kKpK650=",
+        "lastModified": 1711102798,
+        "narHash": "sha256-CXOIJr8byjolqG7eqCLa+Wfi7rah62VmLoqSXENaZnw=",
         "owner": "NixOS",
         "repo": "nix",
-        "rev": "f6316b49a0c37172bca87ede6ea8144d7d89832f",
+        "rev": "a22328066416650471c3545b0b138669ea212ab4",
         "type": "github"
       },
       "original": {
@@ -69,16 +89,33 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1653988320,
-        "narHash": "sha256-ZaqFFsSDipZ6KVqriwM34T739+KLYJvNmCWzErjAg7c=",
+        "lastModified": 1709083642,
+        "narHash": "sha256-7kkJQd4rZ+vFrzWu8sTRtta5D1kBG0LSRYAfhtmMlSo=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "2fa57ed190fd6c7c746319444f34b5917666e5c1",
+        "rev": "b550fe4b4776908ac2a861124307045f8e717c8e",
         "type": "github"
       },
       "original": {
         "owner": "NixOS",
-        "ref": "nixos-22.05-small",
+        "ref": "release-23.11",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "nixpkgs-old": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1581379743,
+        "narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixos-19.03",
         "repo": "nixpkgs",
         "type": "github"
       }
@@ -101,11 +138,11 @@
     },
     "nixpkgs_2": {
       "locked": {
-        "lastModified": 1686089707,
-        "narHash": "sha256-LTNlJcru2qJ0XhlhG9Acp5KyjB774Pza3tRH0pKIb3o=",
+        "lastModified": 1710889954,
+        "narHash": "sha256-Pr6F5Pmd7JnNEMHHmspZ0qVqIBVxyZ13ik1pJtm2QXk=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "af21c31b2a1ec5d361ed8050edd0303c31306397",
+        "rev": "7872526e9c5332274ea5932a0c3270d6e4724f3b",
         "type": "github"
       },
       "original": {
@@ -120,7 +157,23 @@
         "flake-utils": "flake-utils",
         "lean4-mode": "lean4-mode",
         "nix": "nix",
-        "nixpkgs": "nixpkgs_2"
+        "nixpkgs": "nixpkgs_2",
+        "nixpkgs-old": "nixpkgs-old"
+      }
+    },
+    "systems": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
       }
     }
   },

flake.nix

@@ -2,6 +2,9 @@
   description = "Lean interactive theorem prover";
 
   inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable";
+  # old nixpkgs used for portable release with older glibc (2.27)
+  inputs.nixpkgs-old.url = "github:NixOS/nixpkgs/nixos-19.03";
+  inputs.nixpkgs-old.flake = false;
   inputs.flake-utils.url = "github:numtide/flake-utils";
   inputs.nix.url = "github:NixOS/nix";
   inputs.lean4-mode = {
@@ -17,14 +20,41 @@
   #  inputs.lean4-mode.follows = "lean4-mode";
   #};
 
-  outputs = { self, nixpkgs, flake-utils, nix, lean4-mode, ... }@inputs: flake-utils.lib.eachDefaultSystem (system:
+  outputs = { self, nixpkgs, nixpkgs-old, flake-utils, nix, lean4-mode, ... }@inputs: flake-utils.lib.eachDefaultSystem (system:
     let
       pkgs = import nixpkgs {
         inherit system;
         # for `vscode-with-extensions`
         config.allowUnfree = true;
       };
+      # An old nixpkgs for creating releases with an old glibc
+      pkgsDist-old = import nixpkgs-old { inherit system; };
+      # An old nixpkgs for creating releases with an old glibc
+      pkgsDist-old-aarch = import nixpkgs-old { localSystem.config = "aarch64-unknown-linux-gnu"; };
+
       lean-packages = pkgs.callPackage (./nix/packages.nix) { src = ./.; inherit nix lean4-mode; };
+
+      devShellWithDist = pkgsDist: pkgs.mkShell.override {
+	  stdenv = pkgs.overrideCC pkgs.stdenv lean-packages.llvmPackages.clang;
+	} ({
+	  buildInputs = with pkgs; [
+	    cmake gmp ccache
+	    lean-packages.llvmPackages.llvm  # llvm-symbolizer for asan/lsan
+	    # TODO: only add when proven to not affect the flakification
+	    #pkgs.python3
+	  ];
+	  # https://github.com/NixOS/nixpkgs/issues/60919
+	  hardeningDisable = [ "all" ];
+	  # more convenient `ctest` output
+	  CTEST_OUTPUT_ON_FAILURE = 1;
+	} // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
+	  GMP = pkgsDist.gmp.override { withStatic = true; };
+	  GLIBC = pkgsDist.glibc;
+	  GLIBC_DEV = pkgsDist.glibc.dev;
+	  GCC_LIB = pkgsDist.gcc.cc.lib;
+	  ZLIB = pkgsDist.zlib;
+	  GDB = pkgsDist.gdb;
+	});
     in {
       packages = lean-packages // rec {
         debug = lean-packages.override { debug = true; };
@@ -49,7 +79,10 @@
       };
       defaultPackage = lean-packages.lean-all;
 
-      inherit (lean-packages) devShell;
+      # The default development shell for working on lean itself
+      devShells.default = devShellWithDist pkgs;
+      devShells.oldGlibc = devShellWithDist pkgsDist-old;
+      devShells.oldGlibcAArch = devShellWithDist pkgsDist-old-aarch;
 
       checks.lean = lean-packages.test;
     }) // rec {

nix/bootstrap.nix

@@ -65,7 +65,7 @@ rec {
     installPhase = ''
       mkdir -p $out/bin $out/lib/lean
       mv bin/lean $out/bin/
-      mv lib/lean/*.so $out/lib/lean
+      mv lib/lean/*.{so,dylib} $out/lib/lean
     '';
     meta.mainProgram = "lean";
   });
@@ -170,10 +170,11 @@ rec {
           ln -sf ${lean-all}/* .
         '';
         buildPhase = ''
-          ctest --output-on-failure -E 'leancomptest_(doc_example|foreign)' -j$NIX_BUILD_CORES
+          ctest --output-junit test-results.xml --output-on-failure -E 'leancomptest_(doc_example|foreign)' -j$NIX_BUILD_CORES
         '';
         installPhase = ''
-          touch $out
+          mkdir $out
+          mv test-results.xml $out
         '';
       };
       update-stage0 =

shell.nix

@@ -1,27 +0,0 @@
-let
-  flake = (import ./default.nix);
-  flakePkgs = flake.packages.${builtins.currentSystem};
-in { pkgs ? flakePkgs.nixpkgs, pkgsDist ? pkgs }:
-# use `shell` as default
-(attribs: attribs.shell // attribs) rec {
-  shell = pkgs.mkShell.override {
-    stdenv = pkgs.overrideCC pkgs.stdenv flakePkgs.llvmPackages.clang;
-  } (rec {
-    buildInputs = with pkgs; [
-      cmake gmp ccache
-      flakePkgs.llvmPackages.llvm  # llvm-symbolizer for asan/lsan
-    ];
-    # https://github.com/NixOS/nixpkgs/issues/60919
-    hardeningDisable = [ "all" ];
-    # more convenient `ctest` output
-    CTEST_OUTPUT_ON_FAILURE = 1;
-  } // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
-    GMP = pkgsDist.gmp.override { withStatic = true; };
-    GLIBC = pkgsDist.glibc;
-    GLIBC_DEV = pkgsDist.glibc.dev;
-    GCC_LIB = pkgsDist.gcc.cc.lib;
-    ZLIB = pkgsDist.zlib;
-    GDB = pkgsDist.gdb;
-  });
-  nix = flake.devShell.${builtins.currentSystem};
-}

src/Init.lean

@@ -33,3 +33,4 @@ import Init.SizeOfLemmas
 import Init.BinderPredicates
 import Init.Ext
 import Init.Omega
+import Init.MacroTrace

src/Init/ByCases.lean

@@ -21,9 +21,9 @@ macro_rules
 
 /-! ## if-then-else -/
 
-@[simp] theorem if_true {h : Decidable True} (t e : α) : ite True t e = t := if_pos trivial
+@[simp] theorem if_true {_ : Decidable True} (t e : α) : ite True t e = t := if_pos trivial
 
-@[simp] theorem if_false {h : Decidable False} (t e : α) : ite False t e = e := if_neg id
+@[simp] theorem if_false {_ : Decidable False} (t e : α) : ite False t e = e := if_neg id
 
 theorem ite_id [Decidable c] {α} (t : α) : (if c then t else t) = t := by split <;> rfl
 

src/Init/Control/ExceptCps.lean

@@ -18,6 +18,7 @@ namespace ExceptCpsT
 def run {ε α : Type u} [Monad m] (x : ExceptCpsT ε m α) : m (Except ε α) :=
   x _ (fun a => pure (Except.ok a)) (fun e => pure (Except.error e))
 
+set_option linter.unusedVariables false in  -- `s` unused
 @[always_inline, inline]
 def runK {ε α : Type u} (x : ExceptCpsT ε m α) (s : ε) (ok : α → m β) (error : ε → m β) : m β :=
   x _ ok error

src/Init/Conv.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 Notation for operators defined at Prelude.lean
 -/
 prelude
-import Init.Meta
+import Init.Tactics
 
 namespace Lean.Parser.Tactic.Conv
 
@@ -201,7 +201,7 @@ macro (name := anyGoals) tk:"any_goals " s:convSeq : conv =>
   with inaccessible names to the given names.
 * `case tag₁ | tag₂ => tac` is equivalent to `(case tag₁ => tac); (case tag₂ => tac)`.
 -/
-macro (name := case) tk:"case " args:sepBy1(caseArg, " | ") arr:" => " s:convSeq : conv =>
+macro (name := case) tk:"case " args:sepBy1(caseArg, "|") arr:" => " s:convSeq : conv =>
   `(conv| tactic' => case%$tk $args|* =>%$arr conv' => ($s); all_goals rfl)
 
 /--
@@ -210,7 +210,7 @@ has been solved after applying `tac`, nor admits the goal if `tac` failed.
 Recall that `case` closes the goal using `sorry` when `tac` fails, and
 the tactic execution is not interrupted.
 -/
-macro (name := case') tk:"case' " args:sepBy1(caseArg, " | ") arr:" => " s:convSeq : conv =>
+macro (name := case') tk:"case' " args:sepBy1(caseArg, "|") arr:" => " s:convSeq : conv =>
   `(conv| tactic' => case'%$tk $args|* =>%$arr conv' => $s)
 
 /--

src/Init/Core.lean

@@ -165,6 +165,7 @@ whose first component is `a : α` and whose second component is `b : β a`
 It is sometimes known as the dependent sum type, since it is the type level version
 of an indexed summation.
 -/
+@[pp_using_anonymous_constructor]
 structure Sigma {α : Type u} (β : α → Type v) where
   /-- Constructor for a dependent pair. If `a : α` and `b : β a` then `⟨a, b⟩ : Sigma β`.
   (This will usually require a type ascription to determine `β`
@@ -190,6 +191,7 @@ which can cause problems for universe level unification,
 because the equation `max 1 u v = ?u + 1` has no solution in level arithmetic.
 `PSigma` is usually only used in automation that constructs pairs of arbitrary types.
 -/
+@[pp_using_anonymous_constructor]
 structure PSigma {α : Sort u} (β : α → Sort v) where
   /-- Constructor for a dependent pair. If `a : α` and `b : β a` then `⟨a, b⟩ : PSigma β`.
   (This will usually require a type ascription to determine `β`
@@ -1594,7 +1596,7 @@ protected def mk' {α : Sort u} [s : Setoid α] (a : α) : Quotient s :=
 The analogue of `Quot.sound`: If `a` and `b` are related by the equivalence relation,
 then they have equal equivalence classes.
 -/
-def sound {α : Sort u} {s : Setoid α} {a b : α} : a ≈ b → Quotient.mk s a = Quotient.mk s b :=
+theorem sound {α : Sort u} {s : Setoid α} {a b : α} : a ≈ b → Quotient.mk s a = Quotient.mk s b :=
   Quot.sound
 
 /--

src/Init/Data/Array/Basic.lean

@@ -10,7 +10,7 @@ import Init.Data.Fin.Basic
 import Init.Data.UInt.Basic
 import Init.Data.Repr
 import Init.Data.ToString.Basic
-import Init.Util
+import Init.GetElem
 universe u v w
 
 namespace Array
@@ -59,6 +59,8 @@ def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
 instance : GetElem (Array α) USize α fun xs i => i.toNat < xs.size where
   getElem xs i h := xs.uget i h
 
+instance : LawfulGetElem (Array α) USize α fun xs i => i.toNat < xs.size where
+
 def back [Inhabited α] (a : Array α) : α :=
   a.get! (a.size - 1)
 
@@ -456,24 +458,12 @@ def findRev? {α : Type} (as : Array α) (p : α → Bool) : Option α :=
 
 @[inline]
 def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
-  let rec loop (i : Nat) (j : Nat) (inv : i + j = as.size) : Option Nat :=
-    if hlt : j < as.size then
-      match i, inv with
-      | 0, inv => by
-        apply False.elim
-        rw [Nat.zero_add] at inv
-        rw [inv] at hlt
-        exact absurd hlt (Nat.lt_irrefl _)
-      | i+1, inv =>
-        if p as[j] then
-          some j
-        else
-          have : i + (j+1) = as.size := by
-            rw [← inv, Nat.add_comm j 1, Nat.add_assoc]
-          loop i (j+1) this
-    else
-      none
-  loop as.size 0 rfl
+  let rec loop (j : Nat) :=
+    if h : j < as.size then
+      if p as[j] then some j else loop (j + 1)
+    else none
+    termination_by as.size - j
+  loop 0
 
 def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
 a.findIdx? fun a => a == v
@@ -727,33 +717,36 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
     termination_by as.size - i
   go 0 #[]
 
-def eraseIdxAux (i : Nat) (a : Array α) : Array α :=
-  if h : i < a.size then
-    let idx  : Fin a.size := ⟨i, h⟩;
-    let idx1 : Fin a.size := ⟨i - 1, by exact Nat.lt_of_le_of_lt (Nat.pred_le i) h⟩;
-    let a' := a.swap idx idx1
-    eraseIdxAux (i+1) a'
+/-- Remove the element at a given index from an array without bounds checks, using a `Fin` index.
+
+  This function takes worst case O(n) time because
+  it has to backshift all elements at positions greater than `i`.-/
+def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
+  if h : i.val + 1 < a.size then
+    let a' := a.swap ⟨i.val + 1, h⟩ i
+    let i' : Fin a'.size := ⟨i.val + 1, by simp [a', h]⟩
+    have : a'.size - i' < a.size - i := by
+      simp [a', Nat.sub_succ_lt_self _ _ i.isLt]
+    a'.feraseIdx i'
   else
     a.pop
-termination_by a.size - i
+termination_by a.size - i.val
 
-def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
-  eraseIdxAux (i.val + 1) a
+theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
+  induction a, i using Array.feraseIdx.induct with
+  | @case1 a i h a' _ _ ih =>
+    unfold feraseIdx
+    simp [h, a', ih]
+  | case2 a i h =>
+    unfold feraseIdx
+    simp [h]
 
+/-- Remove the element at a given index from an array, or do nothing if the index is out of bounds.
+
+  This function takes worst case O(n) time because
+  it has to backshift all elements at positions greater than `i`.-/
 def eraseIdx (a : Array α) (i : Nat) : Array α :=
-  if i < a.size then eraseIdxAux (i+1) a else a
-
-def eraseIdxSzAux (a : Array α) (i : Nat) (r : Array α) (heq : r.size = a.size) : { r : Array α // r.size = a.size - 1 } :=
-  if h : i < r.size then
-    let idx  : Fin r.size := ⟨i, h⟩;
-    let idx1 : Fin r.size := ⟨i - 1, by exact Nat.lt_of_le_of_lt (Nat.pred_le i) h⟩;
-    eraseIdxSzAux a (i+1) (r.swap idx idx1) ((size_swap r idx idx1).trans heq)
-  else
-    ⟨r.pop, (size_pop r).trans (heq ▸ rfl)⟩
-termination_by r.size - i
-
-def eraseIdx' (a : Array α) (i : Fin a.size) : { r : Array α // r.size = a.size - 1 } :=
-  eraseIdxSzAux a (i.val + 1) a rfl
+  if h : i < a.size then a.feraseIdx ⟨i, h⟩ else a
 
 def erase [BEq α] (as : Array α) (a : α) : Array α :=
   match as.indexOf? a with

src/Init/Data/Array/Subarray.lean

@@ -32,6 +32,8 @@ def get (s : Subarray α) (i : Fin s.size) : α :=
 instance : GetElem (Subarray α) Nat α fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
+instance : LawfulGetElem (Subarray α) Nat α fun xs i => i < xs.size where
+
 @[inline] def getD (s : Subarray α) (i : Nat) (v₀ : α) : α :=
   if h : i < s.size then s.get ⟨i, h⟩ else v₀
 

src/Init/Data/BitVec/Basic.lean

@@ -618,4 +618,14 @@ section normalization_eqs
 @[simp] theorem zero_eq                                   : BitVec.zero n = 0#n               := rfl
 end normalization_eqs
 
+/-- Converts a list of `Bool`s to a big-endian `BitVec`. -/
+def ofBoolListBE : (bs : List Bool) → BitVec bs.length
+| [] => 0#0
+| b :: bs => cons b (ofBoolListBE bs)
+
+/-- Converts a list of `Bool`s to a little-endian `BitVec`. -/
+def ofBoolListLE : (bs : List Bool) → BitVec bs.length
+| [] => 0#0
+| b :: bs => concat (ofBoolListLE bs) b
+
 end BitVec

src/Init/Data/BitVec/Lemmas.lean

@@ -41,12 +41,36 @@ theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsb i := rfl
   have p : 2^w ≤ 2^i := Nat.pow_le_pow_of_le_right (by omega) ge
   omega
 
+@[simp] theorem getMsb_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getMsb x i = false := by
+  rw [getMsb]
+  simp only [Bool.and_eq_false_imp, decide_eq_true_eq]
+  omega
+
 theorem lt_of_getLsb (x : BitVec w) (i : Nat) : getLsb x i = true → i < w := by
   if h : i < w then
     simp [h]
   else
     simp [Nat.ge_of_not_lt h]
 
+theorem lt_of_getMsb (x : BitVec w) (i : Nat) : getMsb x i = true → i < w := by
+  if h : i < w then
+    simp [h]
+  else
+    simp [Nat.ge_of_not_lt h]
+
+theorem getMsb_eq_getLsb (x : BitVec w) (i : Nat) : x.getMsb i = (decide (i < w) && x.getLsb (w - 1 - i)) := by
+  rw [getMsb]
+
+theorem getLsb_eq_getMsb (x : BitVec w) (i : Nat) : x.getLsb i = (decide (i < w) && x.getMsb (w - 1 - i)) := by
+  rw [getMsb]
+  by_cases h₁ : i < w <;> by_cases h₂ : w - 1 - i < w <;>
+    simp only [h₁, h₂] <;> simp only [decide_True, decide_False, Bool.false_and, Bool.and_false, Bool.true_and, Bool.and_true]
+  · congr
+    omega
+  all_goals
+    apply getLsb_ge
+    omega
+
 -- We choose `eq_of_getLsb_eq` as the `@[ext]` theorem for `BitVec`
 -- somewhat arbitrarily over `eq_of_getMsg_eq`.
 @[ext] theorem eq_of_getLsb_eq {x y : BitVec w}
@@ -96,6 +120,8 @@ theorem ofNat_one (n : Nat) : BitVec.ofNat 1 n = BitVec.ofBool (n % 2 = 1) :=  b
 theorem ofBool_eq_iff_eq : ∀(b b' : Bool), BitVec.ofBool b = BitVec.ofBool b' ↔ b = b' := by
   decide
 
+@[simp] theorem not_ofBool : ~~~ (ofBool b) = ofBool (!b) := by cases b <;> rfl
+
 @[simp, bv_toNat] theorem toNat_ofFin (x : Fin (2^n)) : (BitVec.ofFin x).toNat = x.val := rfl
 
 @[simp] theorem toNat_ofNatLt (x : Nat) (p : x < 2^w) : (x#'p).toNat = x := rfl
@@ -290,6 +316,19 @@ theorem nat_eq_toNat (x : BitVec w) (y : Nat)
     getLsb (zeroExtend' ge x) i = getLsb x i := by
   simp [getLsb, toNat_zeroExtend']
 
+@[simp] theorem getMsb_zeroExtend' (ge : m ≥ n) (x : BitVec n) (i : Nat) :
+    getMsb (zeroExtend' ge x) i = (decide (i ≥ m - n) && getMsb x (i - (m - n))) := by
+  simp only [getMsb, getLsb_zeroExtend', gt_iff_lt]
+  by_cases h₁ : decide (i < m) <;> by_cases h₂ : decide (i ≥ m - n) <;> by_cases h₃ : decide (i - (m - n) < n) <;>
+    by_cases h₄ : n - 1 - (i - (m - n)) = m - 1 - i
+  all_goals
+    simp only [h₁, h₂, h₃, h₄]
+    simp_all only [ge_iff_le, decide_eq_true_eq, Nat.not_le, Nat.not_lt, Bool.true_and,
+      Bool.false_and, Bool.and_self] <;>
+    (try apply getLsb_ge) <;>
+    (try apply (getLsb_ge _ _ _).symm) <;>
+    omega
+
 @[simp] theorem getLsb_zeroExtend (m : Nat) (x : BitVec n) (i : Nat) :
     getLsb (zeroExtend m x) i = (decide (i < m) && getLsb x i) := by
   simp [getLsb, toNat_zeroExtend, Nat.testBit_mod_two_pow]
@@ -480,6 +519,24 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   simp [h]
   omega
 
+/-! ### cast -/
+
+@[simp] theorem not_cast {x : BitVec w} (h : w = w') : ~~~(cast h x) = cast h (~~~x) := by
+  ext
+  simp_all [lt_of_getLsb]
+
+@[simp] theorem and_cast {x y : BitVec w} (h : w = w') : cast h x &&& cast h y = cast h (x &&& y) := by
+  ext
+  simp_all [lt_of_getLsb]
+
+@[simp] theorem or_cast {x y : BitVec w} (h : w = w') : cast h x ||| cast h y = cast h (x ||| y) := by
+  ext
+  simp_all [lt_of_getLsb]
+
+@[simp] theorem xor_cast {x y : BitVec w} (h : w = w') : cast h x &&& cast h y = cast h (x &&& y) := by
+  ext
+  simp_all [lt_of_getLsb]
+
 /-! ### shiftLeft -/
 
 @[simp, bv_toNat] theorem toNat_shiftLeft {x : BitVec v} :
@@ -529,6 +586,11 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
     <;> simp_all
     <;> (rw [getLsb_ge]; omega)
 
+@[simp] theorem getMsb_shiftLeftZeroExtend (x : BitVec m) (n : Nat) :
+    getMsb (shiftLeftZeroExtend x n) i = getMsb x i := by
+  have : n ≤ i + n := by omega
+  simp_all [shiftLeftZeroExtend_eq]
+
 @[simp] theorem msb_shiftLeftZeroExtend (x : BitVec w) (i : Nat) :
     (shiftLeftZeroExtend x i).msb = x.msb := by
   simp [shiftLeftZeroExtend_eq, BitVec.msb]
@@ -553,11 +615,18 @@ theorem append_def (x : BitVec v) (y : BitVec w) :
 
 @[simp] theorem getLsb_append {v : BitVec n} {w : BitVec m} :
     getLsb (v ++ w) i = bif i < m then getLsb w i else getLsb v (i - m) := by
-  simp [append_def]
+  simp only [append_def, getLsb_or, getLsb_shiftLeftZeroExtend, getLsb_zeroExtend']
   by_cases h : i < m
   · simp [h]
   · simp [h]; simp_all
 
+@[simp] theorem getMsb_append {v : BitVec n} {w : BitVec m} :
+    getMsb (v ++ w) i = bif n ≤ i then getMsb w (i - n) else getMsb v i := by
+  simp [append_def]
+  by_cases h : n ≤ i
+  · simp [h]
+  · simp [h]
+
 theorem msb_append {x : BitVec w} {y : BitVec v} :
     (x ++ y).msb = bif (w == 0) then (y.msb) else (x.msb) := by
   rw [← append_eq, append]
@@ -586,6 +655,31 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
 @[simp] theorem truncate_cons {x : BitVec w} : (cons a x).truncate w = x := by
   simp [cons]
 
+@[simp] theorem not_append {x : BitVec w} {y : BitVec v} : ~~~ (x ++ y) = (~~~ x) ++ (~~~ y) := by
+  ext i
+  simp only [getLsb_not, getLsb_append, cond_eq_if]
+  split
+  · simp_all
+  · simp_all; omega
+
+@[simp] theorem and_append {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} :
+    (x₁ ++ y₁) &&& (x₂ ++ y₂) = (x₁ &&& x₂) ++ (y₁ &&& y₂) := by
+  ext i
+  simp only [getLsb_append, cond_eq_if]
+  split <;> simp [*]
+
+@[simp] theorem or_append {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} :
+    (x₁ ++ y₁) ||| (x₂ ++ y₂) = (x₁ ||| x₂) ++ (y₁ ||| y₂) := by
+  ext i
+  simp only [getLsb_append, cond_eq_if]
+  split <;> simp [*]
+
+@[simp] theorem xor_append {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} :
+    (x₁ ++ y₁) ^^^ (x₂ ++ y₂) = (x₁ ^^^ x₂) ++ (y₁ ^^^ y₂) := by
+  ext i
+  simp only [getLsb_append, cond_eq_if]
+  split <;> simp [*]
+
 /-! ### rev -/
 
 theorem getLsb_rev (x : BitVec w) (i : Fin w) :
@@ -630,6 +724,13 @@ theorem toNat_cons' {x : BitVec w} :
 @[simp] theorem msb_cons : (cons a x).msb = a := by
   simp [cons, msb_cast, msb_append]
 
+@[simp] theorem getMsb_cons_zero : (cons a x).getMsb 0 = a := by
+  rw [← BitVec.msb, msb_cons]
+
+@[simp] theorem getMsb_cons_succ : (cons a x).getMsb (i + 1) = x.getMsb i := by
+  simp [cons, cond_eq_if]
+  omega
+
 theorem truncate_succ (x : BitVec w) :
     truncate (i+1) x = cons (getLsb x i) (truncate i x) := by
   apply eq_of_getLsb_eq
@@ -650,6 +751,21 @@ theorem eq_msb_cons_truncate (x : BitVec (w+1)) : x = (cons x.msb (x.truncate w)
     · simp_all
     · omega
 
+@[simp] theorem not_cons (x : BitVec w) (b : Bool) : ~~~(cons b x) = cons (!b) (~~~x) := by
+  simp [cons]
+
+@[simp] theorem cons_or_cons (x y : BitVec w) (a b : Bool) :
+    (cons a x) ||| (cons b y) = cons (a || b) (x ||| y) := by
+  ext i; cases i using Fin.succRecOn <;> simp <;> split <;> rfl
+
+@[simp] theorem cons_and_cons (x y : BitVec w) (a b : Bool) :
+    (cons a x) &&& (cons b y) = cons (a && b) (x &&& y) := by
+  ext i; cases i using Fin.succRecOn <;> simp <;> split <;> rfl
+
+@[simp] theorem cons_xor_cons (x y : BitVec w) (a b : Bool) :
+    (cons a x) ^^^ (cons b y) = cons (xor a b) (x ^^^ y) := by
+  ext i; cases i using Fin.succRecOn <;> simp <;> split <;> rfl
+
 /-! ### concat -/
 
 @[simp] theorem toNat_concat (x : BitVec w) (b : Bool) :
@@ -825,7 +941,7 @@ protected theorem lt_of_le_ne (x y : BitVec n) (h1 : x <= y) (h2 : ¬ x = y) : x
   simp
   exact Nat.lt_of_le_of_ne
 
-/- ! ### intMax -/
+/-! ### intMax -/
 
 /-- The bitvector of width `w` that has the largest value when interpreted as an integer. -/
 def intMax (w : Nat) : BitVec w  := (2^w - 1)#w
@@ -839,4 +955,20 @@ theorem toNat_intMax_eq : (intMax w).toNat = 2^w - 1 := by
     omega
   simp [intMax, Nat.shiftLeft_eq, Nat.one_mul, natCast_eq_ofNat, toNat_ofNat, Nat.mod_eq_of_lt h]
 
+/-! ### ofBoolList -/
+
+@[simp] theorem getMsb_ofBoolListBE : (ofBoolListBE bs).getMsb i = bs.getD i false := by
+  induction bs generalizing i <;> cases i <;> simp_all [ofBoolListBE]
+
+@[simp] theorem getLsb_ofBoolListBE :
+    (ofBoolListBE bs).getLsb i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false) := by
+  simp [getLsb_eq_getMsb]
+
+@[simp] theorem getLsb_ofBoolListLE : (ofBoolListLE bs).getLsb i = bs.getD i false := by
+  induction bs generalizing i <;> cases i <;> simp_all [ofBoolListLE]
+
+@[simp] theorem getMsb_ofBoolListLE :
+    (ofBoolListLE bs).getMsb i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false) := by
+  simp [getMsb_eq_getLsb]
+
 end BitVec

src/Init/Data/ByteArray/Basic.lean

@@ -52,9 +52,13 @@ def get : (a : @& ByteArray) → (@& Fin a.size) → UInt8
 instance : GetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
+instance : LawfulGetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
+
 instance : GetElem ByteArray USize UInt8 fun xs i => i.val < xs.size where
   getElem xs i h := xs.uget i h
 
+instance : LawfulGetElem ByteArray USize UInt8 fun xs i => i.val < xs.size where
+
 @[extern "lean_byte_array_set"]
 def set! : ByteArray → (@& Nat) → UInt8 → ByteArray
   | ⟨bs⟩, i, b => ⟨bs.set! i b⟩
@@ -195,18 +199,6 @@ instance : ToString ByteArray := ⟨fun bs => bs.toList.toString⟩
 
 /-- Interpret a `ByteArray` of size 8 as a little-endian `UInt64`. -/
 def ByteArray.toUInt64LE! (bs : ByteArray) : UInt64 :=
-  assert! bs.size == 8
-  (bs.get! 0).toUInt64 <<< 0x38 |||
-  (bs.get! 1).toUInt64 <<< 0x30 |||
-  (bs.get! 2).toUInt64 <<< 0x28 |||
-  (bs.get! 3).toUInt64 <<< 0x20 |||
-  (bs.get! 4).toUInt64 <<< 0x18 |||
-  (bs.get! 5).toUInt64 <<< 0x10 |||
-  (bs.get! 6).toUInt64 <<< 0x8  |||
-  (bs.get! 7).toUInt64
-
-/-- Interpret a `ByteArray` of size 8 as a big-endian `UInt64`. -/
-def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 :=
   assert! bs.size == 8
   (bs.get! 7).toUInt64 <<< 0x38 |||
   (bs.get! 6).toUInt64 <<< 0x30 |||
@@ -216,3 +208,15 @@ def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 :=
   (bs.get! 2).toUInt64 <<< 0x10 |||
   (bs.get! 1).toUInt64 <<< 0x8  |||
   (bs.get! 0).toUInt64
+
+/-- Interpret a `ByteArray` of size 8 as a big-endian `UInt64`. -/
+def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 :=
+  assert! bs.size == 8
+  (bs.get! 0).toUInt64 <<< 0x38 |||
+  (bs.get! 1).toUInt64 <<< 0x30 |||
+  (bs.get! 2).toUInt64 <<< 0x28 |||
+  (bs.get! 3).toUInt64 <<< 0x20 |||
+  (bs.get! 4).toUInt64 <<< 0x18 |||
+  (bs.get! 5).toUInt64 <<< 0x10 |||
+  (bs.get! 6).toUInt64 <<< 0x8  |||
+  (bs.get! 7).toUInt64

src/Init/Data/Fin/Basic.lean

@@ -4,9 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura, Robert Y. Lewis, Keeley Hoek, Mario Carneiro
 -/
 prelude
-import Init.Data.Nat.Div
 import Init.Data.Nat.Bitwise.Basic
-import Init.Coe
 
 open Nat
 
@@ -170,9 +168,3 @@ theorem val_add_one_le_of_lt {n : Nat} {a b : Fin n} (h : a < b) : (a : Nat) + 1
 theorem val_add_one_le_of_gt {n : Nat} {a b : Fin n} (h : a > b) : (b : Nat) + 1 ≤ (a : Nat) := h
 
 end Fin
-
-instance [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i where
-  getElem xs i h := getElem xs i.1 h
-
-macro_rules
-  | `(tactic| get_elem_tactic_trivial) => `(tactic| apply Fin.val_lt_of_le; get_elem_tactic_trivial; done)

src/Init/Data/FloatArray/Basic.lean

@@ -58,9 +58,13 @@ def get? (ds : FloatArray) (i : Nat) : Option Float :=
 instance : GetElem FloatArray Nat Float fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
+instance : LawfulGetElem FloatArray Nat Float fun xs i => i < xs.size where
+
 instance : GetElem FloatArray USize Float fun xs i => i.val < xs.size where
   getElem xs i h := xs.uget i h
 
+instance : LawfulGetElem FloatArray USize Float fun xs i => i.val < xs.size where
+
 @[extern "lean_float_array_uset"]
 def uset : (a : FloatArray) → (i : USize) → Float → i.toNat < a.size → FloatArray
   | ⟨ds⟩, i, v, h => ⟨ds.uset i v h⟩

src/Init/Data/Int/DivModLemmas.lean

@@ -8,6 +8,7 @@ prelude
 import Init.Data.Int.DivMod
 import Init.Data.Int.Order
 import Init.Data.Nat.Dvd
+import Init.RCases
 
 /-!
 # Lemmas about integer division needed to bootstrap `omega`.

src/Init/Data/Int/Lemmas.lean

@@ -6,7 +6,7 @@ Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
 prelude
 import Init.Data.Int.Basic
 import Init.Conv
-import Init.PropLemmas
+import Init.NotationExtra
 
 namespace Int
 

src/Init/Data/Int/Order.lean

@@ -6,7 +6,6 @@ Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
 prelude
 import Init.Data.Int.Lemmas
 import Init.ByCases
-import Init.RCases
 
 /-!
 # Results about the order properties of the integers, and the integers as an ordered ring.
@@ -999,7 +998,8 @@ theorem natAbs_add_le (a b : Int) : natAbs (a + b) ≤ natAbs a + natAbs b := by
   refine fun a b => subNatNat_elim a b.succ
     (fun m n i => n = b.succ → natAbs i ≤ (m + b).succ) ?_
     (fun i n (e : (n + i).succ = _) => ?_) rfl
-  · rintro i n rfl
+  · intro i n h
+    subst h
     rw [Nat.add_comm _ i, Nat.add_assoc]
     exact Nat.le_add_right i (b.succ + b).succ
   · apply succ_le_succ

src/Init/Data/List.lean

@@ -8,3 +8,4 @@ import Init.Data.List.Basic
 import Init.Data.List.BasicAux
 import Init.Data.List.Control
 import Init.Data.List.Lemmas
+import Init.Data.List.Impl

src/Init/Data/List/Basic.lean

@@ -7,6 +7,7 @@ prelude
 import Init.SimpLemmas
 import Init.Data.Nat.Basic
 import Init.Data.Nat.Div
+
 set_option linter.missingDocs true -- keep it documented
 open Decidable List
 
@@ -54,15 +55,6 @@ variable {α : Type u} {β : Type v} {γ : Type w}
 
 namespace List
 
-instance : GetElem (List α) Nat α fun as i => i < as.length where
-  getElem as i h := as.get ⟨i, h⟩
-
-@[simp] theorem cons_getElem_zero (a : α) (as : List α) (h : 0 < (a :: as).length) : getElem (a :: as) 0 h = a := by
-  rfl
-
-@[simp] theorem cons_getElem_succ (a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: as).length) : getElem (a :: as) (i+1) h = getElem as i (Nat.lt_of_succ_lt_succ h) := by
-  rfl
-
 theorem length_add_eq_lengthTRAux (as : List α) (n : Nat) : as.length + n = as.lengthTRAux n := by
   induction as generalizing n with
   | nil  => simp [length, lengthTRAux]
@@ -458,7 +450,7 @@ contains the longest initial segment for which `p` returns true
 and the second part is everything else.
 
 * `span (· > 5) [6, 8, 9, 5, 2, 9] = ([6, 8, 9], [5, 2, 9])`
-* `span (· > 10) [6, 8, 9, 5, 2, 9] = ([6, 8, 9, 5, 2, 9], [])`
+* `span (· > 10) [6, 8, 9, 5, 2, 9] = ([], [6, 8, 9, 5, 2, 9])`
 -/
 @[inline] def span (p : α → Bool) (as : List α) : List α × List α :=
   loop as []
@@ -520,11 +512,6 @@ def drop : Nat → List α → List α
 @[simp] theorem drop_nil : ([] : List α).drop i = [] := by
   cases i <;> rfl
 
-theorem get_drop_eq_drop (as : List α) (i : Nat) (h : i < as.length) : as[i] :: as.drop (i+1) = as.drop i :=
-  match as, i with
-  | _::_, 0   => rfl
-  | _::_, i+1 => get_drop_eq_drop _ i _
-
 /--
 `O(min n |xs|)`. Returns the first `n` elements of `xs`, or the whole list if `n` is too large.
 * `take 0 [a, b, c, d, e] = []`

src/Init/Data/List/Impl.lean

@@ -0,0 +1,261 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+
+prelude
+import Init.Data.Array.Lemmas
+
+/-!
+## Tail recursive implementations for `List` definitions.
+
+Many of the proofs require theorems about `Array`,
+so these are in a separate file to minimize imports.
+-/
+
+namespace List
+
+/-- Tail recursive version of `erase`. -/
+@[inline] def setTR (l : List α) (n : Nat) (a : α) : List α := go l n #[] where
+  /-- Auxiliary for `setTR`: `setTR.go l a xs n acc = acc.toList ++ set xs a`,
+  unless `n ≥ l.length` in which case it returns `l` -/
+  go : List α → Nat → Array α → List α
+  | [], _, _ => l
+  | _::xs, 0, acc => acc.toListAppend (a::xs)
+  | x::xs, n+1, acc => go xs n (acc.push x)
+
+@[csimp] theorem set_eq_setTR : @set = @setTR := by
+  funext α l n a; simp [setTR]
+  let rec go (acc) : ∀ xs n, l = acc.data ++ xs →
+    setTR.go l a xs n acc = acc.data ++ xs.set n a
+  | [], _ => fun h => by simp [setTR.go, set, h]
+  | x::xs, 0 => by simp [setTR.go, set]
+  | x::xs, n+1 => fun h => by simp [setTR.go, set]; rw [go _ xs]; {simp}; simp [h]
+  exact (go #[] _ _ rfl).symm
+
+/-- Tail recursive version of `erase`. -/
+@[inline] def eraseTR [BEq α] (l : List α) (a : α) : List α := go l #[] where
+  /-- Auxiliary for `eraseTR`: `eraseTR.go l a xs acc = acc.toList ++ erase xs a`,
+  unless `a` is not present in which case it returns `l` -/
+  go : List α → Array α → List α
+  | [], _ => l
+  | x::xs, acc => bif x == a then acc.toListAppend xs else go xs (acc.push x)
+
+@[csimp] theorem erase_eq_eraseTR : @List.erase = @eraseTR := by
+  funext α _ l a; simp [eraseTR]
+  suffices ∀ xs acc, l = acc.data ++ xs → eraseTR.go l a xs acc = acc.data ++ xs.erase a from
+    (this l #[] (by simp)).symm
+  intro xs; induction xs with intro acc h
+  | nil => simp [List.erase, eraseTR.go, h]
+  | cons x xs IH =>
+    simp [List.erase, eraseTR.go]
+    cases x == a <;> simp
+    · rw [IH]; simp; simp; exact h
+
+/-- Tail recursive version of `eraseIdx`. -/
+@[inline] def eraseIdxTR (l : List α) (n : Nat) : List α := go l n #[] where
+  /-- Auxiliary for `eraseIdxTR`: `eraseIdxTR.go l n xs acc = acc.toList ++ eraseIdx xs a`,
+  unless `a` is not present in which case it returns `l` -/
+  go : List α → Nat → Array α → List α
+  | [], _, _ => l
+  | _::as, 0, acc => acc.toListAppend as
+  | a::as, n+1, acc => go as n (acc.push a)
+
+@[csimp] theorem eraseIdx_eq_eraseIdxTR : @eraseIdx = @eraseIdxTR := by
+  funext α l n; simp [eraseIdxTR]
+  suffices ∀ xs acc, l = acc.data ++ xs → eraseIdxTR.go l xs n acc = acc.data ++ xs.eraseIdx n from
+    (this l #[] (by simp)).symm
+  intro xs; induction xs generalizing n with intro acc h
+  | nil => simp [eraseIdx, eraseIdxTR.go, h]
+  | cons x xs IH =>
+    match n with
+    | 0 => simp [eraseIdx, eraseIdxTR.go]
+    | n+1 =>
+      simp [eraseIdx, eraseIdxTR.go]
+      rw [IH]; simp; simp; exact h
+
+/-- Tail recursive version of `bind`. -/
+@[inline] def bindTR (as : List α) (f : α → List β) : List β := go as #[] where
+  /-- Auxiliary for `bind`: `bind.go f as = acc.toList ++ bind f as` -/
+  @[specialize] go : List α → Array β → List β
+  | [], acc => acc.toList
+  | x::xs, acc => go xs (acc ++ f x)
+
+@[csimp] theorem bind_eq_bindTR : @List.bind = @bindTR := by
+  funext α β as f
+  let rec go : ∀ as acc, bindTR.go f as acc = acc.data ++ as.bind f
+    | [], acc => by simp [bindTR.go, bind]
+    | x::xs, acc => by simp [bindTR.go, bind, go xs]
+  exact (go as #[]).symm
+
+/-- Tail recursive version of `join`. -/
+@[inline] def joinTR (l : List (List α)) : List α := bindTR l id
+
+@[csimp] theorem join_eq_joinTR : @join = @joinTR := by
+  funext α l; rw [← List.bind_id, List.bind_eq_bindTR]; rfl
+
+/-- Tail recursive version of `filterMap`. -/
+@[inline] def filterMapTR (f : α → Option β) (l : List α) : List β := go l #[] where
+  /-- Auxiliary for `filterMap`: `filterMap.go f l = acc.toList ++ filterMap f l` -/
+  @[specialize] go : List α → Array β → List β
+  | [], acc => acc.toList
+  | a::as, acc => match f a with
+    | none => go as acc
+    | some b => go as (acc.push b)
+
+@[csimp] theorem filterMap_eq_filterMapTR : @List.filterMap = @filterMapTR := by
+  funext α β f l
+  let rec go : ∀ as acc, filterMapTR.go f as acc = acc.data ++ as.filterMap f
+    | [], acc => by simp [filterMapTR.go, filterMap]
+    | a::as, acc => by simp [filterMapTR.go, filterMap, go as]; split <;> simp [*]
+  exact (go l #[]).symm
+
+/-- Tail recursive version of `replace`. -/
+@[inline] def replaceTR [BEq α] (l : List α) (b c : α) : List α := go l #[] where
+  /-- Auxiliary for `replace`: `replace.go l b c xs acc = acc.toList ++ replace xs b c`,
+  unless `b` is not found in `xs` in which case it returns `l`. -/
+  @[specialize] go : List α → Array α → List α
+  | [], _ => l
+  | a::as, acc => bif a == b then acc.toListAppend (c::as) else go as (acc.push a)
+
+@[csimp] theorem replace_eq_replaceTR : @List.replace = @replaceTR := by
+  funext α _ l b c; simp [replaceTR]
+  suffices ∀ xs acc, l = acc.data ++ xs →
+      replaceTR.go l b c xs acc = acc.data ++ xs.replace b c from
+    (this l #[] (by simp)).symm
+  intro xs; induction xs with intro acc
+  | nil => simp [replace, replaceTR.go]
+  | cons x xs IH =>
+    simp [replace, replaceTR.go]; split <;> simp [*]
+    · intro h; rw [IH]; simp; simp; exact h
+
+/-- Tail recursive version of `take`. -/
+@[inline] def takeTR (n : Nat) (l : List α) : List α := go l n #[] where
+  /-- Auxiliary for `take`: `take.go l xs n acc = acc.toList ++ take n xs`,
+  unless `n ≥ xs.length` in which case it returns `l`. -/
+  @[specialize] go : List α → Nat → Array α → List α
+  | [], _, _ => l
+  | _::_, 0, acc => acc.toList
+  | a::as, n+1, acc => go as n (acc.push a)
+
+@[csimp] theorem take_eq_takeTR : @take = @takeTR := by
+  funext α n l; simp [takeTR]
+  suffices ∀ xs acc, l = acc.data ++ xs → takeTR.go l xs n acc = acc.data ++ xs.take n from
+    (this l #[] (by simp)).symm
+  intro xs; induction xs generalizing n with intro acc
+  | nil => cases n <;> simp [take, takeTR.go]
+  | cons x xs IH =>
+    cases n with simp [take, takeTR.go]
+    | succ n => intro h; rw [IH]; simp; simp; exact h
+
+/-- Tail recursive version of `takeWhile`. -/
+@[inline] def takeWhileTR (p : α → Bool) (l : List α) : List α := go l #[] where
+  /-- Auxiliary for `takeWhile`: `takeWhile.go p l xs acc = acc.toList ++ takeWhile p xs`,
+  unless no element satisfying `p` is found in `xs` in which case it returns `l`. -/
+  @[specialize] go : List α → Array α → List α
+  | [], _ => l
+  | a::as, acc => bif p a then go as (acc.push a) else acc.toList
+
+@[csimp] theorem takeWhile_eq_takeWhileTR : @takeWhile = @takeWhileTR := by
+  funext α p l; simp [takeWhileTR]
+  suffices ∀ xs acc, l = acc.data ++ xs →
+      takeWhileTR.go p l xs acc = acc.data ++ xs.takeWhile p from
+    (this l #[] (by simp)).symm
+  intro xs; induction xs with intro acc
+  | nil => simp [takeWhile, takeWhileTR.go]
+  | cons x xs IH =>
+    simp [takeWhile, takeWhileTR.go]; split <;> simp [*]
+    · intro h; rw [IH]; simp; simp; exact h
+
+/-- Tail recursive version of `foldr`. -/
+@[specialize] def foldrTR (f : α → β → β) (init : β) (l : List α) : β := l.toArray.foldr f init
+
+@[csimp] theorem foldr_eq_foldrTR : @foldr = @foldrTR := by
+  funext α β f init l; simp [foldrTR, Array.foldr_eq_foldr_data, -Array.size_toArray]
+
+/-- Tail recursive version of `zipWith`. -/
+@[inline] def zipWithTR (f : α → β → γ) (as : List α) (bs : List β) : List γ := go as bs #[] where
+  /-- Auxiliary for `zipWith`: `zipWith.go f as bs acc = acc.toList ++ zipWith f as bs` -/
+  go : List α → List β → Array γ → List γ
+  | a::as, b::bs, acc => go as bs (acc.push (f a b))
+  | _, _, acc => acc.toList
+
+@[csimp] theorem zipWith_eq_zipWithTR : @zipWith = @zipWithTR := by
+  funext α β γ f as bs
+  let rec go : ∀ as bs acc, zipWithTR.go f as bs acc = acc.data ++ as.zipWith f bs
+    | [], _, acc | _::_, [], acc => by simp [zipWithTR.go, zipWith]
+    | a::as, b::bs, acc => by simp [zipWithTR.go, zipWith, go as bs]
+  exact (go as bs #[]).symm
+
+/-- Tail recursive version of `unzip`. -/
+def unzipTR (l : List (α × β)) : List α × List β :=
+  l.foldr (fun (a, b) (al, bl) => (a::al, b::bl)) ([], [])
+
+@[csimp] theorem unzip_eq_unzipTR : @unzip = @unzipTR := by
+  funext α β l; simp [unzipTR]; induction l <;> simp [*]
+
+/-- Tail recursive version of `enumFrom`. -/
+def enumFromTR (n : Nat) (l : List α) : List (Nat × α) :=
+  let arr := l.toArray
+  (arr.foldr (fun a (n, acc) => (n-1, (n-1, a) :: acc)) (n + arr.size, [])).2
+
+@[csimp] theorem enumFrom_eq_enumFromTR : @enumFrom = @enumFromTR := by
+  funext α n l; simp [enumFromTR, -Array.size_toArray]
+  let f := fun (a : α) (n, acc) => (n-1, (n-1, a) :: acc)
+  let rec go : ∀ l n, l.foldr f (n + l.length, []) = (n, enumFrom n l)
+    | [], n => rfl
+    | a::as, n => by
+      rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., foldr, go as]
+      simp [enumFrom, f]
+  rw [Array.foldr_eq_foldr_data]
+  simp [go]
+
+theorem replicateTR_loop_eq : ∀ n, replicateTR.loop a n acc = replicate n a ++ acc
+  | 0 => rfl
+  | n+1 => by rw [← replicateTR_loop_replicate_eq _ 1 n, replicate, replicate,
+    replicateTR.loop, replicateTR_loop_eq n, replicateTR_loop_eq n, append_assoc]; rfl
+
+/-- Tail recursive version of `dropLast`. -/
+@[inline] def dropLastTR (l : List α) : List α := l.toArray.pop.toList
+
+@[csimp] theorem dropLast_eq_dropLastTR : @dropLast = @dropLastTR := by
+  funext α l; simp [dropLastTR]
+
+/-- Tail recursive version of `intersperse`. -/
+def intersperseTR (sep : α) : List α → List α
+  | [] => []
+  | [x] => [x]
+  | x::y::xs => x :: sep :: y :: xs.foldr (fun a r => sep :: a :: r) []
+
+@[csimp] theorem intersperse_eq_intersperseTR : @intersperse = @intersperseTR := by
+  funext α sep l; simp [intersperseTR]
+  match l with
+  | [] | [_] => rfl
+  | x::y::xs => simp [intersperse]; induction xs generalizing y <;> simp [*]
+
+/-- Tail recursive version of `intercalate`. -/
+def intercalateTR (sep : List α) : List (List α) → List α
+  | [] => []
+  | [x] => x
+  | x::xs => go sep.toArray x xs #[]
+where
+  /-- Auxiliary for `intercalateTR`:
+  `intercalateTR.go sep x xs acc = acc.toList ++ intercalate sep.toList (x::xs)` -/
+  go (sep : Array α) : List α → List (List α) → Array α → List α
+  | x, [], acc => acc.toListAppend x
+  | x, y::xs, acc => go sep y xs (acc ++ x ++ sep)
+
+@[csimp] theorem intercalate_eq_intercalateTR : @intercalate = @intercalateTR := by
+  funext α sep l; simp [intercalate, intercalateTR]
+  match l with
+  | [] => rfl
+  | [_] => simp
+  | x::y::xs =>
+    let rec go {acc x} : ∀ xs,
+      intercalateTR.go sep.toArray x xs acc = acc.data ++ join (intersperse sep (x::xs))
+    | [] => by simp [intercalateTR.go]
+    | _::_ => by simp [intercalateTR.go, go]
+    simp [intersperse, go]
+
+end List

src/Init/Data/List/Lemmas.lean

@@ -266,6 +266,12 @@ theorem get?_reverse {l : List α} (i) (h : i < length l) :
     rw [Nat.add_sub_of_le (Nat.le_sub_one_of_lt h),
       Nat.sub_add_cancel (Nat.lt_of_le_of_lt (Nat.zero_le _) h)]
 
+@[simp] theorem getD_nil : getD [] n d = d := rfl
+
+@[simp] theorem getD_cons_zero : getD (x :: xs) 0 d = x := rfl
+
+@[simp] theorem getD_cons_succ : getD (x :: xs) (n + 1) d = getD xs n d := rfl
+
 /-! ### take and drop -/
 
 @[simp] theorem take_append_drop : ∀ (n : Nat) (l : List α), take n l ++ drop n l = l
@@ -705,3 +711,5 @@ theorem minimum?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ ·
   | _ :: l, i + 1, j + 1 => by
     have g : i ≠ j := h ∘ congrArg (· + 1)
     simp [get_set_ne l g]
+
+end List

src/Init/Data/Ord.lean

@@ -6,6 +6,7 @@ Authors: Dany Fabian, Sebastian Ullrich
 
 prelude
 import Init.Data.String
+import Init.Data.Array.Basic
 
 inductive Ordering where
   | lt | eq | gt
@@ -87,11 +88,24 @@ def isGE : Ordering → Bool
 
 end Ordering
 
+/--
+Yields an `Ordering` s.t. `x < y` corresponds to `Ordering.lt` / `Ordering.gt` and
+`x = y` corresponds to `Ordering.eq`.
+-/
 @[inline] def compareOfLessAndEq {α} (x y : α) [LT α] [Decidable (x < y)] [DecidableEq α] : Ordering :=
   if x < y then Ordering.lt
   else if x = y then Ordering.eq
   else Ordering.gt
 
+/--
+Yields an `Ordering` s.t. `x < y` corresponds to `Ordering.lt` / `Ordering.gt` and
+`x == y` corresponds to `Ordering.eq`.
+-/
+@[inline] def compareOfLessAndBEq {α} (x y : α) [LT α] [Decidable (x < y)] [BEq α] : Ordering :=
+  if x < y then .lt
+  else if x == y then .eq
+  else .gt
+
 /--
 Compare `a` and `b` lexicographically by `cmp₁` and `cmp₂`. `a` and `b` are
 first compared by `cmp₁`. If this returns 'equal', `a` and `b` are compared
@@ -105,6 +119,7 @@ class Ord (α : Type u) where
 
 export Ord (compare)
 
+set_option linter.unusedVariables false in  -- allow specifying `ord` explicitly
 /--
 Compare `x` and `y` by comparing `f x` and `f y`.
 -/
@@ -147,6 +162,13 @@ instance : Ord USize where
 instance : Ord Char where
   compare x y := compareOfLessAndEq x y
 
+instance [Ord α] : Ord (Option α) where
+  compare
+  | none,   none   => .eq
+  | none,   some _ => .lt
+  | some _, none   => .gt
+  | some x, some y => compare x y
+
 /-- The lexicographic order on pairs. -/
 def lexOrd [Ord α] [Ord β] : Ord (α × β) where
   compare p1 p2 := match compare p1.1 p2.1 with
@@ -194,7 +216,7 @@ protected def opposite (ord : Ord α) : Ord α where
 /--
 `ord.on f` compares `x` and `y` by comparing `f x` and `f y` according to `ord`.
 -/
-protected def on (ord : Ord β) (f : α → β) : Ord α where
+protected def on (_ : Ord β) (f : α → β) : Ord α where
   compare := compareOn f
 
 /--
@@ -210,4 +232,13 @@ returns 'equal', by `ord₂`.
 protected def lex' (ord₁ ord₂ : Ord α) : Ord α where
   compare := compareLex ord₁.compare ord₂.compare
 
+/--
+Creates an order which compares elements of an `Array` in lexicographic order.
+-/
+protected def arrayOrd [a : Ord α] : Ord (Array α) where
+  compare x y :=
+    let _ : LT α := a.toLT
+    let _ : BEq α := a.toBEq
+    compareOfLessAndBEq x.toList y.toList
+
 end Ord

src/Init/Data/String/Extra.lean

@@ -62,4 +62,40 @@ namespace Iterator
 
 end Iterator
 
+private def findLeadingSpacesSize (s : String) : Nat :=
+  let it := s.iter
+  let it := it.find (· == '\n') |>.next
+  consumeSpaces it 0 s.length
+where
+  consumeSpaces (it : String.Iterator) (curr min : Nat) : Nat :=
+    if it.atEnd then min
+    else if it.curr == ' ' || it.curr == '\t' then consumeSpaces it.next (curr + 1) min
+    else if it.curr == '\n' then findNextLine it.next min
+    else findNextLine it.next (Nat.min curr min)
+  findNextLine (it : String.Iterator) (min : Nat) : Nat :=
+    if it.atEnd then min
+    else if it.curr == '\n' then consumeSpaces it.next 0 min
+    else findNextLine it.next min
+
+private def removeNumLeadingSpaces (n : Nat) (s : String) : String :=
+  consumeSpaces n s.iter ""
+where
+  consumeSpaces (n : Nat) (it : String.Iterator) (r : String) : String :=
+     match n with
+     | 0 => saveLine it r
+     | n+1 =>
+       if it.atEnd then r
+       else if it.curr == ' ' || it.curr == '\t' then consumeSpaces n it.next r
+       else saveLine it r
+  termination_by (it, 1)
+  saveLine (it : String.Iterator) (r : String) : String :=
+    if it.atEnd then r
+    else if it.curr == '\n' then consumeSpaces n it.next (r.push '\n')
+    else saveLine it.next (r.push it.curr)
+  termination_by (it, 0)
+
+def removeLeadingSpaces (s : String) : String :=
+  let n := findLeadingSpacesSize s
+  if n == 0 then s else removeNumLeadingSpaces n s
+
 end String

src/Init/Ext.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Mario Carneiro
 -/
 prelude
+import Init.Data.ToString.Macro
 import Init.TacticsExtra
 import Init.RCases
 

src/Init/GetElem.lean

@@ -0,0 +1,173 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Mario Carneiro
+-/
+prelude
+import Init.Util
+
+@[never_extract]
+private def outOfBounds [Inhabited α] : α :=
+  panic! "index out of bounds"
+
+/--
+The class `GetElem coll idx elem valid` implements the `xs[i]` notation.
+Given `xs[i]` with `xs : coll` and `i : idx`, Lean looks for an instance of
+`GetElem coll idx elem valid` and uses this to infer the type of return
+value `elem` and side conditions `valid` required to ensure `xs[i]` yields
+a valid value of type `elem`.
+
+For example, the instance for arrays looks like
+`GetElem (Array α) Nat α (fun xs i => i < xs.size)`.
+
+The proof side-condition `valid xs i` is automatically dispatched by the
+`get_elem_tactic` tactic, which can be extended by adding more clauses to
+`get_elem_tactic_trivial`.
+-/
+class GetElem (coll : Type u) (idx : Type v) (elem : outParam (Type w))
+              (valid : outParam (coll → idx → Prop)) where
+  /--
+  The syntax `arr[i]` gets the `i`'th element of the collection `arr`. If there
+  are proof side conditions to the application, they will be automatically
+  inferred by the `get_elem_tactic` tactic.
+
+  The actual behavior of this class is type-dependent, but here are some
+  important implementations:
+  * `arr[i] : α` where `arr : Array α` and `i : Nat` or `i : USize`: does array
+    indexing with no bounds check and a proof side goal `i < arr.size`.
+  * `l[i] : α` where `l : List α` and `i : Nat`: index into a list, with proof
+    side goal `i < l.length`.
+  * `stx[i] : Syntax` where `stx : Syntax` and `i : Nat`: get a syntax argument,
+    no side goal (returns `.missing` out of range)
+
+  There are other variations on this syntax:
+  * `arr[i]!` is syntax for `getElem! arr i` which should panic and return
+    `default : α` if the index is not valid.
+  * `arr[i]?` is syntax for `getElem?` which should return `none` if the index
+    is not valid.
+  * `arr[i]'h` is syntax for `getElem arr i h` with `h` an explicit proof the
+    index is valid.
+  -/
+  getElem (xs : coll) (i : idx) (h : valid xs i) : elem
+
+  getElem? (xs : coll) (i : idx) [Decidable (valid xs i)] : Option elem :=
+    if h : _ then some (getElem xs i h) else none
+
+  getElem! [Inhabited elem] (xs : coll) (i : idx) [Decidable (valid xs i)] : elem :=
+    match getElem? xs i with | some e => e | none => outOfBounds
+
+export GetElem (getElem getElem! getElem?)
+
+@[inherit_doc getElem]
+syntax:max term noWs "[" withoutPosition(term) "]" : term
+macro_rules | `($x[$i]) => `(getElem $x $i (by get_elem_tactic))
+
+@[inherit_doc getElem]
+syntax term noWs "[" withoutPosition(term) "]'" term:max : term
+macro_rules | `($x[$i]'$h) => `(getElem $x $i $h)
+
+/--
+The syntax `arr[i]?` gets the `i`'th element of the collection `arr` or
+returns `none` if `i` is out of bounds.
+-/
+macro:max x:term noWs "[" i:term "]" noWs "?" : term => `(getElem? $x $i)
+
+/--
+The syntax `arr[i]!` gets the `i`'th element of the collection `arr` and
+panics `i` is out of bounds.
+-/
+macro:max x:term noWs "[" i:term "]" noWs "!" : term => `(getElem! $x $i)
+
+class LawfulGetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w))
+   (dom : outParam (cont → idx → Prop)) [ge : GetElem cont idx elem dom] : Prop where
+
+  getElem?_def (c : cont) (i : idx) [Decidable (dom c i)] :
+    c[i]? = if h : dom c i then some (c[i]'h) else none := by intros; eq_refl
+  getElem!_def [Inhabited elem] (c : cont) (i : idx) [Decidable (dom c i)] :
+    c[i]! = match c[i]? with | some e => e | none => default := by intros; eq_refl
+
+export LawfulGetElem (getElem?_def getElem!_def)
+
+theorem getElem?_pos [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] : c[i]? = some (c[i]'h) := by
+  rw [getElem?_def]
+  exact dif_pos h
+
+theorem getElem?_neg [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]? = none := by
+  rw [getElem?_def]
+  exact dif_neg h
+
+theorem getElem!_pos [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    [Inhabited elem] (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] :
+    c[i]! = c[i]'h := by
+  simp only [getElem!_def, getElem?_def, h]
+
+theorem getElem!_neg [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    [Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]! = default := by
+  simp only [getElem!_def, getElem?_def, h]
+
+namespace Fin
+
+instance instGetElemFinVal [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i where
+  getElem xs i h := getElem xs i.1 h
+  getElem? xs i := getElem? xs i.val
+  getElem! xs i := getElem! xs i.val
+
+instance [GetElem cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] :
+      LawfulGetElem cont (Fin n) elem fun xs i => dom xs i where
+
+  getElem?_def _c _i _d := h.getElem?_def ..
+  getElem!_def _c _i _d := h.getElem!_def ..
+
+@[simp] theorem getElem_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
+    a[i] = a[i.1] := rfl
+
+@[simp] theorem getElem?_fin [h : GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n)
+    [Decidable (Dom a i)] : a[i]? = a[i.1]? := by rfl
+
+@[simp] theorem getElem!_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n)
+    [Decidable (Dom a i)] [Inhabited Elem] : a[i]! = a[i.1]! := rfl
+
+macro_rules
+  | `(tactic| get_elem_tactic_trivial) => `(tactic| apply Fin.val_lt_of_le; get_elem_tactic_trivial; done)
+
+end Fin
+
+namespace List
+
+instance : GetElem (List α) Nat α fun as i => i < as.length where
+  getElem as i h := as.get ⟨i, h⟩
+
+instance : LawfulGetElem (List α) Nat α fun as i => i < as.length where
+
+@[simp] theorem cons_getElem_zero (a : α) (as : List α) (h : 0 < (a :: as).length) : getElem (a :: as) 0 h = a := by
+  rfl
+
+@[simp] theorem cons_getElem_succ (a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: as).length) : getElem (a :: as) (i+1) h = getElem as i (Nat.lt_of_succ_lt_succ h) := by
+  rfl
+
+theorem get_drop_eq_drop (as : List α) (i : Nat) (h : i < as.length) : as[i] :: as.drop (i+1) = as.drop i :=
+  match as, i with
+  | _::_, 0   => rfl
+  | _::_, i+1 => get_drop_eq_drop _ i _
+
+end List
+
+namespace Array
+
+instance : GetElem (Array α) Nat α fun xs i => i < xs.size where
+  getElem xs i h := xs.get ⟨i, h⟩
+
+instance : LawfulGetElem (Array α) Nat α fun xs i => i < xs.size where
+
+end Array
+
+namespace Lean.Syntax
+
+instance : GetElem Syntax Nat Syntax fun _ _ => True where
+  getElem stx i _ := stx.getArg i
+
+instance : LawfulGetElem Syntax Nat Syntax fun _ _ => True where
+
+end Lean.Syntax

src/Init/MacroTrace.lean

@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+
+Extra notation that depends on Init/Meta
+-/
+
+prelude
+import Init.Data.ToString.Macro
+import Init.Meta
+
+namespace Lean
+
+macro "Macro.trace[" id:ident "]" s:interpolatedStr(term) : term =>
+  `(Macro.trace $(quote id.getId.eraseMacroScopes) (s! $s))
+
+end Lean

src/Init/Meta.lean

@@ -9,7 +9,6 @@ prelude
 import Init.MetaTypes
 import Init.Data.Array.Basic
 import Init.Data.Option.BasicAux
-import Init.Data.String.Extra
 
 namespace Lean
 
@@ -105,43 +104,6 @@ def idBeginEscape := '«'
 def idEndEscape   := '»'
 def isIdBeginEscape (c : Char) : Bool := c = idBeginEscape
 def isIdEndEscape (c : Char) : Bool := c = idEndEscape
-
-private def findLeadingSpacesSize (s : String) : Nat :=
-  let it := s.iter
-  let it := it.find (· == '\n') |>.next
-  consumeSpaces it 0 s.length
-where
-  consumeSpaces (it : String.Iterator) (curr min : Nat) : Nat :=
-    if it.atEnd then min
-    else if it.curr == ' ' || it.curr == '\t' then consumeSpaces it.next (curr + 1) min
-    else if it.curr == '\n' then findNextLine it.next min
-    else findNextLine it.next (Nat.min curr min)
-  findNextLine (it : String.Iterator) (min : Nat) : Nat :=
-    if it.atEnd then min
-    else if it.curr == '\n' then consumeSpaces it.next 0 min
-    else findNextLine it.next min
-
-private def removeNumLeadingSpaces (n : Nat) (s : String) : String :=
-  consumeSpaces n s.iter ""
-where
-  consumeSpaces (n : Nat) (it : String.Iterator) (r : String) : String :=
-     match n with
-     | 0 => saveLine it r
-     | n+1 =>
-       if it.atEnd then r
-       else if it.curr == ' ' || it.curr == '\t' then consumeSpaces n it.next r
-       else saveLine it r
-  termination_by (it, 1)
-  saveLine (it : String.Iterator) (r : String) : String :=
-    if it.atEnd then r
-    else if it.curr == '\n' then consumeSpaces n it.next (r.push '\n')
-    else saveLine it.next (r.push it.curr)
-  termination_by (it, 0)
-
-def removeLeadingSpaces (s : String) : String :=
-  let n := findLeadingSpacesSize s
-  if n == 0 then s else removeNumLeadingSpaces n s
-
 namespace Name
 
 def getRoot : Name → Name
@@ -947,6 +909,11 @@ def _root_.Substring.toName (s : Substring) : Name :=
       else
         Name.mkStr n comp
 
+/--
+Converts a `String` to a hierarchical `Name` after splitting it at the dots.
+
+`"a.b".toName` is the name `a.b`, not `«a.b»`. For the latter, use `Name.mkSimple`.
+-/
 def _root_.String.toName (s : String) : Name :=
   s.toSubstring.toName
 
@@ -1227,14 +1194,6 @@ instance : Coe (Lean.Term) (Lean.TSyntax `Lean.Parser.Term.funBinder) where
 
 end Lean.Syntax
 
-set_option linter.unusedVariables.funArgs false in
-/--
-  Gadget for automatic parameter support. This is similar to the `optParam` gadget, but it uses
-  the given tactic.
-  Like `optParam`, this gadget only affects elaboration.
-  For example, the tactic will *not* be invoked during type class resolution. -/
-abbrev autoParam.{u} (α : Sort u) (tactic : Lean.Syntax) : Sort u := α
-
 /-! # Helper functions for manipulating interpolated strings -/
 
 namespace Lean.Syntax

src/Init/NotationExtra.lean

@@ -6,14 +6,12 @@ Authors: Leonardo de Moura
 Extra notation that depends on Init/Meta
 -/
 prelude
-import Init.Meta
+import Init.Data.ToString.Basic
 import Init.Data.Array.Subarray
-import Init.Data.ToString
 import Init.Conv
-namespace Lean
+import Init.Meta
 
-macro "Macro.trace[" id:ident "]" s:interpolatedStr(term) : term =>
-  `(Macro.trace $(quote id.getId.eraseMacroScopes) (s! $s))
+namespace Lean
 
 -- Auxiliary parsers and functions for declaring notation with binders
 
@@ -224,35 +222,35 @@ macro tk:"calc" steps:calcSteps : conv =>
   | _ => throw ()
 
 @[app_unexpander Name.mkStr1] def unexpandMkStr1 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a.getString}"]
+  | `($(_) $a:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++  a.getString)]
   | _  => throw ()
 
 @[app_unexpander Name.mkStr2] def unexpandMkStr2 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a1:str $a2:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}"]
+  | `($(_) $a1:str $a2:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString)]
   | _  => throw ()
 
 @[app_unexpander Name.mkStr3] def unexpandMkStr3 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a1:str $a2:str $a3:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}"]
+  | `($(_) $a1:str $a2:str $a3:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString)]
   | _  => throw ()
 
 @[app_unexpander Name.mkStr4] def unexpandMkStr4 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a1:str $a2:str $a3:str $a4:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}"]
+  | `($(_) $a1:str $a2:str $a3:str $a4:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString ++ "." ++ a4.getString)]
   | _  => throw ()
 
 @[app_unexpander Name.mkStr5] def unexpandMkStr5 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}.{a5.getString}"]
+  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString ++ "." ++ a4.getString ++ "." ++ a5.getString)]
   | _  => throw ()
 
 @[app_unexpander Name.mkStr6] def unexpandMkStr6 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}.{a5.getString}.{a6.getString}"]
+  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString ++ "." ++ a4.getString ++ "." ++ a5.getString ++ "." ++ a6.getString)]
   | _  => throw ()
 
 @[app_unexpander Name.mkStr7] def unexpandMkStr7 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str $a7:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}.{a5.getString}.{a6.getString}.{a7.getString}"]
+  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str $a7:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString ++ "." ++ a4.getString ++ "." ++ a5.getString ++ "." ++ a6.getString ++ "." ++ a7.getString)]
   | _  => throw ()
 
 @[app_unexpander Name.mkStr8] def unexpandMkStr8 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str $a7:str $a8:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}.{a5.getString}.{a6.getString}.{a7.getString}.{a8.getString}"]
+  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str $a7:str $a8:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString ++ "." ++ a4.getString ++ "." ++ a5.getString ++ "." ++ a6.getString ++ "." ++ a7.getString ++ "." ++ a8.getString)]
   | _  => throw ()
 
 @[app_unexpander Array.empty] def unexpandArrayEmpty : Lean.PrettyPrinter.Unexpander

src/Init/Omega/Int.lean

@@ -50,6 +50,9 @@ theorem ofNat_shiftLeft_eq {x y : Nat} : (x <<< y : Int) = (x : Int) * (2 ^ y :
 theorem ofNat_shiftRight_eq_div_pow {x y : Nat} : (x >>> y : Int) = (x : Int) / (2 ^ y : Nat) := by
   simp only [Nat.shiftRight_eq_div_pow, Int.ofNat_ediv]
 
+theorem emod_ofNat_nonneg {x : Nat} {y : Int} : 0 ≤ (x : Int) % y :=
+  Int.ofNat_zero_le _
+
 -- FIXME these are insane:
 theorem lt_of_not_ge {x y : Int} (h : ¬ (x ≤ y)) : y < x := Int.not_le.mp h
 theorem lt_of_not_le {x y : Int} (h : ¬ (x ≤ y)) : y < x := Int.not_le.mp h

src/Init/Omega/LinearCombo.lean

@@ -5,6 +5,7 @@ Authors: Scott Morrison
 -/
 prelude
 import Init.Omega.Coeffs
+import Init.Data.ToString.Macro
 
 /-!
 # Linear combinations

src/Init/Prelude.lean

@@ -488,6 +488,7 @@ attribute [unbox] Prod
 Similar to `Prod`, but `α` and `β` can be propositions.
 We use this type internally to automatically generate the `brecOn` recursor.
 -/
+@[pp_using_anonymous_constructor]
 structure PProd (α : Sort u) (β : Sort v) where
   /-- The first projection out of a pair. if `p : PProd α β` then `p.1 : α`. -/
   fst : α
@@ -509,6 +510,7 @@ structure MProd (α β : Type u) where
 constructed and destructed like a pair: if `ha : a` and `hb : b` then
 `⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.
 -/
+@[pp_using_anonymous_constructor]
 structure And (a b : Prop) : Prop where
   /-- `And.intro : a → b → a ∧ b` is the constructor for the And operation. -/
   intro ::
@@ -575,6 +577,7 @@ a pair-like type, so if you have `x : α` and `h : p x` then
 `⟨x, h⟩ : {x // p x}`. An element `s : {x // p x}` will coerce to `α` but
 you can also make it explicit using `s.1` or `s.val`.
 -/
+@[pp_using_anonymous_constructor]
 structure Subtype {α : Sort u} (p : α → Prop) where
   /-- If `s : {x // p x}` then `s.val : α` is the underlying element in the base
   type. You can also write this as `s.1`, or simply as `s` when the type is
@@ -1194,7 +1197,12 @@ class HDiv (α : Type u) (β : Type v) (γ : outParam (Type w)) where
   /-- `a / b` computes the result of dividing `a` by `b`.
   The meaning of this notation is type-dependent.
   * For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
-  * For `Nat` and `Int`, `a / b` rounds toward 0.
+  * For `Nat`, `a / b` rounds downwards.
+  * For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
+    It is implemented as `Int.ediv`, the unique function satisfiying
+    `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
+    Other rounding conventions are available using the functions
+    `Int.fdiv` (floor rounding) and `Int.div` (truncation rounding).
   * For `Float`, `a / 0` follows the IEEE 754 semantics for division,
     usually resulting in `inf` or `nan`. -/
   hDiv : α → β → γ
@@ -1206,7 +1214,8 @@ This enables the notation `a % b : γ` where `a : α`, `b : β`.
 class HMod (α : Type u) (β : Type v) (γ : outParam (Type w)) where
   /-- `a % b` computes the remainder upon dividing `a` by `b`.
   The meaning of this notation is type-dependent.
-  * For `Nat` and `Int`, `a % 0` is defined to be `a`. -/
+  * For `Nat` and `Int` it satisfies `a % b + b * (a / b) = a`,
+    and `a % 0` is defined to be `a`. -/
   hMod : α → β → γ
 
 /--
@@ -1809,6 +1818,7 @@ theorem System.Platform.numBits_eq : Or (Eq numBits 32) (Eq numBits 64) :=
 `Fin n` is a natural number `i` with the constraint that `0 ≤ i < n`.
 It is the "canonical type with `n` elements".
 -/
+@[pp_using_anonymous_constructor]
 structure Fin (n : Nat) where
   /-- If `i : Fin n`, then `i.val : ℕ` is the described number. It can also be
   written as `i.1` or just `i` when the target type is known. -/
@@ -2533,43 +2543,6 @@ def panic {α : Type u} [Inhabited α] (msg : String) : α :=
 -- TODO: this be applied directly to `Inhabited`'s definition when we remove the above workaround
 attribute [nospecialize] Inhabited
 
-/--
-The class `GetElem cont idx elem dom` implements the `xs[i]` notation.
-When you write this, given `xs : cont` and `i : idx`, Lean looks for an instance
-of `GetElem cont idx elem dom`. Here `elem` is the type of `xs[i]`, while
-`dom` is whatever proof side conditions are required to make this applicable.
-For example, the instance for arrays looks like
-`GetElem (Array α) Nat α (fun xs i => i < xs.size)`.
-
-The proof side-condition `dom xs i` is automatically dispatched by the
-`get_elem_tactic` tactic, which can be extended by adding more clauses to
-`get_elem_tactic_trivial`.
--/
-class GetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w)) (dom : outParam (cont → idx → Prop)) where
-  /--
-  The syntax `arr[i]` gets the `i`'th element of the collection `arr`.
-  If there are proof side conditions to the application, they will be automatically
-  inferred by the `get_elem_tactic` tactic.
-
-  The actual behavior of this class is type-dependent,
-  but here are some important implementations:
-  * `arr[i] : α` where `arr : Array α` and `i : Nat` or `i : USize`:
-    does array indexing with no bounds check and a proof side goal `i < arr.size`.
-  * `l[i] : α` where `l : List α` and `i : Nat`: index into a list,
-    with proof side goal `i < l.length`.
-  * `stx[i] : Syntax` where `stx : Syntax` and `i : Nat`: get a syntax argument,
-    no side goal (returns `.missing` out of range)
-
-  There are other variations on this syntax:
-  * `arr[i]`: proves the proof side goal by `get_elem_tactic`
-  * `arr[i]!`: panics if the side goal is false
-  * `arr[i]?`: returns `none` if the side goal is false
-  * `arr[i]'h`: uses `h` to prove the side goal
-  -/
-  getElem (xs : cont) (i : idx) (h : dom xs i) : elem
-
-export GetElem (getElem)
-
 /--
 `Array α` is the type of [dynamic arrays](https://en.wikipedia.org/wiki/Dynamic_array)
 with elements from `α`. This type has special support in the runtime.
@@ -2627,9 +2600,6 @@ def Array.get {α : Type u} (a : @& Array α) (i : @& Fin a.size) : α :=
 def Array.get! {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
   Array.getD a i default
 
-instance : GetElem (Array α) Nat α fun xs i => LT.lt i xs.size where
-  getElem xs i h := xs.get ⟨i, h⟩
-
 /--
 Push an element onto the end of an array. This is amortized O(1) because
 `Array α` is internally a dynamic array.
@@ -2745,7 +2715,7 @@ def List.redLength : List α → Nat
 /-- Convert a `List α` into an `Array α`. This is O(n) in the length of the list.  -/
 -- This function is exported to C, where it is called by `Array.mk`
 -- (the constructor) to implement this functionality.
-@[inline, match_pattern, export lean_list_to_array]
+@[inline, match_pattern, pp_nodot, export lean_list_to_array]
 def List.toArray (as : List α) : Array α :=
   as.toArrayAux (Array.mkEmpty as.redLength)
 
@@ -3482,20 +3452,31 @@ instance : Hashable String where
 namespace Lean
 
 /--
-Hierarchical names. We use hierarchical names to name declarations and
-for creating unique identifiers for free variables and metavariables.
+Hierarchical names consist of a sequence of components, each of
+which is either a string or numeric, that are written separated by dots (`.`).
 
-You can create hierarchical names using the following quotation notation.
+Hierarchical names are used to name declarations and for creating
+unique identifiers for free variables and metavariables.
+
+You can create hierarchical names using a backtick:
 ```
 `Lean.Meta.whnf
 ```
-It is short for `.str (.str (.str .anonymous "Lean") "Meta") "whnf"`
-You can use double quotes to request Lean to statically check whether the name
+It is short for `.str (.str (.str .anonymous "Lean") "Meta") "whnf"`.
+
+You can use double backticks to request Lean to statically check whether the name
 corresponds to a Lean declaration in scope.
 ```
 ``Lean.Meta.whnf
 ```
 If the name is not in scope, Lean will report an error.
+
+There are two ways to convert a `String` to a `Name`:
+
+ 1. `Name.mkSimple` creates a name with a single string component.
+
+ 2. `String.toName` first splits the string into its dot-separated
+    components, and then creates a hierarchical name.
 -/
 inductive Name where
   /-- The "anonymous" name. -/
@@ -3546,7 +3527,9 @@ abbrev mkNum (p : Name) (v : Nat) : Name :=
   Name.num p v
 
 /--
-Short for `.str .anonymous s`.
+Converts a `String` to a `Name` without performing any parsing. `mkSimple s` is short for `.str .anonymous s`.
+
+This means that `mkSimple "a.b"` is the name `«a.b»`, not `a.b`.
 -/
 abbrev mkSimple (s : String) : Name :=
   .str .anonymous s
@@ -3884,9 +3867,6 @@ def getArg (stx : Syntax) (i : Nat) : Syntax :=
   | Syntax.node _ _ args => args.getD i Syntax.missing
   | _                    => Syntax.missing
 
-instance : GetElem Syntax Nat Syntax fun _ _ => True where
-  getElem stx i _ := stx.getArg i
-
 /-- Gets the list of arguments of the syntax node, or `#[]` if it's not a `node`. -/
 def getArgs (stx : Syntax) : Array Syntax :=
   match stx with

src/Init/PropLemmas.lean

@@ -23,6 +23,9 @@ set_option linter.missingDocs true -- keep it documented
 @[simp] theorem eq_true_eq_id : Eq True = id := by
   funext _; simp only [true_iff, id_def, eq_iff_iff]
 
+theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) : HEq hp hq := by
+  cases propext (iff_of_true hp hq); rfl
+
 /-! ## not -/
 
 theorem not_not_em (a : Prop) : ¬¬(a ∨ ¬a) := fun h => h (.inr (h ∘ .inl))

src/Init/RCases.lean

@@ -5,7 +5,8 @@ Authors: Mario Carneiro, Jacob von Raumer
 -/
 prelude
 import Init.Tactics
-import Init.NotationExtra
+import Init.Meta
+
 
 /-!
 # Recursive cases (`rcases`) tactic and related tactics
@@ -127,7 +128,7 @@ the input expression). An `rcases` pattern has the following grammar:
   and so on.
 * A `@` before a tuple pattern as in `@⟨p1, p2, p3⟩` will bind all arguments in the constructor,
   while leaving the `@` off will only use the patterns on the explicit arguments.
-* An alteration pattern `p1 | p2 | p3`, which matches an inductive type with multiple constructors,
+* An alternation pattern `p1 | p2 | p3`, which matches an inductive type with multiple constructors,
   or a nested disjunction like `a ∨ b ∨ c`.
 
 A pattern like `⟨a, b, c⟩ | ⟨d, e⟩` will do a split over the inductive datatype,

src/Init/Simproc.lean

@@ -11,22 +11,23 @@ namespace Lean.Parser
 A user-defined simplification procedure used by the `simp` tactic, and its variants.
 Here is an example.
 ```lean
-simproc reduce_add (_ + _) := fun e => do
-  unless (e.isAppOfArity ``HAdd.hAdd 6) do return none
-  let some n ← getNatValue? (e.getArg! 4) | return none
-  let some m ← getNatValue? (e.getArg! 5) | return none
-  return some (.done { expr := mkNatLit (n+m) })
+theorem and_false_eq {p : Prop} (q : Prop) (h : p = False) : (p ∧ q) = False := by simp [*]
+
+open Lean Meta Simp
+simproc ↓ shortCircuitAnd (And _ _) := fun e => do
+  let_expr And p q := e | return .continue
+  let r ← simp p
+  let_expr False := r.expr | return .continue
+  let proof ← mkAppM ``and_false_eq #[q, (← r.getProof)]
+  return .done { expr := r.expr, proof? := some proof }
 ```
-The `simp` tactic invokes `reduce_add` whenever it finds a term of the form `_ + _`.
+The `simp` tactic invokes `shortCircuitAnd` whenever it finds a term of the form `And _ _`.
 The simplification procedures are stored in an (imperfect) discrimination tree.
 The procedure should **not** assume the term `e` perfectly matches the given pattern.
 The body of a simplification procedure must have type `Simproc`, which is an alias for
-`Expr → SimpM (Option Step)`.
+`Expr → SimpM Step`
 You can instruct the simplifier to apply the procedure before its sub-expressions
-have been simplified by using the modifier `↓` before the procedure name. Example.
-```lean
-simproc ↓ reduce_add (_ + _) := fun e => ...
-```
+have been simplified by using the modifier `↓` before the procedure name.
 Simplification procedures can be also scoped or local.
 -/
 syntax (docComment)? attrKind "simproc " (Tactic.simpPre <|> Tactic.simpPost)? ("[" ident,* "]")? ident " (" term ")" " := " term : command

src/Init/System/FilePath.lean

@@ -73,7 +73,21 @@ private def posOfLastSep (p : FilePath) : Option String.Pos :=
   p.toString.revFind pathSeparators.contains
 
 def parent (p : FilePath) : Option FilePath :=
-  FilePath.mk <$> p.toString.extract {} <$> posOfLastSep p
+  let extractParentPath := FilePath.mk <$> p.toString.extract {} <$> posOfLastSep p
+  if p.isAbsolute then
+    let lengthOfRootDirectory := if pathSeparators.contains p.toString.front then 1 else 3
+    if p.toString.length == lengthOfRootDirectory then
+      -- `p` is a root directory
+      none
+    else if posOfLastSep p == String.Pos.mk (lengthOfRootDirectory - 1) then
+      -- `p` is a direct child of the root
+      some ⟨p.toString.extract 0 ⟨lengthOfRootDirectory⟩⟩
+    else
+      -- `p` is an absolute path with at least two subdirectories
+      extractParentPath
+  else
+    -- `p` is a relative path
+    extractParentPath
 
 def fileName (p : FilePath) : Option String :=
   let lastPart := match posOfLastSep p with

src/Init/Tactics.lean

@@ -224,7 +224,7 @@ the first matching constructor, or else fails.
 syntax (name := constructor) "constructor" : tactic
 
 /--
-Applies the second constructor when
+Applies the first constructor when
 the goal is an inductive type with exactly two constructors, or fails otherwise.
 ```
 example : True ∨ False := by
@@ -354,6 +354,9 @@ macro:1 x:tactic tk:" <;> " y:tactic:2 : tactic => `(tactic|
     with_annotate_state $tk skip
     all_goals $y:tactic)
 
+/-- `fail msg` is a tactic that always fails, and produces an error using the given message. -/
+syntax (name := fail) "fail" (ppSpace str)? : tactic
+
 /-- `eq_refl` is equivalent to `exact rfl`, but has a few optimizations. -/
 syntax (name := eqRefl) "eq_refl" : tactic
 
@@ -365,10 +368,23 @@ for new reflexive relations.
 Remark: `rfl` is an extensible tactic. We later add `macro_rules` to try different
 reflexivity theorems (e.g., `Iff.rfl`).
 -/
-macro "rfl" : tactic => `(tactic| eq_refl)
+macro "rfl" : tactic => `(tactic| fail "The rfl tactic failed. Possible reasons:
+- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
+- The arguments of the relation are not equal.
+Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.")
 
+macro_rules | `(tactic| rfl) => `(tactic| eq_refl)
 macro_rules | `(tactic| rfl) => `(tactic| exact HEq.rfl)
 
+/--
+This tactic applies to a goal whose target has the form `x ~ x`,
+where `~` is a reflexive relation other than `=`,
+that is, a relation which has a reflexive lemma tagged with the attribute @[refl].
+-/
+syntax (name := applyRfl) "apply_rfl" : tactic
+
+macro_rules | `(tactic| rfl) => `(tactic| apply_rfl)
+
 /--
 `rfl'` is similar to `rfl`, but disables smart unfolding and unfolds all kinds of definitions,
 theorems included (relevant for declarations defined by well-founded recursion).
@@ -899,9 +915,6 @@ example : ∀ x : Nat, x = x := by unhygienic
 -/
 macro "unhygienic " t:tacticSeq : tactic => `(tactic| set_option tactic.hygienic false in $t)
 
-/-- `fail msg` is a tactic that always fails, and produces an error using the given message. -/
-syntax (name := fail) "fail" (ppSpace str)? : tactic
-
 /--
 `checkpoint tac` acts the same as `tac`, but it caches the input and output of `tac`,
 and if the file is re-elaborated and the input matches, the tactic is not re-run and
@@ -1310,6 +1323,22 @@ used when closing the goal.
 -/
 syntax (name := apply?) "apply?" (" using " (colGt term),+)? : tactic
 
+/--
+Syntax for excluding some names, e.g. `[-my_lemma, -my_theorem]`.
+-/
+syntax rewrites_forbidden := " [" (("-" ident),*,?) "]"
+
+/--
+`rw?` tries to find a lemma which can rewrite the goal.
+
+`rw?` should not be left in proofs; it is a search tool, like `apply?`.
+
+Suggestions are printed as `rw [h]` or `rw [← h]`.
+
+You can use `rw? [-my_lemma, -my_theorem]` to prevent `rw?` using the named lemmas.
+-/
+syntax (name := rewrites?) "rw?" (ppSpace location)? (rewrites_forbidden)? : tactic
+
 /--
 `show_term tac` runs `tac`, then prints the generated term in the form
 "exact X Y Z" or "refine X ?_ Z" if there are remaining subgoals.
@@ -1493,16 +1522,16 @@ macro "get_elem_tactic" : tactic =>
   - Use `a[i]'h` notation instead, where `h` is a proof that index is valid"
    )
 
-@[inherit_doc getElem]
-syntax:max term noWs "[" withoutPosition(term) "]" : term
-macro_rules | `($x[$i]) => `(getElem $x $i (by get_elem_tactic))
-
-@[inherit_doc getElem]
-syntax term noWs "[" withoutPosition(term) "]'" term:max : term
-macro_rules | `($x[$i]'$h) => `(getElem $x $i $h)
-
 /--
 Searches environment for definitions or theorems that can be substituted in
 for `exact?% to solve the goal.
  -/
 syntax (name := Lean.Parser.Syntax.exact?) "exact?%" : term
+
+set_option linter.unusedVariables.funArgs false in
+/--
+  Gadget for automatic parameter support. This is similar to the `optParam` gadget, but it uses
+  the given tactic.
+  Like `optParam`, this gadget only affects elaboration.
+  For example, the tactic will *not* be invoked during type class resolution. -/
+abbrev autoParam.{u} (α : Sort u) (tactic : Lean.Syntax) : Sort u := α

src/Init/Util.lean

@@ -73,19 +73,6 @@ def withPtrEq {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () =
 @[implemented_by withPtrAddrUnsafe]
 def withPtrAddr {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β := k 0
 
-@[never_extract]
-private def outOfBounds [Inhabited α] : α :=
-  panic! "index out of bounds"
-
-@[inline] def getElem! [GetElem cont idx elem dom] [Inhabited elem] (xs : cont) (i : idx) [Decidable (dom xs i)] : elem :=
-  if h : _ then getElem xs i h else outOfBounds
-
-@[inline] def getElem? [GetElem cont idx elem dom] (xs : cont) (i : idx) [Decidable (dom xs i)] : Option elem :=
-  if h : _ then some (getElem xs i h) else none
-
-macro:max x:term noWs "[" i:term "]" noWs "?" : term => `(getElem? $x $i)
-macro:max x:term noWs "[" i:term "]" noWs "!" : term => `(getElem! $x $i)
-
 /--
   Marks given value and its object graph closure as multi-threaded if currently
   marked single-threaded. This will make reference counter updates atomic and

src/Lean/AuxRecursor.lean

@@ -34,7 +34,7 @@ def isAuxRecursor (env : Environment) (declName : Name) : Bool :=
   || declName == ``Eq.ndrec
   || declName == ``Eq.ndrecOn
 
-def isAuxRecursorWithSuffix (env : Environment) (declName : Name) (suffix : Name) : Bool :=
+def isAuxRecursorWithSuffix (env : Environment) (declName : Name) (suffix : String) : Bool :=
   match declName with
   | .str _ s => s == suffix && isAuxRecursor env declName
   | _ => false

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -663,7 +663,7 @@ def emitExternCall (builder : LLVM.Builder llvmctx)
     (name : String := "") : M llvmctx (LLVM.Value llvmctx) :=
   match getExternEntryFor extData `c with
   | some (ExternEntry.standard _ extFn) => emitSimpleExternalCall builder extFn ps ys retty name
-  | some (ExternEntry.inline "llvm" _pat) => throw "Unimplemented codegen of inline LLVM"
+  | some (ExternEntry.inline `llvm _pat) => throw "Unimplemented codegen of inline LLVM"
   | some (ExternEntry.inline _ pat) => throw s!"Cannot codegen non-LLVM inline code '{pat}'."
   | some (ExternEntry.foreign _ extFn)  => emitSimpleExternalCall builder extFn ps ys retty name
   | _ => throw s!"Failed to emit extern application '{f}'."

src/Lean/Compiler/LCNF/JoinPoints.lean

@@ -346,7 +346,7 @@ We call this whenever we enter a new local function. It clears both the
 current join point and the list of candidates since we can't lift join
 points outside of functions as explained in `mergeJpContextIfNecessary`.
 -/
-def withNewFunScope (decl : FunDecl) (x : ExtendM α): ExtendM α := do
+def withNewFunScope (x : ExtendM α): ExtendM α := do
   withReader (fun ctx => { ctx with currentJp? := none, candidates := {} }) do
     withNewScope do
       x
@@ -412,7 +412,7 @@ where
       withNewCandidate decl.fvarId do
         return Code.updateFun! code decl (← go k)
     | .fun decl k =>
-      let decl ← withNewFunScope decl do
+      let decl ← withNewFunScope do
         decl.updateValue (← go decl.value)
       withNewCandidate decl.fvarId do
         return Code.updateFun! code decl (← go k)

src/Lean/CoreM.lean

@@ -219,7 +219,7 @@ def checkMaxHeartbeatsCore (moduleName : String) (optionName : Name) (max : Nat)
   unless max == 0 do
     let numHeartbeats ← IO.getNumHeartbeats
     if numHeartbeats - (← read).initHeartbeats > max then
-      throwMaxHeartbeat moduleName optionName max
+      throwMaxHeartbeat (.mkSimple moduleName) optionName max
 
 def checkMaxHeartbeats (moduleName : String) : CoreM Unit := do
   checkMaxHeartbeatsCore moduleName `maxHeartbeats (← read).maxHeartbeats

src/Lean/Data/HashMap.lean

@@ -212,6 +212,8 @@ def insertIfNew (m : HashMap α β) (a : α) (b : β) : HashMap α β × Option
 instance : GetElem (HashMap α β) α (Option β) fun _ _ => True where
   getElem m k _ := m.find? k
 
+instance : LawfulGetElem (HashMap α β) α (Option β) fun _ _ => True where
+
 @[inline] def contains (m : HashMap α β) (a : α) : Bool :=
   match m with
   | ⟨ m, _ ⟩ => m.contains a

src/Lean/Data/Json/Basic.lean

@@ -10,6 +10,8 @@ import Init.Data.Range
 import Init.Data.OfScientific
 import Init.Data.Hashable
 import Lean.Data.RBMap
+import Init.Data.ToString.Macro
+
 namespace Lean
 
 -- mantissa * 10^-exponent

src/Lean/Data/Lsp/Basic.lean

@@ -52,7 +52,7 @@ instance : LE Range := leOfOrd
 structure Location where
   uri : DocumentUri
   range : Range
-  deriving Inhabited, BEq, ToJson, FromJson
+  deriving Inhabited, BEq, ToJson, FromJson, Ord
 
 structure LocationLink where
   originSelectionRange? : Option Range

src/Lean/Data/Lsp/Diagnostics.lean

@@ -25,7 +25,7 @@ open Json
 
 inductive DiagnosticSeverity where
   | error | warning | information | hint
-  deriving Inhabited, BEq
+  deriving Inhabited, BEq, Ord
 
 instance : FromJson DiagnosticSeverity := ⟨fun j =>
   match j.getNat? with
@@ -45,7 +45,7 @@ instance : ToJson DiagnosticSeverity := ⟨fun
 inductive DiagnosticCode where
   | int (i : Int)
   | string (s : String)
-  deriving Inhabited, BEq
+  deriving Inhabited, BEq, Ord
 
 instance : FromJson DiagnosticCode := ⟨fun
   | num (i : Int) => return DiagnosticCode.int i
@@ -62,7 +62,7 @@ inductive DiagnosticTag where
   | unnecessary
   /-- Deprecated or obsolete code. Rendered with a strike-through. -/
   | deprecated
-  deriving Inhabited, BEq
+  deriving Inhabited, BEq, Ord
 
 instance : FromJson DiagnosticTag := ⟨fun j =>
   match j.getNat? with
@@ -80,7 +80,7 @@ instance : ToJson DiagnosticTag := ⟨fun
 structure DiagnosticRelatedInformation where
   location : Location
   message : String
-  deriving Inhabited, BEq, ToJson, FromJson
+  deriving Inhabited, BEq, ToJson, FromJson, Ord
 
 /-- Represents a diagnostic, such as a compiler error or warning. Diagnostic objects are only valid in the scope of a resource.
 
@@ -113,6 +113,29 @@ structure DiagnosticWith (α : Type) where
 def DiagnosticWith.fullRange (d : DiagnosticWith α) : Range :=
   d.fullRange?.getD d.range
 
+local instance [Ord α] : Ord (Array α) := Ord.arrayOrd
+
+/-- Restriction of `DiagnosticWith` to properties that are displayed to users in the InfoView. -/
+private structure DiagnosticWith.UserVisible (α : Type) where
+  range               : Range
+  fullRange?          : Option Range
+  severity?           : Option DiagnosticSeverity
+  code?               : Option DiagnosticCode
+  source?             : Option String
+  message             : α
+  tags?               : Option (Array DiagnosticTag)
+  relatedInformation? : Option (Array DiagnosticRelatedInformation)
+  deriving Ord
+
+/-- Extracts user-visible properties from the given `DiagnosticWith`. -/
+private def DiagnosticWith.UserVisible.ofDiagnostic (d : DiagnosticWith α)
+    : DiagnosticWith.UserVisible α :=
+  { d with }
+
+/-- Compares `DiagnosticWith` instances modulo non-user-facing properties. -/
+def compareByUserVisible [Ord α] (a b : DiagnosticWith α) : Ordering :=
+  compare (DiagnosticWith.UserVisible.ofDiagnostic a) (DiagnosticWith.UserVisible.ofDiagnostic b)
+
 abbrev Diagnostic := DiagnosticWith String
 
 /-- Parameters for the [`textDocument/publishDiagnostics` notification](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_publishDiagnostics). -/

src/Lean/Data/Lsp/Internal.lean

@@ -161,9 +161,10 @@ instance : FromJson ModuleRefs where
     node.foldM (init := HashMap.empty) fun m k v =>
       return m.insert (← RefIdent.fromJson? (← Json.parse k)) (← fromJson? v)
 
-/-- `$/lean/ileanInfoUpdate` and `$/lean/ileanInfoFinal` watchdog<-worker notifications.
-
-Contains the file's definitions and references. -/
+/--
+Used in the `$/lean/ileanInfoUpdate` and `$/lean/ileanInfoFinal` watchdog <- worker notifications.
+Contains the definitions and references of the file managed by a worker.
+-/
 structure LeanIleanInfoParams where
   /-- Version of the file these references are from. -/
   version    : Nat
@@ -171,4 +172,22 @@ structure LeanIleanInfoParams where
   references : ModuleRefs
   deriving FromJson, ToJson
 
+/--
+Used in the `$/lean/importClosure` watchdog <- worker notification.
+Contains the full import closure of the file managed by a worker.
+-/
+structure LeanImportClosureParams where
+  /-- Full import closure of the file. -/
+  importClosure : Array DocumentUri
+  deriving FromJson, ToJson
+
+/--
+Used in the `$/lean/importClosure` watchdog -> worker notification.
+Informs the worker that one of its dependencies has gone stale and likely needs to be rebuilt.
+-/
+structure LeanStaleDependencyParams where
+  /-- The dependency that is stale. -/
+  staleDependency : DocumentUri
+  deriving FromJson, ToJson
+
 end Lean.Lsp

src/Lean/Data/Lsp/TextSync.lean

@@ -38,7 +38,7 @@ structure DidOpenTextDocumentParams where
 
 structure TextDocumentChangeRegistrationOptions where
   documentSelector? : Option DocumentSelector := none
-  syncKind : TextDocumentSyncKind
+  syncKind          : TextDocumentSyncKind
   deriving FromJson
 
 inductive TextDocumentContentChangeEvent where
@@ -61,13 +61,18 @@ instance TextDocumentContentChangeEvent.hasToJson : ToJson TextDocumentContentCh
     | TextDocumentContentChangeEvent.fullChange text => [⟨"text", toJson text⟩]⟩
 
 structure DidChangeTextDocumentParams where
-  textDocument : VersionedTextDocumentIdentifier
+  textDocument   : VersionedTextDocumentIdentifier
   contentChanges : Array TextDocumentContentChangeEvent
   deriving ToJson, FromJson
 
+structure DidSaveTextDocumentParams where
+  textDocument : TextDocumentIdentifier
+  text?        : Option String
+  deriving ToJson, FromJson
+
 -- TODO: missing:
 -- WillSaveTextDocumentParams, TextDocumentSaveReason,
--- TextDocumentSaveRegistrationOptions, DidSaveTextDocumentParams
+-- TextDocumentSaveRegistrationOptions
 
 structure SaveOptions where
   includeText : Bool
@@ -81,11 +86,11 @@ structure DidCloseTextDocumentParams where
 
 /-- NOTE: This is defined twice in the spec. The latter version has more fields. -/
 structure TextDocumentSyncOptions where
-  openClose : Bool
-  change : TextDocumentSyncKind
-  willSave : Bool
+  openClose         : Bool
+  change            : TextDocumentSyncKind
+  willSave          : Bool
   willSaveWaitUntil : Bool
-  save? : Option SaveOptions := none
+  save?             : Option SaveOptions
   deriving ToJson, FromJson
 
 end Lsp

src/Lean/Data/Name.lean

@@ -7,8 +7,6 @@ prelude
 import Init.Data.Ord
 namespace Lean
 
-instance : Coe String Name := ⟨Name.mkSimple⟩
-
 namespace Name
 -- Remark: we export the `Name.hash` to make sure it matches the hash implemented in C++
 @[export lean_name_hash_exported] def hashEx : Name → UInt64 :=

src/Lean/Data/NameMap.lean

@@ -11,8 +11,6 @@ import Lean.Data.SSet
 import Lean.Data.Name
 namespace Lean
 
-instance : Coe String Name := ⟨Name.mkSimple⟩
-
 def NameMap (α : Type) := RBMap Name α Name.quickCmp
 
 @[inline] def mkNameMap (α : Type) : NameMap α := mkRBMap Name α Name.quickCmp

src/Lean/Data/Parsec.lean

@@ -5,7 +5,7 @@ Author: Dany Fabian
 -/
 prelude
 import Init.NotationExtra
-import Init.Data.ToString.Basic
+import Init.Data.ToString.Macro
 
 namespace Lean
 

src/Lean/Data/PersistentArray.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Array.Basic
 import Init.NotationExtra
+import Init.Data.ToString.Macro
 
 universe u v w
 
@@ -71,6 +72,8 @@ def get! [Inhabited α] (t : PersistentArray α) (i : Nat) : α :=
 instance [Inhabited α] : GetElem (PersistentArray α) Nat α fun as i => i < as.size where
   getElem xs i _ := xs.get! i
 
+instance [Inhabited α] : LawfulGetElem (PersistentArray α) Nat α fun as i => i < as.size where
+
 partial def setAux : PersistentArrayNode α → USize → USize → α → PersistentArrayNode α
   | node cs, i, shift, a =>
     let j     := div2Shift i shift

src/Lean/Data/PersistentHashMap.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Array.BasicAux
+import Init.Data.ToString.Macro
 
 namespace Lean
 universe u v w w'
@@ -154,6 +155,8 @@ def find? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → Op
 instance {_ : BEq α} {_ : Hashable α} : GetElem (PersistentHashMap α β) α (Option β) fun _ _ => True where
   getElem m i _ := m.find? i
 
+instance {_ : BEq α} {_ : Hashable α} : LawfulGetElem (PersistentHashMap α β) α (Option β) fun _ _ => True where
+
 @[inline] def findD {_ : BEq α} {_ : Hashable α} (m : PersistentHashMap α β) (a : α) (b₀ : β) : β :=
   (m.find? a).getD b₀
 
@@ -226,8 +229,10 @@ partial def eraseAux [BEq α] : Node α β → USize → α → Node α β × Bo
   | n@(Node.collision keys vals heq), _, k =>
     match keys.indexOf? k with
     | some idx =>
-      let ⟨keys', keq⟩ := keys.eraseIdx' idx
-      let ⟨vals', veq⟩ := vals.eraseIdx' (Eq.ndrec idx heq)
+      let keys' := keys.feraseIdx idx
+      have keq := keys.size_feraseIdx idx
+      let vals' := vals.feraseIdx (Eq.ndrec idx heq)
+      have veq := vals.size_feraseIdx (Eq.ndrec idx heq)
       have : keys.size - 1 = vals.size - 1 := by rw [heq]
       (Node.collision keys' vals' (keq.trans (this.trans veq.symm)), true)
     | none     => (n, false)

src/Lean/Data/Position.lean

@@ -38,9 +38,6 @@ structure FileMap where
   The first entry is always `0` and the last always the index of the last character.
   In particular, if the last character is a newline, that index will appear twice. -/
   positions : Array String.Pos
-  /-- The line numbers associated with the `positions`.
-  Has the same length as `positions` and is always of the form `#[1, 2, …, n-1, n-1]`. -/
-  lines     : Array Nat
   deriving Inhabited
 
 class MonadFileMap (m : Type → Type) where
@@ -50,40 +47,50 @@ export MonadFileMap (getFileMap)
 
 namespace FileMap
 
+/-- The last line should always be `positions.size - 1`. -/
+def getLastLine (fmap : FileMap) : Nat :=
+  fmap.positions.size - 1
+
+/-- The line numbers associated with the `positions` of the `FileMap`.
+`fmap.getLine i` is the iᵗʰ entry of `#[1, 2, …, n-1, n-1]`
+where `n` is the `size` of `positions`. -/
+def getLine (fmap : FileMap) (x : Nat) : Nat :=
+  min (x + 1) fmap.getLastLine
+
 partial def ofString (s : String) : FileMap :=
-  let rec loop (i : String.Pos) (line : Nat) (ps : Array String.Pos) (lines : Array Nat) : FileMap :=
-    if s.atEnd i then { source := s, positions := ps.push i, lines := lines.push line }
+  let rec loop (i : String.Pos) (line : Nat) (ps : Array String.Pos) : FileMap :=
+    if s.atEnd i then { source := s, positions := ps.push i }
     else
       let c := s.get i
       let i := s.next i
-      if c == '\n' then loop i (line+1) (ps.push i) (lines.push (line+1))
-      else loop i line ps lines
-  loop 0 1 (#[0]) (#[1])
+      if c == '\n' then loop i (line+1) (ps.push i)
+      else loop i line ps
+  loop 0 1 (#[0])
 
 partial def toPosition (fmap : FileMap) (pos : String.Pos) : Position :=
   match fmap with
-  | { source := str, positions := ps, lines := lines } =>
+  | { source := str, positions := ps } =>
     if ps.size >= 2 && pos <= ps.back then
       let rec toColumn (i : String.Pos) (c : Nat) : Nat :=
         if i == pos || str.atEnd i then c
         else toColumn (str.next i) (c+1)
       let rec loop (b e : Nat) :=
         let posB := ps[b]!
-        if e == b + 1 then { line := lines.get! b, column := toColumn posB 0 }
+        if e == b + 1 then { line := fmap.getLine b, column := toColumn posB 0 }
         else
           let m := (b + e) / 2;
           let posM := ps.get! m;
-          if pos == posM then { line := lines.get! m, column := 0 }
+          if pos == posM then { line := fmap.getLine m, column := 0 }
           else if pos > posM then loop m e
           else loop b m
       loop 0 (ps.size -1)
-    else if lines.isEmpty then
+    else if ps.isEmpty then
       ⟨0, 0⟩
     else
       -- Some systems like the delaborator use synthetic positions without an input file,
       -- which would violate `toPositionAux`'s invariant.
       -- Can also happen with EOF errors, which are not strictly inside the file.
-      ⟨lines.back, (pos - ps.back).byteIdx⟩
+      ⟨fmap.getLastLine, (pos - ps.back).byteIdx⟩
 
 /-- Convert a `Lean.Position` to a `String.Pos`. -/
 def ofPosition (text : FileMap) (pos : Position) : String.Pos :=

src/Lean/Data/Rat.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.NotationExtra
-import Init.Data.ToString.Basic
+import Init.Data.ToString.Macro
 import Init.Data.Int.DivMod
 import Init.Data.Nat.Gcd
 namespace Lean

src/Lean/Data/Xml/Basic.lean

@@ -5,6 +5,8 @@ Author: Dany Fabian
 -/
 prelude
 import Lean.Data.RBMap
+import Init.Data.ToString.Macro
+
 namespace Lean
 namespace Xml
 

src/Lean/DocString.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.DeclarationRange
 import Lean.MonadEnv
+import Init.Data.String.Extra
 
 namespace Lean
 
@@ -13,10 +14,10 @@ private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) ← IO.mk
 private builtin_initialize docStringExt : MapDeclarationExtension String ← mkMapDeclarationExtension
 
 def addBuiltinDocString (declName : Name) (docString : String) : IO Unit :=
-  builtinDocStrings.modify (·.insert declName (removeLeadingSpaces docString))
+  builtinDocStrings.modify (·.insert declName docString.removeLeadingSpaces)
 
 def addDocString [MonadEnv m] (declName : Name) (docString : String) : m Unit :=
-  modifyEnv fun env => docStringExt.insert env declName (removeLeadingSpaces docString)
+  modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces
 
 def addDocString' [Monad m] [MonadEnv m] (declName : Name) (docString? : Option String) : m Unit :=
   match docString? with

src/Lean/Elab/App.lean

@@ -1035,7 +1035,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
   if eType.isForall then
     match lval with
     | LVal.fieldName _ fieldName _ _ =>
-      let fullName := `Function ++ fieldName
+      let fullName := Name.str `Function fieldName
       if (← getEnv).contains fullName then
         return LValResolution.const `Function `Function fullName
     | _ => pure ()
@@ -1060,9 +1060,9 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
   | some structName, LVal.fieldName _ fieldName _ _ =>
     let env ← getEnv
     let searchEnv : Unit → TermElabM LValResolution := fun _ => do
-      if let some (baseStructName, fullName) := findMethod? env structName fieldName then
+      if let some (baseStructName, fullName) := findMethod? env structName (.mkSimple fieldName) then
         return LValResolution.const baseStructName structName fullName
-      else if let some (structName', fullName) := findMethodAlias? env structName fieldName then
+      else if let some (structName', fullName) := findMethodAlias? env structName (.mkSimple fieldName) then
         return LValResolution.const structName' structName' fullName
       else
         throwLValError e eType
@@ -1149,7 +1149,7 @@ private partial def mkBaseProjections (baseStructName : Name) (structName : Name
 private def typeMatchesBaseName (type : Expr) (baseName : Name) : MetaM Bool := do
   if baseName == `Function then
     return (← whnfR type).isForall
-  else if type.consumeMData.isAppOf baseName then
+  else if type.cleanupAnnotations.isAppOf baseName then
     return true
   else
     return (← whnfR type).isAppOf baseName

src/Lean/Elab/BuiltinCommand.lean

@@ -55,7 +55,7 @@ private def popScopes (numScopes : Nat) : CommandElabM Unit :=
 
 private def checkAnonymousScope : List Scope → Option Name
   | { header := "", .. } :: _ => none
-  | { header := h, .. }  :: _ => some h
+  | { header := h, .. }  :: _ => some <| .mkSimple h
   | _                         => some .anonymous -- should not happen
 
 private def checkEndHeader : Name → List Scope → Option Name
@@ -64,7 +64,7 @@ private def checkEndHeader : Name → List Scope → Option Name
     if h == s then
       (.str · s) <$> checkEndHeader p scopes
     else
-      some h
+      some <| .mkSimple h
   | _, _ => some .anonymous -- should not happen
 
 @[builtin_command_elab «namespace»] def elabNamespace : CommandElab := fun stx =>

src/Lean/Elab/Declaration.lean

@@ -95,7 +95,7 @@ private def expandDeclNamespace? (stx : Syntax) : MacroM (Option (Name × Syntax
   let scpView := extractMacroScopes name
   match scpView.name with
   | .str .anonymous _ => return none
-  | .str pre shortName => return some (pre, setDefName stx { scpView with name := shortName }.review)
+  | .str pre shortName => return some (pre, setDefName stx { scpView with name := .mkSimple shortName }.review)
   | _ => return none
 
 def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do

src/Lean/Elab/Deriving/Ord.lean

@@ -84,6 +84,7 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
   for i in [:ctx.typeInfos.size] do
     auxDefs := auxDefs.push (← mkAuxFunction ctx i)
   `(mutual
+     set_option match.ignoreUnusedAlts true
      $auxDefs:command*
     end)
 

src/Lean/Elab/InfoTree/Main.lean

@@ -187,7 +187,7 @@ def FieldRedeclInfo.format (ctx : ContextInfo) (info : FieldRedeclInfo) : Format
   f!"FieldRedecl @ {formatStxRange ctx info.stx}"
 
 def OmissionInfo.format (ctx : ContextInfo) (info : OmissionInfo) : IO Format := do
-  return f!"Omission @ {← TermInfo.format ctx info.toTermInfo}"
+  return f!"Omission @ {← TermInfo.format ctx info.toTermInfo}\nReason: {info.reason}"
 
 def Info.format (ctx : ContextInfo) : Info → IO Format
   | ofTacticInfo i         => i.format ctx

src/Lean/Elab/InfoTree/Types.lean

@@ -157,12 +157,13 @@ structure FieldRedeclInfo where
 
 /--
 Denotes information for the term `⋯` that is emitted by the delaborator when omitting a term
-due to `pp.deepTerms false`. Omission needs to be treated differently from regular terms because
+due to `pp.deepTerms false` or `pp.proofs false`. Omission needs to be treated differently from regular terms because
 it has to be delaborated differently in `Lean.Widget.InteractiveDiagnostics.infoToInteractive`:
 Regular terms are delaborated explicitly, whereas omitted terms are simply to be expanded with
 regular delaboration settings.
 -/
-structure OmissionInfo extends TermInfo
+structure OmissionInfo extends TermInfo where
+  reason : String
 
 /-- Header information for a node in `InfoTree`. -/
 inductive Info where

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -371,7 +371,7 @@ def mkUnfoldEq (declName : Name) (info : EqnInfoCore) : MetaM Name := withLCtx {
       mkUnfoldProof declName goal.mvarId!
       let type ← mkForallFVars xs type
       let value ← mkLambdaFVars xs (← instantiateMVars goal)
-      let name := baseName ++ `def
+      let name := Name.str baseName unfoldThmSuffix
       addDecl <| Declaration.thmDecl {
         name, type, value
         levelParams := info.levelParams

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

@@ -68,7 +68,7 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
   for i in [: eqnTypes.size] do
     let type := eqnTypes[i]!
     trace[Elab.definition.structural.eqns] "{eqnTypes[i]!}"
-    let name := baseName ++ (`eq).appendIndexAfter (i+1)
+    let name := (Name.str baseName eqnThmSuffixBase).appendIndexAfter (i+1)
     thmNames := thmNames.push name
     let value ← mkProof info.declName type
     let (type, value) ← removeUnusedEqnHypotheses type value

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

@@ -119,7 +119,7 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
   for i in [: eqnTypes.size] do
     let type := eqnTypes[i]!
     trace[Elab.definition.wf.eqns] "{eqnTypes[i]!}"
-    let name := baseName ++ (`eq).appendIndexAfter (i+1)
+    let name := (Name.str baseName eqnThmSuffixBase).appendIndexAfter (i+1)
     thmNames := thmNames.push name
     let value ← mkProof declName type
     let (type, value) ← removeUnusedEqnHypotheses type value

src/Lean/Elab/Structure.lean

@@ -302,7 +302,7 @@ private def getFieldType (infos : Array StructFieldInfo) (parentType : Expr) (fi
           let args := e.getAppArgs
           if let some major := args.get? numParams then
             if (← getNestedProjectionArg major) == parent then
-              if let some existingFieldInfo := findFieldInfo? infos subFieldName then
+              if let some existingFieldInfo := findFieldInfo? infos (.mkSimple subFieldName) then
                 return TransformStep.done <| mkAppN existingFieldInfo.fvar args[numParams+1:args.size]
       return TransformStep.done e
     let projType ← Meta.transform projType (post := visit)

src/Lean/Elab/Syntax.lean

@@ -173,7 +173,7 @@ where
           | `(stx| $sym:str) => pure sym
           | _ => return arg'
         let sym := sym.getString
-        return (← `(ParserDescr.nodeWithAntiquot $(quote sym) $(quote (`token ++ sym)) $(arg'.1)), 1)
+        return (← `(ParserDescr.nodeWithAntiquot $(quote sym) $(quote (Name.str `token sym)) $(arg'.1)), 1)
     else
       pure args'
     let (args', stackSz) := if let some stackSz := info.stackSz? then

src/Lean/Elab/Tactic.lean

@@ -38,3 +38,5 @@ import Lean.Elab.Tactic.Symm
 import Lean.Elab.Tactic.SolveByElim
 import Lean.Elab.Tactic.LibrarySearch
 import Lean.Elab.Tactic.ShowTerm
+import Lean.Elab.Tactic.Rfl
+import Lean.Elab.Tactic.Rewrites

src/Lean/Elab/Tactic/Basic.lean

@@ -158,8 +158,9 @@ partial def evalTactic (stx : Syntax) : TacticM Unit := do
     | _ => throwError m!"unexpected tactic{indentD stx}"
 where
     throwExs (failures : Array EvalTacticFailure) : TacticM Unit := do
-     if let some fail := failures[0]? then
-       -- Recall that `failures[0]` is the highest priority evalFn/macro
+     if h : 0 < failures.size  then
+       -- For macros we want to report the error from the first registered / last tried rule (#3770)
+       let fail := failures[failures.size-1]
        fail.state.restore (restoreInfo := true)
        throw fail.exception -- (*)
      else

src/Lean/Elab/Tactic/Induction.lean

@@ -533,11 +533,19 @@ private def elabTermForElim (stx : Syntax) : TermElabM Expr := do
     else
       return e
 
+register_builtin_option tactic.customEliminators : Bool := {
+  defValue := true
+  group    := "tactic"
+  descr    := "enable using custom eliminators in the 'induction' and 'cases' tactics \
+    defined using the '@[induction_eliminator]' and '@[cases_eliminator]' attributes"
+}
+
 -- `optElimId` is of the form `("using" term)?`
 private def getElimNameInfo (optElimId : Syntax) (targets : Array Expr) (induction : Bool) : TacticM ElimInfo := do
   if optElimId.isNone then
-    if let some elimName ← getCustomEliminator? targets induction then
-      return ← getElimInfo elimName
+    if tactic.customEliminators.get (← getOptions) then
+      if let some elimName ← getCustomEliminator? targets induction then
+        return ← getElimInfo elimName
     unless targets.size == 1 do
       throwError "eliminator must be provided when multiple targets are used (use 'using <eliminator-name>'), and no default eliminator has been registered using attribute `[eliminator]`"
     let indVal ← getInductiveValFromMajor targets[0]!

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

@@ -218,7 +218,12 @@ def analyzeAtom (e : Expr) : OmegaM (HashSet Expr) := do
             (mkApp3 (.const ``Int.emod_nonneg []) x k
                 (mkApp3 (.const ``Int.ne_of_gt []) k (toExpr (0 : Int)) cast_pos)) |>.insert
               (mkApp3 (.const ``Int.emod_lt_of_pos []) x k cast_pos)
-      | _ => pure ∅
+      | _ =>  match x.getAppFnArgs with
+        | (``Nat.cast, #[.const ``Int [], _, x']) =>
+          -- Since we push coercions inside `%`, we need to record here that
+          -- `(x : Int) % (y : Int)` is non-negative.
+          pure <| HashSet.empty.insert (mkApp2 (.const ``Int.emod_ofNat_nonneg []) x' k)
+        | _ => pure ∅
     | _ => pure ∅
   | (``Min.min, #[_, _, x, y]) =>
     pure <| HashSet.empty.insert (mkApp2 (.const ``Int.min_le_left []) x y) |>.insert

src/Lean/Elab/Tactic/Rewrites.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2023 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+prelude
+import Lean.Elab.Tactic.Location
+import Lean.Meta.Tactic.Replace
+import Lean.Meta.Tactic.Rewrites
+
+/-!
+# The `rewrites` tactic.
+
+`rw?` tries to find a lemma which can rewrite the goal.
+
+`rw?` should not be left in proofs; it is a search tool, like `apply?`.
+
+Suggestions are printed as `rw [h]` or `rw [← h]`.
+
+-/
+namespace Lean.Elab.Rewrites
+
+open Lean Meta Rewrites
+open Lean.Parser.Tactic
+
+open Lean Elab Tactic
+
+@[builtin_tactic Lean.Parser.Tactic.rewrites?]
+def evalExact : Tactic := fun stx => do
+  let `(tactic| rw?%$tk $[$loc]? $[[ $[-$forbidden],* ]]?) := stx
+        | throwUnsupportedSyntax
+  let moduleRef ← createModuleTreeRef
+  let forbidden : NameSet :=
+    ((forbidden.getD #[]).map Syntax.getId).foldl (init := ∅) fun s n => s.insert n
+  reportOutOfHeartbeats `findRewrites tk
+  let goal ← getMainGoal
+  withLocation (expandOptLocation (Lean.mkOptionalNode loc))
+    fun f => do
+      let some a ← f.findDecl? | return
+      if a.isImplementationDetail then return
+      let target ← instantiateMVars (← f.getType)
+      let hyps ← localHypotheses (except := [f])
+      let results ← findRewrites hyps moduleRef goal target (stopAtRfl := false) forbidden
+      reportOutOfHeartbeats `rewrites tk
+      if results.isEmpty then
+        throwError "Could not find any lemmas which can rewrite the hypothesis {← f.getUserName}"
+      for r in results do withMCtx r.mctx do
+        Tactic.TryThis.addRewriteSuggestion tk [(r.expr, r.symm)]
+          r.result.eNew (loc? := .some (.fvar f)) (origSpan? := ← getRef)
+      if let some r := results[0]? then
+        setMCtx r.mctx
+        let replaceResult ← goal.replaceLocalDecl f r.result.eNew r.result.eqProof
+        replaceMainGoal (replaceResult.mvarId :: r.result.mvarIds)
+    do
+      let target ← instantiateMVars (← goal.getType)
+      let hyps ← localHypotheses
+      let results ← findRewrites hyps moduleRef goal target (stopAtRfl := true) forbidden
+      reportOutOfHeartbeats `rewrites tk
+      if results.isEmpty then
+        throwError "Could not find any lemmas which can rewrite the goal"
+      results.forM (·.addSuggestion tk)
+      if let some r := results[0]? then
+        setMCtx r.mctx
+        replaceMainGoal
+          ((← goal.replaceTargetEq r.result.eNew r.result.eqProof) :: r.result.mvarIds)
+        evalTactic (← `(tactic| try rfl))
+    (fun _ => throwError "Failed to find a rewrite for some location")
+
+end Lean.Elab.Rewrites

src/Lean/Elab/Tactic/Rfl.lean

@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2022 Newell Jensen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Newell Jensen, Thomas Murrills
+-/
+prelude
+import Lean.Meta.Tactic.Rfl
+import Lean.Elab.Tactic.Basic
+
+/-!
+# `rfl` tactic extension for reflexive relations
+
+This extends the `rfl` tactic so that it works on reflexive relations other than `=`,
+provided the reflexivity lemma has been marked as `@[refl]`.
+-/
+
+namespace Lean.Elab.Tactic.Rfl
+
+@[builtin_tactic Lean.Parser.Tactic.applyRfl] def evalApplyRfl : Tactic := fun stx =>
+  match stx with
+  | `(tactic| apply_rfl) => withMainContext do liftMetaFinishingTactic (·.applyRfl)
+  | _ => throwUnsupportedSyntax
+
+end Lean.Elab.Tactic.Rfl

src/Lean/Elab/Tactic/ShowTerm.lean

@@ -7,7 +7,7 @@ prelude
 import Lean.Elab.ElabRules
 import Lean.Meta.Tactic.TryThis
 
-namespace Std.Tactic
+namespace Lean.Elab.Tactic.ShowTerm
 open Lean Elab Term Tactic Meta.Tactic.TryThis Parser.Tactic
 
 @[builtin_tactic showTerm] def evalShowTerm : Tactic := fun stx =>
@@ -26,3 +26,5 @@ open Lean Elab Term Tactic Meta.Tactic.TryThis Parser.Tactic
     addTermSuggestion tk (← instantiateMVars e).headBeta (origSpan? := ← getRef)
     pure e
   | _, _ => throwUnsupportedSyntax
+
+end Lean.Elab.Tactic.ShowTerm

src/Lean/Elab/Tactic/Simpa.lean

@@ -18,7 +18,7 @@ register_option linter.unnecessarySimpa : Bool := {
   descr := "enable the 'unnecessary simpa' linter"
 }
 
-namespace Std.Tactic.Simpa
+namespace Lean.Elab.Tactic.Simpa
 
 open Lean Parser.Tactic Elab Meta Term Tactic Simp Linter
 
@@ -86,3 +86,5 @@ deriving instance Repr for UseImplicitLambdaResult
           | _ => unreachable!
         TryThis.addSuggestion tk stx (origSpan? := ← getRef)
     | _ => throwUnsupportedSyntax
+
+end Lean.Elab.Tactic.Simpa

src/Lean/Elab/Term.lean

@@ -665,7 +665,7 @@ def mkTypeMismatchError (header? : Option String) (e : Expr) (eType : Expr) (exp
   return m!"{header}{← mkHasTypeButIsExpectedMsg eType expectedType}"
 
 def throwTypeMismatchError (header? : Option String) (expectedType : Expr) (eType : Expr) (e : Expr)
-    (f? : Option Expr := none) (extraMsg? : Option MessageData := none) : TermElabM α := do
+    (f? : Option Expr := none) (_extraMsg? : Option MessageData := none) : TermElabM α := do
   /-
     We ignore `extraMsg?` for now. In all our tests, it contained no useful information. It was
     always of the form:

src/Lean/Expr.lean

@@ -1881,6 +1881,22 @@ def letFunAppArgs? (e : Expr) : Option (Array Expr × Name × Expr × Expr × Ex
   | .lam n _ b _ => some (rest, n, t, v, b)
   | _ => some (rest, .anonymous, t, v, .app f (.bvar 0))
 
+/-- Maps `f` on each immediate child of the given expression. -/
+@[specialize]
+def traverseChildren [Applicative M] (f : Expr → M Expr) : Expr → M Expr
+  | e@(forallE _ d b _) => pure e.updateForallE! <*> f d <*> f b
+  | e@(lam _ d b _)     => pure e.updateLambdaE! <*> f d <*> f b
+  | e@(mdata _ b)       => e.updateMData! <$> f b
+  | e@(letE _ t v b _)  => pure e.updateLet! <*> f t <*> f v <*> f b
+  | e@(app l r)         => pure e.updateApp! <*> f l <*> f r
+  | e@(proj _ _ b)      => e.updateProj! <$> f b
+  | e                   => pure e
+
+/-- `e.foldlM f a` folds the monadic function `f` over the subterms of the expression `e`,
+with initial value `a`. -/
+def foldlM {α : Type} {m} [Monad m] (f : α → Expr → m α) (init : α) (e : Expr) : m α :=
+  Prod.snd <$> StateT.run (e.traverseChildren (fun e' => fun a => Prod.mk e' <$> f a e')) init
+
 end Expr
 
 /--

src/Lean/Hygiene.lean

@@ -51,7 +51,7 @@ private def mkInaccessibleUserNameAux (unicode : Bool) (name : Name) (idx : Nat)
     else
       name.appendAfter ("✝" ++ idx.toSuperscriptString)
   else
-    name ++ Name.mkNum "_inaccessible" idx
+    name ++ Name.num `_inaccessible idx
 
 private def mkInaccessibleUserName (unicode : Bool) : Name → Name
   | .num p@(.str ..) idx =>

src/Lean/LabelAttribute.lean

@@ -80,8 +80,7 @@ macro (name := _root_.Lean.Parser.Command.registerLabelAttr)
   doc:(docComment)? "register_label_attr " id:ident : command => do
   let str := id.getId.toString
   let idParser := mkIdentFrom id (`Parser.Attr ++ id.getId)
-  let descr := quote (removeLeadingSpaces
-    (doc.map (·.getDocString) |>.getD ("labelled declarations for " ++ id.getId.toString)))
+  let descr := quote ((doc.map (·.getDocString) |>.getD ("labelled declarations for " ++ id.getId.toString)).removeLeadingSpaces)
   `($[$doc:docComment]? initialize ext : Lean.LabelExtension ←
       registerLabelAttr $(quote id.getId) $descr $(quote id.getId)
     $[$doc:docComment]? syntax (name := $idParser:ident) $(quote str):str : attr)

src/Lean/Language/Basic.lean

@@ -194,7 +194,7 @@ def Snapshot.Diagnostics.ofMessageLog (msgLog : Lean.MessageLog) :
 def diagnosticsOfHeaderError (msg : String) : ProcessingM Snapshot.Diagnostics := do
   let msgLog := MessageLog.empty.add {
     fileName := "<input>"
-    pos := ⟨0, 0⟩
+    pos := ⟨1, 0⟩
     endPos := (← read).fileMap.toPosition (← read).fileMap.source.endPos
     data := msg
   }

src/Lean/Language/Lean.lean

@@ -71,7 +71,7 @@ private def pushOpt (a? : Option α) (as : Array α) : Array α :=
 
 /-- Option for capturing output to stderr during elaboration. -/
 register_builtin_option stderrAsMessages : Bool := {
-  defValue := false
+  defValue := true
   group    := "server"
   descr    := "(server) capture output to the Lean stderr channel (such as from `dbg_trace`) during elaboration of a command as a diagnostic message"
 }

src/Lean/Linter/UnusedVariables.lean

@@ -1,36 +1,109 @@
 /-
 Copyright (c) 2022 Sebastian Ullrich. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Ullrich
+Authors: Sebastian Ullrich, Mario Carneiro
 -/
 prelude
 import Lean.Elab.Command
-import Lean.Util.ForEachExpr
 import Lean.Linter.Util
-import Lean.Server.References
+set_option linter.missingDocs true -- keep it documented
+
+/-! # Unused variable Linter
+
+This file implements the unused variable linter, which runs automatically on all commands
+and reports any local variables that are never referred to, using information from the info tree.
+
+It is not immediately obvious but this is a surprisingly expensive check without some optimizations.
+The main complication is that it can be difficult to determine what constitutes a "use".
+For example, we would like this to be considered a use of `x`:
+```
+def foo (x : Nat) : Nat := by assumption
+```
+
+The final proof term is `fun x => x` so clearly `x` was used, but we can't make use of this because
+the final proof term is after we have abstracted over the original `fvar` for `x`. If we look
+further into the tactic state we can see the `fvar` show up in the instantiation to the original
+goal metavariable `?m : Nat := x`, but it is not always the case that we can follow metavariable
+instantiations to determine what happened after the fact, because tactics might skip the goal
+metavariable and instantiate some other metavariable created prior to it instead.
+
+Instead, we use a (much more expensive) overapproximation, which is just to look through the entire
+metavariable context looking for occurrences of `x`. We use caching to ensure that this is still
+linear in the size of the info tree, even though there are many metavariable contexts in all the
+intermediate stages of elaboration; these are highly similar and make use of `PersistentHashMap`
+so there is a lot of subterm sharing we can take advantage of.
+
+## The `@[unused_variables_ignore_fn]` attribute
+
+Some occurrences of variables are deliberately unused, or at least we don't want to lint on unused
+variables in these positions. For example:
+
+```
+def foo (x : Nat) : (y : Nat) → Nat := fun _ => x
+                  -- ^ don't lint this unused variable because it is public API
+```
+
+They are generally a syntactic criterion, so we allow adding custom `IgnoreFunction`s so that
+external syntax can also opt in to lint suppression, like so:
+
+```
+macro (name := foobarKind) "foobar " name:ident : command => `(def foo ($name : Nat) := 0)
+
+foobar n -- linted because n is unused in the macro expansion
+
+@[unused_variables_ignore_fn]
+def ignoreFoobar : Lean.Linter.IgnoreFunction := fun _ stack _ => stack.matches [``foobarKind]
+
+foobar n -- not linted
+```
+
+-/
 
 namespace Lean.Linter
 open Lean.Elab.Command Lean.Server Std
 
+/-- Enables or disables all unused variable linter warnings -/
 register_builtin_option linter.unusedVariables : Bool := {
   defValue := true,
   descr := "enable the 'unused variables' linter"
 }
+/-- Enables or disables unused variable linter warnings in function arguments -/
 register_builtin_option linter.unusedVariables.funArgs : Bool := {
   defValue := true,
   descr := "enable the 'unused variables' linter to mark unused function arguments"
 }
+/-- Enables or disables unused variable linter warnings in patterns -/
 register_builtin_option linter.unusedVariables.patternVars : Bool := {
   defValue := true,
   descr := "enable the 'unused variables' linter to mark unused pattern variables"
 }
 
-def getLinterUnusedVariables (o : Options) : Bool := getLinterValue linter.unusedVariables o
-def getLinterUnusedVariablesFunArgs (o : Options) : Bool := o.get linter.unusedVariables.funArgs.name (getLinterUnusedVariables o)
-def getLinterUnusedVariablesPatternVars (o : Options) : Bool := o.get linter.unusedVariables.patternVars.name (getLinterUnusedVariables o)
+/-- Gets the status of `linter.unusedVariables` -/
+def getLinterUnusedVariables (o : Options) : Bool :=
+  getLinterValue linter.unusedVariables o
 
+/-- Gets the status of `linter.unusedVariables.funArgs` -/
+def getLinterUnusedVariablesFunArgs (o : Options) : Bool :=
+  o.get linter.unusedVariables.funArgs.name (getLinterUnusedVariables o)
+
+/-- Gets the status of `linter.unusedVariables.patternVars` -/
+def getLinterUnusedVariablesPatternVars (o : Options) : Bool :=
+  o.get linter.unusedVariables.patternVars.name (getLinterUnusedVariables o)
+
+/-- An `IgnoreFunction` receives:
+
+* a `Syntax.ident` for the unused variable
+* a `Syntax.Stack` with the location of this piece of syntax in the command
+* The `Options` set locally to this syntax
+
+and should return `true` to indicate that the lint should be suppressed,
+or `false` to proceed with linting as usual (other `IgnoreFunction`s may still
+say it is ignored). A variable is only linted if it is unused and no
+`IgnoreFunction` returns `true` on this syntax.
+-/
 abbrev IgnoreFunction := Syntax → Syntax.Stack → Options → Bool
 
+/-- Interpret an `IgnoreFunction` from the environment. -/
 unsafe def mkIgnoreFnImpl (constName : Name) : ImportM IgnoreFunction := do
   let { env, opts, .. } ← read
   match env.find? constName with
@@ -40,14 +113,18 @@ unsafe def mkIgnoreFnImpl (constName : Name) : ImportM IgnoreFunction := do
       throw ↑s!"unexpected unused_variables_ignore_fn at '{constName}', must be of type `Lean.Linter.IgnoreFunction`"
     IO.ofExcept <| env.evalConst IgnoreFunction opts constName
 
-@[implemented_by mkIgnoreFnImpl]
+@[inherit_doc mkIgnoreFnImpl, implemented_by mkIgnoreFnImpl]
 opaque mkIgnoreFn (constName : Name) : ImportM IgnoreFunction
 
+/-- The list of builtin `IgnoreFunction`s. -/
 builtin_initialize builtinUnusedVariablesIgnoreFnsRef : IO.Ref <| Array IgnoreFunction ← IO.mkRef #[]
 
+/-- Adds a new builtin `IgnoreFunction`.
+This function should only be used from within the `Lean` package. -/
 def addBuiltinUnusedVariablesIgnoreFn (h : IgnoreFunction) : IO Unit :=
   builtinUnusedVariablesIgnoreFnsRef.modify (·.push h)
 
+/-- An extension which keeps track of registered `IgnoreFunction`s. -/
 builtin_initialize unusedVariablesIgnoreFnsExt :
   PersistentEnvExtension Name (Name × IgnoreFunction) (List Name × Array IgnoreFunction) ←
   registerPersistentEnvExtension {
@@ -60,6 +137,8 @@ builtin_initialize unusedVariablesIgnoreFnsExt :
     statsFn := fun s => format "number of local entries: " ++ format s.1.length
   }
 
+/-- Adds the `@[{builtin_}unused_variables_ignore_fn]` attribute, which is applied
+to declarations of type `IgnoreFunction` for use by the unused variables linter. -/
 builtin_initialize
   let mkAttr (builtin : Bool) (name : Name) := registerBuiltinAttribute {
     name
@@ -81,38 +160,44 @@ builtin_initialize
   mkAttr true `builtin_unused_variables_ignore_fn
   mkAttr false `unused_variables_ignore_fn
 
--- matches builtinUnused variable pattern
-builtin_initialize addBuiltinUnusedVariablesIgnoreFn fun stx _ _ =>
-    stx.getId.toString.startsWith "_"
-
--- is variable
+/-- `variable (unused : Nat)` -/
 builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ =>
     stack.matches [`null, none, `null, ``Lean.Parser.Command.variable])
 
--- is in structure
+/-- `structure Foo where unused : Nat` -/
 builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ =>
   stack.matches [`null, none, `null, ``Lean.Parser.Command.structure])
 
--- is in inductive
+/-- `inductive Foo where | unused : Foo` -/
 builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ =>
   stack.matches [`null, none, `null, none, ``Lean.Parser.Command.inductive] &&
   (stack.get? 3 |>.any fun (stx, pos) =>
     pos == 0 &&
     [``Lean.Parser.Command.optDeclSig, ``Lean.Parser.Command.declSig].any (stx.isOfKind ·)))
 
--- in in constructor or structure binder
+/--
+* `structure Foo where foo (unused : Nat) : Nat`
+* `inductive Foo where | mk (unused : Nat) : Foo`
+-/
 builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ =>
   stack.matches [`null, none, `null, ``Lean.Parser.Command.optDeclSig, none] &&
   (stack.get? 4 |>.any fun (stx, _) =>
     [``Lean.Parser.Command.ctor, ``Lean.Parser.Command.structSimpleBinder].any (stx.isOfKind ·)))
 
--- is in opaque or axiom
+/--
+* `opaque foo (unused : Nat) : Nat`
+* `axiom foo (unused : Nat) : Nat`
+-/
 builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ =>
   stack.matches [`null, none, `null, ``Lean.Parser.Command.declSig, none] &&
   (stack.get? 4 |>.any fun (stx, _) =>
     [``Lean.Parser.Command.opaque, ``Lean.Parser.Command.axiom].any (stx.isOfKind ·)))
 
--- is in definition with foreign definition
+/--
+Definition with foreign definition
+* `@[extern "bla"] def foo (unused : Nat) : Nat := ...`
+* `@[implemented_by bla] def foo (unused : Nat) : Nat := ...`
+-/
 builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ =>
   stack.matches [`null, none, `null, none, none, ``Lean.Parser.Command.declaration] &&
   (stack.get? 3 |>.any fun (stx, _) =>
@@ -123,18 +208,27 @@ builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ =>
       attrs.any (fun attr => attr.raw.isOfKind ``Parser.Attr.extern || attr matches `(attr| implemented_by $_))
     | _ => false))
 
--- is in dependent arrow
+/--
+Dependent arrow
+* `def foo : (unused : Nat) → Nat := id`
+-/
 builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ =>
   stack.matches [`null, ``Lean.Parser.Term.explicitBinder, ``Lean.Parser.Term.depArrow])
 
--- is in let declaration
+/--
+Function argument in let declaration (when `linter.unusedVariables.funArgs` is false)
+* `def foo := let x (unused : Nat) := 1; x`
+-/
 builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack opts =>
   !getLinterUnusedVariablesFunArgs opts &&
   stack.matches [`null, none, `null, ``Lean.Parser.Term.letIdDecl, none] &&
   (stack.get? 3 |>.any fun (_, pos) => pos == 1) &&
   (stack.get? 5 |>.any fun (stx, _) => !stx.isOfKind ``Lean.Parser.Command.whereStructField))
 
--- is in declaration signature
+/--
+Function argument in declaration signature (when `linter.unusedVariables.funArgs` is false)
+* `def foo (unused : Nat) := 1`
+-/
 builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack opts =>
   !getLinterUnusedVariablesFunArgs opts &&
   stack.matches [`null, none, `null, none] &&
@@ -142,26 +236,184 @@ builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack opts =>
     pos == 0 &&
     [``Lean.Parser.Command.optDeclSig, ``Lean.Parser.Command.declSig].any (stx.isOfKind ·)))
 
--- is in function definition
+/--
+Function argument in function definition (when `linter.unusedVariables.funArgs` is false)
+* `def foo := fun (unused : Nat) => 1`
+-/
 builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack opts =>
   !getLinterUnusedVariablesFunArgs opts &&
   (stack.matches [`null, ``Lean.Parser.Term.basicFun] ||
   stack.matches [``Lean.Parser.Term.typeAscription, `null, ``Lean.Parser.Term.basicFun]))
 
--- is pattern variable
+/--
+In pattern (when `linter.unusedVariables.patternVars` is false)
+* `def foo := match 0 with | unused => 1`
+-/
 builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack opts =>
   !getLinterUnusedVariablesPatternVars opts &&
   stack.any fun (stx, pos) =>
     (stx.isOfKind ``Lean.Parser.Term.matchAlt && pos == 1) ||
     (stx.isOfKind ``Lean.Parser.Tactic.inductionAltLHS && pos == 2))
 
-unsafe def getUnusedVariablesIgnoreFnsImpl : CommandElabM (Array IgnoreFunction) := do
+/-- Get the current list of `IgnoreFunction`s. -/
+def getUnusedVariablesIgnoreFns : CommandElabM (Array IgnoreFunction) := do
   return (unusedVariablesIgnoreFnsExt.getState (← getEnv)).2
 
-@[implemented_by getUnusedVariablesIgnoreFnsImpl]
-opaque getUnusedVariablesIgnoreFns : CommandElabM (Array IgnoreFunction)
+namespace UnusedVariables
 
+/-- Collect into a heterogeneous collection of objects with external storage. This uses
+pointer identity and does not store the objects, so it is important not to store the last
+pointer to an object in the map, or it can be freed and reused, resulting in incorrect behavior.
 
+Returns `true` if the object was not already in the set. -/
+unsafe def insertObjImpl {α : Type} (set : IO.Ref (HashSet USize)) (a : α) : IO Bool := do
+  if (← set.get).contains (ptrAddrUnsafe a) then
+    return false
+  set.modify (·.insert (ptrAddrUnsafe a))
+  return true
+
+@[inherit_doc insertObjImpl, implemented_by insertObjImpl]
+opaque insertObj {α : Type} (set : IO.Ref (HashSet USize)) (a : α) : IO Bool
+
+/--
+Collects into `fvarUses` all `fvar`s occurring in the `Expr`s in `assignments`.
+This implementation respects subterm sharing in both the `PersistentHashMap` and the `Expr`
+to ensure that pointer-equal subobjects are not visited multiple times, which is important
+in practice because these expressions are very frequently highly shared.
+-/
+partial def visitAssignments (set : IO.Ref (HashSet USize))
+    (fvarUses : IO.Ref (HashSet FVarId))
+    (assignments : Array (PersistentHashMap MVarId Expr)) : IO Unit := do
+  MonadCacheT.run do
+    for assignment in assignments do
+      visitNode assignment.root
+where
+  /-- Visit a `PersistentHashMap.Node`, collecting all fvars in it into `fvarUses` -/
+  visitNode node : MonadCacheT Expr Unit IO Unit := do
+    if ← insertObj set node then
+      match node with
+      | .entries entries => for e in entries do visitEntry e
+      | .collision _ vs _ => for e in vs do visitExpr e
+  /-- Visit a `PersistentHashMap.Entry`, collecting all fvars in it into `fvarUses` -/
+  visitEntry e : MonadCacheT Expr Unit IO Unit := do
+    if ← insertObj set e then
+      match e with
+      | .entry _ e => visitExpr e
+      | .ref node => visitNode node
+      | .null => pure ()
+  /-- Visit an `Expr`, collecting all fvars in it into `fvarUses` -/
+  visitExpr e : MonadCacheT Expr Unit IO Unit := do
+    if ← insertObj set e then
+      ForEachExpr.visit (e := e) fun e => do
+        match e with
+        | .fvar id => fvarUses.modify (·.insert id); return false
+        | _ => return e.hasFVar
+
+/-- Given `aliases` as a map from an alias to what it aliases, we get the original
+term by recursion. This has no cycle detection, so if `aliases` contains a loop
+then this function will recurse infinitely. -/
+partial def followAliases (aliases : HashMap FVarId FVarId) (x : FVarId) : FVarId :=
+  match aliases.find? x with
+  | none => x
+  | some y => followAliases aliases y
+
+/-- Information regarding an `FVarId` definition. -/
+structure FVarDefinition where
+  /-- The user-provided name of the `FVarId` -/
+  userName : Name
+  /-- A (usually `.ident`) syntax for the defined variable -/
+  stx : Syntax
+  /-- The options set locally to this part of the syntax (used by `IgnoreFn`) -/
+  opts : Options
+  /-- The list of all `FVarId`s that are considered as being defined at this position.
+  This can have more than one element if multiple variables are declared by the same
+  syntax, such as the `h` in `if h : c then ... else ...`. We only report an unused variable
+  at this span if all variables in `aliases` are unused. -/
+  aliases : Array FVarId
+
+/-- The main data structure used to collect information from the info tree regarding unused
+variables. -/
+structure References where
+  /-- The set of all (ranges corresponding to) global definitions that are made in the syntax.
+  For example in `mutual def foo := ...  def bar := ... where baz := ... end` this would be
+  the spans for `foo`, `bar`, and `baz`. Global definitions are always treated as used.
+  (It would be nice to be able to detect unused global definitions but this requires more
+  information than the linter framework can provide.) -/
+  constDecls : HashSet String.Range := .empty
+  /-- The collection of all local declarations, organized by the span of the declaration.
+  We collapse all declarations declared at the same position into a single record using
+  `FVarDefinition.aliases`. -/
+  fvarDefs : HashMap String.Range FVarDefinition := .empty
+  /-- The set of `FVarId`s that are used directly. These may or may not be aliases. -/
+  fvarUses : HashSet FVarId := .empty
+  /-- A mapping from alias to original FVarId. We don't guarantee that the value is not itself
+  an alias, but we use `followAliases` when adding new elements to try to avoid long chains. -/
+  -- TODO: use a `UnionFind` data structure here
+  fvarAliases : HashMap FVarId FVarId := .empty
+  /-- Collection of all `MetavarContext`s following the execution of a tactic. We trawl these
+  if needed to find additional `fvarUses`. -/
+  assignments : Array (PersistentHashMap MVarId Expr) := #[]
+
+/-- Collect information from the `infoTrees` into `References`.
+See `References` for more information about the return value. -/
+def collectReferences (infoTrees : Array Elab.InfoTree) (cmdStxRange : String.Range) :
+    StateRefT References IO Unit := do
+  for tree in infoTrees do
+    tree.visitM' (preNode := fun ci info _ => do
+      match info with
+      | .ofTermInfo ti =>
+        match ti.expr with
+        | .const .. =>
+          if ti.isBinder then
+            let some range := info.range? | return
+            let .original .. := info.stx.getHeadInfo | return -- we are not interested in canonical syntax here
+            modify fun s => { s with constDecls := s.constDecls.insert range }
+        | .fvar id .. =>
+          let some range := info.range? | return
+          let .original .. := info.stx.getHeadInfo | return -- we are not interested in canonical syntax here
+          if ti.isBinder then
+            -- This is a local variable declaration.
+            let some ldecl := ti.lctx.find? id | return
+            -- Skip declarations which are outside the command syntax range, like `variable`s
+            -- (it would be confusing to lint these), or those which are macro-generated
+            if !cmdStxRange.contains range.start || ldecl.userName.hasMacroScopes then return
+            let opts := ci.options
+            -- we have to check for the option again here because it can be set locally
+            if !getLinterUnusedVariables opts then return
+            let stx := skipDeclIdIfPresent info.stx
+            if let .str _ s := stx.getId then
+              -- If the variable name is `_foo` then it is intentionally (possibly) unused, so skip.
+              -- This is the suggested way to silence the warning
+              if s.startsWith "_" then return
+            -- Record this either as a new `fvarDefs`, or an alias of an existing one
+            modify fun s =>
+              if let some ref := s.fvarDefs.find? range then
+                { s with fvarDefs := s.fvarDefs.insert range { ref with aliases := ref.aliases.push id } }
+              else
+                { s with fvarDefs := s.fvarDefs.insert range { userName := ldecl.userName, stx, opts, aliases := #[id] } }
+          else
+            -- Found a direct use, keep track of it
+            modify fun s => { s with fvarUses := s.fvarUses.insert id }
+        | _ => pure ()
+      | .ofTacticInfo ti =>
+        -- Keep track of the `MetavarContext` after a tactic for later
+        modify fun s => { s with assignments := s.assignments.push ti.mctxAfter.eAssignment }
+      | .ofFVarAliasInfo i =>
+        -- record any aliases we find
+        modify fun s =>
+          let id := followAliases s.fvarAliases i.baseId
+          { s with fvarAliases := s.fvarAliases.insert i.id id }
+      | _ => pure ())
+where
+  /-- Since declarations attach the declaration info to the `declId`,
+  we skip that to get to the `.ident` if possible. -/
+  skipDeclIdIfPresent (stx : Syntax) : Syntax :=
+    if stx.isOfKind ``Lean.Parser.Command.declId then
+      stx[0]
+    else
+      stx
+
+/-- Reports unused variable warnings on each command. Use `linter.unusedVariables` to disable. -/
 def unusedVariables : Linter where
   run cmdStx := do
     unless getLinterUnusedVariables (← getOptions) do
@@ -172,126 +424,89 @@ def unusedVariables : Linter where
       return
 
     let some cmdStxRange := cmdStx.getRange?
-      | pure ()
+      | return
 
     let infoTrees := (← get).infoState.trees.toArray
-    let fileMap := (← read).fileMap
 
     if (← infoTrees.anyM (·.hasSorry)) then
       return
 
-    -- collect references
-    let refs := findModuleRefs fileMap infoTrees (allowSimultaneousBinderUse := true)
+    -- Run the main collection pass, resulting in `s : References`.
+    let (_, s) ← (collectReferences infoTrees cmdStxRange).run {}
 
-    let mut vars : HashMap FVarId RefInfo := .empty
-    let mut constDecls : HashSet String.Range := .empty
+    -- If there are no local defs then there is nothing to do
+    if s.fvarDefs.isEmpty then return
 
-    for (ident, info) in refs.toList do
-      match ident with
-      | .fvar _ id =>
-        vars := vars.insert id info
-      | .const .. =>
-        if let some definition := info.definition then
-          if let some range := definition.stx.getRange? then
-            constDecls := constDecls.insert range
+    -- Resolve all recursive references in `fvarAliases`.
+    -- At this point everything in `fvarAliases` is guaranteed not to be itself an alias,
+    -- and should point to some element of `FVarDefinition.aliases` in `s.fvarDefs`
+    let fvarAliases : HashMap FVarId FVarId := s.fvarAliases.fold (init := {}) fun m id baseId =>
+      m.insert id (followAliases s.fvarAliases baseId)
 
-    -- collect uses from tactic infos
-    let tacticMVarAssignments : HashMap MVarId Expr :=
-      infoTrees.foldr (init := .empty) fun tree assignments =>
-        tree.foldInfo (init := assignments) (fun _ i assignments => match i with
-          | .ofTacticInfo ti =>
-            ti.mctxAfter.eAssignment.foldl (init := assignments) fun assignments mvar expr =>
-              if assignments.contains mvar then
-                assignments
-              else
-                assignments.insert mvar expr
-          | _ =>
-            assignments)
+    -- Collect all non-alias fvars corresponding to `fvarUses` by resolving aliases in the list.
+    let fvarUsesRef ← IO.mkRef <| fvarAliases.fold (init := s.fvarUses) fun fvarUses id baseId =>
+      if fvarUses.contains id then fvarUses.insert baseId else fvarUses
 
-    -- collect fvars from mvar assignments
-    let tacticFVarUses : HashSet FVarId ←
-      Elab.Command.liftIO <|  -- no need to carry around other state here
-      StateT.run' (s := HashSet.empty) do
-      -- use one big cache for all `ForEachExpr.visit` invocations
-      MonadCacheT.run do
-        tacticMVarAssignments.forM fun _ e =>
-          ForEachExpr.visit (e := e) fun e => do
-            if e.isFVar then modify (·.insert e.fvarId!)
-            return e.hasFVar
-        get
-
-    -- collect ignore functions
+    -- Collect ignore functions
     let ignoreFns ← getUnusedVariablesIgnoreFns
-    let ignoreFns declStx stack opts :=
-      isTopLevelDecl constDecls declStx stack opts ||
-      ignoreFns.any (· declStx stack opts)
 
-    -- determine unused variables
+    let mut initializedMVars := false
     let mut unused := #[]
-    for (id, ⟨decl?, uses⟩) in vars.toList do
-      -- process declaration
-      let some decl := decl?
+    -- For each variable definition, check to see if it is used
+    for (range, { userName, stx := declStx, opts, aliases }) in s.fvarDefs.toArray do
+      let fvarUses ← fvarUsesRef.get
+      -- If any of the `fvar`s corresponding to this declaration is (an alias of) a variable in
+      -- `fvarUses`, then it is used
+      if aliases.any fun id => fvarUses.contains (fvarAliases.findD id id) then continue
+      -- If this is a global declaration then it is (potentially) used after the command
+      if s.constDecls.contains range then continue
+
+      -- Get the syntax stack for this variable declaration
+      let some ((id', _) :: stack) := cmdStx.findStack? (·.getRange?.any (·.includes range))
         | continue
-      let declStx := skipDeclIdIfPresent decl.stx
-      let some range := declStx.getRange?
-        | continue
-      let some localDecl := decl.info.lctx.find? id
-        | continue
-      if !cmdStxRange.contains range.start || localDecl.userName.hasMacroScopes then
-        continue
 
-      -- check if variable is used
-      if !uses.isEmpty || tacticFVarUses.contains id || decl.aliases.any (match · with | .fvar _ id => tacticFVarUses.contains id | _ => false) then
-          continue
+      -- If it is blacklisted by an `ignoreFn` then skip it
+      if id'.isIdent && ignoreFns.any (· declStx stack opts) then continue
 
-      -- check linter options
-      let opts := decl.ci.options
-      if !getLinterUnusedVariables opts then
-        continue
-
-      -- evaluate ignore functions on original syntax
-      if let some ((id', _) :: stack) := cmdStx.findStack? (·.getRange?.any (·.includes range)) then
-        if id'.isIdent && ignoreFns declStx stack opts then
-          continue
-      else
-        continue
-
-      -- evaluate ignore functions on macro expansion outputs
+      -- Evaluate ignore functions again on macro expansion outputs
       if ← infoTrees.anyM fun tree => do
-        if let some macroExpansions ← collectMacroExpansions? range tree then
-          return macroExpansions.any fun expansion =>
-            -- in a macro expansion, there may be multiple leafs whose (synthetic) range includes `range`, so accept strict matches only
-            if let some (_ :: stack) := expansion.output.findStack? (·.getRange?.any (·.includes range)) (fun stx => stx.isIdent && stx.getRange?.any (· == range)) then
-              ignoreFns declStx stack opts
-            else
-              false
-        else
-          return false
+        let some macroExpansions ← collectMacroExpansions? range tree | return false
+        return macroExpansions.any fun expansion =>
+          -- in a macro expansion, there may be multiple leafs whose (synthetic) range
+          -- includes `range`, so accept strict matches only
+          if let some (_ :: stack) :=
+            expansion.output.findStack?
+              (·.getRange?.any (·.includes range))
+              (fun stx => stx.isIdent && stx.getRange?.any (· == range))
+          then
+            ignoreFns.any (· declStx stack opts)
+          else
+            false
       then
         continue
 
-      -- publish warning if variable is unused and not ignored
-      unused := unused.push (declStx, localDecl)
+      -- Visiting the metavariable assignments is expensive so we delay initialization
+      if !initializedMVars then
+        -- collect additional `fvarUses` from tactic assignments
+        visitAssignments (← IO.mkRef {}) fvarUsesRef s.assignments
+        initializedMVars := true
+        let fvarUses ← fvarUsesRef.get
+        -- Redo the initial check because `fvarUses` could be bigger now
+        if aliases.any fun id => fvarUses.contains (fvarAliases.findD id id) then continue
 
-    for (declStx, localDecl) in unused.qsort (·.1.getPos?.get! < ·.1.getPos?.get!) do
-      logLint linter.unusedVariables declStx m!"unused variable `{localDecl.userName}`"
+      -- If we made it this far then the variable is unused and not ignored
+      unused := unused.push (declStx, userName)
 
-    return ()
-where
-  skipDeclIdIfPresent (stx : Syntax) : Syntax :=
-    if stx.isOfKind ``Lean.Parser.Command.declId then
-      stx[0]
-    else
-      stx
-  isTopLevelDecl (constDecls : HashSet String.Range) : IgnoreFunction := fun stx stack _ => Id.run <| do
-    let some declRange := stx.getRange?
-      | false
-    constDecls.contains declRange &&
-    !stack.matches [``Lean.Parser.Term.letIdDecl]
+    -- Sort the outputs by position
+    for (declStx, userName) in unused.qsort (·.1.getPos?.get! < ·.1.getPos?.get!) do
+      logLint linter.unusedVariables declStx m!"unused variable `{userName}`"
 
 builtin_initialize addLinter unusedVariables
 
+end UnusedVariables
 end Linter
 
+/-- Returns true if this is a message produced by the unused variable linter.
+This is used to give these messages an additional "faded" style in the editor. -/
 def MessageData.isUnusedVariableWarning (msg : MessageData) : Bool :=
   msg.hasTag (· == Linter.linter.unusedVariables.name)

src/Lean/Meta/ArgsPacker.lean

@@ -532,7 +532,7 @@ where
   go : List Expr → Array Expr → MetaM α
   | [], acc => k acc
   | t::ts, acc => do
-    let name := if argsPacker.numFuncs = 1 then name else s!"{name}{acc.size+1}"
+    let name := if argsPacker.numFuncs = 1 then name else .mkSimple s!"{name}{acc.size+1}"
     withLocalDecl name .default t fun x => do
       go ts (acc.push x)
 

src/Lean/Meta/Basic.lean

@@ -1222,7 +1222,7 @@ where
         process mvars bis j b
       | _ => finalize ()
 
-private def withNewFVar (n : Name) (fvar fvarType : Expr) (k : Expr → MetaM α) : MetaM α := do
+private def withNewFVar (fvar fvarType : Expr) (k : Expr → MetaM α) : MetaM α := do
   if let some c ← isClass? fvarType then
     withNewLocalInstance c fvar <| k fvar
   else
@@ -1234,7 +1234,7 @@ private def withLocalDeclImp (n : Name) (bi : BinderInfo) (type : Expr) (k : Exp
   let lctx := ctx.lctx.mkLocalDecl fvarId n type bi kind
   let fvar := mkFVar fvarId
   withReader (fun ctx => { ctx with lctx := lctx }) do
-    withNewFVar n fvar type k
+    withNewFVar fvar type k
 
 /-- Create a free variable `x` with name, binderInfo and type, add it to the context and run in `k`.
 Then revert the context. -/
@@ -1295,7 +1295,7 @@ private def withLetDeclImp (n : Name) (type : Expr) (val : Expr) (k : Expr → M
   let lctx := ctx.lctx.mkLetDecl fvarId n type val (nonDep := false) kind
   let fvar := mkFVar fvarId
   withReader (fun ctx => { ctx with lctx := lctx }) do
-    withNewFVar n fvar type k
+    withNewFVar fvar type k
 
 /--
   Add the local declaration `<name> : <type> := <val>` to the local context and execute `k x`, where `x` is a new

src/Lean/Meta/Canonicalizer.lean

@@ -101,7 +101,7 @@ private partial def mkKey (e : Expr) : CanonM Key := do
         let args ← e.getAppArgs.mapIdxM fun i arg => do
           if h : i < info.paramInfo.size then
             let info := info.paramInfo[i]
-            if info.isExplicit then
+            if info.isExplicit && !info.isProp then
               pure (← mkKey arg).e
             else
               pure (mkSort 0) -- some dummy value for erasing implicit

src/Lean/Meta/Eqns.lean

@@ -9,25 +9,32 @@ import Lean.Meta.Basic
 import Lean.Meta.AppBuilder
 
 namespace Lean.Meta
+def eqnThmSuffixBase := "eq"
+def eqnThmSuffixBasePrefix := eqnThmSuffixBase ++ "_"
+def eqn1ThmSuffix := eqnThmSuffixBasePrefix ++ "1"
+example : eqn1ThmSuffix = "eq_1" := rfl
+
 /-- Returns `true` if `s` is of the form `eq_<idx>` -/
 def isEqnReservedNameSuffix (s : String) : Bool :=
-  "eq_".isPrefixOf s && (s.drop 3).isNat
+  eqnThmSuffixBasePrefix.isPrefixOf s && (s.drop 3).isNat
 
-/-- Returns `true` if `s == "def"` -/
+def unfoldThmSuffix := "eq_def"
+
+/-- Returns `true` if `s == "eq_def"` -/
 def isUnfoldReservedNameSuffix (s : String) : Bool :=
-  s == "def"
+  s == unfoldThmSuffix
 
 /--
 Throw an error if names for equation theorems for `declName` are not available.
 -/
 def ensureEqnReservedNamesAvailable (declName : Name) : CoreM Unit := do
-  ensureReservedNameAvailable declName "def"
-  ensureReservedNameAvailable declName "eq_1"
+  ensureReservedNameAvailable declName unfoldThmSuffix
+  ensureReservedNameAvailable declName eqn1ThmSuffix
   -- TODO: `declName` may need to reserve multiple `eq_<idx>` names, but we check only the first one.
   -- Possible improvement: try to efficiently compute the number of equation theorems at declaration time, and check all of them.
 
 /--
-Ensures that `f.def` and `f.eq_<idx>` are reserved names if `f` is a safe definition.
+Ensures that `f.eq_def` and `f.eq_<idx>` are reserved names if `f` is a safe definition.
 -/
 builtin_initialize registerReservedNamePredicate fun env n =>
   match n with
@@ -87,7 +94,7 @@ builtin_initialize eqnsExt : EnvExtension EqnsExtState ←
 /--
 Simple equation theorem for nonrecursive definitions.
 -/
-private def mkSimpleEqThm (declName : Name) (suffix := `def) : MetaM (Option Name) := do
+private def mkSimpleEqThm (declName : Name) (suffix := Name.mkSimple unfoldThmSuffix) : MetaM (Option Name) := do
   if let some (.defnInfo info) := (← getEnv).find? declName then
     lambdaTelescope (cleanupAnnotations := true) info.value fun xs body => do
       let lhs := mkAppN (mkConst info.name <| info.levelParams.map mkLevelParam) xs
@@ -122,7 +129,7 @@ Equation theorems are generated on demand, check whether they were generated in
 -/
 private partial def alreadyGenerated? (declName : Name) : MetaM (Option (Array Name)) := do
   let env ← getEnv
-  let eq1 := declName ++ `eq_1
+  let eq1 := Name.str declName eqn1ThmSuffix
   if env.contains eq1 then
     let rec loop (idx : Nat) (eqs : Array Name) : MetaM (Array Name) := do
       let nextEq := declName ++ (`eq).appendIndexAfter idx
@@ -152,7 +159,7 @@ def getEqnsFor? (declName : Name) (nonRec := false) : MetaM (Option (Array Name)
         registerEqnThms declName r
         return some r
     if nonRec then
-      let some eqThm ← mkSimpleEqThm declName (suffix := `eq_1) | return none
+      let some eqThm ← mkSimpleEqThm declName (suffix := Name.mkSimple eqn1ThmSuffix) | return none
       let r := #[eqThm]
       registerEqnThms declName r
       return some r
@@ -199,7 +206,7 @@ You can use `nonRec := true` to override this behavior.
 -/
 def getUnfoldEqnFor? (declName : Name) (nonRec := false) : MetaM (Option Name) := withLCtx {} {} do
   let env ← getEnv
-  let unfoldName := declName ++ `def
+  let unfoldName := Name.str declName unfoldThmSuffix
   if env.contains unfoldName then
     return some unfoldName
   if (← shouldGenerateEqnThms declName) then

src/Lean/Meta/IndPredBelow.lean

@@ -65,8 +65,8 @@ def mkContext (declName : Name) : MetaM Context := do
 where
   motiveName (motiveTypes : Array Expr) (i : Nat) : MetaM Name :=
     if motiveTypes.size > 1
-    then mkFreshUserName s!"motive_{i.succ}"
-    else mkFreshUserName "motive"
+    then mkFreshUserName <| .mkSimple s!"motive_{i.succ}"
+    else mkFreshUserName <| .mkSimple "motive"
 
   mkHeader
       (motives : Array (Name × Expr))
@@ -315,7 +315,7 @@ where
 def mkBrecOnDecl (ctx : Context) (idx : Nat) : MetaM Declaration := do
   let type ← mkType
   let indVal := ctx.typeInfos[idx]!
-  let name := indVal.name ++ brecOnSuffix
+  let name := indVal.name ++ .mkSimple brecOnSuffix
   return Declaration.thmDecl {
     name := name
     levelParams := indVal.levelParams
@@ -337,8 +337,8 @@ where
       (motive : Name × Expr) : MetaM $ Name × (Array Expr → MetaM Expr) := do
     let name :=
       if ctx.motives.size > 1
-      then mkFreshUserName s!"ih_{idx.val.succ}"
-      else mkFreshUserName "ih"
+      then mkFreshUserName <| .mkSimple s!"ih_{idx.val.succ}"
+      else mkFreshUserName <| .mkSimple "ih"
     let ih ← instantiateForall motive.2 params
     let mkDomain (_ : Array Expr) : MetaM Expr :=
       forallTelescopeReducing ih fun ys _ => do

src/Lean/Meta/LazyDiscrTree.lean

@@ -393,26 +393,37 @@ Get the root key and rest of terms of an expression using the specified config.
 private def rootKey (cfg: WhnfCoreConfig) (e : Expr) : MetaM (Key × Array Expr) :=
   pushArgs true (Array.mkEmpty initCapacity) e cfg
 
-private partial def mkPathAux (root : Bool) (todo : Array Expr) (keys : Array Key)
-    (config : WhnfCoreConfig) : MetaM (Array Key) := do
+private partial def buildPath (op : Bool → Array Expr → Expr → MetaM (Key × Array Expr)) (root : Bool) (todo : Array Expr) (keys : Array Key) : MetaM (Array Key) := do
   if todo.isEmpty then
     return keys
   else
     let e    := todo.back
     let todo := todo.pop
-    let (k, todo) ← pushArgs root todo e config
-    mkPathAux false todo (keys.push k) config
+    let (k, todo) ← op root todo e
+    buildPath op false todo (keys.push k)
 
 /--
-Create a path from an expression.
+Create a key path from an expression using the function used for patterns.
 
-This differs from Lean.Meta.DiscrTree.mkPath in that the expression
+This differs from Lean.Meta.DiscrTree.mkPath and targetPath in that the expression
 should uses free variables rather than meta-variables for holes.
 -/
-private def mkPath (e : Expr) (config : WhnfCoreConfig) : MetaM (Array Key) := do
+def patternPath (e : Expr) (config : WhnfCoreConfig) : MetaM (Array Key) := do
   let todo : Array Expr := .mkEmpty initCapacity
-  let keys : Array Key := .mkEmpty initCapacity
-  mkPathAux (root := true) (todo.push e) keys config
+  let op root todo e := pushArgs root todo e config
+  buildPath op (root := true) (todo.push e) (.mkEmpty initCapacity)
+
+/--
+Create a key path from an expression we are matching against.
+
+This should have mvars instantiated where feasible.
+-/
+def targetPath (e : Expr) (config : WhnfCoreConfig) : MetaM (Array Key) := do
+  let todo : Array Expr := .mkEmpty initCapacity
+  let op root todo e := do
+        let (k, args) ← MatchClone.getMatchKeyArgs e root config
+        pure (k, todo ++ args)
+  buildPath op (root := true) (todo.push e) (.mkEmpty initCapacity)
 
 /- Monad for finding matches while resolving deferred patterns. -/
 @[reducible]
@@ -434,6 +445,35 @@ private def newTrie [Monad m] [MonadState (Array (Trie α)) m] (e : LazyEntry α
 private def addLazyEntryToTrie (i:TrieIndex) (e : LazyEntry α) : MatchM α Unit :=
   modify (·.modify i (·.pushPending e))
 
+private def evalLazyEntry (config : WhnfCoreConfig)
+    (p : Array α × TrieIndex × HashMap Key TrieIndex)
+    (entry : LazyEntry α)
+    : MatchM α (Array α × TrieIndex × HashMap Key TrieIndex) := do
+  let (values, starIdx, children) := p
+  let (todo, lctx, v) := entry
+  if todo.isEmpty then
+    let values := values.push v
+    pure (values, starIdx, children)
+  else
+    let e    := todo.back
+    let todo := todo.pop
+    let (k, todo) ← withLCtx lctx.1 lctx.2 $ pushArgs false todo e config
+    if k == .star then
+      if starIdx = 0 then
+        let starIdx ← newTrie (todo, lctx, v)
+        pure (values, starIdx, children)
+      else
+        addLazyEntryToTrie starIdx (todo, lctx, v)
+        pure (values, starIdx, children)
+    else
+      match children.find? k with
+      | none =>
+        let children := children.insert k (← newTrie (todo, lctx, v))
+        pure (values, starIdx, children)
+      | some idx =>
+        addLazyEntryToTrie idx (todo, lctx, v)
+        pure (values, starIdx, children)
+
 /--
 This evaluates all lazy entries in a trie and updates `values`, `starIdx`, and `children`
 accordingly.
@@ -442,34 +482,10 @@ private partial def evalLazyEntries (config : WhnfCoreConfig)
     (values : Array α) (starIdx : TrieIndex) (children : HashMap Key TrieIndex)
     (entries : Array (LazyEntry α)) :
     MatchM α (Array α × TrieIndex × HashMap Key TrieIndex) := do
-  let rec iter values starIdx children (i : Nat) : MatchM α _ := do
-        if p : i < entries.size then
-          let (todo, lctx, v) := entries[i]
-          if todo.isEmpty then
-            let values := values.push v
-            iter values starIdx children (i+1)
-          else
-            let e    := todo.back
-            let todo := todo.pop
-            let (k, todo) ← withLCtx lctx.1 lctx.2 $ pushArgs false todo e config
-            if k == .star then
-              if starIdx = 0 then
-                let starIdx ← newTrie (todo, lctx, v)
-                iter values starIdx children (i+1)
-              else
-                addLazyEntryToTrie starIdx (todo, lctx, v)
-                iter values starIdx children (i+1)
-            else
-              match children.find? k with
-              | none =>
-                let children := children.insert k (← newTrie (todo, lctx, v))
-                iter values starIdx children (i+1)
-              | some idx =>
-                addLazyEntryToTrie idx (todo, lctx, v)
-                iter values starIdx children (i+1)
-        else
-          pure (values, starIdx, children)
-  iter values starIdx children 0
+  let mut values := values
+  let mut starIdx := starIdx
+  let mut children := children
+  entries.foldlM (init := (values, starIdx, children)) (evalLazyEntry config)
 
 private def evalNode (c : TrieIndex) :
     MatchM α (Array α × TrieIndex × HashMap Key TrieIndex) := do
@@ -512,7 +528,7 @@ A match result contains the terms formed from matching a term against
 patterns in the discrimination tree.
 
 -/
-private structure MatchResult (α : Type) where
+structure MatchResult (α : Type) where
   /--
   The elements in the match result.
 
@@ -525,7 +541,9 @@ private structure MatchResult (α : Type) where
   -/
   elts : Array (Array (Array α)) := #[]
 
-private def MatchResult.push (r : MatchResult α) (score : Nat) (e : Array α) : MatchResult α :=
+namespace MatchResult
+
+private def push (r : MatchResult α) (score : Nat) (e : Array α) : MatchResult α :=
   if e.isEmpty then
     r
   else if score < r.elts.size then
@@ -539,14 +557,28 @@ private def MatchResult.push (r : MatchResult α) (score : Nat) (e : Array α) :
     termination_by score - a.size
     loop r.elts
 
-private partial def MatchResult.toArray (mr : MatchResult α) : Array α :=
-    loop (Array.mkEmpty n) mr.elts
-  where n := mr.elts.foldl (fun i a => a.foldl (fun n a => n + a.size) i) 0
-        loop (r : Array α) (a : Array (Array (Array α))) :=
-          if a.isEmpty then
-            r
-          else
-            loop (a.back.foldl (init := r) (fun r a => r ++ a)) a.pop
+/--
+Number of elements in result
+-/
+partial def size (mr : MatchResult α) : Nat :=
+  mr.elts.foldl (fun i a => a.foldl (fun n a => n + a.size) i) 0
+
+/--
+Append results to array
+-/
+@[specialize]
+partial def appendResultsAux (mr : MatchResult α) (a : Array β) (f : Nat → α → β) : Array β :=
+  let aa := mr.elts
+  let n := aa.size
+  Nat.fold (n := n) (init := a) fun i r =>
+    let j := n-1-i
+    let b := aa[j]!
+    b.foldl (init := r) (· ++ ·.map (f j))
+
+partial def appendResults (mr : MatchResult α) (a : Array α) : Array α :=
+  mr.appendResultsAux a (fun _ a => a)
+
+end MatchResult
 
 private partial def getMatchLoop (todo : Array Expr) (score : Nat) (c : TrieIndex)
     (result : MatchResult α) : MatchM α (MatchResult α) := do
@@ -563,7 +595,7 @@ private partial def getMatchLoop (todo : Array Expr) (score : Nat) (c : TrieInde
         and there is an edge for `k` and `k != Key.star`. -/
     let visitStar (result : MatchResult α) : MatchM α (MatchResult α) :=
       if star != 0 then
-        getMatchLoop todo score star result
+        getMatchLoop todo (score + 1) star result
       else
         return result
     let visitNonStar (k : Key) (args : Array Expr) (result : MatchResult α) :=
@@ -590,13 +622,13 @@ private def getStarResult (root : Lean.HashMap Key TrieIndex) : MatchM α (Match
     pure <| {}
   | some idx => do
     let (vs, _) ← evalNode idx
-    pure <| ({} : MatchResult α).push 0 vs
+    pure <| ({} : MatchResult α).push (score := 1) vs
 
 private def getMatchRoot (r : Lean.HashMap Key TrieIndex) (k : Key) (args : Array Expr)
     (result : MatchResult α) : MatchM α (MatchResult α) :=
   match r.find? k with
   | none => pure result
-  | some c => getMatchLoop args 1 c result
+  | some c => getMatchLoop args (score := 1) c result
 
 /--
   Find values that match `e` in `root`.
@@ -604,12 +636,12 @@ private def getMatchRoot (r : Lean.HashMap Key TrieIndex) (k : Key) (args : Arra
 private def getMatchCore (root : Lean.HashMap Key TrieIndex) (e : Expr) :
     MatchM α (MatchResult α) := do
   let result ← getStarResult root
-  let (k, args) ← MatchClone.getMatchKeyArgs e (root := true) (←read)
+  let (k, args) ← MatchClone.getMatchKeyArgs e (root := true) (← read)
   match k with
   | .star  => return result
   /- See note about "dep-arrow vs arrow" at `getMatchLoop` -/
   | .arrow =>
-    getMatchRoot root k args (←getMatchRoot root .other #[] result)
+    getMatchRoot root k args (← getMatchRoot root .other #[] result)
   | _ =>
     getMatchRoot root k args result
 
@@ -619,8 +651,8 @@ private def getMatchCore (root : Lean.HashMap Key TrieIndex) (e : Expr) :
   The results are ordered so that the longest matches in terms of number of
   non-star keys are first with ties going to earlier operators first.
 -/
-def getMatch (d : LazyDiscrTree α) (e : Expr) : MetaM (Array α × LazyDiscrTree α) :=
-  withReducible <| runMatch d <| (·.toArray) <$> getMatchCore d.roots e
+def getMatch (d : LazyDiscrTree α) (e : Expr) : MetaM (MatchResult α × LazyDiscrTree α) :=
+  withReducible <| runMatch d <| getMatchCore d.roots e
 
 /--
 Structure for quickly initializing a lazy discrimination tree with a large number
@@ -729,7 +761,28 @@ structure Cache where
 
 def Cache.empty (ngen : NameGenerator) : Cache := { ngen := ngen, core := {}, meta := {} }
 
+def matchPrefix (s : String) (pre : String) :=
+  s.startsWith pre && (s |>.drop pre.length |>.all Char.isDigit)
+
+def isInternalDetail : Name → Bool
+  | .str p s     =>
+    s.startsWith "_"
+      || matchPrefix s "eq_"
+      || matchPrefix s "match_"
+      || matchPrefix s "proof_"
+      || p.isInternalOrNum
+  | .num _ _     => true
+  | p            => p.isInternalOrNum
+
+def blacklistInsertion (env : Environment) (declName : Name) : Bool :=
+  !allowCompletion env declName
+  || declName == ``sorryAx
+  || isInternalDetail declName
+  || (declName matches .str _ "inj")
+  || (declName matches .str _ "noConfusionType")
+
 private def addConstImportData
+    (cctx : Core.Context)
     (env : Environment)
     (modName : Name)
     (d : ImportData)
@@ -738,16 +791,12 @@ private def addConstImportData
     (act : Name → ConstantInfo → MetaM (Array (InitEntry α)))
     (name : Name) (constInfo : ConstantInfo) : BaseIO (PreDiscrTree α) := do
   if constInfo.isUnsafe then return tree
-  if !allowCompletion env name then return tree
+  if blacklistInsertion env name then return tree
   let { ngen, core := core_cache, meta := meta_cache } ← cacheRef.get
   let mstate : Meta.State := { cache := meta_cache }
   cacheRef.set (Cache.empty ngen)
   let ctx : Meta.Context := { config := { transparency := .reducible } }
   let cm := (act name constInfo).run ctx mstate
-  let cctx : Core.Context := {
-    fileName := default,
-    fileMap := default
-  }
   let cstate : Core.State := {env, cache := core_cache, ngen}
   match ←(cm.run cctx cstate).toBaseIO with
   | .ok ((a, ms), cs) =>
@@ -791,7 +840,9 @@ private def toFlat (d : ImportData) (tree : PreDiscrTree α) :
   let de ← d.errors.swap #[]
   pure ⟨tree, de⟩
 
-private partial def loadImportedModule (env : Environment)
+private partial def loadImportedModule
+    (cctx : Core.Context)
+    (env : Environment)
     (act : Name → ConstantInfo → MetaM (Array (InitEntry α)))
     (d : ImportData)
     (cacheRef : IO.Ref Cache)
@@ -802,12 +853,12 @@ private partial def loadImportedModule (env : Environment)
   if h : i < mdata.constNames.size then
     let name := mdata.constNames[i]
     let constInfo  := mdata.constants[i]!
-    let tree ← addConstImportData env mname d cacheRef tree act name constInfo
-    loadImportedModule env act d cacheRef tree mname mdata (i+1)
+    let tree ← addConstImportData cctx env mname d cacheRef tree act name constInfo
+    loadImportedModule cctx env act d cacheRef tree mname mdata (i+1)
   else
     pure tree
 
-private def createImportedEnvironmentSeq (ngen : NameGenerator) (env : Environment)
+private def createImportedEnvironmentSeq (cctx : Core.Context) (ngen : NameGenerator) (env : Environment)
     (act : Name → ConstantInfo → MetaM (Array (InitEntry α)))
     (start stop : Nat) : BaseIO (InitResults α) := do
       let cacheRef ← IO.mkRef (Cache.empty ngen)
@@ -816,7 +867,7 @@ private def createImportedEnvironmentSeq (ngen : NameGenerator) (env : Environme
             if start < stop then
               let mname := env.header.moduleNames[start]!
               let mdata := env.header.moduleData[start]!
-              let tree ← loadImportedModule env act d cacheRef tree mname mdata
+              let tree ← loadImportedModule cctx env act d cacheRef tree mname mdata
               go d cacheRef tree (start+1) stop
             else
               toFlat d tree
@@ -833,6 +884,7 @@ def getChildNgen [Monad M] [MonadNameGenerator M] : M NameGenerator := do
   pure cngen
 
 def createLocalPreDiscrTree
+    (cctx : Core.Context)
     (ngen : NameGenerator)
     (env : Environment)
     (d : ImportData)
@@ -841,28 +893,22 @@ def createLocalPreDiscrTree
   let modName := env.header.mainModule
   let cacheRef ← IO.mkRef (Cache.empty ngen)
   let act (t : PreDiscrTree α) (n : Name) (c : ConstantInfo) : BaseIO (PreDiscrTree α) :=
-        addConstImportData env modName d cacheRef t act n c
+        addConstImportData cctx env modName d cacheRef t act n c
   let r ← (env.constants.map₂.foldlM (init := {}) act : BaseIO (PreDiscrTree α))
   pure r
 
-/-- Create an imported environment for tree. -/
-def createLocalEnvironment
-    (act : Name → ConstantInfo → MetaM (Array (InitEntry α))) :
-    CoreM (LazyDiscrTree α) := do
-  let env ← getEnv
-  let ngen ← getChildNgen
-  let d ← ImportData.new
-  let t ← createLocalPreDiscrTree ngen env d act
-  let errors ← d.errors.get
-  if p : errors.size > 0 then
-    throw errors[0].exception
-  pure <| t.toLazy
+def dropKeys (t : LazyDiscrTree α) (keys : List (List LazyDiscrTree.Key)) : MetaM (LazyDiscrTree α) := do
+  keys.foldlM (init := t) (·.dropKey ·)
 
-/-- Create an imported environment for tree. -/
-def createImportedEnvironment (ngen : NameGenerator) (env : Environment)
+def logImportFailure [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (f : ImportFailure) : m Unit :=
+  logError m!"Processing failure with {f.const} in {f.module}:\n  {f.exception.toMessageData}"
+
+/-- Create a discriminator tree for imported environment. -/
+def createImportedDiscrTree [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [MonadLiftT BaseIO m]
+    (cctx : Core.Context) (ngen : NameGenerator) (env : Environment)
     (act : Name → ConstantInfo → MetaM (Array (InitEntry α)))
     (constantsPerTask : Nat := 1000) :
-    EIO Exception (LazyDiscrTree α) := do
+    m (LazyDiscrTree α) := do
   let n := env.header.moduleData.size
   let rec
     /-- Allocate constants to tasks according to `constantsPerTask`. -/
@@ -872,40 +918,40 @@ def createImportedEnvironment (ngen : NameGenerator) (env : Environment)
         let cnt := cnt + mdata.constants.size
         if cnt > constantsPerTask then
           let (childNGen, ngen) := ngen.mkChild
-          let t ← createImportedEnvironmentSeq childNGen env act start (idx+1) |>.asTask
+          let t ← liftM <| createImportedEnvironmentSeq cctx childNGen env act start (idx+1) |>.asTask
           go ngen (tasks.push t) (idx+1) 0 (idx+1)
         else
           go ngen tasks start cnt (idx+1)
       else
         if start < n then
           let (childNGen, _) := ngen.mkChild
-          tasks.push <$> (createImportedEnvironmentSeq childNGen env act start n).asTask
+          let t ← (createImportedEnvironmentSeq cctx childNGen env act start n).asTask
+          pure (tasks.push t)
         else
           pure tasks
     termination_by env.header.moduleData.size - idx
   let tasks ← go ngen #[] 0 0 0
   let r := combineGet default tasks
-  if p : r.errors.size > 0 then
-    throw r.errors[0].exception
+  r.errors.forM logImportFailure
   pure <| r.tree.toLazy
 
-def dropKeys (t : LazyDiscrTree α) (keys : List (List LazyDiscrTree.Key)) : MetaM (LazyDiscrTree α) := do
-  keys.foldlM (init := t) (·.dropKey ·)
+/-- Creates the core context used for initializing a tree using the current context. -/
+private def createTreeCtx (ctx : Core.Context) : Core.Context := {
+    fileName := ctx.fileName,
+    fileMap := ctx.fileMap,
+    options := ctx.options,
+    maxRecDepth := ctx.maxRecDepth,
+    maxHeartbeats := 0,
+    ref := ctx.ref,
+  }
 
-/--
-`findCandidates` searches for entries in a lazily initialized discriminator tree.
-
-* `ext` should be an environment extension with an IO.Ref for caching the import lazy
-   discriminator tree.
-* `addEntry` is the function for creating discriminator tree entries from constants.
-* `droppedKeys` contains keys we do not want to consider when searching for matches.
-  It is used for dropping very general keys.
--/
-def findCandidates (ext : EnvExtension (IO.Ref (Option (LazyDiscrTree α))))
-    (addEntry : Name → ConstantInfo → MetaM (Array (InitEntry α)))
-    (droppedKeys : List (List LazyDiscrTree.Key) := [])
-    (constantsPerTask : Nat := 1000)
-    (ty : Expr) : MetaM (Array α) := do
+def findImportMatches
+      (ext : EnvExtension (IO.Ref (Option (LazyDiscrTree α))))
+      (addEntry : Name → ConstantInfo → MetaM (Array (InitEntry α)))
+      (droppedKeys : List (List LazyDiscrTree.Key) := [])
+      (constantsPerTask : Nat := 1000)
+      (ty : Expr) : MetaM (MatchResult α) := do
+  let cctx ← (read : CoreM Core.Context)
   let ngen ← getNGen
   let (cNGen, ngen) := ngen.mkChild
   setNGen ngen
@@ -913,14 +959,105 @@ def findCandidates (ext : EnvExtension (IO.Ref (Option (LazyDiscrTree α))))
   let ref := @EnvExtension.getState _ ⟨dummy⟩ ext (←getEnv)
   let importTree ← (←ref.get).getDM $ do
     profileitM Exception  "lazy discriminator import initialization" (←getOptions) $ do
-      let t ← createImportedEnvironment cNGen (←getEnv) addEntry
+      let t ← createImportedDiscrTree (createTreeCtx cctx) cNGen (←getEnv) addEntry
                 (constantsPerTask := constantsPerTask)
       dropKeys t droppedKeys
-  let (localCandidates, _) ←
-    profileitM Exception  "lazy discriminator local search" (←getOptions) $ do
-      let t ← createLocalEnvironment addEntry
-      let t ← dropKeys t droppedKeys
-      t.getMatch ty
   let (importCandidates, importTree) ← importTree.getMatch ty
-  ref.set importTree
-  pure (localCandidates ++ importCandidates)
+  ref.set (some importTree)
+  pure importCandidates
+
+/--
+A discriminator tree for the current module's declarations only.
+
+Note. We use different discriminator trees for imported and current module
+declarations since imported declarations are typically much more numerous but
+not changed after the environment is created.
+-/
+structure ModuleDiscrTreeRef (α : Type _)  where
+  ref : IO.Ref (LazyDiscrTree α)
+
+/-- Create a discriminator tree for current module declarations. -/
+def createModuleDiscrTree
+    (entriesForConst : Name → ConstantInfo → MetaM (Array (InitEntry α))) :
+    CoreM (LazyDiscrTree α) := do
+  let env ← getEnv
+  let ngen ← getChildNgen
+  let d ← ImportData.new
+  let ctx ← read
+  let t ← createLocalPreDiscrTree ctx ngen env d entriesForConst
+  (← d.errors.get).forM logImportFailure
+  pure <| t.toLazy
+
+/--
+Creates reference for lazy discriminator tree that only contains this module's definitions.
+-/
+def createModuleTreeRef (entriesForConst : Name → ConstantInfo → MetaM (Array (InitEntry α)))
+    (droppedKeys : List (List LazyDiscrTree.Key)) : MetaM (ModuleDiscrTreeRef α) := do
+  profileitM Exception "build module discriminator tree" (←getOptions) $ do
+    let t ← createModuleDiscrTree entriesForConst
+    let t ← dropKeys t droppedKeys
+    pure { ref := ← IO.mkRef t }
+
+/--
+Returns candidates from this module in this module that match the expression.
+
+* `moduleRef` is a references to a lazy discriminator tree only containing
+this module's definitions.
+-/
+def findModuleMatches (moduleRef : ModuleDiscrTreeRef α) (ty : Expr) : MetaM (MatchResult α) := do
+  profileitM Exception  "lazy discriminator local search" (← getOptions) $ do
+    let discrTree ← moduleRef.ref.get
+    let (localCandidates, localTree) ← discrTree.getMatch ty
+    moduleRef.ref.set localTree
+    pure localCandidates
+
+/--
+`findMatchesExt` searches for entries in a lazily initialized discriminator tree.
+
+It provides some additional capabilities beyond `findMatches` to adjust results
+based on priority and cache module declarations
+
+* `modulesTreeRef` points to the discriminator tree for local environment.
+  Used for caching and created by `createLocalTree`.
+* `ext` should be an environment extension with an IO.Ref for caching the import lazy
+   discriminator tree.
+* `addEntry` is the function for creating discriminator tree entries from constants.
+* `droppedKeys` contains keys we do not want to consider when searching for matches.
+  It is used for dropping very general keys.
+* `constantsPerTask` stores number of constants in imported modules used to
+  decide when to create new task.
+* `adjustResult` takes the priority and value to produce a final result.
+* `ty` is the expression type.
+-/
+def findMatchesExt
+    (moduleTreeRef : ModuleDiscrTreeRef α)
+    (ext : EnvExtension (IO.Ref (Option (LazyDiscrTree α))))
+    (addEntry : Name → ConstantInfo → MetaM (Array (InitEntry α)))
+    (droppedKeys : List (List LazyDiscrTree.Key) := [])
+    (constantsPerTask : Nat := 1000)
+    (adjustResult : Nat → α → β)
+    (ty : Expr) : MetaM (Array β) := do
+  let moduleMatches ← findModuleMatches moduleTreeRef ty
+  let importMatches ← findImportMatches ext addEntry droppedKeys constantsPerTask ty
+  return Array.mkEmpty (moduleMatches.size + importMatches.size)
+          |> moduleMatches.appendResultsAux (f := adjustResult)
+          |> importMatches.appendResultsAux (f := adjustResult)
+
+/--
+`findMatches` searches for entries in a lazily initialized discriminator tree.
+
+* `ext` should be an environment extension with an IO.Ref for caching the import lazy
+   discriminator tree.
+* `addEntry` is the function for creating discriminator tree entries from constants.
+* `droppedKeys` contains keys we do not want to consider when searching for matches.
+  It is used for dropping very general keys.
+-/
+def findMatches (ext : EnvExtension (IO.Ref (Option (LazyDiscrTree α))))
+    (addEntry : Name → ConstantInfo → MetaM (Array (InitEntry α)))
+    (droppedKeys : List (List LazyDiscrTree.Key) := [])
+    (constantsPerTask : Nat := 1000)
+    (ty : Expr) : MetaM (Array α) := do
+
+  let moduleTreeRef ← createModuleTreeRef addEntry droppedKeys
+  let incPrio _ v := v
+  findMatchesExt moduleTreeRef ext addEntry droppedKeys constantsPerTask incPrio ty

src/Lean/Meta/Match/MatchEqs.lean

@@ -649,10 +649,13 @@ where
 private partial def mkEquationsFor (matchDeclName : Name) :  MetaM MatchEqns := withLCtx {} {} do
   trace[Meta.Match.matchEqs] "mkEquationsFor '{matchDeclName}'"
   withConfig (fun c => { c with etaStruct := .none }) do
-  let baseName := mkPrivateName (← getEnv) matchDeclName
+  let baseName := matchDeclName
+  let splitterName := baseName ++ `splitter
   let constInfo ← getConstInfo matchDeclName
   let us := constInfo.levelParams.map mkLevelParam
   let some matchInfo ← getMatcherInfo? matchDeclName | throwError "'{matchDeclName}' is not a matcher function"
+  -- `alreadyDeclared` is `true` if matcher equations were defined in an imported module
+  let alreadyDeclared := (← getEnv).contains splitterName
   let numDiscrEqs := getNumEqsFromDiscrInfos matchInfo.discrInfos
   forallTelescopeReducing constInfo.type fun xs matchResultType => do
     let mut eqnNames := #[]
@@ -687,52 +690,59 @@ private partial def mkEquationsFor (matchDeclName : Name) :  MetaM MatchEqns :=
         for discr in discrs.toArray.reverse, pattern in patterns.reverse do
           notAlt ← mkArrow (← mkEqHEq discr pattern) notAlt
         notAlt ← mkForallFVars (discrs ++ ys) notAlt
-        /- Recall that when we use the `h : discr`, the alternative type depends on the discriminant.
-           Thus, we need to create new `alts`. -/
-        withNewAlts numDiscrEqs discrs patterns alts fun alts => do
-          let alt := alts[i]!
-          let lhs := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ patterns ++ alts)
-          let rhs := mkAppN alt rhsArgs
-          let thmType ← mkEq lhs rhs
-          let thmType ← hs.foldrM (init := thmType) (mkArrow · ·)
-          let thmType ← mkForallFVars (params ++ #[motive] ++ ys ++ alts) thmType
-          let thmType ← unfoldNamedPattern thmType
-          let thmVal ← proveCondEqThm matchDeclName thmType
-          addDecl <| Declaration.thmDecl {
-            name        := thmName
-            levelParams := constInfo.levelParams
-            type        := thmType
-            value       := thmVal
-          }
-          return (notAlt, splitterAltType, splitterAltNumParam, argMask)
+        if alreadyDeclared then
+          -- If the matcher equations and splitter have already been declared, the only
+          -- values we are `notAlt` and `splitterAltNumParam`. This code is a bit hackish.
+          return (notAlt, default, splitterAltNumParam, default)
+        else
+          /- Recall that when we use the `h : discr`, the alternative type depends on the discriminant.
+             Thus, we need to create new `alts`. -/
+          withNewAlts numDiscrEqs discrs patterns alts fun alts => do
+            let alt := alts[i]!
+            let lhs := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ patterns ++ alts)
+            let rhs := mkAppN alt rhsArgs
+            let thmType ← mkEq lhs rhs
+            let thmType ← hs.foldrM (init := thmType) (mkArrow · ·)
+            let thmType ← mkForallFVars (params ++ #[motive] ++ ys ++ alts) thmType
+            let thmType ← unfoldNamedPattern thmType
+            let thmVal ← proveCondEqThm matchDeclName thmType
+            addDecl <| Declaration.thmDecl {
+              name        := thmName
+              levelParams := constInfo.levelParams
+              type        := thmType
+              value       := thmVal
+            }
+            return (notAlt, splitterAltType, splitterAltNumParam, argMask)
       notAlts := notAlts.push notAlt
       splitterAltTypes := splitterAltTypes.push splitterAltType
       splitterAltNumParams := splitterAltNumParams.push splitterAltNumParam
       altArgMasks := altArgMasks.push argMask
       trace[Meta.Match.matchEqs] "splitterAltType: {splitterAltType}"
       idx := idx + 1
-    -- Define splitter with conditional/refined alternatives
-    withSplitterAlts splitterAltTypes fun altsNew => do
-      let splitterParams := params.toArray ++ #[motive] ++ discrs.toArray ++ altsNew
-      let splitterType ← mkForallFVars splitterParams matchResultType
-      trace[Meta.Match.matchEqs] "splitterType: {splitterType}"
-      let template := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ discrs ++ alts)
-      let template ← deltaExpand template (· == constInfo.name)
-      let template := template.headBeta
-      let splitterVal ← mkLambdaFVars splitterParams (← mkSplitterProof matchDeclName template alts altsNew splitterAltNumParams altArgMasks)
-      let splitterName := baseName ++ `splitter
-      addAndCompile <| Declaration.defnDecl {
-        name        := splitterName
-        levelParams := constInfo.levelParams
-        type        := splitterType
-        value       := splitterVal
-        hints       := .abbrev
-        safety      := .safe
-      }
-      setInlineAttribute splitterName
-      let result := { eqnNames, splitterName, splitterAltNumParams }
-      registerMatchEqns matchDeclName result
-      return result
+    if alreadyDeclared then
+      return { eqnNames, splitterName, splitterAltNumParams }
+    else
+      -- Define splitter with conditional/refined alternatives
+      withSplitterAlts splitterAltTypes fun altsNew => do
+        let splitterParams := params.toArray ++ #[motive] ++ discrs.toArray ++ altsNew
+        let splitterType ← mkForallFVars splitterParams matchResultType
+        trace[Meta.Match.matchEqs] "splitterType: {splitterType}"
+        let template := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ discrs ++ alts)
+        let template ← deltaExpand template (· == constInfo.name)
+        let template := template.headBeta
+        let splitterVal ← mkLambdaFVars splitterParams (← mkSplitterProof matchDeclName template alts altsNew splitterAltNumParams altArgMasks)
+        addAndCompile <| Declaration.defnDecl {
+          name        := splitterName
+          levelParams := constInfo.levelParams
+          type        := splitterType
+          value       := splitterVal
+          hints       := .abbrev
+          safety      := .safe
+        }
+        setInlineAttribute splitterName
+        let result := { eqnNames, splitterName, splitterAltNumParams }
+        registerMatchEqns matchDeclName result
+        return result
 
 /- See header at `MatchEqsExt.lean` -/
 @[export lean_get_match_equations_for]
@@ -743,4 +753,23 @@ def getEquationsForImpl (matchDeclName : Name) : MetaM MatchEqns := do
 
 builtin_initialize registerTraceClass `Meta.Match.matchEqs
 
+private def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
+  unless (← isMatcher declName) do
+    return none
+  let result ← getEquationsForImpl declName
+  return some result.eqnNames
+
+builtin_initialize
+  registerGetEqnsFn getEqnsFor?
+
+/-
+We register `foo.match_<idx>.splitter` as a reserved name, but
+we do not install a realizer. The `splitter` will be generated by the
+`foo.match_<idx>.eq_<idx>` realizer.
+-/
+builtin_initialize registerReservedNamePredicate fun env n =>
+  match n with
+  | .str p "splitter" => isMatcherCore env p
+  | _ => false
+
 end Lean.Meta.Match

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

@@ -176,16 +176,32 @@ def arrowDomainsN (n : Nat) (type : Expr) : MetaM (Array Expr) := do
     type := β
   return ts
 
+private def withUserNamesImpl {α} (fvars : Array Expr) (names : Array Name) (k : MetaM α) : MetaM α := do
+  let lctx := (Array.zip fvars names).foldl (init := ← (getLCtx)) fun lctx (fvar, name) =>
+    lctx.setUserName fvar.fvarId! name
+  withTheReader Meta.Context (fun ctx => { ctx with lctx }) k
+
 /--
 Sets the user name of the FVars in the local context according to the given array of names.
 
 If they differ in size the shorter size wins.
 -/
-def withUserNames {α} (fvars : Array Expr) (names : Array Name) (k : MetaM α ) : MetaM α := do
-  let lctx := (Array.zip fvars names).foldl (init := ← (getLCtx)) fun lctx (fvar, name) =>
-    lctx.setUserName fvar.fvarId! name
-  withTheReader Meta.Context (fun ctx => { ctx with lctx }) k
+def withUserNames {n} [MonadControlT MetaM n] [Monad n]
+  {α} (fvars : Array Expr) (names : Array Name) (k : n α) : n α := do
+  mapMetaM (withUserNamesImpl fvars names) k
 
+/-
+`Match.forallAltTelescope` lifted to a monad transformer
+(and only passing those arguments that we care about below)
+-/
+private def forallAltTelescope'
+    {n} [Monad n] [MonadControlT MetaM n]
+    {α} (origAltType : Expr) (numParams numDiscrEqs : Nat)
+    (k : Array Expr → Array Expr → n α) : n α := do
+  map2MetaM (fun k =>
+    Match.forallAltTelescope origAltType (numParams - numDiscrEqs) 0
+      fun ys _eqs args _mask _bodyType => k ys args
+  ) k
 
 /--
 Performs a possibly type-changing transformation to a `MatcherApp`.
@@ -208,14 +224,17 @@ This function works even if the the type of alternatives do *not* fit the inferr
 allows you to post-process the `MatcherApp` with `MatcherApp.inferMatchType`, which will
 infer a type, given all the alternatives.
 -/
-def transform (matcherApp : MatcherApp)
+def transform
+    {n} [MonadLiftT MetaM n] [MonadControlT MetaM n] [Monad n] [MonadError n] [MonadEnv n] [MonadLog n]
+    [AddMessageContext n] [MonadOptions n]
+    (matcherApp : MatcherApp)
     (useSplitter := false)
     (addEqualities : Array Bool := mkArray matcherApp.discrs.size false)
-    (onParams : Expr → MetaM Expr := pure)
-    (onMotive : Array Expr → Expr → MetaM Expr := fun _ e => pure e)
-    (onAlt : Expr → Expr → MetaM Expr := fun _ e => pure e)
-    (onRemaining : Array Expr → MetaM (Array Expr) := pure) :
-    MetaM MatcherApp := do
+    (onParams : Expr → n Expr := pure)
+    (onMotive : Array Expr → Expr → n Expr := fun _ e => pure e)
+    (onAlt : Expr → Expr → n Expr := fun _ e => pure e)
+    (onRemaining : Array Expr → n (Array Expr) := pure) :
+    n MatcherApp := do
 
   if addEqualities.size != matcherApp.discrs.size then
     throwError "MatcherApp.transform: addEqualities has wrong size"
@@ -247,7 +266,7 @@ def transform (matcherApp : MatcherApp)
 
     -- Prepend (x = e) → to the motive when an equality is requested
     for arg in motiveArgs, discr in discrs', b in addEqualities do if b then
-      motiveBody' ← mkArrow (← mkEq discr arg) motiveBody'
+      motiveBody' ← liftMetaM <| mkArrow (← mkEq discr arg) motiveBody'
 
     return (← mkLambdaFVars motiveArgs motiveBody', ← getLevel motiveBody')
 
@@ -272,7 +291,7 @@ def transform (matcherApp : MatcherApp)
     let aux1 := mkApp aux1 motive'
     let aux1 := mkAppN aux1 discrs'
     unless (← isTypeCorrect aux1) do
-      logError m!"failed to transform matcher, type error when constructing new motive:{indentExpr aux1}"
+      logError m!"failed to transform matcher, type error when constructing new pre-splitter motive:{indentExpr aux1}"
       check aux1
     let origAltTypes ← arrowDomainsN matcherApp.alts.size (← inferType aux1)
 
@@ -280,7 +299,7 @@ def transform (matcherApp : MatcherApp)
     let aux2 := mkApp aux2 motive'
     let aux2 := mkAppN aux2 discrs'
     unless (← isTypeCorrect aux2) do
-      logError m!"failed to transform matcher, type error when constructing new motive:{indentExpr aux2}"
+      logError m!"failed to transform matcher, type error when constructing splitter motive:{indentExpr aux2}"
       check aux2
     let altTypes ← arrowDomainsN matcherApp.alts.size (← inferType aux2)
 
@@ -290,7 +309,7 @@ def transform (matcherApp : MatcherApp)
         splitterNumParams in matchEqns.splitterAltNumParams,
         origAltType in origAltTypes,
         altType in altTypes do
-      let alt' ← Match.forallAltTelescope origAltType (numParams - numDiscrEqs) 0 fun ys _eqs args _mask _bodyType => do
+      let alt' ← forallAltTelescope' origAltType (numParams - numDiscrEqs) 0 fun ys args => do
         let altType ← instantiateForall altType ys
         -- The splitter inserts its extra paramters after the first ys.size parameters, before
         -- the parameters for the numDiscrEqs
@@ -320,7 +339,6 @@ def transform (matcherApp : MatcherApp)
     let aux := mkApp aux motive'
     let aux := mkAppN aux discrs'
     unless (← isTypeCorrect aux) do
-      -- check aux
       logError m!"failed to transform matcher, type error when constructing new motive:{indentExpr aux}"
       check aux
     let altTypes ← arrowDomainsN matcherApp.alts.size (← inferType aux)

src/Lean/Meta/Tactic.lean

@@ -38,3 +38,5 @@ import Lean.Meta.Tactic.Symm
 import Lean.Meta.Tactic.Backtrack
 import Lean.Meta.Tactic.SolveByElim
 import Lean.Meta.Tactic.FunInd
+import Lean.Meta.Tactic.Rfl
+import Lean.Meta.Tactic.Rewrites