feat: display diagnostic information at term and tactic set_option diagnostics true

We don't need to include reduction info at `simp` diagnostic information.

.github/workflows/check-stage0.yml

@@ -0,0 +1,57 @@
+name: Check for stage0 changes
+
+on:
+  merge_group:
+  pull_request:
+
+jobs:
+  check-stage0-on-queue:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v4
+      with:
+        ref: ${{ github.event.pull_request.head.sha }}
+        filter: blob:none
+        fetch-depth: 0
+
+    - name: Find base commit
+      if: github.event_name == 'pull_request'
+      run: echo "BASE=$(git merge-base origin/${{ github.base_ref }} HEAD)" >> "$GITHUB_ENV"
+
+    - name: Identify stage0 changes
+      run: |
+        git diff "${BASE:-HEAD^}..HEAD" --name-only -- stage0 |
+          grep -v -x -F $'stage0/src/stdlib_flags.h\nstage0/src/lean.mk.in' \
+          > "$RUNNER_TEMP/stage0" || true
+        if test -s "$RUNNER_TEMP/stage0"
+        then
+          echo "CHANGES=yes" >> "$GITHUB_ENV"
+        else
+          echo "CHANGES=no" >> "$GITHUB_ENV"
+        fi
+      shell: bash
+
+    - if: github.event_name == 'pull_request'
+      name: Set label
+      uses: actions/github-script@v7
+      with:
+        script: |
+          const { owner, repo, number: issue_number  } = context.issue;
+          if (process.env.CHANGES == 'yes') {
+            await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['changes-stage0'] }).catch(() => {});
+          } else {
+            await github.rest.issues.removeLabel({ owner, repo, issue_number, name: 'changes-stage0' }).catch(() => {});
+          }
+
+    - if: env.CHANGES == 'yes'
+      name: Report changes
+      run: |
+        echo "Found changes to stage0/, please do not merge using the merge queue." | tee "$GITHUB_STEP_SUMMARY"
+        # shellcheck disable=SC2129
+        echo '```'                  >> "$GITHUB_STEP_SUMMARY"
+        cat  "$RUNNER_TEMP/stage0"  >> "$GITHUB_STEP_SUMMARY"
+        echo '```'                  >> "$GITHUB_STEP_SUMMARY"
+
+    - if: github.event_name == 'merge_group' && env.CHANGES == 'yes'
+      name: Fail when on the merge queue
+      run: exit 1

.github/workflows/ci.yml

@@ -110,7 +110,7 @@ jobs:
               },*/
               {
                 "name": "macOS",
-                "os": "macos-latest",
+                "os": "macos-13",
                 "release": true,
                 "quick": false,
                 "shell": "bash -euxo pipefail {0}",
@@ -121,7 +121,7 @@ jobs:
               },
               {
                 "name": "macOS aarch64",
-                "os": "macos-latest",
+                "os": "macos-13",
                 "release": true,
                 "quick": false,
                 "cross": true,
@@ -277,18 +277,18 @@ jobs:
         uses: cachix/install-nix-action@v18
         with:
           install_url: https://releases.nixos.org/nix/nix-2.12.0/install
-        if: matrix.os == 'ubuntu-latest' && !matrix.cmultilib
+        if: runner.os == 'Linux' && !matrix.cmultilib
       - name: Install MSYS2
         uses: msys2/setup-msys2@v2
         with:
           msystem: clang64
           # `:p` means prefix with appropriate msystem prefix
           pacboy: "make python cmake:p clang:p ccache:p gmp:p git zip unzip diffutils binutils tree zstd:p tar"
-        if: matrix.os == 'windows-2022'
+        if: runner.os == 'Windows'
       - name: Install Brew Packages
         run: |
           brew install ccache tree zstd coreutils gmp
-        if: matrix.os == 'macos-latest'
+        if: runner.os == 'macOS'
       - name: Setup emsdk
         uses: mymindstorm/setup-emsdk@v12
         with:
@@ -312,13 +312,13 @@ jobs:
         run: |
           # open nix-shell once for initial setup
           true
-        if: matrix.os == 'ubuntu-latest'
+        if: runner.os == 'Linux'
       - name: Set up core dumps
         run: |
           mkdir -p $PWD/coredumps
           # store in current directory, for easy uploading together with binary
           echo $PWD/coredumps/%e.%p.%t | sudo tee /proc/sys/kernel/core_pattern
-        if: matrix.os == 'ubuntu-latest'
+        if: runner.os == 'Linux'
       - name: Build
         run: |
           mkdir build
@@ -423,7 +423,7 @@ jobs:
       - name: CCache stats
         run: ccache -s
       - name: Show stacktrace for coredumps
-        if: ${{ failure() && matrix.os == 'ubuntu-latest' }}
+        if: ${{ failure() && runner.os == 'Linux' }}
         run: |
           for c in coredumps/*; do
             progbin="$(file $c | sed "s/.*execfn: '\([^']*\)'.*/\1/")"
@@ -433,7 +433,7 @@ jobs:
       # shared libs
       #- name: Upload coredumps
       #  uses: actions/upload-artifact@v3
-      #  if: ${{ failure() && matrix.os == 'ubuntu-latest' }}
+      #  if: ${{ failure() && runner.os == 'Linux' }}
       #  with:
       #    name: coredumps-${{ matrix.name }}
       #    path: |

CODEOWNERS

@@ -6,7 +6,6 @@
 
 /.github/ @Kha @semorrison
 /RELEASES.md @semorrison
-/src/Init/IO.lean @joehendrix
 /src/kernel/ @leodemoura
 /src/lake/ @tydeu
 /src/Lean/Compiler/ @leodemoura
@@ -20,7 +19,6 @@
 /src/Lean/PrettyPrinter/Delaborator/ @kmill
 /src/Lean/Server/ @mhuisi
 /src/Lean/Widget/ @Vtec234
-/src/runtime/io.cpp @joehendrix
 /src/Init/Data/ @semorrison
 /src/Init/Data/Array/Lemmas.lean @digama0
 /src/Init/Data/List/Lemmas.lean @digama0

RELEASES.md

@@ -79,10 +79,13 @@ v4.8.0 (development in progress)
   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).
