feat: add grind_pattern command

This PR introduces a command for specifying patterns used in the
heuristic instantiation of global theorems in the `grind` tactic.
Note that this PR only adds the parser.

doc/dev/release_checklist.md

@@ -5,6 +5,11 @@ See below for the checklist for release candidates.
 
 We'll use `v4.6.0` as the intended release version as a running example.
 
+- One week before the planned release, ensure that
+  (1) someone has written the release notes and
+  (2) someone has written the first draft of the release blog post.
+  If there is any material in `./releases_drafts/` on the `releases/v4.6.0` branch, then the release notes are not done.
+  (See the section "Writing the release notes".)
 - `git checkout releases/v4.6.0`
   (This branch should already exist, from the release candidates.)
 - `git pull`
@@ -81,7 +86,7 @@ We'll use `v4.6.0` as the intended release version as a running example.
       - Toolchain bump PR notes:
         - In addition to updating the `lean-toolchain` and `lakefile.lean`,
           in `.github/workflows/lean4checker.yml` update the line
-          `git checkout v4.6.0` to the appropriate tag.
+          `git checkout v4.6.0` to the appropriate tag. 
         - Push the PR branch to the main Mathlib repository rather than a fork, or CI may not work reliably
         - Create and push the tag
         - Create a new branch from the tag, push it, and open a pull request against `stable`.
@@ -134,13 +139,16 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
     git checkout -b releases/v4.7.0
     ```
 - In `RELEASES.md` replace `Development in progress` in the `v4.7.0` section with `Release notes to be written.`
-- It is essential to choose the nightly that will become the release candidate as early as possible, to avoid confusion.
+- We will rely on automatically generated release notes for release candidates,
+  and the written release notes will be used for stable versions only.
+  It is essential to choose the nightly that will become the release candidate as early as possible, to avoid confusion.
 - In `src/CMakeLists.txt`,
   - verify that you see `set(LEAN_VERSION_MINOR 7)` (for whichever `7` is appropriate); this should already have been updated when the development cycle began.
   - `set(LEAN_VERSION_IS_RELEASE 1)` (this should be a change; on `master` and nightly releases it is always `0`).
   - Commit your changes to `src/CMakeLists.txt`, and push.
 - `git tag v4.7.0-rc1`
 - `git push origin v4.7.0-rc1`
+- Ping the FRO Zulip that release notes need to be written. The release notes do not block completing the rest of this checklist.
 - Now wait, while CI runs.
   - You can monitor this at `https://github.com/leanprover/lean4/actions/workflows/ci.yml`, looking for the `v4.7.0-rc1` tag.
   - This step can take up to an hour.
@@ -240,12 +248,15 @@ Please read https://leanprover-community.github.io/contribute/tags_and_branches.
 
 # Writing the release notes
 
-Release notes are automatically generated from the commit history, using `script/release_notes.py`.
+We are currently trying a system where release notes are compiled all at once from someone looking through the commit history.
+The exact steps are a work in progress.
+Here is the general idea:
 
-Run this as `script/release_notes.py v4.6.0`, where `v4.6.0` is the *previous* release version. This will generate output
-for all commits since that tag. Note that there is output on both stderr, which should be manually reviewed,
-and on stdout, which should be manually copied to `RELEASES.md`.
-
-There can also be pre-written entries in `./releases_drafts`, which should be all incorporated in the release notes and then deleted from the branch.
+* The work is done right on the `releases/v4.6.0` branch sometime after it is created but before the stable release is made.
+  The release notes for `v4.6.0` will later be copied to `master` when we begin a new development cycle.
+* There can be material for release notes entries in commit messages.
+* There can also be pre-written entries in `./releases_drafts`, which should be all incorporated in the release notes and then deleted from the branch.
   See `./releases_drafts/README.md` for more information.
+* The release notes should be written from a downstream expert user's point of view.
 
+This section will be updated when the next release notes are written (for `v4.10.0`).

script/release_notes.py

@@ -1,145 +0,0 @@
-#!/usr/bin/env python3
-
-import sys
-import re
-import json
-import requests
-import subprocess
-from collections import defaultdict
-from git import Repo
-
-def get_commits_since_tag(repo, tag):
-    try:
-        tag_commit = repo.commit(tag)
-        commits = list(repo.iter_commits(f"{tag_commit.hexsha}..HEAD"))
-        return [
-            (commit.hexsha, commit.message.splitlines()[0], commit.message)
-            for commit in commits
-        ]
-    except Exception as e:
-        sys.stderr.write(f"Error retrieving commits: {e}\n")
-        sys.exit(1)
-
-def check_pr_number(first_line):
-    match = re.search(r"\(\#(\d+)\)$", first_line)
-    if match:
-        return int(match.group(1))
-    return None
-
-def fetch_pr_labels(pr_number):
-    try:
-        # Use gh CLI to fetch PR details
-        result = subprocess.run([
-            "gh", "api", f"repos/leanprover/lean4/pulls/{pr_number}"
-        ], capture_output=True, text=True, check=True)
-        pr_data = result.stdout
-        pr_json = json.loads(pr_data)
-        return [label["name"] for label in pr_json.get("labels", [])]
-    except subprocess.CalledProcessError as e:
-        sys.stderr.write(f"Failed to fetch PR #{pr_number} using gh: {e.stderr}\n")
-        return []
-
-def format_section_title(label):
-    title = label.replace("changelog-", "").capitalize()
-    if title == "Doc":
-        return "Documentation"
-    elif title == "Pp":
-        return "Pretty Printing"
-    return title
-
-def sort_sections_order():
-    return [
-        "Language",
-        "Library",
-        "Compiler",
-        "Pretty Printing",
-        "Documentation",
-        "Server",
-        "Lake",
-        "Other",
-        "Uncategorised"
-    ]
-
-def format_markdown_description(pr_number, description):
-    link = f"[#{pr_number}](https://github.com/leanprover/lean4/pull/{pr_number})"
-    return f"{link} {description}"
-
-def main():
-    if len(sys.argv) != 2:
-        sys.stderr.write("Usage: script.py <git-tag>\n")
-        sys.exit(1)
-
-    tag = sys.argv[1]
-    try:
-        repo = Repo(".")
-    except Exception as e:
-        sys.stderr.write(f"Error opening Git repository: {e}\n")
-        sys.exit(1)
-
-    commits = get_commits_since_tag(repo, tag)
-
-    sys.stderr.write(f"Found {len(commits)} commits since tag {tag}:\n")
-    for commit_hash, first_line, _ in commits:
-        sys.stderr.write(f"- {commit_hash}: {first_line}\n")
-
-    changelog = defaultdict(list)
-
-    for commit_hash, first_line, full_message in commits:
-        # Skip commits with the specific first lines
-        if first_line == "chore: update stage0" or first_line.startswith("chore: CI: bump "):
-            continue
-
-        pr_number = check_pr_number(first_line)
-
-        if not pr_number:
-            sys.stderr.write(f"No PR number found in {first_line}\n")
-            continue
-
-        # Remove the first line from the full_message for further processing
-        body = full_message[len(first_line):].strip()
-
-        paragraphs = body.split('\n\n')
-        second_paragraph = paragraphs[0] if len(paragraphs) > 0 else ""
-
-        labels = fetch_pr_labels(pr_number)
-
-        # Skip entries with the "changelog-no" label
-        if "changelog-no" in labels:
-            continue
-
-        report_errors = first_line.startswith("feat:") or first_line.startswith("fix:")
-
-        if not second_paragraph.startswith("This PR "):
-            if report_errors:
-                sys.stderr.write(f"No PR description found in commit:\n{commit_hash}\n{first_line}\n{body}\n\n")
-                fallback_description = re.sub(r":$", "", first_line.split(" ", 1)[1]).rsplit(" (#", 1)[0]
-                markdown_description = format_markdown_description(pr_number, fallback_description)
-            else:
-                continue
-        else:
-            markdown_description = format_markdown_description(pr_number, second_paragraph.replace("This PR ", ""))
-
-        changelog_labels = [label for label in labels if label.startswith("changelog-")]
-        if len(changelog_labels) > 1:
-            sys.stderr.write(f"Warning: Multiple changelog-* labels found for PR #{pr_number}: {changelog_labels}\n")
-
-        if not changelog_labels:
-            if report_errors:
-                sys.stderr.write(f"Warning: No changelog-* label found for PR #{pr_number}\n")
-            else:
-                continue
-
-        for label in changelog_labels:
-            changelog[label].append((pr_number, markdown_description))
-
-    section_order = sort_sections_order()
-    sorted_changelog = sorted(changelog.items(), key=lambda item: section_order.index(format_section_title(item[0])) if format_section_title(item[0]) in section_order else len(section_order))
-
-    for label, entries in sorted_changelog:
-        section_title = format_section_title(label) if label != "Uncategorised" else "Uncategorised"
-        print(f"## {section_title}\n")
-        for _, entry in sorted(entries, key=lambda x: x[0]):
-            print(f"* {entry}\n")
-
-if __name__ == "__main__":
-    main()

src/Init/Data/Array/Lemmas.lean

@@ -954,13 +954,18 @@ theorem size_eq_of_beq [BEq α] {xs ys : Array α} (h : xs == ys) : xs.size = ys
     rw [Bool.eq_iff_iff]
     simp +contextual
 
+private theorem beq_of_beq_singleton [BEq α] {a b : α} : #[a] == #[b] → a == b := by
+  intro h
+  have : isEqv #[a] #[b] BEq.beq = true := h
+  simp [isEqv, isEqvAux] at this
+  assumption
+
 @[simp] theorem reflBEq_iff [BEq α] : ReflBEq (Array α) ↔ ReflBEq α := by
   constructor
   · intro h
     constructor
     intro a
-    suffices (#[a] == #[a]) = true by
-      simpa only [instBEq, isEqv, isEqvAux, Bool.and_true]
+    apply beq_of_beq_singleton
     simp
   · intro h
     constructor
@@ -973,11 +978,9 @@ theorem size_eq_of_beq [BEq α] {xs ys : Array α} (h : xs == ys) : xs.size = ys
     · intro a b h
       apply singleton_inj.1
       apply eq_of_beq
-      simp only [instBEq, isEqv, isEqvAux]
-      simpa
+      simpa [instBEq, isEqv, isEqvAux]
     · intro a
-      suffices (#[a] == #[a]) = true by
-        simpa only [instBEq, isEqv, isEqvAux, Bool.and_true]
+      apply beq_of_beq_singleton
       simp
   · intro h
     constructor

src/Init/Data/Array/Lex/Lemmas.lean

@@ -17,8 +17,8 @@ namespace Array
 @[simp] theorem lt_toList [LT α] (l₁ l₂ : Array α) : l₁.toList < l₂.toList ↔ l₁ < l₂ := Iff.rfl
 @[simp] theorem le_toList [LT α] (l₁ l₂ : Array α) : l₁.toList ≤ l₂.toList ↔ l₁ ≤ l₂ := Iff.rfl
 
-theorem not_lt_iff_ge [LT α] (l₁ l₂ : List α) : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl
-theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : List α) :
+protected theorem not_lt_iff_ge [LT α] (l₁ l₂ : List α) : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl
+protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : List α) :
     ¬ l₁ ≤ l₂ ↔ l₂ < l₁ :=
   Decidable.not_not
 
@@ -135,7 +135,7 @@ protected theorem le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
     {l₁ l₂ : Array α} (h : l₁ < l₂) : l₁ ≤ l₂ :=
   List.le_of_lt h
 
-theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α]
+protected theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)]
     [Std.Total (¬ · < · : α → α → Prop)]
@@ -211,7 +211,7 @@ theorem lex_eq_false_iff_exists [BEq α] [PartialEquivBEq α] (lt : α → α
   cases l₂
   simp_all [List.lex_eq_false_iff_exists]
 
-theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : Array α} :
+protected theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : Array α} :
     l₁ < l₂ ↔
       (l₁ = l₂.take l₁.size ∧ l₁.size < l₂.size) ∨
         (∃ (i : Nat) (h₁ : i < l₁.size) (h₂ : i < l₂.size),
@@ -221,7 +221,7 @@ theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : Arr
   cases l₂
   simp [List.lt_iff_exists]
 
-theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α]
+protected theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)] {l₁ l₂ : Array α} :
@@ -258,14 +258,14 @@ theorem le_append_left [LT α] [Std.Irrefl (· < · : α → α → Prop)]
   cases l₂
   simpa using List.le_append_left
 
-theorem map_lt [LT α] [LT β]
+protected theorem map_lt [LT α] [LT β]
     {l₁ l₂ : Array α} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : l₁ < l₂) :
     map f l₁ < map f l₂ := by
   cases l₁
   cases l₂
   simpa using List.map_lt w h
 
-theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β]
+protected theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)]

src/Init/Data/List/Lex.lean

@@ -14,8 +14,8 @@ namespace List
 @[simp] theorem lex_lt [LT α] (l₁ l₂ : List α) : Lex (· < ·) l₁ l₂ ↔ l₁ < l₂ := Iff.rfl
 @[simp] theorem not_lex_lt [LT α] (l₁ l₂ : List α) : ¬ Lex (· < ·) l₁ l₂ ↔ l₂ ≤ l₁ := Iff.rfl
 
-theorem not_lt_iff_ge [LT α] (l₁ l₂ : List α) : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl
-theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : List α) :
+protected theorem not_lt_iff_ge [LT α] (l₁ l₂ : List α) : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl
+protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : List α) :
     ¬ l₁ ≤ l₂ ↔ l₂ < l₁ :=
   Decidable.not_not
 
@@ -260,7 +260,7 @@ protected theorem le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
   · exfalso
     exact h' h
 
-theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α]
+protected theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)]
     [Std.Total (¬ · < · : α → α → Prop)]
@@ -333,7 +333,7 @@ theorem lex_eq_true_iff_exists [BEq α] (lt : α → α → Bool) :
     cases l₂ with
     | nil => simp [lex]
     | cons b l₂ =>
-      simp only [lex_cons_cons, Bool.or_eq_true, Bool.and_eq_true, ih, isEqv, length_cons]
+      simp [lex_cons_cons, Bool.or_eq_true, Bool.and_eq_true, ih, isEqv, length_cons]
       constructor
       · rintro (hab | ⟨hab, ⟨h₁, h₂⟩ | ⟨i, h₁, h₂, w₁, w₂⟩⟩)
         · exact .inr ⟨0, by simp [hab]⟩
@@ -397,7 +397,7 @@ theorem lex_eq_false_iff_exists [BEq α] [PartialEquivBEq α] (lt : α → α
     cases l₂ with
     | nil => simp [lex]
     | cons b l₂ =>
-      simp only [lex_cons_cons, Bool.or_eq_false_iff, Bool.and_eq_false_imp, ih, isEqv,
+      simp [lex_cons_cons, Bool.or_eq_false_iff, Bool.and_eq_false_imp, ih, isEqv,
         Bool.and_eq_true, length_cons]
       constructor
       · rintro ⟨hab, h⟩
@@ -435,7 +435,7 @@ theorem lex_eq_false_iff_exists [BEq α] [PartialEquivBEq α] (lt : α → α
               simpa using w₁ (j + 1) (by simpa)
             · simpa using w₂
 
-theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} :
+protected theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} :
     l₁ < l₂ ↔
       (l₁ = l₂.take l₁.length ∧ l₁.length < l₂.length) ∨
         (∃ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length),
@@ -444,7 +444,7 @@ theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : Lis
   rw [← lex_eq_true_iff_lt, lex_eq_true_iff_exists]
   simp
 
-theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α]
+protected theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)] {l₁ l₂ : List α} :
@@ -489,7 +489,7 @@ theorem IsPrefix.le [LT α] [Std.Irrefl (· < · : α → α → Prop)]
   rcases h with ⟨_, rfl⟩
   apply le_append_left
 
-theorem map_lt [LT α] [LT β]
+protected theorem map_lt [LT α] [LT β]
     {l₁ l₂ : List α} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : l₁ < l₂) :
     map f l₁ < map f l₂ := by
   match l₁, l₂, h with
@@ -497,11 +497,11 @@ theorem map_lt [LT α] [LT β]
   | nil, cons b l₂, h => simp
   | cons a l₁, nil, h => simp at h
   | cons a l₁, cons _ l₂, .cons h =>
-    simp [cons_lt_cons_iff, map_lt w (by simpa using h)]
+    simp [cons_lt_cons_iff, List.map_lt w (by simpa using h)]
   | cons a l₁, cons b l₂, .rel h =>
     simp [cons_lt_cons_iff, w, h]
 
-theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β]
+protected theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)]
@@ -510,7 +510,7 @@ theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β
     [Std.Antisymm (¬ · < · : β → β → Prop)]
     {l₁ l₂ : List α} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : l₁ ≤ l₂) :
     map f l₁ ≤ map f l₂ := by
-  rw [le_iff_exists] at h ⊢
+  rw [List.le_iff_exists] at h ⊢
   obtain (h | ⟨i, h₁, h₂, w₁, w₂⟩) := h
   · left
     rw [h]

src/Init/Data/List/Zip.lean

@@ -259,7 +259,7 @@ theorem zip_map (f : α → γ) (g : β → δ) :
   | [], _ => rfl
   | _, [] => by simp only [map, zip_nil_right]
   | _ :: _, _ :: _ => by
-    simp only [map, zip_cons_cons, zip_map, Prod.map]; constructor
+    simp only [map, zip_cons_cons, zip_map, Prod.map]; try constructor -- TODO: remove try constructor after update stage0
 
 theorem zip_map_left (f : α → γ) (l₁ : List α) (l₂ : List β) :
     zip (l₁.map f) l₂ = (zip l₁ l₂).map (Prod.map f id) := by rw [← zip_map, map_id]

src/Init/Data/Vector/Lex.lean

@@ -19,6 +19,11 @@ namespace Vector
 @[simp] theorem lt_toList [LT α] (l₁ l₂ : Vector α n) : l₁.toList < l₂.toList ↔ l₁ < l₂ := Iff.rfl
 @[simp] theorem le_toList [LT α] (l₁ l₂ : Vector α n) : l₁.toList ≤ l₂.toList ↔ l₁ ≤ l₂ := Iff.rfl
 
+protected theorem not_lt_iff_ge [LT α] (l₁ l₂ : Vector α n) : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl
+protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : Vector α n) :
+    ¬ l₁ ≤ l₂ ↔ l₂ < l₁ :=
+  Decidable.not_not
+
 @[simp] theorem mk_lt_mk [LT α] :
     Vector.mk (α := α) (n := n) data₁ size₁ < Vector.mk data₂ size₂ ↔ data₁ < data₂ := Iff.rfl
 
@@ -133,7 +138,7 @@ protected theorem le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
     {l₁ l₂ : Vector α n} (h : l₁ < l₂) : l₁ ≤ l₂ :=
   Array.le_of_lt h
 
-theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α]
+protected theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)]
     [Std.Total (¬ · < · : α → α → Prop)]
@@ -200,14 +205,14 @@ theorem lex_eq_false_iff_exists [BEq α] [PartialEquivBEq α] (lt : α → α
   rcases l₂ with ⟨l₂, n₂⟩
   simp_all [Array.lex_eq_false_iff_exists, n₂]
 
-theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : Vector α n} :
+protected theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : Vector α n} :
     l₁ < l₂ ↔
       (∃ (i : Nat) (h : i < n), (∀ j, (hj : j < i) → l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i]) := by
   cases l₁
   cases l₂
   simp_all [Array.lt_iff_exists]
 
-theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α]
+protected theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)] {l₁ l₂ : Vector α n} :
@@ -230,12 +235,12 @@ theorem append_left_le [DecidableEq α] [LT α] [DecidableLT α]
     l₁ ++ l₂ ≤ l₁ ++ l₃ := by
   simpa using Array.append_left_le h
 
-theorem map_lt [LT α] [LT β]
+protected theorem map_lt [LT α] [LT β]
     {l₁ l₂ : Vector α n} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : l₁ < l₂) :
     map f l₁ < map f l₂ := by
   simpa using Array.map_lt w h
 
-theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β]
+protected theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)]

src/Init/Grind.lean

@@ -8,3 +8,5 @@ import Init.Grind.Norm
 import Init.Grind.Tactics
 import Init.Grind.Lemmas
 import Init.Grind.Cases
+import Init.Grind.Propagator
+import Init.Grind.Util

src/Init/Grind/Lemmas.lean

@@ -5,10 +5,49 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Core
+import Init.SimpLemmas
+import Init.Classical
+import Init.ByCases
 
 namespace Lean.Grind
 
 theorem intro_with_eq (p p' q : Prop) (he : p = p') (h : p' → q) : p → q :=
   fun hp => h (he.mp hp)
 
+/-! And -/
+
+theorem and_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a ∧ b) = b := by simp [h]
+theorem and_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a ∧ b) = a := by simp [h]
+theorem and_eq_of_eq_false_left {a b : Prop} (h : a = False) : (a ∧ b) = False := by simp [h]
+theorem and_eq_of_eq_false_right {a b : Prop} (h : b = False) : (a ∧ b) = False := by simp [h]
+
+theorem eq_true_of_and_eq_true_left {a b : Prop} (h : (a ∧ b) = True) : a = True := by simp_all
+theorem eq_true_of_and_eq_true_right {a b : Prop} (h : (a ∧ b) = True) : b = True := by simp_all
+
+/-! Or -/
+
+theorem or_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a ∨ b) = True := by simp [h]
+theorem or_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a ∨ b) = True := by simp [h]
+theorem or_eq_of_eq_false_left {a b : Prop} (h : a = False) : (a ∨ b) = b := by simp [h]
+theorem or_eq_of_eq_false_right {a b : Prop} (h : b = False) : (a ∨ b) = a := by simp [h]
+
+theorem eq_false_of_or_eq_false_left {a b : Prop} (h : (a ∨ b) = False) : a = False := by simp_all
+theorem eq_false_of_or_eq_false_right {a b : Prop} (h : (a ∨ b) = False) : b = False := by simp_all
+
+/-! Not -/
+
+theorem not_eq_of_eq_true {a : Prop} (h : a = True) : (Not a) = False := by simp [h]
+theorem not_eq_of_eq_false {a : Prop} (h : a = False) : (Not a) = True := by simp [h]
+
+theorem eq_false_of_not_eq_true {a : Prop} (h : (Not a) = True) : a = False := by simp_all
+theorem eq_true_of_not_eq_false {a : Prop} (h : (Not a) = False) : a = True := by simp_all
+
+theorem false_of_not_eq_self {a : Prop} (h : (Not a) = a) : False := by
+  by_cases a <;> simp_all
+
+/-! Eq -/
+
+theorem eq_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a = b) = b := by simp [h]
+theorem eq_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a = b) = a := by simp [h]
+
 end Lean.Grind

src/Init/Grind/Norm.lean

@@ -41,7 +41,7 @@ attribute [grind_norm] not_true
 attribute [grind_norm] not_false_eq_true
 
 -- Implication as a clause
-@[grind_norm] theorem imp_eq (p q : Prop) : (p → q) = (¬ p ∨ q) := by
+@[grind_norm↓] theorem imp_eq (p q : Prop) : (p → q) = (¬ p ∨ q) := by
   by_cases p <;> by_cases q <;> simp [*]
 
 -- And

src/Init/Grind/Propagator.lean

