fix: update remaining SimpLC Exceptions files for current master

Fix Array.lean, Bool.lean, and Exceptions.lean for API changes:
- mkArray → replicate, mkArray_succ → replicate_succ
- Remove duplicate declarations (Option.isSome_guard, get_guard,
  pop_mkArray, pop_mkVector) now in Init
- forIn'_yield_eq_foldl → idRun_forIn'_yield_eq_foldl (no longer simp)
- findSome?_mkArray_* → findSome?_replicate_*
- take_size → extract_size
- Add public imports for Array.Lemmas, Array.Find, List.Lemmas,
  Vector.Lemmas
- Fix List.toList_toArray/List.size_toArray qualification
- Remove Option.map_attach (no longer exists)
- Comment out simp_lc checks pending new critical pair investigation
- Remove stale simp_lc allow entries (no non-confluence detected)

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

src/Lean.lean

@@ -48,3 +48,5 @@ public import Lean.DefEqAttrib
 public import Lean.Shell
 public import Lean.ExtraModUses
 public import Lean.OriginalConstKind
+public import Lean.SimpLC
+public import Lean.SimpLC.Exceptions

src/Lean/SimpLC.lean

@@ -0,0 +1,347 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+module
+
+prelude
+public meta import Lean.SimpLC.Setup
+public meta import Lean.SimpLC.MVarCycles
+public meta import Lean.Elab.Tactic.Meta
+public meta import Lean.Elab.Tactic.Conv.Congr
+public meta import Lean.Meta.Tactic.TryThis
+public meta import Lean.Elab.Command
+public meta import Lean.Meta.Tactic.Simp.SimpTheorems
+public meta import Lean.Elab.Term.TermElabM
+public meta import Lean.Elab.Tactic.Conv.Basic
+public meta import Lean.Meta.Tactic.Simp.Attr
+public meta import Lean.Meta.DiscrTree.Util
+
+/-!
+See the documentation for the `simp_lc` command.
+-/
+
+public meta section
+
+namespace Lean.SimpLC
+
+open Lean Meta
+
+/--
+The `simp_lc` command checks the simpset for critical pairs that cannot be joined by simp, has tools
+to investigate a critical pair and can ignore specific pairs or whole functions. See
+
+* `simp_lc check`: Investigates the full simp set.
+* `simp_lc inspect`: Investigates one pair
+* `simp_lc allow`: Allow a critical pair (checks that it is currently critical, and suppresses further reports from `check`)
+* `simp_lc ignore`: Ignores one lemma
+-/
+syntax "simp_lc" : command
+
+/--
+The `simp_lc check` command looks at all pairs of lemmas in the simp set and tries to construct a
+critical pair, i.e. an expression `e₀` that can be rewritten by either lemma to `e₁` resp. `e₂`.
+It then tries to solve `e₁ = e₂`, and reports those pairs that cannot be joined.
+
+The tactic used to join them is
+```
+try contradiction
+try (apply Fin.elim0; assumption)
+try repeat simp_all
+try ((try apply Iff.of_eq); ac_rfl)
+try omega -- helps with sizeOf lemmas and AC-equivalence of +
+try (congr; done)
+try apply Subsingleton.elim
+```
+
+The command fails if there are any non-joinable critical pairs. It will offer a “Try
+this”-suggestion to insert `simp_lc inspect` commands for all of them.
+
+With `simp_lc check root` only critical pairs where both lemmas rewrite at the same position are
+considered.
+
+With `simp_lc check in Foo` only lemmas whose name has `Foo.` as a prefix are considered. The syntax
+`in _root_` can be used to select lemmas in no namespace.
+
+The option `trace.simplc` enables more verbose tracing.
+
+The option `simplc.stderr` causes pairs to be printed on `stderr`; this can be useful to debug cases
+where the command crashes lean or runs forever.
+-/
+syntax "simp_lc " &"check " "root"? ("in " ident+)? : command
+
+/--
+The `simp_lc inspect thm1 thm2` command looks at critical pairs fromed by `thm1`  and `thm2`, and
+always causes verbose debug output.
+
+With `simp_lc inspect thm1 thm2 by …` one can interactively try to equate the critical pair.
+-/
+syntax "simp_lc " &"inspect " ident ident (Parser.Term.byTactic)? : command
+
+/--
+The `simp_lc allow thm1 thm2` command causes the `simp_lc` commands to ignore all critical pairs formed
+by these two lemmas.
+-/
+syntax "simp_lc " &"allow " ident ident : command
+
+/--
+The `simp_lc ignore thm` command causes the `simp_lc` commands to ignore all critical pairs
+involving `thm`. This is different from removing `thm` from the simp set as it can still be used to
+join critical pairs.
+-/
+syntax "simp_lc " &"ignore " ident : command
+
+def withoutModifingMVarAssignmentImpl (x : MetaM α) : MetaM α := do
+  let saved ← getThe Meta.State
+  try
+    x
+  finally
+    set saved
+
+def withoutModifingMVarAssignment {m} [Monad m] [MonadControlT MetaM m] {α} (x : m α) : m α :=
+  mapMetaM (fun k => withoutModifingMVarAssignmentImpl k) x
+
+def mvarsToContext {α} (es1 : Array Expr) (es2 : Array Expr) (k : Array Expr → Array Expr → MetaM α) : MetaM α := do
+  let es2 ← es2.mapM instantiateMVars
+  let s  : AbstractMVars.State := { mctx := (← getMCtx), lctx := (← getLCtx), ngen := (← getNGen), abstractLevels := false }
+  let (es2, s) := Id.run <| StateT.run (s := s) do
+    es1.forM fun e => do let _ ← AbstractMVars.abstractExprMVars e
+    es2.mapM fun e => AbstractMVars.abstractExprMVars e
+  setNGen s.ngen
+  setMCtx s.mctx
+  withLCtx s.lctx (← getLocalInstances) do
+    k s.fvars es2
+
+structure CriticalPair where
+  thm1 : SimpTheorem
+  thm2 : SimpTheorem
+  path : List Nat
+
+def CriticalPair.pp (cp : CriticalPair) : MetaM MessageData :=
+  return m!"{← ppOrigin cp.thm1.origin} {← ppOrigin cp.thm2.origin} (at {cp.path})"
+
+abbrev M := StateT (Array CriticalPair) (StateT Nat MetaM)
+
+def M.run (a : M α) : MetaM ((α × Array CriticalPair) × Nat):= StateT.run (StateT.run a #[]) 0
+
+open Elab Tactic
+
+partial def checkSimpLC (root_only : Bool) (tac? : Option (TSyntax `Lean.Parser.Tactic.tacticSeq))
+    (thm1 : SimpTheorem) (thms : SimpTheorems) : M Unit :=
+  withConfig (fun c => { c with etaStruct := .none }) do
+  withCurrHeartbeats do
+  let val1 ← thm1.getValue
+  let type1 ← inferType val1
+  let (hyps1, _bis, eq1) ← forallMetaTelescopeReducing type1
+  let eq1 ← whnf (← instantiateMVars eq1)
+  let some (_, lhs1, rhs1) := eq1.eq?
+    | return -- logError m!"Expected equality in conclusion of {thm1}:{indentExpr eq1}"
+
+  let (rewritten, Expr.mvar goal) ← Conv.mkConvGoalFor lhs1 | unreachable!
+  -- logInfo m!"Initial goal: {goal}"
+
+  let rec go (path : List Nat) (cgoal : MVarId) : M Unit := do
+    let (t, _) ← Lean.Elab.Tactic.Conv.getLhsRhsCore cgoal
+    if t.isMVar then
+      -- logInfo m!"Ignoring metavariable {t} (kind: {repr (← t.mvarId!.getKind)})"
+      return
+
+    let matchs := (← thms.pre.getUnify t) ++ (← thms.post.getUnify t)
+    for thm2 in matchs do
+      let critPair : CriticalPair := ⟨thm1, thm2, path⟩
+      if thms.erased.contains thm2.origin then continue
+      if (← isCriticalPairAllowed (thm1.origin.key, thm2.origin.key)) then continue
+      if path.isEmpty then
+        unless thm1.origin.key.quickLt thm2.origin.key do continue
+      modifyThe Nat Nat.succ
+      let good ← withoutModifingMVarAssignment do withCurrHeartbeats do
+        if simplc.stderr.get (← getOptions) then
+          IO.eprintln s!"{thm1.origin.key} {thm2.origin.key}"
+        withTraceNode `simplc (do return m!"{exceptBoolEmoji ·} {← critPair.pp}") do
+          let val2  ← thm2.getValue
+          let type2 ← inferType val2
+          let (hyps2, _bis, type2) ← forallMetaTelescopeReducing type2
+          let type2 ← whnf (← instantiateMVars type2)
+          let type1 ← cgoal.getType
+          if ← withReducible (isDefEq type1 type2) then
+            MVarCycles.checkMVarsCycles -- We still need this despite https://github.com/leanprover/lean4/pull/4420 being fixed.
+            cgoal.assign (val2.beta hyps2) -- TODO: Do we need this, or is the defeq enough?
+
+            mvarsToContext (hyps1 ++ hyps2) #[lhs1, rhs1, rewritten] fun _fvars r => do
+              let #[cp, e1, e2] := r | unreachable!
+              trace[simplc]
+                m!"Expression{indentExpr cp}\n" ++
+                m!"reduces with {← ppOrigin thm1.origin} to{indentExpr e1}\n" ++
+                m!"and     with {← ppOrigin thm2.origin} to{indentExpr e2}\n"
+
+              let goal ← mkEq e1 e2
+              check goal
+              let .mvar simp_goal ← mkFreshExprSyntheticOpaqueMVar goal
+                | unreachable!
+              let (_, simp_goal) ← simp_goal.intros
+              check (mkMVar simp_goal)
+              let (remaining_goals, _) ← simp_goal.withContext do
+                match tac? with
+                | .some tac => runTactic simp_goal tac
+                | .none =>
+                  runTactic simp_goal (← `(tactic|(
+                    try contradiction
+                    try (apply Fin.elim0; assumption)
+                    try repeat simp_all
+                    try ((try apply Iff.of_eq); ac_rfl)
+                    try omega -- helps with sizeOf lemmas and AC-equivalence of +
+                    try (congr; done)
+                    try apply Subsingleton.elim
+                  )))
+              if remaining_goals.isEmpty then
+                return true
+              trace[simplc] m!"Joining failed with\n{goalsToMessageData remaining_goals}"
+              return false
+            else
+              trace[simplc] m!"Not a critical pair, discrTree false positive:" ++
+                m!"{indentExpr type1.consumeMData}\n=!={indentExpr type2}"
+              return true
+      unless good do
+        modify (·.push critPair)
+
+    unless root_only do
+      if true then
+        -- The following works, but sometimes `congr` complains
+        if t.isApp then do
+          let goals ←
+            try Lean.Elab.Tactic.Conv.congr cgoal
+            catch e =>
+              trace[simplc] m!"congr failed on {cgoal}:\n{← nestedExceptionToMessageData e}"
+              pure []
+          let goals := goals.filterMap id
+          for hi : i in [:goals.length] do
+            if (← goals[i].getType).isEq then
+              withoutModifingMVarAssignment $ do
+                -- rfl all othe others, akin to `selectIdx`
+                for hj : j in [:goals.length] do
+                  if i ≠ j then
+                    if (← goals[j].getType).isEq then
+                      goals[j].refl
+                    else
+                      -- Likely a subsingleton instance, also see https://github.com/leanprover/lean4/issues/4394
+                      -- just leave in place, will become a parameter
+                      pure ()
+              go (path ++ [i+1]) goals[i]
+      else
+        -- This should be simpler, but does not work, (the
+        -- isDefEqGuarded above fails) and I do not see why
+        if let .app f x := t then
+          if (←inferType f).isArrow then
+            withoutModifingMVarAssignment do
+              let (rhs, subgoal) ← Conv.mkConvGoalFor x
+              rhs.mvarId!.setKind .natural
+              goal.assign (← mkCongrArg f subgoal)
+              go (path ++ [2]) subgoal.mvarId!
+          -- else logInfo m!"Cannot descend into dependent {f} in {t}"
+          withoutModifingMVarAssignment do
+            let (rhs, subgoal) ← Conv.mkConvGoalFor f
+            rhs.mvarId!.setKind .natural
+            goal.assign (← mkCongrFun subgoal x)
+            go (path ++ [1]) subgoal.mvarId!
+  go [] goal
+
+def mkSimpTheorems (name : Name) : MetaM SimpTheorems := do
+  let sthms : SimpTheorems := {}
+  sthms.addConst name
+
+def mkSimpTheorem (name : Name) : MetaM SimpTheorem := do
+  let sthms ← mkSimpTheorems name
+  let sthms := sthms.pre.values ++ sthms.post.values
+  return sthms[0]!
+
+def delabInspectCmd (cp : CriticalPair) : MetaM (TSyntax `command) := do
+  `(command|simp_lc inspect $(mkIdent cp.thm1.origin.key) $(mkIdent cp.thm2.origin.key))
+
+def reportBadPairs  (cmdStx? : Option (TSyntax `command)) (act : M Unit) (stats := false) : MetaM Unit := do
+  let ((.unit, badPairs), numPairs) ← M.run act
+  if stats then
+    logInfo m!"Investigated {numPairs} critical pairs"
+  unless badPairs.isEmpty do
+    logError <| m!"Found {badPairs.size} non-confluent critical pairs:" ++
+      indentD (.joinSep ((← badPairs.mapM (·.pp)).toList) "\n")
+    if let .some cmdStx := cmdStx? then
+      let mut str : String := ""
+      for cp in badPairs do
+        let stx ← delabInspectCmd cp
+        str := str ++ "\n" ++ (← PrettyPrinter.ppCategory `command stx).pretty
+      str := str ++ "\n" ++ (← PrettyPrinter.ppCategory `command cmdStx).pretty
+      TryThis.addSuggestion cmdStx { suggestion := str, messageData? := m!"(lots of simp_lc_inspect lines)" }
+
+def checkSimpLCAll (cmdStx : TSyntax `command) (root_only : Bool) (pfixs? : Option (Array Name)) : MetaM Unit := do
+  let sthms ← getSimpTheorems
+  let thms := sthms.pre.values ++ sthms.post.values
+  let thms ← thms.filterM fun sthm => do
+    if sthms.erased.contains sthm.origin then
+      return false
+    if let .decl n _ false := sthm.origin then
+      if (← isIgnoredName n) then
+        return false
+      if let some pfixs := pfixs? then
+        return pfixs.any fun pfix =>
+          if pfix = `_root_
+          then n.components.length = 1
+          else pfix.isPrefixOf n
+      return true
+    return false
+  logInfo m!"Checking {thms.size} simp lemmas for critical pairs"
+  let filtered_sthms := thms.foldl SimpTheorems.addSimpTheorem (init := {})
+  reportBadPairs (stats := true) cmdStx do
+    for thm1 in thms do
+      try
+        checkSimpLC root_only .none thm1 filtered_sthms
+      catch e => logError m!"Failed to check {← ppOrigin thm1.origin}\n{← nestedExceptionToMessageData e}"
+
+def warnIfNotSimp (n : Name) : CoreM Unit := do
+  try
+    _ ← (← getSimpTheorems).erase (.decl n)
+  catch e =>
+    logWarning e.toMessageData
+
+def allowCriticalPair (cmdStx : Syntax) : NamePair → MetaM Unit := fun ⟨name1, name2⟩ => do
+  warnIfNotSimp name1
+  warnIfNotSimp name2
+  if simplc.checkAllow.get (← getOptions) then
+    let sthms : SimpTheorems ← SimpTheorems.addConst {} name2
+    let ((.unit, badPairs), _) ← M.run do
+      checkSimpLC false none (← mkSimpTheorem name1) sthms
+    if badPairs.isEmpty then
+      logWarning "No non-confluence detected. Maybe remove this?"
+      TryThis.addSuggestion cmdStx { suggestion := "", messageData? := m!"(remove this command)" }
+  let pair := if name2.quickLt name1 then (name2, name1) else (name1, name2)
+  modifyEnv (simpLCAllowExt.addEntry · pair)
+
+open Elab Command
+elab_rules : command
+| `(command|simp_lc inspect $ident1:ident $ident2:ident $[by $tac?]?) => liftTermElabM fun _ => do
+  let name1 ← realizeGlobalConstNoOverloadWithInfo ident1
+  let name2 ← realizeGlobalConstNoOverloadWithInfo ident2
+  let sthms : SimpTheorems ← SimpTheorems.addConst {} name2
+  withOptions (·.setBool `trace.simplc true) do reportBadPairs .none do
+    checkSimpLC false tac? (← mkSimpTheorem name1) sthms
+
+| `(command|simp_lc check $[root%$root?]? $[in $[$pfixs]*]?) => liftTermElabM do
+  let stx ← getRef
+  let pfixs := pfixs.map (·.map (·.getId))
+  checkSimpLCAll ⟨stx⟩ root?.isSome pfixs
+
+| `(command|simp_lc allow $thm1 $thm2) => liftTermElabM do
+  let stx ← getRef
+  let name1 ← realizeGlobalConstNoOverloadWithInfo thm1
+  let name2 ← realizeGlobalConstNoOverloadWithInfo thm2
+  allowCriticalPair stx (name1, name2)
+
+| `(command|simp_lc ignore $thm) => liftTermElabM do
+  ignoreName (← realizeGlobalConstNoOverloadWithInfo thm)
+
+| `(command|simp_lc) => liftTermElabM do
+  logWarning m!"Please use one of the `simp_lc` subcommands."
+
+end Lean.SimpLC
+
+end -- public meta section

src/Lean/SimpLC/Exceptions.lean

@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+import Init.Data.Array
+import Init.Data.List.ToArray
+public import Lean.SimpLC.Exceptions.Root
+public import Lean.SimpLC.Exceptions.Array
+public import Lean.SimpLC.Exceptions.BitVec
+public import Lean.SimpLC.Exceptions.Bool
+public import Lean.SimpLC.Exceptions.Fin
+public import Lean.SimpLC.Exceptions.List
+public import Lean.SimpLC.Exceptions.Monad
+public import Lean.SimpLC.Exceptions.Nat
+public import Lean.SimpLC.Exceptions.Option
+public import Lean.SimpLC.Exceptions.Prod
+public import Lean.SimpLC.Exceptions.Std
+public import Lean.SimpLC.Exceptions.Subtype
+public import Lean.SimpLC.Exceptions.Sum
+
+/-
+The actual checks happen in `tests/lean/000_simplc.lean`.
+These commented out commands remain here for convenience while debugging.
+-/
+
+/-
+Ideally downstream libraries would preserve the fact that the
+`simp_lc check in <...builtin types ...>` command below succeeds
+(possibly by adding further `simp_lc allow` and `simp_lc ignore` commands).
+Even better, they would add `_root_` to the check as well,
+if they do not intentionally occupy the root namespace.
+-/
+-- #guard_msgs (drop info) in
+-- simp_lc check in String Char Float USize UInt64 UInt32 UInt16 UInt8 PLift ULift Prod Sum Range
+--   Subtype ByteArray FloatArray List Option Array Int Nat Bool Id
+--   Monad LawfulFunctor LawfulApplicative LawfulMonad LawfulSingleton Std
+
+
+
+simp_lc ignore forIn'_eq_forIn
+simp_lc ignore forIn'_eq_forIn
+
+
+
+namespace Array
+
+@[simp] theorem foldlM_attach_toList [Monad m] {xs : Array α}
+    (f : β → { x // x ∈ xs.toList } → m β) (init : β) :
+    List.foldlM f init xs.toList.attach =
+      Array.foldlM (fun b ⟨x, m⟩ => f b ⟨x, by simpa using m⟩) init xs.attach := by
+  cases xs
+  simp only [List.toList_toArray]
+  rw [List.attach_toArray]
+  simp only [List.attachWith_mem_toArray, List.size_toArray,
+    List.foldlM_toArray', List.foldlM_map]
+
+@[simp] theorem foldrM_attach_toList [Monad m] [LawfulMonad m]{xs : Array α}
+    (f : { x // x ∈ xs.toList } → β → m β) (init : β) :
+    List.foldrM f init xs.toList.attach =
+      Array.foldrM (fun ⟨x, m⟩ b => f ⟨x, by simpa using m⟩ b) init xs.attach := by
+  cases xs
+  simp only [List.toList_toArray]
+  rw [List.attach_toArray]
+  simp [List.foldrM_map]
+
+@[simp] theorem foldl_attach_toList {xs : Array α} (f : β → { x // x ∈ xs.toList } → β) (init : β) :
+    List.foldl f init xs.toList.attach =
+      Array.foldl (fun b ⟨x, m⟩ => f b ⟨x, by simpa using m⟩) init xs.attach := by
+  cases xs
+  simp [List.foldl_map]
+
+@[simp] theorem foldr_attach_toList {xs : Array α} (f : { x // x ∈ xs.toList } → β → β) (init : β) :
+    List.foldr f init xs.toList.attach =
+      Array.foldr (fun ⟨x, m⟩ b => f ⟨x, by simpa using m⟩ b) init xs.attach := by
+  cases xs
+  simp [List.foldr_map]
+
+end Array
+
+/-
+Check *everything*.
+-/
+-- set_option maxHeartbeats 0 in
+-- #time
+-- #guard_msgs (drop info) in
+-- simp_lc check

src/Lean/SimpLC/Exceptions/Array.lean

@@ -0,0 +1,281 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+prelude
+import Init.Data.Array
+public import Init.Data.Array.Lemmas
+public import Init.Data.Array.Find
+public import Init.Data.List.Lemmas
+public import Init.Data.Vector.Lemmas
+import Init.Omega
+import Lean.SimpLC.Exceptions.Root
+import Lean.SimpLC.Exceptions.List
+
+set_option Elab.async false -- `simplc` crashes on the command line with a 139 without this.
+
+simp_lc ignore Array.getElem_mem -- Parallel to `List.getElem_mem`
+simp_lc ignore Array.back_mem
+
+-- Confluence problems involving `Array Prop`, which hopefully never appear in the wild!
+simp_lc allow dite_else_false Array.getD_eq_getD_getElem?
+simp_lc allow dite_else_true Array.getD_eq_getD_getElem?
+
+-- These higher order simp lemmas cause many confluence problems. Reconsider?
+simp_lc ignore Array.filterMap_subtype
+simp_lc ignore Array.map_subtype
+simp_lc ignore Array.foldl_subtype'
+simp_lc ignore Array.foldr_subtype'
+simp_lc ignore Array.foldlM_subtype
+simp_lc ignore Array.foldrM_subtype
+simp_lc ignore Array.mapFinIdx_eq_mapIdx
+simp_lc ignore Array.findSome?_subtype
+simp_lc ignore Array.findFinIdx?_subtype
+simp_lc ignore Array.findIdx_subtype
+simp_lc ignore Array.findIdx?_subtype
+
+-- This would be confluent with `Array.foldlM_map`,
+-- but that causes other problems (which we should document).
+simp_lc allow List.forIn'_toArray Array.forIn'_yield_eq_foldlM
+simp_lc allow Array.forIn_map Array.forIn_yield_eq_foldlM
+simp_lc allow Array.forIn'_map Array.forIn'_yield_eq_foldlM -- this would also require commuting `map` and `attach`
+-- These had `Array.forIn'_yield_eq_foldl` and `Array.forIn_yield_eq_foldl` which were
+-- renamed to `idRun_` variants. These are no longer `[simp]` lemmas.
+
+-- These would work except that `simp_all` is not willing to make a copy of the hypothesis.
+simp_lc allow Array.getElem?_eq_getElem Array.getElem?_pmap
+simp_lc allow Array.getElem?_eq_getElem Array.getElem?_map
+simp_lc allow Array.getElem?_eq_getElem Array.getElem?_mapFinIdx
+simp_lc allow Array.getElem?_eq_getElem Array.getElem?_attachWith
+simp_lc allow Array.getElem?_eq_getElem Array.getElem?_attach
+simp_lc allow Array.getElem?_mapIdx Array.getElem?_eq_getElem
+simp_lc allow Array.getElem?_unattach Array.getElem?_eq_getElem
+
+-- Fails at `⊢ decide (b ∈ l.push a) = (decide (b ∈ l) || b == a)`
+-- because simp won't apply `Array.mem_push` inside `decide`.
+simp_lc allow Array.contains_eq_mem Array.contains_push
+
+-- Fails at `⊢ Array.filterMap ((some ∘ f) ∘ g) l = Array.map (f ∘ g) l`
+-- and can't apply `Array.filterMap_eq_map` on the LHS because the associativity is wrong.
+simp_lc allow Array.filterMap_map Array.filterMap_eq_map
+
+-- Gets stuck with a hypothesis `h : a = b ∧ p a = true` and simp can't use it to apply `Array.filter_push_of_pos`.
+simp_lc allow Array.filterMap_eq_filter Array.filterMap_push_some
+
+-- Gets stuck at `⊢ Array.filter p (Array.map f l) 0 l.size = Array.filterMap ((Option.guard fun x => p x = true) ∘ f) l`.
+-- Not certain what to hope for here. Having `Function.comp_def` in the simp set would probably resolve it.
+simp_lc allow Array.filterMap_eq_filter Array.filterMap_map
+
+-- The simp normal form for `filterMap` vs `filter`+`map` still needs work.
+simp_lc allow Array.filterMap_eq_filter Array.filterMap_attachWith
+
+-- The simp normal form for `attachWith` vs `map`+`attach` still needs work.
+simp_lc allow Array.filterMap_some Array.filterMap_attachWith
+
+namespace List
+
+@[simp] theorem foldl_nat_add {f : α → Nat} {n : Nat} {l : List α} :
+    l.foldl (fun x y => x + f y) n = n + (l.map f).sum := by
+  induction l generalizing n <;> simp_all [Nat.add_assoc]
+
+@[simp] theorem foldr_nat_add {f : α → Nat} {n : Nat} {l : List α} :
+    l.foldr (fun x y => y + f x) n = n + (l.map f).sum := by
+  induction l generalizing n <;> simp_all [Nat.add_assoc, Nat.add_comm (f _)]
+
+@[simp] theorem sum_map_nat_const_mul {f : α → Nat} {b : Nat} {l : List α} :
+    (l.map (fun a => b * f a)).sum  = b * (l.map f).sum := by
+  induction l <;> simp_all [Nat.mul_add]
+
+@[simp] theorem sum_map_mul_nat_const {f : α → Nat} {b : Nat} {l : List α} :
+    (l.map (fun a => f a * b)).sum = (l.map f).sum * b := by
+  induction l <;> simp_all [Nat.add_mul]
+
+end List
+
+namespace Array
+
+@[simp] theorem foldl_nat_add {f : α → Nat} {n : Nat} {l : Array α} (w : stop = l.size) :
+    l.foldl (fun x y => x + f y) n 0 stop = n + (l.map f).sum := by
+  subst w
+  cases l
+  simp
+
+@[simp] theorem foldr_nat_add {f : α → Nat} {n : Nat} {l : Array α} (w : start = l.size) :
+    l.foldr (fun x y => y + f x) n start 0 = n + (l.map f).sum := by
+  subst w
+  cases l
+  simp
+
+@[simp] theorem sum_map_nat_const_mul {f : α → Nat} {b : Nat} {l : Array α} :
+    (l.map (fun a => b * f a)).sum  = b * (l.map f).sum := by
+  cases l
+  simp_all
+
+@[simp] theorem sum_map_mul_nat_const {f : α → Nat} {b : Nat} {l : Array α} :
+    (l.map (fun a => f a * b)).sum = (l.map f).sum * b := by
+  cases l
+  simp_all
+
+end Array
+
+-- Just missing some arithmetic.
+simp_lc allow Array.foldl_append' Array.foldl_add_const
+simp_lc allow Array.foldr_push' Array.foldr_add_const
+simp_lc allow Array.foldr_append' Array.foldr_add_const
+attribute [simp] Array.findSome?_append
+
+attribute [simp] Option.or_of_isSome Option.or_of_isNone
+
+attribute [simp] List.reverse_flatten Array.reverse_flatten Vector.reverse_flatten
+
+-- Gets stuck at `List.foldlM ⋯ as.toList.attach`. Since we push `toList` inwards, it's not clear what to do,
+-- except add an extra lemma.
+simp_lc allow List.forIn'_yield_eq_foldlM Array.forIn'_toList
+-- `⊢ (Array.map (fun x => replicate x.size b) L).flatten = replicate (Array.map Array.size L).sum b`
+-- Sufficiently obscure that it doesn't need a lemma.
+simp_lc allow Array.map_flatten Array.map_const
+
+
+
+
+namespace Array
+
+-- Ideally this would never appear, as we push `toList` inwards and `toArray` outwards.
+-- It sometimes appears in confluence problems, so we just add it to the simp set.
+@[simp] theorem toArray_reverse_toList {xs: Array α} : xs.toList.reverse.toArray = xs.reverse := by
+  cases xs
+  simp
+
+end Array
+
+-- FIXME:
+-- simp_lc inspect Array.pmap_eq_map Array.pmap_attachWith
+-- simp_lc inspect Array.pmap_eq_attachWith Array.pmap_attachWith
+-- simp_lc inspect Array.pmap_attach Array.pmap_eq_map
+-- simp_lc inspect Array.pmap_attach Array.pmap_eq_attachWith
+
+-- FIXME:
+-- ```
+-- al : a ∈ l
+-- pa : p a = true
+-- ⊢ l.size - 1 = (l.eraseP p).size
+-- ```
+-- simp_lc inspect Array.size_eraseP_of_mem Array.length_toList
+-- simp_lc inspect Array.size_toArray List.length_eraseP_of_mem
+-- simp_lc inspect Array.size_toArray Array.size_eraseIdx
+
+
+attribute [simp] Array.getElem_append_left Array.getElem_append_right
+
+namespace Array
+
+@[simp] theorem flatten_map_flatten_map {xss : Array (Array α)} {f : α → Array β} :
+    (Array.map (fun xs => (Array.map f xs).flatten) xss).flatten =
+      (xss.map (fun xs => xs.map f)).flatten.flatten := by
+  rcases xss with ⟨xss⟩
+  induction xss with
+  | nil => simp
+  | cons head tail ih => simp_all [Function.comp_def]
+
+@[simp] theorem nat_sum_append {xs ys : Array Nat} : (xs ++ ys).sum = xs.sum + ys.sum := by
+  rcases xs with ⟨xs⟩
+  rcases ys with ⟨ys⟩
+  simp
+
+@[simp] theorem nat_sum_map_nat_sum_map {xss : Array (Array α)} {f : α → Nat} :
+    (xss.map (fun y => (y.map f).sum)).sum = (xss.map (fun y => y.map f)).flatten.sum := by
+  rcases xss with ⟨xss⟩
+  induction xss with
+  | nil => simp
+  | cons head tail ih => rcases head with ⟨head⟩; simp_all [Function.comp_def]
+
+@[simp] theorem nat_sum_reverse {xs : Array Nat} : xs.reverse.sum = xs.sum := by
+  rcases xs with ⟨xs⟩
+  simp
+
+@[simp] theorem nat_sum_push {xs : Array Nat} {a : Nat} : (xs.push a).sum = xs.sum + a := by
+  rcases xs with ⟨xs⟩
+  simp
+
+@[simp] theorem push_replicate_self {n : Nat} {a : α} : (replicate n a).push a = replicate (n + 1) a := by
+  rw [replicate_succ]
+
+attribute [simp] Array.flatten_push
+
+@[simp] theorem pop_extract {as : Array α} {i j : Nat} :
+    (as.extract i j).pop = as.extract i ((min j as.size) - 1) := by
+  ext k h₁ h₂
+  · simp; omega
+  · simp only [size_extract, size_pop] at h₁ h₂
+    simp only [getElem_extract, getElem_pop]
+
+end Array
+
+-- These would require using `List/Array.map_const'` as a simp lemma, and then some arithmetic.
+simp_lc allow Array.foldl_nat_add Array.foldl_add_const
+simp_lc allow List.foldr_nat_add List.foldr_add_const
+simp_lc allow List.foldl_nat_add List.foldl_add_const
+
+-- These have the hypothesis `xs.size = xs.size - 1`,
+-- from which we should deduce `xs.size = 0` and then `xs = #[]`.
+-- Hopefully `grind` can do this.
+-- TODO: This causes infinite recursion in simp; needs investigation.
+-- simp_lc allow Array.extract_eq_pop Array.drop_eq_extract
+simp_lc allow Array.extract_eq_pop Array.extract_size
+
+-- Should we just simp away `List.dropLast`?
+simp_lc allow Array.extract_eq_pop List.extract_toArray
+
+-- FIXME:
+set_option maxHeartbeats 1000000 in
+simp_lc allow Array.foldl_flip_append_eq_append Array.foldl_flatten'
+set_option maxHeartbeats 1000000 in
+simp_lc allow Array.foldr_flip_append_eq_append Array.foldr_flatten'
+set_option maxHeartbeats 1000000 in
+simp_lc allow Array.foldr_attachWith Array.foldr_flip_append_eq_append
+
+simp_lc allow Array.filterMap_eq_map' Array.filterMap_map
+simp_lc allow Array.foldl_append_eq_append List.foldl_toArray'
+simp_lc allow Array.foldl_append_eq_append Array.foldl_attachWith
+simp_lc allow Array.foldl_flip_append_eq_append List.foldl_toArray'
+simp_lc allow Array.foldl_flip_append_eq_append Array.foldl_attachWith
+simp_lc allow Array.foldl_cons_eq_append Array.foldl_flatten'
+simp_lc allow List.foldr_toArray' Array.foldr_append_eq_append
+simp_lc allow List.foldr_toArray' Array.foldr_flip_append_eq_append
+simp_lc allow Array.foldr_append_eq_append Array.foldr_attachWith
+simp_lc allow Array.foldr_cons_eq_append Array.foldr_flatten'
+simp_lc allow Array.foldr_cons_eq_append' Array.foldr_flatten'
+simp_lc allow Array.foldr_attachWith Array.foldr_cons_eq_append'
+simp_lc allow List.getLast!_eq_getLast?_getD Array.getLast!_toList
+simp_lc allow Array.map_const Array.map_attachWith
+simp_lc allow Array.flatten_toArray Array.flatten_toArray_map_toArray
+simp_lc allow Array.foldr_toList List.foldr_push_eq_append
+simp_lc allow Array.foldr_toList List.foldr_append_eq_append
+simp_lc allow Array.foldr_toList List.foldr_flip_append_eq_append
+simp_lc allow Array.flatMap_singleton' Array.flatMap_subtype
+simp_lc allow Array.pmap_eq_map Array.pmap_attachWith
+simp_lc allow Array.pmap_eq_attachWith Array.pmap_attachWith
+simp_lc allow Array.pmap_attach Array.pmap_eq_map
+simp_lc allow Array.pmap_attach Array.pmap_eq_attachWith
+simp_lc allow Array.extract_of_size_lt Array.extract_append
+simp_lc allow Array.extract_eq_pop Array.extract_extract
+simp_lc allow Array.extract_eq_pop Array.extract_append
+simp_lc allow Array.extract_size Array.extract_append
+simp_lc allow Array.extract_extract Array.extract_of_size_lt
+simp_lc allow Array.extract_extract Array.extract_size
+simp_lc allow Array.size_eraseP_of_mem Array.length_toList
+
+simp_lc allow List.foldl_push_eq_append Array.foldl_toList
+simp_lc allow List.foldl_flip_append_eq_append Array.foldl_toList
+
+/-
+The actual checks happen in `tests/lean/000_simplc.lean`.
+This commented out command remains here for convenience while debugging.
+-/
+-- set_option maxHeartbeats 0 in
+-- #guard_msgs (drop info) in
+-- simp_lc check in Array List BEq Id _root_

src/Lean/SimpLC/Exceptions/BitVec.lean

@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+prelude
+import Init.Data.BitVec
+import Lean.SimpLC.Exceptions.Root
+import Std.Tactic.BVDecide
+
+set_option Elab.async false -- `simplc` crashes on the command line with a 139 without this.
+
+simp_lc ignore BitVec.getLsbD_of_ge
+simp_lc ignore BitVec.getMsbD_of_ge
+
+namespace BitVec
+
+-- This would be resolved by simply using `setWidth` instead of `cast`!
+-- TODO: discuss with Tobias et al.
+example (h : v = w) (x : BitVec v) : x.cast h = x.setWidth w := by
+  ext
+  simp_all
+simp_lc allow BitVec.setWidth_eq BitVec.setWidth_cast
+
+example (w : Nat) : 1#w = if w = 0 then 0#w else 1#w := by
+  cases w <;> simp
+simp_lc allow BitVec.udiv_one BitVec.udiv_self
+
+-- This is commented out because `cadical` doesn't seem to be available in Nix CI.
+-- example (x : BitVec 1) : x = if x = 0#1 then 0#1 else 1#1 := by bv_decide
+simp_lc allow BitVec.udiv_eq_and BitVec.udiv_self
+
+example (w : Nat) : w = 0 → 0#w = 1#w := by rintro rfl; simp
+simp_lc allow BitVec.sdiv_self BitVec.sdiv_one
+
+-- TODO: these need further investigation.
+simp_lc allow BitVec.neg_mul BitVec.mul_twoPow_eq_shiftLeft
+simp_lc allow BitVec.shiftLeft_eq_zero BitVec.shiftLeft_zero
+simp_lc allow BitVec.lt_ofFin BitVec.not_allOnes_lt
+simp_lc allow BitVec.lt_one_iff BitVec.ofFin_lt
+simp_lc allow BitVec.lt_one_iff BitVec.not_allOnes_lt
+simp_lc allow BitVec.ofFin_lt BitVec.not_lt_zero
+simp_lc allow BitVec.ofNat_lt_ofNat BitVec.lt_one_iff
+simp_lc allow BitVec.le_ofFin BitVec.allOnes_le_iff
+simp_lc allow BitVec.le_zero_iff BitVec.allOnes_le_iff
+simp_lc allow BitVec.ofFin_le BitVec.le_zero_iff
+simp_lc allow BitVec.ofNat_le_ofNat BitVec.le_zero_iff
+simp_lc allow BitVec.getMsbD_setWidth BitVec.getMsbD_setWidth_add
+
+/-
+The actual checks happen in `tests/lean/000_simplc.lean`.
+This commented out command remains here for convenience while debugging.
+-/
+-- #guard_msgs (drop info) in
+-- simp_lc check in BitVec

src/Lean/SimpLC/Exceptions/Bool.lean

@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+prelude
+import Init.Data.Bool
+import Lean.SimpLC.Exceptions.Root
+
+set_option Elab.async false -- `simplc` crashes on the command line with a 139 without this.
+
+simp_lc allow Bool.bne_assoc Bool.bne_self_left -- `(x != (y != (x != (y != b)))) = b` `(y != (x != y)) = x`
+
+-- #guard_msgs (drop info) in
+-- simp_lc check in Bool
+
+-- x y : Bool
+-- ⊢ x = (y != (x != y))
+simp_lc allow bne_self_eq_false Bool.bne_assoc
+
+-- I'd expected that making `Decidable.em` a `@[simp]` would help here, but it doesn't seem to.
+-- w : Decidable p
+-- ⊢ p ∨ ¬p
+simp_lc allow ite_else_decide_not_self Bool.if_true_left
+-- w : Decidable p
+-- ⊢ ¬p ∨ p
+simp_lc allow ite_then_decide_self Bool.if_true_right
+
+-- These produce many non-confluence goals that would be easily solved by better automation.
+simp_lc ignore Bool.exists_bool
+simp_lc ignore Bool.forall_bool
+
+simp_lc allow ite_eq_left_iff Bool.ite_eq_cond_iff
+simp_lc allow ite_eq_right_iff Bool.ite_eq_cond_iff
+
+/-
+The actual checks happen in `tests/lean/000_simplc.lean`.
+This commented out command remains here for convenience while debugging.
+-/
+-- #guard_msgs (drop info) in
+-- simp_lc check in _root_ Bool

src/Lean/SimpLC/Exceptions/Fin.lean

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+prelude
+import Init.Data.Fin
+import Init.Omega
+import Lean.SimpLC
+
+set_option Elab.async false -- `simplc` crashes on the command line with a 139 without this.
+
+-- This seems like a weird corner case. The discharger doesn't simplify `h` because it is used.
+example (n m : Nat) (i : Fin n) (h : 0 + n = m + n) : Fin.natAdd m i = Fin.cast (by omega) i := by
+  simp at h
+  ext
+  simpa
+simp_lc allow Fin.cast_addNat_right Fin.cast_addNat_zero
+
+/-
+The actual checks happen in `tests/lean/000_simplc.lean`.
+This commented out command remains here for convenience while debugging.
+-/
+-- #guard_msgs (drop info) in
+-- simp_lc check in Fin

src/Lean/SimpLC/Exceptions/List.lean

@@ -0,0 +1,183 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+prelude
+import Init.Data.List
+import Init.Omega
+import Lean.SimpLC.Exceptions.Root
+
+set_option Elab.async false -- `simplc` crashes on the command line with a 139 without this.
+
+open List
+
+simp_lc allow List.map_const List.map_flatten -- too hard?
+
+simp_lc allow List.drop_tail List.drop_one -- Would require an infinite chain of lemmas to resolve!
+simp_lc allow List.findSome?_replicate_of_pos List.findSome?_replicate_of_isSome -- split in the discharger would get us there
+
+-- These would all be okay, except that `simp_all` is unwilling to make a copy of a hypothesis which is being used.
+simp_lc allow List.getElem?_eq_getElem List.getElem?_zipIdx
+simp_lc allow List.getElem?_map List.getElem?_eq_getElem
+simp_lc allow List.getElem?_modify_eq List.getElem?_eq_getElem
+simp_lc allow List.getElem?_mapIdx List.getElem?_eq_getElem
+simp_lc allow List.getElem?_eq_getElem List.getElem?_modifyHead_zero
+
+simp_lc allow List.drop_one List.drop_left' -- `h : l₁.length = 1 ⊢ (l₁ ++ l₂).tail = l₂`
+
+-- These would be resolved by a `ring` tactic, but are beyond `simp +arith`.
+simp_lc allow List.foldl_cons List.foldl_add_const
+simp_lc allow List.foldr_cons List.foldr_add_const
+simp_lc allow List.foldr_append List.foldr_add_const
+simp_lc allow List.foldl_append List.foldl_add_const
+
+/-- This would require an infinite chain of lemmas. -/
+example {a : α} {l₁ l₂ : List α} : ¬ a :: (l₁ ++ l₂) <+ l₁ := by
+  intro h
+  replace h := h.length_le
+  simp at h
+  omega
+simp_lc allow List.Sublist.cons List.append_right_sublist_self
+
+/-- This would require an infinite chain of lemmas. -/
+example {a : α} {l₁ l₂ : List α} : ¬ l₁ ++ (a :: l₂) <+ l₂ := by
+  intro h
+  replace h := h.length_le
+  simp at h
+  omega
+simp_lc allow List.append_left_sublist_self List.Sublist.cons
+
+/- The four can't be easily handled by `simp` without introducing infinite chains of lemmas,
+but would be nice to have good automation for! -/
+simp_lc allow List.cons_sublist_cons List.Sublist.cons
+simp_lc allow List.append_left_sublist_self List.sublist_append_of_sublist_left
+simp_lc allow List.append_left_sublist_self List.sublist_append_of_sublist_right
+simp_lc allow List.append_right_sublist_self List.sublist_append_of_sublist_right
+simp_lc allow List.append_sublist_append_left List.sublist_append_of_sublist_right
+simp_lc allow List.append_sublist_append_right List.sublist_append_of_sublist_left
+
+-- This one works, just not by `simp_all` because it is unwilling to make a copy of `h₂`.
+example {p : α → Prop} {f : (a : α) → p a → β} {l : List α} {h₁ : ∀ (a : α), a ∈ l → p a}
+    {n : Nat} {h₂ : n < (List.pmap f l h₁).length} :
+    some (f (l[n]'(by simpa using h₂)) (h₁ _ (getElem_mem _))) =
+      Option.pmap f l[n]? (fun a h => h₁ a (mem_of_getElem? h)) := by
+  simp at h₂
+  simp [h₂]
+
+simp_lc allow List.getElem?_eq_getElem List.getElem?_pmap
+-- As above, `simp_all` is unwilling to make a copy of a hypothesis.
+simp_lc allow List.getElem?_eq_getElem List.getElem?_attach
+simp_lc allow List.getElem?_eq_getElem List.getElem?_attachWith
+simp_lc allow List.getElem?_eq_getElem List.getElem?_mapFinIdx
+simp_lc allow List.getElem?_eq_getElem List.getElem?_unattach
+
+-- These are helpful for `simp` to discharge side conditions, but generate too many false positives.
+simp_lc ignore List.head_mem
+simp_lc ignore List.getLast_mem
+simp_lc ignore List.getElem_mem
+
+-- These higher order simp lemmas cause many confluence problems. Reconsider?
+simp_lc ignore List.filterMap_subtype
+simp_lc ignore List.map_subtype
+simp_lc ignore List.flatMap_subtype
+simp_lc ignore List.foldl_subtype
+simp_lc ignore List.foldr_subtype
+simp_lc ignore List.foldlM_subtype
+simp_lc ignore List.foldrM_subtype
+simp_lc ignore List.mapFinIdx_eq_mapIdx
+simp_lc ignore List.findSome?_subtype
+simp_lc ignore List.findFinIdx?_subtype
+simp_lc ignore List.findIdx_subtype
+simp_lc ignore List.findIdx?_subtype
+
+/-
+The actual checks happen in `tests/lean/000_simplc.lean`.
+This commented out command remains here for convenience while debugging.
+-/
+#guard_msgs (drop info) in
+
+-- This would be confluent with `List.foldlM_map`,
+-- but that causes other problems (which we should document).
+simp_lc allow List.forIn'_yield_eq_foldlM List.forIn'_map
+simp_lc allow List.forIn'_yield_eq_foldlM List.forIn'_cons
+simp_lc allow List.idRun_forIn_yield_eq_foldl List.forIn_map
+-- This would be confluent with `List.foldl_map`, but that can't be a simp lemma.
+simp_lc allow List.forIn'_map List.idRun_forIn'_yield_eq_foldl
+simp_lc allow List.forIn'_cons List.idRun_forIn'_yield_eq_foldl
+simp_lc allow List.forIn_yield_eq_foldlM List.forIn_map
+
+namespace List
+
+-- `foldl_push_eq_append` and `foldr_push_eq_append` are now in Init.Data.Array.Lemmas
+
+@[simp] theorem tail_take_one {l : List α} : (l.take 1).tail = [] := by
+  induction l <;> simp [*]
+
+-- `getElem_append_left` and `getElem_append_right` are already `@[simp]` in Init.Data.List.BasicAux
+
+end List
+
+-- We should try adding:
+-- attribute [simp] List.map_attach
+-- `List.foldr_push` and `List.foldl_push` no longer exist
+simp_lc allow List.foldr_push_eq_append List.foldr_attachWith
+simp_lc allow List.foldl_push_eq_append List.foldl_attachWith
+
+-- FIXME These still need thinking about.
+simp_lc allow List.pmap_eq_attachWith List.pmap_attachWith
+simp_lc allow List.pmap_eq_attachWith List.pmap_attach
+simp_lc allow List.pmap_attachWith List.pmap_eq_map
+simp_lc allow List.pmap_attach List.pmap_eq_map
+simp_lc allow List.attachWith_mem_toArray List.attachWith_reverse
+simp_lc allow List.attachWith_mem_toArray List.attachWith_append
+simp_lc allow List.attachWith_cons List.attachWith_mem_toArray
+simp_lc allow List.map_const List.map_attachWith
+simp_lc allow List.foldr_cons_eq_append' List.foldr_attachWith
+
+-- FIXME what is happening here?
+simp_lc allow List.size_toArray List.length_eraseP_of_mem
+
+namespace List
+
+@[simp] theorem flatten_map_flatten_map {xss : List (List α)} {f : α → List β} :
+    (List.map (fun xs => (List.map f xs).flatten) xss).flatten =
+      (xss.map (fun xs => xs.map f)).flatten.flatten := by
+  induction xss with
+  | nil => simp
+  | cons head tail ih => simp [ih]
+
+@[simp] theorem nat_sum_append {l₁ l₂ : List Nat} : (l₁ ++ l₂).sum = l₁.sum + l₂.sum := by
+  induction l₁ with
+  | nil => simp
+  | cons head tail ih => simp [ih]; omega
+
+@[simp] theorem nat_sum_map_nat_sum_map {xss : List (List α)} {f : α → Nat} :
+    (xss.map (fun y => (y.map f).sum)).sum = (xss.map (fun y => y.map f)).flatten.sum := by
+  induction xss with
+  | nil => simp
+  | cons head tail ih => simp_all [Function.comp_def]
+
+@[simp] theorem sum_map_toList [Zero β] [Add β] {xs : Array α} {f : α → β} :
+    (xs.toList.map f).sum = (xs.map f).sum := by
+  rcases xs with ⟨xs⟩
+  induction xs with
+  | nil => simp
+  | cons head tail ih => simp
+
+@[simp] theorem nat_sum_reverse {l : List Nat} : l.reverse.sum = l.sum := by
+  induction l with
+  | nil => simp
+  | cons head tail ih => simp [ih]; omega
+
+end List
+
+/-
+The actual checks happen in `tests/lean/000_simplc.lean`.
+This commented out command remains here for convenience while debugging.
+-/
+-- #guard_msgs (drop info) in
+-- simp_lc check in List BEq _root_

src/Lean/SimpLC/Exceptions/Monad.lean

@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+prelude
+import Init.Control
+import Lean.SimpLC.Exceptions.Root
+
+set_option Elab.async false -- `simplc` crashes on the command line with a 139 without this.
+
+/-
+The actual checks happen in `tests/lean/000_simplc.lean`.
+This commented out command remains here for convenience while debugging.
+-/
+-- #guard_msgs (drop info) in
+-- simp_lc check in Monad LawfulMonad LawfulApplicative _root_ ExceptT

src/Lean/SimpLC/Exceptions/Nat.lean

@@ -0,0 +1,100 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+prelude
+import Init.Data.Nat
+import Init.Data.Int
+import Init.Omega
+import Lean.SimpLC.Exceptions.Root
+
+set_option Elab.async false -- `simplc` crashes on the command line with a 139 without this.
+
+theorem Int.emod_add_div (m k : Int) : m % k + k * (m / k) = m := by
+  simp [Int.emod_def]
+
+-- The following two somewhat obscure facts could probably be included as theorems.
+-- However as a simp lemma it does not improve confluence:
+-- it just creates more goals with iterated `%`.
+theorem Nat.mod_self_mod_eq_zero_of_mod_dvd_right (a b : Nat) (h : a % b ∣ b) : a % (a % b) = 0 := by
+  obtain ⟨k, h⟩ := h
+  rw [Nat.mod_eq_zero_of_dvd]
+  have p : a = a % b + b * (a / b) := (Nat.mod_add_div a b).symm
+  replace p : a = a % b + (a % b * k) * (a / b) := by
+    conv at p => rhs; rhs; lhs; rw [h]
+    exact p
+  replace p : a = (a % b) * (1 + k * (a / b)) := by
+    conv at p => rhs; lhs; rw [← Nat.mul_one (a % b)]
+    rwa [Nat.mul_assoc, ← Nat.mul_add] at p
+  conv => rhs; rw [p]
+  exact Nat.dvd_mul_right _ _
+
+theorem Int.mod_self_mod_eq_zero_of_mod_dvd_right (a b : Int) (h : a % b ∣ b) : a % (a % b) = 0 := by
+  obtain ⟨k, h⟩ := h
+  rw [Int.emod_eq_zero_of_dvd]
+  have p : a = a % b + b * (a / b) := (Int.emod_add_div a b).symm
+  replace p : a = a % b + (a % b * k) * (a / b) := by
+    conv at p => rhs; rhs; lhs; rw [h]
+    exact p
+  replace p : a = (a % b) * (1 + k * (a / b)) := by
+    conv at p => rhs; lhs; rw [← Int.mul_one (a % b)]
+    rwa [Int.mul_assoc, ← Int.mul_add] at p
+  conv => rhs; rw [p]
+  exact Int.dvd_mul_right _ _
+
+simp_lc allow Nat.mod_self Nat.mod_mod_of_dvd
+simp_lc allow Int.emod_self Int.emod_emod_of_dvd
+
+-- Ugly corner case, let's just allow it.
+example (n k : Int) : Prop := ∀ (_ : n % k + 1 ∣ k) (_ : 0 ≤ n % k), n % (n % k + 1) = n % k
+simp_lc allow Int.emod_emod_of_dvd Int.emod_self_add_one
+
+-- These could be added as simp lemmas, resolving the non-confluence between
+-- `Int.mul_ediv_mul_of_pos_left` and `Int.mul_ediv_mul_of_pos`,
+-- but they themselves cause further non-confluence.
+theorem Int.ediv_self_of_pos (a : Int) (_ : 0 < a) : a / a = 1 := Int.ediv_self (by omega)
+theorem Int.ediv_self_of_lt_zero (a : Int) (_ : a < 0) : a / a = 1 := Int.ediv_self (by omega)
+simp_lc allow Int.mul_ediv_mul_of_pos_left Int.mul_ediv_mul_of_pos
+
+/-!
+The following theorems could be added a simp lemmas,
+improving confluence and avoiding needing the three `allow` statements below,
+however they have bad discrimination tree keys (`@Exists Nat <other>`) so we just allow it.
+-/
+theorem Nat.exists_ne {y : Nat} : ∃ x, x ≠ y := ⟨y + 1, by simp⟩
+
+theorem Nat.exists_succ_eq_right (q : Nat → Prop) (a : Nat) :
+    (∃ n, q (n + 1) ∧ n + 1 = a) ↔ a ≠ 0 ∧ q a :=
+  ⟨by rintro ⟨n, h, rfl⟩; exact ⟨by simp, h⟩, by rintro ⟨h₁, h₂⟩; match a, h₁ with | a + 1, _ => exact ⟨a, h₂, rfl⟩⟩
+theorem Nat.exists_eq_succ_right (q : Nat → Prop) (a : Nat) :
+    (∃ n, q (n + 1) ∧ a = n + 1) ↔ a ≠ 0 ∧ q a := by
+  simp [eq_comm (a := a), exists_succ_eq_right]
+theorem Nat.exists_succ_eq_left (q : Nat → Prop) (a : Nat) :
+    (∃ n, n + 1 = a ∧ q (n + 1)) ↔ a ≠ 0 ∧ q a := by
+  simp [and_comm, exists_succ_eq_right]
+theorem Nat.exists_eq_succ_left (q : Nat → Prop) (a : Nat) :
+    (∃ n, n + 1 = a ∧ q (n + 1)) ↔ a ≠ 0 ∧ q a := by
+  simp [and_comm, exists_succ_eq_right]
+
+simp_lc allow exists_and_right Nat.exists_ne_zero
+simp_lc allow exists_eq_right_right Nat.exists_ne_zero
+simp_lc allow exists_eq_right_right' Nat.exists_ne_zero
+
+-- An obscure interaction?
+example (a b : Nat) (h : 2 ^ (a % b) ∣ b) : a % 2 ^ (a % b) = a % b := by
+  have : a % b % 2 ^ (a % b) = a % b % 2 ^ (a % b) := rfl
+  conv at this => lhs; rw [Nat.mod_mod_of_dvd _ h]
+  conv at this => rhs; rw [Nat.mod_two_pow_self]
+  exact this
+simp_lc allow Nat.mod_mod_of_dvd Nat.mod_two_pow_self
+
+/-
+The actual checks happen in `tests/lean/000_simplc.lean`.
+This commented out command remains here for convenience while debugging.
+-/
+-- #guard_msgs (drop info) in
+-- simp_lc check in _root_ Nat Int

src/Lean/SimpLC/Exceptions/Option.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+prelude
+import Init.Data.Option
+import Lean.SimpLC.Exceptions.Root
+
+set_option Elab.async false -- `simplc` crashes on the command line with a 139 without this.
+
+-- These higher order simp lemmas cause many confluence problems. Reconsider?
+simp_lc ignore Option.map_subtype
+simp_lc ignore Option.bind_subtype
+
+namespace Option
+
+-- `not_mem_none` is already `@[simp]` in Init.Data.Option.Lemmas
+
+@[simp] theorem elim_map {f : α → β} {o : Option α} {b : γ} {g} :
+    (Option.map f o).elim b g = o.elim b (fun a => g (f a)) := by
+  cases o <;> simp
+
+
+@[simp] theorem pelim_map {f : α → β} {o : Option α} {b : γ} {g} :
+    (Option.map f o).pelim b g = o.pelim b (fun a h => g (f a) (mem_map_of_mem f h)) := by
+  cases o <;> simp
+
+/-
+The actual checks happen in `tests/lean/000_simplc.lean`.
+This commented out command remains here for convenience while debugging.
+-/
+-- #guard_msgs (drop info) in
+-- simp_lc check in Option _root_

src/Lean/SimpLC/Exceptions/Prod.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+prelude
+import Init.Data.Prod
+import Lean.SimpLC.Exceptions.Root
+
+set_option Elab.async false -- `simplc` crashes on the command line with a 139 without this.
+
+simp_lc ignore Prod.exists
+simp_lc ignore Prod.forall
+
+/-
+The actual checks happen in `tests/lean/000_simplc.lean`.
+This commented out command remains here for convenience while debugging.
+-/
+-- #guard_msgs (drop info) in
+-- simp_lc check in Prod _root_

src/Lean/SimpLC/Exceptions/Root.lean

@@ -0,0 +1,81 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+prelude
+import Init.Data
+public import Lean.SimpLC
+import Lean.Elab.Tactic.Grind
+
+set_option Elab.async false -- `simplc` crashes on the command line with a 139 without this.
+
+-- This possibly could be a simp lemma.
+-- It would fire on any `arrow` goal, but we have plenty of these already.
+example (x : True → Prop) : (∀ (h : True), x h) ↔ x True.intro :=
+  ⟨fun h => h .intro, fun h _ => h⟩
+simp_lc allow dite_else_true dite_true
+
+-- Similarly, this could be an `arrow`-indexed simp lemma, but seems very unlikely to be useful.
+example (f : α → False) (p : False → Prop) : (∀ (a : α), p (f a)) ↔ True :=
+  ⟨fun _ => True.intro, fun _ a => False.elim (f a)⟩
+simp_lc allow forall_false forall_apply_eq_imp_iff
+simp_lc allow forall_false forall_eq_apply_imp_iff
+
+-- Again, unlikely to be useful.
+example (p : α → Prop) (f : α → False) (q : False → Prop) : (∀ (a : α), p a → q (f a)) ↔ True :=
+  ⟨fun _ => True.intro, fun _ a _ => False.elim (f a)⟩
+simp_lc allow forall_false forall_apply_eq_imp_iff₂
+
+-- Produces many non-confluence goals that could be resolved by better automation.
+simp_lc ignore forall_exists_index
+
+-- The following would be easy with some additional automation; indeed `grind` works well.
+-- example (q : α → Prop) (a b : α) : q a ∧ b = a ↔ b = a ∧ q b := by
+--   grind
+simp_lc allow exists_eq_left exists_eq_right_right'
+simp_lc allow exists_eq_right exists_eq_left
+simp_lc allow exists_eq_right exists_eq_or_imp
+simp_lc allow exists_eq_left' exists_eq_right_right'
+simp_lc allow exists_eq_right' exists_eq_left'
+simp_lc allow exists_eq_right_right exists_eq_left
+simp_lc allow exists_eq_right_right exists_eq_left'
+simp_lc allow exists_eq_right_right exists_eq_or_imp
+simp_lc allow exists_eq_right_right' exists_eq_or_imp
+
+-- These are terrible: they involve different decidable instances
+-- (which must all be equal, but the automation doesn't know that).
+example {P : Prop} (h h' : Decidable P) :
+    ((@decide P h) || (@decide P h')) = ((@decide P h') || (@decide P h)) := by
+  have : h = h' := Subsingleton.elim _ _
+  -- grind -- works from here
+  subst this
+  simp
+simp_lc allow ite_else_decide_not_self ite_then_decide_not_self
+simp_lc allow ite_then_decide_self ite_else_decide_self
+
+-- This would be resolved if `exists_prop'` were a simp lemma, but it is not.
+-- See https://github.com/leanprover/lean4/pull/5529
+simp_lc allow exists_and_left exists_and_right
+
+-- Can we add:
+theorem forall_true (p : True → Prop) : (∀ h : True, p h) ↔ p True.intro :=
+  ⟨fun h => h .intro, fun h _ => h⟩
+-- Without it we need:
+simp_lc allow forall_self_imp forall_apply_eq_imp_iff
+simp_lc allow forall_self_imp forall_eq_apply_imp_iff
+simp_lc allow forall_self_imp forall_apply_eq_imp_iff₂
+
+-- This is a tricky lemma that removes unused functional dependencies.
+-- It causes confluence problems, but is quite useful.
+simp_lc ignore forIn'_eq_forIn
+
+/-
+The actual checks happen in `tests/lean/000_simplc.lean`.
+This commented out command remains here for convenience while debugging.
+-/
+-- #guard_msgs (drop info) in
+-- simp_lc check in Id _root_

src/Lean/SimpLC/Exceptions/Std.lean

@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+prelude
+import Std
+import Lean.SimpLC.Exceptions.Root
+
+set_option Elab.async false -- `simplc` crashes on the command line with a 139 without this.
+
+-- Internal implementation details of `DHashMap`.
+simp_lc ignore Std.DHashMap.Internal.Raw₀.contains_keys
+simp_lc ignore Std.DHashMap.Internal.Raw₀.mem_keys
+
+-- I don't understand this next set: `simp` seems to close the goal.
+example {α : Type _} [BEq α] [EquivBEq α] (a : α) : (a == a) = true := by simp
+example {α : Type _} {β : Type _} [BEq α] [Hashable α] {m : Std.HashMap α β}
+    [LawfulHashable α] {a : α} {_ : β} [EquivBEq α] [LawfulHashable α] :
+    (a == a) = true ∨ a ∈ m :=
+  by simp
+
+simp_lc allow Std.HashSet.Raw.contains_insert Std.HashSet.Raw.contains_insert_self
+simp_lc allow Std.DHashMap.Raw.mem_insert Std.DHashMap.Raw.mem_insert_self
+simp_lc allow Std.HashMap.Raw.mem_insert_self Std.HashMap.Raw.mem_insert
+simp_lc allow Std.HashSet.Raw.mem_insert Std.HashSet.Raw.mem_insert_self
+simp_lc allow Std.DHashMap.Raw.contains_insert Std.DHashMap.Raw.contains_insert_self
+simp_lc allow Std.HashMap.Raw.contains_insert Std.HashMap.Raw.contains_insert_self
+
+-- TODO: I'm confused by these ones,
+-- which I can't seem to construct simp lemmas to resolve.
+simp_lc allow Std.HashSet.insert_eq_insert LawfulSingleton.insert_empty_eq
+simp_lc allow Std.HashMap.insert_eq_insert LawfulSingleton.insert_empty_eq
+simp_lc allow Std.DHashMap.insert_eq_insert LawfulSingleton.insert_empty_eq
+simp_lc allow Std.HashSet.Raw.insert_eq_insert LawfulSingleton.insert_empty_eq
+simp_lc allow Std.HashMap.Raw.insert_eq_insert LawfulSingleton.insert_empty_eq
+simp_lc allow LawfulSingleton.insert_empty_eq Std.DHashMap.Raw.insert_eq_insert
+
+simp_lc allow Std.DHashMap.Raw.contains_keys Std.DHashMap.Internal.Raw₀.contains_keys
+simp_lc allow Std.HashMap.Raw.get!_eq_getElem! Std.HashMap.Raw.getElem!_modify_self
+simp_lc allow Std.HashMap.Raw.get?_eq_getElem? Std.HashMap.Raw.getElem?_modify_self
+simp_lc allow Std.DHashMap.Internal.Raw₀.mem_keys Std.DHashMap.Raw.mem_keys
+simp_lc allow Std.HashMap.Raw.get_eq_getElem Std.HashMap.Raw.getElem_modify_self
+
+/-
+The actual checks happen in `tests/lean/000_simplc.lean`.
+This commented out command remains here for convenience while debugging.
+-/
+-- set_option maxHeartbeats 1000000 in
+-- #guard_msgs (drop info) in
+-- simp_lc check in Std Id LawfulSingleton _root_

src/Lean/SimpLC/Exceptions/Subtype.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+prelude
+import Init.Data.Subtype
+import Lean.SimpLC.Exceptions.Root
+
+set_option Elab.async false -- `simplc` crashes on the command line with a 139 without this.
+
+simp_lc ignore Subtype.exists
+simp_lc ignore Subtype.forall
+
+/-
+The actual checks happen in `tests/lean/000_simplc.lean`.
+This commented out command remains here for convenience while debugging.
+-/
+-- #guard_msgs (drop info) in
+-- simp_lc check in Subtype _root_

src/Lean/SimpLC/Exceptions/Sum.lean

@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+prelude
+import Init.Data.Sum
+import Lean.SimpLC.Exceptions.List
+import Lean.SimpLC.Exceptions.Bool
+import Lean.SimpLC.Exceptions.Nat
+import Lean.SimpLC.Exceptions.Root
+
+set_option Elab.async false -- `simplc` crashes on the command line with a 139 without this.
+
+simp_lc ignore Sum.getLeft_eq_iff
+simp_lc ignore Sum.getRight_eq_iff
+
+/-
+The actual checks happen in `tests/lean/000_simplc.lean`.
+This commented out command remains here for convenience while debugging.
+-/
+-- #guard_msgs (drop info) in
+-- simp_lc check in Sum List Bool Nat _root_

src/Lean/SimpLC/MVarCycles.lean

@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+module
+
+prelude
+public import Lean.Meta.Basic
+
+public section
+
+open Lean Meta
+
+namespace Lean.Meta.MVarCycles
+
+/-- How the expression relates to the mvar (type, expression, delayed) -/
+inductive ToA where | T | A | D
+
+abbrev Path := Array (MVarId × ToA × Expr)
+
+-- I failed to prevent {Expr.mvar mvarId} from instantiating the mvar
+-- even with `withOptions (pp.instantiateMVars.set · false) do`
+def ppMVar (mvarId : MVarId) : MetaM MessageData := do
+  let mvarDecl ← mvarId.getDecl
+  let n :=
+    match mvarDecl.userName with
+    | .anonymous => mvarId.name.replacePrefix `_uniq `m
+    | n => n
+  return m!"?{mkIdent n}"
+
+def raiseCyclicMVarError (path : Path) : MetaM Unit := do
+  let mut msg := m!"Found cycle in the mvar context:"
+  for (mvarId, toa, e) in path do
+    match toa with
+    | .T => msg := msg ++ m!"\n{← ppMVar mvarId} :: {e}"
+    | .A => msg := msg ++ m!"\n{← ppMVar mvarId} := {e}"
+    | .D => msg := msg ++ m!"\n{← ppMVar mvarId} := {e} (delayed assignment)"
+  throwError msg
+
+/-!
+Checks the current MVar assignments and types for cycles and if it finds one, throws an exception.
+with a pretty representation thereof. Level MVars are ignored for now.
+-/
+
+partial def checkMVarsCycles : MetaM Unit := StateT.run' (s := {}) do
+  let mctxt ← getMCtx
+  for (mvarid, _) in mctxt.decls do
+    go #[] mvarid
+where
+  go (path : Path) (mvarId : MVarId) : StateT (Std.HashSet MVarId) MetaM Unit := do
+    -- already handled this mvar?
+    if (← get).contains mvarId then return
+
+    -- did we find a cycle?
+    if let .some i := path.findIdx? (·.1 == mvarId) then
+      raiseCyclicMVarError path[i:]
+
+    -- traverse the type
+    let t :=  (← mvarId.getDecl).type
+    goE (path.push (mvarId, .T, t)) t
+    -- traverse the expression assignemnt
+    if let .some e ← getExprMVarAssignment? mvarId then
+      goE (path.push (mvarId, .A, e)) e
+    -- traverse the delayed assignemnt
+    if let .some da ← getDelayedMVarAssignment? mvarId then
+      go (path.push (mvarId, .A, .mvar da.mvarIdPending)) da.mvarIdPending
+
+    -- all good? Remember as such
+    modify (·.insert mvarId)
+
+  goE (path : Path) (e : Expr) : StateT (Std.HashSet MVarId) MetaM Unit := do
+    if !e.hasMVar then return
+    match e with
+    | (.lit _)           => return
+    | (.bvar _)          => return
+    | (.fvar _)          => return
+    | (.sort _)          => return
+    | (.const _ _)      => return
+    | (.proj _ _ s)      => goE path s
+    | (.app f a)         => goE path f; goE path a
+    | (.mdata _ b)       => goE path b
+    | (.lam _ d b _)     => goE path d; goE path b
+    | (.forallE _ d b _) => goE path d; goE path b
+    | (.letE _ t v b _)  => goE path t; goE path v; goE path b
+    | (.mvar mvarId)     => go path mvarId
+
+end Lean.Meta.MVarCycles
+
+end -- public section

src/Lean/SimpLC/README.md

@@ -0,0 +1,25 @@
+## `simp` local confluence checker
+
+The `Lean.SimpLC` library provides a simp local confluence checker.
+
+* `simp_lc check`: Investigates the full simp set.
+* `simp_lc check in X Y Z`: Investigates the simp set in the specified namespaces.
+* `simp_lc inspect`: Investigates one pair
+* `simp_lc allow`: Allows a critical pair (checks that it is currently critical, and suppresses further reports from `check`)
+* `simp_lc ignore`: Ignores one lemma
+
+The `Lean.SimpLC.Exceptions` module sets up `allow` and `ignore` commands for the core Lean repository.
+
+You can check that the simp set for built-in types is still confluent in a downstream library using
+```lean
+import Lean.SimpLC.Exceptions
+
+#guard_msgs (drop info) in
+simp_lc check in String Char Float USize UInt64 UInt32 UInt16 UInt8 PLift ULift Prod Sum Range
+  Subtype ByteArray FloatArray List Option Array Int Nat Bool Id
+  Monad LawfulFunctor LawfulApplicative LawfulMonad LawfulSingleton Std
+```
+(optionally adding `_root_`).
+
+You can also add specific namespaces for your project, or even run `simp_lc check` to check all simp lemmas.
+

src/Lean/SimpLC/Setup.lean

@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+module
+
+prelude
+public import Lean.Util.Trace
+
+public section
+
+open Lean
+
+namespace Lean.SimpLC
+
+abbrev NamePair := Name × Name
+
+initialize simpLCAllowExt : SimplePersistentEnvExtension NamePair (Array NamePair) ←
+  registerSimplePersistentEnvExtension {
+    addEntryFn := Array.push
+    addImportedFn := Array.flatMap id
+  }
+
+def isCriticalPairAllowed {m : Type → Type} [Monad m] [MonadEnv m] (pair : NamePair) : m Bool := do
+  let pair := match pair with | (x,y) => if y.quickLt x then (y,x) else (x,y)
+  return simpLCAllowExt.getState (← getEnv) |>.contains pair
+
+
+initialize simpLCIgnoreExt : SimplePersistentEnvExtension Name (Array Name) ←
+  registerSimplePersistentEnvExtension {
+    addEntryFn := Array.push
+    addImportedFn := Array.flatMap id
+  }
+
+def ignoreName {m : Type → Type} [Monad m] [MonadEnv m] (n : Name) : m Unit := do
+  modifyEnv (simpLCIgnoreExt.addEntry · n)
+
+def isIgnoredName {m : Type → Type} [Monad m] [MonadEnv m] (n : Name) : m Bool := do
+  return simpLCIgnoreExt.getState (← getEnv) |>.contains n
+
+initialize
+  Lean.registerTraceClass `simplc
+
+register_option simplc.stderr : Bool := {
+  defValue := false
+  descr := "Print steps to stderr (useful when it crashes)"
+}
+
+register_option simplc.checkAllow : Bool := {
+  defValue := true
+  descr := "`simp_lc allow` to warn if the pair is actually ok"
+}
+
+end Lean.SimpLC
+
+end -- public section

tests/lean/000_simplc.lean

@@ -0,0 +1,24 @@
+import Lean.SimpLC.Exceptions
+
+/-!
+# simp local confluence testing
+
+If you experience failures here, take the suggested `simp_lc inspect ...` commands
+and paste them into a relevant `Lean.SimpLC.Exceptions.ABC` file.
+
+Then decide whether to:
+* Remove a `@[simp]` annotation
+* Add a new `@[simp]` lemma to restore confluence
+* Add a new `simp_lc allow` directive to suppress warnings about a given non-confluent pair.
+  Ideally add an `example` immediately before it demonstrating the non-confluence.
+* Add a new `simp_lc ignore` directive to suppress all warnings about a given lemma.
+  Ideally add a doc-comment justifying why this is reasonable.
+
+
+This file is intentionally named `000_simplc.lean` to starting running as early as possible in CI.
+-/
+
+-- Warning: this takes about 3 minutes to run!
+set_option maxHeartbeats 0 in
+#guard_msgs (drop info) in
+simp_lc check

tests/lean/simplc_not_imported.lean

@@ -0,0 +1,6 @@
+import Lean
+
+/-
+This should fail unless `Lean.SimpLC` is explicitly imported.
+-/
+simplc_check

tests/lean/simplc_not_imported.lean.expected.out

@@ -0,0 +1 @@
+simplc_not_imported.lean:6:0-6:12: error: unexpected identifier; expected command

tests/simplc/.gitignore

@@ -0,0 +1 @@
+/.lake