+  When `pp.mvars` is false, expression metavariables pretty print as `?_` and universe metavariables pretty print as `_`.
+  When `pp.mvars.withType` is true, expression metavariables pretty print with a type ascription.
+  These can be set when using `#guard_msgs` to make tests not depend on the particular names of metavariables.
+  [#3798](https://github.com/leanprover/lean4/pull/3798) and
+  [#3978](https://github.com/leanprover/lean4/pull/3978).
+
+* Hovers for terms in `match` expressions in the Infoview now reliably show the correct term.
 
 * Added `@[induction_eliminator]` and `@[cases_eliminator]` attributes to be able to define custom eliminators
   for the `induction` and `cases` tactics, replacing the `@[eliminator]` attribute.

doc/dev/bootstrap.md

@@ -75,14 +75,25 @@ The github repository will automatically update stage0 on `master` once
 
 If you have write access to the lean4 repository, you can also also manually
 trigger that process, for example to be able to use new features in the compiler itself.
-You can do that on <https://github.com/nomeata/lean4/actions/workflows/update-stage0.yml>
+You can do that on <https://github.com/leanprover/lean4/actions/workflows/update-stage0.yml>
 or using Github CLI with
 ```
 gh workflow run update-stage0.yml
 ```
 
-Leaving stage0 updates to the CI automation is preferable, but should you need to do it locally, you can use `make update-stage0-commit` in `build/release` to update `stage0` from `stage1` or `make -C stageN update-stage0-commit` to update from another stage.
-This command will automatically stage the updated files and introduce a commit, so make sure to commit your work before that. Then coordinate with the admins to not squash your PR so that stage 0 updates are preserved as separate commits.
+Leaving stage0 updates to the CI automation is preferable, but should you need
+to do it locally, you can use `make update-stage0-commit` in `build/release` to
+update `stage0` from `stage1` or `make -C stageN update-stage0-commit` to
+update from another stage.
+
+This command will automatically stage the updated files and introduce a commit,
+so make sure to commit your work before that.
+
+The CI should prevent PRs with changes to stage0 (besides `stdlib_flags.h`)
+from entering `master` through the (squashing!) merge queue, and label such PRs
+with the `changes-stage0` label. Such PRs should have a cleaned up history,
+with separate stage0 update commits; then coordinate with the admins to merge
+your PR using rebase merge, bypassing the merge queue.
 
 ## Further Bootstrapping Complications
 

doc/examples/Certora2022/ex8.lean

@@ -4,16 +4,16 @@ def ack : Nat → Nat → Nat
   | 0,   y   => y+1
   | x+1, 0   => ack x 1
   | x+1, y+1 => ack x (ack (x+1) y)
-termination_by ack x y => (x, y)
+termination_by x y => (x, y)
 
 def sum (a : Array Int) : Int :=
   let rec go (i : Nat) :=
-     if i < a.size then
+     if _ : i < a.size then
         a[i] + go (i+1)
      else
         0
+  termination_by a.size - i
   go 0
-termination_by go i => a.size - i
 
 set_option pp.proofs true
 #print sum.go

doc/examples/ICERM2022/ctor.lean

@@ -4,43 +4,42 @@ open Lean Meta
 
 def ctor (mvarId : MVarId) (idx : Nat) : MetaM (List MVarId) := do
   /- Set `MetaM` context using `mvarId` -/
-  withMVarContext mvarId do 
+  mvarId.withContext do
     /- Fail if the metavariable is already assigned. -/
-    checkNotAssigned mvarId `ctor
+    mvarId.checkNotAssigned `ctor
     /- Retrieve the target type, instantiateMVars, and use `whnf`. -/
-    let target ← getMVarType' mvarId
+    let target ← mvarId.getType'
     let .const declName us := target.getAppFn
       | throwTacticEx `ctor mvarId "target is not an inductive datatype"
     let .inductInfo { ctors, .. } ← getConstInfo declName
       | throwTacticEx `ctor mvarId "target is not an inductive datatype"
     if idx = 0 then
-      throwTacticEx `ctor mvarId "invalid index, it must be > 0"  
+      throwTacticEx `ctor mvarId "invalid index, it must be > 0"
     else if h : idx - 1 < ctors.length then
-      apply mvarId (.const ctors[idx - 1] us)
+      mvarId.apply (.const ctors[idx - 1] us)
     else
-      throwTacticEx `ctor mvarId "invalid index, inductive datatype has only {ctors.length} contructors"  
+      throwTacticEx `ctor mvarId "invalid index, inductive datatype has only {ctors.length} contructors"
 
 open Elab Tactic
 
-elab "ctor" idx:num : tactic => 
+elab "ctor" idx:num : tactic =>
   liftMetaTactic (ctor · idx.getNat)
 
-example (p : Prop) : p := by 
+example (p : Prop) : p := by
   ctor 1 -- Error
 
-example (h : q) : p ∨ q := by 
+example (h : q) : p ∨ q := by
   ctor 0 -- Error
   exact h
 
-example (h : q) : p ∨ q := by 
+example (h : q) : p ∨ q := by
   ctor 3 -- Error
   exact h
 
-example (h : q) : p ∨ q := by 
+example (h : q) : p ∨ q := by
   ctor 2
   exact h
 
-example (h : q) : p ∨ q := by 
+example (h : q) : p ∨ q := by
   ctor 1
-  exact h -- Error 
-
+  exact h -- Error

doc/examples/ICERM2022/meta.lean

@@ -5,15 +5,15 @@ open Lean Meta
 def ex1 (declName : Name) : MetaM Unit := do
   let info ← getConstInfo declName
   IO.println s!"{declName} : {← ppExpr info.type}"
-  if let some val := info.value? then 
+  if let some val := info.value? then
     IO.println s!"{declName} : {← ppExpr val}"
-    
+
 #eval ex1 ``Nat
 
 def ex2 (declName : Name) : MetaM Unit := do
   let info ← getConstInfo declName
   trace[Meta.debug] "{declName} : {info.type}"
-  if let some val := info.value? then 
+  if let some val := info.value? then
     trace[Meta.debug] "{declName} : {val}"
 
 #eval ex2 ``Add.add
@@ -30,9 +30,9 @@ def ex3 (declName : Name) : MetaM Unit := do
       trace[Meta.debug] "{x} : {← inferType x}"
 
 def myMin [LT α] [DecidableRel (α := α) (·<·)] (a b : α) : α :=
-  if a < b then 
+  if a < b then
     a
-  else 
+  else
     b
 
 set_option trace.Meta.debug true in
@@ -40,7 +40,7 @@ set_option trace.Meta.debug true in
 
 def ex4 : MetaM Unit := do
   let nat := mkConst ``Nat
-  withLocalDeclD `a nat fun a => 
+  withLocalDeclD `a nat fun a =>
   withLocalDeclD `b nat fun b => do
     let e ← mkAppM ``HAdd.hAdd #[a, b]
     trace[Meta.debug] "{e} : {← inferType e}"
@@ -66,15 +66,17 @@ open Elab Term
 
 def ex5 : TermElabM Unit := do
   let nat := Lean.mkConst ``Nat
-  withLocalDeclD `a nat fun a => do 
+  withLocalDeclD `a nat fun a => do
   withLocalDeclD `b nat fun b => do
     let ab ← mkAppM ``HAdd.hAdd #[a, b]
-    let stx ← `(fun x => if x < 10 then $(← exprToSyntax ab) + x else x + $(← exprToSyntax a))
+    let abStx ← exprToSyntax ab
+    let aStx ← exprToSyntax a
+    let stx ← `(fun x => if x < 10 then $abStx + x else x + $aStx)
     let e ← elabTerm stx none
     trace[Meta.debug] "{e} : {← inferType e}"
     let e := mkApp e (mkNatLit 5)
     let e ← whnf e
     trace[Meta.debug] "{e}"
-       
+
 set_option trace.Meta.debug true in
 #eval ex5

doc/examples/NFM2022/nfm8.lean

@@ -4,16 +4,16 @@ def ack : Nat → Nat → Nat
   | 0,   y   => y+1
   | x+1, 0   => ack x 1
   | x+1, y+1 => ack x (ack (x+1) y)
-termination_by ack x y => (x, y)
+termination_by x y => (x, y)
 
 def sum (a : Array Int) : Int :=
   let rec go (i : Nat) :=
-     if i < a.size then
+     if _ : i < a.size then
         a[i] + go (i+1)
      else
         0
+  termination_by a.size - i
   go 0
-termination_by go i => a.size - i
 
 set_option pp.proofs true
 #print sum.go

script/issues_summary.sh

@@ -0,0 +1,39 @@
+#!/bin/bash
+
+# https://chat.openai.com/share/7469c7c3-aceb-4d80-aee5-62982e1f1538
+
+# Output CSV Header
+echo '"Issue URL","Title","Days Since Creation","Days Since Last Update","Total Reactions","Assignee","Labels"'
+
+# Get the current date in YYYY-MM-DD format
+today=$(date +%Y-%m-%d)
+
+# Fetch only open issues (excluding PRs and closed issues) from the repository 'leanprover/lean4'
+issues=$(gh api repos/leanprover/lean4/issues --paginate --jq '.[] | select(.pull_request == null and .state == "open") | {url: .html_url, title: .title, created_at: (.created_at | split("T")[0]), updated_at: (.updated_at | split("T")[0]), number: .number, assignee: (.assignee.login // ""), labels: [.labels[].name] | join(",")}')
+
+# Process each JSON object
+echo "$issues" | while IFS= read -r issue; do
+    # Extract fields from JSON
+    url=$(echo "$issue" | jq -r '.url')
+    title=$(echo "$issue" | jq -r '.title')
+    created_at=$(echo "$issue" | jq -r '.created_at')
+    updated_at=$(echo "$issue" | jq -r '.updated_at')
+    issue_number=$(echo "$issue" | jq -r '.number')
+    assignee=$(echo "$issue" | jq -r '.assignee')
+    labels=$(echo "$issue" | jq -r '.labels')
+
+    # Calculate days since creation and update using macOS compatible date calculation
+    days_since_created=$(( ($(date -jf "%Y-%m-%d" "$today" +%s) - $(date -jf "%Y-%m-%d" "$created_at" +%s)) / 86400 ))
+    days_since_updated=$(( ($(date -jf "%Y-%m-%d" "$today" +%s) - $(date -jf "%Y-%m-%d" "$updated_at" +%s)) / 86400 ))
+
+    # Fetch the total number of reactions for each issue
+    reaction_data=$(gh api repos/leanprover/lean4/issues/$issue_number/reactions --paginate --jq 'length' 2>&1)
+    if [[ $reaction_data == *"Not Found"* ]]; then
+        total_reactions="Error fetching reactions"
+    else
+        total_reactions=$reaction_data
+    fi
+
+    # Format output as CSV by escaping quotes and delimiting with commas
+    echo "\"$url\",\"${title//\"/\"\"}\",\"$days_since_created\",\"$days_since_updated\",\"$total_reactions\",\"$assignee\",\"$labels\""
+done

src/CMakeLists.txt

@@ -315,6 +315,12 @@ endif()
 string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
 string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
 
+# in local builds, link executables and not just dynlibs against C++ stdlib as well,
+# which is required for e.g. asan
+if(NOT LEAN_STANDALONE)
+  string(APPEND CMAKE_EXE_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
+endif()
+
 # flags for user binaries = flags for toolchain binaries + Lake
 string(APPEND LEANC_STATIC_LINKER_FLAGS " ${TOOLCHAIN_STATIC_LINKER_FLAGS} -lLake")
 

src/Init/Core.lean

@@ -2040,4 +2040,8 @@ class LawfulCommIdentity (op : α → α → α) (o : outParam α) [hc : Commuta
   left_id a := Eq.trans (hc.comm o a) (right_id a)
   right_id a := Eq.trans (hc.comm a o) (left_id a)
 
+instance : Commutative Or := ⟨fun _ _ => propext or_comm⟩
+instance : Commutative And := ⟨fun _ _ => propext and_comm⟩
+instance : Commutative Iff := ⟨fun _ _ => propext iff_comm⟩
+
 end Std

src/Init/Data/Array/Basic.lean

@@ -31,6 +31,7 @@ def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
   go (i : Nat) (acc : Array α) : Array α :=
     if h : i < n then go (i+1) (acc.push (f ⟨i, h⟩)) else acc
 termination_by n - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 /-- The array `#[0, 1, ..., n - 1]`. -/
 def range (n : Nat) : Array Nat :=
@@ -306,6 +307,7 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
     else
       pure r
   termination_by as.size - i
+  decreasing_by simp_wf; decreasing_trivial_pre_omega
   map 0 (mkEmpty as.size)
 
 @[inline]
@@ -378,6 +380,7 @@ def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as :
       else
         pure false
       termination_by stop - j
+      decreasing_by simp_wf; decreasing_trivial_pre_omega
     loop start
   if h : stop ≤ as.size then
     any stop h
@@ -463,6 +466,7 @@ def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
       if p as[j] then some j else loop (j + 1)
     else none
     termination_by as.size - j
+    decreasing_by simp_wf; decreasing_trivial_pre_omega
   loop 0
 
 def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
@@ -557,6 +561,7 @@ def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) (
   else
     true
 termination_by a.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 @[inline] def isEqv (a b : Array α) (p : α → α → Bool) : Bool :=
   if h : a.size = b.size then
@@ -661,6 +666,7 @@ def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size)
     else indexOfAux a v (i+1)
   else none
 termination_by a.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
   indexOfAux a v 0
@@ -703,6 +709,7 @@ def popWhile (p : α → Bool) (as : Array α) : Array α :=
   else
     as
 termination_by as.size
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def takeWhile (p : α → Bool) (as : Array α) : Array α :=
   let rec go (i : Nat) (r : Array α) : Array α :=
@@ -715,6 +722,7 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
     else
       r
     termination_by as.size - i
+    decreasing_by simp_wf; decreasing_trivial_pre_omega
   go 0 #[]
 
 /-- Remove the element at a given index from an array without bounds checks, using a `Fin` index.
@@ -731,6 +739,7 @@ def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
   else
     a.pop
 termination_by a.size - i.val
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
   induction a, i using Array.feraseIdx.induct with
@@ -763,6 +772,7 @@ def erase [BEq α] (as : Array α) (a : α) : Array α :=
     else
       as
     termination_by j.1
+    decreasing_by simp_wf; decreasing_trivial_pre_omega
   let j := as.size
   let as := as.push a
   loop as ⟨j, size_push .. ▸ j.lt_succ_self⟩
@@ -816,6 +826,7 @@ def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : N
   else
     true
 termination_by as.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 /-- Return true iff `as` is a prefix of `bs`.
 That is, `bs = as ++ t` for some `t : List α`.-/
@@ -837,6 +848,7 @@ private def allDiffAux [BEq α] (as : Array α) (i : Nat) : Bool :=
   else
     true
 termination_by as.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def allDiff [BEq α] (as : Array α) : Bool :=
   allDiffAux as 0
@@ -852,6 +864,7 @@ def allDiff [BEq α] (as : Array α) : Bool :=
   else
     cs
 termination_by as.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 @[inline] def zipWith (as : Array α) (bs : Array β) (f : α → β → γ) : Array γ :=
   zipWithAux f as bs 0 #[]

src/Init/Data/Array/BasicAux.lean

@@ -48,6 +48,7 @@ where
       let b ← f as[i]
       go (i+1) ⟨acc.val.push b, by simp [acc.property]⟩ hlt
   termination_by as.size - i
+  decreasing_by decreasing_trivial_pre_omega
 
 @[inline] private unsafe def mapMonoMImp [Monad m] (as : Array α) (f : α → m α) : m (Array α) :=
   go 0 as

src/Init/Data/Array/DecidableEq.lean

@@ -21,6 +21,8 @@ theorem eq_of_isEqvAux [DecidableEq α] (a b : Array α) (hsz : a.size = b.size)
     subst heq
     exact absurd (Nat.lt_of_lt_of_le high low) (Nat.lt_irrefl j)
 termination_by a.size - i
+decreasing_by decreasing_trivial_pre_omega
+
 
 theorem eq_of_isEqv [DecidableEq α] (a b : Array α) : Array.isEqv a b (fun x y => x = y) → a = b := by
   simp [Array.isEqv]
@@ -37,6 +39,7 @@ theorem isEqvAux_self [DecidableEq α] (a : Array α) (i : Nat) : Array.isEqvAux
   case inl h => simp [h, isEqvAux_self a (i+1)]
   case inr h => simp [h]
 termination_by a.size - i
+decreasing_by decreasing_trivial_pre_omega
 
 theorem isEqv_self [DecidableEq α] (a : Array α) : Array.isEqv a a (fun x y => x = y) = true := by
   simp [isEqv, isEqvAux_self]

src/Init/Data/Array/Lemmas.lean

@@ -131,6 +131,7 @@ where
       simp [aux (i+1), map_eq_pure_bind]; rfl
     · rw [List.drop_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
   termination_by arr.size - i
+  decreasing_by decreasing_trivial_pre_omega
 
 @[simp] theorem map_data (f : α → β) (arr : Array α) : (arr.map f).data = arr.data.map f := by
   rw [map, mapM_eq_foldlM]

src/Init/Data/Array/Mem.lean

@@ -27,13 +27,20 @@ theorem sizeOf_lt_of_mem [SizeOf α] {as : Array α} (h : a ∈ as) : sizeOf a <
   cases as with | _ as =>
   exact Nat.lt_trans (List.sizeOf_get ..) (by simp_arith)
 
+@[simp] theorem sizeOf_getElem [SizeOf α] (as : Array α) (i : Nat) (h : i < as.size) :
+  sizeOf (as[i]'h) < sizeOf as := sizeOf_get _ _
+
 /-- This tactic, added to the `decreasing_trivial` toolbox, proves that
 `sizeOf arr[i] < sizeOf arr`, which is useful for well founded recursions
 over a nested inductive like `inductive T | mk : Array T → T`. -/
 macro "array_get_dec" : tactic =>
   `(tactic| first
-    | apply sizeOf_get
-    | apply Nat.lt_trans (sizeOf_get ..); simp_arith)
+    -- subsumed by simp
+    -- | with_reducible apply sizeOf_get
+    -- | with_reducible apply sizeOf_getElem
+    | (with_reducible apply Nat.lt_trans (sizeOf_get ..)); simp_arith
+    | (with_reducible apply Nat.lt_trans (sizeOf_getElem ..)); simp_arith
+    )
 
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| array_get_dec)
 
@@ -43,9 +50,10 @@ provided that `a ∈ arr` which is useful for well founded recursions over a nes
 -- NB: This is analogue to tactic `sizeOf_list_dec`
 macro "array_mem_dec" : tactic =>
   `(tactic| first
-    | apply Array.sizeOf_lt_of_mem; assumption; done
-    | apply Nat.lt_trans (Array.sizeOf_lt_of_mem ?h)
-      case' h => assumption
+    | with_reducible apply Array.sizeOf_lt_of_mem; assumption; done
+    | with_reducible
+        apply Nat.lt_trans (Array.sizeOf_lt_of_mem ?h)
+        case' h => assumption
       simp_arith)
 
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| array_mem_dec)

src/Init/Data/Array/QSort.lean

@@ -27,6 +27,7 @@ def qpartition (as : Array α) (lt : α → α → Bool) (lo hi : Nat) : Nat ×
       let as := as.swap! i hi
       (i, as)
     termination_by hi - j
+    decreasing_by all_goals simp_wf; decreasing_trivial_pre_omega
   loop as lo lo
 
 @[inline] partial def qsort (as : Array α) (lt : α → α → Bool) (low := 0) (high := as.size - 1) : Array α :=

src/Init/Data/BitVec/Lemmas.lean

@@ -103,7 +103,13 @@ theorem eq_of_getMsb_eq {x y : BitVec w}
     have q := pred ⟨w - 1 - i, q_lt⟩
     simpa [q_lt, Nat.sub_sub_self, r] using q
 
-@[simp] theorem of_length_zero {x : BitVec 0} : x = 0#0 := by ext; simp
+-- This cannot be a `@[simp]` lemma, as it would be tried at every term.
+theorem of_length_zero {x : BitVec 0} : x = 0#0 := by ext; simp
+
+@[simp] theorem toNat_zero_length (x : BitVec 0) : x.toNat = 0 := by simp [of_length_zero]
+@[simp] theorem getLsb_zero_length (x : BitVec 0) : x.getLsb i = false := by simp [of_length_zero]
+@[simp] theorem getMsb_zero_length (x : BitVec 0) : x.getMsb i = false := by simp [of_length_zero]
+@[simp] theorem msb_zero_length (x : BitVec 0) : x.msb = false := by simp [BitVec.msb, of_length_zero]
 
 theorem eq_of_toFin_eq : ∀ {x y : BitVec w}, x.toFin = y.toFin → x = y
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
@@ -336,7 +342,7 @@ theorem nat_eq_toNat (x : BitVec w) (y : Nat)
 @[simp] theorem getMsb_zeroExtend_add {x : BitVec w} (h : k ≤ i) :
     (x.zeroExtend (w + k)).getMsb i = x.getMsb (i - k) := by
   by_cases h : w = 0
-  · subst h; simp
+  · subst h; simp [of_length_zero]
   simp only [getMsb, getLsb_zeroExtend]
   by_cases h₁ : i < w + k <;> by_cases h₂ : i - k < w <;> by_cases h₃ : w + k - 1 - i < w + k
     <;> simp [h₁, h₂, h₃]
@@ -826,13 +832,18 @@ theorem ofNat_add_ofNat {n} (x y : Nat) : x#n + y#n = (x + y)#n :=
 
 protected theorem add_assoc (x y z : BitVec n) : x + y + z = x + (y + z) := by
   apply eq_of_toNat_eq ; simp [Nat.add_assoc]
+instance : Std.Associative (α := BitVec n) (· + ·) := ⟨BitVec.add_assoc⟩
 
 protected theorem add_comm (x y : BitVec n) : x + y = y + x := by
   simp [add_def, Nat.add_comm]
+instance : Std.Commutative (α := BitVec n) (· + ·) := ⟨BitVec.add_comm⟩
 
 @[simp] protected theorem add_zero (x : BitVec n) : x + 0#n = x := by simp [add_def]
 
 @[simp] protected theorem zero_add (x : BitVec n) : 0#n + x = x := by simp [add_def]
+instance : Std.LawfulIdentity (α := BitVec n) (· + ·) 0#n where
+  left_id := BitVec.zero_add
+  right_id := BitVec.add_zero
 
 theorem truncate_add (x y : BitVec w) (h : i ≤ w) :
     (x + y).truncate i = x.truncate i + y.truncate i := by

src/Init/Data/Bool.lean

@@ -74,6 +74,7 @@ Added for confluence with `not_and_self` `and_not_self` on term
 @[simp] theorem eq_false_and_eq_true_self : ∀(b : Bool), (b = false ∧ b = true) ↔ False := by decide
 
 theorem and_comm : ∀ (x y : Bool), (x && y) = (y && x) := by decide
+instance : Std.Commutative (· && ·) := ⟨and_comm⟩
 
 theorem and_left_comm : ∀ (x y z : Bool), (x && (y && z)) = (y && (x && z)) := by decide
 theorem and_right_comm : ∀ (x y z : Bool), ((x && y) && z) = ((x && z) && y) := by decide
@@ -120,6 +121,7 @@ Needed for confluence of term `(a || b) ↔ a` which reduces to `(a || b) = a` v
 @[simp] theorem iff_or_self : ∀(a b : Bool), (b = (a || b)) ↔ (a → b) := by decide
 
 theorem or_comm : ∀ (x y : Bool), (x || y) = (y || x) := by decide
+instance : Std.Commutative (· || ·) := ⟨or_comm⟩
 
 theorem or_left_comm : ∀ (x y z : Bool), (x || (y || z)) = (y || (x || z)) := by decide
 theorem or_right_comm : ∀ (x y z : Bool), ((x || y) || z) = ((x || z) || y) := by decide
@@ -186,12 +188,18 @@ in false_eq and true_eq.
 @[simp] theorem true_beq  : ∀b, (true  == b) =  b := by decide
 @[simp] theorem false_beq : ∀b, (false == b) = !b := by decide
 @[simp] theorem beq_true  : ∀b, (b == true)  =  b := by decide
+instance : Std.LawfulIdentity (· == ·) true where
+  left_id := true_beq
+  right_id := beq_true
 @[simp] theorem beq_false : ∀b, (b == false) = !b := by decide
 
 @[simp] theorem true_bne  : ∀(b : Bool), (true  != b) = !b := by decide
 @[simp] theorem false_bne : ∀(b : Bool), (false != b) =  b := by decide
 @[simp] theorem bne_true  : ∀(b : Bool), (b != true)  = !b := by decide
 @[simp] theorem bne_false : ∀(b : Bool), (b != false) =  b := by decide
+instance : Std.LawfulIdentity (· != ·) false where
+  left_id := false_bne
+  right_id := bne_false
 
 @[simp] theorem not_beq_self : ∀ (x : Bool), ((!x) == x) = false := by decide
 @[simp] theorem beq_not_self : ∀ (x : Bool), (x   == !x) = false := by decide
@@ -214,6 +222,7 @@ due to `beq_iff_eq`.
 @[simp] theorem not_bne_not : ∀ (x y : Bool), ((!x) != (!y)) = (x != y) := by decide
 
 @[simp] theorem bne_assoc : ∀ (x y z : Bool), ((x != y) != z) = (x != (y != z)) := by decide
+instance : Std.Associative (· != ·) := ⟨bne_assoc⟩
 
 @[simp] theorem bne_left_inj  : ∀ (x y z : Bool), (x != y) = (x != z) ↔ y = z := by decide
 @[simp] theorem bne_right_inj : ∀ (x y z : Bool), (x != z) = (y != z) ↔ x = y := by decide

src/Init/Data/Fin/Fold.lean

@@ -12,6 +12,7 @@ import Init.Data.Nat.Linear
   loop (x : α) (i : Nat) : α :=
     if h : i < n then loop (f x ⟨i, h⟩) (i+1) else x
   termination_by n - i
+  decreasing_by decreasing_trivial_pre_omega
 
 /-- Folds over `Fin n` from the right: `foldr 3 f x = f 0 (f 1 (f 2 x))`. -/
 @[inline] def foldr (n) (f : Fin n → α → α) (init : α) : α := loop ⟨n, Nat.le_refl n⟩ init where

src/Init/Data/Fin/Iterate.lean

@@ -23,6 +23,7 @@ def hIterateFrom (P : Nat → Sort _) {n} (f : ∀(i : Fin n), P i.val → P (i.
     have p : i = n := (or_iff_left g).mp (Nat.eq_or_lt_of_le ubnd)
     _root_.cast (congrArg P p) a
   termination_by n - i
+  decreasing_by decreasing_trivial_pre_omega
 
 /--
 `hIterate` is a heterogenous iterative operation that applies a

src/Init/Data/Fin/Lemmas.lean

@@ -602,6 +602,7 @@ A version of `Fin.succRec` taking `i : Fin n` as the first argument. -/
     @Fin.succRecOn (n + 1) i.succ motive zero succ = succ n i (Fin.succRecOn i zero succ) := by
   cases i; rfl
 
+
 /-- Define `motive i` by induction on `i : Fin (n + 1)` via induction on the underlying `Nat` value.
 This function has two arguments: `zero` handles the base case on `motive 0`,
 and `succ` defines the inductive step using `motive i.castSucc`.
@@ -610,8 +611,12 @@ and `succ` defines the inductive step using `motive i.castSucc`.
 @[elab_as_elim] def induction {motive : Fin (n + 1) → Sort _} (zero : motive 0)
     (succ : ∀ i : Fin n, motive (castSucc i) → motive i.succ) :
     ∀ i : Fin (n + 1), motive i
-  | ⟨0, hi⟩ => by rwa [Fin.mk_zero]
-  | ⟨i+1, hi⟩ => succ ⟨i, Nat.lt_of_succ_lt_succ hi⟩ (induction zero succ ⟨i, Nat.lt_of_succ_lt hi⟩)
+  | ⟨i, hi⟩ => go i hi
+where
+  -- Use a curried function so that this is structurally recursive
+  go : ∀ (i : Nat) (hi : i < n + 1), motive ⟨i, hi⟩
+  | 0, hi => by rwa [Fin.mk_zero]
+  | i+1, hi => succ ⟨i, Nat.lt_of_succ_lt_succ hi⟩ (go i (Nat.lt_of_succ_lt hi))
 
 @[simp] theorem induction_zero {motive : Fin (n + 1) → Sort _} (zero : motive 0)
     (hs : ∀ i : Fin n, motive (castSucc i) → motive i.succ) :
@@ -793,15 +798,20 @@ protected theorem mul_one (k : Fin (n + 1)) : k * 1 = k := by
 
 protected theorem mul_comm (a b : Fin n) : a * b = b * a :=
   ext <| by rw [mul_def, mul_def, Nat.mul_comm]
+instance : Std.Commutative (α := Fin n) (· * ·) := ⟨Fin.mul_comm⟩
 
 protected theorem mul_assoc (a b c : Fin n) : a * b * c = a * (b * c) := by
   apply eq_of_val_eq
   simp only [val_mul]
   rw [← Nat.mod_eq_of_lt a.isLt, ← Nat.mod_eq_of_lt b.isLt, ← Nat.mod_eq_of_lt c.isLt]
   simp only [← Nat.mul_mod, Nat.mul_assoc]
+instance : Std.Associative (α := Fin n) (· * ·) := ⟨Fin.mul_assoc⟩
 
 protected theorem one_mul (k : Fin (n + 1)) : (1 : Fin (n + 1)) * k = k := by
   rw [Fin.mul_comm, Fin.mul_one]
+instance : Std.LawfulIdentity (α := Fin (n + 1)) (· * ·) 1 where
+  left_id := Fin.one_mul
+  right_id := Fin.mul_one
 
 protected theorem mul_zero (k : Fin (n + 1)) : k * 0 = 0 := by simp [ext_iff, mul_def]
 

src/Init/Data/Int/Lemmas.lean

@@ -137,12 +137,16 @@ protected theorem add_comm : ∀ a b : Int, a + b = b + a
   | ofNat _, -[_+1]  => rfl
   | -[_+1],  ofNat _ => rfl
   | -[_+1],  -[_+1]  => by simp [Nat.add_comm]
+instance : Std.Commutative (α := Int) (· + ·) := ⟨Int.add_comm⟩
 
 @[simp] protected theorem add_zero : ∀ a : Int, a + 0 = a
   | ofNat _ => rfl
   | -[_+1]  => rfl
 
 @[simp] protected theorem zero_add (a : Int) : 0 + a = a := Int.add_comm .. ▸ a.add_zero
+instance : Std.LawfulIdentity (α := Int) (· + ·) 0 where
+  left_id := Int.zero_add
+  right_id := Int.add_zero
 
 theorem ofNat_add_negSucc_of_lt (h : m < n.succ) : ofNat m + -[n+1] = -[n - m+1] :=
   show subNatNat .. = _ by simp [succ_sub (le_of_lt_succ h), subNatNat]
@@ -196,6 +200,7 @@ where
     simp
     rw [Int.add_comm, subNatNat_add_negSucc]
     simp [Nat.add_comm, Nat.add_left_comm, Nat.add_assoc]
+instance : Std.Associative (α := Int) (· + ·) := ⟨Int.add_assoc⟩
 
 protected theorem add_left_comm (a b c : Int) : a + (b + c) = b + (a + c) := by
   rw [← Int.add_assoc, Int.add_comm a, Int.add_assoc]
@@ -351,6 +356,7 @@ protected theorem sub_right_inj (i j k : Int) : (i - k = j - k) ↔ i = j := by
 
 protected theorem mul_comm (a b : Int) : a * b = b * a := by
   cases a <;> cases b <;> simp [Nat.mul_comm]
+instance : Std.Commutative (α := Int) (· * ·) := ⟨Int.mul_comm⟩
 
 theorem ofNat_mul_negOfNat (m n : Nat) : (m : Nat) * negOfNat n = negOfNat (m * n) := by
   cases n <;> rfl
@@ -369,6 +375,7 @@ attribute [local simp] ofNat_mul_negOfNat negOfNat_mul_ofNat
 
 protected theorem mul_assoc (a b c : Int) : a * b * c = a * (b * c) := by
   cases a <;> cases b <;> cases c <;> simp [Nat.mul_assoc]
+instance : Std.Associative (α := Int) (· * ·) := ⟨Int.mul_assoc⟩
 
 protected theorem mul_left_comm (a b c : Int) : a * (b * c) = b * (a * c) := by
   rw [← Int.mul_assoc, ← Int.mul_assoc, Int.mul_comm a]
@@ -458,6 +465,9 @@ protected theorem sub_mul (a b c : Int) : (a - b) * c = a * c - b * c := by
   | -[n+1]  => show -[1 * n +1] = -[n+1] by rw [Nat.one_mul]
 
 @[simp] protected theorem mul_one (a : Int) : a * 1 = a := by rw [Int.mul_comm, Int.one_mul]
+instance : Std.LawfulIdentity (α := Int) (· * ·) 1 where
+  left_id := Int.one_mul
+  right_id := Int.mul_one
 
 protected theorem mul_neg_one (a : Int) : a * -1 = -a := by rw [Int.mul_neg, Int.mul_one]
 

src/Init/Data/Int/Order.lean

@@ -187,6 +187,7 @@ protected theorem min_comm (a b : Int) : min a b = min b a := by
   by_cases h₁ : a ≤ b <;> by_cases h₂ : b ≤ a <;> simp [h₁, h₂]
   · exact Int.le_antisymm h₁ h₂
   · cases not_or_intro h₁ h₂ <| Int.le_total ..
+instance : Std.Commutative (α := Int) min := ⟨Int.min_comm⟩
 
 protected theorem min_le_right (a b : Int) : min a b ≤ b := by rw [Int.min_def]; split <;> simp [*]
 
@@ -206,6 +207,7 @@ protected theorem max_comm (a b : Int) : max a b = max b a := by
   by_cases h₁ : a ≤ b <;> by_cases h₂ : b ≤ a <;> simp [h₁, h₂]
   · exact Int.le_antisymm h₂ h₁
   · cases not_or_intro h₁ h₂ <| Int.le_total ..
+instance : Std.Commutative (α := Int) max := ⟨Int.max_comm⟩
 
 protected theorem le_max_left (a b : Int) : a ≤ max a b := by rw [Int.max_def]; split <;> simp [*]
 

src/Init/Data/List/Basic.lean

@@ -127,6 +127,9 @@ instance : Append (List α) := ⟨List.append⟩
   | nil => rfl
   | cons a as ih =>
     simp_all [HAppend.hAppend, Append.append, List.append]
+instance : Std.LawfulIdentity (α := List α) (· ++ ·) [] where
+  left_id := nil_append
+  right_id := append_nil
 
 @[simp] theorem cons_append (a : α) (as bs : List α) : (a::as) ++ bs = a::(as ++ bs) := rfl
 
@@ -136,6 +139,7 @@ theorem append_assoc (as bs cs : List α) : (as ++ bs) ++ cs = as ++ (bs ++ cs)
   induction as with
   | nil => rfl
   | cons a as ih => simp [ih]
+instance : Std.Associative (α := List α) (· ++ ·) := ⟨append_assoc⟩
 
 theorem append_cons (as : List α) (b : α) (bs : List α) : as ++ b :: bs = as ++ [b] ++ bs := by
   induction as with

src/Init/Data/List/BasicAux.lean

@@ -157,6 +157,13 @@ def getLastD : (as : List α) → (fallback : α) → α
   | [],   a₀ => a₀
   | a::as, _ => getLast (a::as) (fun h => List.noConfusion h)
 
+/--
+`O(n)`. Rotates the elements of `xs` to the left such that the element at
+`xs[i]` rotates to `xs[(i - n) % l.length]`.
+* `rotateLeft [1, 2, 3, 4, 5] 3 = [4, 5, 1, 2, 3]`
+* `rotateLeft [1, 2, 3, 4, 5] 5 = [1, 2, 3, 4, 5]`
+* `rotateLeft [1, 2, 3, 4, 5] = [2, 3, 4, 5, 1]`
+-/
 def rotateLeft (xs : List α) (n : Nat := 1) : List α :=
   let len := xs.length
   if len ≤ 1 then
@@ -167,6 +174,13 @@ def rotateLeft (xs : List α) (n : Nat := 1) : List α :=
     let e := xs.drop n
     e ++ b
 
+/--
+`O(n)`. Rotates the elements of `xs` to the right such that the element at
+`xs[i]` rotates to `xs[(i + n) % l.length]`.
+* `rotateRight [1, 2, 3, 4, 5] 3 = [3, 4, 5, 1, 2]`
+* `rotateRight [1, 2, 3, 4, 5] 5 = [1, 2, 3, 4, 5]`
+* `rotateRight [1, 2, 3, 4, 5] = [5, 1, 2, 3, 4]`
+-/
 def rotateRight (xs : List α) (n : Nat := 1) : List α :=
   let len := xs.length
   if len ≤ 1 then
@@ -212,9 +226,10 @@ theorem sizeOf_lt_of_mem [SizeOf α] {as : List α} (h : a ∈ as) : sizeOf a <
 over a nested inductive like `inductive T | mk : List T → T`. -/
 macro "sizeOf_list_dec" : tactic =>
   `(tactic| first
-    | apply sizeOf_lt_of_mem; assumption; done
-    | apply Nat.lt_trans (sizeOf_lt_of_mem ?h)
-      case' h => assumption
+    | with_reducible apply sizeOf_lt_of_mem; assumption; done
+    | with_reducible
+        apply Nat.lt_trans (sizeOf_lt_of_mem ?h)
+        case' h => assumption
       simp_arith)
 
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| sizeOf_list_dec)
@@ -297,6 +312,15 @@ def mapMono (as : List α) (f : α → α) : List α :=
 Monadic generalization of `List.partition`.
 
 This uses `Array.toList` and which isn't imported by `Init.Data.List.Basic`.
+```
+def posOrNeg (x : Int) : Except String Bool :=
+  if x > 0 then pure true
+  else if x < 0 then pure false
+  else throw "Zero is not positive or negative"
+
+partitionM posOrNeg [-1, 2, 3] = Except.ok ([2, 3], [-1])
+partitionM posOrNeg [0, 2, 3] = Except.error "Zero is not positive or negative"
+```
 -/
 @[inline] def partitionM [Monad m] (p : α → m Bool) (l : List α) : m (List α × List α) :=
   go l #[] #[]

src/Init/Data/Nat/Basic.lean

@@ -137,6 +137,9 @@ instance : LawfulBEq Nat where
 @[simp] protected theorem zero_add : ∀ (n : Nat), 0 + n = n
   | 0   => rfl
   | n+1 => congrArg succ (Nat.zero_add n)
+instance : Std.LawfulIdentity (α := Nat) (· + ·) 0 where
+  left_id := Nat.zero_add
+  right_id := Nat.add_zero
 
 theorem succ_add : ∀ (n m : Nat), (succ n) + m = succ (n + m)
   | _, 0   => rfl
@@ -160,10 +163,12 @@ protected theorem add_comm : ∀ (n m : Nat), n + m = m + n
     have : succ (n + m) = succ (m + n) := by apply congrArg; apply Nat.add_comm
     rw [succ_add m n]
     apply this
+instance : Std.Commutative (α := Nat) (· + ·) := ⟨Nat.add_comm⟩
 
 protected theorem add_assoc : ∀ (n m k : Nat), (n + m) + k = n + (m + k)
   | _, _, 0      => rfl
   | n, m, succ k => congrArg succ (Nat.add_assoc n m k)
+instance : Std.Associative (α := Nat) (· + ·) := ⟨Nat.add_assoc⟩
 
 protected theorem add_left_comm (n m k : Nat) : n + (m + k) = m + (n + k) := by
   rw [← Nat.add_assoc, Nat.add_comm n m, Nat.add_assoc]
@@ -207,12 +212,16 @@ theorem succ_mul (n m : Nat) : (succ n) * m = (n * m) + m := by
 protected theorem mul_comm : ∀ (n m : Nat), n * m = m * n
   | n, 0      => (Nat.zero_mul n).symm ▸ (Nat.mul_zero n).symm ▸ rfl
   | n, succ m => (mul_succ n m).symm ▸ (succ_mul m n).symm ▸ (Nat.mul_comm n m).symm ▸ rfl
+instance : Std.Commutative (α := Nat) (· * ·) := ⟨Nat.mul_comm⟩
 
 @[simp] protected theorem mul_one : ∀ (n : Nat), n * 1 = n :=
   Nat.zero_add
 
 @[simp] protected theorem one_mul (n : Nat) : 1 * n = n :=
   Nat.mul_comm n 1 ▸ Nat.mul_one n
+instance : Std.LawfulIdentity (α := Nat) (· * ·) 1 where
+  left_id := Nat.one_mul
+  right_id := Nat.mul_one
 
 protected theorem left_distrib (n m k : Nat) : n * (m + k) = n * m + n * k := by
   induction n with
@@ -231,6 +240,7 @@ protected theorem add_mul (n m k : Nat) : (n + m) * k = n * k + m * k :=
 protected theorem mul_assoc : ∀ (n m k : Nat), (n * m) * k = n * (m * k)
   | n, m, 0      => rfl
   | n, m, succ k => by simp [mul_succ, Nat.mul_assoc n m k, Nat.left_distrib]
+instance : Std.Associative (α := Nat) (· * ·) := ⟨Nat.mul_assoc⟩
 
 protected theorem mul_left_comm (n m k : Nat) : n * (m * k) = m * (n * k) := by
   rw [← Nat.mul_assoc, Nat.mul_comm n m, Nat.mul_assoc]

src/Init/Data/Nat/Gcd.lean

@@ -54,9 +54,13 @@ theorem gcd_succ (x y : Nat) : gcd (succ x) y = gcd (y % succ x) (succ x) :=
     -- `simp [gcd_succ]` produces an invalid term unless `gcd_succ` is proved with `id rfl` instead
     rw [gcd_succ]
     exact gcd_zero_left _
+instance : Std.LawfulIdentity gcd 0 where
+  left_id := gcd_zero_left
+  right_id := gcd_zero_right
 
 @[simp] theorem gcd_self (n : Nat) : gcd n n = n := by
   cases n <;> simp [gcd_succ]
+instance : Std.IdempotentOp gcd := ⟨gcd_self⟩
 
 theorem gcd_rec (m n : Nat) : gcd m n = gcd (n % m) m :=
   match m with
@@ -97,6 +101,7 @@ theorem gcd_comm (m n : Nat) : gcd m n = gcd n m :=
   Nat.dvd_antisymm
     (dvd_gcd (gcd_dvd_right m n) (gcd_dvd_left m n))
     (dvd_gcd (gcd_dvd_right n m) (gcd_dvd_left n m))
+instance : Std.Commutative gcd := ⟨gcd_comm⟩
 
 theorem gcd_eq_left_iff_dvd : m ∣ n ↔ gcd m n = m :=
   ⟨fun h => by rw [gcd_rec, mod_eq_zero_of_dvd h, gcd_zero_left],

src/Init/Data/Nat/Lcm.lean

@@ -14,6 +14,7 @@ def lcm (m n : Nat) : Nat := m * n / gcd m n
 
 theorem lcm_comm (m n : Nat) : lcm m n = lcm n m := by
   rw [lcm, lcm, Nat.mul_comm n m, gcd_comm n m]
+instance : Std.Commutative lcm := ⟨lcm_comm⟩
 
 @[simp] theorem lcm_zero_left (m : Nat) : lcm 0 m = 0 := by simp [lcm]
 
@@ -22,11 +23,15 @@ theorem lcm_comm (m n : Nat) : lcm m n = lcm n m := by
 @[simp] theorem lcm_one_left (m : Nat) : lcm 1 m = m := by simp [lcm]
 
 @[simp] theorem lcm_one_right (m : Nat) : lcm m 1 = m := by simp [lcm]
+instance : Std.LawfulIdentity lcm 1 where
+  left_id := lcm_one_left
+  right_id := lcm_one_right
 
 @[simp] theorem lcm_self (m : Nat) : lcm m m = m := by
   match eq_zero_or_pos m with
   | .inl h => rw [h, lcm_zero_left]
   | .inr h => simp [lcm, Nat.mul_div_cancel _ h]
+instance : Std.IdempotentOp lcm := ⟨lcm_self⟩
 
 theorem dvd_lcm_left (m n : Nat) : m ∣ lcm m n :=
   ⟨n / gcd m n, by rw [← Nat.mul_div_assoc m (Nat.gcd_dvd_right m n)]; rfl⟩
@@ -54,6 +59,7 @@ Nat.dvd_antisymm
     (Nat.dvd_trans (dvd_lcm_left m n) (dvd_lcm_left (lcm m n) k))
     (lcm_dvd (Nat.dvd_trans (dvd_lcm_right m n) (dvd_lcm_left (lcm m n) k))
       (dvd_lcm_right (lcm m n) k)))
+instance : Std.Associative lcm := ⟨lcm_assoc⟩
 
 theorem lcm_ne_zero (hm : m ≠ 0) (hn : n ≠ 0) : lcm m n ≠ 0 := by
   intro h

src/Init/Data/Nat/Lemmas.lean

@@ -200,6 +200,7 @@ theorem succ_min_succ (x y) : min (succ x) (succ y) = succ (min x y) := by
   | inr h => rw [Nat.min_eq_right h, Nat.min_eq_right (Nat.succ_le_succ h)]
 
 @[simp] protected theorem min_self (a : Nat) : min a a = a := Nat.min_eq_left (Nat.le_refl _)
+instance : Std.IdempotentOp (α := Nat) min := ⟨Nat.min_self⟩
 
 @[simp] protected theorem zero_min (a) : min 0 a = 0 := Nat.min_eq_left (Nat.zero_le _)
 
@@ -210,6 +211,7 @@ protected theorem min_assoc : ∀ (a b c : Nat), min (min a b) c = min a (min b
   | _, 0, _ => by rw [Nat.zero_min, Nat.min_zero, Nat.zero_min]
   | _, _, 0 => by rw [Nat.min_zero, Nat.min_zero, Nat.min_zero]
   | _+1, _+1, _+1 => by simp only [Nat.succ_min_succ]; exact congrArg succ <| Nat.min_assoc ..
+instance : Std.Associative (α := Nat) min := ⟨Nat.min_assoc⟩
 
 protected theorem sub_sub_eq_min : ∀ (a b : Nat), a - (a - b) = min a b
   | 0, _ => by rw [Nat.zero_sub, Nat.zero_min]
@@ -249,16 +251,21 @@ protected theorem max_lt {a b c : Nat} : max a b < c ↔ a < c ∧ b < c := by
   rw [← Nat.succ_le, ← Nat.succ_max_succ a b]; exact Nat.max_le
 
 @[simp] protected theorem max_self (a : Nat) : max a a = a := Nat.max_eq_right (Nat.le_refl _)
+instance : Std.IdempotentOp (α := Nat) max := ⟨Nat.max_self⟩
 
 @[simp] protected theorem zero_max (a) : max 0 a = a := Nat.max_eq_right (Nat.zero_le _)
 
 @[simp] protected theorem max_zero (a) : max a 0 = a := Nat.max_eq_left (Nat.zero_le _)
+instance : Std.LawfulIdentity (α := Nat) max 0 where
+  left_id := Nat.zero_max
+  right_id := Nat.max_zero
 
 protected theorem max_assoc : ∀ (a b c : Nat), max (max a b) c = max a (max b c)
   | 0, _, _ => by rw [Nat.zero_max, Nat.zero_max]
   | _, 0, _ => by rw [Nat.zero_max, Nat.max_zero]
   | _, _, 0 => by rw [Nat.max_zero, Nat.max_zero]
   | _+1, _+1, _+1 => by simp only [Nat.succ_max_succ]; exact congrArg succ <| Nat.max_assoc ..
+instance : Std.Associative (α := Nat) max := ⟨Nat.max_assoc⟩
 
 protected theorem sub_add_eq_max (a b : Nat) : a - b + b = max a b := by
   match Nat.le_total a b with

src/Init/Data/Nat/MinMax.lean

@@ -17,6 +17,7 @@ protected theorem min_comm (a b : Nat) : min a b = min b a := by
   | .inl h => simp [Nat.min_def, h, Nat.le_of_lt, Nat.not_le_of_lt]
   | .inr (.inl h) => simp [Nat.min_def, h]
   | .inr (.inr h) => simp [Nat.min_def, h, Nat.le_of_lt, Nat.not_le_of_lt]
+instance : Std.Commutative (α := Nat) min := ⟨Nat.min_comm⟩
 
 protected theorem min_le_right (a b : Nat) : min a b ≤ b := by
   by_cases (a <= b) <;> simp [Nat.min_def, *]
@@ -47,6 +48,7 @@ protected theorem max_comm (a b : Nat) : max a b = max b a := by
   by_cases h₁ : a ≤ b <;> by_cases h₂ : b ≤ a <;> simp [h₁, h₂]
   · exact Nat.le_antisymm h₂ h₁
   · cases not_or_intro h₁ h₂ <| Nat.le_total ..
+instance : Std.Commutative (α := Nat) max := ⟨Nat.max_comm⟩
 
 protected theorem le_max_left ( a b : Nat) : a ≤ max a b := by
   by_cases (a <= b) <;> simp [Nat.max_def, *]

src/Init/Data/String/Extra.lean

@@ -132,13 +132,17 @@ theorem Iterator.sizeOf_next_lt_of_hasNext (i : String.Iterator) (h : i.hasNext)
   cases i; rename_i s pos; simp [Iterator.next, Iterator.sizeOf_eq]; simp [Iterator.hasNext] at h
   exact Nat.sub_lt_sub_left h (String.lt_next s pos)
 
-macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply String.Iterator.sizeOf_next_lt_of_hasNext; assumption)
+macro_rules
+| `(tactic| decreasing_trivial) =>
+  `(tactic| with_reducible apply String.Iterator.sizeOf_next_lt_of_hasNext; assumption)
 
 theorem Iterator.sizeOf_next_lt_of_atEnd (i : String.Iterator) (h : ¬ i.atEnd = true) : sizeOf i.next < sizeOf i :=
   have h : i.hasNext := decide_eq_true <| Nat.gt_of_not_le <| mt decide_eq_true h
   sizeOf_next_lt_of_hasNext i h
 
-macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply String.Iterator.sizeOf_next_lt_of_atEnd; assumption)
+macro_rules
+| `(tactic| decreasing_trivial) =>
+  `(tactic| with_reducible apply String.Iterator.sizeOf_next_lt_of_atEnd; assumption)
 
 namespace Iterator
 

src/Init/Meta.lean

@@ -1057,6 +1057,7 @@ where
     else
       Syntax.mkCApp (Name.mkStr2 "Array" ("mkArray" ++ toString xs.size)) args
   termination_by xs.size - i
+  decreasing_by decreasing_trivial_pre_omega
 
 instance [Quote α `term] : Quote (Array α) `term where
   quote := quoteArray

src/Init/Notation.lean

@@ -296,7 +296,7 @@ macro_rules | `($x - $y)   => `(binop% HSub.hSub $x $y)
 macro_rules | `($x * $y)   => `(binop% HMul.hMul $x $y)
 macro_rules | `($x / $y)   => `(binop% HDiv.hDiv $x $y)
 macro_rules | `($x % $y)   => `(binop% HMod.hMod $x $y)
--- exponentiation should be considered a right action (#2220)
+-- exponentiation should be considered a right action (#2854)
 macro_rules | `($x ^ $y)   => `(rightact% HPow.hPow $x $y)
 macro_rules | `($x ++ $y)  => `(binop% HAppend.hAppend $x $y)
 macro_rules | `(- $x)      => `(unop% Neg.neg $x)
@@ -492,9 +492,12 @@ The attribute `@[deprecated]` on a declaration indicates that the declaration
 is discouraged for use in new code, and/or should be migrated away from in
 existing code. It may be removed in a future version of the library.
 
-`@[deprecated myBetterDef]` means that `myBetterDef` is the suggested replacement.
+* `@[deprecated myBetterDef]` means that `myBetterDef` is the suggested replacement.
+* `@[deprecated myBetterDef "use myBetterDef instead"]` allows customizing the deprecation message.
+* `@[deprecated (since := "2024-04-21")]` records when the deprecation was first applied.
 -/
-syntax (name := deprecated) "deprecated" (ppSpace ident)? : attr
+syntax (name := deprecated) "deprecated" (ppSpace ident)? (ppSpace str)?
+    (" (" &"since" " := " str ")")? : attr
 
 /--
 The `@[coe]` attribute on a function (which should also appear in a

src/Init/Prelude.lean

@@ -4335,8 +4335,13 @@ def addMacroScope (mainModule : Name) (n : Name) (scp : MacroScope) : Name :=
     Name.mkNum (Name.mkStr (Name.appendCore (Name.mkStr n "_@") mainModule) "_hyg") scp
 
 /--
-Append two names that may have macro scopes. The macro scopes in `b` are always erased.
-If `a` has macro scopes, then they are propagated to the result of `append a b`.
+Appends two names `a` and `b`, propagating macro scopes from `a` or `b`, if any, to the result.
+Panics if both `a` and `b` have macro scopes.
+
+This function is used for the `Append Name` instance.
+
+See also `Lean.Name.appendCore`, which appends names without any consideration for macro scopes.
+Also consider `Lean.Name.eraseMacroScopes` to erase macro scopes before appending, if appropriate.
 -/
 def Name.append (a b : Name) : Name :=
   match a.hasMacroScopes, b.hasMacroScopes with
@@ -4367,7 +4372,7 @@ def defaultMaxRecDepth := 512
 
 /-- The message to display on stack overflow. -/
 def maxRecDepthErrorMessage : String :=
-  "maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)"
+  "maximum recursion depth has been reached\nuse `set_option maxRecDepth <num>` to increase limit\nuse `set_option diagnostics true` to get diagnostic information"
 
 namespace Syntax
 

src/Init/SimpLemmas.lean

@@ -103,18 +103,26 @@ end SimprocHelperLemmas
 
 @[simp] theorem and_true (p : Prop) : (p ∧ True) = p := propext ⟨(·.1), (⟨·, trivial⟩)⟩
 @[simp] theorem true_and (p : Prop) : (True ∧ p) = p := propext ⟨(·.2), (⟨trivial, ·⟩)⟩
+instance : Std.LawfulIdentity And True where
+  left_id := true_and
+  right_id := and_true
 @[simp] theorem and_false (p : Prop) : (p ∧ False) = False := eq_false (·.2)
 @[simp] theorem false_and (p : Prop) : (False ∧ p) = False := eq_false (·.1)
 @[simp] theorem and_self (p : Prop) : (p ∧ p) = p := propext ⟨(·.left), fun h => ⟨h, h⟩⟩
+instance : Std.IdempotentOp And := ⟨and_self⟩
 @[simp] theorem and_not_self : ¬(a ∧ ¬a) | ⟨ha, hn⟩ => absurd ha hn
 @[simp] theorem not_and_self : ¬(¬a ∧ a) := and_not_self ∘ And.symm
 @[simp] theorem and_imp : (a ∧ b → c) ↔ (a → b → c) := ⟨fun h ha hb => h ⟨ha, hb⟩, fun h ⟨ha, hb⟩ => h ha hb⟩
 @[simp] theorem not_and : ¬(a ∧ b) ↔ (a → ¬b) := and_imp
 @[simp] theorem or_self (p : Prop) : (p ∨ p) = p := propext ⟨fun | .inl h | .inr h => h, .inl⟩
+instance : Std.IdempotentOp Or := ⟨or_self⟩
 @[simp] theorem or_true (p : Prop) : (p ∨ True) = True := eq_true (.inr trivial)
 @[simp] theorem true_or (p : Prop) : (True ∨ p) = True := eq_true (.inl trivial)
 @[simp] theorem or_false (p : Prop) : (p ∨ False) = p := propext ⟨fun (.inl h) => h, .inl⟩
 @[simp] theorem false_or (p : Prop) : (False ∨ p) = p := propext ⟨fun (.inr h) => h, .inr⟩
+instance : Std.LawfulIdentity Or False where
+  left_id := false_or
+  right_id := or_false
 @[simp] theorem iff_self (p : Prop) : (p ↔ p) = True := eq_true .rfl
 @[simp] theorem iff_true (p : Prop) : (p ↔ True) = p := propext ⟨(·.2 trivial), fun h => ⟨fun _ => trivial, fun _ => h⟩⟩
 @[simp] theorem true_iff (p : Prop) : (True ↔ p) = p := propext ⟨(·.1 trivial), fun h => ⟨fun _ => h, fun _ => trivial⟩⟩
@@ -140,6 +148,7 @@ theorem and_congr_left (h : c → (a ↔ b)) : a ∧ c ↔ b ∧ c :=
 theorem and_assoc : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) :=
   Iff.intro (fun ⟨⟨ha, hb⟩, hc⟩ => ⟨ha, hb, hc⟩)
             (fun ⟨ha, hb, hc⟩ => ⟨⟨ha, hb⟩, hc⟩)
+instance : Std.Associative And := ⟨fun _ _ _ => propext and_assoc⟩
 
 @[simp] theorem and_self_left  : a ∧ (a ∧ b) ↔ a ∧ b := by rw [←propext and_assoc, and_self]
 @[simp] theorem and_self_right : (a ∧ b) ∧ b ↔ a ∧ b := by rw [ propext and_assoc, and_self]
@@ -167,6 +176,7 @@ theorem Or.imp_right (f : b → c) : a ∨ b → a ∨ c := .imp id f
 theorem or_assoc : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) :=
   Iff.intro (.rec (.imp_right .inl) (.inr ∘ .inr))
             (.rec (.inl ∘ .inl) (.imp_left .inr))
+instance : Std.Associative Or := ⟨fun _ _ _ => propext or_assoc⟩
 
 @[simp] theorem or_self_left  : a ∨ (a ∨ b) ↔ a ∨ b := by rw [←propext or_assoc, or_self]
 @[simp] theorem or_self_right : (a ∨ b) ∨ b ↔ a ∨ b := by rw [ propext or_assoc, or_self]
@@ -187,8 +197,12 @@ theorem or_iff_left_of_imp  (hb : b → a) : (a ∨ b) ↔ a  := Iff.intro (Or.r
 @[simp] theorem Bool.or_false (b : Bool) : (b || false) = b  := by cases b <;> rfl
 @[simp] theorem Bool.or_true (b : Bool) : (b || true) = true := by cases b <;> rfl
 @[simp] theorem Bool.false_or (b : Bool) : (false || b) = b  := by cases b <;> rfl
+instance : Std.LawfulIdentity (· || ·) false where
+  left_id := Bool.false_or
+  right_id := Bool.or_false
 @[simp] theorem Bool.true_or (b : Bool) : (true || b) = true := by cases b <;> rfl
 @[simp] theorem Bool.or_self (b : Bool) : (b || b) = b       := by cases b <;> rfl
+instance : Std.IdempotentOp (· || ·) := ⟨Bool.or_self⟩
 @[simp] theorem Bool.or_eq_true (a b : Bool) : ((a || b) = true) = (a = true ∨ b = true) := by
   cases a <;> cases b <;> decide
 
@@ -196,14 +210,20 @@ theorem or_iff_left_of_imp  (hb : b → a) : (a ∨ b) ↔ a  := Iff.intro (Or.r
 @[simp] theorem Bool.and_true (b : Bool) : (b && true) = b       := by cases b <;> rfl
 @[simp] theorem Bool.false_and (b : Bool) : (false && b) = false := by cases b <;> rfl
 @[simp] theorem Bool.true_and (b : Bool) : (true && b) = b       := by cases b <;> rfl
+instance : Std.LawfulIdentity (· && ·) true where
+  left_id := Bool.true_and
+  right_id := Bool.and_true
 @[simp] theorem Bool.and_self (b : Bool) : (b && b) = b          := by cases b <;> rfl
+instance : Std.IdempotentOp (· && ·) := ⟨Bool.and_self⟩
 @[simp] theorem Bool.and_eq_true (a b : Bool) : ((a && b) = true) = (a = true ∧ b = true) := by
   cases a <;> cases b <;> decide
 
 theorem Bool.and_assoc (a b c : Bool) : (a && b && c) = (a && (b && c)) := by
   cases a <;> cases b <;> cases c <;> decide
+instance : Std.Associative (· && ·) := ⟨Bool.and_assoc⟩
 theorem Bool.or_assoc (a b c : Bool) : (a || b || c) = (a || (b || c)) := by
   cases a <;> cases b <;> cases c <;> decide
+instance : Std.Associative (· || ·) := ⟨Bool.or_assoc⟩
 
 @[simp] theorem Bool.not_not (b : Bool) : (!!b) = b := by cases b <;> rfl
 @[simp] theorem Bool.not_true  : (!true) = false := by decide

src/Init/Tactics.lean

@@ -1542,7 +1542,7 @@ macro "get_elem_tactic" : tactic =>
 
 /--
 Searches environment for definitions or theorems that can be substituted in
-for `exact?% to solve the goal.
+for `exact?%` to solve the goal.
  -/
 syntax (name := Lean.Parser.Syntax.exact?) "exact?%" : term
 

src/Init/WFTactics.lean

@@ -25,9 +25,16 @@ syntax "decreasing_trivial" : tactic
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| (simp (config := { arith := true, failIfUnchanged := false })) <;> done)
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| omega)
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| assumption)
-macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.sub_succ_lt_self; assumption) -- a - (i+1) < a - i if i < a
-macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.pred_lt'; assumption) -- i-1 < i if j < i
-macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.pred_lt; assumption)  -- i-1 < i if i ≠ 0
+
+/--
+Variant of `decreasing_trivial` that does not use `omega`, intended to be used in core modules
+before `omega` is available.
+-/
+syntax "decreasing_trivial_pre_omega" : tactic
+macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.sub_succ_lt_self; assumption) -- a - (i+1) < a - i if i < a
+macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.pred_lt'; assumption) -- i-1 < i if j < i
+macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.pred_lt; assumption)  -- i-1 < i if i ≠ 0
+
 
 /-- Constructs a proof of decreasing along a well founded relation, by applying
 lexicographic order lemmas and using `ts` to solve the base case. If it fails,

