Merge remote-tracking branch 'origin/master' into getElem_simps

Author: kim-em

.github/workflows/awaiting-mathlib.yml

@@ -10,11 +10,29 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Check awaiting-mathlib label
+        id: check-awaiting-mathlib-label
         if: github.event_name == 'pull_request'
         uses: actions/github-script@v7
         with:
           script: |
-            const { labels } = context.payload.pull_request;
-            if (labels.some(label => label.name == "awaiting-mathlib") && !labels.some(label => label.name == "builds-mathlib")) {
-              core.setFailed('PR is marked "awaiting-mathlib" but "builds-mathlib" label has not been applied yet by the bot');
+            const { labels, number: prNumber } = context.payload.pull_request;
+            const hasAwaiting = labels.some(label => label.name == "awaiting-mathlib");
+            const hasBreaks = labels.some(label => label.name == "breaks-mathlib");
+            const hasBuilds = labels.some(label => label.name == "builds-mathlib");
+
+            if (hasAwaiting && hasBreaks) {
+              core.setFailed('PR has both "awaiting-mathlib" and "breaks-mathlib" labels.');
+            } else if (hasAwaiting && !hasBreaks && !hasBuilds) {
+              core.info('PR is marked "awaiting-mathlib" but neither "breaks-mathlib" nor "builds-mathlib" labels are present.');
+              core.setOutput('awaiting', 'true');
             }
+      
+      - name: Wait for mathlib compatibility
+        if: github.event_name == 'pull_request' && steps.check-awaiting-mathlib-label.outputs.awaiting == 'true'
+        run: |
+          echo "::notice title=Awaiting mathlib::PR is marked 'awaiting-mathlib' but neither 'breaks-mathlib' nor 'builds-mathlib' labels are present."
+          echo "This check will remain in progress until the PR is updated with appropriate mathlib compatibility labels."
+          # Keep the job running indefinitely to show "in progress" status
+          while true; do
+            sleep 3600  # Sleep for 1 hour at a time
+          done

src/Init/Data/List/Pairwise.lean

@@ -24,7 +24,7 @@ open Nat
 
 /-! ### Pairwise -/
 
-theorem Pairwise.sublist : l₁ <+ l₂ → l₂.Pairwise R → l₁.Pairwise R
+@[grind →] theorem Pairwise.sublist : l₁ <+ l₂ → l₂.Pairwise R → l₁.Pairwise R
   | .slnil, h => h
   | .cons _ s, .cons _ h₂ => h₂.sublist s
   | .cons₂ _ s, .cons h₁ h₂ => (h₂.sublist s).cons fun _ h => h₁ _ (s.subset h)
@@ -37,11 +37,11 @@ theorem Pairwise.imp {α R S} (H : ∀ {a b}, R a b → S a b) :
 theorem rel_of_pairwise_cons (p : (a :: l).Pairwise R) : ∀ {a'}, a' ∈ l → R a a' :=
   (pairwise_cons.1 p).1 _
 
-theorem Pairwise.of_cons (p : (a :: l).Pairwise R) : Pairwise R l :=
+@[grind →] theorem Pairwise.of_cons (p : (a :: l).Pairwise R) : Pairwise R l :=
   (pairwise_cons.1 p).2
 
 set_option linter.unusedVariables false in
-theorem Pairwise.tail : ∀ {l : List α} (h : Pairwise R l), Pairwise R l.tail
+@[grind] theorem Pairwise.tail : ∀ {l : List α} (h : Pairwise R l), Pairwise R l.tail
   | [], h => h
   | _ :: _, h => h.of_cons
 
@@ -101,11 +101,11 @@ theorem Pairwise.forall_of_forall_of_flip (h₁ : ∀ x ∈ l, R x x) (h₂ : Pa
     · exact h₃.1 _ hx
     · exact ih (fun x hx => h₁ _ <| mem_cons_of_mem _ hx) h₂.2 h₃.2 hx hy
 
-theorem pairwise_singleton (R) (a : α) : Pairwise R [a] := by simp
+@[grind] theorem pairwise_singleton (R) (a : α) : Pairwise R [a] := by simp
 
-theorem pairwise_pair {a b : α} : Pairwise R [a, b] ↔ R a b := by simp
+@[grind =] theorem pairwise_pair {a b : α} : Pairwise R [a, b] ↔ R a b := by simp
 
-theorem pairwise_map {l : List α} :
+@[grind =] theorem pairwise_map {l : List α} :
     (l.map f).Pairwise R ↔ l.Pairwise fun a b => R (f a) (f b) := by
   induction l
   · simp
@@ -115,11 +115,11 @@ theorem Pairwise.of_map {S : β → β → Prop} (f : α → β) (H : ∀ a b :
     (p : Pairwise S (map f l)) : Pairwise R l :=
   (pairwise_map.1 p).imp (H _ _)
 
-theorem Pairwise.map {S : β → β → Prop} (f : α → β) (H : ∀ a b : α, R a b → S (f a) (f b))
+@[grind] theorem Pairwise.map {S : β → β → Prop} (f : α → β) (H : ∀ a b : α, R a b → S (f a) (f b))
     (p : Pairwise R l) : Pairwise S (map f l) :=
   pairwise_map.2 <| p.imp (H _ _)
 
-theorem pairwise_filterMap {f : β → Option α} {l : List β} :
+@[grind =] theorem pairwise_filterMap {f : β → Option α} {l : List β} :
     Pairwise R (filterMap f l) ↔ Pairwise (fun a a' : β => ∀ b, f a = some b → ∀ b', f a' = some b' → R b b') l := by
   let _S (a a' : β) := ∀ b, f a = some b → ∀ b', f a' = some b' → R b b'
   induction l with
@@ -134,20 +134,20 @@ theorem pairwise_filterMap {f : β → Option α} {l : List β} :
     simpa [IH, e] using fun _ =>
       ⟨fun h a ha b hab => h _ _ ha hab, fun h a b ha hab => h _ ha _ hab⟩
 
-theorem Pairwise.filterMap {S : β → β → Prop} (f : α → Option β)
+@[grind] theorem Pairwise.filterMap {S : β → β → Prop} (f : α → Option β)
     (H : ∀ a a' : α, R a a' → ∀ b, f a = some b → ∀ b', f a' = some b' → S b b') {l : List α} (p : Pairwise R l) :
     Pairwise S (filterMap f l) :=
   pairwise_filterMap.2 <| p.imp (H _ _)
 
-theorem pairwise_filter {p : α → Prop} [DecidablePred p] {l : List α} :
+@[grind =] theorem pairwise_filter {p : α → Bool} {l : List α} :
     Pairwise R (filter p l) ↔ Pairwise (fun x y => p x → p y → R x y) l := by
   rw [← filterMap_eq_filter, pairwise_filterMap]
   simp
 
-theorem Pairwise.filter (p : α → Bool) : Pairwise R l → Pairwise R (filter p l) :=
+@[grind] theorem Pairwise.filter (p : α → Bool) : Pairwise R l → Pairwise R (filter p l) :=
   Pairwise.sublist filter_sublist
 
-theorem pairwise_append {l₁ l₂ : List α} :
+@[grind =] theorem pairwise_append {l₁ l₂ : List α} :
     (l₁ ++ l₂).Pairwise R ↔ l₁.Pairwise R ∧ l₂.Pairwise R ∧ ∀ a ∈ l₁, ∀ b ∈ l₂, R a b := by
   induction l₁ <;> simp [*, or_imp, forall_and, and_assoc, and_left_comm]
 
@@ -157,13 +157,13 @@ theorem pairwise_append_comm {R : α → α → Prop} (s : ∀ {x y}, R x y →
     (x : α) (xm : x ∈ l₂) (y : α) (ym : y ∈ l₁) : R x y := s (H y ym x xm)
   simp only [pairwise_append, and_left_comm]; rw [Iff.intro (this l₁ l₂) (this l₂ l₁)]
 
-theorem pairwise_middle {R : α → α → Prop} (s : ∀ {x y}, R x y → R y x) {a : α} {l₁ l₂ : List α} :
+@[grind =] theorem pairwise_middle {R : α → α → Prop} (s : ∀ {x y}, R x y → R y x) {a : α} {l₁ l₂ : List α} :
     Pairwise R (l₁ ++ a :: l₂) ↔ Pairwise R (a :: (l₁ ++ l₂)) := by
   show Pairwise R (l₁ ++ ([a] ++ l₂)) ↔ Pairwise R ([a] ++ l₁ ++ l₂)
   rw [← append_assoc, pairwise_append, @pairwise_append _ _ ([a] ++ l₁), pairwise_append_comm s]
   simp only [mem_append, or_comm]
 
-theorem pairwise_flatten {L : List (List α)} :
+@[grind =] theorem pairwise_flatten {L : List (List α)} :
     Pairwise R (flatten L) ↔
       (∀ l ∈ L, Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ x ∈ l₁, ∀ y ∈ l₂, R x y) L := by
   induction L with
@@ -174,16 +174,16 @@ theorem pairwise_flatten {L : List (List α)} :
     rw [and_comm, and_congr_left_iff]
     intros; exact ⟨fun h l' b c d e => h c d e l' b, fun h c d e l' b => h l' b c d e⟩
 
-theorem pairwise_flatMap {R : β → β → Prop} {l : List α} {f : α → List β} :
+@[grind =] theorem pairwise_flatMap {R : β → β → Prop} {l : List α} {f : α → List β} :
     List.Pairwise R (l.flatMap f) ↔
       (∀ a ∈ l, Pairwise R (f a)) ∧ Pairwise (fun a₁ a₂ => ∀ x ∈ f a₁, ∀ y ∈ f a₂, R x y) l := by
   simp [List.flatMap, pairwise_flatten, pairwise_map]
 
-theorem pairwise_reverse {l : List α} :
+@[grind =] theorem pairwise_reverse {l : List α} :
     l.reverse.Pairwise R ↔ l.Pairwise (fun a b => R b a) := by
   induction l <;> simp [*, pairwise_append, and_comm]
 
-@[simp] theorem pairwise_replicate {n : Nat} {a : α} :
+@[simp, grind =] theorem pairwise_replicate {n : Nat} {a : α} :
     (replicate n a).Pairwise R ↔ n ≤ 1 ∨ R a a := by
   induction n with
   | zero => simp
@@ -205,10 +205,10 @@ theorem pairwise_reverse {l : List α} :
         simp
       · exact ⟨fun _ => h, Or.inr h⟩
 
-theorem Pairwise.drop {l : List α} {i : Nat} (h : List.Pairwise R l) : List.Pairwise R (l.drop i) :=
+@[grind] theorem Pairwise.drop {l : List α} {i : Nat} (h : List.Pairwise R l) : List.Pairwise R (l.drop i) :=
   h.sublist (drop_sublist _ _)
 
-theorem Pairwise.take {l : List α} {i : Nat} (h : List.Pairwise R l) : List.Pairwise R (l.take i) :=
+@[grind] theorem Pairwise.take {l : List α} {i : Nat} (h : List.Pairwise R l) : List.Pairwise R (l.take i) :=
   h.sublist (take_sublist _ _)
 
 theorem pairwise_iff_forall_sublist : l.Pairwise R ↔ (∀ {a b}, [a,b] <+ l → R a b) := by
@@ -247,7 +247,7 @@ theorem pairwise_of_forall_mem_list {l : List α} {r : α → α → Prop} (h :
   intro a b hab
   apply h <;> (apply hab.subset; simp)
 
-theorem pairwise_pmap {p : β → Prop} {f : ∀ b, p b → α} {l : List β} (h : ∀ x ∈ l, p x) :
+@[grind =] theorem pairwise_pmap {p : β → Prop} {f : ∀ b, p b → α} {l : List β} (h : ∀ x ∈ l, p x) :
     Pairwise R (l.pmap f h) ↔
       Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l := by
   induction l with
@@ -259,7 +259,7 @@ theorem pairwise_pmap {p : β → Prop} {f : ∀ b, p b → α} {l : List β} (h
     rintro H _ b hb rfl
     exact H b hb _ _
 
-theorem Pairwise.pmap {l : List α} (hl : Pairwise R l) {p : α → Prop} {f : ∀ a, p a → β}
+@[grind] theorem Pairwise.pmap {l : List α} (hl : Pairwise R l) {p : α → Prop} {f : ∀ a, p a → β}
     (h : ∀ x ∈ l, p x) {S : β → β → Prop}
     (hS : ∀ ⦃x⦄ (hx : p x) ⦃y⦄ (hy : p y), R x y → S (f x hx) (f y hy)) :
     Pairwise S (l.pmap f h) := by
@@ -268,15 +268,15 @@ theorem Pairwise.pmap {l : List α} (hl : Pairwise R l) {p : α → Prop} {f : 
 
 /-! ### Nodup -/
 
-@[simp]
+@[simp, grind]
 theorem nodup_nil : @Nodup α [] :=
   Pairwise.nil
 
-@[simp]
+@[simp, grind =]
 theorem nodup_cons {a : α} {l : List α} : Nodup (a :: l) ↔ a ∉ l ∧ Nodup l := by
   simp only [Nodup, pairwise_cons, forall_mem_ne]
 
-theorem Nodup.sublist : l₁ <+ l₂ → Nodup l₂ → Nodup l₁ :=
+@[grind →] theorem Nodup.sublist : l₁ <+ l₂ → Nodup l₂ → Nodup l₁ :=
   Pairwise.sublist
 
 theorem Sublist.nodup : l₁ <+ l₂ → Nodup l₂ → Nodup l₁ :=
@@ -303,7 +303,7 @@ theorem getElem?_inj {xs : List α}
       rw [mem_iff_getElem?]
     exact ⟨_, h₂⟩; exact ⟨_ , h₂.symm⟩
 
-@[simp] theorem nodup_replicate {n : Nat} {a : α} :
+@[simp, grind =] theorem nodup_replicate {n : Nat} {a : α} :
     (replicate n a).Nodup ↔ n ≤ 1 := by simp [Nodup]
 
 end List

src/Lean/Compiler/LCNF/PhaseExt.lean

@@ -13,25 +13,37 @@ abbrev DeclExtState := PHashMap Name Decl
 private abbrev declLt (a b : Decl) :=
   Name.quickLt a.name b.name
 
-private abbrev sortDecls (decls : Array Decl) : Array Decl :=
+private def sortedDecls (s : DeclExtState) : Array Decl :=
+  let decls := s.foldl (init := #[]) fun ps _ v => ps.push v
   decls.qsort declLt
 
 private abbrev findAtSorted? (decls : Array Decl) (declName : Name) : Option Decl :=
   let tmpDecl : Decl := default
   let tmpDecl := { tmpDecl with name := declName }
   decls.binSearch tmpDecl declLt
 
-abbrev DeclExt := SimplePersistentEnvExtension Decl DeclExtState
-
-def mkDeclExt (name : Name := by exact decl_name%) : IO DeclExt := do
-  registerSimplePersistentEnvExtension {
-    name            := name
-    addImportedFn   := fun _ => {}
-    addEntryFn      := fun decls decl => decls.insert decl.name decl
-    toArrayFn       := (sortDecls ·.toArray)
-    asyncMode       := .sync  -- compilation is non-parallel anyway
-    replay?         := some <| SimplePersistentEnvExtension.replayOfFilter
-      (fun s d => !s.contains d.name) (fun decls decl => decls.insert decl.name decl)
+def DeclExt := PersistentEnvExtension Decl Decl DeclExtState
+
+instance : Inhabited DeclExt :=
+  inferInstanceAs (Inhabited (PersistentEnvExtension Decl Decl DeclExtState))
+
+def mkDeclExt (name : Name := by exact decl_name%) : IO DeclExt :=
+  registerPersistentEnvExtension {
+    name,
+    mkInitial := pure {},
+    addImportedFn := fun _ => pure {},
+    addEntryFn := fun s decl => s.insert decl.name decl
+    exportEntriesFn := sortedDecls
+    statsFn := fun s =>
+      let numEntries := s.foldl (init := 0) (fun count _ _ => count + 1)
+      format "number of local entries: " ++ format numEntries
+    asyncMode := .sync,
+    replay? := some <| fun oldState newState _ otherState =>
+      newState.foldl (init := otherState) fun otherState k v =>
+        if oldState.contains k then
+          otherState
+        else
+          otherState.insert k v
   }
 
 builtin_initialize baseExt : DeclExt ← mkDeclExt

src/Lean/Environment.lean

@@ -454,6 +454,9 @@ private partial def AsyncConsts.findRec? (aconsts : AsyncConsts) (declName : Nam
   let c ← aconsts.findPrefix? declName
   if c.constInfo.name == declName then
     return c
+  -- If privacy is the only difference between `declName` and `findPrefix?` result, we can assume
+  -- `declName` does not exist according to the `add` invariant
+  guard <| privateToUserName c.constInfo.name != privateToUserName declName
   let aconsts ← c.consts.get.get? AsyncConsts
   AsyncConsts.findRec? aconsts declName
 

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

@@ -0,0 +1,112 @@
+/-
+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 Lean.Meta.Tactic.Grind.ENodeKey
+
+namespace Lean.Meta.Grind
+
+private def hashChild (e : Expr) : UInt64 :=
+  match e with
+  | .bvar .. | .mvar .. | .const .. | .fvar .. | .sort .. | .lit .. =>
+    hash e
+  | .app .. | .letE .. | .forallE .. | .lam .. | .mdata .. | .proj .. =>
+    (unsafe ptrAddrUnsafe e).toUInt64
+
+private def alphaHash (e : Expr) : UInt64 :=
+  match e with
+  | .bvar .. | .mvar .. | .const .. | .fvar .. | .sort .. | .lit .. =>
+    hash e
+  | .app f a => mixHash (hashChild f) (hashChild a)
+  | .letE _ _ v b _ => mixHash (hashChild v) (hashChild b)
+  | .forallE _ d b _ | .lam _ d b _ => mixHash (hashChild d) (hashChild b)
+  | .mdata _ b => mixHash 13 (hashChild b)
+  | .proj n i b => mixHash (mixHash (hash n) (hash i)) (hashChild b)
+
+private def alphaEq (e₁ e₂ : Expr) : Bool := Id.run do
+  match e₁ with
+  | .bvar .. | .mvar .. | .const .. | .fvar .. | .sort .. | .lit .. =>
+    e₁ == e₂
+  | .app f₁ a₁ =>
+    let .app f₂ a₂ := e₂ | false
+    isSameExpr f₁ f₂ && isSameExpr a₁ a₂
+  | .letE _ _ v₁ b₁ _ =>
+    let .letE _ _ v₂ b₂ _ := e₂ | false
+    isSameExpr v₁ v₂ && isSameExpr b₁ b₂
+  | .forallE _ d₁ b₁ _ =>
+    let .forallE _ d₂ b₂ _ := e₂ | false
+    isSameExpr d₁ d₂ && isSameExpr b₁ b₂
+  | .lam _ d₁ b₁ _ =>
+    let .lam _ d₂ b₂ _ := e₂ | false
+    isSameExpr d₁ d₂ && isSameExpr b₁ b₂
+  | .mdata d₁ b₁ =>
+    let .mdata d₂ b₂ := e₂ | false
+    return isSameExpr b₁ b₂ && d₁ == d₂
+  | .proj n₁ i₁ b₁ =>
+    let .proj n₂ i₂ b₂ := e₂ | false
+    n₁ == n₂ && i₁ == i₂ && isSameExpr b₁ b₂
+
+structure AlphaKey where
+  expr : Expr
+
+instance : Hashable AlphaKey where
+  hash k := alphaHash k.expr
+
+instance : BEq AlphaKey where
+  beq k₁ k₂ := alphaEq k₁.expr k₂.expr
+
+structure AlphaShareCommon.State where
+  map : PHashMap ENodeKey Expr := {}
+  set : PHashSet AlphaKey := {}
+
+abbrev AlphaShareCommonM := StateM AlphaShareCommon.State
+
+private def save (e : Expr) (r : Expr) : AlphaShareCommonM Expr := do
+  if let some r := (← get).set.find? { expr := r } then
+    let r := r.expr
+    modify fun { set, map } => {
+      set
+      map := map.insert { expr := e } r
+    }
+    return r
+  else
+    modify fun { set, map } => {
+      set := set.insert { expr := r }
+      map := map.insert { expr := e } r |>.insert { expr := r } r
+    }
+    return r
+
+private abbrev visit (e : Expr) (k : AlphaShareCommonM Expr) : AlphaShareCommonM Expr := do
+  if let some r := (← get).map.find? { expr := e } then
+    return r
+  else
+    save e (← k)
+
+/-- Similar to `shareCommon`, but handles alpha-equivalence. -/
+def shareCommonAlpha (e : Expr) : AlphaShareCommonM Expr :=
+  go e
+where
+  go (e : Expr) : AlphaShareCommonM Expr := do
+    match e with
+    | .bvar .. | .mvar .. | .const .. | .fvar .. | .sort .. | .lit .. =>
+      if let some r := (← get).set.find? { expr := e } then
+        return r.expr
+      else
+        modify fun { set, map } => { set := set.insert { expr := e }, map }
+        return e
+    | .app f a =>
+      visit e (return mkApp (← go f) (← go a))
+    | .letE n t v b nd =>
+      visit e (return mkLet n t (← go v) (← go b) nd)
+    | .forallE n d b bi =>
+      visit e (return mkForall n bi (← go d) (← go b))
+    | .lam n d b bi =>
+      visit e (return mkLambda n bi (← go d) (← go b))
+    | .mdata d b =>
+      visit e (return mkMData d (← go b))
+    | .proj n i b =>
+      visit e (return mkProj n i (← go b))
+
+end Lean.Meta.Grind