perf: use structural equality at ACLt

closes #3705

test: for issue

.github/workflows/ci.yml

@@ -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

@@ -149,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,31 @@ 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 options `pp.mvars` (default: true) and `pp.mvars.withType` (default: false).
+  When `pp.mvars` is false, metavariables pretty print as `?_`,
+  and when `pp.mvars.withType` is true, metavariables pretty print with a type ascription.
+  These can be set when using `#guard_msgs` to make tests not rely on the unique ids assigned to anonymous metavariables.
+  [#3798](https://github.com/leanprover/lean4/pull/3798).
+
+* 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 +110,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
 ---------
 

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;
       });

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,16 @@
     },
     "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"
       }
@@ -118,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": {
@@ -140,6 +160,21 @@
         "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"
+      }
     }
   },
   "root": "root",

nix/bootstrap.nix

@@ -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 =

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
@@ -742,10 +732,8 @@ def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
     a.pop
 termination_by a.size - i.val
 
-derive_functional_induction feraseIdx
-
 theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
-  induction a, i using feraseIdx.induct with
+  induction a, i using Array.feraseIdx.induct with
   | @case1 a i h a' _ _ ih =>
     unfold feraseIdx
     simp [h, a', ih]

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]
@@ -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

@@ -119,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`.
 -/
@@ -215,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
 
 /--

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
@@ -134,11 +137,13 @@ theorem add_le_iff_le_sub (a b c : Int) : a + b ≤ c ↔ a ≤ c - b := by
     lhs
     rw [← Int.add_zero c, ← Int.sub_self (-b), Int.sub_eq_add_neg, ← Int.add_assoc, Int.neg_neg,
       Int.add_le_add_iff_right]
+  try rfl -- stage0 update TODO: Change this to rfl or remove
 
 theorem le_add_iff_sub_le (a b c : Int) : a ≤ b + c ↔ a - c ≤ b := by
   conv =>
     lhs
     rw [← Int.neg_neg c, ← Int.sub_eq_add_neg, ← add_le_iff_le_sub]
+  try rfl -- stage0 update TODO: Change this to rfl or remove
 
 theorem add_le_zero_iff_le_neg (a b : Int) : a + b ≤ 0 ↔ a ≤ - b := by
   rw [add_le_iff_le_sub, Int.zero_sub]

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/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,13 +368,18 @@ 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, that is, a relation which has a reflexive lemma tagged with the attribute [refl].
+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
 
@@ -907,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
@@ -1318,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.
@@ -1501,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/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₀
 

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/Structural/Main.lean

@@ -101,6 +101,7 @@ def structuralRecursion (preDefs : Array PreDefinition) : TermElabM Unit :=
         -/
         registerEqnsInfo preDef recArgPos
     addSmartUnfoldingDef preDef recArgPos
+    markAsRecursive preDef.declName
     applyAttributesOf #[preDefNonRec] AttributeApplicationTime.afterCompilation
 
 builtin_initialize

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/PreDefinition/WF/Main.lean

@@ -144,6 +144,7 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
   let preDefs ← preDefs.mapM (abstractNestedProofs ·)
   registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize argsPacker
   for preDef in preDefs do
+    markAsRecursive preDef.declName
     applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
 
 builtin_initialize registerTraceClass `Elab.definition.wf

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

@@ -39,3 +39,4 @@ 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/Conv/Basic.lean

@@ -115,7 +115,7 @@ def evalSepByIndentConv (stx : Syntax) : TacticM Unit := do
     -- save state before/after entering focus on `{`
     withInfoContext (pure ()) initInfo
     evalSepByIndentConv stx[1]
-    evalTactic (← `(tactic| all_goals (try rfl)))
+    evalTactic (← `(tactic| all_goals (try with_reducible rfl)))
 
 @[builtin_tactic Lean.Parser.Tactic.Conv.nestedConv] def evalNestedConv : Tactic := fun stx => do
   evalConvSeqBracketed stx[0]
@@ -163,7 +163,7 @@ private def convTarget (conv : Syntax) : TacticM Unit := withMainContext do
    let target ← getMainTarget
    let (targetNew, proof) ← convert target (withTacticInfoContext (← getRef) (evalTactic conv))
    liftMetaTactic1 fun mvarId => mvarId.replaceTargetEq targetNew proof
-   evalTactic (← `(tactic| try rfl))
+   evalTactic (← `(tactic| try with_reducible rfl))
 
 private def convLocalDecl (conv : Syntax) (hUserName : Name) : TacticM Unit := withMainContext do
    let localDecl ← getLocalDeclFromUserName hUserName

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

@@ -10,19 +10,12 @@ import Lean.Elab.Tactic.Basic
 /-!
 # `rfl` tactic extension for reflexive relations
 
-This extends the `rfl` tactic so that it works on any reflexive relation,
+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
 
-/--
-This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive
-relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl].
--/
-elab_rules : tactic
-  | `(tactic| rfl) => withMainContext do liftMetaFinishingTactic (·.applyRfl)
-
 @[builtin_tactic Lean.Parser.Tactic.applyRfl] def evalApplyRfl : Tactic := fun stx =>
   match stx with
   | `(tactic| apply_rfl) => withMainContext do liftMetaFinishingTactic (·.applyRfl)

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/ACLt.lean

@@ -50,7 +50,7 @@ mutual
    - We ignore metadata.
    - We ignore universe parameterst at constants.
 -/
-unsafe def main (a b : Expr) (mode : ReduceMode := .none) : MetaM Bool :=
+partial def main (a b : Expr) (mode : ReduceMode := .none) : MetaM Bool := do
   lt a b
 where
   reduce (e : Expr) : MetaM Expr := do
@@ -66,7 +66,9 @@ where
       | .none => return e
 
   lt (a b : Expr) : MetaM Bool := do
-    if ptrAddrUnsafe a == ptrAddrUnsafe b then
+    if a == b then
+      -- We used to have an "optimization" using only pointer equality.
+      -- This was a bad idea, `==` is often much cheaper than `acLt`.
       return false
     -- We ignore metadata
     else if a.isMData then
@@ -84,6 +86,16 @@ where
     else
       lt a₂ b₂
 
+  getParamsInfo (f : Expr) (numArgs : Nat) : MetaM (Array ParamInfo) := do
+    -- Ensure `f` does not have loose bound variables. This may happen in
+    -- since we go inside binders without extending the local context.
+    -- See `lexSameCtor` and `allChildrenLt`
+    -- See issue #3705.
+    if f.hasLooseBVars then
+      return #[]
+    else
+      return (← getFunInfoNArgs f numArgs).paramInfo
+
   ltApp (a b : Expr) : MetaM Bool := do
     let aFn := a.getAppFn
     let bFn := b.getAppFn
@@ -99,7 +111,7 @@ where
       else if aArgs.size > bArgs.size then
         return false
       else
-        let infos := (← getFunInfoNArgs aFn aArgs.size).paramInfo
+        let infos ← getParamsInfo aFn aArgs.size
         for i in [:infos.size] do
           -- We ignore instance implicit arguments during comparison
           if !infos[i]!.isInstImplicit then
@@ -137,7 +149,7 @@ where
     | .proj _ _ e ..    => lt e b
     | .app ..           =>
       a.withApp fun f args => do
-        let infos := (← getFunInfoNArgs f args.size).paramInfo
+        let infos ← getParamsInfo f args.size
         for i in [:infos.size] do
           -- We ignore instance implicit arguments during comparison
           if !infos[i]!.isInstImplicit then
@@ -176,7 +188,8 @@ end
 
 end ACLt
 
-@[implemented_by ACLt.main, inherit_doc ACLt.main]
-opaque Expr.acLt : Expr → Expr → (mode : ACLt.ReduceMode := .none) → MetaM Bool
+@[inherit_doc ACLt.main]
+def acLt (a b : Expr) (mode : ACLt.ReduceMode := .none) : MetaM Bool :=
+  ACLt.main a b mode
 
 end Lean.Meta

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
@@ -1444,6 +1444,12 @@ def whnfD (e : Expr) : MetaM Expr :=
 def whnfI (e : Expr) : MetaM Expr :=
   withTransparency TransparencyMode.instances <| whnf e
 
+/-- `whnf` with at most instances transparency. -/
+def whnfAtMostI (e : Expr) : MetaM Expr := do
+  match (← getTransparency) with
+  | .all | .default => withTransparency TransparencyMode.instances <| whnf e
+  | _ => whnf e
+
 /--
   Mark declaration `declName` with the attribute `[inline]`.
   This method does not check whether the given declaration is a definition.

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

@@ -7,31 +7,64 @@ prelude
 import Lean.ReservedNameAction
 import Lean.Meta.Basic
 import Lean.Meta.AppBuilder
+import Lean.Meta.Match.MatcherInfo
 
 namespace Lean.Meta
+/--
+Environment extension for storing which declarations are recursive.
+This information is populated by the `PreDefinition` module, but the simplifier
+uses when unfolding declarations.
+-/
+builtin_initialize recExt : TagDeclarationExtension ← mkTagDeclarationExtension `recExt
+
+/--
+Marks the given declaration as recursive.
+-/
+def markAsRecursive (declName : Name) : CoreM Unit :=
+  modifyEnv (recExt.tag · declName)
+
+/--
+Returns `true` if `declName` was defined using well-founded recursion, or structural recursion.
+-/
+def isRecursiveDefinition (declName : Name) : CoreM Bool :=
+  return recExt.isTagged (← getEnv) declName
+
+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
-  | .str p s => (isEqnReservedNameSuffix s || isUnfoldReservedNameSuffix s) && env.isSafeDefinition p
+  | .str p s =>
+    (isEqnReservedNameSuffix s || isUnfoldReservedNameSuffix s)
+    && env.isSafeDefinition p
+    -- Remark: `f.match_<idx>.eq_<idx>` are private definitions and are not treated as reserved names
+    -- Reason: `f.match_<idx>.splitter is generated at the same time, and can eliminate into type.
+    -- Thus, it cannot be defined in different modules since it is not a theorem, and is used to generate code.
+    && !isMatcherCore env p
   | _ => false
 
 def GetEqnsFn := Name → MetaM (Option (Array Name))
@@ -87,7 +120,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 +155,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 +185,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 +232,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/ExprDefEq.lean

@@ -1690,9 +1690,9 @@ private def isDefEqOnFailure (t s : Expr) : MetaM Bool := do
     tryUnificationHints t s <||> tryUnificationHints s t
 
 private def isDefEqProj : Expr → Expr → MetaM Bool