src/Lean/Attributes.lean

@@ -183,7 +183,6 @@ structure ParametricAttribute (α : Type) where
   deriving Inhabited
 
 structure ParametricAttributeImpl (α : Type) extends AttributeImplCore where
-  /-- This is used as the target for go-to-definition queries for simple attributes -/
   getParam : Name → Syntax → AttrM α
   afterSet : Name → α → AttrM Unit := fun _ _ _ => pure ()
   afterImport : Array (Array (Name × α)) → ImportM Unit := fun _ => pure ()

src/Lean/Compiler/ExternAttr.lean

@@ -66,12 +66,13 @@ builtin_initialize externAttr : ParametricAttribute ExternAttrData ←
     descr := "builtin and foreign functions"
     getParam := fun _ stx => syntaxToExternAttrData stx
     afterSet := fun declName _ => do
-      let mut env ← getEnv
-      if env.isProjectionFn declName || env.isConstructor declName then do
-        env ← ofExcept <| addExtern env declName
+      let env ← getEnv
+      if env.isProjectionFn declName || env.isConstructor declName then
+        if let some (.thmInfo ..) := env.find? declName then
+          -- We should not mark theorems as extern
+          return ()
+        let env ← ofExcept <| addExtern env declName
         setEnv env
-      else
-        pure ()
   }
 
 @[export lean_get_extern_attr_data]

src/Lean/Compiler/IR/RC.lean

@@ -9,9 +9,10 @@ import Lean.Compiler.IR.CompilerM
 import Lean.Compiler.IR.LiveVars
 
 namespace Lean.IR.ExplicitRC
-/-! Insert explicit RC instructions. So, it assumes the input code does not contain `inc` nor `dec` instructions.
-   This transformation is applied before lower level optimizations
-   that introduce the instructions `release` and `set`
+/-!
+Insert explicit RC instructions. So, it assumes the input code does not contain `inc` nor `dec` instructions.
+This transformation is applied before lower level optimizations
+that introduce the instructions `release` and `set`
 -/
 
 structure VarInfo where

src/Lean/Compiler/IR/ResetReuse.lean

@@ -9,21 +9,24 @@ import Lean.Compiler.IR.LiveVars
 import Lean.Compiler.IR.Format
 
 namespace Lean.IR.ResetReuse
-/-! Remark: the insertResetReuse transformation is applied before we have
-   inserted `inc/dec` instructions, and performed lower level optimizations
-   that introduce the instructions `release` and `set`. -/
+/-!
+Remark: the insertResetReuse transformation is applied before we have
+inserted `inc/dec` instructions, and performed lower level optimizations
+that introduce the instructions `release` and `set`.
+-/
 
-/-! Remark: the functions `S`, `D` and `R` defined here implement the
-  corresponding functions in the paper "Counting Immutable Beans"
+/-!
+Remark: the functions `S`, `D` and `R` defined here implement the
+corresponding functions in the paper "Counting Immutable Beans"
 
-  Here are the main differences:
-  - We use the State monad to manage the generation of fresh variable names.
-  - Support for join points, and `uset` and `sset` instructions for unboxed data.
-  - `D` uses the auxiliary function `Dmain`.
-  - `Dmain` returns a pair `(b, found)` to avoid quadratic behavior when checking
-    the last occurrence of the variable `x`.
-  - Because we have join points in the actual implementation, a variable may be live even if it
-    does not occur in a function body. See example at `livevars.lean`.
+Here are the main differences:
+- We use the State monad to manage the generation of fresh variable names.
+- Support for join points, and `uset` and `sset` instructions for unboxed data.
+- `D` uses the auxiliary function `Dmain`.
+- `Dmain` returns a pair `(b, found)` to avoid quadratic behavior when checking
+  the last occurrence of the variable `x`.
+- Because we have join points in the actual implementation, a variable may be live even if it
+  does not occur in a function body. See example at `livevars.lean`.
 -/
 
 private def mayReuse (c₁ c₂ : CtorInfo) : Bool :=
@@ -33,39 +36,68 @@ private def mayReuse (c₁ c₂ : CtorInfo) : Bool :=
      because it produces counterintuitive behavior. -/
   c₁.name.getPrefix == c₂.name.getPrefix
 
+/--
+Replace `ctor` applications with `reuse` applications if compatible.
+`w` contains the "memory cell" being reused.
+-/
 private partial def S (w : VarId) (c : CtorInfo) : FnBody → FnBody