@@ -0,0 +1,27 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.NotationExtra
+
+namespace Lean.Parser
+
+/-- A user-defined propagator for the `grind` tactic. -/
+-- TODO: not implemented yet
+syntax (docComment)? "grind_propagator " (Tactic.simpPre <|> Tactic.simpPost) ident " (" ident ")" " := " term : command
+
+/-- A builtin propagator for the `grind` tactic. -/
+syntax (docComment)? "builtin_grind_propagator " ident (Tactic.simpPre <|> Tactic.simpPost) ident " := " term : command
+
+/-- Auxiliary attribute for builtin `grind` propagators. -/
+syntax (name := grindPropagatorBuiltinAttr) "builtin_grind_propagator" (Tactic.simpPre <|> Tactic.simpPost) ident : attr
+
+macro_rules
+  | `($[$doc?:docComment]? builtin_grind_propagator $propagatorName:ident $direction $op:ident := $body) => do
+    let propagatorType := `Lean.Meta.Grind.Propagator
+    `($[$doc?:docComment]? def $propagatorName:ident : $(mkIdent propagatorType) := $body
+      attribute [builtin_grind_propagator $direction $op] $propagatorName)
+
+end Lean.Parser

src/Init/Grind/Tactics.lean

@@ -19,7 +19,15 @@ structure Config where
   eager : Bool := false
   deriving Inhabited, BEq
 
+end Lean.Grind
+
+namespace Lean.Parser.Tactic
+
 /-!
 `grind` tactic and related tactics.
 -/
-end Lean.Grind
+
+-- TODO: configuration option, parameters
+syntax (name := grind) "grind" : tactic
+
+end Lean.Parser.Tactic

src/Init/Grind/Util.lean

@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Core
+
+namespace Lean.Grind
+
+/-- A helper gadget for annotating nested proofs in goals. -/
+def nestedProof (p : Prop) (h : p) : p := h
+
+set_option pp.proofs true
+
+theorem nestedProof_congr (p q : Prop) (h : p = q) (hp : p) (hq : q) : HEq (nestedProof p hp) (nestedProof q hq) := by
+  subst h; apply HEq.refl
+
+end Lean.Grind

src/Lean/Compiler/ExternAttr.lean

@@ -18,6 +18,7 @@ inductive ExternEntry where
   | inline   (backend : Name) (pattern : String)
   | standard (backend : Name) (fn : String)
   | foreign  (backend : Name) (fn : String)
+  deriving BEq, Hashable
 
 /--
 - `@[extern]`
@@ -36,7 +37,7 @@ inductive ExternEntry where
 structure ExternAttrData where
   arity?   : Option Nat := none
   entries  : List ExternEntry
-  deriving Inhabited
+  deriving Inhabited, BEq, Hashable
 
 -- def externEntry := leading_parser optional ident >> optional (nonReservedSymbol "inline ") >> strLit
 -- @[builtin_attr_parser] def extern     := leading_parser nonReservedSymbol "extern " >> optional numLit >> many externEntry

src/Lean/Compiler/LCNF/Basic.lean

@@ -7,6 +7,7 @@ prelude
 import Init.Data.List.BasicAux
 import Lean.Expr
 import Lean.Meta.Instances
+import Lean.Compiler.ExternAttr
 import Lean.Compiler.InlineAttrs
 import Lean.Compiler.Specialize
 import Lean.Compiler.LCNF.Types
@@ -429,6 +430,80 @@ where
     | .cases c => c.alts.forM fun alt => go alt.getCode
     | .unreach .. | .return .. | .jmp .. => return ()
 
+partial def Code.instantiateValueLevelParams (code : Code) (levelParams : List Name) (us : List Level) : Code :=
+  instCode code
+where
+  instLevel (u : Level) :=
+    u.instantiateParams levelParams us
+
+  instExpr (e : Expr) :=
+    e.instantiateLevelParamsNoCache levelParams us
+
+  instParams (ps : Array Param) :=
+    ps.mapMono fun p => p.updateCore (instExpr p.type)
+
+  instAlt (alt : Alt) :=
+    match alt with
+    | .default k => alt.updateCode (instCode k)
+    | .alt _ ps k => alt.updateAlt! (instParams ps) (instCode k)
+
+  instArg (arg : Arg) : Arg :=
+    match arg with
+    | .type e => arg.updateType! (instExpr e)
+    | .fvar .. | .erased => arg
+
+  instLetValue (e : LetValue) : LetValue :=
+    match e with
+    | .const declName vs args => e.updateConst! declName (vs.mapMono instLevel) (args.mapMono instArg)
+    | .fvar fvarId args => e.updateFVar! fvarId (args.mapMono instArg)
+    | .proj .. | .value .. | .erased => e
+
+  instLetDecl (decl : LetDecl) :=
+    decl.updateCore (instExpr decl.type) (instLetValue decl.value)
+
+  instFunDecl (decl : FunDecl) :=
+    decl.updateCore (instExpr decl.type) (instParams decl.params) (instCode decl.value)
+
+  instCode (code : Code) :=
+    match code with
+    | .let decl k => code.updateLet! (instLetDecl decl) (instCode k)
+    | .jp decl k | .fun decl k => code.updateFun! (instFunDecl decl) (instCode k)
+    | .cases c => code.updateCases! (instExpr c.resultType) c.discr (c.alts.mapMono instAlt)
+    | .jmp fvarId args => code.updateJmp! fvarId (args.mapMono instArg)
+    | .return .. => code
+    | .unreach type => code.updateUnreach! (instExpr type)
+
+inductive DeclValue where
+  | code (code : Code)
+  | extern (externAttrData : ExternAttrData)
+  deriving Inhabited, BEq
+
+partial def DeclValue.size : DeclValue → Nat
+  | .code c => c.size
+  | .extern .. => 0
+
+def DeclValue.mapCode (f : Code → Code) : DeclValue → DeclValue :=
+  fun
+    | .code c => .code (f c)
+    | .extern e => .extern e
+
+def DeclValue.mapCodeM [Monad m] (f : Code → m Code) : DeclValue → m DeclValue :=
+  fun v => do
+    match v with
+    | .code c => return .code (← f c)
+    | .extern .. => return v
+
+def DeclValue.forCodeM [Monad m] (f : Code → m Unit) : DeclValue → m Unit :=
+  fun v => do
+    match v with
+    | .code c => f c
+    | .extern .. => return ()
+
+def DeclValue.isCodeAndM [Monad m] (v : DeclValue) (f : Code → m Bool) : m Bool :=
+  match v with
+  | .code c => f c
+  | .extern .. => pure false
+
 /--
 Declaration being processed by the Lean to Lean compiler passes.
 -/
@@ -455,7 +530,7 @@ structure Decl where
   The body of the declaration, usually changes as it progresses
   through compiler passes.
   -/
-  value : Code
+  value : DeclValue
   /--
   We set this flag to true during LCNF conversion. When we receive
   a block of functions to be compiled, we set this flag to `true`
@@ -536,7 +611,9 @@ We use this function to decide whether we should inline a declaration tagged wit
 `[inline_if_reduce]` or not.
 -/
 def Decl.isCasesOnParam? (decl : Decl) : Option Nat :=
-  go decl.value
+  match decl.value with
+  | .code c => go c
+  | .extern .. => none
 where
   go (code : Code) : Option Nat :=
     match code with
@@ -550,49 +627,6 @@ def Decl.instantiateTypeLevelParams (decl : Decl) (us : List Level) : Expr :=
 def Decl.instantiateParamsLevelParams (decl : Decl) (us : List Level) : Array Param :=
   decl.params.mapMono fun param => param.updateCore (param.type.instantiateLevelParamsNoCache decl.levelParams us)
 
-partial def Decl.instantiateValueLevelParams (decl : Decl) (us : List Level) : Code :=
-  instCode decl.value
-where
-  instLevel (u : Level) :=
-    u.instantiateParams decl.levelParams us
-
-  instExpr (e : Expr) :=
-    e.instantiateLevelParamsNoCache decl.levelParams us
-
-  instParams (ps : Array Param) :=
-    ps.mapMono fun p => p.updateCore (instExpr p.type)
-
-  instAlt (alt : Alt) :=
-    match alt with
-    | .default k => alt.updateCode (instCode k)
-    | .alt _ ps k => alt.updateAlt! (instParams ps) (instCode k)
-
-  instArg (arg : Arg) : Arg :=
-    match arg with
-    | .type e => arg.updateType! (instExpr e)
-    | .fvar .. | .erased => arg
-
-  instLetValue (e : LetValue) : LetValue :=
-    match e with
-    | .const declName vs args => e.updateConst! declName (vs.mapMono instLevel) (args.mapMono instArg)
-    | .fvar fvarId args => e.updateFVar! fvarId (args.mapMono instArg)
-    | .proj .. | .value .. | .erased => e
-
-  instLetDecl (decl : LetDecl) :=
-    decl.updateCore (instExpr decl.type) (instLetValue decl.value)
-
-  instFunDecl (decl : FunDecl) :=
-    decl.updateCore (instExpr decl.type) (instParams decl.params) (instCode decl.value)
-
-  instCode (code : Code) :=
-    match code with
-    | .let decl k => code.updateLet! (instLetDecl decl) (instCode k)
-    | .jp decl k | .fun decl k => code.updateFun! (instFunDecl decl) (instCode k)
-    | .cases c => code.updateCases! (instExpr c.resultType) c.discr (c.alts.mapMono instAlt)
-    | .jmp fvarId args => code.updateJmp! fvarId (args.mapMono instArg)
-    | .return .. => code
-    | .unreach type => code.updateUnreach! (instExpr type)
-
 /--
 Return `true` if the arrow type contains an instance implicit argument.
 -/
@@ -693,7 +727,7 @@ where
       visit k
 
   go : StateM NameSet Unit :=
-    decls.forM fun decl => visit decl.value
+    decls.forM (·.value.forCodeM visit)
 
 def instantiateRangeArgs (e : Expr) (beginIdx endIdx : Nat) (args : Array Arg) : Expr :=
   if !e.hasLooseBVars then

src/Lean/Compiler/LCNF/Bind.lean

@@ -123,7 +123,10 @@ def FunDeclCore.etaExpand (decl : FunDecl) : CompilerM FunDecl := do
   decl.update decl.type params value
 
 def Decl.etaExpand (decl : Decl) : CompilerM Decl := do
-  let some (params, value) ← etaExpandCore? decl.type decl.params decl.value | return decl
-  return { decl with params, value }
+  match decl.value with
+  | .code code =>
+    let some (params, newCode) ← etaExpandCore? decl.type decl.params code | return decl
+    return { decl with params, value := .code newCode}
+  | .extern .. => return decl
 
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/CSE.lean

@@ -102,7 +102,7 @@ end CSE
 Common sub-expression elimination
 -/
 def Decl.cse (decl : Decl) : CompilerM Decl := do
-  let value ← decl.value.cse
+  let value ← decl.value.mapCodeM (·.cse)
   return { decl with value }
 
 def cse (phase : Phase := .base) (occurrence := 0) : Pass :=

src/Lean/Compiler/LCNF/Check.lean

@@ -261,7 +261,7 @@ def run (x : CheckM α) : CompilerM α :=
 end Check
 
 def Decl.check (decl : Decl) : CompilerM Unit := do
-  Check.run do Check.checkFunDeclCore decl.name decl.params decl.type decl.value
+  Check.run do decl.value.forCodeM (Check.checkFunDeclCore decl.name decl.params decl.type)
 
 /--
 Check whether every local declaration in the local context is used in one of given `decls`.
@@ -299,7 +299,7 @@ where
 
   visitDecl (decl : Decl) : StateM FVarIdHashSet Unit := do
     visitParams decl.params
-    visitCode decl.value
+    decl.value.forCodeM visitCode
 
   visitDecls (decls : Array Decl) : StateM FVarIdHashSet Unit :=
     decls.forM visitDecl

src/Lean/Compiler/LCNF/CompilerM.lean

@@ -148,7 +148,7 @@ def eraseCodeDecls (decls : Array CodeDecl) : CompilerM Unit := do
 
 def eraseDecl (decl : Decl) : CompilerM Unit := do
   eraseParams decl.params
-  eraseCode decl.value
+  decl.value.forCodeM eraseCode
 
 abbrev Decl.erase (decl : Decl) : CompilerM Unit :=
   eraseDecl decl

src/Lean/Compiler/LCNF/DeclHash.lean

@@ -38,6 +38,7 @@ end
 instance : Hashable Code where
   hash c := hashCode c
 
+deriving instance Hashable for DeclValue
 deriving instance Hashable for Decl
 
-end Lean.Compiler.LCNF
+end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/ElimDead.lean

@@ -95,6 +95,6 @@ def Code.elimDead (code : Code) : CompilerM Code :=
   ElimDead.elimDead code |>.run' {}
 
 def Decl.elimDead (decl : Decl) : CompilerM Decl := do
-  return { decl with value := (← decl.value.elimDead) }
+  return { decl with value := (← decl.value.mapCodeM Code.elimDead) }
 
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/ElimDeadBranches.lean

@@ -513,7 +513,7 @@ def inferStep : InterpM Bool := do
     let currentVal ← getFunVal idx
     withReader (fun ctx => { ctx with currFnIdx := idx }) do
       decl.params.forM fun p => updateVarAssignment p.fvarId .top
-      interpCode decl.value
+      decl.value.forCodeM interpCode
     let newVal ← getFunVal idx
     if currentVal != newVal then
       return true
@@ -538,7 +538,7 @@ Use the information produced by the abstract interpreter to:
 -/
 partial def elimDead (assignment : Assignment) (decl : Decl) : CompilerM Decl := do
   trace[Compiler.elimDeadBranches] s!"Eliminating {decl.name} with {repr (← assignment.toArray |>.mapM (fun (name, val) => do return (toString (← getBinderName name), val)))}"
-  return { decl with value := (← go decl.value) }
+  return { decl with value := (← decl.value.mapCodeM go) }
 where
   go (code : Code) : CompilerM Code := do
     match code with

src/Lean/Compiler/LCNF/FixedParams.lean

@@ -141,8 +141,9 @@ partial def evalApp (declName : Name) (args : Array Arg) : FixParamM Unit := do
       let key := (declName, values)
       unless (← get).visited.contains key do
         modify fun s => { s with visited := s.visited.insert key }
-        let assignment := mkAssignment decl values
-        withReader (fun ctx => { ctx with assignment }) <| evalCode decl.value
+        decl.value.forCodeM fun c =>
+          let assignment := mkAssignment decl values
+          withReader (fun ctx => { ctx with assignment }) <| evalCode c
 
 end
 
@@ -169,8 +170,12 @@ def mkFixedParamsMap (decls : Array Decl) : NameMap (Array Bool) := Id.run do
     let values := mkInitialValues decl.params.size
     let assignment := mkAssignment decl values
     let fixed := Array.mkArray decl.params.size true
-    match evalCode decl.value |>.run { main := decl, decls, assignment } |>.run { fixed } with
-    | .ok _ s | .error _ s => result := result.insert decl.name s.fixed
+    match decl.value with
+    | .code c =>
+      match evalCode c |>.run { main := decl, decls, assignment } |>.run { fixed } with
+      | .ok _ s | .error _ s => result := result.insert decl.name s.fixed
+    | .extern .. =>
+      result := result.insert decl.name fixed
   return result
 
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/FloatLetIn.lean

@@ -239,7 +239,7 @@ Iterate through `decl`, pushing local declarations that are only used in one
 control flow arm into said arm in order to avoid useless computations.
 -/
 partial def floatLetIn (decl : Decl) : CompilerM Decl := do
-  let newValue ← go decl.value |>.run {}
+  let newValue ← decl.value.mapCodeM go |>.run {}
   return { decl with value := newValue }
 where
   /--

src/Lean/Compiler/LCNF/Internalize.lean

@@ -108,7 +108,7 @@ where
   go (decl : Decl) : InternalizeM Decl := do
     let type ← normExpr decl.type
     let params ← decl.params.mapM internalizeParam
-    let value ← internalizeCode decl.value
+    let value ← decl.value.mapCodeM internalizeCode
     return { decl with type, params, value }
 
 /--

src/Lean/Compiler/LCNF/JoinPoints.lean

@@ -133,7 +133,7 @@ this. This is because otherwise the calls to `myjp` in `f` and `g` would
 produce out of scope join point jumps.
 -/
 partial def find (decl : Decl) : CompilerM FindState := do
-  let (_, candidates) ← go decl.value |>.run none |>.run {} |>.run' {}
+  let (_, candidates) ← decl.value.forCodeM go |>.run none |>.run {} |>.run' {}
   return candidates
 where
   go : Code → FindM Unit
@@ -178,7 +178,7 @@ and all calls to them with `jmp`s.
 partial def replace (decl : Decl) (state : FindState) : CompilerM Decl := do
   let mapper := fun acc cname _ => do return acc.insert cname (← mkFreshJpName)
   let replaceCtx : ReplaceCtx ← state.candidates.foldM (init := .empty) mapper
-  let newValue ← go decl.value |>.run replaceCtx
+  let newValue ← decl.value.mapCodeM go |>.run replaceCtx
   return { decl with value := newValue }
 where
   go (code : Code) : ReplaceM Code := do
@@ -389,7 +389,7 @@ position within the code so we can pull them out as far as possible, hopefully
 enabling new inlining possibilities in the next simplifier run.
 -/
 partial def extend (decl : Decl) : CompilerM Decl := do
-  let newValue ← go decl.value |>.run {} |>.run' {} |>.run' {}
+  let newValue ← decl.value.mapCodeM go |>.run {} |>.run' {} |>.run' {}
   let decl := { decl with value := newValue }
   decl.pullFunDecls
 where
@@ -510,8 +510,8 @@ After we have performed all of these optimizations we can take away the
 code that has as little arguments as possible in the join points.
 -/
 partial def reduce (decl : Decl) : CompilerM Decl := do
-  let (_, analysis) ← goAnalyze decl.value |>.run {} |>.run {} |>.run' {}
-  let newValue ← goReduce decl.value |>.run analysis
+  let (_, analysis) ← decl.value.forCodeM goAnalyze |>.run {} |>.run {} |>.run' {}
+  let newValue ← decl.value.mapCodeM goReduce |>.run analysis
   return { decl with value := newValue }
 where
   goAnalyzeFunDecl (fn : FunDecl) : ReduceAnalysisM Unit := do

src/Lean/Compiler/LCNF/LambdaLifting.lean

@@ -108,9 +108,10 @@ def mkAuxDecl (closure : Array Param) (decl : FunDecl) : LiftM LetDecl := do
 where
   go (nameNew : Name) (safe : Bool) (inlineAttr? : Option InlineAttributeKind) : InternalizeM Decl := do
     let params := (← closure.mapM internalizeParam) ++ (← decl.params.mapM internalizeParam)
-    let value ← internalizeCode decl.value
-    let type ← value.inferType
+    let code ← internalizeCode decl.value
+    let type ← code.inferType
     let type ← mkForallParams params type
+    let value := .code code
     let decl := { name := nameNew, levelParams := [], params, type, value, safe, inlineAttr?, recursive := false : Decl }
     return decl.setLevelParams
 
@@ -149,7 +150,7 @@ mutual
 end
 
 def main (decl : Decl) : LiftM Decl := do
-  let value ← withParams decl.params <| visitCode decl.value
+  let value ← withParams decl.params <| decl.value.mapCodeM visitCode
   return { decl with value }
 
 end LambdaLifting

src/Lean/Compiler/LCNF/Level.lean

@@ -139,6 +139,10 @@ mutual
     | .jmp _ args => visitArgs args
 end
 
+def visitDeclValue : DeclValue → Visitor
+  | .code c => visitCode c
+  | .extern .. => id
+
 end CollectLevelParams
 
 open Lean.CollectLevelParams
@@ -149,7 +153,7 @@ Collect universe level parameters collecting in the type, parameters, and value,
 set `decl.levelParams` with the resulting value.
 -/
 def Decl.setLevelParams (decl : Decl) : Decl :=
-  let levelParams := (visitCode decl.value ∘ visitParams decl.params ∘ visitType decl.type) {} |>.params.toList
+  let levelParams := (visitDeclValue decl.value ∘ visitParams decl.params ∘ visitType decl.type) {} |>.params.toList
   { decl with levelParams }
 
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/Main.lean

@@ -28,10 +28,10 @@ and `[specialize]` since they can be partially applied.
 -/
 def shouldGenerateCode (declName : Name) : CoreM Bool := do
   if (← isCompIrrelevant |>.run') then return false
+  let env ← getEnv
+  if isExtern env declName then return true
   let some info ← getDeclInfo? declName | return false
   unless info.hasValue (allowOpaque := true) do return false
-  let env ← getEnv
-  if isExtern env declName then return false
   if hasMacroInlineAttribute env declName then return false
   if (← Meta.isMatcher declName) then return false
   if isCasesOnRecursor env declName then return false

src/Lean/Compiler/LCNF/PrettyPrinter.lean

@@ -105,6 +105,11 @@ mutual
         return f!"⊥ : {← ppExpr type}"
       else
         return "⊥"
+
+  partial def ppDeclValue (b : DeclValue) : M Format := do
+    match b with
+    | .code c => ppCode c
+    | .extern .. => return "extern"
 end
 
 def run (x : M α) : CompilerM α :=
@@ -121,7 +126,7 @@ def ppLetValue (e : LetValue) : CompilerM Format :=
 
 def ppDecl (decl : Decl) : CompilerM Format :=
   PP.run do
-    return f!"def {decl.name}{← PP.ppParams decl.params} : {← PP.ppExpr (← PP.getFunType decl.params decl.type)} :={indentD (← PP.ppCode decl.value)}"
+    return f!"def {decl.name}{← PP.ppParams decl.params} : {← PP.ppExpr (← PP.getFunType decl.params decl.type)} :={indentD (← PP.ppDeclValue decl.value)}"
 
 def ppFunDecl (decl : FunDecl) : CompilerM Format :=
   PP.run do

src/Lean/Compiler/LCNF/Probing.lean

@@ -57,7 +57,7 @@ where
     | .cases (cases : CasesCore Code) => cases.alts.forM (go ·.getCode)
     | .jmp .. | .return .. | .unreach .. => return ()
   start (decls : Array Decl) : StateRefT (Array LetValue) CompilerM Unit :=
-    decls.forM (go ·.value)
+    decls.forM (·.value.forCodeM go)
 
 partial def getJps : Probe Decl FunDecl := fun decls => do
   let (_, res) ← start decls |>.run #[]
@@ -72,10 +72,10 @@ where
     | .jmp .. | .return .. | .unreach .. => return ()
 
   start (decls : Array Decl) : StateRefT (Array FunDecl) CompilerM Unit :=
-    decls.forM fun decl => go decl.value
+    decls.forM (·.value.forCodeM go)
 
 partial def filterByLet (f : LetDecl → CompilerM Bool) : Probe Decl Decl :=
-  filter (fun decl => go decl.value)
+  filter (·.value.isCodeAndM go)
 where
   go : Code → CompilerM Bool
   | .let decl k => do if (← f decl) then return true else go k
@@ -84,7 +84,7 @@ where
   | .jmp .. | .return .. | .unreach .. => return false
 
 partial def filterByFun (f : FunDecl → CompilerM Bool) : Probe Decl Decl :=
-  filter (fun decl => go decl.value)
+  filter (·.value.isCodeAndM go)
 where
   go : Code → CompilerM Bool
   | .let _ k | .jp _ k  => go k
@@ -93,7 +93,7 @@ where
   | .jmp .. | .return .. | .unreach .. => return false
 
 partial def filterByJp (f : FunDecl → CompilerM Bool) : Probe Decl Decl :=
-  filter (fun decl => go decl.value)
+  filter (·.value.isCodeAndM go)
 where
   go : Code → CompilerM Bool
   | .let _ k => go k
@@ -103,7 +103,7 @@ where
   | .jmp .. | .return .. | .unreach .. => return false
 
 partial def filterByFunDecl (f : FunDecl → CompilerM Bool) : Probe Decl Decl :=
-  filter (fun decl => go decl.value)
+  filter (·.value.isCodeAndM go)
 where
   go : Code → CompilerM Bool
   | .let _ k => go k
@@ -112,7 +112,7 @@ where
   | .jmp .. | .return .. | .unreach .. => return false
 
 partial def filterByCases (f : Cases → CompilerM Bool) : Probe Decl Decl :=
-  filter (fun decl => go decl.value)
+  filter (·.value.isCodeAndM go)
 where
   go : Code → CompilerM Bool
   | .let _ k => go k
@@ -121,7 +121,7 @@ where
   | .jmp .. | .return .. | .unreach .. => return false
 
 partial def filterByJmp (f : FVarId → Array Arg → CompilerM Bool) : Probe Decl Decl :=
-  filter (fun decl => go decl.value)
+  filter (·.value.isCodeAndM go)
 where
   go : Code → CompilerM Bool
   | .let _ k => go k
@@ -131,7 +131,7 @@ where
   | .return .. | .unreach .. => return false
 
 partial def filterByReturn (f : FVarId → CompilerM Bool) : Probe Decl Decl :=
-  filter (fun decl => go decl.value)
+  filter (·.value.isCodeAndM go)
 where
   go : Code → CompilerM Bool
   | .let _ k => go k
@@ -141,7 +141,7 @@ where
   | .return var  => f var
 
 partial def filterByUnreach (f : Expr → CompilerM Bool) : Probe Decl Decl :=
-  filter (fun decl => go decl.value)
+  filter (·.value.isCodeAndM go)
 where
   go : Code → CompilerM Bool
   | .let _ k => go k

src/Lean/Compiler/LCNF/PullFunDecls.lean

@@ -172,8 +172,8 @@ open PullFunDecls
 Pull local function declarations and join points in the given declaration.
 -/
 def Decl.pullFunDecls (decl : Decl) : CompilerM Decl := do
-  let (value, ps) ← pull decl.value |>.run []
-  let value := attach ps.toArray value
+  let (value, ps) ← decl.value.mapCodeM pull |>.run []
+  let value := value.mapCode (attach ps.toArray)
   return { decl with value }
 
 def pullFunDecls : Pass :=

src/Lean/Compiler/LCNF/PullLetDecls.lean

@@ -96,8 +96,8 @@ open PullLetDecls
 def Decl.pullLetDecls (decl : Decl) (isCandidateFn : LetDecl → FVarIdSet → CompilerM Bool) : CompilerM Decl := do
   PullM.run (isCandidateFn := isCandidateFn) do
     withParams decl.params do
-      let value ← pullDecls decl.value
-      let value ← attachToPull value
+      let value ← decl.value.mapCodeM pullDecls
+      let value ← value.mapCodeM attachToPull
       return { decl with value }
 
 def Decl.pullInstances (decl : Decl) : CompilerM Decl :=

src/Lean/Compiler/LCNF/ReduceArity.lean

@@ -108,7 +108,7 @@ partial def visit (code : Code) : FindUsedM Unit := do
 
 def collectUsedParams (decl : Decl) : CompilerM FVarIdSet := do
   let params := decl.params.foldl (init := {}) fun s p => s.insert p.fvarId
-  let (_, { used, .. }) ← visit decl.value |>.run { decl, params } |>.run {}
+  let (_, { used, .. }) ← decl.value.forCodeM visit |>.run { decl, params } |>.run {}
   return used
 
 end FindUsed
@@ -146,37 +146,40 @@ end ReduceArity
 open FindUsed ReduceArity Internalize
 
 def Decl.reduceArity (decl : Decl) : CompilerM (Array Decl) := do
-  let used ← collectUsedParams decl
-  if used.size == decl.params.size then
-    return #[decl] -- Declarations uses all parameters
-  else
-    trace[Compiler.reduceArity] "{decl.name}, used params: {used.toList.map mkFVar}"
-    let mask   := decl.params.map fun param => used.contains param.fvarId
-    let auxName   := decl.name ++ `_redArg
-    let mkAuxDecl : CompilerM Decl := do
-      let params := decl.params.filter fun param => used.contains param.fvarId
-      let value  ← reduce decl.value |>.run { declName := decl.name, auxDeclName := auxName, paramMask := mask }
-      let type ← value.inferType
-      let type ← mkForallParams params type
-      let auxDecl := { decl with name := auxName, levelParams := [], type, params, value }
-      auxDecl.saveMono
-      return auxDecl
-    let updateDecl : InternalizeM Decl := do
-      let params ← decl.params.mapM internalizeParam
-      let mut args := #[]
-      for used in mask, param in params do
-        if used then
-          args := args.push param.toArg
-      let letDecl ← mkAuxLetDecl (.const auxName [] args)
-      let value := .let letDecl (.return letDecl.fvarId)
-      let decl := { decl with params, value, inlineAttr? := some .inline, recursive := false }
-      decl.saveMono
-      return decl
-    let unusedParams := decl.params.filter fun param => !used.contains param.fvarId
-    let auxDecl ← mkAuxDecl
-    let decl ← updateDecl |>.run' {}
-    eraseParams unusedParams
-    return #[auxDecl, decl]
+  match decl.value with
+  | .code code =>
+    let used ← collectUsedParams decl
+    if used.size == decl.params.size then
+      return #[decl] -- Declarations uses all parameters
+    else
+      trace[Compiler.reduceArity] "{decl.name}, used params: {used.toList.map mkFVar}"
+      let mask   := decl.params.map fun param => used.contains param.fvarId
+      let auxName   := decl.name ++ `_redArg
+      let mkAuxDecl : CompilerM Decl := do
+        let params := decl.params.filter fun param => used.contains param.fvarId
+        let value  ← decl.value.mapCodeM reduce |>.run { declName := decl.name, auxDeclName := auxName, paramMask := mask }
+        let type ← code.inferType
+        let type ← mkForallParams params type
+        let auxDecl := { decl with name := auxName, levelParams := [], type, params, value }
+        auxDecl.saveMono
+        return auxDecl
+      let updateDecl : InternalizeM Decl := do
+        let params ← decl.params.mapM internalizeParam
+        let mut args := #[]
+        for used in mask, param in params do
+          if used then
+            args := args.push param.toArg
+        let letDecl ← mkAuxLetDecl (.const auxName [] args)
+        let value := .code (.let letDecl (.return letDecl.fvarId))
+        let decl := { decl with params, value, inlineAttr? := some .inline, recursive := false }
+        decl.saveMono
+        return decl
+      let unusedParams := decl.params.filter fun param => !used.contains param.fvarId
+      let auxDecl ← mkAuxDecl
+      let decl ← updateDecl |>.run' {}
+      eraseParams unusedParams
+      return #[auxDecl, decl]
+  | .extern .. => return #[decl]
 
 def reduceArity : Pass where
   phase := .mono
@@ -187,4 +190,4 @@ def reduceArity : Pass where
 builtin_initialize
   registerTraceClass `Compiler.reduceArity (inherited := true)
 