-  | Expr.proj m i t, Expr.proj n j s => pure (i == j && m == n) <&&> Meta.isExprDefEqAux t s
-  | Expr.proj structName 0 s, v => isDefEqSingleton structName s v
-  | v, Expr.proj structName 0 s => isDefEqSingleton structName s v
+  | .proj m i t, .proj n j s => pure (i == j && m == n) <&&> Meta.isExprDefEqAux t s
+  | .proj structName 0 s, v  => isDefEqSingleton structName s v
+  | v, .proj structName 0 s  => isDefEqSingleton structName s v
   | _, _ => pure false
 where
   /-- If `structName` is a structure with a single field and `(?m ...).1 =?= v`, then solve constraint as `?m ... =?= ⟨v⟩` -/
@@ -1779,25 +1779,30 @@ private def isExprDefEqExpensive (t : Expr) (s : Expr) : MetaM Bool := do
   whenUndefDo (isDefEqEta t s) do
   whenUndefDo (isDefEqEta s t) do
   if (← isDefEqProj t s) then return true
-  whenUndefDo (isDefEqNative t s) do
-  whenUndefDo (isDefEqNat t s) do
-  whenUndefDo (isDefEqOffset t s) do
-  whenUndefDo (isDefEqDelta t s) do
-  -- We try structure eta *after* lazy delta reduction;
-  -- otherwise we would end up applying it at every step of a reduction chain
-  -- as soon as one of the sides is a constructor application,
-  -- which is very costly because it requires us to unify the fields.
-  if (← (isDefEqEtaStruct t s <||> isDefEqEtaStruct s t)) then
-    return true
-  if t.isConst && s.isConst then
-    if t.constName! == s.constName! then isListLevelDefEqAux t.constLevels! s.constLevels! else return false
-  else if (← pure t.isApp <&&> pure s.isApp <&&> isDefEqApp t s) then
-    return true
+  let t' ← whnfCore t
+  let s' ← whnfCore s
+  if t != t' || s != s' then
+    Meta.isExprDefEqAux t' s'
   else
-    whenUndefDo (isDefEqProjInst t s) do
-    whenUndefDo (isDefEqStringLit t s) do
-    if (← isDefEqUnitLike t s) then return true else
-    isDefEqOnFailure t s
+    whenUndefDo (isDefEqNative t s) do
+    whenUndefDo (isDefEqNat t s) do
+    whenUndefDo (isDefEqOffset t s) do
+    whenUndefDo (isDefEqDelta t s) do
+    -- We try structure eta *after* lazy delta reduction;
+    -- otherwise we would end up applying it at every step of a reduction chain
+    -- as soon as one of the sides is a constructor application,
+    -- which is very costly because it requires us to unify the fields.
+    if (← (isDefEqEtaStruct t s <||> isDefEqEtaStruct s t)) then
+      return true
+    if t.isConst && s.isConst then
+      if t.constName! == s.constName! then isListLevelDefEqAux t.constLevels! s.constLevels! else return false
+    else if (← pure t.isApp <&&> pure s.isApp <&&> isDefEqApp t s) then
+      return true
+    else
+      whenUndefDo (isDefEqProjInst t s) do
+      whenUndefDo (isDefEqStringLit t s) do
+      if (← isDefEqUnitLike t s) then return true else
+      isDefEqOnFailure t s
 
 inductive DefEqCacheKind where
   | transient -- problem has mvars or is using nonstandard configuration, we should use transient cache
@@ -1863,14 +1868,41 @@ partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecD
   whenUndefDo (isDefEqProofIrrel t s) do
   /-
     We also reduce projections here to prevent expensive defeq checks when unifying TC operations.
-    When unifying e.g. `@Neg.neg α (@Field.toNeg α inst1) =?= @Neg.neg α (@Field.toNeg α inst2)`,
+    When unifying e.g. `(@Field.toNeg α inst1).1 =?= (@Field.toNeg α inst2).1`,
     we only want to unify negation (and not all other field operations as well).
     Unifying the field instances slowed down unification: https://github.com/leanprover/lean4/issues/1986
-    We used to *not* reduce projections here, to support unifying `(?a).1 =?= (x, y).1`.
-    NOTE: this still seems to work because we don't eagerly unfold projection definitions to primitive projections.
+
+    Note that ew use `proj := .yesWithDeltaI` to ensure `whnfAtMostI` is used to reduce the projection structure.
+    We added this refinement to address a performance issue in code such as
+    ```
+    let val : Test := bar c1 key
+    have : val.1 = (bar c1 key).1 := rfl
+    ```
+    where `bar` is a complex function that takes a long time to be reduced.
+
+    Note that the current solution times out at unification problems such as
+    `(f x).1 =?= (g x).1` where `f`, `g` are defined as
+    ```
+    structure Foo where
+      x : Nat
+      y : Nat
+
+    def f (x : Nat) : Foo :=
+      { x, y := ack 10 10 }
+
+    def g (x : Nat) : Foo :=
+      { x, y := ack 10 11 }
+    ```
+    and `ack` is ackermann. We claim this is an abuse of the unifier.
+    That being said, we could in principle address this issue by implementing
+    lazy-delta reduction at `isDefEqProj`.
+
+    The current solution should be sufficient. In the past, we have used
+    `whnfCore t (config := { proj := .yes })` which more conservative than `.yesWithDeltaI`,
+    and it only created performance issues when handling TC unification problems.
   -/
-  let t' ← whnfCore t
-  let s' ← whnfCore s
+  let t' ← whnfCore t (config := { proj := .yesWithDeltaI })
+  let s' ← whnfCore s (config := { proj := .yesWithDeltaI })
   if t != t' || s != s' then
     isExprDefEqAuxImpl t' s'
   else

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,7 +649,15 @@ 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
+  /-
+  Remark: user have requested the `split` tactic to be available for writing code.
+  Thus, the `splitter` declaration must be a definition instead of a theorem.
+  Moreover, the `splitter` is generated on demand, and we currently
+  can't import the same definition from different modules. Thus, we must
+  keep `splitter` as a private declaration to prevent import failures.
+  -/
   let baseName := mkPrivateName (← getEnv) 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"
@@ -720,7 +728,6 @@ private partial def mkEquationsFor (matchDeclName : Name) :  MetaM MatchEqns :=
       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

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

@@ -39,3 +39,4 @@ 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

src/Lean/Meta/Tactic/FunInd.lean

@@ -13,20 +13,21 @@ import Lean.Meta.Tactic.Subst
 import Lean.Meta.Injective -- for elimOptParam
 import Lean.Meta.ArgsPacker
 import Lean.Elab.PreDefinition.WF.Eqns
+import Lean.Elab.PreDefinition.Structural.Eqns
 import Lean.Elab.Command
+import Lean.Meta.Tactic.ElimInfo
 
 /-!
-This module contains code to derive, from the definition of a recursive function
-(or mutually recursive functions) defined by well-founded recursion, a
-**functional induction principle** tailored to proofs about that function(s). For
-example from:
+This module contains code to derive, from the definition of a recursive function (structural or
+well-founded, possibly mutual), a **functional induction principle** tailored to proofs about that
+function(s).
 
+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
 ```
@@ -59,7 +60,7 @@ by `MVarId.cleanup`).
 Mutual recursion is supported and results in multiple motives.
 
 
-## Implementation overview
+## Implementation overview (well-founded recursion)
 
 For a non-mutual, unary function `foo` (or else for the `_unary` function), we
 
@@ -129,6 +130,8 @@ For a non-mutual, unary function `foo` (or else for the `_unary` function), we
 
 The resulting term then becomes `foo.induct` at its inferred type.
 
+## Implementation overview (mutual/non-unary well-founded recursion)
+
 If `foo` is not unary and/or part of a mutual reduction, then the induction theorem for `foo._unary`
 (i.e. the unary non-mutual recursion function produced by the equation compiler)
 of the form
@@ -154,8 +157,30 @@ foo.induct : {motive1 : a → b → Prop} {motive2 : c → Prop} →
   (x : a) → (y : b) → motive1 x y
 ```
 
+## Implementation overview (structural recursion)
+
+When handling structural recursion, the overall approach is the same, with the following
+differences:
+
+* Instead of `WellFounded.fix` we look for a `.brecOn` application, using `isBRecOnRecursor`
+
+  Despite its name, this function does *not* recognize the `.brecOn` of inductive *predicates*,
+  which we also do not support at this point.
+
+* The elaboration of structurally recursive function can handle extra arguments. We keep the
+  `motive` parameters in the original order.
+
+* The “induction hyothesis” in a `.brecOn` call is a `below x` term that contains all the possible
+  recursive calls, whic are projected out using `.fst.snd.…`. The `is_wf` flag that we pass down
+  tells us which form of induction hypothesis we are looking for.
+
+* If we have nested recursion (`foo n (foo m acc))`), then we need to infer the argument `m` of the
+  nested call `ih.fst.snd acc`. To do so reliably, we replace the `ih` with the “new `ih`”, which
+  will have type `motive m acc`, and since `motive` is a FVar we can then read off the arguments
+  off this nicely..
 -/
 
+
 set_option autoImplicit false
 
 namespace Lean.Tactic.FunInd
@@ -166,32 +191,81 @@ open Lean Elab Meta
 This is used when replacing parameters with different expressions.
 This way it will not be picked up by metavariables.
 -/
-def removeLamda {α} (e : Expr) (k : FVarId → Expr →  MetaM α) : MetaM α := do
+def removeLamda {n} [MonadLiftT MetaM n] [MonadError n] [MonadNameGenerator n] [Monad n] {α} (e : Expr) (k : FVarId → Expr → n α) : n α := do
   let .lam _n _d b _bi := ← whnfD e | throwError "removeLamda: expected lambda, got {e}"
   let x ← mkFreshFVarId
   let b := b.instantiate1 (.fvar x)
   k x b
 