-  | FnBody.vdecl x t v@(Expr.ctor c' ys) b   =>
+  | .vdecl x t v@(.ctor c' ys) b   =>
     if mayReuse c c' then
       let updtCidx := c.cidx != c'.cidx
-      FnBody.vdecl x t (Expr.reuse w c' updtCidx ys) b
+      .vdecl x t (.reuse w c' updtCidx ys) b
     else
-      FnBody.vdecl x t v (S w c b)
-  | FnBody.jdecl j ys v b   =>
+      .vdecl x t v (S w c b)
+  | .jdecl j ys v b   =>
     let v' := S w c v
-    if v == v' then FnBody.jdecl j ys v (S w c b)
-    else FnBody.jdecl j ys v' b
-  | FnBody.case tid x xType alts    => FnBody.case tid x xType <| alts.map fun alt => alt.modifyBody (S w c)
+    if v == v' then
+      .jdecl j ys v (S w c b)
+    else
+      .jdecl j ys v' b
+  | .case tid x xType alts =>
+    .case tid x xType <| alts.map fun alt => alt.modifyBody (S w c)
   | b =>
-    if b.isTerminal then b
+    if b.isTerminal then
+      b
     else let
       (instr, b) := b.split
       instr.setBody (S w c b)
 
+structure Context where
+  lctx      : LocalContext := {}
+  /--
+  Contains all variables in `cases` statements in the current path.
+  We use this information to prevent double-reset in code such as
+  ```
+  case x_i : obj of
+  Prod.mk →
+    case x_i : obj of
+    Prod.mk →
+    ...
+  ```
+  -/
+  casesVars : PHashSet VarId := {}
+
 /-- We use `Context` to track join points in scope. -/
-abbrev M := ReaderT LocalContext (StateT Index Id)
+abbrev M := ReaderT Context (StateT Index Id)
 
 private def mkFresh : M VarId := do
-  let idx ← getModify (fun n => n + 1)
-  pure { idx := idx }
+  let idx ← getModify fun n => n + 1
+  return { idx := idx }
 
+/--
+Helper function for applying `S`. We only introduce a `reset` if we managed
+to replace a `ctor` withe `reuse` in `b`.
+-/
 private def tryS (x : VarId) (c : CtorInfo) (b : FnBody) : M FnBody := do
   let w ← mkFresh
   let b' := S w c b
-  if b == b' then pure b
-  else pure $ FnBody.vdecl w IRType.object (Expr.reset c.size x) b'
+  if b == b' then
+    return b
+  else
+    return .vdecl w IRType.object (.reset c.size x) b'
 
 private def Dfinalize (x : VarId) (c : CtorInfo) : FnBody × Bool → M FnBody
-  | (b, true)  => pure b
+  | (b, true)  => return b
   | (b, false) => tryS x c b
 
 private def argsContainsVar (ys : Array Arg) (x : VarId) : Bool :=
@@ -75,75 +107,85 @@ private def argsContainsVar (ys : Array Arg) (x : VarId) : Bool :=
 
 private def isCtorUsing (b : FnBody) (x : VarId) : Bool :=
   match b with
-  | (FnBody.vdecl _ _ (Expr.ctor _ ys) _) => argsContainsVar ys x
+  | .vdecl _ _ (.ctor _ ys) _ => argsContainsVar ys x
   | _ => false
 
-/-- Given `Dmain b`, the resulting pair `(new_b, flag)` contains the new body `new_b`,
-   and `flag == true` if `x` is live in `b`.
+/--
+Given `Dmain b`, the resulting pair `(new_b, flag)` contains the new body `new_b`,
+and `flag == true` if `x` is live in `b`.
 
-   Note that, in the function `D` defined in the paper, for each `let x := e; F`,
-   `D` checks whether `x` is live in `F` or not. This is great for clarity but it
-   is expensive: `O(n^2)` where `n` is the size of the function body. -/
-private partial def Dmain (x : VarId) (c : CtorInfo) : FnBody → M (FnBody × Bool)
-  | e@(FnBody.case tid y yType alts) => do
-    let ctx ← read
-    if e.hasLiveVar ctx x then do
+Note that, in the function `D` defined in the paper, for each `let x := e; F`,
+`D` checks whether `x` is live in `F` or not. This is great for clarity but it
+is expensive: `O(n^2)` where `n` is the size of the function body. -/
+private partial def Dmain (x : VarId) (c : CtorInfo) (e : FnBody) : M (FnBody × Bool) := do
+  match e with
+  | .case tid y yType alts =>
+    if e.hasLiveVar (← read).lctx x then
       /- If `x` is live in `e`, we recursively process each branch. -/
       let alts ← alts.mapM fun alt => alt.mmodifyBody fun b => Dmain x c b >>= Dfinalize x c
-      pure (FnBody.case tid y yType alts, true)
-    else pure (e, false)
-  | FnBody.jdecl j ys v b   => do
-    let (b, found) ← withReader (fun ctx => ctx.addJP j ys v) (Dmain x c b)
+      return (.case tid y yType alts, true)
+    else
+      return (e, false)
+  | .jdecl j ys v b =>
+    let (b, found) ← withReader (fun ctx => { ctx with lctx := ctx.lctx.addJP j ys v }) (Dmain x c b)
     let (v, _ /- found' -/) ← Dmain x c v
     /- If `found' == true`, then `Dmain b` must also have returned `(b, true)` since
        we assume the IR does not have dead join points. So, if `x` is live in `j` (i.e., `v`),
        then it must also live in `b` since `j` is reachable from `b` with a `jmp`.
        On the other hand, `x` may be live in `b` but dead in `j` (i.e., `v`). -/
-    pure (FnBody.jdecl j ys v b, found)
-  | e => do
-    let ctx ← read
+    return (.jdecl j ys v b, found)
+  | e =>
     if e.isTerminal then
-      pure (e, e.hasLiveVar ctx x)
+      return (e, e.hasLiveVar (← read).lctx x)
     else do
       let (instr, b) := e.split
       if isCtorUsing instr x then
         /- If the scrutinee `x` (the one that is providing memory) is being
            stored in a constructor, then reuse will probably not be able to reuse memory at runtime.
            It may work only if the new cell is consumed, but we ignore this case. -/
-        pure (e, true)
+        return (e, true)
       else
         let (b, found) ← Dmain x c b
         /- Remark: it is fine to use `hasFreeVar` instead of `hasLiveVar`
-           since `instr` is not a `FnBody.jmp` (it is not a terminal) nor it is a `FnBody.jdecl`. -/
+           since `instr` is not a `FnBody.jmp` (it is not a terminal) nor
+           it is a `FnBody.jdecl`. -/
         if found || !instr.hasFreeVar x then
-          pure (instr.setBody b, found)
+          return (instr.setBody b, found)
         else
           let b ← tryS x c b
-          pure (instr.setBody b, true)
+          return (instr.setBody b, true)
 
 private def D (x : VarId) (c : CtorInfo) (b : FnBody) : M FnBody :=
   Dmain x c b >>= Dfinalize x c
 
-partial def R : FnBody → M FnBody
-  | FnBody.case tid x xType alts   => do
+partial def R (e : FnBody) : M FnBody := do
+  match e with
+  | .case tid x xType alts =>
+    let alreadyFound := (← read).casesVars.contains x
+    withReader (fun ctx => { ctx with casesVars := ctx.casesVars.insert x }) do
       let alts ← alts.mapM fun alt => do
         let alt ← alt.mmodifyBody R
         match alt with
-        | Alt.ctor c b =>
-          if c.isScalar then pure alt
-          else Alt.ctor c <$> D x c b
-        | _            => pure alt
-      pure $ FnBody.case tid x xType alts
-  | FnBody.jdecl j ys v b   => do
+        | .ctor c b =>
+          if c.isScalar || alreadyFound then
+            -- If `alreadyFound`, then we don't try to reuse memory cell to avoid
+            -- double reset.
+            return alt
+          else
+            .ctor c <$> D x c b
+        | _ => return alt
+      return .case tid x xType alts
+  | .jdecl j ys v b =>
     let v ← R v
-    let b ← withReader (fun ctx => ctx.addJP j ys v) (R b)
-    pure $ FnBody.jdecl j ys v b
-  | e => do
-    if e.isTerminal then pure e
-    else do
+    let b ← withReader (fun ctx => { ctx with lctx := ctx.lctx.addJP j ys v }) (R b)
+    return .jdecl j ys v b
+  | e =>
+    if e.isTerminal then
+      return e
+    else
       let (instr, b) := e.split
       let b ← R b
-      pure (instr.setBody b)
+      return instr.setBody b
 
 end ResetReuse
 
@@ -151,7 +193,7 @@ open ResetReuse
 
 def Decl.insertResetReuse (d : Decl) : Decl :=
   match d with
-  | .fdecl (body := b) ..=>
+  | .fdecl (body := b) .. =>
     let nextIndex := d.maxIndex + 1
     let bNew      := (R b {}).run' nextIndex
     d.updateBody! bNew

src/Lean/CoreM.lean

@@ -13,13 +13,25 @@ import Lean.Elab.InfoTree.Types
 import Lean.MonadEnv
 
 namespace Lean
-namespace Core
+register_builtin_option diagnostics : Bool := {
+  defValue := false
+  group    := "diagnostics"
+  descr    := "collect diagnostic information"
+}
+
+register_builtin_option diagnostics.threshold : Nat := {
+  defValue := 20
+  group    := "diagnostics"
+  descr    := "only diagnostic counters above this threshold are reported by the definitional equality"
+}
 
 register_builtin_option maxHeartbeats : Nat := {
   defValue := 200000
   descr := "maximum amount of heartbeats per command. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit"
 }
 
+namespace Core
+
 builtin_initialize registerTraceClass `Kernel
 
 def getMaxHeartbeats (opts : Options) : Nat :=
@@ -72,6 +84,11 @@ structure Context where
   Recall that runtime exceptions are `maxRecDepth` or `maxHeartbeats`.
   -/
   catchRuntimeEx : Bool := false
+  /--
+  If `diag := true`, different parts of the system collect diagnostics.
+  Use the `set_option diag true` to set it to true.
+  -/
+  diag           : Bool := false
   deriving Nonempty
 
 /-- CoreM is a monad for manipulating the Lean environment.
@@ -104,7 +121,15 @@ instance : MonadOptions CoreM where
   getOptions := return (← read).options
 
 instance : MonadWithOptions CoreM where
-  withOptions f x := withReader (fun ctx => { ctx with options := f ctx.options }) x
+  withOptions f x :=
+    withReader
+      (fun ctx =>
+        let options := f ctx.options
+        { ctx with
+          options
+          diag := diagnostics.get options
+          maxRecDepth := maxRecDepth.get options })
+      x
 
 instance : AddMessageContext CoreM where
   addMessageContext := addMessageContextPartial
@@ -206,7 +231,7 @@ def mkFreshUserName (n : Name) : CoreM Name :=
 instance [MetaEval α] : MetaEval (CoreM α) where
   eval env opts x _ := do
     let x : CoreM α := do try x finally printTraces
-    let (a, s) ← x.toIO { maxRecDepth := maxRecDepth.get opts, options := opts, fileName := "<CoreM>", fileMap := default } { env := env }
+    let (a, s) ← (withOptions (fun _ => opts) x).toIO { fileName := "<CoreM>", fileMap := default } { env := env }
     MetaEval.eval s.env opts a (hideUnit := true)
 
 -- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`
@@ -219,7 +244,7 @@ protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m
     throw <| Exception.error .missing "elaboration interrupted"
 
 def throwMaxHeartbeat (moduleName : Name) (optionName : Name) (max : Nat) : CoreM Unit := do
-  let msg := s!"(deterministic) timeout at '{moduleName}', maximum number of heartbeats ({max/1000}) has been reached (use 'set_option {optionName} <num>' to set the limit)"
+  let msg := s!"(deterministic) timeout at `{moduleName}`, maximum number of heartbeats ({max/1000}) has been reached\nuse `set_option {optionName} <num>` to set the limit\nuse `set_option {diagnostics.name} true` to get diagnostic information"
   throw <| Exception.error (← getRef) (MessageData.ofFormat (Std.Format.text msg))
 
 def checkMaxHeartbeatsCore (moduleName : String) (optionName : Name) (max : Nat) : CoreM Unit := do
@@ -372,9 +397,16 @@ def addAndCompile (decl : Declaration) : CoreM Unit := do
   addDecl decl;
   compileDecl decl
 
+def getDiag (opts : Options) : Bool :=
+  diagnostics.get opts
+
+/-- Return `true` if diagnostic information collection is enabled. -/
+def isDiagnosticsEnabled : CoreM Bool :=
+  return (← read).diag
+
 def ImportM.runCoreM (x : CoreM α) : ImportM α := do
   let ctx ← read
-  let (a, _) ← x.toIO { options := ctx.opts, fileName := "<ImportM>", fileMap := default } { env := ctx.env }
+  let (a, _) ← (withOptions (fun _ => ctx.opts) x).toIO { fileName := "<ImportM>", fileMap := default } { env := ctx.env }
   return a
 
 /-- Return `true` if the exception was generated by one our resource limits. -/

src/Lean/Data/HashMap.lean

@@ -92,6 +92,7 @@ def moveEntries [Hashable α] (i : Nat) (source : Array (AssocList α β)) (targ
      moveEntries (i+1) source target
   else target
 termination_by source.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β :=
   let bucketsNew : HashMapBucket α β := ⟨

src/Lean/Data/HashSet.lean

@@ -84,6 +84,7 @@ def moveEntries [Hashable α] (i : Nat) (source : Array (List α)) (target : Has
   else
     target
 termination_by source.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def expand [Hashable α] (size : Nat) (buckets : HashSetBucket α) : HashSetImp α :=
   let bucketsNew : HashSetBucket α := ⟨

src/Lean/Declaration.lean

@@ -135,6 +135,11 @@ structure TheoremVal extends ConstantVal where
   all : List Name := [name]
   deriving Inhabited, BEq
 
+@[export lean_mk_theorem_val]
+def mkTheoremValEx (name : Name) (levelParams : List Name) (type : Expr) (value : Expr) (all : List Name) : TheoremVal := {
+  name, levelParams, type, value, all
+}
+
 /-- Value for an opaque constant declaration `opaque x : t := e` -/
 structure OpaqueVal extends ConstantVal where
   value : Expr

src/Lean/Elab/BuiltinNotation.lean

@@ -409,6 +409,8 @@ private def withLocalIdentFor (stx : Term) (e : Expr) (k : Term → TermElabM Ex
          let h ← elabTerm hStx none
          let hType ← inferType h
          let hTypeAbst ← kabstract hType lhs
+         unless hTypeAbst.hasLooseBVars do
+           throwError "invalid `▸` notation, the equality{indentExpr heq}\nhas type {indentExpr heqType}\nbut its left hand side is not mentioned in the type{indentExpr hType}"
          let motive ← mkMotive lhs hTypeAbst
          unless (← isTypeCorrect motive) do
            throwError "invalid `▸` notation, failed to compute motive for the substitution"

src/Lean/Elab/BuiltinTerm.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Meta.Diagnostics
 import Lean.Elab.Open
 import Lean.Elab.SetOption
 import Lean.Elab.Eval
@@ -313,8 +314,12 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
 
 @[builtin_term_elab «set_option»] def elabSetOption : TermElab := fun stx expectedType? => do
   let options ← Elab.elabSetOption stx[1] stx[3]
-  withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options }) do
-    elabTerm stx[5] expectedType?
+  withOptions (fun _ => options) do
+    try
+      elabTerm stx[5] expectedType?
+    finally
+      if stx[1].getId == `diagnostics then
+        reportDiag
 
 @[builtin_term_elab withAnnotateTerm] def elabWithAnnotateTerm : TermElab := fun stx expectedType? => do
   match stx with

src/Lean/Elab/Command.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Gabriel Ebner
 -/
 prelude
+import Lean.Meta.Diagnostics
 import Lean.Elab.Binders
 import Lean.Elab.SyntheticMVars
 import Lean.Elab.SetOption
@@ -138,7 +139,8 @@ private def mkCoreContext (ctx : Context) (s : State) (heartbeats : Nat) : Core.
     currNamespace  := scope.currNamespace
     openDecls      := scope.openDecls
     initHeartbeats := heartbeats
-    currMacroScope := ctx.currMacroScope }
+    currMacroScope := ctx.currMacroScope
+    diag           := getDiag scope.opts }
 
 private def addTraceAsMessagesCore (ctx : Context) (log : MessageLog) (traceState : TraceState) : MessageLog := Id.run do
   if traceState.traces.isEmpty then return log
@@ -411,7 +413,7 @@ def liftTermElabM (x : TermElabM α) : CommandElabM α := do
   -- make sure `observing` below also catches runtime exceptions (like we do by default in
   -- `CommandElabM`)
   let _ := MonadAlwaysExcept.except (m := TermElabM)
-  let x : MetaM _      := (observing x).run (mkTermContext ctx s) { levelNames := scope.levelNames }
+  let x : MetaM _      := (observing (try x finally Meta.reportDiag)).run (mkTermContext ctx s) { levelNames := scope.levelNames }
   let x : CoreM _      := x.run mkMetaContext {}
   let x : EIO _ _      := x.run (mkCoreContext ctx s heartbeats) { env := s.env, ngen := s.ngen, nextMacroScope := s.nextMacroScope, infoState.enabled := s.infoState.enabled, traceState := s.traceState }
   let (((ea, _), _), coreS) ← liftEIO x

src/Lean/Elab/Extra.lean

@@ -96,7 +96,7 @@ Here are brief descriptions of each of the operator types:
 - `rightact% f a b` elaborates `f a b` as a right action (the `b` operand "acts upon" the `a` operand).
   Only `a` participates in the protocol since `b` can have an unrelated type.
   This is used by `HPow` since, for example, there are both `Real -> Nat -> Real` and `Real -> Real -> Real`
-  exponentiation functions, and we prefer the former in the case of `x ^ 2`, but `binop%` would choose the latter. (#2220)
+  exponentiation functions, and we prefer the former in the case of `x ^ 2`, but `binop%` would choose the latter. (#2854)
 - There are also `binrel%` and `binrel_no_prop%` (see the docstring for `elabBinRelCore`).
 
 The elaborator works as follows:
@@ -449,7 +449,7 @@ def elabOp : TermElab := fun stx expectedType? => do
 
   - `binrel% R x y` elaborates `R x y` using the `binop%/...` expression trees in both `x` and `y`.
     It is similar to how `binop% R x y` elaborates but with a significant difference:
-    it does not use the expected type when computing the types of the operads.
+    it does not use the expected type when computing the types of the operands.
   - `binrel_no_prop% R x y` elaborates `R x y` like `binrel% R x y`, but if the resulting type for `x` and `y`
     is `Prop` they are coerced to `Bool`.
     This is used for relations such as `==` which do not support `Prop`, but we still want

src/Lean/Elab/InfoTree/Main.lean

@@ -102,8 +102,10 @@ def ContextInfo.runCoreM (info : ContextInfo) (x : CoreM α) : IO α := do
     have been used in `lctx` and `info.mctx`.
   -/
   (·.1) <$>
-    x.toIO { options := info.options, currNamespace := info.currNamespace, openDecls := info.openDecls, fileName := "<InfoTree>", fileMap := default }
-           { env := info.env, ngen := info.ngen }
+    (withOptions (fun _ => info.options) x).toIO
+      { currNamespace := info.currNamespace, openDecls := info.openDecls
+        fileName := "<InfoTree>", fileMap := default }
+      { env := info.env, ngen := info.ngen }
 
 def ContextInfo.runMetaM (info : ContextInfo) (lctx : LocalContext) (x : MetaM α) : IO α := do
   (·.1) <$> info.runCoreM (x.run { lctx := lctx } { mctx := info.mctx })

src/Lean/Elab/Print.lean

@@ -65,8 +65,36 @@ private def printInduct (id : Name) (levelParams : List Name) (numParams : Nat)
     m := m ++ Format.line ++ ctor ++ " : " ++ cinfo.type
   logInfo m
 
+open Meta in
+private def printStructure (id : Name) (levelParams : List Name) (numParams : Nat) (type : Expr)
+    (ctor : Name) (fields : Array Name) (isUnsafe : Bool) (isClass : Bool) : CommandElabM Unit := do
+  let kind := if isClass then "class" else "structure"
+  let mut m ← mkHeader' kind id levelParams type isUnsafe
+  m := m ++ Format.line ++ "number of parameters: " ++ toString numParams
+  m := m ++ Format.line ++ "constructor:"
+  let cinfo ← getConstInfo ctor
+  m := m ++ Format.line ++ ctor ++ " : " ++ cinfo.type
+  m := m ++ Format.line ++ "fields:" ++ (← doFields)
+  logInfo m
+where
+  doFields := liftTermElabM do
+    forallTelescope (← getConstInfo id).type fun params type =>
+      withLocalDeclD `self type fun self => do
+        let params := params.push self
+        let mut m : Format := ""
+        for field in fields do
+          match getProjFnForField? (← getEnv) id field with
+          | some proj =>
+            let field : Format := if isPrivateName proj then "private " ++ toString field else toString field
+            let cinfo ← getConstInfo proj
+            let ftype ← instantiateForall cinfo.type params
+            m := m ++ Format.line ++ field ++ " : " ++ (← ppExpr ftype) -- Why ppExpr here?
+          | none => panic! "missing structure field info"
+        return m
+
 private def printIdCore (id : Name) : CommandElabM Unit := do
-  match (← getEnv).find? id with
+  let env ← getEnv
+  match env.find? id with
   | ConstantInfo.axiomInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "axiom" id us t u
   | ConstantInfo.defnInfo  { levelParams := us, type := t, value := v, safety := s, .. } => printDefLike "def" id us t v s
   | ConstantInfo.thmInfo  { levelParams := us, type := t, value := v, .. } => printDefLike "theorem" id us t v
@@ -75,7 +103,11 @@ private def printIdCore (id : Name) : CommandElabM Unit := do
   | ConstantInfo.ctorInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constructor" id us t u
   | ConstantInfo.recInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "recursor" id us t u
   | ConstantInfo.inductInfo { levelParams := us, numParams, type := t, ctors, isUnsafe := u, .. } =>
-    printInduct id us numParams t ctors u
+    match getStructureInfo? env id with
+    | some { fieldNames, .. } =>
+      let [ctor] := ctors | panic! "structures have only one constructor"
+      printStructure id us numParams t ctor fieldNames u (isClass env id)
+    | none => printInduct id us numParams t ctors u
   | none => throwUnknownId id
 
 private def printId (id : Syntax) : CommandElabM Unit := do

src/Lean/Elab/StructInst.lean

@@ -821,7 +821,9 @@ partial def reduce (structNames : Array Name) (e : Expr) : MetaM Expr := do
     | some r => reduce structNames r
     | none   => return e.updateProj! (← reduce structNames b)
   | .app f .. =>
-    match (← reduceProjOf? e structNames.contains) with
+    -- Recall that proposition fields are theorems. Thus, we must set transparency to .all
+    -- to ensure they are unfolded here
+    match (← withTransparency .all <| reduceProjOf? e structNames.contains) with
     | some r => reduce structNames r
     | none   =>
       let f := f.getAppFn

src/Lean/Elab/Structure.lean

@@ -82,15 +82,6 @@ def StructFieldInfo.isSubobject (info : StructFieldInfo) : Bool :=
   | StructFieldKind.subobject => true
   | _                         => false
 
-structure ElabStructResult where
-  decl            : Declaration
-  projInfos       : List ProjectionInfo
-  projInstances   : List Name -- projections (to parent classes) that must be marked as instances.
-  mctx            : MetavarContext
-  lctx            : LocalContext
-  localInsts      : LocalInstances
-  defaultAuxDecls : Array (Name × Expr × Expr)
-
 private def defaultCtorName := `mk
 
 /-
@@ -713,8 +704,8 @@ private def registerStructure (structName : Name) (infos : Array StructFieldInfo
           subobject? :=
             if info.kind == StructFieldKind.subobject then
               match env.find? info.declName with
-              | some (ConstantInfo.defnInfo val) =>
-                match val.type.getForallBody.getAppFn with
+              | some info =>
+                match info.type.getForallBody.getAppFn with
                 | Expr.const parentName .. => some parentName
                 | _ => panic! "ill-formed structure"
               | _ => panic! "ill-formed environment"

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Meta.Diagnostics
 import Lean.Meta.Tactic.Apply
 import Lean.Meta.Tactic.Assumption
 import Lean.Meta.Tactic.Contradiction
@@ -163,8 +164,12 @@ private def getOptRotation (stx : Syntax) : Nat :=
 
 @[builtin_tactic Parser.Tactic.set_option] def elabSetOption : Tactic := fun stx => do
   let options ← Elab.elabSetOption stx[1] stx[3]
-  withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options }) do
-    evalTactic stx[5]
+  withOptions (fun _ => options) do
+    try
+      evalTactic stx[5]
+    finally
+      if stx[1].getId == `diagnostics then
+        reportDiag
 
 @[builtin_tactic Parser.Tactic.allGoals] def evalAllGoals : Tactic := fun stx => do
   let mvarIds ← getGoals

src/Lean/Elab/Tactic/LibrarySearch.lean

@@ -68,11 +68,8 @@ def elabExact?Term : TermElab := fun stx expectedType? => do
     let (_, introdGoal) ← goal.mvarId!.intros
     introdGoal.withContext do
       if let some suggestions ← librarySearch introdGoal then
-        reportOutOfHeartbeats `library_search stx
-        for suggestion in suggestions do
-          withMCtx suggestion.2 do
-            addTermSuggestion stx (← instantiateMVars goal).headBeta
-        if suggestions.isEmpty then logError "exact?# didn't find any relevant lemmas"
+        if suggestions.isEmpty then logError "`exact?%` didn't find any relevant lemmas"
+        else logError "`exact?%` could not close the goal. Try `by apply` to see partial suggestions."
         mkSorry expectedType (synthetic := true)
       else
         addTermSuggestion stx (← instantiateMVars goal).headBeta

src/Lean/Elab/Tactic/NormCast.lean

@@ -146,7 +146,9 @@ It tries to rewrite an expression using the elim and move lemmas.
 On failure, it calls the splitting procedure heuristic.
 -/
 partial def upwardAndElim (up : SimpTheorems) (e : Expr) : SimpM Simp.Step := do
-  let r ← withDischarger prove do
+  -- Remark: we set `wellBehavedDischarge := false` because `prove` may access arbitrary elements in the local context.
+  -- See comment at `Methods.wellBehavedDischarge`
+  let r ← withDischarger prove (wellBehavedDischarge := false) do
     Simp.rewrite? e up.post up.erased (tag := "squash") (rflOnly := false)
   let r := r.getD { expr := e }
   let r ← r.mkEqTrans (← splittingProcedure r.expr)

src/Lean/Elab/Tactic/Simp.lean

@@ -15,7 +15,6 @@ import Lean.Elab.Tactic.Config
 namespace Lean.Elab.Tactic
 open Meta
 open TSyntax.Compat
-open Simp (UsedSimps)
 
 declare_config_elab elabSimpConfigCore    Meta.Simp.Config
 declare_config_elab elabSimpConfigCtxCore Meta.Simp.ConfigCtx
@@ -327,7 +326,7 @@ If `stx` is the syntax of a `simp`, `simp_all` or `dsimp` tactic invocation, and
 creates the syntax of an equivalent `simp only`, `simp_all only` or `dsimp only`
 invocation.
 -/
-def mkSimpOnly (stx : Syntax) (usedSimps : UsedSimps) : MetaM Syntax := do
+def mkSimpOnly (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Syntax := do
   let isSimpAll := stx.isOfKind ``Parser.Tactic.simpAll
   let mut stx := stx
   if stx[3].isNone then
@@ -379,7 +378,7 @@ def mkSimpOnly (stx : Syntax) (usedSimps : UsedSimps) : MetaM Syntax := do
   let argsStx := if args.isEmpty then #[] else #[mkAtom "[", (mkAtom ",").mkSep args, mkAtom "]"]
   return stx.setArg 4 (mkNullNode argsStx)
 
-def traceSimpCall (stx : Syntax) (usedSimps : UsedSimps) : MetaM Unit := do
+def traceSimpCall (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Unit := do
   logInfoAt stx[0] m!"Try this: {← mkSimpOnly stx usedSimps}"
 
 /--
@@ -396,7 +395,7 @@ For many tactics other than the simplifier,
 one should use the `withLocation` tactic combinator
 when working with a `location`.
 -/
-def simpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (discharge? : Option Simp.Discharge := none) (loc : Location) : TacticM UsedSimps := do
+def simpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (discharge? : Option Simp.Discharge := none) (loc : Location) : TacticM Simp.Stats := do
   match loc with
   | Location.targets hyps simplifyTarget =>
     withMainContext do
@@ -406,33 +405,39 @@ def simpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (discharge
     withMainContext do
       go (← (← getMainGoal).getNondepPropHyps) (simplifyTarget := true)
 where
-  go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM UsedSimps := do
+  go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Simp.Stats := do
     let mvarId ← getMainGoal
-    let (result?, usedSimps) ← simpGoal mvarId ctx (simprocs := simprocs) (simplifyTarget := simplifyTarget) (discharge? := discharge?) (fvarIdsToSimp := fvarIdsToSimp)
+    let (result?, stats) ← simpGoal mvarId ctx (simprocs := simprocs) (simplifyTarget := simplifyTarget) (discharge? := discharge?) (fvarIdsToSimp := fvarIdsToSimp)
     match result? with
     | none => replaceMainGoal []
     | some (_, mvarId) => replaceMainGoal [mvarId]
-    return usedSimps
+    return stats
+
+def withSimpDiagnostics (x : TacticM Simp.Diagnostics) : TacticM Unit := do
+  let stats ← x
+  Simp.reportDiag stats
 
 /-
   "simp" (config)? (discharger)? (" only")? (" [" ((simpStar <|> simpErase <|> simpLemma),*,?) "]")?
   (location)?
 -/
-@[builtin_tactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => withMainContext do
+@[builtin_tactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => withMainContext do withSimpDiagnostics do
   let { ctx, simprocs, dischargeWrapper } ← mkSimpContext stx (eraseLocal := false)
-  let usedSimps ← dischargeWrapper.with fun discharge? =>
+  let stats ← dischargeWrapper.with fun discharge? =>
     simpLocation ctx simprocs discharge? (expandOptLocation stx[5])
   if tactic.simp.trace.get (← getOptions) then
-    traceSimpCall stx usedSimps
+    traceSimpCall stx stats.usedTheorems
+  return stats.diag
 
-@[builtin_tactic Lean.Parser.Tactic.simpAll] def evalSimpAll : Tactic := fun stx => withMainContext do
+@[builtin_tactic Lean.Parser.Tactic.simpAll] def evalSimpAll : Tactic := fun stx => withMainContext do withSimpDiagnostics do
   let { ctx, simprocs, .. } ← mkSimpContext stx (eraseLocal := true) (kind := .simpAll) (ignoreStarArg := true)
-  let (result?, usedSimps) ← simpAll (← getMainGoal) ctx (simprocs := simprocs)
+  let (result?, stats) ← simpAll (← getMainGoal) ctx (simprocs := simprocs)
   match result? with
   | none => replaceMainGoal []
   | some mvarId => replaceMainGoal [mvarId]
   if tactic.simp.trace.get (← getOptions) then
-    traceSimpCall stx usedSimps
+    traceSimpCall stx stats.usedTheorems
+  return stats.diag
 
 def dsimpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (loc : Location) : TacticM Unit := do
   match loc with
@@ -444,14 +449,15 @@ def dsimpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (loc : Lo
     withMainContext do
       go (← (← getMainGoal).getNondepPropHyps) (simplifyTarget := true)
 where
-  go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Unit := do
+  go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Unit := withSimpDiagnostics do
     let mvarId ← getMainGoal
-    let (result?, usedSimps) ← dsimpGoal mvarId ctx simprocs (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp)
+    let (result?, stats) ← dsimpGoal mvarId ctx simprocs (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp)
     match result? with
     | none => replaceMainGoal []
     | some mvarId => replaceMainGoal [mvarId]
     if tactic.simp.trace.get (← getOptions) then
-      mvarId.withContext <| traceSimpCall (← getRef) usedSimps
+      mvarId.withContext <| traceSimpCall (← getRef) stats.usedTheorems
+    return stats.diag
 
 @[builtin_tactic Lean.Parser.Tactic.dsimp] def evalDSimp : Tactic := fun stx => do
   let { ctx, simprocs, .. } ← withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)

src/Lean/Elab/Tactic/SimpTrace.lean

@@ -25,39 +25,41 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
 @[builtin_tactic simpTrace] def evalSimpTrace : Tactic := fun stx =>
   match stx with
   | `(tactic|
-      simp?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) => withMainContext do
+      simp?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) => withMainContext do withSimpDiagnostics do
     let stx ← if bang.isSome then
       `(tactic| simp!%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
     else
       `(tactic| simp%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
     let { ctx, simprocs, dischargeWrapper } ← mkSimpContext stx (eraseLocal := false)
-    let usedSimps ← dischargeWrapper.with fun discharge? =>
+    let stats ← dischargeWrapper.with fun discharge? =>
       simpLocation ctx (simprocs := simprocs) discharge? <|
         (loc.map expandLocation).getD (.targets #[] true)
-    let stx ← mkSimpCallStx stx usedSimps
+    let stx ← mkSimpCallStx stx stats.usedTheorems
     addSuggestion tk stx (origSpan? := ← getRef)
+    return stats.diag
   | _ => throwUnsupportedSyntax
 
 @[builtin_tactic simpAllTrace] def evalSimpAllTrace : Tactic := fun stx =>
   match stx with
-  | `(tactic| simp_all?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?) => do
+  | `(tactic| simp_all?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?) => withSimpDiagnostics do
     let stx ← if bang.isSome then
       `(tactic| simp_all!%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?)
     else
       `(tactic| simp_all%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?)
     let { ctx, .. } ← mkSimpContext stx (eraseLocal := true)
       (kind := .simpAll) (ignoreStarArg := true)
-    let (result?, usedSimps) ← simpAll (← getMainGoal) ctx
+    let (result?, stats) ← simpAll (← getMainGoal) ctx
     match result? with
     | none => replaceMainGoal []
     | some mvarId => replaceMainGoal [mvarId]
-    let stx ← mkSimpCallStx stx usedSimps
+    let stx ← mkSimpCallStx stx stats.usedTheorems
     addSuggestion tk stx (origSpan? := ← getRef)
+    return stats.diag
   | _ => throwUnsupportedSyntax
 
 /-- Implementation of `dsimp?`. -/
 def dsimpLocation' (ctx : Simp.Context) (simprocs : SimprocsArray) (loc : Location) :
-    TacticM Simp.UsedSimps := do
+    TacticM Simp.Stats := do
   match loc with
   | Location.targets hyps simplifyTarget =>
     withMainContext do
@@ -68,25 +70,26 @@ def dsimpLocation' (ctx : Simp.Context) (simprocs : SimprocsArray) (loc : Locati
       go (← (← getMainGoal).getNondepPropHyps) (simplifyTarget := true)
 where
   /-- Implementation of `dsimp?`. -/
-  go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Simp.UsedSimps := do
+  go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Simp.Stats := do
     let mvarId ← getMainGoal
-    let (result?, usedSimps) ← dsimpGoal mvarId ctx simprocs (simplifyTarget := simplifyTarget)
+    let (result?, stats) ← dsimpGoal mvarId ctx simprocs (simplifyTarget := simplifyTarget)
       (fvarIdsToSimp := fvarIdsToSimp)
     match result? with
     | none => replaceMainGoal []
     | some mvarId => replaceMainGoal [mvarId]
-    pure usedSimps
+    pure stats
 
 @[builtin_tactic dsimpTrace] def evalDSimpTrace : Tactic := fun stx =>
   match stx with
-  | `(tactic| dsimp?%$tk $[!%$bang]? $(config)? $[only%$o]? $[[$args,*]]? $(loc)?) => do
+  | `(tactic| dsimp?%$tk $[!%$bang]? $(config)? $[only%$o]? $[[$args,*]]? $(loc)?) => withSimpDiagnostics do
     let stx ← if bang.isSome then
       `(tactic| dsimp!%$tk $(config)? $[only%$o]? $[[$args,*]]? $(loc)?)
     else
       `(tactic| dsimp%$tk $(config)? $[only%$o]? $[[$args,*]]? $(loc)?)
     let { ctx, simprocs, .. } ←
       withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
-    let usedSimps ← dsimpLocation' ctx simprocs <| (loc.map expandLocation).getD (.targets #[] true)
-    let stx ← mkSimpCallStx stx usedSimps
+    let stats ← dsimpLocation' ctx simprocs <| (loc.map expandLocation).getD (.targets #[] true)
+    let stx ← mkSimpCallStx stx stats.usedTheorems
     addSuggestion tk stx (origSpan? := ← getRef)
+    return stats.diag
   | _ => throwUnsupportedSyntax

src/Lean/Elab/Tactic/Simpa.lean

@@ -31,7 +31,7 @@ deriving instance Repr for UseImplicitLambdaResult
 @[builtin_tactic Lean.Parser.Tactic.simpa] def evalSimpa : Tactic := fun stx => do
   match stx with
   | `(tactic| simpa%$tk $[?%$squeeze]? $[!%$unfold]? $(cfg)? $(disch)? $[only%$only]?
-        $[[$args,*]]? $[using $usingArg]?) => Elab.Tactic.focus do
+        $[[$args,*]]? $[using $usingArg]?) => Elab.Tactic.focus do withSimpDiagnostics do
     let stx ← `(tactic| simp $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]?)
     let { ctx, simprocs, dischargeWrapper } ←
       withMainContext <| mkSimpContext stx (eraseLocal := false)
@@ -39,12 +39,13 @@ deriving instance Repr for UseImplicitLambdaResult
     -- TODO: have `simpa` fail if it doesn't use `simp`.
     let ctx := { ctx with config := { ctx.config with failIfUnchanged := false } }
     dischargeWrapper.with fun discharge? => do
-      let (some (_, g), usedSimps) ← simpGoal (← getMainGoal) ctx (simprocs := simprocs)
+      let (some (_, g), stats) ← simpGoal (← getMainGoal) ctx (simprocs := simprocs)
           (simplifyTarget := true) (discharge? := discharge?)
         | if getLinterUnnecessarySimpa (← getOptions) then
             logLint linter.unnecessarySimpa (← getRef) "try 'simp' instead of 'simpa'"
+          return {}
       g.withContext do
-      let usedSimps ← if let some stx := usingArg then
+      let stats ← if let some stx := usingArg then
         setGoals [g]
         g.withContext do
         let e ← Tactic.elabTerm stx none (mayPostpone := true)
@@ -52,8 +53,8 @@ deriving instance Repr for UseImplicitLambdaResult
           pure (h, g)
         else
           (← g.assert `h (← inferType e) e).intro1
-        let (result?, usedSimps) ← simpGoal g ctx (simprocs := simprocs) (fvarIdsToSimp := #[h])
-          (simplifyTarget := false) (usedSimps := usedSimps) (discharge? := discharge?)
+        let (result?, stats) ← simpGoal g ctx (simprocs := simprocs) (fvarIdsToSimp := #[h])
+          (simplifyTarget := false) (stats := stats) (discharge? := discharge?)
         match result? with
         | some (xs, g) =>
           let h := match xs with | #[h] | #[] => h | _ => unreachable!
@@ -66,18 +67,18 @@ deriving instance Repr for UseImplicitLambdaResult
             if (← getLCtx).getRoundtrippingUserName? h |>.isSome then
               logLint linter.unnecessarySimpa (← getRef)
                 m!"try 'simp at {Expr.fvar h}' instead of 'simpa using {Expr.fvar h}'"
-        pure usedSimps
+        pure stats
       else if let some ldecl := (← getLCtx).findFromUserName? `this then
-        if let (some (_, g), usedSimps) ← simpGoal g ctx (simprocs := simprocs)
-            (fvarIdsToSimp := #[ldecl.fvarId]) (simplifyTarget := false) (usedSimps := usedSimps)
+        if let (some (_, g), stats) ← simpGoal g ctx (simprocs := simprocs)
+            (fvarIdsToSimp := #[ldecl.fvarId]) (simplifyTarget := false) (stats := stats)
             (discharge? := discharge?) then
-          g.assumption; pure usedSimps
+          g.assumption; pure stats
         else
-          pure usedSimps
+          pure stats
       else
-        g.assumption; pure usedSimps
+        g.assumption; pure stats
       if tactic.simp.trace.get (← getOptions) || squeeze.isSome then
-        let stx ← match ← mkSimpOnly stx usedSimps with
+        let stx ← match ← mkSimpOnly stx stats.usedTheorems with
           | `(tactic| simp $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]?) =>
             if unfold.isSome then
               `(tactic| simpa! $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
@@ -85,6 +86,7 @@ deriving instance Repr for UseImplicitLambdaResult
               `(tactic| simpa $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
           | _ => unreachable!
         TryThis.addSuggestion tk stx (origSpan? := ← getRef)
+      return stats.diag
     | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Tactic.Simpa

src/Lean/Level.lean

@@ -428,15 +428,18 @@ def Result.imax : Result → Result → Result
   | f, Result.imaxNode Fs => Result.imaxNode (f::Fs)
   | f₁, f₂                => Result.imaxNode [f₁, f₂]
 
-def toResult : Level → Result
+def toResult (l : Level) (mvars : Bool) : Result :=
+  match l with
   | zero       => Result.num 0
-  | succ l     => Result.succ (toResult l)
-  | max l₁ l₂  => Result.max (toResult l₁) (toResult l₂)
-  | imax l₁ l₂ => Result.imax (toResult l₁) (toResult l₂)
+  | succ l     => Result.succ (toResult l mvars)
+  | max l₁ l₂  => Result.max (toResult l₁ mvars) (toResult l₂ mvars)
+  | imax l₁ l₂ => Result.imax (toResult l₁ mvars) (toResult l₂ mvars)
   | param n    => Result.leaf n
   | mvar n     =>
-    let n := n.name.replacePrefix `_uniq (Name.mkSimple "?u");
-    Result.leaf n
+    if mvars then
+      Result.leaf <| n.name.replacePrefix `_uniq (Name.mkSimple "?u")
+    else
+      Result.leaf `_
 
 private def parenIfFalse : Format → Bool → Format
   | f, true  => f
@@ -471,17 +474,17 @@ protected partial def Result.quote (r : Result) (prec : Nat) : Syntax.Level :=
 
 end PP
 
-protected def format (u : Level) : Format :=
-  (PP.toResult u).format true
+protected def format (u : Level) (mvars : Bool) : Format :=
+  (PP.toResult u mvars).format true
 
 instance : ToFormat Level where
-  format u := Level.format u
+  format u := Level.format u (mvars := true)
 
 instance : ToString Level where
-  toString u := Format.pretty (Level.format u)
+  toString u := Format.pretty (format u)
 
-protected def quote (u : Level) (prec : Nat := 0) : Syntax.Level :=
-  (PP.toResult u).quote prec
+protected def quote (u : Level) (prec : Nat := 0) (mvars : Bool := true) : Syntax.Level :=
+  (PP.toResult u (mvars := mvars)).quote prec
 
 instance : Quote Level `level where
   quote := Level.quote

src/Lean/Linter/Deprecated.lean

@@ -15,17 +15,23 @@ register_builtin_option linter.deprecated : Bool := {
   descr := "if true, generate deprecation warnings"
 }
 
-builtin_initialize deprecatedAttr : ParametricAttribute (Option Name) ←
+structure DeprecationEntry where
+  newName? : Option Name := none
+  text? : Option String := none
+  since? : Option String := none
+  deriving Inhabited
+
+builtin_initialize deprecatedAttr : ParametricAttribute DeprecationEntry ←
   registerParametricAttribute {
     name := `deprecated
     descr := "mark declaration as deprecated",
     getParam := fun _ stx => do
-     match stx with
-     | `(attr| deprecated $[$id?]?) =>
-       let some id := id? | return none
-       let declNameNew ← Elab.realizeGlobalConstNoOverloadWithInfo id
-       return some declNameNew
-     | _  => throwError "invalid `[deprecated]` attribute"
+      let `(attr| deprecated $[$id?]? $[$text?]? $[(since := $since?)]?) := stx
+        | throwError "invalid `[deprecated]` attribute"
+      let newName? ← id?.mapM Elab.realizeGlobalConstNoOverloadWithInfo
+      let text? := text?.map TSyntax.getString
+      let since? := since?.map TSyntax.getString
+      return { newName?, text?, since? }
   }
 
 def isDeprecated (env : Environment) (declName : Name) : Bool :=
@@ -34,12 +40,13 @@ def isDeprecated (env : Environment) (declName : Name) : Bool :=
 def _root_.Lean.MessageData.isDeprecationWarning (msg : MessageData) : Bool :=
   msg.hasTag (· == ``deprecatedAttr)
 
-def getDeprecatedNewName (env : Environment) (declName : Name) : Option Name :=
-  (deprecatedAttr.getParam? env declName).getD none
+def getDeprecatedNewName (env : Environment) (declName : Name) : Option Name := do
+  (← deprecatedAttr.getParam? env declName).newName?
 
 def checkDeprecated [Monad m] [MonadEnv m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (declName : Name) : m Unit := do
   if getLinterValue linter.deprecated (← getOptions) then
-    match deprecatedAttr.getParam? (← getEnv) declName with
-    | none => pure ()
-    | some none => logWarning <| .tagged ``deprecatedAttr m!"`{declName}` has been deprecated"
-    | some (some newName) => logWarning <| .tagged ``deprecatedAttr m!"`{declName}` has been deprecated, use `{newName}` instead"
+    let some attr := deprecatedAttr.getParam? (← getEnv) declName | pure ()
+    logWarning <| .tagged ``deprecatedAttr <| attr.text?.getD <|
+      match attr.newName? with
+      | none => s!"`{declName}` has been deprecated"
+      | some newName => s!"`{declName}` has been deprecated, use `{newName}` instead"

src/Lean/Message.lean

@@ -120,7 +120,13 @@ def ofExpr (e : Expr) : MessageData :=
     hasSyntheticSorry := (instantiateMVarsCore · e |>.1.hasSyntheticSorry)
   }
 
-def ofLevel (l : Level) : MessageData := ofFormat (format l)
+def ofLevel (l : Level) : MessageData :=
+  .ofPPFormat {
+    pp := fun
+      | some ctx => ppLevel ctx l
+      | none => return format l
+  }
+
 def ofName (n : Name) : MessageData := ofFormat (format n)
 
 partial def hasSyntheticSorry (msg : MessageData) : Bool :=

src/Lean/Meta.lean

@@ -49,3 +49,4 @@ import Lean.Meta.LazyDiscrTree
 import Lean.Meta.LitValues
 import Lean.Meta.CheckTactic
 import Lean.Meta.Canonicalizer
+import Lean.Meta.Diagnostics

src/Lean/Meta/Basic.lean

@@ -110,6 +110,14 @@ structure Config where
   trackZetaDelta     : Bool := false
   /-- Eta for structures configuration mode. -/
   etaStruct          : EtaStructMode := .all
+  /--
+  When `univApprox` is set to true,
+  we use approximations when solving postponed universe constraints.
+  Examples:
+  - `max u ?v =?= u` is solved with `?v := u` and ignoring the solution `?v := 0`.
+  - `max u w =?= mav u ?v` is solved with `?v := w` ignoring the solution `?v := max u w`
+  -/
+  univApprox : Bool := true
 
 /--
   Function parameter information cache.
@@ -258,6 +266,15 @@ structure PostponedEntry where
   ctx? : Option DefEqContext
   deriving Inhabited
 
+structure Diagnostics where
+  /-- Number of times each declaration has been unfolded -/
+  unfoldCounter : PHashMap Name Nat := {}
+  /-- Number of times `f a =?= f b` heuristic has been used per function `f`. -/
+  heuristicCounter : PHashMap Name Nat := {}
+  /-- Number of times a TC instance is used. -/
+  instanceCounter : PHashMap Name Nat := {}
+  deriving Inhabited
+
 /--
   `MetaM` monad state.
 -/
@@ -268,6 +285,7 @@ structure State where
   zetaDeltaFVarIds : FVarIdSet := {}
   /-- Array of postponed universe level constraints -/
   postponed        : PersistentArray PostponedEntry := {}
+  diag             : Diagnostics := {}
   deriving Inhabited
 
 /--
@@ -300,6 +318,17 @@ structure Context where
     A predicate to control whether a constant can be unfolded or not at `whnf`.
     Note that we do not cache results at `whnf` when `canUnfold?` is not `none`. -/
   canUnfold?        : Option (Config → ConstantInfo → CoreM Bool) := none
+  /--
+  When `Config.univApprox := true`, this flag is set to `true` when there is no
+  progress processing universe constraints.
+  -/
+  univApprox        : Bool := false
+  /--
+  `inTypeClassResolution := true` when `isDefEq` is invoked at `tryResolve` in the type class
+   resolution module. We don't use `isDefEqProjDelta` when performing TC resolution due to performance issues.
+   This is not a great solution, but a proper solution would require a more sophisticased caching mechanism.
+  -/
+  inTypeClassResolution : Bool := false
 
 /--
 The `MetaM` monad is a core component of Lean's metaprogramming framework, facilitating the
@@ -421,7 +450,7 @@ section Methods
 variable [MonadControlT MetaM n] [Monad n]
 
 @[inline] def modifyCache (f : Cache → Cache) : MetaM Unit :=
-  modify fun { mctx, cache, zetaDeltaFVarIds, postponed } => { mctx, cache := f cache, zetaDeltaFVarIds, postponed }
+  modify fun { mctx, cache, zetaDeltaFVarIds, postponed, diag } => { mctx, cache := f cache, zetaDeltaFVarIds, postponed, diag }
 
 @[inline] def modifyInferTypeCache (f : InferTypeCache → InferTypeCache) : MetaM Unit :=
   modifyCache fun ⟨ic, c1, c2, c3, c4, c5, c6⟩ => ⟨f ic, c1, c2, c3, c4, c5, c6⟩
@@ -435,6 +464,28 @@ variable [MonadControlT MetaM n] [Monad n]
 @[inline] def resetDefEqPermCaches : MetaM Unit :=
   modifyDefEqPermCache fun _ => {}
 
+@[inline] def modifyDiag (f : Diagnostics → Diagnostics) : MetaM Unit := do
+  if (← isDiagnosticsEnabled) then
+    modify fun { mctx, cache, zetaDeltaFVarIds, postponed, diag } => { mctx, cache, zetaDeltaFVarIds, postponed, diag := f diag }
+
+/-- If diagnostics are enabled, record that `declName` has been unfolded. -/
+def recordUnfold (declName : Name) : MetaM Unit := do
+  modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter } =>
+    let newC := if let some c := unfoldCounter.find? declName then c + 1 else 1
+    { unfoldCounter := unfoldCounter.insert declName newC, heuristicCounter, instanceCounter }
+
+/-- If diagnostics are enabled, record that heuristic for solving `f a =?= f b` has been used. -/
+def recordDefEqHeuristic (declName : Name) : MetaM Unit := do
+  modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter } =>
+    let newC := if let some c := heuristicCounter.find? declName then c + 1 else 1
+    { unfoldCounter, heuristicCounter := heuristicCounter.insert declName newC, instanceCounter }
+
+/-- If diagnostics are enabled, record that instance `declName` was used during TC resolution. -/
+def recordInstance (declName : Name) : MetaM Unit := do
+  modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter } =>
+    let newC := if let some c := instanceCounter.find? declName then c + 1 else 1
+    { unfoldCounter, heuristicCounter, instanceCounter := instanceCounter.insert declName newC }
+
 def getLocalInstances : MetaM LocalInstances :=
   return (← read).localInstances
 
@@ -1690,6 +1741,10 @@ partial def processPostponed (mayPostpone : Bool := true) (exceptionOnFailure :=
               return true
             else if numPostponed' < numPostponed then
               loop
+            -- If we cannot pospone anymore, `Config.univApprox := true`, but we haven't tried universe approximations yet,
+            -- then try approximations before failing.
+            else if !mayPostpone && (← getConfig).univApprox && !(← read).univApprox then
+              withReader (fun ctx => { ctx with univApprox := true }) loop
             else
               trace[Meta.isLevelDefEq.postponed] "no progress solving pending is-def-eq level constraints"
               return mayPostpone

src/Lean/Meta/Diagnostics.lean

@@ -0,0 +1,88 @@
+/-
+Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.PrettyPrinter
+import Lean.Meta.Basic
+import Lean.Meta.Instances
+
+namespace Lean.Meta
+
+def collectAboveThreshold [BEq α] [Hashable α] (counters : PHashMap α Nat) (threshold : Nat) (p : α → Bool) (lt : α → α → Bool) : Array (α × Nat) := Id.run do
+  let mut r := #[]
+  for (declName, counter) in counters do
+    if counter > threshold then
+    if p declName then
+      r := r.push (declName, counter)
+  return r.qsort fun (d₁, c₁) (d₂, c₂) => if c₁ == c₂ then lt d₁ d₂ else c₁ > c₂
+
+def subCounters [BEq α] [Hashable α] (newCounters oldCounters : PHashMap α Nat) : PHashMap α Nat := Id.run do
+  let mut result := {}
+  for (a, counterNew) in newCounters do
+    if let some counterOld := oldCounters.find? a then
+      result := result.insert a (counterNew - counterOld)
+    else
+      result := result.insert a counterNew
+  return result
+
+structure DiagSummary where
+  data  : Array MessageData := #[]
+  max   : Nat := 0
+  deriving Inhabited
+
+def DiagSummary.isEmpty (s : DiagSummary) : Bool :=
+  s.data.isEmpty
+
+def mkDiagSummary (counters : PHashMap Name Nat) (p : Name → Bool := fun _ => true) : MetaM DiagSummary := do
+  let threshold := diagnostics.threshold.get (← getOptions)
+  let entries := collectAboveThreshold counters threshold p Name.lt
+  if entries.isEmpty then
+    return {}
+  else
+    let mut data := #[]
+    for (declName, counter) in entries do
+      data := data.push m!"{if data.isEmpty then "  " else "\n"}{MessageData.ofConst (← mkConstWithLevelParams declName)} ↦ {counter}"
+    return { data, max := entries[0]!.2 }
+
+def mkDiagSummaryForUnfolded (counters : PHashMap Name Nat) (instances := false) : MetaM DiagSummary := do
+  let env ← getEnv
+  mkDiagSummary counters fun declName =>
+    getReducibilityStatusCore env declName matches .semireducible
+    && isInstanceCore env declName == instances
+
+def mkDiagSummaryForUnfoldedReducible (counters : PHashMap Name Nat) : MetaM DiagSummary := do
+  let env ← getEnv
+  mkDiagSummary counters fun declName =>
+    getReducibilityStatusCore env declName matches .reducible
+
+def mkDiagSummaryForUsedInstances : MetaM DiagSummary := do
+  mkDiagSummary (← get).diag.heuristicCounter
+
+def appendSection (m : MessageData) (cls : Name) (header : String) (s : DiagSummary) : MessageData :=
+  if s.isEmpty then
+    m
+  else
+    let header := s!"{header} (max: {s.max}, num: {s.data.size}):"
+    m ++ .trace { cls } header s.data
+
+def reportDiag : MetaM Unit := do
+  if (← isDiagnosticsEnabled) then
+    let unfoldCounter := (← get).diag.unfoldCounter
+    let unfoldDefault ← mkDiagSummaryForUnfolded unfoldCounter
+    let unfoldInstance ← mkDiagSummaryForUnfolded unfoldCounter (instances := true)
+    let unfoldReducible ← mkDiagSummaryForUnfoldedReducible unfoldCounter
+    let heu ← mkDiagSummary (← get).diag.heuristicCounter
+    let inst ← mkDiagSummaryForUsedInstances
+    unless unfoldDefault.isEmpty && unfoldInstance.isEmpty && unfoldReducible.isEmpty && heu.isEmpty && inst.isEmpty do
+      let m := MessageData.nil
+      let m := appendSection m `reduction "unfolded declarations" unfoldDefault
+      let m := appendSection m `reduction "unfolded instances" unfoldInstance
+      let m := appendSection m `reduction "unfolded reducible declarations" unfoldReducible
+      let m := appendSection m `type_class "used instances" inst
+      let m := appendSection m `def_eq "heuristic for solving `f a =?= f b`" heu
+      let m := m ++ "use `set_option diagnostics.threshold <num>` to control threshold for reporting counters"
+      logInfo m
+
+end Lean.Meta

src/Lean/Meta/ExprDefEq.lean

@@ -10,6 +10,18 @@ import Lean.Util.OccursCheck
 
 namespace Lean.Meta
 
+register_builtin_option backward.isDefEq.lazyProjDelta : Bool := {
+  defValue := true
+  group    := "backward compatibility"
+  descr    := "use lazy delta reduction when solving unification constrains of the form `(f a).i =?= (g b).i`"
+}
+
+register_builtin_option backward.isDefEq.lazyWhnfCore : Bool := {
+  defValue := true
+  group    := "backward compatibility"
+  descr    := "specifies transparency mode when normalizing constraints of the form `(f a).i =?= s`, if `true` only reducible definitions and instances are unfolded when reducing `f a`. Otherwise, the default setting is used"
+}
+
 /--
   Return `true` if `e` is of the form `fun (x_1 ... x_n) => ?m y_1 ... y_k)`, and `?m` is unassigned.
   Remark: `n`, `k` may be 0.
@@ -1239,6 +1251,7 @@ private def tryHeuristic (t s : Expr) : MetaM Bool := do
     unless t.hasExprMVar || s.hasExprMVar do
       return false
   withTraceNodeBefore `Meta.isDefEq.delta (return m!"{t} =?= {s}") do
+    recordDefEqHeuristic tFn.constName!
     /-
       We process arguments before universe levels to reduce a source of brittleness in the TC procedure.
 
@@ -1757,10 +1770,21 @@ private def isDefEqDeltaStep (t s : Expr) : MetaM DeltaStepResult := do
     | .lt => unfold t (return .unknown) (k · s)
     | .gt => unfold s (return .unknown) (k t ·)
     | .eq =>
-      unfold t
-        (unfold s (return .unknown) (k t ·))
-        (fun t => unfold s (k t s) (k t ·))
+      -- Remark: if `t` and `s` are both some `f`-application, we use `tryHeuristic`
+      -- if `f` is not a projection. The projection case generates a performance regression.
+      if tInfo.name == sInfo.name then
+        if t.isApp && s.isApp && (← tryHeuristic t s) then
+          return .eq
+        else
+          unfoldBoth t s
+      else
+        unfoldBoth t s
 where
+  unfoldBoth (t s : Expr) : MetaM DeltaStepResult := do
+    unfold t
+      (unfold s (return .unknown) (k t ·))
+      (fun t => unfold s (k t s) (k t ·))
+
   k (t s : Expr) : MetaM DeltaStepResult := do
     let t ← whnfCore t
     let s ← whnfCore s
@@ -1792,8 +1816,13 @@ where
     | _, _ => Meta.isExprDefEqAux t s
 
 private def isDefEqProj : Expr → Expr → MetaM Bool
-  | .proj m i t, .proj n j s =>
-    if i == j && m == n then
+  | .proj m i t, .proj n j s => do
+    if (← read).inTypeClassResolution then
+      -- See comment at `inTypeClassResolution`
+      pure (i == j && m == n) <&&> Meta.isExprDefEqAux t s
+    else if !backward.isDefEq.lazyProjDelta.get (← getOptions) then
+      pure (i == j && m == n) <&&> Meta.isExprDefEqAux t s
+    else if i == j && m == n then
       isDefEqProjDelta t s i
     else
       return false
@@ -1966,6 +1995,12 @@ private def cacheResult (keyInfo : DefEqCacheKeyInfo) (result : Bool) : MetaM Un
     let key := (← instantiateMVars key.1, ← instantiateMVars key.2)
     modifyDefEqTransientCache fun c => c.update mode key result
 
+private def whnfCoreAtDefEq (e : Expr) : MetaM Expr := do
+  if backward.isDefEq.lazyWhnfCore.get (← getOptions) then
+    whnfCore e (config := { proj := .yesWithDeltaI })
+  else
+    whnfCore e
+
 @[export lean_is_expr_def_eq]
 partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecDepth do
   withTraceNodeBefore `Meta.isDefEq (return m!"{t} =?= {s}") do
@@ -1978,7 +2013,7 @@ partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecD
     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
 
-    Note that ew use `proj := .yesWithDeltaI` to ensure `whnfAtMostI` is used to reduce the projection structure.
+    Note that we 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
@@ -2007,8 +2042,8 @@ partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecD
     `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 (config := { proj := .yesWithDeltaI })
-  let s' ← whnfCore s (config := { proj := .yesWithDeltaI })
+  let t' ← whnfCoreAtDefEq t
+  let s' ← whnfCoreAtDefEq s
   if t != t' || s != s' then
     isExprDefEqAuxImpl t' s'
   else

src/Lean/Meta/ExprLens.lean

@@ -21,27 +21,28 @@ section ExprLens
 
 open Lean.SubExpr
 
-variable {M} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] [MonadError M]
+variable [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] [MonadError M]
 
 /-- Given a constructor index for Expr, runs `g` on the value of that subexpression and replaces it.
 If the subexpression is under a binder it will instantiate and abstract the binder body correctly.
 Mdata is ignored. An index of 3 is interpreted as the type of the expression. An index of 3 will throw since we can't replace types.
 
 See also `Lean.Meta.transform`, `Lean.Meta.traverseChildren`. -/
-private def lensCoord (g : Expr → M Expr) : Nat → Expr → M Expr
-  | 0, e@(Expr.app f a)         => return e.updateApp! (← g f) a
-  | 1, e@(Expr.app f a)         => return e.updateApp! f (← g a)
-  | 0, e@(Expr.lam _ y b _)     => return e.updateLambdaE! (← g y) b
-  | 1,   (Expr.lam n y b c)     => withLocalDecl n c y fun x => do mkLambdaFVars #[x] <|← g <| b.instantiateRev #[x]
-  | 0, e@(Expr.forallE _ y b _) => return e.updateForallE! (← g y) b
-  | 1,   (Expr.forallE n y b c) => withLocalDecl n c y fun x => do mkForallFVars #[x] <|← g <| b.instantiateRev #[x]
-  | 0, e@(Expr.letE _ y a b _)  => return e.updateLet! (← g y) a b
-  | 1, e@(Expr.letE _ y a b _)  => return e.updateLet! y (← g a) b
-  | 2,   (Expr.letE n y a b _)  => withLetDecl n y a fun x => do mkLetFVars #[x] <|← g <| b.instantiateRev #[x]
-  | 0, e@(Expr.proj _ _ b)      => e.updateProj! <$> g b
-  | n, e@(Expr.mdata _ a)       => e.updateMData! <$> lensCoord g n a
-  | 3, _                        => throwError "Lensing on types is not supported"
-  | c, e                        => throwError "Invalid coordinate {c} for {e}"
+private def lensCoord (g : Expr → M Expr) (n : Nat) (e : Expr) : M Expr := do
+  match n, e with
+  | 0, .app f a         => return e.updateApp! (← g f) a
+  | 1, .app f a         => return e.updateApp! f (← g a)
+  | 0, .lam _ y b _     => return e.updateLambdaE! (← g y) b
+  | 1, .lam n y b c     => withLocalDecl n c y fun x => do mkLambdaFVars #[x] <|← g <| b.instantiateRev #[x]
+  | 0, .forallE _ y b _ => return e.updateForallE! (← g y) b
+  | 1, .forallE n y b c => withLocalDecl n c y fun x => do mkForallFVars #[x] <|← g <| b.instantiateRev #[x]
+  | 0, .letE _ y a b _  => return e.updateLet! (← g y) a b
+  | 1, .letE _ y a b _  => return e.updateLet! y (← g a) b
+  | 2, .letE n y a b _  => withLetDecl n y a fun x => do mkLetFVars #[x] <|← g <| b.instantiateRev #[x]
+  | 0, .proj _ _ b      => e.updateProj! <$> g b
+  | n, .mdata _ a       => e.updateMData! <$> lensCoord g n a
+  | 3, _                => throwError "Lensing on types is not supported"
+  | c, e                => throwError "Invalid coordinate {c} for {e}"
 
 private def lensAux (g : Expr → M Expr) : List Nat → Expr → M Expr
   | [], e => g e
@@ -56,20 +57,21 @@ def replaceSubexpr (replace : (subexpr : Expr) → M Expr) (p : Pos) (root : Exp
 /-- Runs `k` on the given coordinate, including handling binders properly.
 The subexpression value passed to `k` is not instantiated with respect to the
 array of free variables. -/
-private def viewCoordAux (k : Array Expr → Expr → M α) (fvars: Array Expr) : Nat → Expr → M α
-  | 3, _                      => throwError "Internal: Types should be handled by viewAux"
-  | 0, (Expr.app f _)         => k fvars f
-  | 1, (Expr.app _ a)         => k fvars a
-  | 0, (Expr.lam _ y _ _)     => k fvars y
-  | 1, (Expr.lam n y b c)     => withLocalDecl n c (y.instantiateRev fvars) fun x => k (fvars.push x) b
-  | 0, (Expr.forallE _ y _ _) => k fvars y
-  | 1, (Expr.forallE n y b c) => withLocalDecl n c (y.instantiateRev fvars) fun x => k (fvars.push x) b
-  | 0, (Expr.letE _ y _ _ _)  => k fvars y
-  | 1, (Expr.letE _ _ a _ _)  => k fvars a
-  | 2, (Expr.letE n y a b _)  => withLetDecl n (y.instantiateRev fvars) (a.instantiateRev fvars) fun x => k (fvars.push x) b
-  | 0, (Expr.proj _ _ b)      => k fvars b
-  | n, (Expr.mdata _ a)       => viewCoordAux k fvars n a
-  | c, e                      => throwError "Invalid coordinate {c} for {e}"
+private def viewCoordAux (k : Array Expr → Expr → M α) (fvars: Array Expr) (n : Nat) (e : Expr) : M α := do
+  match n, e with
+  | 3, _                => throwError "Internal: Types should be handled by viewAux"
+  | 0, .app f _         => k fvars f
+  | 1, .app _ a         => k fvars a
+  | 0, .lam _ y _ _     => k fvars y
+  | 1, .lam n y b c     => withLocalDecl n c (y.instantiateRev fvars) fun x => k (fvars.push x) b
+  | 0, .forallE _ y _ _ => k fvars y
+  | 1, .forallE n y b c => withLocalDecl n c (y.instantiateRev fvars) fun x => k (fvars.push x) b
+  | 0, .letE _ y _ _ _  => k fvars y
+  | 1, .letE _ _ a _ _  => k fvars a
+  | 2, .letE n y a b _  => withLetDecl n (y.instantiateRev fvars) (a.instantiateRev fvars) fun x => k (fvars.push x) b
+  | 0, .proj _ _ b      => k fvars b
+  | n, .mdata _ a       => viewCoordAux k fvars n a
+  | c, e                => throwError "Invalid coordinate {c} for {e}"
 
 private def viewAux (k : Array Expr → Expr → M α) (fvars : Array Expr) : List Nat → Expr → M α
   | [],         e => k fvars <| e.instantiateRev fvars
@@ -119,24 +121,24 @@ open Lean.SubExpr
 
 section ViewRaw
 
-variable {M} [Monad M] [MonadError M]
+variable [Monad M] [MonadError M]
 
 /-- Get the raw subexpression without performing any instantiation. -/
-private def viewCoordRaw: Expr → Nat → M Expr
-  | e                     , 3 => throwError "Can't viewRaw the type of {e}"
-  | (Expr.app f _)        , 0 => pure f
-  | (Expr.app _ a)        , 1 => pure a
-  | (Expr.lam _ y _ _)    , 0 => pure y
-  | (Expr.lam _ _ b _)    , 1 => pure b
-  | (Expr.forallE _ y _ _), 0 => pure y
-  | (Expr.forallE _ _ b _), 1 => pure b
-  | (Expr.letE _ y _ _ _) , 0 => pure y
-  | (Expr.letE _ _ a _ _) , 1 => pure a
-  | (Expr.letE _ _ _ b _) , 2 => pure b
-  | (Expr.proj _ _ b)     , 0 => pure b
-  | (Expr.mdata _ a)      , n => viewCoordRaw a n
-  | e                     , c => throwError "Bad coordinate {c} for {e}"
-
+private def viewCoordRaw (e : Expr) (n : Nat) : M Expr := do
+  match e, n with
+  | e,                3 => throwError "Can't viewRaw the type of {e}"
+  | .app f _,         0 => pure f
+  | .app _ a,         1 => pure a
+  | .lam _ y _ _,     0 => pure y
+  | .lam _ _ b _,     1 => pure b
+  | .forallE _ y _ _, 0 => pure y
+  | .forallE _ _ b _, 1 => pure b
+  | .letE _ y _ _ _,  0 => pure y
+  | .letE _ _ a _ _,  1 => pure a
+  | .letE _ _ _ b _,  2 => pure b
+  | .proj _ _ b,      0 => pure b
+  | .mdata _ a,       n => viewCoordRaw a n
+  | e,                c => throwError "Bad coordinate {c} for {e}"
 
 /-- Given a valid `SubExpr`, return the raw current expression without performing any instantiation.
 If the given `SubExpr` has a type subexpression coordinate, then throw an error.
@@ -148,21 +150,20 @@ def viewSubexpr (p : Pos) (root : Expr) : M Expr :=
   p.foldlM viewCoordRaw root
 
 private def viewBindersCoord : Nat → Expr → Option (Name × Expr)
-  | 1, (Expr.lam n y _ _)     => some (n, y)
-  | 1, (Expr.forallE n y _ _) => some (n, y)
-  | 2, (Expr.letE n y _ _ _)  => some (n, y)
-  | _, _                      => none
+  | 1, .lam n y _ _     => some (n, y)
+  | 1, .forallE n y _ _ => some (n, y)
+  | 2, .letE n y _ _ _  => some (n, y)
+  | _, _                => none
 
 /-- `viewBinders p e` returns a list of all of the binders (name, type) above the given position `p` in the root expression `e` -/
 def viewBinders (p : Pos) (root : Expr) : M (Array (Name × Expr)) := do
-  let (acc, _) ← p.foldlM (fun (acc, e) c => do
+  let (acc, _) ← p.foldlM (init := (#[], root)) fun (acc, e) c => do
     let e₂ ← viewCoordRaw e c
     let acc :=
       match viewBindersCoord c e with
       | none => acc
       | some b => acc.push b
     return (acc, e₂)
-  ) (#[], root)
   return acc
 
 /-- Returns the number of binders above a given subexpr position. -/

src/Lean/Meta/Instances.lean

@@ -114,7 +114,7 @@ For example:
 
 (The type of `inst` must not contain mvars.)
 -/
-partial def computeSynthOrder (inst : Expr) : MetaM (Array Nat) :=
+private partial def computeSynthOrder (inst : Expr) : MetaM (Array Nat) :=
   withReducible do
   let instTy ← inferType inst
 
@@ -217,8 +217,11 @@ def getGlobalInstancesIndex : CoreM (DiscrTree InstanceEntry) :=
 def getErasedInstances : CoreM (PHashSet Name) :=
   return Meta.instanceExtension.getState (← getEnv) |>.erased
 
+def isInstanceCore (env : Environment) (declName : Name) : Bool :=
+  Meta.instanceExtension.getState env |>.instanceNames.contains declName
+
 def isInstance (declName : Name) : CoreM Bool :=
-  return Meta.instanceExtension.getState (← getEnv) |>.instanceNames.contains declName
+  return isInstanceCore (← getEnv) declName
 
 def getInstancePriority? (declName : Name) : CoreM (Option Nat) := do
   let some entry := Meta.instanceExtension.getState (← getEnv) |>.instanceNames.find? declName | return none

src/Lean/Meta/LazyDiscrTree.lean

@@ -978,12 +978,13 @@ def createImportedDiscrTree [Monad m] [MonadLog m] [AddMessageContext m] [MonadO
 
 /-- 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,
+    fileName := ctx.fileName
+    fileMap := ctx.fileMap
+    options := ctx.options
+    maxRecDepth := ctx.maxRecDepth
+    maxHeartbeats := 0
+    ref := ctx.ref
+    diag := getDiag ctx.options
   }
 
 def findImportMatches

src/Lean/Meta/LevelDefEq.lean

@@ -16,26 +16,62 @@ namespace Lean.Meta
   That is, `lvl` is a proper level subterm of some `u_i`. -/
 private def strictOccursMax (lvl : Level) : Level → Bool
   | Level.max u v => visit u || visit v
-  | _               => false
+  | _             => false
 where
   visit : Level → Bool
     | Level.max u v => visit u || visit v
-    | u               => u != lvl && lvl.occurs u
+    | u             => u != lvl && lvl.occurs u
 
 /-- `mkMaxArgsDiff mvarId (max u_1 ... (mvar mvarId) ... u_n) v` => `max v u_1 ... u_n` -/
 private def mkMaxArgsDiff (mvarId : LMVarId) : Level → Level → Level
   | Level.max u v,     acc => mkMaxArgsDiff mvarId v <| mkMaxArgsDiff mvarId u acc
   | l@(Level.mvar id), acc => if id != mvarId then mkLevelMax' acc l else acc
-  | l,                   acc => mkLevelMax' acc l
+  | l,                 acc => mkLevelMax' acc l
 
 /--
-  Solve `?m =?= max ?m v` by creating a fresh metavariable `?n`
-  and assigning `?m := max ?n v` -/
+Solves `?m =?= max ?m v` by creating a fresh metavariable `?n`
+and assigning `?m := max ?n v`
+-/
 private def solveSelfMax (mvarId : LMVarId) (v : Level) : MetaM Unit := do
   assert! v.isMax
   let n ← mkFreshLevelMVar
   assignLevelMVar mvarId <| mkMaxArgsDiff mvarId v n
 
+/--
+Returns true if `v` is `max u ?m` (or variant). That is, we solve `u =?= max u ?m` as `?m := u`.
+This is an approximation. For example, we ignore the solution `?m := 0`.
+-/
+-- TODO: investigate whether we need to improve this approximation.
+private def tryApproxSelfMax (u v : Level) : MetaM Bool := do
+  match v with
+  | .max v' (.mvar mvarId) => solve v' mvarId
+  | .max (.mvar mvarId) v' => solve v' mvarId
+  | _ => return false
+where
+  solve (v' : Level) (mvarId : LMVarId) : MetaM Bool := do
+    if u == v' then
+      assignLevelMVar mvarId u
+      return true
+    else
+      return false
+
+/--
+Returns true if `u` of the form `max u₁ u₂` and `v` of the form `max u₁ ?w` (or variant).
+That is, we solve `max u₁ u₂ =?= max u₁ ?v` as `?v := u₂`.
+This is an approximation. For example, we ignore the solution `?w := max u₁ u₂`.
+-/
+-- TODO: investigate whether we need to improve this approximation.
+private def tryApproxMaxMax (u v : Level) : MetaM Bool := do
+  match u, v with
+  | .max u₁ u₂, .max v' (.mvar mvarId) => solve u₁ u₂ v' mvarId
+  | .max u₁ u₂, .max (.mvar mvarId) v' => solve u₁ u₂ v' mvarId
+  | _, _ => return false
+where
+  solve (u₁ u₂ v' : Level) (mvarId : LMVarId) : MetaM Bool := do
+    if u₁ == v' then assignLevelMVar mvarId u₂; return true
+    else if u₂ == v' then assignLevelMVar mvarId u₁; return true
+    else return false
+
 private def postponeIsLevelDefEq (lhs : Level) (rhs : Level) : MetaM Unit := do
   let ref ← getRef
   let ctx ← read
@@ -82,7 +118,13 @@ mutual
         match (← Meta.decLevel? v) with
         | some v => Bool.toLBool <$> isLevelDefEqAux u v
         | none   => return LBool.undef
-    | _, _ => return LBool.undef
+    | _, _ =>
+      if (← read).univApprox then
+        if (← tryApproxSelfMax u v) then
+          return LBool.true
+        if (← tryApproxMaxMax u v) then
+          return LBool.true
+      return LBool.undef
 
   @[export lean_is_level_def_eq]
   partial def isLevelDefEqAuxImpl : Level → Level → MetaM Bool

src/Lean/Meta/SynthInstance.lean

@@ -25,6 +25,12 @@ register_builtin_option synthInstance.maxSize : Nat := {
   descr := "maximum number of instances used to construct a solution in the type class instance synthesis procedure"
 }
 
+register_builtin_option backward.synthInstance.canonInstances : Bool := {
+  defValue := true
+  group    := "backward compatibility"
+  descr := "use optimization that relies on 'morally canonical' instances during type class resolution"
+}
+
 namespace SynthInstance
 
 def getMaxHeartbeats (opts : Options) : Nat :=
@@ -41,6 +47,14 @@ structure GeneratorNode where
   mctx            : MetavarContext
   instances       : Array Instance
   currInstanceIdx : Nat
+  /--
+  `typeHasMVars := true` if type of `mvar` contains metavariables.
+  We store this information to implement an optimization that relies on the fact
+  that instances are "morally canonical."
+  That is, we need to find at most one answer for this generator node if the type
+  does not have metavariables.
+  -/
+  typeHasMVars    : Bool
   deriving Inhabited
 
 structure ConsumerNode where
@@ -56,8 +70,8 @@ inductive Waiter where
   | root         : Waiter
 
 def Waiter.isRoot : Waiter → Bool
-  | Waiter.consumerNode _ => false
-  | Waiter.root           => true
+  | .consumerNode _ => false
+  | .root           => true
 
 /-!
   In tabled resolution, we creating a mapping from goals (e.g., `Coe Nat ?x`) to
@@ -98,10 +112,10 @@ partial def normLevel (u : Level) : M Level := do
   if !u.hasMVar then
     return u
   else match u with
-    | Level.succ v      => return u.updateSucc! (← normLevel v)
-    | Level.max v w     => return u.updateMax! (← normLevel v) (← normLevel w)
-    | Level.imax v w    => return u.updateIMax! (← normLevel v) (← normLevel w)
-    | Level.mvar mvarId =>
+    | .succ v      => return u.updateSucc! (← normLevel v)
+    | .max v w     => return u.updateMax! (← normLevel v) (← normLevel w)
+    | .imax v w    => return u.updateIMax! (← normLevel v) (← normLevel w)
+    | .mvar mvarId =>
       if (← getMCtx).getLevelDepth mvarId != (← getMCtx).depth then
         return u
       else
@@ -118,15 +132,15 @@ partial def normExpr (e : Expr) : M Expr := do
   if !e.hasMVar then
     pure e
   else match e with
-    | Expr.const _ us      => return e.updateConst! (← us.mapM normLevel)
-    | Expr.sort u          => return e.updateSort! (← normLevel u)
-    | Expr.app f a         => return e.updateApp! (← normExpr f) (← normExpr a)
-    | Expr.letE _ t v b _  => return e.updateLet! (← normExpr t) (← normExpr v) (← normExpr b)
-    | Expr.forallE _ d b _ => return e.updateForallE! (← normExpr d) (← normExpr b)
-    | Expr.lam _ d b _     => return e.updateLambdaE! (← normExpr d) (← normExpr b)
-    | Expr.mdata _ b       => return e.updateMData! (← normExpr b)
-    | Expr.proj _ _ b      => return e.updateProj! (← normExpr b)
-    | Expr.mvar mvarId     =>
+    | .const _ us      => return e.updateConst! (← us.mapM normLevel)
+    | .sort u          => return e.updateSort! (← normLevel u)
+    | .app f a         => return e.updateApp! (← normExpr f) (← normExpr a)
+    | .letE _ t v b _  => return e.updateLet! (← normExpr t) (← normExpr v) (← normExpr b)
+    | .forallE _ d b _ => return e.updateForallE! (← normExpr d) (← normExpr b)
+    | .lam _ d b _     => return e.updateLambdaE! (← normExpr d) (← normExpr b)
+    | .mdata _ b       => return e.updateMData! (← normExpr b)
+    | .proj _ _ b      => return e.updateProj! (← normExpr b)
+    | .mvar mvarId     =>
       if !(← mvarId.isAssignable) then
         return e
       else
@@ -202,7 +216,7 @@ def getInstances (type : Expr) : MetaM (Array Instance) := do
       let result := result.insertionSort fun e₁ e₂ => e₁.priority < e₂.priority
       let erasedInstances ← getErasedInstances
       let mut result ← result.filterMapM fun e => match e.val with
-        | Expr.const constName us =>
+        | .const constName us =>
           if erasedInstances.contains constName then
             return none
           else
@@ -234,6 +248,7 @@ def mkGeneratorNode? (key mvar : Expr) : MetaM (Option GeneratorNode) := do
     let mctx ← getMCtx
     return some {
       mvar, key, mctx, instances
+      typeHasMVars := mvarType.hasMVar
       currInstanceIdx := instances.size
     }
 
@@ -347,11 +362,14 @@ private def mkLambdaFVars' (xs : Array Expr) (e : Expr) : MetaM Expr :=
   If it succeeds, the result is a new updated metavariable context and a new list of subgoals.
   A subgoal is created for each instance implicit parameter of `inst`. -/
 def tryResolve (mvar : Expr) (inst : Instance) : MetaM (Option (MetavarContext × List Expr)) := do
+  if (← isDiagnosticsEnabled) then
+    if let .const declName _ := inst.val.getAppFn then
+      recordInstance declName
   let mvarType   ← inferType mvar
   let lctx       ← getLCtx
   let localInsts ← getLocalInstances
   forallTelescopeReducing mvarType fun xs mvarTypeBody => do
-    let ⟨subgoals, instVal, instTypeBody⟩ ← getSubgoals lctx localInsts xs inst
+    let { subgoals, instVal, instTypeBody } ← getSubgoals lctx localInsts xs inst
     withTraceNode `Meta.synthInstance.tryResolve (withMCtx (← getMCtx) do
         return m!"{exceptOptionEmoji ·} {← instantiateMVars mvarTypeBody} ≟ {← instantiateMVars instTypeBody}") do
     if (← isDefEq mvarTypeBody instTypeBody) then
@@ -373,7 +391,7 @@ def tryAnswer (mctx : MetavarContext) (mvar : Expr) (answer : Answer) : SynthM (
 
 /-- Move waiters that are waiting for the given answer to the resume stack. -/
 def wakeUp (answer : Answer) : Waiter → SynthM Unit
-  | Waiter.root               => do
+  | .root               => do
     /- Recall that we now use `ignoreLevelMVarDepth := true`. Thus, we should allow solutions
        containing universe metavariables, and not check `answer.result.paramNames.isEmpty`.
        We use `openAbstractMVarsResult` to construct the universe metavariables
@@ -383,7 +401,7 @@ def wakeUp (answer : Answer) : Waiter → SynthM Unit
     else
       let (_, _, answerExpr) ← openAbstractMVarsResult answer.result
       trace[Meta.synthInstance] "skip answer containing metavariables {answerExpr}"
-  | Waiter.consumerNode cNode =>
+  | .consumerNode cNode =>
     modify fun s => { s with resumeStack := s.resumeStack.push (cNode, answer) }
 
 def isNewAnswer (oldAnswers : Array Answer) (answer : Answer) : Bool :=
@@ -407,18 +425,18 @@ private def mkAnswer (cNode : ConsumerNode) : MetaM Answer :=
 def addAnswer (cNode : ConsumerNode) : SynthM Unit := do
   withMCtx cNode.mctx do
   if cNode.size ≥ (← read).maxResultSize then
-      trace[Meta.synthInstance.answer] "{crossEmoji} {← instantiateMVars (← inferType cNode.mvar)}{Format.line}(size: {cNode.size} ≥ {(← read).maxResultSize})"
+    trace[Meta.synthInstance.answer] "{crossEmoji} {← instantiateMVars (← inferType cNode.mvar)}{Format.line}(size: {cNode.size} ≥ {(← read).maxResultSize})"
   else
     withTraceNode `Meta.synthInstance.answer
       (fun _ => return m!"{checkEmoji} {← instantiateMVars (← inferType cNode.mvar)}") do
     let answer ← mkAnswer cNode
     -- Remark: `answer` does not contain assignable or assigned metavariables.
     let key := cNode.key
-    let entry ← getEntry key
-    if isNewAnswer entry.answers answer then
-      let newEntry := { entry with answers := entry.answers.push answer }
+    let { waiters, answers } ← getEntry key
+    if isNewAnswer answers answer then
+      let newEntry := { waiters, answers := answers.push answer }
       modify fun s => { s with tableEntries := s.tableEntries.insert key newEntry }
-      entry.waiters.forM (wakeUp answer)
+      waiters.forM (wakeUp answer)
 
 /--
   Return `true` if a type of the form `(a_1 : A_1) → ... → (a_n : A_n) → B` has an unused argument `a_i`.
@@ -426,7 +444,7 @@ def addAnswer (cNode : ConsumerNode) : SynthM Unit := do
   Remark: This is syntactic check and no reduction is performed.
 -/
 private def hasUnusedArguments : Expr → Bool
-  | Expr.forallE _ _ b _ => !b.hasLooseBVar 0 || hasUnusedArguments b
+  | .forallE _ _ b _ => !b.hasLooseBVar 0 || hasUnusedArguments b
   | _ => false
 
 /--
@@ -539,6 +557,18 @@ def generate : SynthM Unit := do
     let inst := gNode.instances.get! idx
     let mctx := gNode.mctx
     let mvar := gNode.mvar
+    /- See comment at `typeHasMVars` -/
+    if backward.synthInstance.canonInstances.get (← getOptions) then
+      unless gNode.typeHasMVars do
+        if let some entry := (← get).tableEntries.find? key then
+          unless entry.answers.isEmpty do
+            /-
+            We already have an answer for this node, and since its type does not have metavariables,
+            we can skip other solutions because we assume instances are "morally canonical".
+            We have added this optimization to address issue #3996.
+            -/
+            modify fun s => { s with generatorStack := s.generatorStack.pop }
+            return
     discard do withMCtx mctx do
       withTraceNode `Meta.synthInstance
         (return m!"{exceptOptionEmoji ·} apply {inst.val} to {← instantiateMVars (← inferType mvar)}") do
@@ -667,7 +697,7 @@ private partial def preprocessArgs (type : Expr) (i : Nat) (args : Array Expr) (
 private def preprocessOutParam (type : Expr) : MetaM Expr :=
   forallTelescope type fun xs typeBody => do
     match typeBody.getAppFn with
-    | c@(Expr.const declName _) =>
+    | c@(.const declName _) =>
       let env ← getEnv
       if let some outParamsPos := getOutParamPositions? env declName then
         unless outParamsPos.isEmpty do
@@ -690,7 +720,8 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
   withTraceNode `Meta.synthInstance
     (return m!"{exceptOptionEmoji ·} {← instantiateMVars type}") do
   withConfig (fun config => { config with isDefEqStuckEx := true, transparency := TransparencyMode.instances,
-                                          foApprox := true, ctxApprox := true, constApprox := false }) do
+                                          foApprox := true, ctxApprox := true, constApprox := false, univApprox := false }) do
+  withReader (fun ctx => { ctx with inTypeClassResolution := true }) do
     let localInsts ← getLocalInstances
     let type ← instantiateMVars type
     let type ← preprocess type
@@ -775,8 +806,7 @@ def synthInstance (type : Expr) (maxResultSize? : Option Nat := none) : MetaM Ex
 private def synthPendingImp (mvarId : MVarId) : MetaM Bool := withIncRecDepth <| mvarId.withContext do
   let mvarDecl ← mvarId.getDecl
   match mvarDecl.kind with
-  | MetavarKind.syntheticOpaque =>
-    return false
+  | .syntheticOpaque => return false
   | _ =>
     /- Check whether the type of the given metavariable is a class or not. If yes, then try to synthesize
        it using type class resolution. We only do it for `synthetic` and `natural` metavariables. -/

src/Lean/Meta/Tactic/LinearArith/Solver.lean

@@ -81,6 +81,7 @@ def Poly.add (e₁ e₂ : Poly) : Poly :=
       else
         { val := r }
     termination_by (e₁.size - i₁, e₂.size - i₂)
+    decreasing_by all_goals decreasing_with decreasing_trivial_pre_omega
   go 0 0 #[]
 
 def Poly.combine (d₁ : Int) (e₁ : Poly) (d₂ : Int) (e₂ : Poly) : Poly :=
@@ -108,6 +109,7 @@ def Poly.combine (d₁ : Int) (e₁ : Poly) (d₂ : Int) (e₂ : Poly) : Poly :=
       else
         { val := r }
     termination_by (e₁.size - i₁, e₂.size - i₂)
+    decreasing_by all_goals decreasing_with decreasing_trivial_pre_omega
   go 0 0 #[]
 
 def Poly.eval? (e : Poly) (a : Assignment) : Option Rat := Id.run do

src/Lean/Meta/Tactic/Simp.lean

@@ -14,6 +14,7 @@ import Lean.Meta.Tactic.Simp.Simproc
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs
 import Lean.Meta.Tactic.Simp.RegisterCommand
 import Lean.Meta.Tactic.Simp.Attr
+import Lean.Meta.Tactic.Simp.Diagnostics
 
 namespace Lean
 

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

@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Diagnostics
+import Lean.Meta.Tactic.Simp.Types
+
+namespace Lean.Meta.Simp
+
+def mkSimpDiagSummary (counters : PHashMap Origin Nat) (usedCounters? : Option (PHashMap Origin Nat) := none) : MetaM DiagSummary := do
+  let threshold := diagnostics.threshold.get (← getOptions)
+  let entries := collectAboveThreshold counters threshold (fun _ => true) (lt := (· < ·))
+  if entries.isEmpty then
+    return {}
+  else
+    let mut data := #[]
+    for (thmId, counter) in entries do
+      let key ← match thmId with
+        | .decl declName _ _ =>
+          if (← getEnv).contains declName then
+            pure m!"{MessageData.ofConst (← mkConstWithLevelParams declName)}"
+          else
+            pure m!"{declName} (builtin simproc)"
+        | .fvar fvarId => pure m!"{mkFVar fvarId}"
+        | _ => pure thmId.key
+      let usedMsg ← if let some usedCounters := usedCounters? then
+        if let some c := usedCounters.find? thmId then pure s!", succeeded: {c}" else pure s!" {crossEmoji}" -- not used
+      else
+        pure ""
+      data := data.push m!"{if data.isEmpty then "  " else "\n"}{key} ↦ {counter}{usedMsg}"
+    return { data, max := entries[0]!.2 }
+
+def reportDiag (diag : Simp.Diagnostics) : MetaM Unit := do
+  if (← isDiagnosticsEnabled) then
+    let used ← mkSimpDiagSummary diag.usedThmCounter
+    let tried ← mkSimpDiagSummary diag.triedThmCounter diag.usedThmCounter
+    let congr ← mkDiagSummary diag.congrThmCounter
+    unless used.isEmpty && tried.isEmpty && congr.isEmpty do
+      let m := MessageData.nil
+      let m := appendSection m `simp "used theorems" used
+      let m := appendSection m `simp "tried theorems" tried
+      let m := appendSection m `simp "tried congruence theorems" congr
+      let m := m ++ "use `set_option diagnostics.threshold <num>` to control threshold for reporting counters"
+      logInfo m
+
+end Lean.Meta.Simp

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

@@ -8,6 +8,7 @@ import Lean.Meta.Transform
 import Lean.Meta.Tactic.Replace
 import Lean.Meta.Tactic.UnifyEq
 import Lean.Meta.Tactic.Simp.Rewrite
+import Lean.Meta.Tactic.Simp.Diagnostics
 import Lean.Meta.Match.Value
 
 namespace Lean.Meta
@@ -243,28 +244,26 @@ def getSimpLetCase (n : Name) (t : Expr) (b : Expr) : MetaM SimpLetCase := do
 
 /--
 We use `withNewlemmas` whenever updating the local context.
-We use `withFreshCache` because the local context affects `simp` rewrites
-even when `contextual := false`.
-For example, the `discharger` may inspect the current local context. The default
-discharger does that when applying equational theorems, and the user may
-use `(discharger := assumption)` or `(discharger := omega)`.
-If the `wishFreshCache` introduces performance issues, we can design a better solution
-for the default discharger which is used most of the time.
 -/
-def withNewLemmas {α} (xs : Array Expr) (f : SimpM α) : SimpM α := withFreshCache do
+def withNewLemmas {α} (xs : Array Expr) (f : SimpM α) : SimpM α := do
   if (← getConfig).contextual then
-    let mut s ← getSimpTheorems
-    let mut updated := false
-    for x in xs do
-      if (← isProof x) then
-        s ← s.addTheorem (.fvar x.fvarId!) x
-        updated := true
-    if updated then
-      withTheReader Context (fun ctx => { ctx with simpTheorems := s }) f
-    else
-      f
-  else
+    withFreshCache do
+      let mut s ← getSimpTheorems
+      let mut updated := false
+      for x in xs do
+        if (← isProof x) then
+          s ← s.addTheorem (.fvar x.fvarId!) x
+          updated := true
+      if updated then
+        withTheReader Context (fun ctx => { ctx with simpTheorems := s }) f
+      else
+        f
+  else if (← getMethods).wellBehavedDischarge then
+    -- See comment at `Methods.wellBehavedDischarge` to understand why
+    -- we don't have to reset the cache
     f
+  else
+    withFreshCache do f
 
 def simpProj (e : Expr) : SimpM Result := do
   match (← reduceProj? e) with
@@ -519,6 +518,7 @@ def processCongrHypothesis (h : Expr) : SimpM Bool := do
 
 /-- Try to rewrite `e` children using the given congruence theorem -/
 def trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : SimpM (Option Result) := withNewMCtxDepth do
+  recordCongrTheorem c.theoremName
   trace[Debug.Meta.Tactic.simp.congr] "{c.theoremName}, {e}"
   let thm ← mkConstWithFreshMVarLevels c.theoremName
   let (xs, bis, type) ← forallMetaTelescopeReducing (← inferType thm)
@@ -652,63 +652,75 @@ where
     trace[Meta.Tactic.simp.heads] "{repr e.toHeadIndex}"
     simpLoop e
 
-@[inline] def withSimpConfig (ctx : Context) (x : MetaM α) : MetaM α :=
+@[inline] def withSimpContext (ctx : Context) (x : MetaM α) : MetaM α :=
   withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| withReducible x
 
-def main (e : Expr) (ctx : Context) (usedSimps : UsedSimps := {}) (methods : Methods := {}) : MetaM (Result × UsedSimps) := do
-  let ctx := { ctx with config := (← ctx.config.updateArith) }
-  withSimpConfig ctx do withCatchingRuntimeEx do
+def main (e : Expr) (ctx : Context) (stats : Stats := {}) (methods : Methods := {}) : MetaM (Result × Stats) := do
+  let ctx := { ctx with config := (← ctx.config.updateArith), lctxInitIndices := (← getLCtx).numIndices }
+  withSimpContext ctx do
+    let (r, s) ← simpMain e methods.toMethodsRef ctx |>.run { stats with }
+    trace[Meta.Tactic.simp.numSteps] "{s.numSteps}"
+    return (r, { s with })
+where
+  simpMain (e : Expr) : SimpM Result := withCatchingRuntimeEx do
     try
-      withoutCatchingRuntimeEx do
-        let (r, s) ← simp e methods.toMethodsRef ctx |>.run { usedTheorems := usedSimps }
-        trace[Meta.Tactic.simp.numSteps] "{s.numSteps}"
-        return (r, s.usedTheorems)
+      withoutCatchingRuntimeEx <| simp e
     catch ex =>
-      if ex.isRuntime then throwNestedTacticEx `simp ex else throw ex
+      reportDiag (← get).diag
+      if ex.isRuntime then
+        throwNestedTacticEx `simp ex
+      else
+        throw ex
 
-def dsimpMain (e : Expr) (ctx : Context) (usedSimps : UsedSimps := {}) (methods : Methods := {}) : MetaM (Expr × UsedSimps) := do
-  withSimpConfig ctx do withCatchingRuntimeEx do
+def dsimpMain (e : Expr) (ctx : Context) (stats : Stats := {}) (methods : Methods := {}) : MetaM (Expr × Stats) := do
+  withSimpContext ctx do
+    let (r, s) ← dsimpMain e methods.toMethodsRef ctx |>.run { stats with }
+    pure (r, { s with })
+where
+  dsimpMain (e : Expr) : SimpM Expr := withCatchingRuntimeEx do
     try
-      withoutCatchingRuntimeEx do
-        let (r, s) ← dsimp e methods.toMethodsRef ctx |>.run { usedTheorems := usedSimps }
-        pure (r, s.usedTheorems)
+      withoutCatchingRuntimeEx <| dsimp e
     catch ex =>
-      if ex.isRuntime then throwNestedTacticEx `dsimp ex else throw ex
+      reportDiag (← get).diag
+      if ex.isRuntime then
+        throwNestedTacticEx `simp ex
+      else
+        throw ex
 
 end Simp
-open Simp (UsedSimps SimprocsArray)
+open Simp (SimprocsArray Stats)
 
 def simp (e : Expr) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
-    (usedSimps : UsedSimps := {}) : MetaM (Simp.Result × UsedSimps) := do profileitM Exception "simp" (← getOptions) do
+    (stats : Stats := {}) : MetaM (Simp.Result × Stats) := do profileitM Exception "simp" (← getOptions) do
   match discharge? with
-  | none   => Simp.main e ctx usedSimps (methods := Simp.mkDefaultMethodsCore simprocs)
-  | some d => Simp.main e ctx usedSimps (methods := Simp.mkMethods simprocs d)
+  | none   => Simp.main e ctx stats (methods := Simp.mkDefaultMethodsCore simprocs)
+  | some d => Simp.main e ctx stats (methods := Simp.mkMethods simprocs d (wellBehavedDischarge := false))
 
 def dsimp (e : Expr) (ctx : Simp.Context) (simprocs : SimprocsArray := #[])
-    (usedSimps : UsedSimps := {}) : MetaM (Expr × UsedSimps) := do profileitM Exception "dsimp" (← getOptions) do
-  Simp.dsimpMain e ctx usedSimps (methods := Simp.mkDefaultMethodsCore simprocs )
+    (stats : Stats := {}) : MetaM (Expr × Stats) := do profileitM Exception "dsimp" (← getOptions) do
+  Simp.dsimpMain e ctx stats (methods := Simp.mkDefaultMethodsCore simprocs )
 
 /-- See `simpTarget`. This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/
 def simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
-    (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
+    (mayCloseGoal := true) (stats : Stats := {}) : MetaM (Option MVarId × Stats) := do
   let target ← instantiateMVars (← mvarId.getType)
-  let (r, usedSimps) ← simp target ctx simprocs discharge? usedSimps
+  let (r, stats) ← simp target ctx simprocs discharge? stats
   if mayCloseGoal && r.expr.isTrue then
     match r.proof? with
     | some proof => mvarId.assign (← mkOfEqTrue proof)
     | none => mvarId.assign (mkConst ``True.intro)
-    return (none, usedSimps)
+    return (none, stats)
   else
-    return (← applySimpResultToTarget mvarId target r, usedSimps)
+    return (← applySimpResultToTarget mvarId target r, stats)
 
 /--
   Simplify the given goal target (aka type). Return `none` if the goal was closed. Return `some mvarId'` otherwise,
   where `mvarId'` is the simplified new goal. -/
 def simpTarget (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
-    (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) :=
+    (mayCloseGoal := true) (stats : Stats := {}) : MetaM (Option MVarId × Stats) :=
   mvarId.withContext do
     mvarId.checkNotAssigned `simp
-    simpTargetCore mvarId ctx simprocs discharge? mayCloseGoal usedSimps
+    simpTargetCore mvarId ctx simprocs discharge? mayCloseGoal stats
 
 /--
   Apply the result `r` for `prop` (which is inhabited by `proof`). Return `none` if the goal was closed. Return `some (proof', prop')`
@@ -740,9 +752,9 @@ def applySimpResultToFVarId (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result
 
   This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/
 def simpStep (mvarId : MVarId) (proof : Expr) (prop : Expr) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
-    (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option (Expr × Expr) × UsedSimps) := do
-  let (r, usedSimps) ← simp prop ctx simprocs discharge? usedSimps
-  return (← applySimpResultToProp mvarId proof prop r (mayCloseGoal := mayCloseGoal), usedSimps)
+    (mayCloseGoal := true) (stats : Stats := {}) : MetaM (Option (Expr × Expr) × Stats) := do
+  let (r, stats) ← simp prop ctx simprocs discharge? stats
+  return (← applySimpResultToProp mvarId proof prop r (mayCloseGoal := mayCloseGoal), stats)
 
 def applySimpResultToLocalDeclCore (mvarId : MVarId) (fvarId : FVarId) (r : Option (Expr × Expr)) : MetaM (Option (FVarId × MVarId)) := do
   match r with
@@ -773,99 +785,99 @@ def applySimpResultToLocalDecl (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Res
     applySimpResultToLocalDeclCore mvarId fvarId (← applySimpResultToFVarId mvarId fvarId r mayCloseGoal)
 
 def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
-    (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option (FVarId × MVarId) × UsedSimps) := do
+    (mayCloseGoal := true) (stats : Stats := {}) : MetaM (Option (FVarId × MVarId) × Stats) := do
   mvarId.withContext do
     mvarId.checkNotAssigned `simp
     let type ← instantiateMVars (← fvarId.getType)
-    let (r, usedSimps) ← simpStep mvarId (mkFVar fvarId) type ctx simprocs discharge? mayCloseGoal usedSimps
-    return (← applySimpResultToLocalDeclCore mvarId fvarId r, usedSimps)
+    let (r, stats) ← simpStep mvarId (mkFVar fvarId) type ctx simprocs discharge? mayCloseGoal stats
+    return (← applySimpResultToLocalDeclCore mvarId fvarId r, stats)
 
 def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
     (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
-    (usedSimps : UsedSimps := {}) : MetaM (Option (Array FVarId × MVarId) × UsedSimps) := do
+    (stats : Stats := {}) : MetaM (Option (Array FVarId × MVarId) × Stats) := do
   mvarId.withContext do
     mvarId.checkNotAssigned `simp
     let mut mvarIdNew := mvarId
     let mut toAssert := #[]
     let mut replaced := #[]
-    let mut usedSimps := usedSimps
+    let mut stats := stats
     for fvarId in fvarIdsToSimp do
       let localDecl ← fvarId.getDecl
       let type ← instantiateMVars localDecl.type
       let ctx := { ctx with simpTheorems := ctx.simpTheorems.eraseTheorem (.fvar localDecl.fvarId) }
-      let (r, usedSimps') ← simp type ctx simprocs discharge? usedSimps
-      usedSimps := usedSimps'
+      let (r, stats') ← simp type ctx simprocs discharge? stats
+      stats := stats'
       match r.proof? with
       | some _ => match (← applySimpResultToProp mvarIdNew (mkFVar fvarId) type r) with
-        | none => return (none, usedSimps)
+        | none => return (none, stats)
         | some (value, type) => toAssert := toAssert.push { userName := localDecl.userName, type := type, value := value }
       | none =>
         if r.expr.isFalse then
           mvarIdNew.assign (← mkFalseElim (← mvarIdNew.getType) (mkFVar fvarId))
-          return (none, usedSimps)
+          return (none, stats)
         -- TODO: if there are no forwards dependencies we may consider using the same approach we used when `r.proof?` is a `some ...`
         -- Reason: it introduces a `mkExpectedTypeHint`
         mvarIdNew ← mvarIdNew.replaceLocalDeclDefEq fvarId r.expr
         replaced := replaced.push fvarId
     if simplifyTarget then
-      match (← simpTarget mvarIdNew ctx simprocs discharge? (usedSimps := usedSimps)) with
-      | (none, usedSimps') => return (none, usedSimps')
-      | (some mvarIdNew', usedSimps') => mvarIdNew := mvarIdNew'; usedSimps := usedSimps'
+      match (← simpTarget mvarIdNew ctx simprocs discharge? (stats := stats)) with
+      | (none, stats') => return (none, stats')
+      | (some mvarIdNew', stats') => mvarIdNew := mvarIdNew'; stats := stats'
     let (fvarIdsNew, mvarIdNew') ← mvarIdNew.assertHypotheses toAssert
     mvarIdNew := mvarIdNew'
     let toClear := fvarIdsToSimp.filter fun fvarId => !replaced.contains fvarId
     mvarIdNew ← mvarIdNew.tryClearMany toClear
     if ctx.config.failIfUnchanged && mvarId == mvarIdNew then
       throwError "simp made no progress"
-    return (some (fvarIdsNew, mvarIdNew), usedSimps)
+    return (some (fvarIdsNew, mvarIdNew), stats)
 
 def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
-    (usedSimps : UsedSimps := {}) : MetaM (TacticResultCNM × UsedSimps) := mvarId.withContext do
+    (stats : Stats := {}) : MetaM (TacticResultCNM × Stats) := mvarId.withContext do
   let mut ctx := ctx
   for h in (← getPropHyps) do
     let localDecl ← h.getDecl
     let proof  := localDecl.toExpr
     let simpTheorems ← ctx.simpTheorems.addTheorem (.fvar h) proof
     ctx := { ctx with simpTheorems }
-  match (← simpTarget mvarId ctx simprocs discharge? (usedSimps := usedSimps)) with
-  | (none, usedSimps) => return (TacticResultCNM.closed, usedSimps)
-  | (some mvarId', usedSimps') =>
+  match (← simpTarget mvarId ctx simprocs discharge? (stats := stats)) with
+  | (none, stats) => return (TacticResultCNM.closed, stats)
+  | (some mvarId', stats') =>
     if (← mvarId.getType) == (← mvarId'.getType) then
-      return (TacticResultCNM.noChange, usedSimps)
+      return (TacticResultCNM.noChange, stats)
     else
-      return (TacticResultCNM.modified mvarId', usedSimps')
+      return (TacticResultCNM.modified mvarId', stats')
 
 def dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
-    (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
+    (stats : Stats := {}) : MetaM (Option MVarId × Stats) := do
    mvarId.withContext do
     mvarId.checkNotAssigned `simp
     let mut mvarIdNew := mvarId
-    let mut usedSimps : UsedSimps := usedSimps
+    let mut stats : Stats := stats
     for fvarId in fvarIdsToSimp do
       let type ← instantiateMVars (← fvarId.getType)
-      let (typeNew, usedSimps') ← dsimp type ctx simprocs
-      usedSimps := usedSimps'
+      let (typeNew, stats') ← dsimp type ctx simprocs
+      stats := stats'
       if typeNew.isFalse then
         mvarIdNew.assign (← mkFalseElim (← mvarIdNew.getType) (mkFVar fvarId))
-        return (none, usedSimps)
+        return (none, stats)
       if typeNew != type then
         mvarIdNew ← mvarIdNew.replaceLocalDeclDefEq fvarId typeNew
     if simplifyTarget then
       let target ← mvarIdNew.getType
-      let (targetNew, usedSimps') ← dsimp target ctx simprocs usedSimps
-      usedSimps := usedSimps'
+      let (targetNew, stats') ← dsimp target ctx simprocs stats
+      stats := stats'
       if targetNew.isTrue then
         mvarIdNew.assign (mkConst ``True.intro)
-        return (none, usedSimps)
+        return (none, stats)
       if let some (_, lhs, rhs) := targetNew.consumeMData.eq? then
         if (← withReducible <| isDefEq lhs rhs) then
           mvarIdNew.assign (← mkEqRefl lhs)
-          return (none, usedSimps)
+          return (none, stats)
       if target != targetNew then
         mvarIdNew ← mvarIdNew.replaceTargetDefEq targetNew
       pure () -- FIXME: bug in do notation if this is removed?
     if ctx.config.failIfUnchanged && mvarId == mvarIdNew then
       throwError "dsimp made no progress"
-    return (some mvarIdNew, usedSimps)
+    return (some mvarIdNew, stats)
 
 end Lean.Meta

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

@@ -109,6 +109,7 @@ where
       return false
 
 private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInfo) (val : Expr) (type : Expr) (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat) : SimpM (Option Result) := do
+  recordTriedSimpTheorem thm.origin
   let rec go (e : Expr) : SimpM (Option Result) := do
     if (← isDefEq lhs e) then
       unless (← synthesizeArgs thm.origin bis xs) do
@@ -406,6 +407,7 @@ def mkSEvalMethods : CoreM Methods := do
     dpre       := dpreDefault #[s]
     dpost      := dpostDefault #[s]
     discharge? := dischargeGround
+    wellBehavedDischarge := true
   }
 
 def mkSEvalContext : CoreM Context := do
@@ -493,10 +495,16 @@ where
     | .forallE _ d b _ => (d.isEq || d.isHEq || b.hasLooseBVar 0) && go b
     | _ => e.isFalse
 
-def dischargeUsingAssumption? (e : Expr) : SimpM (Option Expr) := do
+private def dischargeUsingAssumption? (e : Expr) : SimpM (Option Expr) := do
+  let lctxInitIndices := (← readThe Simp.Context).lctxInitIndices
+  let contextual := (← getConfig).contextual
   (← getLCtx).findDeclRevM? fun localDecl => do
     if localDecl.isImplementationDetail then
       return none
+    -- The following test is needed to ensure `dischargeUsingAssumption?` is a
+    -- well-behaved discharger. See comment at `Methods.wellBehavedDischarge`
+    else if !contextual && localDecl.index >= lctxInitIndices then
+      return none
     else if (← isDefEq e localDecl.type) then
       return some localDecl.toExpr
     else
@@ -545,16 +553,17 @@ def dischargeDefault? (e : Expr) : SimpM (Option Expr) := do
 
 abbrev Discharge := Expr → SimpM (Option Expr)
 
-def mkMethods (s : SimprocsArray) (discharge? : Discharge) : Methods := {
+def mkMethods (s : SimprocsArray) (discharge? : Discharge) (wellBehavedDischarge : Bool) : Methods := {
   pre        := preDefault s
   post       := postDefault s
   dpre       := dpreDefault s
   dpost      := dpostDefault s
-  discharge? := discharge?
+  discharge?
+  wellBehavedDischarge
 }
 
 def mkDefaultMethodsCore (simprocs : SimprocsArray) : Methods :=
-  mkMethods simprocs dischargeDefault?
+  mkMethods simprocs dischargeDefault? (wellBehavedDischarge := true)
 
 def mkDefaultMethods : CoreM Methods := do
   if simprocs.get (← getOptions) then

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

@@ -10,7 +10,7 @@ import Lean.Meta.Tactic.Simp.Main
 
 namespace Lean.Meta
 
-open Simp (UsedSimps SimprocsArray)
+open Simp (Stats SimprocsArray)
 
 namespace SimpAll
 
@@ -24,12 +24,13 @@ structure Entry where
   deriving Inhabited
 
 structure State where
-  modified  : Bool := false
-  mvarId    : MVarId
-  entries   : Array Entry := #[]
-  ctx       : Simp.Context
-  simprocs  : SimprocsArray
-  usedSimps : UsedSimps := {}
+  modified     : Bool := false
+  mvarId       : MVarId
+  entries      : Array Entry := #[]
+  ctx          : Simp.Context
+  simprocs     : SimprocsArray
+  usedTheorems : Simp.UsedSimps := {}
+  diag         : Simp.Diagnostics := {}
 
 abbrev M := StateRefT State MetaM
 
@@ -62,8 +63,8 @@ private partial def loop : M Bool := do
     -- We disable the current entry to prevent it to be simplified to `True`
     let simpThmsWithoutEntry := (← getSimpTheorems).eraseTheorem entry.id
     let ctx := { ctx with simpTheorems := simpThmsWithoutEntry }
-    let (r, usedSimps) ← simpStep (← get).mvarId entry.proof entry.type ctx simprocs (usedSimps := (← get).usedSimps)
-    modify fun s => { s with usedSimps }
+    let (r, stats) ← simpStep (← get).mvarId entry.proof entry.type ctx simprocs (stats := { (← get) with })
+    modify fun s => { s with usedTheorems := stats.usedTheorems, diag := stats.diag }
     match r with
     | none => return true -- closed the goal
     | some (proofNew, typeNew) =>
@@ -102,8 +103,8 @@ private partial def loop : M Bool := do
         }
   -- simplify target
   let mvarId := (← get).mvarId
-  let (r, usedSimps) ← simpTarget mvarId (← get).ctx simprocs (usedSimps := (← get).usedSimps)
-  modify fun s => { s with usedSimps }
+  let (r, stats) ← simpTarget mvarId (← get).ctx simprocs (stats := { (← get) with })
+  modify fun s => { s with usedTheorems := stats.usedTheorems, diag := stats.diag }
   match r with
   | none => return true
   | some mvarIdNew =>
@@ -143,12 +144,12 @@ def main : M (Option MVarId) := do
 
 end SimpAll
 
-def simpAll (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
+def simpAll (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (stats : Stats := {}) : MetaM (Option MVarId × Stats) := do
   mvarId.withContext do
-    let (r, s) ← SimpAll.main.run { mvarId, ctx, usedSimps, simprocs }
+    let (r, s) ← SimpAll.main.run { stats with mvarId, ctx, simprocs }
     if let .some mvarIdNew := r then
       if ctx.config.failIfUnchanged && mvarId == mvarIdNew then
         throwError "simp_all made no progress"
-    return (r, s.usedSimps)
+    return (r, { s with })
 
 end Lean.Meta

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

@@ -50,6 +50,9 @@ def Origin.key : Origin → Name
 
 instance : BEq Origin := ⟨(·.key == ·.key)⟩
 instance : Hashable Origin := ⟨(hash ·.key)⟩
+instance : LT Origin := ⟨(·.key.lt ·.key)⟩
+instance (a b : Origin) : Decidable (a < b) :=
+  inferInstanceAs (Decidable (a.key.lt b.key = true))
 
 /-
 Note: we want to use iota reduction when indexing instances. Otherwise,

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

@@ -90,6 +90,12 @@ structure Context where
   -/
   parent?           : Option Expr := none
   dischargeDepth    : UInt32 := 0
+  /--
+  Number of indices in the local context when starting `simp`.
+  We use this information to decide which assumptions we can use without
+  invalidating the cache.
+  -/
+  lctxInitIndices   : Nat := 0
   deriving Inhabited
 
 def Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool :=
@@ -98,11 +104,25 @@ def Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool :=
 -- We should use `PHashMap` because we backtrack the contents of `UsedSimps`
 abbrev UsedSimps := PHashMap Origin Nat
 
+structure Diagnostics where
+  /-- Number of times each simp theorem has been used/applied. -/
+  usedThmCounter : PHashMap Origin Nat := {}
+  /-- Number of times each simp theorem has been tried. -/
+  triedThmCounter : PHashMap Origin Nat := {}
+  /-- Number of times each congr theorem has been tried. -/
+  congrThmCounter : PHashMap Name Nat := {}
+  deriving Inhabited
+
 structure State where
   cache        : Cache := {}
   congrCache   : CongrCache := {}
   usedTheorems : UsedSimps := {}
   numSteps     : Nat := 0
+  diag         : Diagnostics := {}
+
+structure Stats where
+  usedTheorems : UsedSimps := {}
+  diag : Diagnostics := {}
 
 private opaque MethodsRefPointed : NonemptyType.{0}
 
@@ -118,6 +138,10 @@ opaque simp (e : Expr) : SimpM Result
 @[extern "lean_dsimp"]
 opaque dsimp (e : Expr) : SimpM Expr
 
+@[inline] def modifyDiag (f : Diagnostics → Diagnostics) : SimpM Unit := do
+  if (← isDiagnosticsEnabled) then
+    modify fun { cache, congrCache, usedTheorems, numSteps, diag } => { cache, congrCache, usedTheorems, numSteps, diag := f diag }
+
 /--
 Result type for a simplification procedure. We have `pre` and `post` simplication procedures.
 -/
@@ -230,11 +254,18 @@ structure Simprocs where
   deriving Inhabited
 
 structure Methods where
-  pre        : Simproc                    := fun _ => return .continue
-  post       : Simproc                    := fun e => return .done { expr := e }
-  dpre       : DSimproc                   := fun _ => return .continue
-  dpost      : DSimproc                   := fun e => return .done e
+  pre        : Simproc  := fun _ => return .continue
+  post       : Simproc  := fun e => return .done { expr := e }
+  dpre       : DSimproc := fun _ => return .continue
+  dpost      : DSimproc := fun e => return .done e
   discharge? : Expr → SimpM (Option Expr) := fun _ => return none
+  /--
+  `wellBehavedDischarge` must **not** be set to `true` IF `discharge?`
+  access local declarations with index >= `Context.lctxInitIndices` when
+  `contextual := false`.
+  Reason: it would prevent us from aggressively caching `simp` results.
+  -/
+  wellBehavedDischarge : Bool := true
   deriving Inhabited
 
 unsafe def Methods.toMethodsRefImpl (m : Methods) : MethodsRef :=
@@ -288,10 +319,19 @@ Save current cache, reset it, execute `x`, and then restore original cache.
   modify fun s => { s with cache := {} }
   try x finally modify fun s => { s with cache := cacheSaved }
 
-@[inline] def withDischarger (discharge? : Expr → SimpM (Option Expr)) (x : SimpM α) : SimpM α :=
-  withFreshCache <| withReader (fun r => { MethodsRef.toMethods r with discharge? }.toMethodsRef) x
+@[inline] def withDischarger (discharge? : Expr → SimpM (Option Expr)) (wellBehavedDischarge : Bool) (x : SimpM α) : SimpM α :=
+  withFreshCache <|
+  withReader (fun r => { MethodsRef.toMethods r with discharge?, wellBehavedDischarge }.toMethodsRef) x
+
+def recordTriedSimpTheorem (thmId : Origin) : SimpM Unit := do
+  modifyDiag fun { usedThmCounter, triedThmCounter, congrThmCounter } =>
+    let cNew := if let some c := triedThmCounter.find? thmId then c + 1 else 1
+    { usedThmCounter, triedThmCounter := triedThmCounter.insert thmId cNew, congrThmCounter }
 
 def recordSimpTheorem (thmId : Origin) : SimpM Unit := do
+  modifyDiag fun { usedThmCounter, triedThmCounter, congrThmCounter } =>
+    let cNew := if let some c := usedThmCounter.find? thmId then c + 1 else 1
+    { usedThmCounter := usedThmCounter.insert thmId cNew, triedThmCounter, congrThmCounter }
   /-
   If `thmId` is an equational theorem (e.g., `foo.eq_1`), we should record `foo` instead.
   See issue #3547.
@@ -311,6 +351,11 @@ def recordSimpTheorem (thmId : Origin) : SimpM Unit := do
     let n := s.usedTheorems.size
     { s with usedTheorems := s.usedTheorems.insert thmId n }
 
+def recordCongrTheorem (declName : Name) : SimpM Unit := do
+  modifyDiag fun { usedThmCounter, triedThmCounter, congrThmCounter } =>
+    let cNew := if let some c := congrThmCounter.find? declName then c + 1 else 1
+    { congrThmCounter := congrThmCounter.insert declName cNew, triedThmCounter, usedThmCounter }
+
 def Result.getProof (r : Result) : MetaM Expr := do
   match r.proof? with
   | some p => return p

src/Lean/Meta/WHNF.lean

@@ -344,7 +344,7 @@ inductive ProjReductionKind where
   | yesWithDelta
   /--
   Projections `s.i` are reduced at `whnfCore`, and `whnfAtMostI` is used at `s` during the process.
-  Recall that `whnfAtMostII` is like `whnf` but uses transparency at most `instances`.
+  Recall that `whnfAtMostI` is like `whnf` but uses transparency at most `instances`.
   This option is stronger than `yes`, but weaker than `yesWithDelta`.
   We use this option to ensure we reduce projections to prevent expensive defeq checks when unifying TC operations.
   When unifying e.g. `(@Field.toNeg α inst1).1 =?= (@Field.toNeg α inst2).1`,
@@ -608,10 +608,11 @@ where
           | .notMatcher   =>
             matchConstAux f' (fun _ => return e) fun cinfo lvls =>
               match cinfo with
-              | .recInfo rec    => reduceRec rec lvls e.getAppArgs (fun _ => return e) go
-              | .quotInfo rec   => reduceQuotRec rec e.getAppArgs (fun _ => return e) go
+              | .recInfo rec    => reduceRec rec lvls e.getAppArgs (fun _ => return e) (fun e => do recordUnfold cinfo.name; go e)
+              | .quotInfo rec   => reduceQuotRec rec e.getAppArgs (fun _ => return e) (fun e => do recordUnfold cinfo.name; go e)
               | c@(.defnInfo _) => do
                 if (← isAuxDef c.name) then
+                  recordUnfold c.name
                   deltaBetaDefinition c lvls e.getAppRevArgs (fun _ => return e) go
                 else
                   return e
@@ -706,7 +707,7 @@ mutual
         | some e =>
           match (← withReducibleAndInstances <| reduceProj? e.getAppFn) with
           | none   => return none
-          | some r => return mkAppN r e.getAppArgs |>.headBeta
+          | some r => recordUnfold declName; return mkAppN r e.getAppArgs |>.headBeta
       | _ => return none
     | _ => return none
 
@@ -729,8 +730,9 @@ mutual
         if fInfo.levelParams.length != fLvls.length then
           return none
         else
-          let unfoldDefault (_ : Unit) : MetaM (Option Expr) :=
+          let unfoldDefault (_ : Unit) : MetaM (Option Expr) := do
             if fInfo.hasValue then
+              recordUnfold fInfo.name
               deltaBetaDefinition fInfo fLvls e.getAppRevArgs (fun _ => pure none) (fun e => pure (some e))
             else
               return none
@@ -778,11 +780,13 @@ mutual
                   Thus, we should keep `return some r` until Mathlib has been ported to Lean 3.
                   Note that the `Vector` example above does not even work in Lean 3.
                 -/
-                let some recArgPos ← getStructuralRecArgPos? fInfo.name | return some r
+                let some recArgPos ← getStructuralRecArgPos? fInfo.name
+                  | recordUnfold fInfo.name; return some r
                 let numArgs := e.getAppNumArgs
                 if recArgPos >= numArgs then return none
                 let recArg := e.getArg! recArgPos numArgs
                 if !(← isConstructorApp (← whnfMatcher recArg)) then return none
+                recordUnfold fInfo.name
                 return some r
             | _ =>
               if (← getMatcherInfo? fInfo.name).isSome then
@@ -800,7 +804,7 @@ mutual
         unless cinfo.hasValue do return none
         deltaDefinition cinfo lvls
           (fun _ => pure none)
-          (fun e => pure (some e))
+          (fun e => do recordUnfold declName; pure (some e))
     | _ => return none
 end
 
@@ -833,11 +837,11 @@ def reduceRecMatcher? (e : Expr) : MetaM (Option Expr) := do
     | .reduced e => return e
     | _ => matchConstAux e.getAppFn (fun _ => pure none) fun cinfo lvls => do
       match cinfo with
-      | .recInfo «rec»  => reduceRec «rec» lvls e.getAppArgs (fun _ => pure none) (fun e => pure (some e))
-      | .quotInfo «rec» => reduceQuotRec «rec» e.getAppArgs (fun _ => pure none) (fun e => pure (some e))
+      | .recInfo «rec»  => reduceRec «rec» lvls e.getAppArgs (fun _ => pure none) (fun e => do recordUnfold cinfo.name; pure (some e))
+      | .quotInfo «rec» => reduceQuotRec «rec» e.getAppArgs (fun _ => pure none) (fun e => do recordUnfold cinfo.name; pure (some e))
       | c@(.defnInfo _) =>
         if (← isAuxDef c.name) then
-          deltaBetaDefinition c lvls e.getAppRevArgs (fun _ => pure none) (fun e => pure (some e))
+          deltaBetaDefinition c lvls e.getAppRevArgs (fun _ => pure none) (fun e => do recordUnfold c.name; pure (some e))
         else
           return none
       | _ => return none

src/Lean/Parser/Term.lean

@@ -870,7 +870,7 @@ def matchExprElseAlt (rhsParser : Parser) := leading_parser "| " >> ppIndent (ho
 def matchExprAlts (rhsParser : Parser) :=
   leading_parser withPosition $
     many (ppLine >> checkColGe "irrelevant" >> notFollowedBy (symbol "| " >> " _ ") "irrelevant" >> matchExprAlt rhsParser)
-    >> (ppLine >> checkColGe "irrelevant" >> matchExprElseAlt rhsParser)
+    >> (ppLine >> checkColGe "else-alternative for `match_expr`, i.e., `| _ => ...`" >> matchExprElseAlt rhsParser)
 @[builtin_term_parser] def matchExpr := leading_parser:leadPrec
   "match_expr " >> termParser >> " with" >> ppDedent (matchExprAlts termParser)
 

src/Lean/PrettyPrinter.lean

@@ -13,7 +13,10 @@ import Lean.ParserCompiler
 namespace Lean
 
 def PPContext.runCoreM {α : Type} (ppCtx : PPContext) (x : CoreM α) : IO α :=
-  Prod.fst <$> x.toIO { options := ppCtx.opts, currNamespace := ppCtx.currNamespace, openDecls := ppCtx.openDecls, fileName := "<PrettyPrinter>", fileMap := default }
+  Prod.fst <$> x.toIO { options := ppCtx.opts, currNamespace := ppCtx.currNamespace
+                        openDecls := ppCtx.openDecls
+                        fileName := "<PrettyPrinter>", fileMap := default
+                        diag     := getDiag ppCtx.opts }
                       { env := ppCtx.env, ngen := { namePrefix := `_pp_uniq } }
 
 def PPContext.runMetaM {α : Type} (ppCtx : PPContext) (x : MetaM α) : IO α :=
@@ -48,7 +51,9 @@ def ppExprWithInfos (e : Expr) (optsPerPos : Delaborator.OptionsPerPos := {}) (d
 
 @[export lean_pp_expr]
 def ppExprLegacy (env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) (e : Expr) : IO Format :=
-  Prod.fst <$> ((ppExpr e).run' { lctx := lctx } { mctx := mctx }).toIO { options := opts, fileName := "<PrettyPrinter>", fileMap := default } { env := env }
+  Prod.fst <$> ((withOptions (fun _ => opts) <| ppExpr e).run' { lctx := lctx } { mctx := mctx }).toIO
+    { fileName := "<PrettyPrinter>", fileMap := default }
+    { env := env }
 
 def ppTactic (stx : TSyntax `tactic) : CoreM Format := ppCategory `tactic stx
 
@@ -86,6 +91,7 @@ builtin_initialize
   ppFnsRef.set {
     ppExprWithInfos := fun ctx e => ctx.runMetaM <| withoutContext <| ppExprWithInfos e,
     ppTerm := fun ctx stx => ctx.runCoreM <| withoutContext <| ppTerm stx,
+    ppLevel := fun ctx l => return l.format (mvars := getPPMVars ctx.opts),
     ppGoal := fun ctx mvarId => ctx.runMetaM <| withoutContext <| Meta.ppGoal mvarId
   }
 

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -71,9 +71,11 @@ def delabSort : Delab := do
   match l with
   | Level.zero => `(Prop)
   | Level.succ .zero => `(Type)
-  | _ => match l.dec with
-    | some l' => `(Type $(Level.quote l' max_prec))
-    | none    => `(Sort $(Level.quote l max_prec))
+  | _ =>
+    let mvars ← getPPOption getPPMVars
+    match l.dec with
+    | some l' => `(Type $(Level.quote l' (prec := max_prec) (mvars := mvars)))
+    | none    => `(Sort $(Level.quote l (prec := max_prec) (mvars := mvars)))
 
 /--
 Delaborator for `const` expressions.
@@ -96,7 +98,8 @@ def delabConst : Delab := do
         c := c₀
     pure <| mkIdent c
   else
-    `($(mkIdent c).{$[$(ls.toArray.map quote)],*})
+    let mvars ← getPPOption getPPMVars
+    `($(mkIdent c).{$[$(ls.toArray.map (Level.quote · (prec := 0) (mvars := mvars)))],*})
 
   let stx ← maybeAddBlockImplicit stx
   if (← getPPOption getPPTagAppFns) then
@@ -526,64 +529,57 @@ def withOverApp (arity : Nat) (x : Delab) : Delab := do
 /-- State for `delabAppMatch` and helpers. -/
 structure AppMatchState where
   info        : MatcherInfo
-  matcherTy   : Expr
-  params      : Array Expr := #[]
+  /-- The `matcherTy` instantiated with universe levels and the matcher parameters, with a position at the type of
+  this application prefix. -/
+  matcherTy : SubExpr
+  /-- The motive, with the pi type version delaborated and the original expression version.
+  Once `AppMatchState` is complete, this is not `none`. -/
   motive      : Option (Term × Expr) := none
+  /-- Whether `pp.analysis.namedArg` was set for the motive argument. -/
   motiveNamed : Bool := false
+  /-- The delaborated discriminants, without `h :` annotations. -/
   discrs      : Array Term := #[]
+  /-- The collection of names used for the `h :` discriminant annotations, in order.
+  Uniquified names are constructed after the first phase. -/
+  hNames?     : Array (Option Name) := #[]
+  /-- Lambda subexpressions for each alternate. -/
+  alts        : Array SubExpr := #[]
+  /-- For each match alternative, the names to use for the pattern variables.
+  Each ends with `hNames?.filterMap id` exactly. -/
   varNames    : Array (Array Name) := #[]
+  /-- The delaborated right-hand sides for each match alternative. -/
   rhss        : Array Term := #[]
-  -- additional arguments applied to the result of the `match` expression
-  moreArgs    : Array Term := #[]
-/--
-  Extract arguments of motive applications from the matcher type.
-  For the example below: `#[#[`([])], #[`(a::as)]]` -/
-private partial def delabPatterns (st : AppMatchState) : DelabM (Array (Array Term)) :=
-  withReader (fun ctx => { ctx with inPattern := true, optionsPerPos := {} }) do
-    let ty ← instantiateForall st.matcherTy st.params
-    -- need to reduce `let`s that are lifted into the matcher type
-    forallTelescopeReducing ty fun params _ => do
-      -- skip motive and discriminators
-      let alts := Array.ofSubarray params[1 + st.discrs.size:]
-      alts.mapIdxM fun idx alt => do
-        let ty ← inferType alt
-        -- TODO: this is a hack; we are accessing the expression out-of-sync with the position
-        -- Currently, we reset `optionsPerPos` at the beginning of `delabPatterns` to avoid
-        -- incorrectly considering annotations.
-        withTheReader SubExpr ({ · with expr := ty }) $
-          usingNames st.varNames[idx]! do
-            withAppFnArgs (pure #[]) (fun pats => do pure $ pats.push (← delab))
-where
-  usingNames {α} (varNames : Array Name) (x : DelabM α) : DelabM α :=
-    usingNamesAux 0 varNames x
-  usingNamesAux {α} (i : Nat) (varNames : Array Name) (x : DelabM α) : DelabM α :=
-    if i < varNames.size then
-      withBindingBody varNames[i]! <| usingNamesAux (i+1) varNames x
-    else
-      x
 
-/-- Skip `numParams` binders, and execute `x varNames` where `varNames` contains the new binder names. -/
-private partial def skippingBinders {α} (numParams : Nat) (x : Array Name → DelabM α) : DelabM α :=
-  loop numParams #[]
+/--
+Skips `numParams` binders, and execute `x varNames` where `varNames` contains the new binder names.
+The `hNames` array is used for the last params.
+Helper for `delabAppMatch`.
+-/
+private partial def skippingBinders {α} (numParams : Nat) (hNames : Array Name) (x : Array Name → DelabM α) : DelabM α := do
+  loop 0 #[]
 where
-  loop : Nat → Array Name → DelabM α
-    | 0,   varNames => x varNames
-    | n+1, varNames => do
-      let rec visitLambda : DelabM α := do
-        let varName := (← getExpr).bindingName!.eraseMacroScopes
-        -- Pattern variables cannot shadow each other
-        if varNames.contains varName then
-          let varName := (← getLCtx).getUnusedName varName
-          withBindingBody varName do
-            loop n (varNames.push varName)
-        else
-          withBindingBodyUnusedName fun id => do
-            loop n (varNames.push id.getId)
+  loop (i : Nat) (varNames : Array Name) : DelabM α := do
+    let rec visitLambda : DelabM α := do
+      let varName := (← getExpr).bindingName!.eraseMacroScopes
+      if numParams - hNames.size ≤ i then
+        -- It is an "h annotation", so use the one we have already chosen.
+        let varName := hNames[i + hNames.size - numParams]!
+        withBindingBody varName do
+          loop (i + 1) (varNames.push varName)
+      else if varNames.contains varName then
+        -- Pattern variables must not shadow each other, so ensure a unique name
+        let varName := (← getLCtx).getUnusedName varName
+        withBindingBody varName do
+          loop (i + 1) (varNames.push varName)
+      else
+        withBindingBodyUnusedName fun id => do
+          loop (i + 1) (varNames.push id.getId)
+    if i < numParams then
       let e ← getExpr
       if e.isLambda then
         visitLambda
       else
-        -- eta expand `e`
+        -- Eta expand `e`
         let e ← forallTelescopeReducing (← inferType e) fun xs _ => do
           if xs.size == 1 && (← inferType xs[0]!).isConstOf ``Unit then
             -- `e` might be a thunk create by the dependent pattern matching compiler, and `xs[0]` may not even be a pattern variable.
@@ -594,75 +590,117 @@ where
           else
             mkLambdaFVars xs (mkAppN e xs)
         withTheReader SubExpr (fun ctx => { ctx with expr := e }) visitLambda
+    else x varNames
 
 /--
-  Delaborate applications of "matchers" such as
-  ```
-  List.map.match_1 : {α : Type _} →
-    (motive : List α → Sort _) →
-      (x : List α) → (Unit → motive List.nil) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
-  ```
+Delaborates applications of "matchers" such as
+```
+List.map.match_1 : {α : Type _} →
+  (motive : List α → Sort _) →
+    (x : List α) → (Unit → motive List.nil) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
+```
 -/
 @[builtin_delab app]
-def delabAppMatch : Delab := whenPPOption getPPNotation <| whenPPOption getPPMatch do
-  -- incrementally fill `AppMatchState` from arguments
-  let st ← withAppFnArgs
-    (do
-      let (Expr.const c us) ← getExpr | failure
-      let (some info) ← getMatcherInfo? c | failure
-      let matcherTy ← instantiateTypeLevelParams (← getConstInfo c) us
-      return { matcherTy, info : AppMatchState })
-    (fun st => do
-      if st.params.size < st.info.numParams then
-        return { st with params := st.params.push (← getExpr) }
-      else if st.motive.isNone then
-        -- store motive argument separately
-        let lamMotive ← getExpr
-        let piMotive ← lambdaTelescope lamMotive fun xs body => mkForallFVars xs body
-        -- TODO: pp.analyze has not analyzed `piMotive`, only `lamMotive`
-        -- Thus the binder types won't have any annotations
-        let piStx ← withTheReader SubExpr (fun cfg => { cfg with expr := piMotive }) delab
-        let named ← getPPOption getPPAnalysisNamedArg
-        return { st with motive := (piStx, lamMotive), motiveNamed := named }
-      else if st.discrs.size < st.info.numDiscrs then
-        let idx := st.discrs.size
-        let discr ← delab
-        if let some hName := st.info.discrInfos[idx]!.hName? then
-          -- TODO: we should check whether the corresponding binder name, matches `hName`.
-          -- If it does not we should pretty print this `match` as a regular application.
-          return { st with discrs := st.discrs.push (← `(matchDiscr| $(mkIdent hName) : $discr)) }
+partial def delabAppMatch : Delab := whenPPOption getPPNotation <| whenPPOption getPPMatch do
+  -- Check that this is a matcher, and then set up overapplication.
+  let Expr.const c us := (← getExpr).getAppFn | failure
+  let some info ← getMatcherInfo? c | failure
+  withOverApp info.arity do
+    -- First pass visiting the match application. Incrementally fills `AppMatchState`,
+    -- collecting information needed to delaborate the patterns and RHSs.
+    -- No need to visit the parameters themselves.
+    let st : AppMatchState ← withBoundedAppFnArgs (1 + info.numDiscrs + info.numAlts)
+      (do
+        let params := (← getExpr).getAppArgs
+        let matcherTy : SubExpr :=
+          { expr := ← instantiateForall (← instantiateTypeLevelParams (← getConstInfo c) us) params
+            pos := (← getPos).pushType }
+        guard <| ← isDefEq matcherTy.expr (← inferType (← getExpr))
+        return { info, matcherTy })
+      (fun st => do
+        if st.motive.isNone then
+          -- A motive for match notation is a type, so need to delaborate the lambda motive as a pi type.
+          let lamMotive ← getExpr
+          let piMotive ← lambdaTelescope lamMotive fun xs body => mkForallFVars xs body
+          -- TODO: pp.analyze has not analyzed `piMotive`, only `lamMotive`
+          -- Thus the binder types won't have any annotations.
+          -- Though, by using the same position we can use the body annotations
+          let piStx ← withTheReader SubExpr (fun cfg => { cfg with expr := piMotive }) delab
+          let named ← getPPOption getPPAnalysisNamedArg
+          return { st with motive := (piStx, lamMotive), motiveNamed := named }
+        else if st.discrs.size < st.info.numDiscrs then
+          return { st with discrs := st.discrs.push (← delab) }
+        else if st.alts.size < st.info.numAlts then
+          return { st with alts := st.alts.push (← readThe SubExpr) }
         else
-          return { st with discrs := st.discrs.push (← `(matchDiscr| $discr:term)) }
-      else if st.rhss.size < st.info.altNumParams.size then
-        /- We save the variables names here to be able to implement safe_shadowing.
-           The pattern delaboration must use the names saved here. -/
-        let (varNames, rhs) ← skippingBinders st.info.altNumParams[st.rhss.size]! fun varNames => do
-          let rhs ← delab
-          return (varNames, rhs)
-        return { st with rhss := st.rhss.push rhs, varNames := st.varNames.push varNames }
-      else
-        return { st with moreArgs := st.moreArgs.push (← delab) })
+          panic! "impossible, number of arguments does not match arity")
 
-  if st.discrs.size < st.info.numDiscrs || st.rhss.size < st.info.altNumParams.size then
-    -- underapplied
-    failure
+    -- Second pass, create names for the h parameters, come up with pattern variable names,
+    -- and delaborate the RHSs.
+    -- We need to create dummy variables for the `h :` annotation variables first because they
+    -- come *last* in each alternative.
+    let st ← withDummyBinders (st.info.discrInfos.map (·.hName?)) (← getExpr) fun hNames? => do
+      let hNames := hNames?.filterMap id
+      let mut st := {st with hNames? := hNames?}
+      for i in [0:st.alts.size] do
+        st ← withTheReader SubExpr (fun _ => st.alts[i]!) do
+          -- We save the variables names here to be able to implement safe shadowing.
+          -- The pattern delaboration must use the names saved here.
+          skippingBinders st.info.altNumParams[i]! hNames fun varNames => do
+            let rhs ← delab
+            return { st with rhss := st.rhss.push rhs, varNames := st.varNames.push varNames }
+      return st
 
-  match st.discrs, st.rhss with
-  | #[discr], #[] =>
-    let stx ← `(nomatch $discr)
-    return Syntax.mkApp stx st.moreArgs
-  | _,        #[] => failure
-  | _,        _   =>
-    let pats ← delabPatterns st
-    let stx ← do
+    if st.rhss.isEmpty then
+      `(nomatch $(st.discrs),*)
+    else
+      -- Third pass, delaborate patterns.
+      -- Extracts arguments of motive applications from the matcher type.
+      -- For the example in the docstring, yields `#[#[([])], #[(a::as)]]`.
+      let pats ← withReader (fun ctx => { ctx with inPattern := true, subExpr := st.matcherTy }) do
+        -- Need to reduce since there can be `let`s that are lifted into the matcher type
+        forallTelescopeReducing (← getExpr) fun afterParams _ => do
+          -- Skip motive and discriminators
+          let alts := Array.ofSubarray afterParams[1 + st.discrs.size:]
+          -- Visit minor premises
+          alts.mapIdxM fun idx alt => do
+            let altTy ← inferType alt
+            withTheReader SubExpr (fun ctx =>
+                { ctx with expr := altTy, pos := ctx.pos.pushNthBindingDomain (1 + st.discrs.size + idx) }) do
+              usingNames st.varNames[idx]! <|
+                withAppFnArgs (pure #[]) fun pats => return pats.push (← delab)
+      -- Finally, assemble
+      let discrs ← (st.hNames?.zip st.discrs).mapM fun (hName?, discr) =>
+        match hName? with
+        | none => `(matchDiscr| $discr:term)
+        | some hName => `(matchDiscr| $(mkIdent hName) : $discr)
       let (piStx, lamMotive) := st.motive.get!
       let opts ← getOptions
       -- TODO: disable the match if other implicits are needed?
       if ← pure st.motiveNamed <||> shouldShowMotive lamMotive opts then
-        `(match (motive := $piStx) $[$st.discrs:matchDiscr],* with $[| $pats,* => $st.rhss]*)
+        `(match (motive := $piStx) $[$discrs:matchDiscr],* with $[| $pats,* => $st.rhss]*)
       else
-        `(match $[$st.discrs:matchDiscr],* with $[| $pats,* => $st.rhss]*)
-    return Syntax.mkApp stx st.moreArgs
+        `(match $[$discrs:matchDiscr],* with $[| $pats,* => $st.rhss]*)
+where
+  /-- Adds hNames to the local context to reserve their names and runs `m` in that context. -/
+  withDummyBinders {α : Type} (hNames? : Array (Option Name)) (body : Expr)
+      (m : Array (Option Name) → DelabM α) (acc : Array (Option Name) := #[]) : DelabM α := do
+    let i := acc.size
+    if i < hNames?.size then
+      if let some name := hNames?[i]! then
+        let n' ← getUnusedName name body
+        withLocalDecl n' .default (.sort levelZero) (kind := .implDetail) fun _ =>
+          withDummyBinders hNames? body m (acc.push n')
+      else
+        withDummyBinders hNames? body m (acc.push none)
+    else
+      m acc
+
+  usingNames {α} (varNames : Array Name) (x : DelabM α) (i : Nat := 0) : DelabM α :=
+    if i < varNames.size then
+      withBindingBody varNames[i]! <| usingNames varNames x (i+1)
+    else
+      x
 
 /--
 Delaborates applications of the form `letFun v (fun x => b)` as `let_fun x := v; b`.

src/Lean/PrettyPrinter/Delaborator/Options.lean

@@ -82,7 +82,8 @@ register_builtin_option pp.instantiateMVars : Bool := {
 register_builtin_option pp.mvars : Bool := {
   defValue := true
   group    := "pp"
-  descr    := "(pretty printer) display names of metavariables when true, and otherwise display them as '?_'"
+  descr    := "(pretty printer) display names of metavariables when true, \
+    and otherwise display them as '?_' (for expression metavariables) and as '_' (for universe level metavariables)"
 }
 register_builtin_option pp.mvars.withType : Bool := {
   defValue := false

src/Lean/ReducibilityAttrs.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Attributes
+import Lean.ScopedEnvExtension
 
 namespace Lean
 
@@ -13,36 +14,100 @@ Reducibility status for a definition.
 -/
 inductive ReducibilityStatus where
   | reducible | semireducible | irreducible
-  deriving Inhabited, Repr
+  deriving Inhabited, Repr, BEq
 
-/--
-Environment extension for storing the reducibility attribute for definitions.
--/
-builtin_initialize reducibilityAttrs : EnumAttributes ReducibilityStatus ←
-  registerEnumAttributes
-    [(`reducible, "reducible", ReducibilityStatus.reducible),
-     (`semireducible, "semireducible", ReducibilityStatus.semireducible),
-     (`irreducible, "irreducible", ReducibilityStatus.irreducible)]
+builtin_initialize reducibilityCoreExt : PersistentEnvExtension (Name × ReducibilityStatus) (Name × ReducibilityStatus) (NameMap ReducibilityStatus) ←
+  registerPersistentEnvExtension {
+    name            := `reducibilityCore
+    mkInitial       := pure {}
+    addImportedFn   := fun _ _ => pure {}
+    addEntryFn      := fun (s : NameMap ReducibilityStatus) (p : Name × ReducibilityStatus) => s.insert p.1 p.2
+    exportEntriesFn := fun m =>
+      let r : Array (Name × ReducibilityStatus) := m.fold (fun a n p => a.push (n, p)) #[]
+      r.qsort (fun a b => Name.quickLt a.1 b.1)
+    statsFn         := fun s => "reducibility attribute core extension" ++ Format.line ++ "number of local entries: " ++ format s.size
+  }
+
+builtin_initialize reducibilityExtraExt : SimpleScopedEnvExtension (Name × ReducibilityStatus) (SMap Name ReducibilityStatus) ←
+  registerSimpleScopedEnvExtension {
+    name := `reducibilityExtra
+    initial := {}
+    addEntry := fun d (declName, status) => d.insert declName status
+    finalizeImport := fun d => d.switch
+  }
 
 @[export lean_get_reducibility_status]
-private def getReducibilityStatusImp (env : Environment) (declName : Name) : ReducibilityStatus :=
-  match reducibilityAttrs.getValue env declName with
-  | some s => s
-  | none   => ReducibilityStatus.semireducible
+def getReducibilityStatusCore (env : Environment) (declName : Name) : ReducibilityStatus :=
+  let m := reducibilityExtraExt.getState env
+  if let some status := m.find? declName then
+    status
+  else match env.getModuleIdxFor? declName with
+  | some modIdx =>
+    match (reducibilityCoreExt.getModuleEntries env modIdx).binSearch (declName, .semireducible) (fun a b => Name.quickLt a.1 b.1) with
+    | some (_, status) => status
+    | none => .semireducible
+  | none => (reducibilityCoreExt.getState env).find? declName |>.getD .semireducible
+
+def setReducibilityStatusCore (env : Environment) (declName : Name) (status : ReducibilityStatus) (attrKind : AttributeKind) (currNamespace : Name) : Environment :=
+  if attrKind matches .global then
+    match env.getModuleIdxFor? declName with
+    | some _ =>
+      -- Trying to set the attribute of a declaration defined in an imported module.
+      reducibilityExtraExt.addEntry env (declName, status)
+    | none =>
+      --
+      reducibilityCoreExt.addEntry env (declName, status)
+  else
+    -- `scoped` and `local` must be handled by `reducibilityExtraExt`
+    reducibilityExtraExt.addCore env (declName, status) attrKind currNamespace
 
 @[export lean_set_reducibility_status]
-private def setReducibilityStatusImp (env : Environment) (declName : Name) (s : ReducibilityStatus) : Environment :=
-  match reducibilityAttrs.setValue env declName s with
-  | Except.ok env => env
-  | _ => env -- TODO(Leo): we should extend EnumAttributes.setValue in the future and ensure it never fails
+private def setReducibilityStatusImp (env : Environment) (declName : Name) (status : ReducibilityStatus) : Environment :=
+  setReducibilityStatusCore env declName status .global .anonymous
+
+builtin_initialize
+  registerBuiltinAttribute {
+    ref             := by exact decl_name%
+    name            := `irreducible
+    descr           := "irreducible declaration"
+    add             := fun declName stx attrKind => do
+      Attribute.Builtin.ensureNoArgs stx
+      let ns ← getCurrNamespace
+      modifyEnv fun env => setReducibilityStatusCore env declName .irreducible attrKind ns
+    applicationTime := .afterTypeChecking
+ }
+
+builtin_initialize
+  registerBuiltinAttribute {
+    ref             := by exact decl_name%
+    name            := `reducible
+    descr           := "reducible declaration"
+    add             := fun declName stx attrKind => do
+      Attribute.Builtin.ensureNoArgs stx
+      let ns ← getCurrNamespace
+      modifyEnv fun env => setReducibilityStatusCore env declName .reducible attrKind ns
+    applicationTime := .afterTypeChecking
+ }
+
+builtin_initialize
+  registerBuiltinAttribute {
+    ref             := by exact decl_name%
+    name            := `semireducible
+    descr           := "semireducible declaration"
+    add             := fun declName stx attrKind => do
+      Attribute.Builtin.ensureNoArgs stx
+      let ns ← getCurrNamespace
+      modifyEnv fun env => setReducibilityStatusCore env declName .reducible attrKind ns
+    applicationTime := .afterTypeChecking
+ }
 
 /-- Return the reducibility attribute for the given declaration. -/
 def getReducibilityStatus [Monad m] [MonadEnv m] (declName : Name) : m ReducibilityStatus := do
-  return getReducibilityStatusImp (← getEnv) declName
+  return getReducibilityStatusCore (← getEnv) declName
 
 /-- Set the reducibility attribute for the given declaration. -/
 def setReducibilityStatus [Monad m] [MonadEnv m] (declName : Name) (s : ReducibilityStatus) : m Unit := do
-  modifyEnv fun env => setReducibilityStatusImp env declName s
+  modifyEnv fun env => setReducibilityStatusCore env declName s .global .anonymous
 
 /-- Set the given declaration as `[reducible]` -/
 def setReducibleAttribute [Monad m] [MonadEnv m] (declName : Name) : m Unit := do
@@ -51,13 +116,13 @@ def setReducibleAttribute [Monad m] [MonadEnv m] (declName : Name) : m Unit := d
 /-- Return `true` if the given declaration has been marked as `[reducible]`. -/
 def isReducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
   match (← getReducibilityStatus declName) with
-  | ReducibilityStatus.reducible => return true
+  | .reducible => return true
   | _ => return false
 
 /-- Return `true` if the given declaration has been marked as `[irreducible]` -/
 def isIrreducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
   match (← getReducibilityStatus declName) with
-  | ReducibilityStatus.irreducible => return true
+  | .irreducible => return true
   | _ => return false
 
 end Lean

src/Lean/ResolveName.lean

@@ -404,7 +404,7 @@ where
     for _ in [:revComponents.length] do
       match revComponents with
       | [] => return none
-      | cmpt::rest => candidate := cmpt ++ candidate; revComponents := rest
+      | cmpt::rest => candidate := Name.appendCore cmpt candidate; revComponents := rest
       match (← resolveGlobalName candidate) with
       | [(potentialMatch, _)] => if potentialMatch == n₀ then return some candidate else continue
       | _ => continue

src/Lean/ScopedEnvExtension.lean

@@ -146,11 +146,15 @@ def ScopedEnvExtension.addLocalEntry (ext : ScopedEnvExtension α β σ) (env :
     let top := { top with state := ext.descr.addEntry top.state b }
     ext.ext.setState env { s with stateStack := top :: states }
 
-def ScopedEnvExtension.add [Monad m] [MonadResolveName m] [MonadEnv m] (ext : ScopedEnvExtension α β σ) (b : β) (kind := AttributeKind.global) : m Unit := do
+def ScopedEnvExtension.addCore (env : Environment) (ext : ScopedEnvExtension α β σ) (b : β) (kind : AttributeKind) (namespaceName : Name) : Environment :=
   match kind with
-  | AttributeKind.global => modifyEnv (ext.addEntry · b)
-  | AttributeKind.local  => modifyEnv (ext.addLocalEntry · b)
-  | AttributeKind.scoped => modifyEnv (ext.addScopedEntry · (← getCurrNamespace) b)
+  | AttributeKind.global => ext.addEntry env b
+  | AttributeKind.local  => ext.addLocalEntry env b
+  | AttributeKind.scoped => ext.addScopedEntry env namespaceName b
+
+def ScopedEnvExtension.add [Monad m] [MonadResolveName m] [MonadEnv m] (ext : ScopedEnvExtension α β σ) (b : β) (kind := AttributeKind.global) : m Unit := do
+  let ns ← getCurrNamespace
+  modifyEnv (ext.addCore · b kind ns)
 
 def ScopedEnvExtension.getState [Inhabited σ] (ext : ScopedEnvExtension α β σ) (env : Environment) : σ :=
   match ext.ext.getState env |>.stateStack with

src/Lean/SubExpr.lean

@@ -54,24 +54,24 @@ def push (p : Pos) (c : Nat) : Pos :=
 variable {α : Type} [Inhabited α]
 
 /-- Fold over the position starting at the root and heading to the leaf-/
-partial def foldl  (f : α → Nat → α) (a : α) (p : Pos) : α :=
-  if p.isRoot then a else f (foldl f a p.tail) p.head
+partial def foldl  (f : α → Nat → α) (init : α) (p : Pos) : α :=
+  if p.isRoot then init else f (foldl f init p.tail) p.head
 
 /-- Fold over the position starting at the leaf and heading to the root-/
-partial def foldr  (f : Nat → α → α) (p : Pos) (a : α) : α :=
-  if p.isRoot then a else foldr f p.tail (f p.head a)
+partial def foldr  (f : Nat → α → α) (p : Pos) (init : α) : α :=
+  if p.isRoot then init else foldr f p.tail (f p.head init)
 
 /-- monad-fold over the position starting at the root and heading to the leaf -/
-partial def foldlM  [Monad M] (f : α → Nat → M α) (a : α) (p : Pos) : M α :=
+partial def foldlM  [Monad M] (f : α → Nat → M α) (init : α) (p : Pos) : M α :=
   have : Inhabited (M α) := inferInstance
-  if p.isRoot then pure a else do foldlM f a p.tail >>= (f · p.head)
+  if p.isRoot then pure init else do foldlM f init p.tail >>= (f · p.head)
 
 /-- monad-fold over the position starting at the leaf and finishing at the root. -/
-partial def foldrM [Monad M] (f : Nat → α → M α) (p : Pos) (a : α) : M α :=
-  if p.isRoot then pure a else f p.head a >>= foldrM f p.tail
+partial def foldrM [Monad M] (f : Nat → α → M α) (p : Pos) (init : α) : M α :=
+  if p.isRoot then pure init else f p.head init >>= foldrM f p.tail
 
 def depth (p : Pos) :=
-  p.foldr (fun _ => Nat.succ) 0
+  p.foldr (init := 0) fun _ => Nat.succ
 
 /-- Returns true if `pred` is true for each coordinate in `p`.-/
 def all (pred : Nat → Bool) (p : Pos) : Bool :=
@@ -98,6 +98,7 @@ def pushLetBody       (p : Pos) := p.push 2
 def pushAppFn         (p : Pos) := p.push 0
 def pushAppArg        (p : Pos) := p.push 1
 def pushProj          (p : Pos) := p.push 0
+def pushType          (p : Pos) := p.push Pos.typeCoord
 
 def pushNaryFn (numArgs : Nat) (p : Pos) : Pos :=
   p.asNat * (maxChildren ^ numArgs)
@@ -134,8 +135,8 @@ protected def fromString? : String → Except String Pos
 
 protected def fromString! (s : String) : Pos :=
   match Pos.fromString? s with
-  | Except.ok a => a
-  | Except.error e => panic! e
+  | .ok a => a
+  | .error e => panic! e
 
 instance : Ord Pos := show Ord Nat by infer_instance
 instance : DecidableEq Pos := show DecidableEq Nat by infer_instance
@@ -213,7 +214,7 @@ open SubExpr in
 `SubExpr.Pos` argument for tracking subexpression position. -/
 def Expr.traverseAppWithPos {M} [Monad M] (visit : Pos → Expr → M Expr) (p : Pos) (e : Expr) : M Expr :=
   match e with
-  | Expr.app f a =>
+  | .app f a =>
     e.updateApp!
       <$> traverseAppWithPos visit p.pushAppFn f
       <*> visit p.pushAppArg a

src/Lean/Util/FindExpr.lean

@@ -11,17 +11,17 @@ namespace Lean
 namespace Expr
 namespace FindImpl
 
-unsafe abbrev FindM := StateT (PtrSet Expr) Id
+unsafe abbrev FindM (m) := StateT (PtrSet Expr) m
 
-@[inline] unsafe def checkVisited (e : Expr) : OptionT FindM Unit := do
+@[inline] unsafe def checkVisited [Monad m] (e : Expr) : OptionT (FindM m) Unit := do
   if (← get).contains e then
     failure
   modify fun s => s.insert e
 
-unsafe def findM? (p : Expr → Bool) (e : Expr) : OptionT FindM Expr :=
+unsafe def findM? [Monad m] (p : Expr → m Bool) (e : Expr) : OptionT (FindM m) Expr :=
   let rec visit (e : Expr) := do
     checkVisited e
-    if p e then
+    if ← p e then
       pure e
     else match e with
       | .forallE _ d b _ => visit d <|> visit b
@@ -33,29 +33,35 @@ unsafe def findM? (p : Expr → Bool) (e : Expr) : OptionT FindM Expr :=
       | _                => failure
   visit e
 
-unsafe def findUnsafe? (p : Expr → Bool) (e : Expr) : Option Expr :=
-  Id.run <| findM? p e |>.run' mkPtrSet
+unsafe def findUnsafeM? {m} [Monad m] (p : Expr → m Bool) (e : Expr) : m (Option Expr) :=
+  findM? p e |>.run' mkPtrSet
+
+@[inline] unsafe def findUnsafe? (p : Expr → Bool) (e : Expr) : Option Expr := findUnsafeM? (m := Id) p e
 
 end FindImpl
 
-@[implemented_by FindImpl.findUnsafe?]
-def find? (p : Expr → Bool) (e : Expr) : Option Expr :=
-  /- This is a reference implementation for the unsafe one above -/
-  if p e then
-    some e
+@[implemented_by FindImpl.findUnsafeM?]
+/- This is a reference implementation for the unsafe one above -/
+def findM? [Monad m] (p : Expr → m Bool) (e : Expr) : m (Option Expr) := do
+  if ← p e then
+    return some e
   else match e with
-    | .forallE _ d b _ => find? p d <|> find? p b
-    | .lam _ d b _     => find? p d <|> find? p b
-    | .mdata _ b       => find? p b
-    | .letE _ t v b _  => find? p t <|> find? p v <|> find? p b
-    | .app f a         => find? p f <|> find? p a
-    | .proj _ _ b      => find? p b
-    | _                => none
+    | .forallE _ d b _ => findM? p d <||> findM? p b
+    | .lam _ d b _     => findM? p d <||> findM? p b
+    | .mdata _ b       => findM? p b
+    | .letE _ t v b _  => findM? p t <||> findM? p v <||> findM? p b
+    | .app f a         => findM? p f <||> findM? p a
+    | .proj _ _ b      => findM? p b
+    | _                => pure none
+
+@[implemented_by FindImpl.findUnsafe?]
+def find? (p : Expr → Bool) (e : Expr) : Option Expr := findM? (m := Id) p e
 
 /-- Return true if `e` occurs in `t` -/
 def occurs (e : Expr) (t : Expr) : Bool :=
   (t.find? fun s => s == e).isSome
 
+
 /--
   Return type for `findExt?` function argument.
 -/
@@ -66,7 +72,7 @@ inductive FindStep where
 
 namespace FindExtImpl
 
-unsafe def findM? (p : Expr → FindStep) (e : Expr) : OptionT FindImpl.FindM Expr :=
+unsafe def findM? (p : Expr → FindStep) (e : Expr) : OptionT (FindImpl.FindM Id) Expr :=
   visit e
 where
   visitApp (e : Expr) :=

src/Lean/Util/PPExt.lean

@@ -49,6 +49,7 @@ instance : Coe Format FormatWithInfos where
 structure PPFns where
   ppExprWithInfos : PPContext → Expr → IO FormatWithInfos
   ppTerm : PPContext → Term → IO Format
+  ppLevel : PPContext → Level → IO Format
   ppGoal : PPContext → MVarId → IO Format
   deriving Inhabited
 
@@ -56,6 +57,7 @@ builtin_initialize ppFnsRef : IO.Ref PPFns ←
   IO.mkRef {
     ppExprWithInfos := fun _ e => return format (toString e)
     ppTerm := fun ctx stx => return stx.raw.formatStx (some <| pp.raw.maxDepth.get ctx.opts)
+    ppLevel := fun _ l => return format l
     ppGoal := fun _ _ => return "goal"
   }
 
@@ -88,7 +90,10 @@ def ppTerm (ctx : PPContext) (stx : Term) : IO Format :=
       else
         pure f!"failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)"
 
+def ppLevel (ctx : PPContext) (l : Level) : IO Format :=
+  ppExt.getState ctx.env |>.ppLevel ctx l
+
 def ppGoal (ctx : PPContext) (mvarId : MVarId) : IO Format :=
-    ppExt.getState ctx.env |>.ppGoal ctx mvarId
+  ppExt.getState ctx.env |>.ppGoal ctx mvarId
 
 end Lean

src/Lean/Util/TestExtern.lean

@@ -8,8 +8,9 @@ import Lean.Elab.SyntheticMVars
 import Lean.Elab.Command
 import Lean.Meta.Tactic.Unfold
 import Lean.Meta.Eval
+import Lean.Compiler.ImplementedByAttr
 
-open Lean Elab Meta Command Term
+open Lean Elab Meta Command Term Compiler
 
 syntax (name := testExternCmd) "test_extern " term : command
 
@@ -18,14 +19,15 @@ syntax (name := testExternCmd) "test_extern " term : command
     let t ← elabTermAndSynthesize t none
     match t.getAppFn with
     | .const f _ =>
-      if isExtern (← getEnv) f then
+      let env ← getEnv
+      if isExtern env f || (getImplementedBy? env f).isSome then
         let t' := (← unfold t f).expr
-        let r := mkApp (.const ``reduceBool []) (← mkAppM ``BEq.beq #[t, t'])
+        let r := mkApp (.const ``reduceBool []) (← mkDecide (← mkEq t t'))
         if ! (← evalExpr Bool (.const ``Bool []) r) then
           throwError
             ("native implementation did not agree with reference implementation!\n" ++
             m!"Compare the outputs of:\n#eval {t}\n and\n#eval {t'}")
       else
-        throwError "test_extern: {f} does not have an @[extern] attribute"
+        throwError "test_extern: {f} does not have an @[extern] attribute or @[implemented_by] attribute"
     | _ => throwError "test_extern: expects a function application"
   | _ => throwUnsupportedSyntax

src/Lean/Widget/InteractiveDiagnostic.lean

@@ -144,7 +144,9 @@ where
   | ctx,       compose d₁ d₂            => do let d₁ ← go nCtx ctx d₁; let d₂ ← go nCtx ctx d₂; pure $ d₁ ++ d₂
   | ctx,       group d                  => Format.group <$> go nCtx ctx d
   | ctx,       .trace data header children => do
-    let header := (← go nCtx ctx header).nest 4
+    let mut header := (← go nCtx ctx header).nest 4
+    if data.startTime != 0 then
+      header := f!"[{data.stopTime - data.startTime}] {header}"
     let nodes ←
       if data.collapsed && !children.isEmpty then
         let children := children.map fun child =>

src/kernel/CMakeLists.txt

@@ -2,4 +2,4 @@ add_library(kernel OBJECT level.cpp expr.cpp expr_eq_fn.cpp
 for_each_fn.cpp replace_fn.cpp abstract.cpp instantiate.cpp
 local_ctx.cpp declaration.cpp environment.cpp type_checker.cpp
 init_module.cpp expr_cache.cpp equiv_manager.cpp quot.cpp
-inductive.cpp)
+inductive.cpp trace.cpp)

src/kernel/declaration.cpp

@@ -71,8 +71,10 @@ definition_val::definition_val(name const & n, names const & lparams, expr const
 
 definition_safety definition_val::get_safety() const { return static_cast<definition_safety>(lean_definition_val_get_safety(to_obj_arg())); }
 
-theorem_val::theorem_val(name const & n, names const & lparams, expr const & type, expr const & val):
-    object_ref(mk_cnstr(0, constant_val(n, lparams, type), val)) {
+extern "C" object * lean_mk_theorem_val(object * n, object * lparams, object * type, object * value, object * all);
+
+theorem_val::theorem_val(name const & n, names const & lparams, expr const & type, expr const & val, names const & all):
+    object_ref(lean_mk_theorem_val(n.to_obj_arg(), lparams.to_obj_arg(), type.to_obj_arg(), val.to_obj_arg(), all.to_obj_arg())) {
 }
 
 extern "C" object * lean_mk_opaque_val(object * n, object * lparams, object * type, object * value, uint8 is_unsafe, object * all);
@@ -205,6 +207,10 @@ declaration mk_definition(environment const & env, name const & n, names const &
     return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Definition), mk_definition_val(env, n, params, t, v, safety)));
 }
 
+declaration mk_theorem(name const & n, names const & lparams, expr const & type, expr const & val) {
+    return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Theorem), theorem_val(n, lparams, type, val, names(n))));
+}
+
 declaration mk_opaque(name const & n, names const & params, expr const & t, expr const & v, bool is_unsafe) {
     return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Opaque), opaque_val(n, params, t, v, is_unsafe, names(n))));
 }

src/kernel/declaration.h

@@ -112,12 +112,13 @@ public:
 typedef list_ref<definition_val> definition_vals;
 
 /*
-structure theorem_val extends constant_val :=
-(value : task expr)
+structure TheoremVal extends ConstantVal where
+  value : Expr
+  all : List Name := [name]
 */
 class theorem_val : public object_ref {
 public:
-    theorem_val(name const & n, names const & lparams, expr const & type, expr const & val);
+    theorem_val(name const & n, names const & lparams, expr const & type, expr const & val, names const & all);
     theorem_val(theorem_val const & other):object_ref(other) {}
     theorem_val(theorem_val && other):object_ref(other) {}
     theorem_val & operator=(theorem_val const & other) { object_ref::operator=(other); return *this; }
@@ -223,10 +224,12 @@ inline optional<declaration> none_declaration() { return optional<declaration>()
 inline optional<declaration> some_declaration(declaration const & o) { return optional<declaration>(o); }
 inline optional<declaration> some_declaration(declaration && o) { return optional<declaration>(std::forward<declaration>(o)); }
 
+bool use_unsafe(environment const & env, expr const & e);
 declaration mk_definition(name const & n, names const & lparams, expr const & t, expr const & v,
                           reducibility_hints const & hints, definition_safety safety = definition_safety::safe);
 declaration mk_definition(environment const & env, name const & n, names const & lparams, expr const & t, expr const & v,
                           definition_safety safety = definition_safety::safe);
+declaration mk_theorem(name const & n, names const & lparams, expr const & type, expr const & val);
 declaration mk_opaque(name const & n, names const & lparams, expr const & t, expr const & v, bool unsafe);
 declaration mk_axiom(name const & n, names const & lparams, expr const & t, bool unsafe = false);
 declaration mk_inductive_decl(names const & lparams, nat const & nparams, inductive_types const & types, bool is_unsafe);

src/kernel/init_module.cpp

@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "kernel/local_ctx.h"
 #include "kernel/inductive.h"
 #include "kernel/quot.h"
+#include "kernel/trace.h"
 
 namespace lean {
 void initialize_kernel_module() {
@@ -23,9 +24,11 @@ void initialize_kernel_module() {
     initialize_local_ctx();
     initialize_inductive();
     initialize_quot();
+    initialize_trace();
 }
 
 void finalize_kernel_module() {
+    finalize_trace();
     finalize_quot();
     finalize_inductive();
     finalize_local_ctx();

src/kernel/trace.cpp

@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 #include "util/option_declarations.h"
 #include "kernel/environment.h"
 #include "kernel/local_ctx.h"
-#include "library/trace.h"
+#include "kernel/trace.h"
 
 namespace lean {
 static name_set *            g_trace_classes = nullptr;