-end Lean.Compiler.LCNF
+end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/ReduceJpArity.lean

@@ -68,7 +68,7 @@ open ReduceJpArity
 Try to reduce arity of join points
 -/
 def Decl.reduceJpArity (decl : Decl) : CompilerM Decl := do
-  let value ← reduce decl.value |>.run {}
+  let value ← decl.value.mapCodeM reduce |>.run {}
   return { decl with value }
 
 def reduceJpArity (phase := Phase.base) : Pass :=

src/Lean/Compiler/LCNF/Renaming.lean

@@ -55,7 +55,7 @@ def Decl.applyRenaming (decl : Decl) (r : Renaming) : CompilerM Decl := do
     return decl
   else
     let params ← decl.params.mapMonoM (·.applyRenaming r)
-    let value ← decl.value.applyRenaming r
+    let value ← decl.value.mapCodeM (·.applyRenaming r)
     return { decl with params, value }
 
-end Lean.Compiler.LCNF
+end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/Simp.lean

@@ -22,19 +22,20 @@ namespace Lean.Compiler.LCNF
 open Simp
 
 def Decl.simp? (decl : Decl) : SimpM (Option Decl) := do
-  updateFunDeclInfo decl.value
+  let .code code := decl.value | return none
+  updateFunDeclInfo code
   traceM `Compiler.simp.inline.info do return m!"{decl.name}:{Format.nest 2 (← (← get).funDeclInfoMap.format)}"
   traceM `Compiler.simp.step do ppDecl decl
-  let value ← simp decl.value
+  let code ← simp code
   let s ← get
-  let value ← value.applyRenaming s.binderRenaming
-  traceM `Compiler.simp.step.new do return m!"{decl.name} :=\n{← ppCode value}"
-  trace[Compiler.simp.stat] "{decl.name}, size: {value.size}, # visited: {s.visited}, # inline: {s.inline}, # inline local: {s.inlineLocal}"
-  if let some value ← simpJpCases? value then
-    let decl := { decl with value }
+  let code ← code.applyRenaming s.binderRenaming
+  traceM `Compiler.simp.step.new do return m!"{decl.name} :=\n{← ppCode code}"
+  trace[Compiler.simp.stat] "{decl.name}, size: {code.size}, # visited: {s.visited}, # inline: {s.inline}, # inline local: {s.inlineLocal}"
+  if let some code ← simpJpCases? code then
+    let decl := { decl with value := .code code }
     decl.reduceJpArity
   else if (← get).simplified then
-    return some { decl with value }
+    return some { decl with value := .code code }
   else
     return none
 

src/Lean/Compiler/LCNF/Simp/InlineCandidate.lean

@@ -43,6 +43,7 @@ def inlineCandidate? (e : LetValue) : SimpM (Option InlineCandidateInfo) := do
     unless (← read).config.inlineDefs do
       return none
     let some decl ← getDecl? declName | return none
+    let .code code := decl.value | return none
     let shouldInline : SimpM Bool := do
       if !decl.inlineIfReduceAttr && decl.recursive then return false
       if mustInline then return true
@@ -63,9 +64,8 @@ def inlineCandidate? (e : LetValue) : SimpM (Option InlineCandidateInfo) := do
       if decl.alwaysInlineAttr then return true
       -- TODO: check inlining quota
       if decl.inlineAttr || decl.inlineIfReduceAttr then return true
-      unless decl.noinlineAttr do
-        if (← isSmall decl.value) then return true
-      return false
+      if decl.noinlineAttr then return false
+      isSmall code
     unless (← shouldInline) do return none
     /- check arity -/
     let arity := decl.getArity
@@ -77,7 +77,7 @@ def inlineCandidate? (e : LetValue) : SimpM (Option InlineCandidateInfo) := do
       let arg := args[paramIdx]!
       unless (← arg.isConstructorApp) do return none
     let params := decl.instantiateParamsLevelParams us