-/-- Replace calls to oldIH back to calls to the original function. At the end, if `oldIH` occurs, an error is thrown. -/
-partial def foldCalls (fn : Expr) (oldIH : FVarId) (e : Expr) : MetaM Expr := do
+/-- Structural recursion only: recognizes `oldIH.fst.snd a₁ a₂` and returns `newIH.fst.snd`. -/
+partial def isPProdProj (oldIH newIH : FVarId) (e : Expr) : MetaM (Option Expr) := do
+  if e.isAppOfArity ``PProd.fst 3 then
+    if let some e' ← isPProdProj oldIH newIH e.appArg! then
+      return some (← mkAppM ``PProd.fst #[e'])
+    else
+      return none
+  else if e.isAppOfArity ``PProd.snd 3 then
+    if let some e' ← isPProdProj oldIH newIH e.appArg! then
+      return some (← mkAppM ``PProd.snd #[e'])
+    else
+      return none
+  else if e.isFVarOf oldIH then
+    return some (mkFVar newIH)
+  else
+    return none
+
+/--
+Structural recursion only:
+Recognizes `oldIH.fst.snd a₁ a₂` and returns `newIH.fst.snd` and `#[a₁, a₂]`.
+-/
+def isPProdProjWithArgs (oldIH newIH : FVarId) (e : Expr) : MetaM (Option (Expr × Array Expr)) := do
+  if e.isAppOf ``PProd.fst || e.isAppOf ``PProd.snd then
+    let arity := e.getAppNumArgs
+    unless 3 ≤ arity do return none
+    let args := e.getAppArgsN (arity - 3)
+    if let some e' ← isPProdProj oldIH newIH (e.stripArgsN (arity - 3)) then
+      return some (e', args)
+  return none
+
+/--
+Replace calls to oldIH back to calls to the original function. At the end, if `oldIH` occurs, an
+error is thrown.
+
+The `newIH` will not show up in the output of `foldCalls`, we use it as a helper to infer the
+argument of nested recursive calls when we have structural recursion.
+-/
+partial def foldCalls (is_wf : Bool) (fn : Expr) (oldIH newIH : FVarId) (e : Expr) : MetaM Expr := do
   unless e.containsFVar oldIH do
     return e
 
-  if e.getAppNumArgs = 2 && e.getAppFn.isFVarOf oldIH then
-    let #[arg, _proof] := e.getAppArgs | unreachable!
-    let arg' ← foldCalls fn oldIH arg
-    return .app fn arg'
+  if is_wf then
+    if e.getAppNumArgs = 2 && e.getAppFn.isFVarOf oldIH then
+      let #[arg, _proof] := e.getAppArgs | unreachable!
+      let arg' ← foldCalls is_wf fn oldIH newIH arg
+      return .app fn arg'
+  else
+    if let some (e', args) ← isPProdProjWithArgs oldIH newIH e then
+      let t ← whnf (← inferType e')
+      let e' ← forallTelescopeReducing t fun xs t' => do
+        unless t'.getAppFn.isFVar do -- we expect an application of the `motive` FVar here
+          throwError m!"Unexpected type {t} of {e}: Reduced to application of {t'.getAppFn}"
+        mkLambdaFVars xs (fn.beta t'.getAppArgs)
+      let args' ← args.mapM (foldCalls is_wf fn oldIH newIH)
+      let e' := e'.beta args'
+      unless ← isTypeCorrect e' do
+        throwError m!"foldCalls: type incorrect after replacing recursive call:{indentExpr e'}"
+      return e'
 
   if let some matcherApp ← matchMatcherApp? e (alsoCasesOn := true) then
     if matcherApp.remaining.size == 1 && matcherApp.remaining[0]!.isFVarOf oldIH then
       let matcherApp' ← matcherApp.transform
-        (onParams := foldCalls fn oldIH)
+        (onParams := foldCalls is_wf fn oldIH newIH)
         (onMotive := fun _motiveArgs motiveBody => do
           let some (_extra, body) := motiveBody.arrow? | throwError "motive not an arrow"
-          foldCalls fn oldIH body)
+          foldCalls is_wf fn oldIH newIH body)
         (onAlt := fun _altType alt => do
           removeLamda alt fun oldIH alt => do
-            foldCalls fn oldIH alt)
+            foldCalls is_wf fn oldIH newIH alt)
         (onRemaining := fun _ => pure #[])
       return matcherApp'.toExpr
 
@@ -203,43 +277,43 @@ partial def foldCalls (fn : Expr) (oldIH : FVarId) (e : Expr) : MetaM Expr := do
     let e' ← withTransparency .all do whnf e
     if e == e' then
       throwError "foldCalls: cannot reduce application of {e.getAppFn} in {indentExpr e} "
-    return ← foldCalls fn oldIH e'
+    return ← foldCalls is_wf fn oldIH newIH e'
 
   if let some (n, t, v, b) := e.letFun? then
-    let t' ← foldCalls fn oldIH t
-    let v' ← foldCalls fn oldIH v
+    let t' ← foldCalls is_wf fn oldIH newIH t
+    let v' ← foldCalls is_wf fn oldIH newIH v
     return ← withLocalDecl n .default t' fun x => do
-      let b' ← foldCalls fn oldIH (b.instantiate1 x)
+      let b' ← foldCalls is_wf fn oldIH newIH (b.instantiate1 x)
       mkLetFun x v' b'
 
   match e with
   | .app e1 e2 =>
-    return .app (← foldCalls fn oldIH e1) (← foldCalls fn oldIH e2)
+    return .app (← foldCalls is_wf fn oldIH newIH e1) (← foldCalls is_wf fn oldIH newIH e2)
 
   | .lam n t body bi =>
-    let t' ← foldCalls fn oldIH t
+    let t' ← foldCalls is_wf fn oldIH newIH t
     return ← withLocalDecl n bi t' fun x => do
-      let body' ← foldCalls fn oldIH (body.instantiate1 x)
+      let body' ← foldCalls is_wf fn oldIH newIH (body.instantiate1 x)
       mkLambdaFVars #[x] body'
 
   | .forallE n t body bi =>
-    let t' ← foldCalls fn oldIH t
+    let t' ← foldCalls is_wf fn oldIH newIH t
     return ← withLocalDecl n bi t' fun x => do
-      let body' ← foldCalls fn oldIH (body.instantiate1 x)
+      let body' ← foldCalls is_wf fn oldIH newIH (body.instantiate1 x)
       mkForallFVars #[x] body'
 
   | .letE n t v b _ =>
-    let t' ← foldCalls fn oldIH t
-    let v' ← foldCalls fn oldIH v
+    let t' ← foldCalls is_wf fn oldIH newIH t
+    let v' ← foldCalls is_wf fn oldIH newIH v
     return ← withLetDecl n t' v' fun x => do
-      let b' ← foldCalls fn oldIH (b.instantiate1 x)
+      let b' ← foldCalls is_wf fn oldIH newIH (b.instantiate1 x)
       mkLetFVars  #[x] b'
 
   | .mdata m b =>
-    return .mdata m (← foldCalls fn oldIH b)
+    return .mdata m (← foldCalls is_wf fn oldIH newIH b)
 
   | .proj t i e =>
-    return .proj t i (← foldCalls fn oldIH e)
+    return .proj t i (← foldCalls is_wf fn oldIH newIH e)
 
   | .sort .. | .lit .. | .const .. | .mvar .. | .bvar .. =>
     unreachable! -- cannot contain free variables, so early exit above kicks in
@@ -248,35 +322,56 @@ partial def foldCalls (fn : Expr) (oldIH : FVarId) (e : Expr) : MetaM Expr := do
     throwError m!"collectIHs: cannot eliminate unsaturated call to induction hypothesis"
 
 
--- Non-tail-positions: Collect induction hypotheses
--- (TODO: Worth folding with `foldCalls`, like before?)
--- (TODO: Accumulated with a left fold)
-partial def collectIHs (fn : Expr) (oldIH newIH : FVarId) (e : Expr) : MetaM (Array Expr) := do
+/-
+In non-tail-positions, we collect the induction hypotheses from all the recursive calls.
+-/
+-- We could run `collectIHs` and `foldCalls` together, and save a few traversals. Not sure if it
+-- worth the extra code complexity.
+-- Also, this way of collecting arrays is not as efficient as a left-fold, but we do not expect
+-- large arrays here.
+partial def collectIHs (is_wf : Bool) (fn : Expr) (oldIH newIH : FVarId) (e : Expr) : MetaM (Array Expr) := do
   unless e.containsFVar oldIH do
     return #[]
 
-  if e.getAppNumArgs = 2 && e.getAppFn.isFVarOf oldIH then
-    let #[arg, proof] := e.getAppArgs  | unreachable!
+  if is_wf then
+    if e.getAppNumArgs = 2 && e.getAppFn.isFVarOf oldIH then
+      let #[arg, proof] := e.getAppArgs  | unreachable!
 
-    let arg' ← foldCalls fn oldIH arg
-    let proof' ← foldCalls fn oldIH proof
-    let ihs ← collectIHs fn oldIH newIH arg
+      let arg' ← foldCalls is_wf fn oldIH newIH arg
+      let proof' ← foldCalls is_wf fn oldIH newIH proof
+      let ihs ← collectIHs is_wf fn oldIH newIH arg
+
+      return ihs.push (mkApp2 (.fvar newIH) arg' proof')
+  else
+    if let some (e', args) ← isPProdProjWithArgs oldIH newIH e then
+      let args' ← args.mapM (foldCalls is_wf fn oldIH newIH)
+      let ihs ← args.concatMapM (collectIHs is_wf fn oldIH newIH)
+      let t ← whnf (← inferType e')
+      let arity ← forallTelescopeReducing t fun xs t' => do
+        unless t'.getAppFn.isFVar do -- we expect an application of the `motive` FVar here
+          throwError m!"Unexpected type {t} of {e}: Reduced to application of {t'.getAppFn}"
+        pure xs.size
+      let e' := mkAppN e' args'[:arity]
+      let eTyp ← inferType e'
+      -- The inferred type that comes out of motive projections has beta redexes
+      let eType' := eTyp.headBeta
+      return ihs.push (← mkExpectedTypeHint e' eType')
 
-    return ihs.push (mkApp2 (.fvar newIH) arg' proof')
 
   if let some (n, t, v, b) := e.letFun? then
-    let ihs1 ← collectIHs fn oldIH newIH v
-    let v' ← foldCalls fn oldIH v
+    let ihs1 ← collectIHs is_wf fn oldIH newIH v
+    let v' ← foldCalls is_wf fn oldIH newIH v
     return ← withLetDecl n t v' fun x => do
-      let ihs2 ← collectIHs fn oldIH newIH (b.instantiate1 x)
+      let ihs2 ← collectIHs is_wf fn oldIH newIH (b.instantiate1 x)
       let ihs2 ← ihs2.mapM (mkLetFVars (usedLetOnly := true) #[x] ·)
       return ihs1 ++ ihs2
 
+
   if let some matcherApp ← matchMatcherApp? e (alsoCasesOn := true) then
     if matcherApp.remaining.size == 1 && matcherApp.remaining[0]!.isFVarOf oldIH then
 
       let matcherApp' ← matcherApp.transform
-        (onParams := foldCalls fn oldIH)
+        (onParams := foldCalls is_wf fn oldIH newIH)
         (onMotive := fun xs _body => do
           -- Remove the old IH that was added in mkFix
           let eType ← newIH.getType
@@ -294,7 +389,7 @@ partial def collectIHs (fn : Expr) (oldIH newIH : FVarId) (e : Expr) : MetaM (Ar
           removeLamda alt fun oldIH' alt => do
             forallBoundedTelescope altType (some 1) fun newIH' _goal' => do
               let #[newIH'] := newIH' | unreachable!
-              let altIHs ← collectIHs fn oldIH' newIH'.fvarId! alt
+              let altIHs ← collectIHs is_wf fn oldIH' newIH'.fvarId! alt
               let altIH ← mkAndIntroN altIHs
               mkLambdaFVars #[newIH'] altIH)
         (onRemaining := fun _ => pure #[mkFVar newIH])
@@ -310,40 +405,40 @@ partial def collectIHs (fn : Expr) (oldIH newIH : FVarId) (e : Expr) : MetaM (Ar
     let e' ← withTransparency .all do whnf e
     if e == e' then
       throwError "collectIHs: cannot reduce application of {e.getAppFn} in {indentExpr e} "
-    return ← collectIHs fn oldIH newIH e'
+    return ← collectIHs is_wf fn oldIH newIH e'
 
   if e.getAppArgs.any (·.isFVarOf oldIH) then
     throwError "collectIHs: could not collect recursive calls from call {indentExpr e}"
 
   match e with
   | .letE n t v b _ =>
-    let ihs1 ← collectIHs fn oldIH newIH v
-    let v' ← foldCalls fn oldIH v
+    let ihs1 ← collectIHs is_wf fn oldIH newIH v
+    let v' ← foldCalls is_wf fn oldIH newIH v
     return ← withLetDecl n t v' fun x => do
-      let ihs2 ← collectIHs fn oldIH newIH (b.instantiate1 x)
+      let ihs2 ← collectIHs is_wf fn oldIH newIH (b.instantiate1 x)
       let ihs2 ← ihs2.mapM (mkLetFVars (usedLetOnly := true) #[x] ·)
       return ihs1 ++ ihs2
 
   | .app e1 e2 =>
-    return (← collectIHs fn oldIH newIH e1) ++ (← collectIHs fn oldIH newIH e2)
+    return (← collectIHs is_wf fn oldIH newIH e1) ++ (← collectIHs is_wf fn oldIH newIH e2)
 
   | .proj _ _ e =>
-    return ← collectIHs fn oldIH newIH e
+    return ← collectIHs is_wf fn oldIH newIH e
 
   | .forallE n t body bi =>
-    let t' ← foldCalls fn oldIH t
+    let t' ← foldCalls is_wf fn oldIH newIH t
     return ← withLocalDecl n bi t' fun x => do
-      let ihs ← collectIHs fn oldIH newIH (body.instantiate1 x)
+      let ihs ← collectIHs is_wf fn oldIH newIH (body.instantiate1 x)
       ihs.mapM (mkLambdaFVars (usedOnly := true) #[x])
 
   | .lam n t body bi =>
-    let t' ← foldCalls fn oldIH t
+    let t' ← foldCalls is_wf fn oldIH newIH t
     return ← withLocalDecl n bi t' fun x => do
-      let ihs ← collectIHs fn oldIH newIH (body.instantiate1 x)
+      let ihs ← collectIHs is_wf fn oldIH newIH (body.instantiate1 x)
       ihs.mapM (mkLambdaFVars (usedOnly := true) #[x])
 
   | .mdata _m b =>
-    return ← collectIHs fn oldIH newIH b
+    return ← collectIHs is_wf fn oldIH newIH b
 
   | .sort .. | .lit .. | .const .. | .mvar .. | .bvar .. =>
     unreachable! -- cannot contain free variables, so early exit above kicks in
@@ -368,7 +463,7 @@ def deduplicateIHs (vals : Array Expr) : MetaM (Array Expr) := do
 def assertIHs (vals : Array Expr) (mvarid : MVarId) : MetaM MVarId := do
   let mut mvarid := mvarid
   for v in vals.reverse, i in [0:vals.size] do
-    mvarid ← mvarid.assert s!"ih{i+1}" (← inferType v) v
+    mvarid ← mvarid.assert (.mkSimple s!"ih{i+1}") (← inferType v) v
   return mvarid
 
 
@@ -386,11 +481,16 @@ def substVarAfter (mvarId : MVarId) (x : FVarId) : MetaM MVarId := do
         mvarId ← trySubstVar mvarId localDecl.fvarId
     return mvarId
 
+/--
+Helper monad to traverse the function body, collecting the cases as mvars
+-/
+abbrev M α := StateT (Array MVarId) MetaM α
+
 
 /-- Base case of `buildInductionBody`: Construct a case for the final induction hypthesis.  -/
-def buildInductionCase (fn : Expr) (oldIH newIH : FVarId) (toClear toPreserve : Array FVarId)
-    (goal : Expr) (IHs : Array Expr) (e : Expr) : MetaM Expr := do
-  let IHs := IHs ++ (← collectIHs fn oldIH newIH e)
+def buildInductionCase (is_wf : Bool) (fn : Expr) (oldIH newIH : FVarId) (toClear toPreserve : Array FVarId)
+    (goal : Expr) (IHs : Array Expr) (e : Expr) : M Expr := do
+  let IHs := IHs ++ (← collectIHs is_wf fn oldIH newIH e)
   let IHs ← deduplicateIHs IHs
 
   let mvar ← mkFreshExprSyntheticOpaqueMVar goal (tag := `hyp)
@@ -399,6 +499,7 @@ def buildInductionCase (fn : Expr) (oldIH newIH : FVarId) (toClear toPreserve :
   for fvarId in toClear do
     mvarId ← mvarId.clear fvarId
   mvarId ← mvarId.cleanup (toPreserve := toPreserve)
+  modify (·.push mvarId)
   let mvar ← instantiateMVars mvar
   pure mvar
 
@@ -437,29 +538,50 @@ def maskArray {α} (mask : Array Bool) (xs : Array α) : Array α := Id.run do
     if b then ys := ys.push x
   return ys
 
-partial def buildInductionBody (fn : Expr) (toClear toPreserve : Array FVarId)
-    (goal : Expr) (oldIH newIH : FVarId) (IHs : Array Expr) (e : Expr) : MetaM Expr := do
+/--
+Builds an expression of type `goal` by replicating the expression `e` into its tail-call-positions,
+where it calls `buildInductionCase`. Collects the cases of the final induction hypothesis
+as `MVars` as it goes.
+-/
+partial def buildInductionBody (is_wf : Bool) (fn : Expr) (toClear toPreserve : Array FVarId)
+    (goal : Expr) (oldIH newIH : FVarId) (IHs : Array Expr) (e : Expr) : M Expr := do
+  -- logInfo m!"buildInductionBody {e}"
 
-  if e.isDIte then
-    let #[_α, c, h, t, f] := e.getAppArgs | unreachable!
-    let IHs := IHs ++ (← collectIHs fn oldIH newIH c)
-    let c' ← foldCalls fn oldIH c
-    let h' ← foldCalls fn oldIH h
+  -- if-then-else cause case split:
+  match_expr e with
+  | ite _α c h t f =>
+    let IHs := IHs ++ (← collectIHs is_wf fn oldIH newIH c)
+    let c' ← foldCalls is_wf fn oldIH newIH c
+    let h' ← foldCalls is_wf fn oldIH newIH h
     let t' ← withLocalDecl `h .default c' fun h => do
-      let t ← instantiateLambda t #[h]
-      let t' ← buildInductionBody fn toClear (toPreserve.push h.fvarId!) goal oldIH newIH IHs t
+      let t' ← buildInductionBody is_wf fn toClear (toPreserve.push h.fvarId!) goal oldIH newIH IHs t
       mkLambdaFVars #[h] t'
     let f' ← withLocalDecl `h .default (mkNot c') fun h => do
-      let f ← instantiateLambda f #[h]
-      let f' ← buildInductionBody fn toClear (toPreserve.push h.fvarId!) goal oldIH newIH IHs f
+      let f' ← buildInductionBody is_wf fn toClear (toPreserve.push h.fvarId!) goal oldIH newIH IHs f
       mkLambdaFVars #[h] f'
     let u ← getLevel goal
     return mkApp5 (mkConst ``dite [u]) goal c' h' t' f'
+  | dite _α c h t f =>
+    let IHs := IHs ++ (← collectIHs is_wf fn oldIH newIH c)
+    let c' ← foldCalls is_wf fn oldIH newIH c
+    let h' ← foldCalls is_wf fn oldIH newIH h
+    let t' ← withLocalDecl `h .default c' fun h => do
+      let t ← instantiateLambda t #[h]
+      let t' ← buildInductionBody is_wf fn toClear (toPreserve.push h.fvarId!) goal oldIH newIH IHs t
+      mkLambdaFVars #[h] t'
+    let f' ← withLocalDecl `h .default (mkNot c') fun h => do
+      let f ← instantiateLambda f #[h]
+      let f' ← buildInductionBody is_wf fn toClear (toPreserve.push h.fvarId!) goal oldIH newIH IHs f
+      mkLambdaFVars #[h] f'
+    let u ← getLevel goal
+    return mkApp5 (mkConst ``dite [u]) goal c' h' t' f'
+  | _ =>
 
+  -- match and casesOn application cause case splitting
   if let some matcherApp ← matchMatcherApp? e (alsoCasesOn := true) then
     -- Collect IHs from the parameters and discrs of the matcher
     let paramsAndDiscrs := matcherApp.params ++ matcherApp.discrs
-    let IHs := IHs ++ (← paramsAndDiscrs.concatMapM (collectIHs fn oldIH newIH))
+    let IHs := IHs ++ (← paramsAndDiscrs.concatMapM (collectIHs is_wf fn oldIH newIH ·))
 
     -- Calculate motive
     let eType ← newIH.getType
@@ -471,13 +593,13 @@ partial def buildInductionBody (fn : Expr) (toClear toPreserve : Array FVarId)
     if matcherApp.remaining.size == 1 && matcherApp.remaining[0]!.isFVarOf oldIH then
       let matcherApp' ← matcherApp.transform (useSplitter := true)
         (addEqualities := mask.map not)
-        (onParams := foldCalls fn oldIH)
+        (onParams := (foldCalls is_wf fn oldIH newIH ·))
         (onMotive := fun xs _body => pure (absMotiveBody.beta (maskArray mask xs)))
         (onAlt := fun expAltType alt => do
           removeLamda alt fun oldIH' alt => do
             forallBoundedTelescope expAltType (some 1) fun newIH' goal' => do
               let #[newIH'] := newIH' | unreachable!
-              let alt' ← buildInductionBody fn (toClear.push newIH'.fvarId!) toPreserve goal' oldIH' newIH'.fvarId! IHs alt
+              let alt' ← buildInductionBody is_wf fn (toClear.push newIH'.fvarId!) toPreserve goal' oldIH' newIH'.fvarId! IHs alt
               mkLambdaFVars #[newIH'] alt')
         (onRemaining := fun _ => pure #[.fvar newIH])
       return matcherApp'.toExpr
@@ -490,41 +612,139 @@ partial def buildInductionBody (fn : Expr) (toClear toPreserve : Array FVarId)
 
       let matcherApp' ← matcherApp.transform (useSplitter := true)
         (addEqualities := mask.map not)
-        (onParams := foldCalls fn oldIH)
+        (onParams := (foldCalls is_wf fn oldIH newIH ·))
         (onMotive := fun xs _body => pure (absMotiveBody.beta (maskArray mask xs)))
         (onAlt := fun expAltType alt => do
-          buildInductionBody fn toClear toPreserve expAltType oldIH newIH IHs alt)
+          buildInductionBody is_wf fn toClear toPreserve expAltType oldIH newIH IHs alt)
       return matcherApp'.toExpr
 
   if let .letE n t v b _ := e then
-    let IHs := IHs ++ (← collectIHs fn oldIH newIH v)
-    let t' ← foldCalls fn oldIH t
-    let v' ← foldCalls fn oldIH v
+    let IHs := IHs ++ (← collectIHs is_wf fn oldIH newIH v)
+    let t' ← foldCalls is_wf fn oldIH newIH t
+    let v' ← foldCalls is_wf fn oldIH newIH v
     return ← withLetDecl n t' v' fun x => do
-      let b' ← buildInductionBody fn toClear toPreserve goal oldIH newIH IHs (b.instantiate1 x)
+      let b' ← buildInductionBody is_wf fn toClear toPreserve goal oldIH newIH IHs (b.instantiate1 x)
       mkLetFVars #[x] b'
 
   if let some (n, t, v, b) := e.letFun? then
-    let IHs := IHs ++ (← collectIHs fn oldIH newIH v)
-    let t' ← foldCalls fn oldIH t
-    let v' ← foldCalls fn oldIH v
+    let IHs := IHs ++ (← collectIHs is_wf fn oldIH newIH v)
+    let t' ← foldCalls is_wf fn oldIH newIH t
+    let v' ← foldCalls is_wf fn oldIH newIH v
     return ← withLocalDecl n .default t' fun x => do
-      let b' ← buildInductionBody fn toClear toPreserve goal oldIH newIH IHs (b.instantiate1 x)
+      let b' ← buildInductionBody is_wf fn toClear toPreserve goal oldIH newIH IHs (b.instantiate1 x)
       mkLetFun x v' b'
 
-  buildInductionCase fn oldIH newIH toClear toPreserve goal IHs e
+  liftM <| buildInductionCase is_wf fn oldIH newIH toClear toPreserve goal IHs e
+
+/--
+Given an expression `e` with metavariables
+* collects all these meta-variables,
+* lifts them to the current context by reverting all local declarations up to `x`
+* introducing a local variable for each of the meta variable
+* assigning that local variable to the mvar
+* and finally lambda-abstracting over these new local variables.
+
+This operation only works if the metavariables are independent from each other.
+
+The resulting meta variable assignment is no longer valid (mentions out-of-scope
+variables), so after this operations, terms that still mention these meta variables must not
+be used anymore.
+
+We are not using `mkLambdaFVars` on mvars directly, nor `abstractMVars`, as these at the moment
+do not handle delayed assignemnts correctly.
+-/
+def abstractIndependentMVars (mvars : Array MVarId) (x : FVarId) (e : Expr) : MetaM Expr := do
+  let mvars ← mvars.mapM fun mvar => do
+    let mvar ← substVarAfter mvar x
+    let (_, mvar) ← mvar.revertAfter x
+    pure mvar
+  let decls := mvars.mapIdx fun i mvar =>
+    (.mkSimple s!"case{i.val+1}", .default, (fun _ => mvar.getType))
+  Meta.withLocalDecls decls fun xs => do
+      for mvar in mvars, x in xs do
+        mvar.assign x
+      mkLambdaFVars xs (← instantiateMVars e)
+
+/--
+This function looks that the body of a recursive function and looks for either users of
+`fix`, `fixF` or a `.brecOn`, and abstracts over the differences between them. It passes
+to the continuation
+
+* whether we are using well-founded recursion
+* the fixed parameters of the function body
+* the varying parameters of the function body (this includes both the targets of the
+  recursion and extra parameters passed to the recursor)
+* the position of the motive/induction hypothesis in the body's arguments
+* the body, as passed to the recursor. Expected to be a lambda that takes the
+  varying paramters and the motive
+* a function to re-assemble the call with a new Motive. The resulting expression expects
+  the new body next, so that the expected type of the body can be inferred
+* a function to finish assembling the call with the new body.
+-/
+def findRecursor {α} (name : Name) (varNames : Array Name) (e : Expr)
+    (k :(is_wf : Bool) →
+        (fixedParams : Array Expr) →
+        (varyingParams : Array Expr) →
+        (motivePosInBody : Nat) →
+        (body : Expr) →
+        (mkAppMotive : Expr → MetaM Expr) →
+        (mkAppBody : Expr → Expr → Expr) →
+        MetaM α) :
+    MetaM α := do
+  -- Uses of WellFounded.fix can be partially applied. Here we eta-expand the body
+  -- to avoid dealing with this
+  let e ← lambdaTelescope e fun params body => do mkLambdaFVars params (← etaExpand body)
+  lambdaTelescope e fun params body => body.withApp fun f args => do
+    MatcherApp.withUserNames params varNames do
+      if not f.isConst then err else
+      if isBRecOnRecursor (← getEnv) f.constName! then
+        let elimInfo ← getElimExprInfo f
+        let targets : Array Expr := elimInfo.targetsPos.map (args[·]!)
+        let body := args[elimInfo.motivePos + 1 + elimInfo.targetsPos.size]!
+        let extraArgs : Array Expr := args[elimInfo.motivePos + 1 + elimInfo.targetsPos.size + 1:]
+
+        let fixedParams := params.filter fun x => !(targets.contains x || extraArgs.contains x)
+        let varyingParams := params.filter fun x => targets.contains x || extraArgs.contains x
+        unless params == fixedParams ++ varyingParams do
+          throwError "functional induction: unexpected order of fixed and varying parameters:{indentExpr e}"
+        -- we assume the motive's universe parameter is the first
+        unless 1 ≤ f.constLevels!.length do
+          throwError "functional induction: unexpected recursor: {f} has no universe parameters"
+        let us := f.constLevels!.set 0 levelZero
+
+        let value := mkAppN (.const f.constName us) (args[:elimInfo.motivePos])
+        k false fixedParams varyingParams targets.size body
+          (fun newMotive => do
+            -- We may have to reorder the parameters for motive before passing it to brec
+            let brecMotive ← mkLambdaFVars targets
+              (← mkForallFVars extraArgs (mkAppN newMotive varyingParams))
+            return mkAppN (mkApp value brecMotive) targets)
+          (fun value newBody => mkAppN (.app value newBody) extraArgs)
+      else if Name.isSuffixOf `brecOn f.constName! then
+        throwError m!"Function {name} is defined in a way not supported by functional induction, " ++
+          "for example by recursion over an inductive predicate."
+      else match_expr body with
+      | WellFounded.fixF α rel _motive body target acc =>
+        unless params.back == target do
+          throwError "functional induction: expected the target as last parameter{indentExpr e}"
+        let value := .const ``WellFounded.fixF [f.constLevels![0]!, levelZero]
+        k true params.pop #[params.back] 1 body
+          (fun newMotive => pure (mkApp3 value α rel newMotive))
+          (fun value newBody => mkApp2 value newBody acc)
+      | WellFounded.fix α _motive rel wf body target =>
+        unless params.back == target do
+          throwError "functional induction: expected the target as last parameter{indentExpr e}"
+        let value := .const ``WellFounded.fix [f.constLevels![0]!, levelZero]
+        k true params.pop #[target] 1 body
+          (fun newMotive => pure (mkApp4 value α newMotive rel wf))
+          (fun value newBody => mkApp2 value newBody target)
+      | _ => err
+  where
+    err := throwError m!"Function {name} does not look like a function defined by recursion." ++
+      m!"\nNB: If {name} is not itself recursive, but contains an inner recursive " ++
+      m!"function (via `let rec` or `where`), try `{name}.go` where `go` is name of the inner " ++
+      "function."
 
-partial def findFixF {α} (name : Name) (e : Expr) (k : Array Expr → Expr → MetaM α) : MetaM α := do
-  lambdaTelescope e fun params body => do
-    if body.isAppOf ``WellFounded.fixF then
-      k params body
-    else if body.isAppOf ``WellFounded.fix then
-      findFixF name (← unfoldDefinition body) fun args e' => k (params ++ args) e'
-    else
-      throwError m!"Function {name} does not look like a function defined by well-founded " ++
-        m!"recursion.\nNB: If {name} is not itself recursive, but contains an inner recursive " ++
-        m!"function (via `let rec` or `where`), try `{name}.go` where `go` is name of the inner " ++
-        "function."
 
 /--
 Given a definition `foo` defined via `WellFounded.fixF`, derive a suitable induction principle
@@ -535,77 +755,60 @@ def deriveUnaryInduction (name : Name) : MetaM Name := do
   if ← hasConst inductName then return inductName
 
   let info ← getConstInfoDefn name
-  findFixF name info.value fun params body => body.withApp fun f fixArgs => do
-    -- logInfo f!"{fixArgs}"
-    unless params.size > 0 do
-      throwError "Value of {name} is not a lambda application"
-    unless f.isConstOf ``WellFounded.fixF do
-      throwError "Term isn’t application of {``WellFounded.fixF}, but of {f}"
-    let #[argType, rel, _motive, body, arg, acc] := fixArgs |
-      throwError "Application of WellFounded.fixF has wrong arity {fixArgs.size}"
-    unless ← isDefEq arg params.back do
-      throwError "fixF application argument {arg} is not function argument "
-    let [argLevel, _motiveLevel] := f.constLevels! | unreachable!
 
-    let motiveType ← mkArrow argType (.sort levelZero)
-    withLocalDecl `motive .default motiveType fun motive => do
+  let varNames ← forallTelescope info.type fun xs _ => xs.mapM (·.fvarId!.getUserName)
 
-    let e' := mkApp3 (.const ``WellFounded.fixF [argLevel, levelZero]) argType rel motive
-    let fn := mkAppN (.const name (info.levelParams.map mkLevelParam)) params.pop
-    let body' ← forallTelescope (← inferType e').bindingDomain! fun xs _ => do
-      let #[param, genIH] := xs | unreachable!
-      -- open body with the same arg
-      let body ← instantiateLambda body #[param]
-      removeLamda body fun oldIH body => do
-        let body' ← buildInductionBody fn #[genIH.fvarId!] #[] (.app motive param) oldIH genIH.fvarId! #[] body
-        if body'.containsFVar oldIH then
-          throwError m!"Did not fully eliminate {mkFVar oldIH} from induction principle body:{indentExpr body}"
-        mkLambdaFVars #[param, genIH] body'
-
-    let e' := mkApp3 e' body' arg acc
-
-    let e' ← mkLambdaFVars #[params.back] e'
-    let mvars ← getMVarsNoDelayed e'
-    let mvars ← mvars.mapM fun mvar => do
-      let mvar ← substVarAfter mvar motive.fvarId!
-      let (_, mvar) ← mvar.revertAfter motive.fvarId!
-      pure mvar
-    -- Using `mkLambdaFVars` on mvars directly does not reliably replace
-    -- the mvars with the parameter, in the presence of delayed assignemnts.
-    -- Also `abstractMVars` does not handle delayed assignments correctly (as of now).
-    -- So instead we bring suitable fvars into scope and use `assign`; this handles
-    -- delayed assignemnts correctly.
-    -- NB: This idiom only works because
-    -- * we know that the `MVars` have the right local context (thanks to `mvarId.revertAfter`)
-    -- * the MVars are independent (so we don’t need to reorder them)
-    -- * we do no need the mvars in their unassigned form later
-    let e' ← Meta.withLocalDecls
-      (mvars.mapIdx (fun i mvar => (s!"case{i.val+1}", .default, (fun _ => mvar.getType))))
-      fun xs => do
-        for mvar in mvars, x in xs do
-          mvar.assign x
-        let e' ← instantiateMVars e'
-        mkLambdaFVars xs e'
-
-    -- We could pass (usedOnly := true) below, and get nicer induction principles that
-    -- do do not mention odd unused parameters.
-    -- But the downside is that automatic instantiation of the principle (e.g. in a tactic
-    -- that derives them from an function application in the goal) is harder, as
-    -- one would have to infer or keep track of which parameters to pass.
-    -- So for now lets just keep them around.
-    let e' ← mkLambdaFVars (binderInfoForMVars := .default) (params.pop ++ #[motive]) e'
-    let e' ← instantiateMVars e'
-
-    let eTyp ← inferType e'
-    let eTyp ← elimOptParam eTyp
-    -- logInfo m!"eTyp: {eTyp}"
-    unless (← isTypeCorrect e') do
-      logError m!"failed to derive induction priciple:{indentExpr e'}"
+  let e' ← findRecursor name varNames info.value
+    fun is_wf fixedParams varyingParams motivePosInBody body mkAppMotive mkAppBody => do
+      let motiveType ← mkForallFVars varyingParams (.sort levelZero)
+      withLocalDecl `motive .default motiveType fun motive => do
+      let fn := mkAppN (.const name (info.levelParams.map mkLevelParam)) fixedParams
+      let e' ← mkAppMotive motive
       check e'
+      let (body', mvars) ← StateT.run (s := {}) do
+        forallTelescope (← inferType e').bindingDomain! fun xs goal => do
+          let arity := varyingParams.size + 1
+          if xs.size ≠ arity then
+            throwError "expected recursor argument to take {arity} parameters, got {xs}" else
+          let targets : Array Expr := xs[:motivePosInBody]
+          let genIH := xs[motivePosInBody]!
+          let extraParams := xs[motivePosInBody+1:]
+          -- open body with the same arg
+          let body ← instantiateLambda body targets
+          removeLamda body fun oldIH body => do
+            let body ← instantiateLambda body extraParams
+            let body' ← buildInductionBody is_wf fn #[genIH.fvarId!] #[] goal oldIH genIH.fvarId! #[] body
+            if body'.containsFVar oldIH then
+              throwError m!"Did not fully eliminate {mkFVar oldIH} from induction principle body:{indentExpr body}"
+            mkLambdaFVars (targets.push genIH) (← mkLambdaFVars extraParams body')
+      let e' := mkAppBody e' body'
+      let e' ← mkLambdaFVars varyingParams e'
+      let e' ← abstractIndependentMVars mvars motive.fvarId! e'
+      let e' ← mkLambdaFVars #[motive] e'
 
-    addDecl <| Declaration.thmDecl
-      { name := inductName, levelParams := info.levelParams, type := eTyp, value := e' }
-    return inductName
+      -- We could pass (usedOnly := true) below, and get nicer induction principles that
+      -- do do not mention odd unused parameters.
+      -- But the downside is that automatic instantiation of the principle (e.g. in a tactic
+      -- that derives them from an function application in the goal) is harder, as
+      -- one would have to infer or keep track of which parameters to pass.
+      -- So for now lets just keep them around.
+      let e' ← mkLambdaFVars (binderInfoForMVars := .default) fixedParams e'
+      instantiateMVars e'
+
+  unless (← isTypeCorrect e') do
+    logError m!"failed to derive induction priciple:{indentExpr e'}"
+    check e'
+
+  let eTyp ← inferType e'
+  let eTyp ← elimOptParam eTyp
+  -- logInfo m!"eTyp: {eTyp}"
+  let params := (collectLevelParams {} eTyp).params
+  -- Prune unused level parameters, preserving the original order
+  let us := info.levelParams.filter (params.contains ·)
+
+  addDecl <| Declaration.thmDecl
+    { name := inductName, levelParams := us, type := eTyp, value := e' }
+  return inductName
 
 /--
 In the type of `value`, reduces
@@ -738,10 +941,21 @@ def deriveInduction (name : Name) : MetaM Unit := do
   else
     _ ← deriveUnaryInduction name
 
-@[builtin_command_elab Parser.Command.deriveInduction]
-def elabDeriveInduction : Command.CommandElab := fun stx => Command.runTermElabM fun _xs => do
-  let ident := stx[1]
-  let name ← realizeGlobalConstNoOverloadWithInfo ident
-  deriveInduction name
+def isFunInductName (env : Environment) (name : Name) : Bool := Id.run do
+  let .str p s := name | return false
+  unless s = "induct" do return false
+  if (WF.eqnInfoExt.find? env p).isSome then return true
+  if (Structural.eqnInfoExt.find? env p).isSome then return true
+  return false
+
+builtin_initialize
+  registerReservedNamePredicate isFunInductName
+
+  registerReservedNameAction fun name => do
+    if isFunInductName (← getEnv) name then
+      let .str p _ := name | return false
+      MetaM.run' <| deriveInduction p
+      return true
+    return false
 
 end Lean.Tactic.FunInd

src/Lean/Meta/Tactic/LibrarySearch.lean

@@ -67,7 +67,7 @@ to find candidate lemmas.
 @[reducible]
 def CandidateFinder := Expr → MetaM (Array (Name × DeclMod))
 
-open LazyDiscrTree (InitEntry findCandidates)
+open LazyDiscrTree (InitEntry findMatches)
 
 private def addImport (name : Name) (constInfo : ConstantInfo) :
     MetaM (Array (InitEntry (Name × DeclMod))) :=
@@ -111,7 +111,7 @@ private def constantsPerImportTask : Nat := 6500
 
 /-- Create function for finding relevant declarations. -/
 def libSearchFindDecls : Expr → MetaM (Array (Name × DeclMod)) :=
-  findCandidates ext addImport
+  findMatches ext addImport
       (droppedKeys := droppedKeys)
       (constantsPerTask := constantsPerImportTask)
 
@@ -278,15 +278,15 @@ private def librarySearch' (goal : MVarId)
     MetaM (Option (Array (List MVarId × MetavarContext))) := do
   withTraceNode `Tactic.librarySearch (return m!"{librarySearchEmoji ·} {← goal.getType}") do
   profileitM Exception "librarySearch" (← getOptions) do
-  -- Create predicate that returns true when running low on heartbeats.
-  let candidates ← librarySearchSymm libSearchFindDecls goal
-  let cfg : ApplyConfig := { allowSynthFailures := true }
-  let shouldAbort ← mkHeartbeatCheck leavePercentHeartbeats
-  let act := fun cand => do
-      if ←shouldAbort then
-        abortSpeculation
-      librarySearchLemma cfg tactic allowFailure cand
-  tryOnEach act candidates
+    -- Create predicate that returns true when running low on heartbeats.
+    let candidates ← librarySearchSymm libSearchFindDecls goal
+    let cfg : ApplyConfig := { allowSynthFailures := true }
+    let shouldAbort ← mkHeartbeatCheck leavePercentHeartbeats
+    let act := fun cand => do
+        if ←shouldAbort then
+          abortSpeculation
+        librarySearchLemma cfg tactic allowFailure cand
+    tryOnEach act candidates
 
 /--
 Tries to solve the goal either by:

src/Lean/Meta/Tactic/Replace.lean

@@ -141,16 +141,36 @@ def _root_.Lean.MVarId.change (mvarId : MVarId) (targetNew : Expr) (checkDefEq :
 def change (mvarId : MVarId) (targetNew : Expr) (checkDefEq := true) : MetaM MVarId := mvarId.withContext do
   mvarId.change targetNew checkDefEq
 
-/-- Runs the continuation `k` after temporarily reverting some variables from the local context of a metavariable (identified by `mvarId`), then reintroduces local variables as specified by `k`.
+/--
+Executes the revert/intro pattern, running the continuation `k` after temporarily reverting
+the given local variables from the local context of the metavariable `mvarId`,
+and then re-introducing the local variables specified by `k`.
 
-The argument `fvarIds` is an array of `fvarIds` to revert in the order specified. An error is thrown if they cannot be reverted in order.
+- `mvarId` is the goal metavariable to operate on.
+- `fvarIds` is an array of `fvarIds` to revert in the order specified.
+  An error is thrown if they cannot be reverted in order.
+- `clearAuxDeclsInsteadOfRevert` is configuration passed to `Lean.MVarId.revert`.
+- `k` is the continuation run once the local variables have been reverted.
+  It is provided `mvarId` after the requested variables have been reverted along with the array of reverted variables.
+  This array always contains `fvarIds`, but it may contain additional variables that were reverted due to dependencies.
+  The continuation returns a value, a new goal, and an _aliasing array_.
 
-Once the local variables have been reverted, `k` is passed `mvarId` along with an array of local variables that were reverted. This array always has `fvarIds` as a prefix, but it may contain additional variables that were reverted due to dependencies. `k` returns a value, a goal, an array of _link variables_.
+Once `k` has completed, one variable is introduced per entry in the aliasing array.
+* If the entry is `none`, the variable is just introduced.
+* If the entry is `some fv` (where `fv` is a variable from `fvarIds`),
+  the variable is introduced and then recorded as an alias of `fv` in the info tree.
+  This for example causes the unused variable linter as seeing `fv` and this newly introduced variable as being "the same".
 
-Once `k` has completed, one variable is introduced for each link variable returned by `k`. If the returned variable is `none`, the variable is just introduced. If it is `some fv`, the variable is introduced and then linked as an alias of `fv` in the info tree. For example, having `k` return `fvars.map .some` as the link variables causes all reverted variables to be introduced and linked.
+For example, if `k` leaves all the reverted variables in the same order,
+having it return `fvars.map .some` as the aliasing array causes those variables to be re-introduced and aliased
+to the original local variables.
 
-Returns the value returned by `k` along with the resulting goal.
- -/
+Returns the value returned by `k` along with the resulting goal after variable introduction.
+
+See `Lean.MVarId.changeLocalDecl` for an example. The motivation is that to work on a local variable,
+you need to move it into the goal, alter the goal, and then bring it back into the local context,
+all while keeping track of any other local variables that depend on this one.
+-/
 def _root_.Lean.MVarId.withReverted (mvarId : MVarId) (fvarIds : Array FVarId)
     (k : MVarId → Array FVarId → MetaM (α × Array (Option FVarId) × MVarId))
     (clearAuxDeclsInsteadOfRevert := false) : MetaM (α × MVarId) := do

src/Lean/Meta/Tactic/Rewrites.lean

@@ -0,0 +1,341 @@
+/-
+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.Meta.LazyDiscrTree
+import Lean.Meta.Tactic.Assumption
+import Lean.Meta.Tactic.Rewrite
+import Lean.Meta.Tactic.Refl
+import Lean.Meta.Tactic.SolveByElim
+import Lean.Meta.Tactic.TryThis
+import Lean.Util.Heartbeats
+
+namespace Lean.Meta.Rewrites
+
+open Lean.Meta.LazyDiscrTree (InitEntry MatchResult)
+open Lean.Meta.SolveByElim
+
+builtin_initialize registerTraceClass `Tactic.rewrites
+builtin_initialize registerTraceClass `Tactic.rewrites.lemmas
+
+/-- Extract the lemma, with arguments, that was used to produce a `RewriteResult`. -/
+-- This assumes that `r.eqProof` was constructed as:
+-- `mkApp6 (.const ``congrArg _) α eType lhs rhs motive heq`
+-- in `Lean.Meta.Tactic.Rewrite` and we want `heq`.
+def rewriteResultLemma (r : RewriteResult) : Option Expr :=
+  if r.eqProof.isAppOfArity ``congrArg 6 then
+    r.eqProof.getArg! 5
+  else
+    none
+
+/-- Weight to multiply the "specificity" of a rewrite lemma by when rewriting forwards. -/
+def forwardWeight := 2
+/-- Weight to multiply the "specificity" of a rewrite lemma by when rewriting backwards. -/
+def backwardWeight := 1
+
+inductive RwDirection : Type where
+  | forward : RwDirection
+  | backward : RwDirection
+
+private def addImport (name : Name) (constInfo : ConstantInfo) :
+    MetaM (Array (InitEntry (Name × RwDirection))) := do
+  if constInfo.isUnsafe then return #[]
+  if !allowCompletion (←getEnv) name then return #[]
+  -- We now remove some injectivity lemmas which are not useful to rewrite by.
+  if name matches .str _ "injEq" then return #[]
+  if name matches .str _ "sizeOf_spec" then return #[]
+  match name with
+  | .str _ n => if n.endsWith "_inj" ∨ n.endsWith "_inj'" then return #[]
+  | _ => pure ()
+  withNewMCtxDepth do withReducible do
+    forallTelescopeReducing constInfo.type fun _ type => do
+      match type.getAppFnArgs with
+      | (``Eq, #[_, lhs, rhs])
+      | (``Iff, #[lhs, rhs]) => do
+        let a := Array.mkEmpty 2
+        let a := a.push (← InitEntry.fromExpr lhs (name, RwDirection.forward))
+        let a := a.push (← InitEntry.fromExpr rhs (name, RwDirection.backward))
+        pure a
+      | _ => return #[]
+
+/-- Configuration for `DiscrTree`. -/
+def discrTreeConfig : WhnfCoreConfig := {}
+
+/-- Select `=` and `↔` local hypotheses. -/
+def localHypotheses (except : List FVarId := []) : MetaM (Array (Expr × Bool × Nat)) := do
+  let r ← getLocalHyps
+  let mut result := #[]
+  for h in r do
+    if except.contains h.fvarId! then continue
+    let (_, _, type) ← forallMetaTelescopeReducing (← inferType h)
+    let type ← whnfR type
+    match type.getAppFnArgs with
+    | (``Eq, #[_, _, _])
+    | (``Iff, #[_, _]) => do
+      result := result.push (h, false, forwardWeight)
+                    |>.push (h, true, backwardWeight)
+    | _ => pure ()
+  return result
+
+/--
+We drop `.star` and `Eq * * *` from the discriminator trees because
+they match too much.
+-/
+def droppedKeys : List (List LazyDiscrTree.Key) := [[.star], [.const `Eq 3, .star, .star, .star]]
+
+def createModuleTreeRef : MetaM (LazyDiscrTree.ModuleDiscrTreeRef (Name × RwDirection)) :=
+  LazyDiscrTree.createModuleTreeRef addImport droppedKeys
+
+private def ExtState := IO.Ref (Option (LazyDiscrTree (Name × RwDirection)))
+
+private builtin_initialize ExtState.default : IO.Ref (Option (LazyDiscrTree (Name × RwDirection))) ← do
+  IO.mkRef .none
+
+private instance : Inhabited ExtState where
+  default := ExtState.default
+
+private builtin_initialize ext : EnvExtension ExtState ←
+  registerEnvExtension (IO.mkRef .none)
+
+/--
+The maximum number of constants an individual task may perform.
+
+The value was picked because it roughly correponded to 50ms of work on the
+machine this was developed on.  Smaller numbers did not seem to improve
+performance when importing Std and larger numbers (<10k) seemed to degrade
+initialization performance.
+-/
+private def constantsPerImportTask : Nat := 6500
+
+def incPrio : Nat → Name × RwDirection → Name × Bool × Nat
+| q, (nm, d) =>
+  match d with
+  | .forward => (nm, false, 2 * q)
+  | .backward => (nm, true, q)
+
+/-- Create function for finding relevant declarations. -/
+def rwFindDecls (moduleRef : LazyDiscrTree.ModuleDiscrTreeRef (Name × RwDirection)) : Expr → MetaM (Array (Name × Bool × Nat)) :=
+  LazyDiscrTree.findMatchesExt moduleRef ext addImport
+      (droppedKeys := droppedKeys)
+      (constantsPerTask := constantsPerImportTask)
+      (adjustResult := incPrio)
+
+/-- Data structure recording a potential rewrite to report from the `rw?` tactic. -/
+structure RewriteResult where
+  /-- The lemma we rewrote by.
+  This is `Expr`, not just a `Name`, as it may be a local hypothesis. -/
+  expr : Expr
+  /-- `True` if we rewrote backwards (i.e. with `rw [← h]`). -/
+  symm : Bool
+  /-- The "weight" of the rewrite. This is calculated based on how specific the rewrite rule was. -/
+  weight : Nat
+  /-- The result from the `rw` tactic. -/
+  result : Meta.RewriteResult
+  /-- The metavariable context after the rewrite.
+  This needs to be stored as part of the result so we can backtrack the state. -/
+  mctx : MetavarContext
+  rfl? : Bool
+
+/-- Check to see if this expression (which must be a type) can be closed by `with_reducible rfl`. -/
+def dischargableWithRfl? (mctx : MetavarContext) (e : Expr) : MetaM Bool := do
+  try
+    withoutModifyingState <| withMCtx mctx do
+      -- We use `withReducible` here to follow the behaviour of `rw`.
+      withReducible (← mkFreshExprMVar e).mvarId!.refl
+      pure true
+  catch _e =>
+    pure false
+
+/--
+Pretty print the result of the rewrite.
+-/
+private def RewriteResult.ppResult (r : RewriteResult) : MetaM String :=
+  return (← ppExpr r.result.eNew).pretty
+
+
+/-- Should we try discharging side conditions? If so, using `assumption`, or `solve_by_elim`? -/
+inductive SideConditions
+| none
+| assumption
+| solveByElim
+
+/-- Shortcut for calling `solveByElim`. -/
+def solveByElim (goals : List MVarId) (depth : Nat := 6) : MetaM PUnit := do
+  -- There is only a marginal decrease in performance for using the `symm` option for `solveByElim`.
+  -- (measured via `lake build && time lake env lean test/librarySearch.lean`).
+  let cfg : SolveByElimConfig := { maxDepth := depth, exfalso := false, symm := true }
+  let ⟨lemmas, ctx⟩ ← mkAssumptionSet false false [] [] #[]
+  let [] ← SolveByElim.solveByElim cfg lemmas ctx goals
+    | failure
+
+def rwLemma (ctx : MetavarContext) (goal : MVarId) (target : Expr) (side : SideConditions := .solveByElim)
+    (lem : Expr ⊕ Name) (symm : Bool) (weight : Nat) : MetaM (Option RewriteResult) :=
+  withMCtx ctx do
+    let some expr ← (match lem with
+    | .inl hyp => pure (some hyp)
+    | .inr lem => some <$> mkConstWithFreshMVarLevels lem <|> pure none)
+      | return none
+    trace[Tactic.rewrites] m!"considering {if symm then "← " else ""}{expr}"
+    let some result ← some <$> goal.rewrite target expr symm <|> pure none
+      | return none
+    if result.mvarIds.isEmpty then
+      let mctx ← getMCtx
+      let rfl? ← dischargableWithRfl? mctx result.eNew
+      return some { expr, symm, weight, result, mctx, rfl? }
+    else
+      -- There are side conditions, which we try to discharge using local hypotheses.
+      let discharge ←
+        match side with
+        | .none => pure false
+        | .assumption => ((fun _ => true) <$> result.mvarIds.mapM fun m => m.assumption) <|> pure false
+        | .solveByElim => (solveByElim result.mvarIds >>= fun _ => pure true) <|> pure false
+      match discharge with
+      | false =>
+        return none
+      | true =>
+        -- If we succeed, we need to reconstruct the expression to report that we rewrote by.
+        let some expr := rewriteResultLemma result | return none
+        let expr ← instantiateMVars expr
+        let (expr, symm) := if expr.isAppOfArity ``Eq.symm 4 then
+            (expr.getArg! 3, true)
+          else
+            (expr, false)
+        let mctx ← getMCtx
+        let rfl? ← dischargableWithRfl? mctx result.eNew
+        return some { expr, symm, weight, result, mctx, rfl? }
+
+/--
+Find keys which match the expression, or some subexpression.
+
+Note that repeated subexpressions will be visited each time they appear,
+making this operation potentially very expensive.
+It would be good to solve this problem!
+
+Implementation: we reverse the results from `getMatch`,
+so that we return lemmas matching larger subexpressions first,
+and amongst those we return more specific lemmas first.
+-/
+partial def getSubexpressionMatches (op : Expr → MetaM (Array α)) (e : Expr) : MetaM (Array α) := do
+  match e with
+  | .bvar _ => return #[]
+  | .forallE _ _ _ _ =>
+    forallTelescope e fun args body => do
+      args.foldlM (fun acc arg => return acc ++ (← getSubexpressionMatches op (← inferType arg)))
+        (← getSubexpressionMatches op body).reverse
+  | .lam _ _ _ _
+  | .letE _ _ _ _ _ =>
+    lambdaLetTelescope e (fun args body => do
+      args.foldlM (fun acc arg => return acc ++ (← getSubexpressionMatches op (← inferType arg)))
+        (← getSubexpressionMatches op body).reverse)
+  | _ =>
+    let init := ((← op e).reverse)
+    e.foldlM (init := init) (fun a f => return a ++ (← getSubexpressionMatches op f))
+
+/--
+Find lemmas which can rewrite the goal.
+
+See also `rewrites` for a more convenient interface.
+-/
+def rewriteCandidates (hyps : Array (Expr × Bool × Nat))
+    (moduleRef : LazyDiscrTree.ModuleDiscrTreeRef (Name × RwDirection))
+    (target : Expr)
+    (forbidden : NameSet := ∅) :
+    MetaM (Array ((Expr ⊕ Name) × Bool × Nat)) := do
+  -- Get all lemmas which could match some subexpression
+  let candidates ← getSubexpressionMatches (rwFindDecls moduleRef) target
+  -- Sort them by our preferring weighting
+  -- (length of discriminant key, doubled for the forward implication)
+  let candidates := candidates.insertionSort fun (_, _, rp) (_, _, sp) => rp > sp
+
+  -- Now deduplicate. We can't use `Array.deduplicateSorted` as we haven't completely sorted,
+  -- and in fact want to keep some of the residual ordering from the discrimination tree.
+  let mut forward : NameSet := ∅
+  let mut backward : NameSet := ∅
+  let mut deduped := #[]
+  for (l, s, w) in candidates do
+    if forbidden.contains l then continue
+    if s then
+      if ¬ backward.contains l then
+        deduped := deduped.push (l, s, w)
+        backward := backward.insert l
+    else
+      if ¬ forward.contains l then
+        deduped := deduped.push (l, s, w)
+        forward := forward.insert l
+
+  trace[Tactic.rewrites.lemmas] m!"Candidate rewrite lemmas:\n{deduped}"
+
+  let hyps := hyps.map fun ⟨hyp, symm, weight⟩ => (Sum.inl hyp, symm, weight)
+  let lemmas := deduped.map fun ⟨lem, symm, weight⟩ => (Sum.inr lem, symm, weight)
+  pure <| hyps ++ lemmas
+
+def RewriteResult.newGoal (r : RewriteResult) : Option Expr :=
+  if r.rfl? = true then
+    some (Expr.lit (.strVal "no goals"))
+  else
+    some r.result.eNew
+
+def RewriteResult.addSuggestion (ref : Syntax) (r : RewriteResult) : Elab.TermElabM Unit := do
+  withMCtx r.mctx do
+    Tactic.TryThis.addRewriteSuggestion ref [(r.expr, r.symm)] (type? := r.newGoal) (origSpan? := ← getRef)
+
+structure RewriteResultConfig where
+  stopAtRfl : Bool
+  max : Nat
+  minHeartbeats : Nat
+  goal : MVarId
+  target : Expr
+  side : SideConditions := .solveByElim
+  mctx : MetavarContext
+
+def takeListAux (cfg : RewriteResultConfig) (seen : HashMap String Unit) (acc : Array RewriteResult)
+    (xs : List ((Expr ⊕ Name) × Bool × Nat)) : MetaM (Array RewriteResult) := do
+  let mut seen := seen
+  let mut acc := acc
+  for (lem, symm, weight) in xs do
+    if (← getRemainingHeartbeats) < cfg.minHeartbeats then
+      return acc
+    if acc.size ≥ cfg.max then
+      return acc
+    let res ←
+          withoutModifyingState <| withMCtx cfg.mctx do
+            rwLemma cfg.mctx cfg.goal cfg.target cfg.side lem symm weight
+    match res with
+    | none => continue
+    | some r =>
+      let s ← withoutModifyingState <| withMCtx r.mctx r.ppResult
+      if seen.contains s then
+        continue
+      let rfl? ← dischargableWithRfl? r.mctx r.result.eNew
+      if cfg.stopAtRfl then
+        if rfl? then
+          return #[r]
+        else
+          seen := seen.insert s ()
+          acc := acc.push r
+      else
+        seen := seen.insert s ()
+        acc := acc.push r
+  return acc
+
+/-- Find lemmas which can rewrite the goal. -/
+def findRewrites (hyps : Array (Expr × Bool × Nat))
+    (moduleRef : LazyDiscrTree.ModuleDiscrTreeRef (Name × RwDirection))
+    (goal : MVarId) (target : Expr)
+    (forbidden : NameSet := ∅) (side : SideConditions := .solveByElim)
+    (stopAtRfl : Bool) (max : Nat := 20)
+    (leavePercentHeartbeats : Nat := 10) : MetaM (List RewriteResult) := do
+  let mctx ← getMCtx
+  let candidates ← rewriteCandidates hyps moduleRef target forbidden
+  let minHeartbeats : Nat :=
+        if (← getMaxHeartbeats) = 0 then
+          0
+        else
+          leavePercentHeartbeats * (← getRemainingHeartbeats) / 100
+  let cfg : RewriteResultConfig :=
+        { stopAtRfl, minHeartbeats, max, mctx, goal, target, side }
+  return (← takeListAux cfg {} (Array.mkEmpty max) candidates.toList).toList
+
+end Lean.Meta.Rewrites

src/Lean/Meta/Tactic/Rfl.lean

@@ -6,6 +6,7 @@ Authors: Newell Jensen, Thomas Murrills
 prelude
 import Lean.Meta.Tactic.Apply
 import Lean.Elab.Tactic.Basic
+import Lean.Meta.Tactic.Refl
 
 /-!
 # `rfl` tactic extension for reflexive relations
@@ -38,6 +39,8 @@ initialize registerBuiltinAttribute {
     let fail := throwError
       "@[refl] attribute only applies to lemmas proving x ∼ x, got {declTy}"
     let .app (.app rel lhs) rhs := targetTy | fail
+    if let .app (.const ``Eq [_]) _ := rel then
+      throwError "@[refl] attribute may not be used on `Eq.refl`."
     unless ← withNewMCtxDepth <| isDefEq lhs rhs do fail
     let key ← DiscrTree.mkPath rel reflExt.config
     reflExt.add (decl, key) kind
@@ -47,29 +50,33 @@ open Elab Tactic
 
 /-- `MetaM` version of the `rfl` tactic.
 
-This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive
-relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl].
+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].
 -/
 def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := do
   let .app (.app rel _) _ ← whnfR <|← instantiateMVars <|← goal.getType
     | throwError "reflexivity lemmas only apply to binary relations, not{
         indentExpr (← goal.getType)}"
-  let s ← saveState
-  let mut ex? := none
-  for lem in ← (reflExt.getState (← getEnv)).getMatch rel reflExt.config do
-    try
-      let gs ← goal.apply (← mkConstWithFreshMVarLevels lem)
-      if gs.isEmpty then return () else
-        logError <| MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
-          goalsToMessageData gs}"
-    catch e =>
-      ex? := ex? <|> (some (← saveState, e)) -- stash the first failure of `apply`
-    s.restore
-  if let some (sErr, e) := ex? then
-    sErr.restore
-    throw e
+  if let .app (.const ``Eq [_]) _ := rel then
+    throwError "MVarId.applyRfl does not solve `=` goals. Use `MVarId.refl` instead."
   else
-    throwError "rfl failed, no lemma with @[refl] applies"
+    let s ← saveState
+    let mut ex? := none
+    for lem in ← (reflExt.getState (← getEnv)).getMatch rel reflExt.config do
+      try
+        let gs ← goal.apply (← mkConstWithFreshMVarLevels lem)
+        if gs.isEmpty then return () else
+          logError <| MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
+            goalsToMessageData gs}"
+      catch e =>
+        ex? := ex? <|> (some (← saveState, e)) -- stash the first failure of `apply`
+      s.restore
+    if let some (sErr, e) := ex? then
+      sErr.restore
+      throw e
+    else
+      throwError "rfl failed, no lemma with @[refl] applies"
 
 /-- Helper theorem for `Lean.MVarId.liftReflToEq`. -/
 private theorem rel_of_eq_and_refl {α : Sort _} {R : α → α → Prop}
@@ -78,7 +85,7 @@ private theorem rel_of_eq_and_refl {α : Sort _} {R : α → α → Prop}
 
 /--
 Convert a goal of the form `x ~ y` into the form `x = y`, where `~` is a reflexive
-relation, that is, a relation which has a reflexive lemma tagged with the attribute `[refl]`.
+relation, that is, a relation which has a reflexive lemma tagged with the attribute `@[refl]`.
 If this can't be done, returns the original `MVarId`.
 -/
 def _root_.Lean.MVarId.liftReflToEq (mvarId : MVarId) : MetaM MVarId := do

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

@@ -14,7 +14,7 @@ macro (name := _root_.Lean.Parser.Command.registerSimpAttr) doc:(docComment)?
   "register_simp_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 s!"simp set for {id.getId.toString}"))
+  let descr := quote ((doc.map (·.getDocString) |>.getD s!"simp set for {id.getId.toString}").removeLeadingSpaces)
   let procId := mkIdentFrom id (simpAttrNameToSimprocAttrName id.getId)
   let procStr := procId.getId.toString
   let procIdParser := mkIdentFrom procId (`Parser.Attr ++ procId.getId)