chore: fix signature of perm_insertIdx

This PR avoids unnecessarily importing "kitchen sink" files.

doc/dev/release_checklist.md

@@ -5,11 +5,6 @@ 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,12 +76,16 @@ We'll use `v4.6.0` as the intended release version as a running example.
       - Toolchain bump PR including updated Lake manifest
       - Create and push the tag
       - There is no `stable` branch; skip this step
+    - [plausible](https://github.com/leanprover-community/plausible)
+      - Toolchain bump PR including updated Lake manifest
+      - Create and push the tag
+      - There is no `stable` branch; skip this step
     - [Mathlib](https://github.com/leanprover-community/mathlib4)
       - Dependencies: `Aesop`, `ProofWidgets4`, `lean4checker`, `Batteries`, `doc-gen4`, `import-graph`
       - 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`.
@@ -139,16 +138,13 @@ 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.`
-- 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.
+- 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.
@@ -248,15 +244,12 @@ Please read https://leanprover-community.github.io/contribute/tags_and_branches.
 
 # Writing the release notes
 
-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:
+Release notes are automatically generated from the commit history, using `script/release_notes.py`.
 
-* 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.
+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.
   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

@@ -0,0 +1,145 @@
+#!/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/List/Perm.lean

@@ -510,4 +510,18 @@ theorem Perm.eraseP (f : α → Bool) {l₁ l₂ : List α}
     refine (IH₁ H).trans (IH₂ ((p₁.pairwise_iff ?_).1 H))
     exact fun h h₁ h₂ => h h₂ h₁
 
+theorem perm_insertIdx {α} (x : α) (l : List α) {n} (h : n ≤ l.length) :
+    insertIdx n x l ~ x :: l := by
+  induction l generalizing n with
+  | nil =>
+    cases n with
+    | zero => rfl
+    | succ => cases h
+  | cons _ _ ih =>
+    cases n with
+    | zero => simp [insertIdx]
+    | succ =>
+      simp only [insertIdx, modifyTailIdx]
+      refine .trans (.cons _ (ih (Nat.le_of_succ_le_succ h))) (.swap ..)
+
 end List

src/Init/Data/List/Sort/Lemmas.lean

@@ -253,6 +253,10 @@ theorem merge_perm_append : ∀ {xs ys : List α}, merge xs ys le ~ xs ++ ys
     · exact (merge_perm_append.cons y).trans
         ((Perm.swap x y _).trans (perm_middle.symm.cons x))
 
+theorem Perm.merge (s₁ s₂ : α → α → Bool) (hl : l₁ ~ l₂) (hr : r₁ ~ r₂) :
+    merge l₁ r₁ s₁ ~ merge l₂ r₂ s₂ :=
+  Perm.trans (merge_perm_append ..) <| Perm.trans (Perm.append hl hr) <| Perm.symm (merge_perm_append ..)
+
 /-! ### mergeSort -/
 
 @[simp] theorem mergeSort_nil : [].mergeSort r = [] := by rw [List.mergeSort]

src/Init/Grind/Norm.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.SimpLemmas
+import Init.PropLemmas
 import Init.Classical
 import Init.ByCases
 
@@ -64,7 +65,7 @@ attribute [grind_norm] forall_and
 
 -- Exists
 @[grind_norm↓] theorem not_exists (p : α → Prop) : (¬∃ x, p x) = ∀ x, ¬p x := by simp
-attribute [grind_norm] exists_const exists_or
+attribute [grind_norm] exists_const exists_or exists_prop exists_and_left exists_and_right
 
 -- Bool cond
 @[grind_norm] theorem cond_eq_ite (c : Bool) (a b : α) : cond c a b = ite c a b := by

src/Init/Grind/Tactics.lean

@@ -28,6 +28,8 @@ structure Config where
   gen : Nat := 5
   /-- Maximum number of theorem instances generated using E-matching in a proof search tree branch. -/
   instances : Nat := 1000
+  /-- If `matchEqs` is `true`, `grind` uses `match`-equations as E-matching theorems. -/
+  matchEqs : Bool := true
   deriving Inhabited, BEq
 
 end Lean.Grind

src/Init/Grind/Util.lean

@@ -11,6 +11,13 @@ namespace Lean.Grind
 /-- A helper gadget for annotating nested proofs in goals. -/
 def nestedProof (p : Prop) (h : p) : p := h
 
+/--
+Gadget for marking terms that should not be normalized by `grind`s simplifier.
+`grind` uses a simproc to implement this feature.
+We use it when adding instances of `match`-equations to prevent them from being simplified to true.
+-/
+def doNotSimp {α : Sort u} (a : α) : α := a
+
 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

src/Lean/Data/Lsp/Utf16.lean

@@ -6,7 +6,6 @@ Authors: Marc Huisinga, Wojciech Nawrocki
 -/
 prelude
 import Init.Data.String
-import Init.Data.Array
 import Lean.Data.Lsp.Basic
 import Lean.Data.Position
 import Lean.DeclarationRange

src/Lean/Linter/MissingDocs.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 prelude
+import Lean.Parser.Syntax
 import Lean.Meta.Tactic.Simp.RegisterCommand
 import Lean.Elab.Command
 import Lean.Elab.SetOption

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

@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Grind.Util
+import Init.Simproc
+import Lean.Meta.Tactic.Simp.Simproc
+
+namespace Lean.Meta.Grind
+
+/--
+Returns `Grind.doNotSimp e`.
+Recall that `Grind.doNotSimp` is an identity function, but the following simproc is used to prevent the term `e` from being simplified.
+-/
+def markAsDoNotSimp (e : Expr) : MetaM Expr :=
+  mkAppM ``Grind.doNotSimp #[e]
+
+builtin_dsimproc_decl reduceDoNotSimp (Grind.doNotSimp _) := fun e => do
+  let_expr Grind.doNotSimp _ _ ← e | return .continue
+  return .done e
+
+/-- Adds `reduceDoNotSimp` to `s` -/
+def addDoNotSimp (s : Simprocs) : CoreM Simprocs := do
+  s.add ``reduceDoNotSimp (post := false)
+
+/-- Erases `Grind.doNotSimp` annotations. -/
+def eraseDoNotSimp (e : Expr) : CoreM Expr := do
+  let pre (e : Expr) := do
+    let_expr Grind.doNotSimp _ a := e | return .continue e
+    return .continue a
+  Core.transform e (pre := pre)
+
+end Lean.Meta.Grind

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

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Intro
+import Lean.Meta.Tactic.Grind.DoNotSimp
 
 namespace Lean.Meta.Grind
 namespace EMatch
@@ -146,6 +147,15 @@ private def processContinue (c : Choice) (p : Expr) : M Unit := do
         let c := { c with gen := Nat.max gen c.gen }
         modify fun s => { s with choiceStack := c :: s.choiceStack }
 
+/-- Helper function for marking parts of `match`-equation theorem as "do-not-simplify" -/
+private partial def annotateMatchEqnType (prop : Expr) : M Expr := do
+  if let .forallE n d b bi := prop then
+    withLocalDecl n bi (← markAsDoNotSimp d) fun x => do
+      mkForallFVars #[x] (← annotateMatchEqnType (b.instantiate1 x))
+  else
+    let_expr f@Eq α lhs rhs := prop | return prop
+    return mkApp3 f α (← markAsDoNotSimp lhs) rhs
+
 /--
 Stores new theorem instance in the state.
 Recall that new instances are internalized later, after a full round of ematching.
@@ -154,7 +164,9 @@ private def addNewInstance (origin : Origin) (proof : Expr) (generation : Nat) :
   let proof ← instantiateMVars proof
   if grind.debug.proofs.get (← getOptions) then
     check proof
-  let prop ← inferType proof
+  let mut prop ← inferType proof
+  if Match.isMatchEqnTheorem (← getEnv) origin.key then
+    prop ← annotateMatchEqnType prop
   trace[grind.ematch.instance] "{← origin.pp}: {prop}"
   addTheoremInstance proof prop generation
 
@@ -189,10 +201,10 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w
       unless (← synthesizeInstance mvar type) do
         trace[grind.issues] "failed to synthesize instance when instantiating {← thm.origin.pp}{indentExpr type}"
         return ()
+  let proof := mkAppN proof mvars
   if (← mvars.allM (·.mvarId!.isAssigned)) then
-    addNewInstance thm.origin (mkAppN proof mvars) c.gen
+    addNewInstance thm.origin proof c.gen
   else
-    let proof := mkAppN proof mvars
     let mvars ← mvars.filterM fun mvar => return !(← mvar.mvarId!.isAssigned)
     if let some mvarBad ← mvars.findM? fun mvar => return !(← isProof mvar) then
       trace[grind.issues] "failed to instantiate {← thm.origin.pp}, failed to instantiate non propositional argument with type{indentExpr (← inferType mvarBad)}"

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

@@ -56,17 +56,47 @@ structure EMatchTheorem where
   origin      : Origin
   deriving Inhabited
 
-/-- The key is a symbol from `EMatchTheorem.symbols`. -/
-abbrev EMatchTheorems := PHashMap Name (List EMatchTheorem)
+/-- Set of E-matching theorems. -/
+structure EMatchTheorems where
+  /-- The key is a symbol from `EMatchTheorem.symbols`. -/
+  private map : PHashMap Name (List EMatchTheorem) := {}
+  /-- Set of theorem names that have been inserted using `insert`. -/
+  private thmNames : PHashSet Name := {}
+  deriving Inhabited
 
+/--
+Inserts a `thm` with symbols `[s_1, ..., s_n]` to `s`.
+We add `s_1 -> { thm with symbols := [s_2, ..., s_n] }`.
+When `grind` internalizes a term containing symbol `s`, we
+process all theorems `thm` associated with key `s`.
+If their `thm.symbols` is empty, we say they are activated.
+Otherwise, we reinsert into `map`.
+-/
 def EMatchTheorems.insert (s : EMatchTheorems) (thm : EMatchTheorem) : EMatchTheorems := Id.run do
   let .const declName :: syms := thm.symbols
     | unreachable!
   let thm := { thm with symbols := syms }
-  if let some thms := s.find? declName then
-    return PersistentHashMap.insert s declName (thm::thms)
+  let { map, thmNames } := s
+  let thmNames := thmNames.insert thm.origin.key
+  if let some thms := map.find? declName then
+    return { map := map.insert declName (thm::thms), thmNames }
   else
-    return PersistentHashMap.insert s declName [thm]
+    return { map := map.insert declName [thm], thmNames }
+
+/--
+Retrieves theorems from `s` associated with the given symbol. See `EMatchTheorem.insert`.
+The theorems are removed from `s`.
+-/
+@[inline]
+def EMatchTheorems.retrieve? (s : EMatchTheorems) (sym : Name) : Option (List EMatchTheorem × EMatchTheorems) :=
+  if let some thms := s.map.find? sym then
+    some (thms, { s with map := s.map.erase sym })
+  else
+    none
+
+/-- Returns `true` if `declName` is the name of a theorem that was inserted using `insert`. -/
+def EMatchTheorems.containsTheoremName (s : EMatchTheorems) (declName : Name) : Bool :=
+  s.thmNames.contains declName
 
 def EMatchTheorem.getProofWithFreshMVarLevels (thm : EMatchTheorem) : MetaM Expr := do
   if thm.proof.isConst && thm.levelParams.isEmpty then
@@ -85,7 +115,7 @@ def EMatchTheorem.getProofWithFreshMVarLevels (thm : EMatchTheorem) : MetaM Expr
 private builtin_initialize ematchTheoremsExt : SimpleScopedEnvExtension EMatchTheorem EMatchTheorems ←
   registerSimpleScopedEnvExtension {
     addEntry := EMatchTheorems.insert
-    initial  := .empty
+    initial  := {}
   }
 
 -- TODO: create attribute?
@@ -320,8 +350,8 @@ private def checkCoverage (thmProof : Expr) (numParams : Nat) (bvarsFound : Std.
 Given a theorem with proof `proof` and `numParams` parameters, returns a message
 containing the parameters at positions `paramPos`.
 -/
-private def ppParamsAt (proof : Expr) (numParms : Nat) (paramPos : List Nat) : MetaM MessageData := do
-  forallBoundedTelescope (← inferType proof) numParms fun xs _ => do
+private def ppParamsAt (proof : Expr) (numParams : Nat) (paramPos : List Nat) : MetaM MessageData := do
+  forallBoundedTelescope (← inferType proof) numParams fun xs _ => do
     let mut msg := m!""
     let mut first := true
     for h : i in [:xs.size] do
@@ -331,23 +361,53 @@ private def ppParamsAt (proof : Expr) (numParms : Nat) (paramPos : List Nat) : M
         msg := msg ++ m!"{x} : {← inferType x}"
     addMessageContextFull msg
 
-def addEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) : MetaM Unit := do
+/--
+Creates an E-matching theorem for `declName` with `numParams` parameters, and the given set of patterns.
+Pattern variables are represented using de Bruijn indices.
+-/
+def mkEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) : MetaM EMatchTheorem := do
   let .thmInfo info ← getConstInfo declName
     | throwError "`{declName}` is not a theorem, you cannot assign patterns to non-theorems for the `grind` tactic"
   let us := info.levelParams.map mkLevelParam
   let proof := mkConst declName us
   let (patterns, symbols, bvarFound) ← NormalizePattern.main patterns
   assert! symbols.all fun s => s matches .const _
-  trace[grind.ematch.pattern] "{declName}: {patterns.map ppPattern}"
+  trace[grind.ematch.pattern] "{MessageData.ofConst proof}: {patterns.map ppPattern}"
   if let .missing pos ← checkCoverage proof numParams bvarFound then
      let pats : MessageData := m!"{patterns.map ppPattern}"
      throwError "invalid pattern(s) for `{declName}`{indentD pats}\nthe following theorem parameters cannot be instantiated:{indentD (← ppParamsAt proof numParams pos)}"
-  ematchTheoremsExt.add {
-     proof, patterns, numParams, symbols
-     levelParams := #[]
-     origin      := .decl declName
+  return {
+    proof, patterns, numParams, symbols
+    levelParams := #[]
+    origin      := .decl declName
   }
 
+/--
+Given theorem with name `declName` and type of the form `∀ (a_1 ... a_n), lhs = rhs`,
+creates an E-matching pattern for it using `addEMatchTheorem n [lhs]`
+-/
+def mkEMatchEqTheorem (declName : Name) : MetaM EMatchTheorem := do
+  let info ← getConstInfo declName
+  let (numParams, patterns) ← forallTelescopeReducing info.type fun xs type => do
+    let_expr Eq _ lhs _ := type | throwError "invalid E-matching equality theorem, conclusion must be an equality{indentExpr type}"
+    return (xs.size, [lhs.abstract xs])
+  mkEMatchTheorem declName numParams patterns
+
+/--
+Adds an E-matching theorem to the environment.
+See `mkEMatchTheorem`.
+-/
+def addEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) : MetaM Unit := do
+  ematchTheoremsExt.add (← mkEMatchTheorem declName numParams patterns)
+
+/--
+Adds an E-matching equality theorem to the environment.
+See `mkEMatchEqTheorem`.
+-/
+def addEMatchEqTheorem (declName : Name) : MetaM Unit := do
+  ematchTheoremsExt.add (← mkEMatchEqTheorem declName)
+
+/-- Returns the E-matching theorems registered in the environment. -/
 def getEMatchTheorems : CoreM EMatchTheorems :=
   return ematchTheoremsExt.getState (← getEnv)
 

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

@@ -6,6 +6,8 @@ Authors: Leonardo de Moura
 prelude
 import Init.Grind.Util
 import Lean.Meta.LitValues
+import Lean.Meta.Match.MatcherInfo
+import Lean.Meta.Match.MatchEqsExt
 import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Util
 
@@ -50,21 +52,36 @@ private partial def internalizePattern (pattern : Expr) (generation : Nat) : Goa
   else pattern.withApp fun f args => do
     return mkAppN f (← args.mapM (internalizePattern · generation))
 
+private partial def activateTheorem (thm : EMatchTheorem) (generation : Nat) : GoalM Unit := do
+  -- Recall that we use the proof as part of the key for a set of instances found so far.
+  -- We don't want to use structural equality when comparing keys.
+  let proof ← shareCommon thm.proof
+  let thm := { thm with proof, patterns := (← thm.patterns.mapM (internalizePattern · generation)) }
+  trace[grind.ematch] "activated `{thm.origin.key}`, {thm.patterns.map ppPattern}"
+  modify fun s => { s with newThms := s.newThms.push thm }
+
+/--
+If `Config.matchEqs` is set to `true`, and `f` is `match`-auxiliary function,
+adds its equations to `newThms`.
+-/
+private partial def addMatchEqns (f : Expr) (generation : Nat) : GoalM Unit := do
+  if !(← getConfig).matchEqs then return ()
+  let .const declName _ := f | return ()
+  if !(← isMatcher declName) then return ()
+  if (← get).matchEqNames.contains declName then return ()
+  modify fun s => { s with matchEqNames := s.matchEqNames.insert declName }
+  for eqn in (← Match.getEquationsFor declName).eqnNames do
+    activateTheorem (← mkEMatchEqTheorem eqn) generation
+
 private partial def activateTheoremPatterns (fName : Name) (generation : Nat) : GoalM Unit := do
-  if let some thms := (← get).thmMap.find? fName then
-    modify fun s => { s with thmMap := s.thmMap.erase fName }
+  if let some (thms, thmMap) := (← get).thmMap.retrieve? fName then
+    modify fun s => { s with thmMap }
     let appMap := (← get).appMap
     for thm in thms do
       let symbols := thm.symbols.filter fun sym => !appMap.contains sym
       let thm := { thm with symbols }
       match symbols with
-      | [] =>
-        -- Recall that we use the proof as part of the key for a set of instances found so far.
-        -- We don't want to use structural equality when comparing keys.
-        let proof ← shareCommon thm.proof
-        let thm := { thm with proof, patterns := (← thm.patterns.mapM (internalizePattern · generation)) }
-        trace[grind.ematch] "activated `{thm.origin.key}`, {thm.patterns.map ppPattern}"
-        modify fun s => { s with newThms := s.newThms.push thm }
+      | [] => activateTheorem thm generation
       | _ =>
         trace[grind.ematch] "reinsert `{thm.origin.key}`"
         modify fun s => { s with thmMap := s.thmMap.insert thm }
@@ -95,6 +112,7 @@ partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do
       -- We do not want to internalize the components of a literal value.
       mkENode e generation
     else e.withApp fun f args => do
+      addMatchEqns f generation
       if f.isConstOf ``Lean.Grind.nestedProof && args.size == 2 then
         -- We only internalize the proposition. We can skip the proof because of
         -- proof irrelevance

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

@@ -14,6 +14,7 @@ import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.Inv
 import Lean.Meta.Tactic.Grind.Intro
 import Lean.Meta.Tactic.Grind.EMatch
+import Lean.Meta.Tactic.Grind.DoNotSimp
 
 namespace Lean.Meta.Grind
 
@@ -38,7 +39,7 @@ def GrindM.run (x : GrindM α) (mainDeclName : Name) (config : Grind.Config) (fa
   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 simprocs := #[(← addDoNotSimp (← grindNormSimprocExt.getSimprocs))]
   let simp ← Simp.mkContext
     (config := { arith := true })
     (simpTheorems := #[thms])

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

@@ -9,6 +9,7 @@ import Lean.Meta.Tactic.Assert
 import Lean.Meta.Tactic.Simp.Main
 import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.DoNotSimp
 import Lean.Meta.Tactic.Grind.MarkNestedProofs
 
 namespace Lean.Meta.Grind
@@ -33,6 +34,7 @@ def simp (e : Expr) : GrindM Simp.Result := do
   let e' ← eraseIrrelevantMData e'
   let e' ← foldProjs e'
   let e' ← normalizeLevels e'
+  let e' ← eraseDoNotSimp e'
   let e' ← canon e'
   let e' ← shareCommon e'
   trace[grind.simp] "{e}\n===>\n{e'}"

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

@@ -379,6 +379,8 @@ structure Goal where
   preInstances : PreInstanceSet := {}
   /-- new facts to be processed. -/
   newFacts     : Std.Queue NewFact := ∅
+  /-- `match` auxiliary functions whose equations have already been created and activated. -/
+  matchEqNames : PHashSet Name := {}
   deriving Inhabited
 
 def Goal.admit (goal : Goal) : MetaM Unit :=

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich, Leonardo de Moura, Gabriel Ebner, Mario Carneiro
 -/
 prelude
-import Lean.Parser
 import Lean.PrettyPrinter.Delaborator.Attributes
 import Lean.PrettyPrinter.Delaborator.Basic
 import Lean.PrettyPrinter.Delaborator.SubExpr

src/Lean/Server/Completion.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Marc Huisinga
 -/
 prelude
 import Lean.Server.Completion.CompletionCollectors
+import Std.Data.HashMap
 
 namespace Lean.Server.Completion
 open Lsp

src/Lean/Util/ShareCommon.lean

@@ -5,8 +5,8 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.ShareCommon
-import Std.Data.HashSet
-import Std.Data.HashMap
+import Std.Data.HashSet.Basic
+import Std.Data.HashMap.Basic
 import Lean.Data.PersistentHashMap
 import Lean.Data.PersistentHashSet
 

src/Std/Sat/AIG/Basic.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 prelude
-import Std.Data.HashMap
 import Std.Data.HashSet
 
 namespace Std

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Josh Clune
 -/
 prelude
-import Init.Data.Array
 import Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
 import Std.Tactic.BVDecide.LRAT.Internal.Assignment
 import Std.Sat.CNF.Basic

src/Std/Time/DateTime/Timestamp.lean

@@ -5,7 +5,6 @@ Authors: Sofia Rodrigues
 -/
 prelude
 import Std.Time.Internal
-import Init.Data.Int
 import Init.System.IO
 import Std.Time.Time
 import Std.Time.Date

src/Std/Time/Internal/Bounded.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sofia Rodrigues
 -/
 prelude
-import Init.Data.Int
+import Init.Omega
 
 namespace Std
 namespace Time

tests/lean/run/grind_match1.lean

@@ -0,0 +1,56 @@
+def g (xs : List α) (ys : List α) :=
+  match xs, ys with
+  | [], _         => ys
+  | _::_::_, [ ]  => []
+  | x::xs,   ys   => x :: g xs ys
+
+attribute [simp] g
+
+set_option trace.grind.assert true
+
+/--
+info: [grind.assert] (match as, bs with
+      | [], x => bs
+      | head :: head_1 :: tail, [] => []
+      | x :: xs, ys => x :: g xs ys) =
+      d
+[grind.assert] bs = []
+[grind.assert] a₁ :: f 0 = as
+[grind.assert] f 0 = a₂ :: f 1
+[grind.assert] ¬d = []
+[grind.assert] (match a₁ :: a₂ :: f 1, [] with
+      | [], x => bs
+      | head :: head_1 :: tail, [] => []
+      | x :: xs, ys => x :: g xs ys) =
+      []
+-/
+#guard_msgs (info) in
+example (f : Nat → List Nat) : g as bs = d → bs = [] → a₁ :: f 0 = as → f 0 = a₂ :: f 1 → d = [] := by
+  unfold g
+  grind
+
+
+example : g as bs = d → as = [] → d = bs := by
+  unfold g
+  grind
+
+def f (x : List α) : Bool :=
+  match x with
+  | [] => true
+  | _::_ => false
+
+example : f a = b → a = [] → b = true := by
+  unfold f
+  grind
+
+def f' (x : List Nat) : Bool :=
+  match x with
+  | [] => true
+  | _::_ => false
+
+attribute [simp] f'
+#check f'.match_1.eq_1
+
+example : f' a = b → a = [] → b = true := by
+  unfold f'
+  grind