-    let value := decl.instantiateValueLevelParams us
+    let value := code.instantiateValueLevelParams decl.levelParams us
     let type := decl.instantiateTypeLevelParams us
     incInline
     return some {

src/Lean/Compiler/LCNF/Simp/InlineProj.lean

@@ -69,11 +69,14 @@ where
           visit fvarId projs
       else
         let some decl ← getDecl? declName | failure
-        guard (decl.getArity == args.size)
-        let params := decl.instantiateParamsLevelParams us
-        let code := decl.instantiateValueLevelParams us
-        let code ← betaReduce params code args (mustInline := true)
-        visitCode code projs
+        match decl.value with
+        | .code code =>
+          guard (decl.getArity == args.size)
+          let params := decl.instantiateParamsLevelParams us
+          let code := code.instantiateValueLevelParams decl.levelParams us
+          let code ← betaReduce params code args (mustInline := true)
+          visitCode code projs
+        | .extern .. => failure
 
   visitCode (code : Code) (projs : List Nat) : OptionT (StateRefT (Array CodeDecl) SimpM) FVarId := do
     match code with

src/Lean/Compiler/LCNF/Specialize.lean

@@ -222,6 +222,7 @@ def mkSpecDecl (decl : Decl) (us : List Level) (argMask : Array (Option Arg)) (p
     eraseDecl decl
 where
   go (decl : Decl) (nameNew : Name) : InternalizeM Decl := do
+    let .code code := decl.value | panic! "can only specialize decls with code"
     let mut params ← params.mapM internalizeParam
     let decls ← decls.mapM internalizeCodeDecl
     for param in decl.params, arg in argMask do
@@ -235,11 +236,12 @@ where
     for param in decl.params[argMask.size:] do
       let param := { param with type := param.type.instantiateLevelParamsNoCache decl.levelParams us }
       params := params.push (← internalizeParam param)
-    let value := decl.instantiateValueLevelParams us
-    let value ← internalizeCode value
-    let value := attachCodeDecls decls value
-    let type ← value.inferType
+    let code := code.instantiateValueLevelParams decl.levelParams us
+    let code ← internalizeCode code
+    let code := attachCodeDecls decls code
+    let type ← code.inferType
     let type ← mkForallParams params type
+    let value := .code code
     let safe := decl.safe
     let recursive := decl.recursive
     let decl := { name := nameNew, levelParams := levelParamsNew, params, type, value, safe, recursive, inlineAttr? := none : Decl }
@@ -268,6 +270,7 @@ mutual
     let some paramsInfo ← getSpecParamInfo? declName | return none
     unless (← shouldSpecialize paramsInfo args) do return none
     let some decl ← getDecl? declName | return none
+    let .code _ := decl.value | return none
     trace[Compiler.specialize.candidate] "{e.toExpr}, {paramsInfo}"
     let (argMask, params, decls) ← Collector.collect paramsInfo args
     let keyBody := .const declName us (argMask.filterMap id)
@@ -290,7 +293,7 @@ mutual
       let specDecl ← specDecl.simp {}
       let specDecl ← specDecl.simp { etaPoly := true, inlinePartial := true, implementedBy := true }
       let value ← withReader (fun _ => { declName := specDecl.name }) do
-         withParams specDecl.params <| visitCode specDecl.value
+         withParams specDecl.params <| specDecl.value.mapCodeM visitCode
       let specDecl := { specDecl with value }
       modify fun s => { s with decls := s.decls.push specDecl }
       return some (.const specDecl.name usNew argsNew)
@@ -325,7 +328,7 @@ def main (decl : Decl) : SpecializeM Decl := do
   if (← decl.isTemplateLike) then
     return decl
   else
-    let value ← withParams decl.params <| visitCode decl.value
+    let value ← withParams decl.params <| decl.value.mapCodeM visitCode
     return { decl with value }
 
 end Specialize

src/Lean/Compiler/LCNF/Testing.lean

@@ -235,12 +235,17 @@ Assert that the pass under test produces `Decl`s that do not contain
 `Expr.const constName` in their `Code.let` values anymore.
 -/
 def assertDoesNotContainConstAfter (constName : Name) (msg : String) : TestInstaller :=
-  assertForEachDeclAfterEachOccurrence (fun _ decl => !decl.value.containsConst constName) msg
+  assertForEachDeclAfterEachOccurrence
+    fun _ decl =>
+      match decl.value with
+      | .code c => !c.containsConst constName
+      | .extern .. => true
+    msg
 
 def assertNoFun : TestInstaller :=
   assertAfter do
     for decl in (← getDecls) do
-      decl.value.forM fun
+      decl.value.forCodeM fun
         | .fun .. => throwError "declaration `{decl.name}` contains a local function declaration"
         | _ => return ()
 

src/Lean/Compiler/LCNF/ToDecl.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Meta.Transform
 import Lean.Meta.Match.MatcherInfo
+import Lean.Compiler.ExternAttr
 import Lean.Compiler.ImplementedByAttr
 import Lean.Compiler.LCNF.ToLCNF
 
@@ -96,31 +97,48 @@ The steps for this are roughly:
 def toDecl (declName : Name) : CompilerM Decl := do
   let declName := if let some name := isUnsafeRecName? declName then name else declName
   let some info ← getDeclInfo? declName | throwError "declaration `{declName}` not found"
-  let some value := info.value? (allowOpaque := true) | throwError "declaration `{declName}` does not have a value"
-  let (type, value) ← Meta.MetaM.run' do
-    let type  ← toLCNFType info.type
-    let value ← Meta.lambdaTelescope value fun xs body => do Meta.mkLambdaFVars xs (← Meta.etaExpand body)
-    let value ← replaceUnsafeRecNames value
-    let value ← macroInline value
-    /- Recall that some declarations tagged with `macro_inline` contain matchers. -/
-    let value ← inlineMatchers value
-    /- Recall that `inlineMatchers` may have exposed `ite`s and `dite`s which are tagged as `[macro_inline]`. -/
-    let value ← macroInline value
-    /-
-    Remark: we have disabled the following transformatbion, we will perform it at phase 2, after code specialization.
-    It prevents many optimizations (e.g., "cases-of-ctor").
-    -/
-    -- let value ← applyCasesOnImplementedBy value
-    return (type, value)
-  let value ← toLCNF value
   let safe := !info.isPartial && !info.isUnsafe
   let inlineAttr? := getInlineAttribute? (← getEnv) declName
-  let decl ← if let .fun decl (.return _) := value then
-    eraseFunDecl decl (recursive := false)
-    pure { name := declName, params := decl.params, type, value := decl.value, levelParams := info.levelParams, safe, inlineAttr? : Decl }
+  if let some externAttrData := getExternAttrData? (← getEnv) declName then
+    let paramsFromTypeBinders (expr : Expr) : CompilerM (Array Param) := do
+      let mut params := #[]
+      let mut currentExpr := expr
+      repeat
+        match currentExpr with
+        | .forallE binderName type body _ =>
+          let borrow := isMarkedBorrowed type
+          params := params.push (← mkParam binderName type borrow)
+          currentExpr := body
+        | _ => break
+      return params
+
+    let type ← Meta.MetaM.run' (toLCNFType info.type)
+    let params ← paramsFromTypeBinders type
+    return { name := declName, params, type, value := .extern externAttrData, levelParams := info.levelParams, safe, inlineAttr? }
   else
-    pure { name := declName, params := #[], type, value, levelParams := info.levelParams, safe, inlineAttr? }
-  /- `toLCNF` may eta-reduce simple declarations. -/
-  decl.etaExpand
+    let some value := info.value? (allowOpaque := true) | throwError "declaration `{declName}` does not have a value"
+    let (type, value) ← Meta.MetaM.run' do
+      let type  ← toLCNFType info.type
+      let value ← Meta.lambdaTelescope value fun xs body => do Meta.mkLambdaFVars xs (← Meta.etaExpand body)
+      let value ← replaceUnsafeRecNames value
+      let value ← macroInline value
+      /- Recall that some declarations tagged with `macro_inline` contain matchers. -/
+      let value ← inlineMatchers value
+      /- Recall that `inlineMatchers` may have exposed `ite`s and `dite`s which are tagged as `[macro_inline]`. -/
+      let value ← macroInline value
+      /-
+      Remark: we have disabled the following transformatbion, we will perform it at phase 2, after code specialization.
+      It prevents many optimizations (e.g., "cases-of-ctor").
+      -/
+      -- let value ← applyCasesOnImplementedBy value
+      return (type, value)
+    let code ← toLCNF value
+    let decl ← if let .fun decl (.return _) := code then
+      eraseFunDecl decl (recursive := false)
+      pure { name := declName, params := decl.params, type, value := .code decl.value, levelParams := info.levelParams, safe, inlineAttr? : Decl }
+    else
+      pure { name := declName, params := #[], type, value := .code code, levelParams := info.levelParams, safe, inlineAttr? }
+    /- `toLCNF` may eta-reduce simple declarations. -/
+    decl.etaExpand
 
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/ToExpr.lean

@@ -110,7 +110,4 @@ def Code.toExpr (code : Code) (xs : Array FVarId := #[]) : Expr :=
 def FunDeclCore.toExpr (decl : FunDecl) (xs : Array FVarId := #[]) : Expr :=
   run' decl.toExprM xs
 
-def Decl.toExpr (decl : Decl) : Expr :=
-  run do withParams decl.params do mkLambdaM decl.params (← decl.value.toExprM)
-
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/ToMono.lean

@@ -143,7 +143,7 @@ where
   go : ToMonoM Decl := do
     let type ← toMonoType decl.type
     let params ← decl.params.mapM (·.toMono)
-    let value ← decl.value.toMono
+    let value ← decl.value.mapCodeM (·.toMono)
     let decl := { decl with type, params, value, levelParams := [] }
     decl.saveMono
     return decl

src/Lean/Elab/Tactic.lean

@@ -44,3 +44,4 @@ import Lean.Elab.Tactic.DiscrTreeKey
 import Lean.Elab.Tactic.BVDecide
 import Lean.Elab.Tactic.BoolToPropSimps
 import Lean.Elab.Tactic.Classical
+import Lean.Elab.Tactic.Grind

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean

@@ -82,7 +82,7 @@ instance : ToExpr Gate where
     | .and => mkConst ``Gate.and
     | .xor => mkConst ``Gate.xor
     | .beq => mkConst ``Gate.beq
-    | .imp => mkConst ``Gate.imp
+    | .or => mkConst ``Gate.or
   toTypeExpr := mkConst ``Gate
 
 instance : ToExpr BVPred where

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean

@@ -91,7 +91,7 @@ where
     | .and => ``Std.Tactic.BVDecide.Reflect.Bool.and_congr
     | .xor => ``Std.Tactic.BVDecide.Reflect.Bool.xor_congr
     | .beq => ``Std.Tactic.BVDecide.Reflect.Bool.beq_congr
-    | .imp => ``Std.Tactic.BVDecide.Reflect.Bool.imp_congr
+    | .or => ``Std.Tactic.BVDecide.Reflect.Bool.or_congr
 
 /--
 Construct the reified version of `Bool.not subExpr`.
@@ -136,7 +136,7 @@ def mkIte (discr lhs rhs : ReifiedBVLogical) (discrExpr lhsExpr rhsExpr : Expr)
         lhsEvalExpr lhsProof?
         rhsEvalExpr rhsProof? | return none
     return mkApp9
-      (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.ite_congr)
+      (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.cond_congr)
       discrExpr lhsExpr rhsExpr
       discrEvalExpr lhsEvalExpr rhsEvalExpr
       discrProof lhsProof rhsProof

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean

@@ -22,67 +22,70 @@ This function adds the two lemmas:
 - `discrExpr = false → atomExpr = rhsExpr`
 It assumes that `discrExpr`, `lhsExpr` and `rhsExpr` are the expressions corresponding to `discr`,
 `lhs` and `rhs`. Furthermore it assumes that `atomExpr` is of the form
-`if discrExpr = true then lhsExpr else rhsExpr`.
+`bif discrExpr then lhsExpr else rhsExpr`.
 -/
-def addIfLemmas (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
+def addCondLemmas (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
     (discrExpr atomExpr lhsExpr rhsExpr : Expr) : LemmaM Unit := do
-  let some trueLemma ← mkIfTrueLemma discr atom lhs rhs discrExpr atomExpr lhsExpr rhsExpr | return ()
+  let some trueLemma ← mkCondTrueLemma discr atom lhs discrExpr atomExpr lhsExpr rhsExpr | return ()
   LemmaM.addLemma trueLemma
-  let some falseLemma ← mkIfFalseLemma discr atom lhs rhs discrExpr atomExpr lhsExpr rhsExpr | return ()
+  let some falseLemma ← mkCondFalseLemma discr atom rhs discrExpr atomExpr lhsExpr rhsExpr | return ()
   LemmaM.addLemma falseLemma
 where
-  mkIfTrueLemma (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
-      (discrExpr atomExpr lhsExpr rhsExpr : Expr) : M (Option SatAtBVLogical) :=
-    mkIfLemma true discr atom lhs rhs discrExpr atomExpr lhsExpr rhsExpr
-
-  mkIfFalseLemma (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
-      (discrExpr atomExpr lhsExpr rhsExpr : Expr) : M (Option SatAtBVLogical) :=
-    mkIfLemma false discr atom lhs rhs discrExpr atomExpr lhsExpr rhsExpr
-
-  mkIfLemma (discrVal : Bool) (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
+  mkCondTrueLemma (discr : ReifiedBVLogical) (atom lhs : ReifiedBVExpr)
       (discrExpr atomExpr lhsExpr rhsExpr : Expr) : M (Option SatAtBVLogical) := do
-    let resExpr := if discrVal then lhsExpr else rhsExpr
-    let resValExpr := if discrVal then lhs else rhs
-    let lemmaName :=
-      if discrVal then
-        ``Std.Tactic.BVDecide.Reflect.BitVec.if_true
-      else
-        ``Std.Tactic.BVDecide.Reflect.BitVec.if_false
-    let discrValExpr := toExpr discrVal
-    let discrVal ← ReifiedBVLogical.mkBoolConst discrVal
+    let resExpr := lhsExpr
+    let resValExpr := lhs
+    let lemmaName := ``Std.Tactic.BVDecide.Reflect.BitVec.cond_true
 
-    let eqDiscrExpr ← mkAppM ``BEq.beq #[discrExpr, discrValExpr]
-    let eqDiscr ← ReifiedBVLogical.mkGate discr discrVal discrExpr discrValExpr .beq
+
+    let notDiscrExpr := mkApp (mkConst ``Bool.not) discrExpr
+    let notDiscr ← ReifiedBVLogical.mkNot discr discrExpr
 
     let eqBVExpr ← mkAppM ``BEq.beq #[atomExpr, resExpr]
     let some eqBVPred ← ReifiedBVPred.mkBinPred atom resValExpr atomExpr resExpr .eq | return none
     let eqBV ← ReifiedBVLogical.ofPred eqBVPred
 
-    let imp ← ReifiedBVLogical.mkGate eqDiscr eqBV eqDiscrExpr eqBVExpr .imp
+    let imp ← ReifiedBVLogical.mkGate notDiscr eqBV notDiscrExpr eqBVExpr .or
 
     let proof := do
       let evalExpr ← ReifiedBVLogical.mkEvalExpr imp.expr
       let congrProof := (← imp.evalsAtAtoms).getD (ReifiedBVLogical.mkRefl evalExpr)
       let lemmaProof := mkApp4 (mkConst lemmaName) (toExpr lhs.width) discrExpr lhsExpr rhsExpr
 
-      let trueExpr := mkConst ``Bool.true
-      let eqDiscrTrueExpr ← mkEq eqDiscrExpr trueExpr
-      let eqBVExprTrueExpr ← mkEq eqBVExpr trueExpr
-      let impExpr ← mkArrow eqDiscrTrueExpr eqBVExprTrueExpr
-      -- construct a `Decidable` instance for the implication using forall_prop_decidable
-      let decEqDiscrTrue := mkApp2 (mkConst ``instDecidableEqBool) eqDiscrExpr trueExpr
-      let decEqBVExprTrue := mkApp2 (mkConst ``instDecidableEqBool) eqBVExpr trueExpr
-      let impDecidable := mkApp4 (mkConst ``forall_prop_decidable)
-        eqDiscrTrueExpr
-        (.lam .anonymous eqDiscrTrueExpr eqBVExprTrueExpr .default)
-        decEqDiscrTrue
-        (.lam .anonymous eqDiscrTrueExpr decEqBVExprTrue .default)
-
-      let decideImpExpr := mkApp2 (mkConst ``Decidable.decide) impExpr impDecidable
+      -- !discr || (atom == rhs)
+      let impExpr := mkApp2 (mkConst ``Bool.or) notDiscrExpr eqBVExpr
 
       return mkApp4
         (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.lemma_congr)
-        decideImpExpr
+        impExpr
+        evalExpr
+        congrProof
+        lemmaProof
+    return some ⟨imp.bvExpr, proof, imp.expr⟩
+
+  mkCondFalseLemma (discr : ReifiedBVLogical) (atom rhs : ReifiedBVExpr)
+      (discrExpr atomExpr lhsExpr rhsExpr : Expr) : M (Option SatAtBVLogical) := do
+    let resExpr := rhsExpr
+    let resValExpr := rhs
+    let lemmaName := ``Std.Tactic.BVDecide.Reflect.BitVec.cond_false
+
+    let eqBVExpr ← mkAppM ``BEq.beq #[atomExpr, resExpr]
+    let some eqBVPred ← ReifiedBVPred.mkBinPred atom resValExpr atomExpr resExpr .eq | return none
+    let eqBV ← ReifiedBVLogical.ofPred eqBVPred
+
+    let imp ← ReifiedBVLogical.mkGate discr eqBV discrExpr eqBVExpr .or
+
+    let proof := do
+      let evalExpr ← ReifiedBVLogical.mkEvalExpr imp.expr
+      let congrProof := (← imp.evalsAtAtoms).getD (ReifiedBVLogical.mkRefl evalExpr)
+      let lemmaProof := mkApp4 (mkConst lemmaName) (toExpr rhs.width) discrExpr lhsExpr rhsExpr
+
+      -- discr || (atom == rhs)
+      let impExpr := mkApp2 (mkConst ``Bool.or) discrExpr eqBVExpr
+
+      return mkApp4
+        (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.lemma_congr)
+        impExpr
         evalExpr
         congrProof
         lemmaProof

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean

@@ -220,15 +220,12 @@ where
         .rotateRight
         ``BVUnOp.rotateRight
         ``Std.Tactic.BVDecide.Reflect.BitVec.rotateRight_congr
-    | ite _ discrExpr _ lhsExpr rhsExpr =>
-      let_expr Eq α discrExpr val := discrExpr | return none
-      let_expr Bool := α | return none
-      let_expr Bool.true := val | return none
+    | cond _ discrExpr lhsExpr rhsExpr =>
       let some atom ← ReifiedBVExpr.bitVecAtom x true | return none
       let some discr ← ReifiedBVLogical.of discrExpr | return none
       let some lhs ← goOrAtom lhsExpr | return none
       let some rhs ← goOrAtom rhsExpr | return none
-      addIfLemmas discr atom lhs rhs discrExpr x lhsExpr rhsExpr
+      addCondLemmas discr atom lhs rhs discrExpr x lhsExpr rhsExpr
       return some atom
     | _ => return none
 
@@ -392,10 +389,7 @@ where
       | Bool => gateReflection lhsExpr rhsExpr .beq
       | BitVec _ => goPred t
       | _ => return none
-    | ite _ discrExpr _ lhsExpr rhsExpr =>
-      let_expr Eq α discrExpr val := discrExpr | return none
-      let_expr Bool := α | return none
-      let_expr Bool.true := val | return none
+    | cond _ discrExpr lhsExpr rhsExpr =>
       let some discr ← goOrAtom discrExpr | return none
       let some lhs ← goOrAtom lhsExpr | return none
       let some rhs ← goOrAtom rhsExpr | return none

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean

@@ -28,6 +28,18 @@ namespace Frontend.Normalize
 open Lean.Meta
 open Std.Tactic.BVDecide.Normalize
 
+builtin_simproc ↓ [bv_normalize] reduceCond (cond _ _ _) := fun e => do
+  let_expr f@cond α c tb eb := e | return .continue
+  let r ← Simp.simp c
+  if r.expr.cleanupAnnotations.isConstOf ``Bool.true then
+    let pr := mkApp (mkApp4 (mkConst ``Bool.cond_pos f.constLevels!) α c tb eb) (← r.getProof)
+    return .visit { expr := tb, proof? := pr }
+  else if r.expr.cleanupAnnotations.isConstOf ``Bool.false then
+    let pr := mkApp (mkApp4 (mkConst ``Bool.cond_neg f.constLevels!) α c tb eb) (← r.getProof)
+    return .visit { expr := eb, proof? := pr }
+  else
+    return .continue
+
 builtin_simproc [bv_normalize] eqToBEq (((_ : Bool) = (_ : Bool))) := fun e => do
   let_expr Eq _ lhs rhs := e | return .continue
   match_expr rhs with
@@ -127,8 +139,6 @@ builtin_simproc [bv_normalize] bv_add_const' (((_ : BitVec _) + (_ : BitVec _))
       else
         return .continue
 
-attribute [builtin_bv_normalize_proc↓] reduceIte
-
 /-- Return a number `k` such that `2^k = n`. -/
 private def Nat.log2Exact (n : Nat) : Option Nat := do
   guard <| n ≠ 0

src/Lean/Elab/Tactic/Grind.lean

@@ -0,0 +1,27 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Grind.Tactics
+import Lean.Meta.Tactic.Grind
+import Lean.Elab.Tactic.Basic
+
+namespace Lean.Elab.Tactic
+open Meta
+
+def grind (mvarId : MVarId) (mainDeclName : Name) : MetaM Unit := do
+  let mvarIds ← Grind.main mvarId mainDeclName
+  unless mvarIds.isEmpty do
+    throwError "`grind` failed\n{goalsToMessageData mvarIds}"
+
+@[builtin_tactic Lean.Parser.Tactic.grind] def evalApplyRfl : Tactic := fun stx => do
+  match stx with
+  | `(tactic| grind) =>
+    logWarningAt stx "The `grind` tactic is experimental and still under development. Avoid using it in production projects"
+    let declName := (← Term.getDeclName?).getD `_grind
+    withMainContext do liftMetaFinishingTactic (grind · declName)
+  | _ => throwUnsupportedSyntax
+
+end Lean.Elab.Tactic

src/Lean/Elab/Tactic/Induction.lean

@@ -579,12 +579,25 @@ private def checkAltsOfOptInductionAlts (optInductionAlts : Syntax) : TacticM Un
           throwErrorAt alt "more than one wildcard alternative '| _ => ...' used"
         found := true
 
-def getInductiveValFromMajor (major : Expr) : TacticM InductiveVal :=
+def getInductiveValFromMajor (induction : Bool) (major : Expr) : TacticM InductiveVal :=
   liftMetaMAtMain fun mvarId => do
     let majorType ← inferType major
     let majorType ← whnf majorType
     matchConstInduct majorType.getAppFn
-      (fun _ => Meta.throwTacticEx `induction mvarId m!"major premise type is not an inductive type {indentExpr majorType}")
+      (fun _ => do
+        let tacticName := if induction then `induction else `cases
+        let mut hint := m!"\n\nExplanation: the '{tacticName}' tactic is for constructor-based reasoning \
+          as well as for applying custom {tacticName} principles with a 'using' clause or a registered '@[{tacticName}_eliminator]' theorem. \
+          The above type neither is an inductive type nor has a registered theorem."
+        if majorType.isProp then
+          hint := m!"{hint}\n\n\
+            Consider using the 'by_cases' tactic, which does true/false reasoning for propositions."
+        else if majorType.isType then
+          hint := m!"{hint}\n\n\
+            Type universes are not inductive types, and type-constructor-based reasoning is not possible. \
+            This is a strong limitation. According to Lean's underlying theory, the only provable distinguishing \
+            feature of types is their cardinalities."
+        Meta.throwTacticEx tacticName mvarId m!"major premise type is not an inductive type{indentExpr majorType}{hint}")
       (fun val _ => pure val)
 
 /--
@@ -627,7 +640,7 @@ private def getElimNameInfo (optElimId : Syntax) (targets : Array Expr) (inducti
         return ← getElimInfo elimName
     unless targets.size == 1 do
       throwError "eliminator must be provided when multiple targets are used (use 'using <eliminator-name>'), and no default eliminator has been registered using attribute `[eliminator]`"
-    let indVal ← getInductiveValFromMajor targets[0]!
+    let indVal ← getInductiveValFromMajor induction targets[0]!
     if induction && indVal.all.length != 1 then
       throwError "'induction' tactic does not support mutually inductive types, the eliminator '{mkRecName indVal.name}' has multiple motives"
     if induction && indVal.isNested then

src/Lean/Expr.lean

@@ -769,6 +769,11 @@ opaque quickLt (a : @& Expr) (b : @& Expr) : Bool
 @[extern "lean_expr_lt"]
 opaque lt (a : @& Expr) (b : @& Expr) : Bool
 
+def quickComp (a b : Expr) : Ordering :=
+  if quickLt a b then .lt
+  else if quickLt b a then .gt
+  else .eq
+
 /--
 Return true iff `a` and `b` are alpha equivalent.
 Binder annotations are ignored.
@@ -1643,6 +1648,23 @@ def isFalse (e : Expr) : Bool :=
 def isTrue (e : Expr) : Bool :=
   e.cleanupAnnotations.isConstOf ``True
 
+/--
+`getForallArity type` returns the arity of a `forall`-type. This function consumes nested annotations,
+and performs pending beta reductions. It does **not** use whnf.
+Examples:
+- If `a` is `Nat`, `getForallArity a` returns `0`
+- If `a` is `Nat → Bool`, `getForallArity a` returns `1`
+-/
+partial def getForallArity : Expr → Nat
+  | .mdata _ b       => getForallArity b
+  | .forallE _ _ b _ => getForallArity b + 1
+  | e                =>
+    if e.isHeadBetaTarget then
+      getForallArity e.headBeta
+    else
+      let e' := e.cleanupAnnotations
+      if e != e' then getForallArity e' else 0
+
 /--
 Checks if an expression is a "natural number numeral in normal form",
 i.e. of type `Nat`, and explicitly of the form `OfNat.ofNat n`

src/Lean/Meta/AppBuilder.lean

@@ -176,6 +176,14 @@ def mkEqOfHEq (h : Expr) : MetaM Expr := do
   | _ =>
     throwAppBuilderException ``eq_of_heq m!"heterogeneous equality proof expected{indentExpr h}"
 
+/-- Given `h : Eq a b`, returns a proof of `HEq a b`. -/
+def mkHEqOfEq (h : Expr) : MetaM Expr := do
+  let hType ← infer h
+  let some (α, a, b) := hType.eq?
+    | throwAppBuilderException ``heq_of_eq m!"equality proof expected{indentExpr h}"
+  let u ← getLevel α
+  return mkApp4 (mkConst ``heq_of_eq [u]) α a b h
+
 /--
 If `e` is `@Eq.refl α a`, return `a`.
 -/

src/Lean/Meta/Basic.lean

@@ -605,6 +605,9 @@ variable [MonadControlT MetaM n] [Monad n]
 @[inline] def modifyCache (f : Cache → Cache) : MetaM Unit :=
   modify fun { mctx, cache, zetaDeltaFVarIds, postponed, diag } => { mctx, cache := f cache, zetaDeltaFVarIds, postponed, diag }
 
+def resetCache : MetaM Unit :=
+  modifyCache fun _ => {}
+
 @[inline] def modifyInferTypeCache (f : InferTypeCache → InferTypeCache) : MetaM Unit :=
   modifyCache fun ⟨ic, c1, c2, c3, c4, c5⟩ => ⟨f ic, c1, c2, c3, c4, c5⟩
 
@@ -1777,9 +1780,9 @@ private def withMVarContextImp (mvarId : MVarId) (x : MetaM α) : MetaM α := do
   withLocalContextImp mvarDecl.lctx mvarDecl.localInstances x
 
 /--
-  Execute `x` using the given metavariable `LocalContext` and `LocalInstances`.
-  The type class resolution cache is flushed when executing `x` if its `LocalInstances` are
-  different from the current ones. -/
+Executes `x` using the given metavariable `LocalContext` and `LocalInstances`.
+The type class resolution cache is flushed when executing `x` if its `LocalInstances` are
+different from the current ones. -/
 def _root_.Lean.MVarId.withContext (mvarId : MVarId) : n α → n α :=
   mapMetaM <| withMVarContextImp mvarId
 
@@ -1789,13 +1792,25 @@ private def withMCtxImp (mctx : MetavarContext) (x : MetaM α) : MetaM α := do
   try x finally setMCtx mctx'
 
 /--
-  `withMCtx mctx k` replaces the metavariable context and then executes `k`.
-  The metavariable context is restored after executing `k`.
+`withMCtx mctx k` replaces the metavariable context and then executes `k`.
+The metavariable context is restored after executing `k`.
 
-  This method is used to implement the type class resolution procedure. -/
+This method is used to implement the type class resolution procedure. -/
 def withMCtx (mctx : MetavarContext) : n α → n α :=
   mapMetaM <| withMCtxImp mctx
 
+/--
+`withoutModifyingMCtx k` executes `k` and then restores the metavariable context.
+-/
+def withoutModifyingMCtx : n α → n α :=
+  mapMetaM fun x => do
+    let mctx ← getMCtx
+    try
+      x
+    finally
+      resetCache
+      setMCtx mctx
+
 @[inline] private def approxDefEqImp (x : MetaM α) : MetaM α :=
   withConfig (fun config => { config with foApprox := true, ctxApprox := true, quasiPatternApprox := true}) x
 

src/Lean/Meta/ExprDefEq.lean

@@ -167,7 +167,7 @@ def isDefEqStringLit (s t : Expr) : MetaM LBool := do
   Remark: `n` may be 0. -/
 def isEtaUnassignedMVar (e : Expr) : MetaM Bool := do
   match e.etaExpanded? with
-  | some (Expr.mvar mvarId) =>
+  | some (.mvar mvarId) =>
     if (← mvarId.isReadOnlyOrSyntheticOpaque) then
       pure false
     else if (← mvarId.isAssigned) then
@@ -361,9 +361,9 @@ private partial def isDefEqBindingAux (lctx : LocalContext) (fvars : Array Expr)
     let fvars  := fvars.push (mkFVar fvarId)
     isDefEqBindingAux lctx fvars b₁ b₂ (ds₂.push d₂)
   match e₁, e₂ with
-  | Expr.forallE n d₁ b₁ _, Expr.forallE _ d₂ b₂ _ => process n d₁ d₂ b₁ b₂
-  | Expr.lam     n d₁ b₁ _, Expr.lam     _ d₂ b₂ _ => process n d₁ d₂ b₁ b₂
-  | _,                      _                      =>
+  | .forallE n d₁ b₁ _, .forallE _ d₂ b₂ _ => process n d₁ d₂ b₁ b₂
+  | .lam     n d₁ b₁ _, .lam     _ d₂ b₂ _ => process n d₁ d₂ b₁ b₂
+  | _,                  _                  =>
     withLCtx' lctx do
       isDefEqBindingDomain fvars ds₂ do
         Meta.isExprDefEqAux (e₁.instantiateRev fvars) (e₂.instantiateRev fvars)
@@ -1037,13 +1037,13 @@ def checkedAssignImpl (mvarId : MVarId) (val : Expr) : MetaM Bool := do
 
 private def processAssignmentFOApproxAux (mvar : Expr) (args : Array Expr) (v : Expr) : MetaM Bool :=
   match v with
-  | .mdata _ e   => processAssignmentFOApproxAux mvar args e
-  | Expr.app f a =>
+  | .mdata _ e => processAssignmentFOApproxAux mvar args e
+  | .app f a   =>
     if args.isEmpty then
       pure false
     else
       Meta.isExprDefEqAux args.back! a <&&> Meta.isExprDefEqAux (mkAppRange mvar 0 (args.size - 1) args) f
-  | _            => pure false
+  | _ => pure false
 
 /--
   Auxiliary method for applying first-order unification. It is an approximation.
@@ -1177,7 +1177,7 @@ private partial def processAssignment (mvarApp : Expr) (v : Expr) : MetaM Bool :
         let arg ← simpAssignmentArg arg
         let args := args.set i arg
         match arg with
-        | Expr.fvar fvarId =>
+        | .fvar fvarId =>
           if args[0:i].any fun prevArg => prevArg == arg then
             useFOApprox args
           else if mvarDecl.lctx.contains fvarId && !cfg.quasiPatternApprox then
@@ -1233,7 +1233,7 @@ private def processAssignment' (mvarApp : Expr) (v : Expr) : MetaM Bool := do
 
 private def isDeltaCandidate? (t : Expr) : MetaM (Option ConstantInfo) := do
   match t.getAppFn with
-  | Expr.const c _ =>
+  | .const c _ =>
     match (← getUnfoldableConst? c) with
     | r@(some info) => if info.hasValue then return r else return none
     | _             => return none
@@ -1375,8 +1375,8 @@ private def unfoldBothDefEq (fn : Name) (t s : Expr) : MetaM LBool := do
 
 private def sameHeadSymbol (t s : Expr) : Bool :=
   match t.getAppFn, s.getAppFn with
-  | Expr.const c₁ _, Expr.const c₂ _ => c₁ == c₂
-  | _,               _               => false
+  | .const c₁ _, .const c₂ _ => c₁ == c₂
+  | _,           _           => false
 
 /--
   - If headSymbol (unfold t) == headSymbol s, then unfold t
@@ -1521,8 +1521,8 @@ private def isDefEqDelta (t s : Expr) : MetaM LBool := do
       unfoldNonProjFnDefEq tInfo sInfo t s
 
 private def isAssigned : Expr → MetaM Bool
-  | Expr.mvar mvarId => mvarId.isAssigned
-  | _                => pure false
+  | .mvar mvarId => mvarId.isAssigned
+  | _            => pure false
 
 private def expandDelayedAssigned? (t : Expr) : MetaM (Option Expr) := do
   let tFn := t.getAppFn
@@ -1647,8 +1647,8 @@ private partial def isDefEqQuick (t s : Expr) : MetaM LBool :=
   | .sort u,       .sort v     => toLBoolM <| isLevelDefEqAux u v
   | .lam ..,       .lam ..     => if t == s then pure LBool.true else toLBoolM <| isDefEqBinding t s
   | .forallE ..,   .forallE .. => if t == s then pure LBool.true else toLBoolM <| isDefEqBinding t s
-  -- | Expr.mdata _ t _,    s                   => isDefEqQuick t s
-  -- | t,                   Expr.mdata _ s _    => isDefEqQuick t s
+  -- | .mdata _ t _, s               => isDefEqQuick t s
+  -- | t,            .mdata _ s _    => isDefEqQuick t s
   | .fvar fvarId₁, .fvar fvarId₂ => do
     if fvarId₁ == fvarId₂ then
       return .true

src/Lean/Meta/Tactic/Grind.lean

@@ -12,6 +12,15 @@ import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.Cases
 import Lean.Meta.Tactic.Grind.Injection
 import Lean.Meta.Tactic.Grind.Core
+import Lean.Meta.Tactic.Grind.Canon
+import Lean.Meta.Tactic.Grind.MarkNestedProofs
+import Lean.Meta.Tactic.Grind.Inv
+import Lean.Meta.Tactic.Grind.Proof
+import Lean.Meta.Tactic.Grind.Propagate
+import Lean.Meta.Tactic.Grind.PP
+import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.Ctor
+import Lean.Meta.Tactic.Grind.Parser
 
 namespace Lean
 
@@ -21,5 +30,10 @@ builtin_initialize registerTraceClass `grind.issues
 builtin_initialize registerTraceClass `grind.add
 builtin_initialize registerTraceClass `grind.pre
 builtin_initialize registerTraceClass `grind.debug
+builtin_initialize registerTraceClass `grind.debug.proofs
+builtin_initialize registerTraceClass `grind.simp
+builtin_initialize registerTraceClass `grind.congr
+builtin_initialize registerTraceClass `grind.proof
+builtin_initialize registerTraceClass `grind.proof.detail
 
 end Lean

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

@@ -0,0 +1,157 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Grind.Util
+import Lean.Meta.Basic
+import Lean.Meta.FunInfo
+import Lean.Util.FVarSubset
+import Lean.Util.PtrSet
+import Lean.Util.FVarSubset
+
+namespace Lean.Meta.Grind
+namespace Canon
+
+/-!
+A canonicalizer module for the `grind` tactic. The canonicalizer defined in `Meta/Canonicalizer.lean` is
+not suitable for the `grind` tactic. It was designed for tactics such as `omega`, where the goal is
+to detect when two structurally different atoms are definitionally equal.
+
+The `grind` tactic, on the other hand, uses congruence closure. Moreover, types, type formers, proofs, and instances
+are considered supporting elements and are not factored into congruence detection.
+
+This module minimizes the number of `isDefEq` checks by comparing two terms `a` and `b` only if they instances,
+types, or type formers and are the `i`-th arguments of two different `f`-applications. This approach is
+sufficient for the congruence closure procedure used by the `grind` tactic.
+
+To further optimize `isDefEq` checks, instances are compared using `TransparencyMode.instances`, which reduces
+the number of constants that need to be unfolded. If diagnostics are enabled, instances are compared using
+the default transparency mode too for sanity checking, and discrepancies are reported.
+Types and type formers are always checked using default transparency.
+
+Remark:
+The canonicalizer minimizes issues with non-canonical instances and structurally different but definitionally equal types,
+but it does not solve all problems. For example, consider a situation where we have `(a : BitVec n)`
+and `(b : BitVec m)`, along with instances `inst1 n : Add (BitVec n)` and `inst2 m : Add (BitVec m)` where `inst1`
+and `inst2` are structurally different. Now consider the terms `a + a` and `b + b`. After canonicalization, the two
+additions will still use structurally different (and definitionally different) instances: `inst1 n` and `inst2 m`.
+Furthermore, `grind` will not be able to infer that  `HEq (a + a) (b + b)` even if we add the assumptions `n = m` and `HEq a b`.
+-/
+
+structure State where
+  argMap : PHashMap (Expr × Nat) (List Expr) := {}
+  canon  : PHashMap Expr Expr := {}
+  deriving Inhabited
+
+/--
+Helper function for canonicalizing `e` occurring as the `i`th argument of an `f`-application.
+`isInst` is true if `e` is an type class instance.
+
+Recall that we use `TransparencyMode.instances` for checking whether two instances are definitionally equal or not.
+Thus, if diagnostics are enabled, we also check them using `TransparencyMode.default`. If the result is different
+we report to the user.
+-/
+def canonElemCore (f : Expr) (i : Nat) (e : Expr) (isInst : Bool) : StateT State MetaM Expr := do
+  let s ← get
+  if let some c := s.canon.find? e then
+    return c
+  let key := (f, i)
+  let cs := s.argMap.find? key |>.getD []
+  for c in cs do
+    if (← isDefEq e c) then
+      if c.fvarsSubset e then
+        -- It is not in general safe to replace `e` with `c` if `c` has more free variables than `e`.
+        modify fun s => { s with canon := s.canon.insert e c }
+        return c
+    if isInst then
+      if (← isDiagnosticsEnabled <&&> pure (c.fvarsSubset e) <&&> (withDefault <| isDefEq e c)) then
+        -- TODO: consider storing this information in some structure that can be browsed later.
+        trace[grind.issues] "the following `grind` static elements are definitionally equal with `default` transparency, but not with `instances` transparency{indentExpr e}\nand{indentExpr c}"
+  modify fun s => { s with canon := s.canon.insert e e, argMap := s.argMap.insert key (e::cs) }
+  return e
+
+abbrev canonType (f : Expr) (i : Nat) (e : Expr) := withDefault <| canonElemCore f i e false
+abbrev canonInst (f : Expr) (i : Nat) (e : Expr) := withReducibleAndInstances <| canonElemCore f i e true
+
+/--
+Return type for the `shouldCanon` function.
+-/
+private inductive ShouldCanonResult where
+  | /- Nested types (and type formers) are canonicalized. -/
+    canonType
+  | /- Nested instances are canonicalized. -/
+    canonInst
+  | /-
+    Term is not a proof, type (former), nor an instance.
+    Thus, it must be recursively visited by the canonizer.
+    -/
+    visit
+  deriving Inhabited
+
+/--
+See comments at `ShouldCanonResult`.
+-/
+def shouldCanon (pinfos : Array ParamInfo) (i : Nat) (arg : Expr) : MetaM ShouldCanonResult := do
+  if h : i < pinfos.size then
+    let pinfo := pinfos[i]
+    if pinfo.isInstImplicit then
+      return .canonInst
+    else if pinfo.isProp then
+      return .visit
+  if (← isTypeFormer arg) then
+    return .canonType
+  else
+    return .visit
+
+unsafe def canonImpl (e : Expr) : StateT State MetaM Expr := do
+  visit e |>.run' mkPtrMap
+where
+  visit (e : Expr) : StateRefT (PtrMap Expr Expr) (StateT State MetaM) Expr := do
+    match e with
+    | .bvar .. => unreachable!
+    -- Recall that `grind` treats `let`, `forall`, and `lambda` as atomic terms.
+    | .letE .. | .forallE .. | .lam ..
+    | .const .. | .lit .. | .mvar .. | .sort .. | .fvar ..
+    -- Recall that the `grind` preprocessor uses the `foldProjs` preprocessing step.
+    | .proj ..
+    -- Recall that the `grind` preprocessor uses the `eraseIrrelevantMData` preprocessing step.
+    | .mdata ..  => return e
+    -- We only visit applications
+    | .app .. =>
+      -- Check whether it is cached
+      if let some r := (← get).find? e then
+        return r
+      e.withApp fun f args => do
+        let e' ← if f.isConstOf ``Lean.Grind.nestedProof && args.size == 2 then
+          -- We just canonize the proposition
+          let prop := args[0]!
+          let prop' ← visit prop
+          pure <| if ptrEq prop prop' then mkAppN f (args.set! 0 prop') else e
+        else
+          let pinfos := (← getFunInfo f).paramInfo
+          let mut modified := false
+          let mut args := args
+          for i in [:args.size] do
+            let arg := args[i]!
+            let arg' ← match (← shouldCanon pinfos i arg) with
+            | .canonType  => canonType f i arg
+            | .canonInst  => canonInst f i arg
+            | .visit      => visit arg
+            unless ptrEq arg arg' do
+              args := args.set! i arg'
+              modified := true
+          pure <| if modified then mkAppN f args else e
+        modify fun s => s.insert e e'
+        return e'
+
+/--
+Canonicalizes nested types, type formers, and instances in `e`.
+-/
+def canon (e : Expr) : StateT State MetaM Expr :=
+  unsafe canonImpl e
+
+end Canon
+
+end Lean.Meta.Grind

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

@@ -4,144 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Meta.Tactic.Grind.Types
+import Init.Grind.Util
 import Lean.Meta.LitValues
+import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.Inv
+import Lean.Meta.Tactic.Grind.PP
+import Lean.Meta.Tactic.Grind.Ctor
+import Lean.Meta.Tactic.Grind.Internalize
 
 namespace Lean.Meta.Grind
-/-- Helper function for pretty printing the state for debugging purposes. -/
-def ppENodeRef (e : Expr) : GoalM Format := do
-  let some n ← getENode? e | return "_"
-  return f!"#{n.idx}"
-
-/-- Returns expressions in the given expression equivalence class. -/
-partial def getEqc (e : Expr) : GoalM (List Expr) :=
-  go e e []
-where
-  go (first : Expr) (e : Expr) (acc : List Expr) : GoalM (List Expr) := do
-    let next ← getNext e
-    let acc := e :: acc
-    if isSameExpr first next then
-      return acc
-    else
-      go first next acc
-
-/-- Returns all equivalence classes in the current goal. -/
-partial def getEqcs : GoalM (List (List Expr)) := do
-  let mut r := []
-  for (_, node) in (← get).enodes do
-    if isSameExpr node.root node.self then
-      r := (← getEqc node.self) :: r
-  return r
-
-/-- Helper function for pretty printing the state for debugging purposes. -/
-def ppENodeDeclValue (e : Expr) : GoalM Format := do
-  if e.isApp && !(← isLitValue e) then
-    e.withApp fun f args => do
-      let r ← if f.isConst then
-        ppExpr f
-      else
-        ppENodeRef f
-      let mut r := r
-      for arg in args do
-        r := r ++ " " ++ (← ppENodeRef arg)
-      return r
-  else
-    ppExpr e
-
-/-- Helper function for pretty printing the state for debugging purposes. -/
-def ppENodeDecl (e : Expr) : GoalM Format := do
-  let mut r := f!"{← ppENodeRef e} := {← ppENodeDeclValue e}"
-  let n ← getENode e
-  unless isSameExpr e n.root do
-    r := r ++ f!" ↦ {← ppENodeRef n.root}"
-  if n.interpreted then
-    r := r ++ ", [val]"
-  if n.ctor then
-    r := r ++ ", [ctor]"
-  return r
-
-/-- Pretty print goal state for debugging purposes. -/
-def ppState : GoalM Format := do
-  let mut r := f!"Goal:"
-  let nodes := (← get).enodes.toArray.map (·.2)
-  let nodes := nodes.qsort fun a b => a.idx < b.idx
-  for node in nodes do
-    r := r ++ "\n" ++ (← ppENodeDecl node.self)
-  let eqcs ← getEqcs
-  for eqc in eqcs do
-    if eqc.length > 1 then
-      r := r ++ "\n" ++ "{" ++ (Format.joinSep (← eqc.mapM ppENodeRef) ", ") ++  "}"
-  return r
-
-/--
-Returns `true` if `e` is `True`, `False`, or a literal value.
-See `LitValues` for supported literals.
--/
-def isInterpreted (e : Expr) : MetaM Bool := do
-  if e.isTrue || e.isFalse then return true
-  isLitValue e
-
-/--
-Creates an `ENode` for `e` if one does not already exist.
-This method assumes `e` has been hashconsed.
--/
-def mkENode (e : Expr) (generation : Nat) : GoalM Unit := do
-  if (← alreadyInternalized e) then return ()
-  let ctor := (← isConstructorAppCore? e).isSome
-  let interpreted ← isInterpreted e
-  mkENodeCore e interpreted ctor generation
-
-private def pushNewEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit :=
-  modify fun s => { s with newEqs := s.newEqs.push { lhs, rhs, proof, isHEq } }
-
-@[inline] private def pushNewEq (lhs rhs proof : Expr) : GoalM Unit :=
-  pushNewEqCore lhs rhs proof (isHEq := false)
-
-@[inline] private def pushNewHEq (lhs rhs proof : Expr) : GoalM Unit :=
-  pushNewEqCore lhs rhs proof (isHEq := true)
-
-/--
-Adds `e` to congruence table.
--/
-def addCongrTable (_e : Expr) : GoalM Unit := do
-  -- TODO
-  return ()
-
-partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do
-  if (← alreadyInternalized e) then return ()
-  match e with
-  | .bvar .. => unreachable!
-  | .sort .. => return ()
-  | .fvar .. | .letE .. | .lam .. | .forallE .. =>
-    mkENodeCore e (ctor := false) (interpreted := false) (generation := generation)
-  | .lit .. | .const .. =>
-    mkENode e generation
-  | .mvar ..
-  | .mdata ..
-  | .proj .. =>
-    trace[grind.issues] "unexpected term during internalization{indentExpr e}"
-    mkENodeCore e (ctor := false) (interpreted := false) (generation := generation)
-  | .app .. =>
-    if (← isLitValue e) then
-      -- We do not want to internalize the components of a literal value.
-      mkENode e generation
-    else e.withApp fun f args => do
-      unless f.isConst do
-        internalize f generation
-      let info ← getFunInfo f
-      let shouldInternalize (i : Nat) : GoalM Bool := do
-        if h : i < info.paramInfo.size then
-          let pinfo := info.paramInfo[i]
-          if pinfo.binderInfo.isInstImplicit || pinfo.isProp then
-            return false
-        return true
-      for h : i in [: args.size] do
-        let arg := args[i]
-        if (← shouldInternalize i) then
-          unless (← isTypeFormer arg) do
-            internalize arg generation
-      mkENode e generation
-      addCongrTable e
 
 /--
 The fields `target?` and `proof?` in `e`'s `ENode` are encoding a transitivity proof
@@ -163,11 +34,40 @@ where
       proof?  := proofNew?
     }
 
-private def markAsInconsistent : GoalM Unit :=
-  modify fun s => { s with inconsistent := true }
+/--
+Remove `root` parents from the congruence table.
+This is an auxiliary function performed while merging equivalence classes.
+-/
+private def removeParents (root : Expr) : GoalM ParentSet := do
+  let parents ← getParentsAndReset root
+  for parent in parents do
+    modify fun s => { s with congrTable := s.congrTable.erase { e := parent } }
+  return parents
 
-def isInconsistent : GoalM Bool :=
-  return (← get).inconsistent
+/--
+Reinsert parents into the congruence table and detect new equalities.
+This is an auxiliary function performed while merging equivalence classes.
+-/
+private def reinsertParents (parents : ParentSet) : GoalM Unit := do
+  for parent in parents do
+    addCongrTable parent
+
+/-- Closes the goal when `True` and `False` are in the same equivalence class. -/
+private def closeGoalWithTrueEqFalse : GoalM Unit := do
+  let mvarId := (← get).mvarId
+  unless (← mvarId.isAssigned) do
+    let trueEqFalse ← mkEqFalseProof (← getTrueExpr)
+    let falseProof ← mkEqMP trueEqFalse (mkConst ``True.intro)
+    closeGoal falseProof
+
+/-- Closes the goal when `lhs` and `rhs` are both literal values and belong to the same equivalence class. -/
+private def closeGoalWithValuesEq (lhs rhs : Expr) : GoalM Unit := do
+  let p ← mkEq lhs rhs
+  let hp ← mkEqProof lhs rhs
+  let d ← mkDecide p
+  let pEqFalse := mkApp3 (mkConst ``eq_false_of_decide) p d.appArg! (mkApp2 (mkConst ``Eq.refl [1]) (mkConst ``Bool) (mkConst ``false))
+  let falseProof ← mkEqMP pEqFalse hp
+  closeGoal falseProof
 
 private partial def addEqStep (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit := do
   trace[grind.eq] "{lhs} {if isHEq then "≡" else "="} {rhs}"
@@ -179,23 +79,33 @@ private partial def addEqStep (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit
     return ()
   let lhsRoot ← getENode lhsNode.root
   let rhsRoot ← getENode rhsNode.root
+  let mut valueInconsistency := false
+  let mut trueEqFalse := false
+  if lhsRoot.interpreted && rhsRoot.interpreted then
+    if lhsNode.root.isTrue || rhsNode.root.isTrue then
+      markAsInconsistent
+      trueEqFalse := true
+    else
+      valueInconsistency := true
   if    (lhsRoot.interpreted && !rhsRoot.interpreted)
      || (lhsRoot.ctor && !rhsRoot.ctor)
      || (lhsRoot.size > rhsRoot.size && !rhsRoot.interpreted && !rhsRoot.ctor) then
     go rhs lhs rhsNode lhsNode rhsRoot lhsRoot true
   else
     go lhs rhs lhsNode rhsNode lhsRoot rhsRoot false
+  if trueEqFalse then
+    closeGoalWithTrueEqFalse
+  unless (← isInconsistent) do
+    if lhsRoot.ctor && rhsRoot.ctor then
+      propagateCtor lhsRoot.self rhsRoot.self
+  unless (← isInconsistent) do
+    if valueInconsistency then
+      closeGoalWithValuesEq lhsRoot.self rhsRoot.self
   trace[grind.debug] "after addEqStep, {← ppState}"
+  checkInvariants
 where
   go (lhs rhs : Expr) (lhsNode rhsNode lhsRoot rhsRoot : ENode) (flipped : Bool) : GoalM Unit := do
     trace[grind.debug] "adding {← ppENodeRef lhs} ↦ {← ppENodeRef rhs}"
-    let mut valueInconsistency := false
-    if lhsRoot.interpreted && rhsRoot.interpreted then
-      if lhsNode.root.isTrue || rhsNode.root.isTrue then
-        markAsInconsistent
-      else
-        valueInconsistency := true
-    -- TODO: process valueInconsistency := true
     /-
     We have the following `target?/proof?`
     `lhs -> ... -> lhsNode.root`
@@ -210,14 +120,12 @@ where
       proof?  := proof
       flipped
     }
-    -- TODO: Remove parents from congruence table
-    -- TODO: set propagateBool
-    updateRoots lhs rhsNode.root true -- TODO
+    let parents ← removeParents lhsRoot.self
+    updateRoots lhs rhsNode.root
     trace[grind.debug] "{← ppENodeRef lhs} new root {← ppENodeRef rhsNode.root}, {← ppENodeRef (← getRoot lhs)}"
-    -- TODO: Reinsert parents into congruence table
-    setENode lhsNode.root { lhsRoot with
+    reinsertParents parents
+    setENode lhsNode.root { (← getENode lhsRoot.self) with -- We must retrieve `lhsRoot` since it was updated.
       next := rhsRoot.next
-      root := rhsNode.root
     }
     setENode rhsNode.root { rhsRoot with
       next := lhsRoot.next
@@ -225,22 +133,33 @@ where
       hasLambdas := rhsRoot.hasLambdas || lhsRoot.hasLambdas
       heqProofs  := isHEq || rhsRoot.heqProofs || lhsRoot.heqProofs
     }
-    -- TODO: copy parentst from lhsRoot parents to rhsRoot parents
+    copyParentsTo parents rhsNode.root
+    unless (← isInconsistent) do
+      for parent in parents do
+        propagateUp parent
 
-  updateRoots (lhs : Expr) (rootNew : Expr) (_propagateBool : Bool) : GoalM Unit := do
+  updateRoots (lhs : Expr) (rootNew : Expr) : GoalM Unit := do
     let rec loop (e : Expr) : GoalM Unit := do
-      -- TODO: propagateBool
       let n ← getENode e
       setENode e { n with root := rootNew }
+      unless (← isInconsistent) do
+        propagateDown e
       if isSameExpr lhs n.next then return ()
       loop n.next
     loop lhs
 
 /-- Ensures collection of equations to be processed is empty. -/
-def resetNewEqs : GoalM Unit :=
+private def resetNewEqs : GoalM Unit :=
   modify fun s => { s with newEqs := #[] }
 
-partial def addEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit := do
+/-- Pops and returns the next equality to be processed. -/
+private def popNextEq? : GoalM (Option NewEq) := do
+  let r := (← get).newEqs.back?
+  if r.isSome then
+    modify fun s => { s with newEqs := s.newEqs.pop }
+  return r
+
+private partial def addEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit := do
   addEqStep lhs rhs proof isHEq
   processTodo
 where
@@ -248,7 +167,7 @@ where
     if (← isInconsistent) then
       resetNewEqs
       return ()
-    let some { lhs, rhs, proof, isHEq } := (← get).newEqs.back? | return ()
+    let some { lhs, rhs, proof, isHEq } := (← popNextEq?) | return ()
     addEqStep lhs rhs proof isHEq
     processTodo
 
@@ -273,7 +192,7 @@ where
     trace[grind.add] "isNeg: {isNeg}, {p}"
     match_expr p with
     | Eq _ lhs rhs => goEq p lhs rhs isNeg false
-    | HEq _ _ lhs rhs => goEq p lhs rhs isNeg true
+    | HEq _ lhs _ rhs => goEq p lhs rhs isNeg true
     | _ =>
       internalize p generation
       if isNeg then

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

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Types
+
+namespace Lean.Meta.Grind
+
+private partial def propagateInjEqs (eqs : Expr) (proof : Expr) : GoalM Unit := do
+  match_expr eqs with
+  | And left right =>
+    propagateInjEqs left (.proj ``And 0 proof)
+    propagateInjEqs right (.proj ``And 1 proof)
+  | Eq _ lhs rhs    => pushEq lhs rhs proof
+  | HEq _ lhs _ rhs => pushHEq lhs rhs proof
+  | _ =>
+   trace[grind.issues] "unexpected injectivity theorem result type{indentExpr eqs}"
+   return ()
+
+/--
+Given constructors `a` and `b`, propagate equalities if they are the same,
+and close goal if they are different.
+-/
+def propagateCtor (a b : Expr) : GoalM Unit := do
+  let aType ← whnfD (← inferType a)
+  let bType ← whnfD (← inferType b)
+  unless (← withDefault <| isDefEq aType bType) do
+    return ()
+  let ctor₁ := a.getAppFn
+  let ctor₂ := b.getAppFn
+  if ctor₁ == ctor₂ then
+    let .const ctorName _ := a.getAppFn | return ()
+    let injDeclName := Name.mkStr ctorName "inj"
+    unless (← getEnv).contains injDeclName do return ()
+    let info ← getConstInfo injDeclName
+    let n := info.type.getForallArity
+    let mask : Array (Option Expr) := mkArray n none
+    let mask := mask.set! (n-1) (some (← mkEqProof a b))
+    let injLemma ← mkAppOptM injDeclName mask
+    propagateInjEqs (← inferType injLemma) injLemma
+  else
+    let .const declName _ := aType.getAppFn | return ()
+    let noConfusionDeclName := Name.mkStr declName "noConfusion"
+    unless (← getEnv).contains noConfusionDeclName do return ()
+    closeGoal (← mkNoConfusion (← getFalseExpr) (← mkEqProof a b))
+
+end Lean.Meta.Grind

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

@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Grind.Util
+import Lean.Meta.LitValues
+import Lean.Meta.Tactic.Grind.Types
+
+namespace Lean.Meta.Grind
+
+/-- Adds `e` to congruence table. -/
+def addCongrTable (e : Expr) : GoalM Unit := do
+  if let some { e := e' } := (← get).congrTable.find? { e } then
+    -- `f` and `g` must have the same type.
+    -- See paper: Congruence Closure in Intensional Type Theory
+    let f := e.getAppFn
+    let g := e'.getAppFn
+    unless isSameExpr f g do
+      unless (← hasSameType f g) do
+        trace[grind.issues] "found congruence between{indentExpr e}\nand{indentExpr e'}\nbut functions have different types"
+        return ()
+    trace[grind.congr] "{e} = {e'}"
+    pushEqHEq e e' congrPlaceholderProof
+    let node ← getENode e
+    setENode e { node with cgRoot := e' }
+  else
+    modify fun s => { s with congrTable := s.congrTable.insert { e } }
+
+partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do
+  if (← alreadyInternalized e) then return ()
+  match e with
+  | .bvar .. => unreachable!
+  | .sort .. => return ()
+  | .fvar .. | .letE .. | .lam .. | .forallE .. =>
+    mkENodeCore e (ctor := false) (interpreted := false) (generation := generation)
+  | .lit .. | .const .. =>
+    mkENode e generation
+  | .mvar ..
+  | .mdata ..
+  | .proj .. =>
+    trace[grind.issues] "unexpected term during internalization{indentExpr e}"
+    mkENodeCore e (ctor := false) (interpreted := false) (generation := generation)
+  | .app .. =>
+    if (← isLitValue e) then
+      -- We do not want to internalize the components of a literal value.
+      mkENode e generation
+    else e.withApp fun f args => do
+      if f.isConstOf ``Lean.Grind.nestedProof && args.size == 2 then
+        -- We only internalize the proposition. We can skip the proof because of
+        -- proof irrelevance
+        let c := args[0]!
+        internalize c generation
+        registerParent e c
+      else
+        unless f.isConst do
+          internalize f generation
+          registerParent e f
+        for h : i in [: args.size] do
+          let arg := args[i]
+          internalize arg generation
+          registerParent e arg
+      mkENode e generation
+      addCongrTable e
+      propagateUp e
+
+end Lean.Meta.Grind

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

@@ -0,0 +1,102 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.Proof
+
+namespace Lean.Meta.Grind
+
+/-!
+Debugging support code for checking basic invariants.
+-/
+
+private def checkEqc (root : ENode) : GoalM Unit := do
+  let mut size := 0
+  let mut curr := root.self
+  repeat
+    size := size + 1
+    -- The root of `curr` must be `root`
+    assert! isSameExpr (← getRoot curr) root.self
+    -- Check congruence root
+    if curr.isApp then
+      if let some { e } := (← get).congrTable.find? { e := curr } then
+        if (← hasSameType e.getAppFn curr.getAppFn) then
+          assert! isSameExpr e (← getENode curr).cgRoot
+      else
+        assert! isSameExpr curr (← getENode curr).cgRoot
+    -- If the equivalence class does not have HEq proofs, then the types must be definitionally equal.
+    unless root.heqProofs do
+      assert! (← hasSameType curr root.self)
+    -- Starting at `curr`, following the `target?` field leads to `root`.
+    let mut n := curr
+    repeat
+      if let some target ← getTarget? n then
+        n := target
+      else
+        break
+    assert! isSameExpr n root.self
+    -- Go to next element
+    curr ← getNext curr
+    if isSameExpr root.self curr then
+      break
+  -- The size of the equivalence class is correct.
+  assert! root.size == size
+
+private def checkParents (e : Expr) : GoalM Unit := do
+  if (← isRoot e) then
+    for parent in (← getParents e) do
+      let mut found := false
+      let checkChild (child : Expr) : GoalM Bool := do
+        let some childRoot ← getRoot? child | return false
+        return isSameExpr childRoot e
+      -- There is an argument `arg` s.t. root of `arg` is `e`.
+      for arg in parent.getAppArgs do
+        if (← checkChild arg) then
+          found := true
+          break
+      unless found do
+        assert! (← checkChild parent.getAppFn)
+  else
+    -- All the parents are stored in the root of the equivalence class.
+    assert! (← getParents e).isEmpty
+
+private def checkPtrEqImpliesStructEq : GoalM Unit := do
+  let nodes ← getENodes
+  for h₁ : i in [: nodes.size] do
+    let n₁ := nodes[i]
+    for h₂ : j in [i+1 : nodes.size] do
+      let n₂ := nodes[j]
+      -- We don't have multiple nodes for the same expression
+      assert! !isSameExpr n₁.self n₂.self
+      -- and the two expressions must not be structurally equal
+      assert! !Expr.equal n₁.self n₂.self
+
+private def checkProofs : GoalM Unit := do
+  let eqcs ← getEqcs
+  for eqc in eqcs do
+    for a in eqc do
+      for b in eqc do
+        unless isSameExpr a b do
+          let p ← mkEqProof a b
+          trace[grind.debug.proofs] "{a} = {b}"
+          check p
+          trace[grind.debug.proofs] "checked: {← inferType p}"
+
+/--
+Checks basic invariants if `grind.debug` is enabled.
+-/
+def checkInvariants (expensive := false) : GoalM Unit := do
+  if grind.debug.get (← getOptions) then
+    for (_, node) in (← get).enodes do
+      checkParents node.self
+      if isSameExpr node.self node.root then
+        checkEqc node
+    if expensive then
+      checkPtrEqImpliesStructEq
+  if expensive && grind.debug.proofs.get (← getOptions) then
+    checkProofs
+
+end Lean.Meta.Grind

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

@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Grind.Util
+import Lean.Util.PtrSet
+import Lean.Meta.Basic
+import Lean.Meta.InferType
+
+namespace Lean.Meta.Grind
+
+unsafe def markNestedProofsImpl (e : Expr) : MetaM Expr := do
+  visit e |>.run' mkPtrMap
+where
+  visit (e : Expr) : StateRefT (PtrMap Expr Expr) MetaM Expr := do
+    if (← isProof e) then
+      if e.isAppOf ``Lean.Grind.nestedProof then
+        return e -- `e` is already marked
+      if let some r := (← get).find? e then
+        return r
+      let prop ← inferType e
+      let e' := mkApp2 (mkConst ``Lean.Grind.nestedProof) prop e
+      modify fun s => s.insert e e'
+      return e'
+    else match e with
+      | .bvar .. => unreachable!
+      -- See comments on `Canon.lean` for why we do not visit these cases.
+      | .letE .. | .forallE .. | .lam ..
+      | .const .. | .lit .. | .mvar .. | .sort .. | .fvar ..
+      | .proj ..
+      | .mdata ..  => return e
+      -- We only visit applications
+      | .app .. =>
+        -- Check whether it is cached
+        if let some r := (← get).find? e then
+          return r
+        e.withApp fun f args => do
+          let mut modified := false
+          let mut args := args
+          for i in [:args.size] do
+            let arg := args[i]!
+            let arg' ← visit arg
+            unless ptrEq arg arg' do
+              args := args.set! i arg'
+              modified := true
+          let e' := if modified then mkAppN f args else e
+          modify fun s => s.insert e e'
+          return e'
+
+/--
+Wrap nested proofs `e` with `Lean.Grind.nestedProof`-applications.
+Recall that the congruence closure module has special support for `Lean.Grind.nestedProof`.
+-/
+def markNestedProofs (e : Expr) : MetaM Expr :=
+  unsafe markNestedProofsImpl e
+
+end Lean.Meta.Grind

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

@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Grind.Util
+import Lean.Meta.Tactic.Grind.Types
+
+namespace Lean.Meta.Grind
+
+/-- Helper function for pretty printing the state for debugging purposes. -/
+def ppENodeRef (e : Expr) : GoalM Format := do
+  let some n ← getENode? e | return "_"
+  return f!"#{n.idx}"
+
+/-- Helper function for pretty printing the state for debugging purposes. -/
+def ppENodeDeclValue (e : Expr) : GoalM Format := do
+  if e.isApp && !(← isLitValue e) then
+    e.withApp fun f args => do
+      let r ← if f.isConst then
+        ppExpr f
+      else
+        ppENodeRef f
+      let mut r := r
+      for arg in args do
+        r := r ++ " " ++ (← ppENodeRef arg)
+      return r
+  else
+    ppExpr e
+
+/-- Helper function for pretty printing the state for debugging purposes. -/
+def ppENodeDecl (e : Expr) : GoalM Format := do
+  let mut r := f!"{← ppENodeRef e} := {← ppENodeDeclValue e}"
+  let n ← getENode e
+  unless isSameExpr e n.root do
+    r := r ++ f!" ↦ {← ppENodeRef n.root}"
+  if n.interpreted then
+    r := r ++ ", [val]"
+  if n.ctor then
+    r := r ++ ", [ctor]"
+  if grind.debug.get (← getOptions) then
+    if let some target ← getTarget? e then
+      r := r ++ f!" ↝ {← ppENodeRef target}"
+  return r
+
+/-- Pretty print goal state for debugging purposes. -/
+def ppState : GoalM Format := do
+  let mut r := f!"Goal:"
+  let nodes ← getENodes
+  for node in nodes do
+    r := r ++ "\n" ++ (← ppENodeDecl node.self)
+  let eqcs ← getEqcs
+  for eqc in eqcs do
+    if eqc.length > 1 then
+      r := r ++ "\n" ++ "{" ++ (Format.joinSep (← eqc.mapM ppENodeRef) ", ") ++  "}"
+  return r
+
+end Lean.Meta.Grind

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

@@ -0,0 +1,15 @@
+/-
+Copyright (c) 2024 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.Parser.Command
+
+namespace Lean.Parser.Command
+/-!
+Builtin parsers for `grind` related commands
+-/
+@[builtin_command_parser] def grindPattern := leading_parser
+  "grind_pattern " >>  ident >> darrow >> sepBy1 termParser ","
+end Lean.Parser.Command

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

@@ -16,40 +16,20 @@ import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.Cases
 import Lean.Meta.Tactic.Grind.Injection
 import Lean.Meta.Tactic.Grind.Core
+import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.Run
 
 namespace Lean.Meta.Grind
 namespace Preprocessor
 
--- TODO: use congruence closure and decision procedures during pre-processing
--- TODO: implement `simp` discharger using preprocessor state
-
-structure Context where
-  simp     : Simp.Context
-  simprocs : Array Simp.Simprocs
-  deriving Inhabited
-
 structure State where
-  simpStats : Simp.Stats := {}
   goals     : PArray Goal := {}
   deriving Inhabited
 
-abbrev PreM := ReaderT Context $ StateRefT State GrindM
+abbrev PreM := StateRefT State GrindM
 
 def PreM.run (x : PreM α) : GrindM α := do
-  let thms ← grindNormExt.getTheorems
-  let simprocs := #[(← grindNormSimprocExt.getSimprocs)]
-  let simp ← Simp.mkContext
-    (config := { arith := true })
-    (simpTheorems := #[thms])
-    (congrTheorems := (← getSimpCongrTheorems))
-  x { simp, simprocs } |>.run' {}
-
-def simp (_goal : Goal) (e : Expr) : PreM Simp.Result := do
-  -- TODO: use `goal` state in the simplifier
-  let simpStats := (← get).simpStats
-  let (r, simpStats) ← Meta.simp e (← read).simp (← read).simprocs (stats := simpStats)
-  modify fun s => { s with simpStats }
-  return r
+ x.run' {}
 
 inductive IntroResult where
   | done
@@ -69,21 +49,16 @@ def introNext (goal : Goal) : PreM IntroResult := do
         let tag ← goal.mvarId.getTag
         let q := target.bindingBody!
         -- TODO: keep applying simp/eraseIrrelevantMData/canon/shareCommon until no progress
-        let r ← simp goal p
-        let p' := r.expr
-        let p' ← eraseIrrelevantMData p'
-        let p' ← foldProjs p'
-        let p' ← canon p'
-        let p' ← shareCommon p'
+        let r ← pre p
         let fvarId ← mkFreshFVarId
-        let lctx := (← getLCtx).mkLocalDecl fvarId target.bindingName! p' target.bindingInfo!
+        let lctx := (← getLCtx).mkLocalDecl fvarId target.bindingName! r.expr target.bindingInfo!
         let mvarNew ← mkFreshExprMVarAt lctx (← getLocalInstances) q .syntheticOpaque tag
         let mvarIdNew := mvarNew.mvarId!
         mvarIdNew.withContext do
           let h ← mkLambdaFVars #[mkFVar fvarId] mvarNew
           match r.proof? with
           | some he =>
-            let hNew := mkAppN (mkConst ``Lean.Grind.intro_with_eq) #[p, p', q, he, h]
+            let hNew := mkAppN (mkConst ``Lean.Grind.intro_with_eq) #[p, r.expr, q, he, h]
             goal.mvarId.assign hNew
             return .newHyp fvarId { goal with mvarId := mvarIdNew }
           | none =>
@@ -96,7 +71,7 @@ def introNext (goal : Goal) : PreM IntroResult := do
       let localDecl ← fvarId.getDecl
       if (← isProp localDecl.type) then
         -- Add a non-dependent copy
-        let mvarId ← mvarId.assert localDecl.userName localDecl.type (mkFVar fvarId)
+        let mvarId ← mvarId.assert (← mkFreshUserName localDecl.userName) localDecl.type (mkFVar fvarId)
         return .newDepHyp { goal with mvarId }
       else
         return .newLocal fvarId { goal with mvarId }
@@ -124,6 +99,8 @@ def applyInjection? (goal : Goal) (fvarId : FVarId) : MetaM (Option Goal) := do
     return none
 
 partial def loop (goal : Goal) : PreM Unit := do
+  if goal.inconsistent then
+    return ()
   match (← introNext goal) with
   | .done =>
     if let some mvarId ← goal.mvarId.byContra? then
@@ -153,26 +130,43 @@ def ppGoals : PreM Format := do
   return r
 
 def preprocess (mvarId : MVarId) : PreM State := do
-  loop (← mkGoal mvarId)
-  if (← isTracingEnabledFor `grind.pre) then
-    trace[grind.pre] (← ppGoals)
-  get
-
-end Preprocessor
-
-open Preprocessor
-
-partial def main (mvarId : MVarId) (mainDeclName : Name) : MetaM (List MVarId) := do
   mvarId.ensureProp
   -- TODO: abstract metavars
   mvarId.ensureNoMVar
   let mvarId ← mvarId.clearAuxDecls
   let mvarId ← mvarId.revertAll
   mvarId.ensureNoMVar
-  let mvarId ← mvarId.abstractNestedProofs mainDeclName
+  let mvarId ← mvarId.abstractNestedProofs (← getMainDeclName)
   let mvarId ← mvarId.unfoldReducible
   let mvarId ← mvarId.betaReduce
-  let s ← preprocess mvarId |>.run |>.run mainDeclName
-  return s.goals.toList.map (·.mvarId)
+  loop (← mkGoal mvarId)
+  if (← isTracingEnabledFor `grind.pre) then
+    trace[grind.pre] (← ppGoals)
+  for goal in (← get).goals do
+    discard <| GoalM.run' goal <| checkInvariants (expensive := true)
+  get
+
+def preprocessAndProbe (mvarId : MVarId) (p : GoalM Unit) : PreM Unit := do
+  let s ← preprocess mvarId
+  s.goals.forM fun goal =>
+    discard <| GoalM.run' goal p
+
+end Preprocessor
+
+open Preprocessor
+
+def preprocessAndProbe (mvarId : MVarId) (mainDeclName : Name) (p : GoalM Unit) : MetaM Unit :=
+  withoutModifyingMCtx do
+    Preprocessor.preprocessAndProbe mvarId p |>.run |>.run mainDeclName
+
+def preprocess (mvarId : MVarId) (mainDeclName : Name) : MetaM Preprocessor.State :=
+  Preprocessor.preprocess mvarId |>.run |>.run mainDeclName
+
+def main (mvarId : MVarId) (mainDeclName : Name) : MetaM (List MVarId) := do
+  let go : GrindM (List MVarId) := do
+    let s ← Preprocessor.preprocess mvarId |>.run
+    let goals := s.goals.toList.filter fun goal => !goal.inconsistent
+    return goals.map (·.mvarId)
+  go.run mainDeclName
 
 end Lean.Meta.Grind

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

@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2024 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.ProjFns
+import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.Internalize
+
+namespace Lean.Meta.Grind
+
+/--
+If `parent` is a projection-application `proj_i c`,
+check whether the root of the equivalence class containing `c` is a constructor-application `ctor ... a_i ...`.
+If so, internalize the term `proj_i (ctor ... a_i ...)` and add the equality `proj_i (ctor ... a_i ...) = a_i`.
+-/
+def propagateProjEq (parent : Expr) : GoalM Unit := do
+  let .const declName _ := parent.getAppFn | return ()
+  let some info ← getProjectionFnInfo? declName | return ()
+  unless info.numParams + 1 == parent.getAppNumArgs do return ()
+  let arg := parent.appArg!
+  let ctor ← getRoot arg
+  unless ctor.isAppOf info.ctorName do return ()
+  if isSameExpr arg ctor then
+    let idx := info.numParams + info.i
+    unless idx < ctor.getAppNumArgs do return ()
+    let v := ctor.getArg! idx
+    pushEq parent v (← mkEqRefl v)
+  else
+    let newProj := mkApp parent.appFn! ctor
+    let newProj ← shareCommon newProj
+    internalize newProj (← getGeneration parent)
+
+end Lean.Meta.Grind

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

@@ -0,0 +1,239 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Sorry -- TODO: remove
+import Lean.Meta.Tactic.Grind.Types
+
+namespace Lean.Meta.Grind
+
+private def isEqProof (h : Expr) : MetaM Bool := do
+  return (← whnfD (← inferType h)).isAppOf ``Eq
+
+private def flipProof (h : Expr) (flipped : Bool) (heq : Bool) : MetaM Expr := do
+  let mut h' := h
+  if (← pure heq <&&> isEqProof h') then
+    h' ← mkHEqOfEq h'
+  if flipped then
+    if heq then mkHEqSymm h' else mkEqSymm h'
+  else
+    return h'
+
+private def mkRefl (a : Expr) (heq : Bool) : MetaM Expr :=
+  if heq then mkHEqRefl a else mkEqRefl a
+
+private def mkTrans (h₁ h₂ : Expr) (heq : Bool) : MetaM Expr :=
+  if heq then
+    mkHEqTrans h₁ h₂
+  else
+    mkEqTrans h₁ h₂
+
+private def mkTrans' (h₁ : Option Expr) (h₂ : Expr) (heq : Bool) : MetaM Expr := do
+  let some h₁ := h₁ | return h₂
+  mkTrans h₁ h₂ heq
+
+/--
+Given `h : HEq a b`, returns a proof `a = b` if `heq == false`.
+Otherwise, it returns `h`.
+-/
+private def mkEqOfHEqIfNeeded (h : Expr) (heq : Bool) : MetaM Expr := do
+  if heq then return h else mkEqOfHEq h
+
+/--
+Given `lhs` and `rhs` that are in the same equivalence class,
+find the common expression that are in the paths from `lhs` and `rhs` to
+the root of their equivalence class.
+Recall that this expression must exist since it is the root itself in the
+worst case.
+-/
+private def findCommon (lhs rhs : Expr) : GoalM Expr := do
+  let mut visited : RBMap Nat Expr compare := {}
+  let mut it := lhs
+  -- Mark elements found following the path from `lhs` to the root.
+  repeat
+    let n ← getENode it
+    visited := visited.insert n.idx n.self
+    let some target := n.target? | break
+    it := target
+  -- Find the marked element from the path from `rhs` to the root.
+  it := rhs
+  repeat
+    let n ← getENode it
+    if let some common := visited.find? n.idx then
+      return common
+    let some target := n.target? | unreachable! --
+    it := target
+  unreachable!
+
+/--
+Returns `true` if we can construct a congruence proof for `lhs = rhs` using `congrArg`, `congrFun`, and `congr`.
+`f` (`g`) is the function of the `lhs` (`rhs`) application. `numArgs` is the number of arguments.
+-/
+private partial def isCongrDefaultProofTarget (lhs rhs : Expr) (f g : Expr) (numArgs : Nat) : GoalM Bool := do
+  unless isSameExpr f g do return false
+  let info := (← getFunInfo f).paramInfo
+  let rec loop (lhs rhs : Expr) (i : Nat) : GoalM Bool := do
+    if lhs.isApp then
+      let a₁ := lhs.appArg!
+      let a₂ := rhs.appArg!
+      let i  := i - 1
+      unless isSameExpr a₁ a₂ do
+        if h : i < info.size then
+          if info[i].hasFwdDeps then
+            -- Cannot use `congrArg` because there are forward dependencies
+            return false
+        else
+          return false -- Don't have information about argument
+      loop lhs.appFn! rhs.appFn! i
+    else
+      return true
+  loop lhs rhs numArgs
+
+mutual
+  /--
+  Given `lhs` and `rhs` proof terms of the form `nestedProof p hp` and `nestedProof q hq`,
+  constructs a congruence proof for `HEq (nestedProof p hp) (nestedProof q hq)`.
+  `p` and `q` are in the same equivalence class.
+  -/
+  private partial def mkNestedProofCongr (lhs rhs : Expr) (heq : Bool) : GoalM Expr := do
+    let p  := lhs.appFn!.appArg!
+    let hp := lhs.appArg!
+    let q  := rhs.appFn!.appArg!
+    let hq := rhs.appArg!
+    let h  := mkApp5 (mkConst ``Lean.Grind.nestedProof_congr) p q (← mkEqProofCore p q false) hp hq
+    mkEqOfHEqIfNeeded h heq
+
+  /--
+  Constructs a congruence proof for `lhs` and `rhs` using `congr`, `congrFun`, and `congrArg`.
+  This function assumes `isCongrDefaultProofTarget` returned `true`.
+  -/
+  private partial def mkCongrDefaultProof (lhs rhs : Expr) (heq : Bool) : GoalM Expr := do
+    let rec loop (lhs rhs : Expr) : GoalM (Option Expr) := do
+      if lhs.isApp then
+        let a₁ := lhs.appArg!
+        let a₂ := rhs.appArg!
+        if let some proof ← loop lhs.appFn! rhs.appFn! then
+          if isSameExpr a₁ a₂ then
+            mkCongrFun proof a₁
+          else
+            mkCongr proof (← mkEqProofCore a₁ a₂ false)
+        else if isSameExpr a₁ a₂ then
+          return none -- refl case
+        else
+          mkCongrArg lhs.appFn! (← mkEqProofCore a₁ a₂ false)
+      else
+        return none
+    let r := (← loop lhs rhs).get!
+    if heq then mkHEqOfEq r else return r
+
+  /-- Constructs a congruence proof for `lhs` and `rhs`. -/
+  private partial def mkCongrProof (lhs rhs : Expr) (heq : Bool) : GoalM Expr := do
+    let f := lhs.getAppFn
+    let g := rhs.getAppFn
+    let numArgs := lhs.getAppNumArgs
+    assert! rhs.getAppNumArgs == numArgs
+    if f.isConstOf ``Lean.Grind.nestedProof && g.isConstOf ``Lean.Grind.nestedProof && numArgs == 2 then
+      mkNestedProofCongr lhs rhs heq
+    else if (← isCongrDefaultProofTarget lhs rhs f g numArgs) then
+      mkCongrDefaultProof lhs rhs heq
+    else
+      let thm ← mkHCongrWithArity f numArgs
+      assert! thm.argKinds.size == numArgs
+      let rec loop (lhs rhs : Expr) (i : Nat) : GoalM Expr := do
+        let i := i - 1
+        if lhs.isApp then
+          let proof ← loop lhs.appFn! rhs.appFn! i
+          let a₁  := lhs.appArg!
+          let a₂  := rhs.appArg!
+          let k   := thm.argKinds[i]!
+          return mkApp3 proof a₁ a₂ (← mkEqProofCore a₁ a₂ (k matches .heq))
+        else
+          return thm.proof
+      let proof ← loop lhs rhs numArgs
+      if isSameExpr f g then
+        mkEqOfHEqIfNeeded proof heq
+      else
+        /-
+        `lhs` is of the form `f a_1 ... a_n`
+        `rhs` is of the form `g b_1 ... b_n`
+        `proof : HEq (f a_1 ... a_n) (f b_1 ... b_n)`
+        We construct a proof for `HEq (f a_1 ... a_n) (g b_1 ... b_n)` using `Eq.ndrec`
+        -/
+        let motive ← withLocalDeclD (← mkFreshUserName `x) (← inferType f) fun x => do
+          mkLambdaFVars #[x] (← mkHEq lhs (mkAppN x rhs.getAppArgs))
+        let fEq ← mkEqProofCore f g false
+        let proof ← mkEqNDRec motive proof fEq
+        mkEqOfHEqIfNeeded proof heq
+
+  private partial def realizeEqProof (lhs rhs : Expr) (h : Expr) (flipped : Bool) (heq : Bool) : GoalM Expr := do
+    let h ← if h == congrPlaceholderProof then
+      mkCongrProof lhs rhs heq
+    else
+      flipProof h flipped heq
+
+  /-- Given `acc : lhs₀ = lhs`, returns a proof of `lhs₀ = common`. -/
+  private partial def mkProofTo (lhs : Expr) (common : Expr) (acc : Option Expr) (heq : Bool) : GoalM (Option Expr) := do
+    if isSameExpr lhs common then
+      return acc
+    let n ← getENode lhs
+    let some target := n.target? | unreachable!
+    let some h := n.proof? | unreachable!
+    let h ← realizeEqProof lhs target h n.flipped heq
+    -- h : lhs = target
+    let acc ← mkTrans' acc h heq
+    mkProofTo target common (some acc) heq
+
+  /-- Given `lhsEqCommon : lhs = common`, returns a proof for `lhs = rhs`. -/
+  private partial def mkProofFrom (rhs : Expr) (common : Expr) (lhsEqCommon? : Option Expr) (heq : Bool) : GoalM (Option Expr) := do
+    if isSameExpr rhs common then
+      return lhsEqCommon?
+    let n ← getENode rhs
+    let some target := n.target? | unreachable!
+    let some h := n.proof? | unreachable!
+    let h ← realizeEqProof target rhs h (!n.flipped) heq
+    -- `h : target = rhs`
+    let h' ← mkProofFrom target common lhsEqCommon? heq
+    -- `h' : lhs = target`
+    mkTrans' h' h heq
+
+  private partial def mkEqProofCore (lhs rhs : Expr) (heq : Bool) : GoalM Expr := do
+    if isSameExpr lhs rhs then
+      return (← mkRefl lhs heq)
+    let n₁ ← getENode lhs
+    let n₂ ← getENode rhs
+    assert! isSameExpr n₁.root n₂.root
+    let common ← findCommon lhs rhs
+    let lhsEqCommon? ← mkProofTo lhs common none heq
+    let some lhsEqRhs ← mkProofFrom rhs common lhsEqCommon? heq | unreachable!
+    return lhsEqRhs
+end
+
+/--
+Returns a proof that `a = b` (or `HEq a b`).
+It assumes `a` and `b` are in the same equivalence class.
+-/
+@[export lean_grind_mk_eq_proof]
+def mkEqProofImpl (a b : Expr) : GoalM Expr := do
+  let p ← go
+  trace[grind.proof.detail] "{p}"
+  return p
+where
+  go : GoalM Expr := do
+    let n ← getRootENode a
+    if !n.heqProofs then
+      trace[grind.proof] "{a} = {b}"
+      mkEqProofCore a b (heq := false)
+    else
+      if (← hasSameType a b) then
+        trace[grind.proof] "{a} = {b}"
+        mkEqOfHEq (← mkEqProofCore a b (heq := true))
+      else
+        trace[grind.proof] "{a} ≡ {b}"
+        mkEqProofCore a b (heq := true)
+
+def mkHEqProof (a b : Expr) : GoalM Expr :=
+  mkEqProofCore a b (heq := true)
+
+end Lean.Meta.Grind

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

@@ -0,0 +1,145 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Grind
+import Lean.Meta.Tactic.Grind.Proof
+import Lean.Meta.Tactic.Grind.PropagatorAttr
+
+namespace Lean.Meta.Grind
+
+/--
+Propagates equalities for a conjunction `a ∧ b` based on the truth values
+of its components `a` and `b`. This function checks the truth value of `a` and `b`,
+and propagates the following equalities:
+
+- If `a = True`, propagates `(a ∧ b) = b`.
+- If `b = True`, propagates `(a ∧ b) = a`.
+- If `a = False`, propagates `(a ∧ b) = False`.
+- If `b = False`, propagates `(a ∧ b) = False`.
+-/
+builtin_grind_propagator propagateAndUp ↑And := fun e => do
+  let_expr And a b := e | return ()
+  if (← isEqTrue a) then
+    -- a = True → (a ∧ b) = b
+    pushEq e b <| mkApp3 (mkConst ``Lean.Grind.and_eq_of_eq_true_left) a b (← mkEqTrueProof a)
+  else if (← isEqTrue b) then
+    -- b = True → (a ∧ b) = a
+    pushEq e a <| mkApp3 (mkConst ``Lean.Grind.and_eq_of_eq_true_right) a b (← mkEqTrueProof b)
+  else if (← isEqFalse a) then
+    -- a = False → (a ∧ b) = False
+    pushEqFalse e <| mkApp3 (mkConst ``Lean.Grind.and_eq_of_eq_false_left) a b (← mkEqFalseProof a)
+  else if (← isEqFalse b) then
+    -- b = False → (a ∧ b) = False
+    pushEqFalse e <| mkApp3 (mkConst ``Lean.Grind.and_eq_of_eq_false_right) a b (← mkEqFalseProof b)
+
+/--
+Propagates truth values downwards for a conjunction `a ∧ b` when the
+expression itself is known to be `True`.
+-/
+builtin_grind_propagator propagateAndDown ↓And := fun e => do
+  if (← isEqTrue e) then
+    let_expr And a b := e | return ()
+    let h ← mkEqTrueProof e
+    pushEqTrue a <| mkApp3 (mkConst ``Lean.Grind.eq_true_of_and_eq_true_left) a b h
+    pushEqTrue b <| mkApp3 (mkConst ``Lean.Grind.eq_true_of_and_eq_true_right) a b h
+
+/--
+Propagates equalities for a disjunction `a ∨ b` based on the truth values
+of its components `a` and `b`. This function checks the truth value of `a` and `b`,
+and propagates the following equalities:
+
+- If `a = False`, propagates `(a ∨ b) = b`.
+- If `b = False`, propagates `(a ∨ b) = a`.
+- If `a = True`, propagates `(a ∨ b) = True`.
+- If `b = True`, propagates `(a ∨ b) = True`.
+-/
+builtin_grind_propagator propagateOrUp ↑Or := fun e => do
+  let_expr Or a b := e | return ()
+  if (← isEqFalse a) then
+    -- a = False → (a ∨ b) = b
+    pushEq e b <| mkApp3 (mkConst ``Lean.Grind.or_eq_of_eq_false_left) a b (← mkEqFalseProof a)
+  else if (← isEqFalse b) then
+    -- b = False → (a ∨ b) = a
+    pushEq e a <| mkApp3 (mkConst ``Lean.Grind.or_eq_of_eq_false_right) a b (← mkEqFalseProof b)
+  else if (← isEqTrue a) then
+    -- a = True → (a ∨ b) = True
+    pushEqTrue e <| mkApp3 (mkConst ``Lean.Grind.or_eq_of_eq_true_left) a b (← mkEqTrueProof a)
+  else if (← isEqTrue b) then
+    -- b = True → (a ∧ b) = True
+    pushEqTrue e <| mkApp3 (mkConst ``Lean.Grind.or_eq_of_eq_true_right) a b (← mkEqTrueProof b)
+
+/--
+Propagates truth values downwards for a disjuction `a ∨ b` when the
+expression itself is known to be `False`.
+-/
+builtin_grind_propagator propagateOrDown ↓Or := fun e => do
+  if (← isEqFalse e) then
+    let_expr Or a b := e | return ()
+    let h ← mkEqFalseProof e
+    pushEqFalse a <| mkApp3 (mkConst ``Lean.Grind.eq_false_of_or_eq_false_left) a b h
+    pushEqFalse b <| mkApp3 (mkConst ``Lean.Grind.eq_false_of_or_eq_false_right) a b h
+
+/--
+Propagates equalities for a negation `Not a` based on the truth value of `a`.
+This function checks the truth value of `a` and propagates the following equalities:
+
+- If `a = False`, propagates `(Not a) = True`.
+- If `a = True`, propagates `(Not a) = False`.
+-/
+builtin_grind_propagator propagateNotUp ↑Not := fun e => do
+  let_expr Not a := e | return ()
+  if (← isEqFalse a) then
+    -- a = False → (Not a) = True
+    pushEqTrue e <| mkApp2 (mkConst ``Lean.Grind.not_eq_of_eq_false) a (← mkEqFalseProof a)
+  else if (← isEqTrue a) then
+    -- a = True → (Not a) = False
+    pushEqFalse e <| mkApp2 (mkConst ``Lean.Grind.not_eq_of_eq_true) a (← mkEqTrueProof a)
+
+/--
+Propagates truth values downwards for a negation expression `Not a` based on the truth value of `Not a`.
+This function performs the following:
+
+- If `(Not a) = False`, propagates `a = True`.
+- If `(Not a) = True`, propagates `a = False`.
+-/
+builtin_grind_propagator propagateNotDown ↓Not := fun e => do
+  let_expr Not a := e | return ()
+  if (← isEqFalse e) then
+    pushEqTrue a <| mkApp2 (mkConst ``Lean.Grind.eq_true_of_not_eq_false) a (← mkEqFalseProof e)
+  else if (← isEqTrue e) then
+    pushEqFalse a <| mkApp2 (mkConst ``Lean.Grind.eq_false_of_not_eq_true) a (← mkEqTrueProof e)
+  else if (← isEqv e a) then
+    closeGoal <| mkApp2 (mkConst ``Lean.Grind.false_of_not_eq_self) a (← mkEqProof e a)
+
+/-- Propagates `Eq` upwards -/
+builtin_grind_propagator propagateEqUp ↑Eq := fun e => do
+  let_expr Eq _ a b := e | return ()
+  if (← isEqTrue a) then
+    pushEq e b <| mkApp3 (mkConst ``Lean.Grind.eq_eq_of_eq_true_left) a b (← mkEqTrueProof a)
+  else if (← isEqTrue b) then
+    pushEq e a <| mkApp3 (mkConst ``Lean.Grind.eq_eq_of_eq_true_right) a b (← mkEqTrueProof b)
+  else if (← isEqv a b) then
+    pushEqTrue e <| mkApp2 (mkConst ``eq_true) e (← mkEqProof a b)
+
+/-- Propagates `Eq` downwards -/
+builtin_grind_propagator propagateEqDown ↓Eq := fun e => do
+  if (← isEqTrue e) then
+    let_expr Eq _ a b := e | return ()
+    pushEq a b <| mkApp2 (mkConst ``of_eq_true) e (← mkEqTrueProof e)
+
+/-- Propagates `HEq` downwards -/
+builtin_grind_propagator propagateHEqDown ↓HEq := fun e => do
+  if (← isEqTrue e) then
+    let_expr HEq _ a _ b := e | return ()
+    pushHEq a b <| mkApp2 (mkConst ``of_eq_true) e (← mkEqTrueProof e)
+
+/-- Propagates `HEq` upwards -/
+builtin_grind_propagator propagateHEqUp ↑HEq := fun e => do
+  let_expr HEq _ a _ b := e | return ()
+  if (← isEqv a b) then
+    pushEqTrue e <| mkApp2 (mkConst ``eq_true) e (← mkHEqProof a b)
+
+end Lean.Meta.Grind

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

@@ -0,0 +1,61 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Grind
+import Lean.Meta.Tactic.Grind.Proof
+
+namespace Lean.Meta.Grind
+
+/-- Builtin propagators. -/
+structure BuiltinPropagators where
+  up   : Std.HashMap Name Propagator := {}
+  down : Std.HashMap Name Propagator := {}
+  deriving Inhabited
+
+builtin_initialize builtinPropagatorsRef : IO.Ref BuiltinPropagators ← IO.mkRef {}
+
+private def registerBuiltinPropagatorCore (declName : Name) (up : Bool) (proc : Propagator) : IO Unit := do
+  unless (← initializing) do
+    throw (IO.userError s!"invalid builtin `grind` propagator declaration, it can only be registered during initialization")
+  if up then
+    if (← builtinPropagatorsRef.get).up.contains declName then
+      throw (IO.userError s!"invalid builtin `grind` upward propagator `{declName}`, it has already been declared")
+    builtinPropagatorsRef.modify fun { up, down } => { up := up.insert declName proc, down }
+  else
+    if (← builtinPropagatorsRef.get).down.contains declName then
+      throw (IO.userError s!"invalid builtin `grind` downward propagator `{declName}`, it has already been declared")
+    builtinPropagatorsRef.modify fun { up, down } => { up, down := down.insert declName proc }
+
+def registerBuiltinUpwardPropagator (declName : Name) (proc : Propagator) : IO Unit :=
+  registerBuiltinPropagatorCore declName true proc
+
+def registerBuiltinDownwardPropagator (declName : Name) (proc : Propagator) : IO Unit :=
+  registerBuiltinPropagatorCore declName false proc
+
+private def addBuiltin (propagatorName : Name) (stx : Syntax) : AttrM Unit := do
+  let go : MetaM Unit := do
+    let up := stx[1].getKind == ``Lean.Parser.Tactic.simpPost
+    let addDeclName := if up then
+      ``registerBuiltinUpwardPropagator
+    else
+      ``registerBuiltinDownwardPropagator
+    let declName ← resolveGlobalConstNoOverload stx[2]
+    let val := mkAppN (mkConst addDeclName) #[toExpr declName, mkConst propagatorName]
+    let initDeclName ← mkFreshUserName (propagatorName ++ `declare)
+    declareBuiltin initDeclName val
+  go.run' {}
+
+builtin_initialize
+  registerBuiltinAttribute {
+    ref             := by exact decl_name%
+    name            := `grindPropagatorBuiltinAttr
+    descr           := "Builtin `grind` propagator procedure"
+    applicationTime := AttributeApplicationTime.afterCompilation
+    erase           := fun _ => throwError "Not implemented yet, [-builtin_simproc]"
+    add             := fun declName stx _ => addBuiltin declName stx
+  }
+
+end Lean.Meta.Grind

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

@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Grind.Lemmas
+import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.PropagatorAttr
+import Lean.Meta.Tactic.Grind.Proj
+
+namespace Lean.Meta.Grind
+
+def mkMethods : CoreM Methods := do
+  let builtinPropagators ← builtinPropagatorsRef.get
+  return {
+    propagateUp := fun e => do
+     let .const declName _ := e.getAppFn | return ()
+     propagateProjEq e
+     if let some prop := builtinPropagators.up[declName]? then
+       prop e
+    propagateDown := fun e => do
+     let .const declName _ := e.getAppFn | return ()
+     if let some prop := builtinPropagators.down[declName]? then
+       prop e
+  }
+
+def GrindM.run (x : GrindM α) (mainDeclName : Name) : MetaM α := do
+  let scState := ShareCommon.State.mk _
+  let (falseExpr, scState) := ShareCommon.State.shareCommon scState (mkConst ``False)
+  let (trueExpr, scState)  := ShareCommon.State.shareCommon scState (mkConst ``True)
+  let thms ← grindNormExt.getTheorems
+  let simprocs := #[(← grindNormSimprocExt.getSimprocs)]
+  let simp ← Simp.mkContext
+    (config := { arith := true })
+    (simpTheorems := #[thms])
+    (congrTheorems := (← getSimpCongrTheorems))
+  x (← mkMethods).toMethodsRef { mainDeclName, simprocs, simp } |>.run' { scState, trueExpr, falseExpr }
+
+@[inline] def GoalM.run (goal : Goal) (x : GoalM α) : GrindM (α × Goal) :=
+  goal.mvarId.withContext do StateRefT'.run x goal
+
+@[inline] def GoalM.run' (goal : Goal) (x : GoalM Unit) : GrindM Goal :=
+  goal.mvarId.withContext do StateRefT'.run' (x *> get) goal
+
+def mkGoal (mvarId : MVarId) : GrindM Goal := do
+  let trueExpr ← getTrueExpr
+  let falseExpr ← getFalseExpr
+  GoalM.run' { mvarId } do
+    mkENodeCore falseExpr (interpreted := true) (ctor := false) (generation := 0)
+    mkENodeCore trueExpr (interpreted := true) (ctor := false) (generation := 0)
+
+end Lean.Meta.Grind

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

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Simp.Main
+import Lean.Meta.Tactic.Grind.Util
+import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.MarkNestedProofs
+
+namespace Lean.Meta.Grind
+
+-- TODO: use congruence closure and decision procedures during pre-processing
+-- TODO: implement `simp` discharger using preprocessor state
+
+/-- Simplifies the given expression using the `grind` simprocs and normalization theorems. -/
+def simp (e : Expr) : GrindM Simp.Result := do
+  let simpStats := (← get).simpStats
+  let (r, simpStats) ← Meta.simp e (← readThe Context).simp (← readThe Context).simprocs (stats := simpStats)
+  modify fun s => { s with simpStats }
+  return r
+
+/--
+Simplifies `e` using `grind` normalization theorems and simprocs,
+and then applies several other preprocessing steps.
+-/
+def pre (e : Expr) : GrindM Simp.Result := do
+  let r ← simp e
+  let e' := r.expr
+  let e' ← markNestedProofs e'
+  let e' ← unfoldReducible e'
+  let e' ← eraseIrrelevantMData e'
+  let e' ← foldProjs e'
+  let e' ← normalizeLevels e'
+  let e' ← canon e'
+  let e' ← shareCommon e'
+  trace[grind.simp] "{e}\n===>\n{e'}"
+  return { r with expr := e' }
+
+end Lean.Meta.Grind

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

@@ -8,8 +8,10 @@ import Lean.Util.ShareCommon
 import Lean.Meta.Basic
 import Lean.Meta.CongrTheorems
 import Lean.Meta.AbstractNestedProofs
-import Lean.Meta.Canonicalizer
+import Lean.Meta.Tactic.Simp.Types
 import Lean.Meta.Tactic.Util
+import Lean.Meta.Tactic.Grind.Canon
+import Lean.Meta.Tactic.Grind.Attr
 
 namespace Lean.Meta.Grind
 
@@ -18,12 +20,36 @@ namespace Lean.Meta.Grind
   -- inserted into the E-graph
   unsafe ptrEq a b
 
-structure Context where
-  mainDeclName : Name
+/-- We use this auxiliary constant to mark delayed congruence proofs. -/
+def congrPlaceholderProof := mkConst (Name.mkSimple "[congruence]")
 
 /--
-Key for the congruence theorem cache.
+Returns `true` if `e` is `True`, `False`, or a literal value.
+See `LitValues` for supported literals.
 -/
+def isInterpreted (e : Expr) : MetaM Bool := do
+  if e.isTrue || e.isFalse then return true
+  isLitValue e
+
+register_builtin_option grind.debug : Bool := {
+  defValue := false
+  group    := "debug"
+  descr    := "check invariants after updates"
+}
+
+register_builtin_option grind.debug.proofs : Bool := {
+  defValue := false
+  group    := "debug"
+  descr    := "check proofs between the elements of all equivalence classes"
+}
+
+/-- Context for `GrindM` monad. -/
+structure Context where
+  simp     : Simp.Context
+  simprocs : Array Simp.Simprocs
+  mainDeclName : Name
+
+/-- Key for the congruence theorem cache. -/
 structure CongrTheoremCacheKey where
   f       : Expr
   numArgs : Nat
@@ -36,8 +62,9 @@ instance : BEq CongrTheoremCacheKey where
 instance : Hashable CongrTheoremCacheKey where
   hash a := mixHash (unsafe ptrAddrUnsafe a.f).toUInt64 (hash a.numArgs)
 
+/-- State for the `GrindM` monad. -/
 structure State where
-  canon      : Canonicalizer.State := {}
+  canon      : Canon.State := {}
   /-- `ShareCommon` (aka `Hashconsing`) state. -/
   scState    : ShareCommon.State.{0} ShareCommon.objectFactory := ShareCommon.State.mk _
   /-- Next index for creating auxiliary theorems. -/
@@ -48,29 +75,36 @@ structure State where
   Remark: we currently do not reuse congruence theorems
   -/
   congrThms  : PHashMap CongrTheoremCacheKey CongrTheorem := {}
+  simpStats  : Simp.Stats := {}
   trueExpr   : Expr
   falseExpr  : Expr
 
-abbrev GrindM := ReaderT Context $ StateRefT State MetaM
+private opaque MethodsRefPointed : NonemptyType.{0}
+private def MethodsRef : Type := MethodsRefPointed.type
+instance : Nonempty MethodsRef := MethodsRefPointed.property
 
-def GrindM.run (x : GrindM α) (mainDeclName : Name) : MetaM α := do
-  let scState := ShareCommon.State.mk _
-  let (falseExpr, scState) := ShareCommon.State.shareCommon scState (mkConst ``False)
-  let (trueExpr, scState)  := ShareCommon.State.shareCommon scState (mkConst ``True)
-  x { mainDeclName } |>.run' { scState, trueExpr, falseExpr }
+abbrev GrindM := ReaderT MethodsRef $ ReaderT Context $ StateRefT State MetaM
 
+/-- Returns the internalized `True` constant.  -/
 def getTrueExpr : GrindM Expr := do
   return (← get).trueExpr
 
+/-- Returns the internalized `False` constant.  -/
 def getFalseExpr : GrindM Expr := do
   return (← get).falseExpr
 
+def getMainDeclName : GrindM Name :=
+  return (← readThe Context).mainDeclName
+
+@[inline] def getMethodsRef : GrindM MethodsRef :=
+  read
+
 /--
 Abtracts nested proofs in `e`. This is a preprocessing step performed before internalization.
 -/
 def abstractNestedProofs (e : Expr) : GrindM Expr := do
   let nextIdx := (← get).nextThmIdx
-  let (e, s') ← AbstractNestedProofs.visit e |>.run { baseName := (← read).mainDeclName } |>.run |>.run { nextIdx }
+  let (e, s') ← AbstractNestedProofs.visit e |>.run { baseName := (← getMainDeclName) } |>.run |>.run { nextIdx }
   modify fun s => { s with nextThmIdx := s'.nextIdx }
   return e
 
@@ -79,30 +113,18 @@ Applies hash-consing to `e`. Recall that all expressions in a `grind` goal have
 been hash-consing. We perform this step before we internalize expressions.
 -/
 def shareCommon (e : Expr) : GrindM Expr := do
-  modifyGet fun { canon, scState, nextThmIdx, congrThms, trueExpr, falseExpr } =>
+  modifyGet fun { canon, scState, nextThmIdx, congrThms, trueExpr, falseExpr, simpStats } =>
     let (e, scState) := ShareCommon.State.shareCommon scState e
-    (e, { canon, scState, nextThmIdx, congrThms, trueExpr, falseExpr })
+    (e, { canon, scState, nextThmIdx, congrThms, trueExpr, falseExpr, simpStats })
 
 /--
-Applies the canonicalizer to all subterms of `e`.
+Canonicalizes nested types, type formers, and instances in `e`.
 -/
--- TODO: the current canonicalizer is not a good solution for `grind`.
--- The problem is that two different applications `@f inst_1 a` and `@f inst_2 b`
--- may still have syntaticaally different instances. Thus, if we learn that `a = b`,
--- congruence closure will fail to see that the two applications are congruent.
 def canon (e : Expr) : GrindM Expr := do
   let canonS ← modifyGet fun s => (s.canon, { s with canon := {} })
-  let (e, canonS) ← Canonicalizer.CanonM.run (canonRec e) (s := canonS)
+  let (e, canonS) ← Canon.canon e |>.run canonS
   modify fun s => { s with canon := canonS }
   return e
-where
-  canonRec (e : Expr) : CanonM Expr := do
-    let post (e : Expr) : CanonM TransformStep := do
-      if e.isApp then
-        return .done (← Meta.canon e)
-      else
-        return .done e
-    transform e post
 
 /--
 Creates a congruence theorem for a `f`-applications with `numArgs` arguments.
@@ -169,9 +191,73 @@ structure NewEq where
   proof : Expr
   isHEq : Bool
 
+abbrev ENodes := PHashMap USize ENode
+
+structure CongrKey (enodes : ENodes) where
+  e : Expr
+
+private abbrev toENodeKey (e : Expr) : USize :=
+  unsafe ptrAddrUnsafe e
+
+private def hashRoot (enodes : ENodes) (e : Expr) : UInt64 :=
+  if let some node := enodes.find? (toENodeKey e) then
+    toENodeKey node.root |>.toUInt64
+  else
+    13
+
+private def hasSameRoot (enodes : ENodes) (a b : Expr) : Bool := Id.run do
+  let ka := toENodeKey a
+  let kb := toENodeKey b
+  if ka == kb then
+    return true
+  else
+    let some n1 := enodes.find? ka | return false
+    let some n2 := enodes.find? kb | return false
+    toENodeKey n1.root == toENodeKey n2.root
+
+def congrHash (enodes : ENodes) (e : Expr) : UInt64 :=
+  if e.isAppOfArity ``Lean.Grind.nestedProof 2 then
+    -- We only hash the proposition
+    hashRoot enodes (e.getArg! 0)
+  else
+    go e 17
+where
+  go (e : Expr) (r : UInt64) : UInt64 :=
+    match e with
+    | .app f a => go f (mixHash r (hashRoot enodes a))
+    | _ => mixHash r (hashRoot enodes e)
+
+partial def isCongruent (enodes : ENodes) (a b : Expr) : Bool :=
+  if a.isAppOfArity ``Lean.Grind.nestedProof 2 && b.isAppOfArity ``Lean.Grind.nestedProof 2 then
+    hasSameRoot enodes (a.getArg! 0) (b.getArg! 0)
+  else
+    go a b
+where
+  go (a b : Expr) : Bool :=
+    if a.isApp && b.isApp then
+      hasSameRoot enodes a.appArg! b.appArg! && go a.appFn! b.appFn!
+    else
+      -- Remark: we do not check whether the types of the functions are equal here
+      -- because we are not in the `MetaM` monad.
+      hasSameRoot enodes a b
+
+instance : Hashable (CongrKey enodes) where
+  hash k := congrHash enodes k.e
+
+instance : BEq (CongrKey enodes) where
+  beq k1 k2 := isCongruent enodes k1.e k2.e
+
+abbrev CongrTable (enodes : ENodes) := PHashSet (CongrKey enodes)
+
+-- Remark: we cannot use pointer addresses here because we have to traverse the tree.
+abbrev ParentSet := RBTree Expr Expr.quickComp
+abbrev ParentMap := PHashMap USize ParentSet
+
 structure Goal where
   mvarId       : MVarId
-  enodes       : PHashMap USize ENode := {}
+  enodes       : ENodes := {}
+  parents      : ParentMap := {}
+  congrTable   : CongrTable enodes := {}
   /-- Equations to be processed. -/
   newEqs       : Array NewEq := #[]
   /-- `inconsistent := true` if `ENode`s for `True` and `False` are in the same equivalence class. -/
@@ -187,11 +273,15 @@ def Goal.admit (goal : Goal) : MetaM Unit :=
 
 abbrev GoalM := StateRefT Goal GrindM
 
-@[inline] def GoalM.run (goal : Goal) (x : GoalM α) : GrindM (α × Goal) :=
-  goal.mvarId.withContext do StateRefT'.run x goal
+abbrev Propagator := Expr → GoalM Unit
 
-@[inline] def GoalM.run' (goal : Goal) (x : GoalM Unit) : GrindM Goal :=
-  goal.mvarId.withContext do StateRefT'.run' (x *> get) goal
+/-- Returns `true` if `e` is the internalized `True` expression.  -/
+def isTrueExpr (e : Expr) : GrindM Bool :=
+  return isSameExpr e (← getTrueExpr)
+
+/-- Returns `true` if `e` is the internalized `False` expression.  -/
+def isFalseExpr (e : Expr) : GrindM Bool :=
+  return isSameExpr e (← getFalseExpr)
 
 /--
 Returns `some n` if `e` has already been "internalized" into the
@@ -202,13 +292,51 @@ def getENode? (e : Expr) : GoalM (Option ENode) :=
 
 /-- Returns node associated with `e`. It assumes `e` has already been internalized. -/
 def getENode (e : Expr) : GoalM ENode := do
-  let some n := (← get).enodes.find? (unsafe ptrAddrUnsafe e) | unreachable!
+  let some n := (← get).enodes.find? (unsafe ptrAddrUnsafe e)
+    | throwError "internal `grind` error, term has not been internalized{indentExpr e}"
   return n
 
+/-- Returns the generation of the given term. Is assumes it has been internalized -/
+def getGeneration (e : Expr) : GoalM Nat :=
+  return (← getENode e).generation
+
+/-- Returns `true` if `e` is in the equivalence class of `True`. -/
+def isEqTrue (e : Expr) : GoalM Bool := do
+  let n ← getENode e
+  return isSameExpr n.root (← getTrueExpr)
+
+/-- Returns `true` if `e` is in the equivalence class of `False`. -/
+def isEqFalse (e : Expr) : GoalM Bool := do
+  let n ← getENode e
+  return isSameExpr n.root (← getFalseExpr)
+
+/-- Returns `true` if `a` and `b` are in the same equivalence class. -/
+def isEqv (a b : Expr) : GoalM Bool := do
+  if isSameExpr a b then
+    return true
+  else
+    let na ← getENode a
+    let nb ← getENode b
+    return isSameExpr na.root nb.root
+
+/-- Returns `true` if the root of its equivalence class. -/
+def isRoot (e : Expr) : GoalM Bool := do
+  let some n ← getENode? e | return false -- `e` has not been internalized. Panic instead?
+  return isSameExpr n.root e
+
+/-- Returns the root element in the equivalence class of `e` IF `e` has been internalized. -/
+def getRoot? (e : Expr) : GoalM (Option Expr) := do
+  let some n ← getENode? e | return none
+  return some n.root
+
 /-- Returns the root element in the equivalence class of `e`. -/
 def getRoot (e : Expr) : GoalM Expr :=
   return (← getENode e).root
 
+/-- Returns the root enode in the equivalence class of `e`. -/
+def getRootENode (e : Expr) : GoalM ENode := do
+  getENode (← getRoot e)
+
 /-- Returns the next element in the equivalence class of `e`. -/
 def getNext (e : Expr) : GoalM Expr :=
   return (← getENode e).next
@@ -217,8 +345,86 @@ def getNext (e : Expr) : GoalM Expr :=
 def alreadyInternalized (e : Expr) : GoalM Bool :=
   return (← get).enodes.contains (unsafe ptrAddrUnsafe e)
 
+def getTarget? (e : Expr) : GoalM (Option Expr) := do
+  let some n ← getENode? e | return none
+  return n.target?
+
+/--
+If `isHEq` is `false`, it pushes `lhs = rhs` with `proof` to `newEqs`.
+Otherwise, it pushes `HEq lhs rhs`.
+-/
+def pushEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit :=
+  modify fun s => { s with newEqs := s.newEqs.push { lhs, rhs, proof, isHEq } }
+
+/-- Return `true` if `a` and `b` have the same type. -/
+def hasSameType (a b : Expr) : MetaM Bool :=
+  withDefault do isDefEq (← inferType a) (← inferType b)
+
+@[inline] def pushEqHEq (lhs rhs proof : Expr) : GoalM Unit := do
+  if (← hasSameType lhs rhs) then
+    pushEqCore lhs rhs proof (isHEq := false)
+  else
+    pushEqCore lhs rhs proof (isHEq := true)
+
+/-- Pushes `lhs = rhs` with `proof` to `newEqs`. -/
+@[inline] def pushEq (lhs rhs proof : Expr) : GoalM Unit :=
+  pushEqCore lhs rhs proof (isHEq := false)
+
+/-- Pushes `HEq lhs rhs` with `proof` to `newEqs`. -/
+@[inline] def pushHEq (lhs rhs proof : Expr) : GoalM Unit :=
+  pushEqCore lhs rhs proof (isHEq := true)
+
+/-- Pushes `a = True` with `proof` to `newEqs`. -/
+def pushEqTrue (a proof : Expr) : GoalM Unit := do
+  pushEq a (← getTrueExpr) proof
+
+/-- Pushes `a = False` with `proof` to `newEqs`. -/
+def pushEqFalse (a proof : Expr) : GoalM Unit := do
+  pushEq a (← getFalseExpr) proof
+
+/--
+Records that `parent` is a parent of `child`. This function actually stores the
+information in the root (aka canonical representative) of `child`.
+-/
+def registerParent (parent : Expr) (child : Expr) : GoalM Unit := do
+  let some childRoot ← getRoot? child | return ()
+  let key := toENodeKey childRoot
+  let parents := if let some parents := (← get).parents.find? key then parents else {}
+  modify fun s => { s with parents := s.parents.insert key (parents.insert parent) }
+
+/--
+Returns the set of expressions `e` is a child of, or an expression in
+`e`s equivalence class is a child of.
+The information is only up to date if `e` is the root (aka canonical representative) of the equivalence class.
+-/
+def getParents (e : Expr) : GoalM ParentSet := do
+  let some parents := (← get).parents.find? (toENodeKey e) | return {}
+  return parents
+
+/--
+Similar to `getParents`, but also removes the entry `e ↦ parents` from the parent map.
+-/
+def getParentsAndReset (e : Expr) : GoalM ParentSet := do
+  let parents ← getParents e
+  modify fun s => { s with parents := s.parents.erase (toENodeKey e) }
+  return parents
+
+/--
+Copy `parents` to the parents of `root`.
+`root` must be the root of its equivalence class.
+-/
+def copyParentsTo (parents : ParentSet) (root : Expr) : GoalM Unit := do
+  let key := toENodeKey root
+  let mut curr := if let some parents := (← get).parents.find? key then parents else {}
+  for parent in parents do
+    curr := curr.insert parent
+  modify fun s => { s with parents := s.parents.insert key curr }
+
 def setENode (e : Expr) (n : ENode) : GoalM Unit :=
-  modify fun s => { s with enodes := s.enodes.insert (unsafe ptrAddrUnsafe e) n }
+  modify fun s => { s with
+    enodes := s.enodes.insert (unsafe ptrAddrUnsafe e) n
+    congrTable := unsafe unsafeCast s.congrTable
+  }
 
 def mkENodeCore (e : Expr) (interpreted ctor : Bool) (generation : Nat) : GoalM Unit := do
   setENode e {
@@ -232,11 +438,123 @@ def mkENodeCore (e : Expr) (interpreted ctor : Bool) (generation : Nat) : GoalM
   }
   modify fun s => { s with nextIdx := s.nextIdx + 1 }
 
-def mkGoal (mvarId : MVarId) : GrindM Goal := do
-  let trueExpr ← getTrueExpr
-  let falseExpr ← getFalseExpr
-  GoalM.run' { mvarId } do
-    mkENodeCore falseExpr (interpreted := true) (ctor := false) (generation := 0)
-    mkENodeCore trueExpr (interpreted := true) (ctor := false) (generation := 0)
+/--
+Creates an `ENode` for `e` if one does not already exist.
+This method assumes `e` has been hashconsed.
+-/
+def mkENode (e : Expr) (generation : Nat) : GoalM Unit := do
+  if (← alreadyInternalized e) then return ()
+  let ctor := (← isConstructorAppCore? e).isSome
+  let interpreted ← isInterpreted e
+  mkENodeCore e interpreted ctor generation
+
+/-- Return `true` if the goal is inconsistent. -/
+def isInconsistent : GoalM Bool :=
+  return (← get).inconsistent
+
+/--
+Returns a proof that `a = b` (or `HEq a b`).
+It assumes `a` and `b` are in the same equivalence class.
+-/
+-- Forward definition
+@[extern "lean_grind_mk_eq_proof"]
+opaque mkEqProof (a b : Expr) : GoalM Expr
+
+/--
+Returns a proof that `a = True`.
+It assumes `a` and `True` are in the same equivalence class.
+-/
+def mkEqTrueProof (a : Expr) : GoalM Expr := do
+  mkEqProof a (← getTrueExpr)
+
+/--
+Returns a proof that `a = False`.
+It assumes `a` and `False` are in the same equivalence class.
+-/
+def mkEqFalseProof (a : Expr) : GoalM Expr := do
+  mkEqProof a (← getFalseExpr)
+
+/-- Marks current goal as inconsistent without assigning `mvarId`. -/
+def markAsInconsistent : GoalM Unit := do
+  modify fun s => { s with inconsistent := true }
+
+/--
+Closes the current goal using the given proof of `False` and
+marks it as inconsistent if it is not already marked so.
+-/
+def closeGoal (falseProof : Expr) : GoalM Unit := do
+  markAsInconsistent
+  let mvarId := (← get).mvarId
+  unless (← mvarId.isAssigned) do
+    let target ← mvarId.getType
+    if target.isFalse then
+      mvarId.assign falseProof
+    else
+      mvarId.assign (← mkFalseElim target falseProof)
+
+/-- Returns all enodes in the goal -/
+def getENodes : GoalM (Array ENode) := do
+  -- We must sort because we are using pointer addresses as keys in `enodes`
+  let nodes := (← get).enodes.toArray.map (·.2)
+  return nodes.qsort fun a b => a.idx < b.idx
+
+def forEachENode (f : ENode → GoalM Unit) : GoalM Unit := do
+  let nodes ← getENodes
+  for n in nodes do
+    f n
+
+def filterENodes (p : ENode → GoalM Bool) : GoalM (Array ENode) := do
+  let ref ← IO.mkRef #[]
+  forEachENode fun n => do
+    if (← p n) then
+      ref.modify (·.push n)
+  ref.get
+
+def forEachEqc (f : ENode → GoalM Unit) : GoalM Unit := do
+  let nodes ← getENodes
+  for n in nodes do
+    if isSameExpr n.self n.root then
+      f n
+
+structure Methods where
+  propagateUp   : Propagator := fun _ => return ()
+  propagateDown : Propagator := fun _ => return ()
+  deriving Inhabited
+
+def Methods.toMethodsRef (m : Methods) : MethodsRef :=
+  unsafe unsafeCast m
+
+private def MethodsRef.toMethods (m : MethodsRef) : Methods :=
+  unsafe unsafeCast m
+
+@[inline] def getMethods : GrindM Methods :=
+  return (← getMethodsRef).toMethods
+
+def propagateUp (e : Expr) : GoalM Unit := do
+  (← getMethods).propagateUp e
+
+def propagateDown (e : Expr) : GoalM Unit := do
+  (← getMethods).propagateDown e
+
+/-- Returns expressions in the given expression equivalence class. -/
+partial def getEqc (e : Expr) : GoalM (List Expr) :=
+  go e e []
+where
+  go (first : Expr) (e : Expr) (acc : List Expr) : GoalM (List Expr) := do
+    let next ← getNext e
+    let acc := e :: acc
+    if isSameExpr first next then
+      return acc
+    else
+      go first next acc
+
+/-- Returns all equivalence classes in the current goal. -/
+partial def getEqcs : GoalM (List (List Expr)) := do
+  let mut r := []
+  let nodes ← getENodes
+  for node in nodes do
+    if isSameExpr node.root node.self then
+      r := (← getEqc node.self) :: r
+  return r
 
 end Lean.Meta.Grind

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

@@ -124,4 +124,15 @@ def foldProjs (e : Expr) : MetaM Expr := do
       return .done e
   Meta.transform e (post := post)
 
+/--
+Normalizes universe levels in constants and sorts.
+-/
+def normalizeLevels (e : Expr) : CoreM Expr := do
+  let pre (e : Expr) := do
+    match e with
+    | .sort u => return .done <| e.updateSort! u.normalize
+    | .const _ us => return .done <| e.updateConst! (us.map Level.normalize)
+    | _ => return .continue
+  Core.transform e (pre := pre)
+
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean

@@ -49,17 +49,13 @@ If they do, they must disable the following `simprocs`.
 -/
 
 builtin_dsimproc [simp, seval] reduceNeg ((- _ : Int)) := fun e => do
-  unless e.isAppOfArity ``Neg.neg 3 do return .continue
-  let arg := e.appArg!
+  let_expr Neg.neg _ _ arg ← e | return .continue
   if arg.isAppOfArity ``OfNat.ofNat 3 then
     -- We return .done to ensure `Neg.neg` is not unfolded even when `ground := true`.
     return .done e
   else
     let some v ← fromExpr? arg | return .continue
-    if v < 0 then
-      return .done <| toExpr (- v)
-    else
-      return .done <| toExpr v
+    return .done <| toExpr (- v)
 
 /-- Return `.done` for positive Int values. We don't want to unfold in the symbolic evaluator. -/
 builtin_dsimproc [seval] isPosValue ((OfNat.ofNat _ : Int)) := fun e => do

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

@@ -47,6 +47,17 @@ def isOfScientificLit (e : Expr) : Bool :=
 def isCharLit (e : Expr) : Bool :=
   e.isAppOfArity ``Char.ofNat 1 && e.appArg!.isRawNatLit
 
+/--
+Unfold definition even if it is not marked as `@[reducible]`.
+Remark: We never unfold irreducible definitions. Mathlib relies on that in the implementation of the
+command `irreducible_def`.
+-/
+private def unfoldDefinitionAny? (e : Expr) : MetaM (Option Expr) := do
+  if let .const declName _ := e.getAppFn then
+    if (← isIrreducible declName) then
+      return none
+  unfoldDefinition? e (ignoreTransparency := true)
+
 private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do
   matchConst e.getAppFn (fun _ => pure none) fun cinfo _ => do
     match (← getProjectionFnInfo? cinfo.name) with
@@ -83,7 +94,7 @@ private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do
           let major := e.getArg! projInfo.numParams
           unless (← isConstructorApp major) do
             return none
-          reduceProjCont? (← withDefault <| unfoldDefinition? e)
+          reduceProjCont? (← unfoldDefinitionAny? e)
       else
         -- `structure` projections
         reduceProjCont? (← unfoldDefinition? e)
@@ -133,7 +144,7 @@ private def unfold? (e : Expr) : SimpM (Option Expr) := do
     if cfg.unfoldPartialApp -- If we are unfolding partial applications, ignore issue #2042
        -- When smart unfolding is enabled, and `f` supports it, we don't need to worry about issue #2042
        || (smartUnfolding.get options && (← getEnv).contains (mkSmartUnfoldingNameFor fName)) then
-      withDefault <| unfoldDefinition? e
+      unfoldDefinitionAny? e
     else
       -- `We are not unfolding partial applications, and `fName` does not have smart unfolding support.
       -- Thus, we must check whether the arity of the function >= number of arguments.
@@ -142,16 +153,16 @@ private def unfold? (e : Expr) : SimpM (Option Expr) := do
       let arity := value.getNumHeadLambdas
       -- Partially applied function, return `none`. See issue #2042
       if arity > e.getAppNumArgs then return none
-      withDefault <| unfoldDefinition? e
+      unfoldDefinitionAny? e
   if (← isProjectionFn fName) then
     return none -- should be reduced by `reduceProjFn?`
   else if ctx.config.autoUnfold then
     if ctx.simpTheorems.isErased (.decl fName) then
       return none
     else if hasSmartUnfoldingDecl (← getEnv) fName then
-      withDefault <| unfoldDefinition? e
+      unfoldDefinitionAny? e
     else if (← isMatchDef fName) then
-      let some value ← withDefault <| unfoldDefinition? e | return none
+      let some value ← unfoldDefinitionAny? e | return none
       let .reduced value ← withSimpMetaConfig <| reduceMatcher? value | return none
       return some value
     else

src/Lean/Meta/WHNF.lean

@@ -64,10 +64,38 @@ def isAuxDef (constName : Name) : MetaM Bool := do
   let env ← getEnv
   return isAuxRecursor env constName || isNoConfusion env constName
 
-@[inline] private def matchConstAux {α} (e : Expr) (failK : Unit → MetaM α) (k : ConstantInfo → List Level → MetaM α) : MetaM α := do
-  let .const name lvls := e
+/--
+Retrieves `ConstInfo` for `declName`.
+Remark: if `ignoreTransparency = false`, then `getUnfoldableConst?` is used.
+For example, if `ignoreTransparency = false` and `transparencyMode = .reducible` and `declName` is not reducible,
+then the result is `none`.
+-/
+private def getConstInfo? (declName : Name) (ignoreTransparency : Bool) : MetaM (Option ConstantInfo) := do
+  if ignoreTransparency then
+    return (← getEnv).find? declName
+  else
+    getUnfoldableConst? declName
+
+/--
+Similar to `getConstInfo?` but using `getUnfoldableConstNoEx?`.
+-/
+private def getConstInfoNoEx? (declName : Name) (ignoreTransparency : Bool) : MetaM (Option ConstantInfo) := do
+  if ignoreTransparency then
+    return (← getEnv).find? declName
+  else
+    getUnfoldableConstNoEx? declName
+
+/--
+If `e` is of the form `Expr.const declName us`, executes `k info us` if
+- `declName` is in the `Environment` and (is unfoldable or `ignoreTransparency = true`)
+- `info` is the `ConstantInfo` associated with `declName`.
+
+Otherwise executes `failK`.
+-/
+@[inline] private def matchConstAux {α} (e : Expr) (failK : Unit → MetaM α) (k : ConstantInfo → List Level → MetaM α) (ignoreTransparency := false) : MetaM α := do
+  let .const declName lvls := e
     | failK ()
-  let (some cinfo) ← getUnfoldableConst? name
+  let some cinfo ← getConstInfo? declName ignoreTransparency
     | failK ()
   k cinfo lvls
 
@@ -713,11 +741,14 @@ mutual
     else
       unfoldProjInst? e
 
-  /-- Unfold definition using "smart unfolding" if possible. -/
-  partial def unfoldDefinition? (e : Expr) : MetaM (Option Expr) :=
+  /--
+  Unfold definition using "smart unfolding" if possible.
+  If `ignoreTransparency = true`, then the definition is unfolded even if the transparency setting does not allow it.
+  -/
+  partial def unfoldDefinition? (e : Expr) (ignoreTransparency := false) : MetaM (Option Expr) :=
     match e with
     | .app f _ =>
-      matchConstAux f.getAppFn (fun _ => unfoldProjInstWhenInstances? e) fun fInfo fLvls => do
+      matchConstAux (ignoreTransparency := ignoreTransparency) f.getAppFn (fun _ => unfoldProjInstWhenInstances? e) fun fInfo fLvls => do
         if fInfo.levelParams.length != fLvls.length then
           return none
         else
@@ -756,7 +787,8 @@ mutual
 
                   Remark 2: the match expression reduces reduces to `cons a xs` when the discriminants are `⟨0, h⟩` and `xs`.
 
-                  Remark 3: this check is unnecessary in most cases, but we don't need dependent elimination to trigger the issue                        fixed by this extra check. Here is another example that triggers the issue fixed by this check.
+                  Remark 3: this check is unnecessary in most cases, but we don't need dependent elimination to trigger the issue
+                  fixed by this extra check. Here is another example that triggers the issue fixed by this check.
                   ```
                   def f : Nat → Nat → Nat
                     | 0,   y   => y
@@ -788,7 +820,7 @@ mutual
           else
             unfoldDefault ()
     | .const declName lvls => do
-      let some cinfo ← getUnfoldableConstNoEx? declName | pure none
+      let some cinfo ← getConstInfoNoEx? declName ignoreTransparency | pure none
       -- check smart unfolding only after `getUnfoldableConstNoEx?` because smart unfoldings have a
       -- significant chance of not existing and `Environment.contains` misses are more costly
       if smartUnfolding.get (← getOptions) && (← getEnv).contains (mkSmartUnfoldingNameFor declName) then

src/Lean/Util.lean

@@ -34,3 +34,4 @@ import Lean.Util.SearchPath
 import Lean.Util.SafeExponentiation
 import Lean.Util.NumObjs
 import Lean.Util.NumApps
+import Lean.Util.FVarSubset

src/Lean/Util/CollectFVars.lean

@@ -26,14 +26,14 @@ mutual
     else main e { s with visitedExpr := s.visitedExpr.insert e }
 
   partial def main : Expr → Visitor
-    | Expr.proj _ _ e      => visit e
-    | Expr.forallE _ d b _ => visit b ∘ visit d
-    | Expr.lam _ d b _     => visit b ∘ visit d
-    | Expr.letE _ t v b _  => visit b ∘ visit v ∘ visit t
-    | Expr.app f a         => visit a ∘ visit f
-    | Expr.mdata _ b       => visit b
-    | Expr.fvar fvarId     => fun s => s.add fvarId
-    | _                    => id
+    | .proj _ _ e      => visit e
+    | .forallE _ d b _ => visit b ∘ visit d
+    | .lam _ d b _     => visit b ∘ visit d
+    | .letE _ t v b _  => visit b ∘ visit v ∘ visit t
+    | .app f a         => visit a ∘ visit f
+    | .mdata _ b       => visit b
+    | .fvar fvarId     => fun s => s.add fvarId
+    | _                => id
 end
 
 end CollectFVars

src/Lean/Util/FVarSubset.lean

@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Util.CollectFVars
+import Lean.Util.FindExpr
+
+namespace Lean.Expr
+
+/-- Returns true if the free variables in `a` are subset of the free variables in `b`. -/
+def fvarsSubset (a b : Expr) : Bool :=
+  if !a.hasFVar then
+    true -- Empty set is subset of anything
+  else if !b.hasFVar then
+    false -- Empty set is not a superset of a nonempty set.
+  else
+    let s := collectFVars {} b
+    Option.isNone <| a.findExt? fun e =>
+      if !e.hasFVar then .done
+      else if e.isFVar && !s.fvarSet.contains e.fvarId! then .found
+      else .visit
+
+end Lean.Expr

src/Lean/Util/FindExpr.lean

@@ -14,25 +14,24 @@ opaque findImpl? (p : @& (Expr → Bool)) (e : @& Expr) : Option Expr
 
 @[inline] def find? (p : Expr → Bool) (e : Expr) : Option Expr := findImpl? p e
 
-/-- Return true if `e` occurs in `t` -/
+/-- Returns 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.
+Returns type for `findExt?` function argument.
 -/
 inductive FindStep where
-  /-- Found desired subterm -/ | found
-  /-- Search subterms -/ | visit
-  /-- Do not search subterms -/ | done
+  | /-- Found desired subterm -/ found
+  | /-- Search subterms -/ visit
+  | /-- Do not search subterms -/ done
 
 @[extern "lean_find_ext_expr"]
 opaque findExtImpl? (p : @& (Expr → FindStep)) (e : @& Expr) : Option Expr
 
 /--
-  Similar to `find?`, but `p` can return `FindStep.done` to interrupt the search on subterms.
-  Remark: Differently from `find?`, we do not invoke `p` for partial applications of an application. -/
+Similar to `find?`, but `p` can return `FindStep.done` to interrupt the search on subterms.
+Remark: Differently from `find?`, we do not invoke `p` for partial applications of an application. -/
 @[inline] def findExt? (p : Expr → FindStep) (e : Expr) : Option Expr := findExtImpl? p e
 
-end Expr
-end Lean
+end Lean.Expr

src/Lean/Util/ForEachExpr.lean

@@ -20,13 +20,13 @@ def visit (g : Expr → m Bool) (e : Expr) : MonadCacheT Expr Unit m Unit :=
   checkCache e fun _ => do
     if (← g e) then
       match e with
-      | Expr.forallE _ d b _   => do visit g d; visit g b
-      | Expr.lam _ d b _       => do visit g d; visit g b
-      | Expr.letE _ t v b _    => do visit g t; visit g v; visit g b
-      | Expr.app f a           => do visit g f; visit g a
-      | Expr.mdata _ b         => visit g b
-      | Expr.proj _ _ b        => visit g b
-      | _                      => pure ()
+      | .forallE _ d b _   => do visit g d; visit g b
+      | .lam _ d b _       => do visit g d; visit g b
+      | .letE _ t v b _    => do visit g t; visit g v; visit g b
+      | .app f a           => do visit g f; visit g a
+      | .mdata _ b         => visit g b
+      | .proj _ _ b        => visit g b
+      | _                  => pure ()
 
 end ForEachExpr
 

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean

@@ -293,8 +293,15 @@ The semantics for `BVExpr`.
 -/
 def eval (assign : Assignment) : BVExpr w → BitVec w
   | .var idx =>
-    let ⟨bv⟩ := assign.get idx
-    bv.truncate w
+    let packedBv := assign.get idx
+    /-
+    This formulation improves performance, as in a well formed expression the condition always holds
+    so there is no need for the more involved `BitVec.truncate` logic.
+    -/
+    if h : packedBv.w = w then
+      h ▸ packedBv.bv
+    else
+      packedBv.bv.truncate w
   | .const val => val
   | .zeroExtend v expr => BitVec.zeroExtend v (eval assign expr)
   | .extract start len expr => BitVec.extractLsb' start len (eval assign expr)
@@ -308,8 +315,13 @@ def eval (assign : Assignment) : BVExpr w → BitVec w
   | .arithShiftRight lhs rhs => BitVec.sshiftRight' (eval assign lhs) (eval assign rhs)
 
 @[simp]
-theorem eval_var : eval assign ((.var idx) : BVExpr w) = (assign.get idx).bv.truncate _ := by
-  rfl
+theorem eval_var : eval assign ((.var idx) : BVExpr w) = (assign.get idx).bv.truncate w := by
+  rw [eval]
+  split
+  · next h =>
+    subst h
+    simp
+  · rfl
 
 @[simp]
 theorem eval_const : eval assign (.const val) = val := by rfl
@@ -454,7 +466,7 @@ def eval (assign : BVExpr.Assignment) (expr : BVLogicalExpr) : Bool :=
 @[simp] theorem eval_not : eval assign (.not x) = !eval assign x := rfl
 @[simp] theorem eval_gate : eval assign (.gate g x y) = g.eval (eval assign x) (eval assign y) := rfl
 @[simp] theorem eval_ite :
-  eval assign (.ite d l r) = if (eval assign d) then (eval assign l) else (eval assign r) := rfl
+  eval assign (.ite d l r) = bif (eval assign d) then (eval assign l) else (eval assign r) := rfl
 
 def Sat (x : BVLogicalExpr) (assign : BVExpr.Assignment) : Prop := eval assign x = true
 

src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean

@@ -18,7 +18,7 @@ inductive Gate
   | and
   | xor
   | beq
-  | imp
+  | or
 
 namespace Gate
 
@@ -26,13 +26,13 @@ def toString : Gate → String
   | and => "&&"
   | xor => "^^"
   | beq => "=="
-  | imp => "->"
+  | or => "||"
 
 def eval : Gate → Bool → Bool → Bool
   | and => (· && ·)
   | xor => (· ^^ ·)
   | beq => (· == ·)
-  | imp => (· → ·)
+  | or => (· || ·)
 
 end Gate
 
@@ -59,13 +59,13 @@ def eval (a : α → Bool) : BoolExpr α → Bool
   | .const b => b
   | .not x => !eval a x
   | .gate g x y => g.eval (eval a x) (eval a y)
-  | .ite d l r => if d.eval a then l.eval a else r.eval a
+  | .ite d l r => bif d.eval a then l.eval a else r.eval a
 
 @[simp] theorem eval_literal : eval a (.literal l) = a l := rfl
 @[simp] theorem eval_const : eval a (.const b) = b := rfl
 @[simp] theorem eval_not : eval a (.not x) = !eval a x := rfl
 @[simp] theorem eval_gate : eval a (.gate g x y) = g.eval (eval a x) (eval a y) := rfl
-@[simp] theorem eval_ite : eval a (.ite d l r) = if d.eval a then l.eval a else r.eval a := rfl
+@[simp] theorem eval_ite : eval a (.ite d l r) = bif d.eval a then l.eval a else r.eval a := rfl
 
 def Sat (a : α → Bool) (x : BoolExpr α) : Prop := eval a x = true
 def Unsat (x : BoolExpr α) : Prop := ∀ f, eval f x = false

src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean

@@ -75,9 +75,9 @@ where
         let ret := aig.mkBEqCached input
         have := LawfulOperator.le_size (f := mkBEqCached) aig input
         ⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩
-      | .imp =>
-        let ret := aig.mkImpCached input
-        have := LawfulOperator.le_size (f := mkImpCached) aig input
+      | .or =>
+        let ret := aig.mkOrCached input
+        have := LawfulOperator.le_size (f := mkOrCached) aig input
         ⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩
 
 namespace ofBoolExprCached
@@ -127,9 +127,9 @@ theorem go_decl_eq (idx) (aig : AIG β) (h : idx < aig.decls.size) (hbounds) :
     | beq =>
       simp only [go]
       rw [AIG.LawfulOperator.decl_eq (f := mkBEqCached), rih, lih]
-    | imp =>
+    | or =>
       simp only [go]
-      rw [AIG.LawfulOperator.decl_eq (f := mkImpCached), rih, lih]
+      rw [AIG.LawfulOperator.decl_eq (f := mkOrCached), rih, lih]
 
 theorem go_isPrefix_aig {aig : AIG β} :
     IsPrefix aig.decls (go aig expr atomHandler).val.aig.decls := by

src/Std/Tactic/BVDecide/Normalize/BitVec.lean

@@ -118,7 +118,6 @@ theorem BitVec.srem_umod (x y : BitVec w) :
   rw [BitVec.srem_eq]
   cases x.msb <;> cases y.msb <;> simp
 
-attribute [bv_normalize] Bool.cond_eq_if
 attribute [bv_normalize] BitVec.abs_eq
 attribute [bv_normalize] BitVec.twoPow_eq
 

src/Std/Tactic/BVDecide/Normalize/Bool.lean

@@ -41,7 +41,14 @@ attribute [bv_normalize] Bool.not_not
 attribute [bv_normalize] Bool.and_self_left
 attribute [bv_normalize] Bool.and_self_right
 attribute [bv_normalize] eq_self
-attribute [bv_normalize] ite_self
+attribute [bv_normalize] Bool.cond_self
+attribute [bv_normalize] cond_false
+attribute [bv_normalize] cond_true
+attribute [bv_normalize] Bool.cond_not
+
+@[bv_normalize]
+theorem if_eq_cond {b : Bool} {x y : α} : (if b = true then x else y) = (bif b then x else y) := by
+  rw [cond_eq_if]
 
 @[bv_normalize]
 theorem Bool.not_xor : ∀ (a b : Bool), !(a ^^ b) = (a == b) := by decide

src/Std/Tactic/BVDecide/Normalize/Prop.lean

@@ -13,8 +13,6 @@ This module contains the `Prop` simplifying part of the `bv_normalize` simp set.
 namespace Std.Tactic.BVDecide
 namespace Frontend.Normalize
 
-attribute [bv_normalize] ite_true
-attribute [bv_normalize] ite_false
 attribute [bv_normalize] dite_true
 attribute [bv_normalize] dite_false
 attribute [bv_normalize] and_true

src/Std/Tactic/BVDecide/Reflect.lean

@@ -123,12 +123,12 @@ theorem umod_congr (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' =
     (lhs' % rhs') = (lhs % rhs) := by
   simp[*]
 
-theorem if_true (discr : Bool) (lhs rhs : BitVec w) :
-    decide ((discr == true) = true → ((if discr = true then lhs else rhs) == lhs) = true) = true := by
+theorem cond_true (discr : Bool) (lhs rhs : BitVec w) :
+    (!discr || ((bif discr then lhs else rhs) == lhs)) = true := by
   cases discr <;> simp
 
-theorem if_false (discr : Bool) (lhs rhs : BitVec w) :
-    decide ((discr == false) = true → ((if discr = true then lhs else rhs) == rhs) = true) = true := by
+theorem cond_false (discr : Bool) (lhs rhs : BitVec w) :
+    (discr || ((bif discr then lhs else rhs) == rhs)) = true := by
   cases discr <;> simp
 
 end BitVec
@@ -150,13 +150,13 @@ theorem beq_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs)
     (lhs' == rhs') = (lhs == rhs) := by
   simp[*]
 
-theorem imp_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
-    (decide (lhs' → rhs')) = (decide (lhs → rhs)) := by
+theorem or_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
+    (lhs' || rhs') = (lhs || rhs) := by
   simp[*]
 
-theorem ite_congr (discr lhs rhs discr' lhs' rhs' : Bool) (h1 : discr' = discr) (h2 : lhs' = lhs)
+theorem cond_congr (discr lhs rhs discr' lhs' rhs' : Bool) (h1 : discr' = discr) (h2 : lhs' = lhs)
     (h3 : rhs' = rhs) :
-    (if discr' = true then lhs' else rhs') = (if discr = true then lhs else rhs) := by
+    (bif discr' = true then lhs' else rhs') = (bif discr = true then lhs else rhs) := by
   simp[*]
 
 theorem false_of_eq_true_of_eq_false (h₁ : x = true) (h₂ : x = false) : False := by