feat: fine-grained equational lemmas for non-recursive functions (#4154)

This is part of #3983.

Fine-grained equational lemmas are useful even for non-recursive
functions, so this adds them.

The new option `eqns.nonrecursive` can be set to `false` to have the old
behavior.

### Breaking channge

This is a breaking change: Previously, `rw [Option.map]` would rewrite
`Option.map f o` to `match o with … `. Now this rewrite will fail
because the equational lemmas require constructors here (like they do
for, say, `List.map`).

Remedies:

 * Split on `o` before rewriting.
* Use `rw [Option.map.eq_def]`, which rewrites any (saturated)
application of `Option.map`
* Use `set_option eqns.nonrecursive false` when *defining* the function
in question.

### Interaction with simp

The `simp` tactic so far had a special provision for non-recursive
functions so that `simp [f]` will try to use the equational lemmas, but
will also unfold `f` else, so less breakage here (but maybe performance
improvements with functions with many cases when applied to a
constructor, as the simplifier will no longer unfold to a large
`match`-statement and then collapse it right away).

For projection functions and functions marked `[reducible]`, `simp [f]`
won’t use the equational theorems, and will only use its internal
unfolding machinery.

### Implementation notes

It uses the same `mkEqnTypes` function as for recursive functions, so we
are close to a consistency here. There is still the wrinkle that for
recursive functions we don't split matches without an interesting
recursive call inside. Unifying that is future work.

src/Init/Data/Int/Order.lean

@@ -1006,7 +1006,7 @@ theorem natAbs_mul_self : ∀ {a : Int}, ↑(natAbs a * natAbs a) = a * a
 theorem eq_nat_or_neg (a : Int) : ∃ n : Nat, a = n ∨ a = -↑n := ⟨_, natAbs_eq a⟩
 
 theorem natAbs_mul_natAbs_eq {a b : Int} {c : Nat}
-    (h : a * b = (c : Int)) : a.natAbs * b.natAbs = c := by rw [← natAbs_mul, h, natAbs]
+    (h : a * b = (c : Int)) : a.natAbs * b.natAbs = c := by rw [← natAbs_mul, h, natAbs.eq_def]
 
 @[simp] theorem natAbs_mul_self' (a : Int) : (natAbs a * natAbs a : Int) = a * a := by
   rw [← Int.ofNat_mul, natAbs_mul_self]

src/Init/Omega/Int.lean

@@ -116,7 +116,7 @@ theorem ofNat_max (a b : Nat) : ((max a b : Nat) : Int) = max (a : Int) (b : Int
   split <;> rfl
 
 theorem ofNat_natAbs (a : Int) : (a.natAbs : Int) = if 0 ≤ a then a else -a := by
-  rw [Int.natAbs]
+  rw [Int.natAbs.eq_def]
   split <;> rename_i n
   · simp only [Int.ofNat_eq_coe]
     rw [if_pos (Int.ofNat_nonneg n)]

src/Init/Tactics.lean

@@ -552,9 +552,9 @@ The `simp` tactic uses lemmas and hypotheses to simplify the main goal target or
 non-dependent hypotheses. It has many variants:
 - `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.
 - `simp [h₁, h₂, ..., hₙ]` simplifies the main goal target using the lemmas tagged
-  with the attribute `[simp]` and the given `hᵢ`'s, where the `hᵢ`'s are expressions.
-  If an `hᵢ` is a defined constant `f`, then the equational lemmas associated with
-  `f` are used. This provides a convenient way to unfold `f`.
+  with the attribute `[simp]` and the given `hᵢ`'s, where the `hᵢ`'s are expressions.-
+- If an `hᵢ` is a defined constant `f`, then `f` is unfolded. If `f` has equational lemmas associated
+  with it (and is not a projection or a `reducible` definition), these are used to rewrite with `f`.
 - `simp [*]` simplifies the main goal target using the lemmas tagged with the
   attribute `[simp]` and all hypotheses.
 - `simp only [h₁, h₂, ..., hₙ]` is like `simp [h₁, h₂, ..., hₙ]` but does not use `[simp]` lemmas.

src/Lean/Elab/PreDefinition.lean

@@ -10,3 +10,4 @@ import Lean.Elab.PreDefinition.Main
 import Lean.Elab.PreDefinition.MkInhabitant
 import Lean.Elab.PreDefinition.WF
 import Lean.Elab.PreDefinition.Eqns
+import Lean.Elab.PreDefinition.Nonrec.Eqns

src/Lean/Elab/PreDefinition/Basic.lean

@@ -12,6 +12,7 @@ import Lean.Util.NumApps
 import Lean.PrettyPrinter
 import Lean.Meta.AbstractNestedProofs
 import Lean.Meta.ForEachExpr
+import Lean.Meta.Eqns
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.DefView
 import Lean.Elab.PreDefinition.TerminationHint
@@ -153,6 +154,7 @@ private def addNonRecAux (preDef : PreDefinition) (compile : Bool) (all : List N
     if compile && shouldGenCodeFor preDef then
       discard <| compileDecl decl
     if applyAttrAfterCompilation then
+      generateEagerEqns preDef.declName
       applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
 
 def addAndCompileNonRec (preDef : PreDefinition) (all : List Name := [preDef.declName]) : TermElabM Unit := do

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -75,7 +75,12 @@ private def findMatchToSplit? (env : Environment) (e : Expr) (declNames : Array
           break
       unless hasFVarDiscr do
         return Expr.FindStep.visit
-      -- At least one alternative must contain a `declNames` application with loose bound variables.
+      -- For non-recursive functions (`declNames` empty), we split here
+      if declNames.isEmpty then
+          return Expr.FindStep.found
+      -- For recursive functions we only split when at least one alternatives contains a `declNames`
+      -- application with loose bound variables.
+      -- (We plan to disable this by default and treat recursive and non-recursie functions the same)
       for i in [info.getFirstAltPos : info.getFirstAltPos + info.numAlts] do
         let alt := args[i]!
         if Option.isSome <| alt.find? fun e => declNames.any e.isAppOf && e.hasLooseBVars then

src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean

@@ -0,0 +1,108 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Joachim Breitner
+-/
+prelude
+import Lean.Meta.Tactic.Rewrite
+import Lean.Meta.Tactic.Split
+import Lean.Elab.PreDefinition.Basic
+import Lean.Elab.PreDefinition.Eqns
+import Lean.Meta.ArgsPacker.Basic
+import Init.Data.Array.Basic
+
+namespace Lean.Elab.Nonrec
+open Meta
+open Eqns
+
+/--
+Simple, coarse-grained equation theorem for nonrecursive definitions.
+-/
+private def mkSimpleEqThm (declName : Name) (suffix := Name.mkSimple unfoldThmSuffix) : MetaM (Option Name) := do
+  if let some (.defnInfo info) := (← getEnv).find? declName then
+    lambdaTelescope (cleanupAnnotations := true) info.value fun xs body => do
+      let lhs := mkAppN (mkConst info.name <| info.levelParams.map mkLevelParam) xs
+      let type  ← mkForallFVars xs (← mkEq lhs body)
+      let value ← mkLambdaFVars xs (← mkEqRefl lhs)
+      let name := declName ++ suffix
+      addDecl <| Declaration.thmDecl {
+        name, type, value
+        levelParams := info.levelParams
+      }
+      return some name
+  else
+    return none
+
+private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
+  trace[Elab.definition.eqns] "proving: {type}"
+  withNewMCtxDepth do
+    let main ← mkFreshExprSyntheticOpaqueMVar type
+    let (_, mvarId) ← main.mvarId!.intros
+    let rec go (mvarId : MVarId) : MetaM Unit := do
+      trace[Elab.definition.eqns] "step\n{MessageData.ofGoal mvarId}"
+      if ← withAtLeastTransparency .all (tryURefl mvarId) then
+        return ()
+      else if (← tryContradiction mvarId) then
+        return ()
+      else if let some mvarId ← simpMatch? mvarId then
+        go mvarId
+      else if let some mvarId ← simpIf? mvarId then
+        go mvarId
+      else if let some mvarId ← whnfReducibleLHS? mvarId then
+        go mvarId
+      else match (← simpTargetStar mvarId { config.dsimp := false } (simprocs := {})).1 with
+        | TacticResultCNM.closed => return ()
+        | TacticResultCNM.modified mvarId => go mvarId
+        | TacticResultCNM.noChange =>
+          if let some mvarIds ← casesOnStuckLHS? mvarId then
+            mvarIds.forM go
+          else if let some mvarIds ← splitTarget? mvarId then
+            mvarIds.forM go
+          else
+            throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}"
+
+    -- Try rfl before deltaLHS to avoid `id` checkpoints in the proof, which would make
+    -- the lemma ineligible for dsimp
+    unless ← withAtLeastTransparency .all (tryURefl mvarId) do
+      go (← deltaLHS mvarId)
+    instantiateMVars main
+
+def mkEqns (declName : Name) (info : DefinitionVal) : MetaM (Array Name) :=
+  withOptions (tactic.hygienic.set · false) do
+  let baseName := declName
+  let eqnTypes ← withNewMCtxDepth <| lambdaTelescope (cleanupAnnotations := true) info.value fun xs body => do
+    let us := info.levelParams.map mkLevelParam
+    let target ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
+    let goal ← mkFreshExprSyntheticOpaqueMVar target
+    withReducible do
+      mkEqnTypes #[] goal.mvarId!
+  let mut thmNames := #[]
+  for i in [: eqnTypes.size] do
+    let type := eqnTypes[i]!
+    trace[Elab.definition.eqns] "eqnType[{i}]: {eqnTypes[i]!}"
+    let name := (Name.str baseName eqnThmSuffixBase).appendIndexAfter (i+1)
+    thmNames := thmNames.push name
+    let value ← mkProof declName type
+    let (type, value) ← removeUnusedEqnHypotheses type value
+    addDecl <| Declaration.thmDecl {
+      name, type, value
+      levelParams := info.levelParams
+    }
+  return thmNames
+
+def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
+  if (← isRecursiveDefinition declName) then
+    return none
+  if let some (.defnInfo info) := (← getEnv).find? declName then
+    if eqns.nonrecursive.get (← getOptions) then
+      mkEqns declName info
+    else
+      let o ← mkSimpleEqThm declName
+      return o.map (#[·])
+  else
+    return none
+
+builtin_initialize
+  registerGetEqnsFn getEqnsFor?
+
+end Lean.Elab.Nonrec

src/Lean/Elab/PreDefinition/Structural/Main.lean

@@ -193,6 +193,7 @@ def structuralRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Opti
         registerEqnsInfo preDef (preDefs.map (·.declName)) recArgPos numFixed
     addSmartUnfoldingDef preDef recArgPos
     markAsRecursive preDef.declName
+    generateEagerEqns preDef.declName
   applyAttributesOf preDefsNonRec AttributeApplicationTime.afterCompilation
 
 

src/Lean/Elab/PreDefinition/WF/Main.lean

@@ -145,6 +145,7 @@ def wfRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Option Termi
   registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize argsPacker
   for preDef in preDefs do
     markAsRecursive preDef.declName
+    generateEagerEqns preDef.declName
     applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
     -- Unless the user asks for something else, mark the definition as irreducible
     unless preDef.modifiers.attrs.any fun a =>

src/Lean/Elab/Print.lean

@@ -134,7 +134,7 @@ private def printAxiomsOf (constName : Name) : CommandElabM Unit := do
   | _ => throwUnsupportedSyntax
 
 private def printEqnsOf (constName : Name) : CommandElabM Unit := do
-  let some eqns ← liftTermElabM <| Meta.getEqnsFor? constName (nonRec := true) |
+  let some eqns ← liftTermElabM <| Meta.getEqnsFor? constName |
     logInfo m!"'{constName}' does not have equations"
   let mut m := m!"equations:"
   for eq in eqns do

src/Lean/Elab/Tactic/Rewrite.lean

@@ -52,9 +52,11 @@ def withRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool)
           else
             -- Try to get equation theorems for `id`.
             let declName ← try realizeGlobalConstNoOverload id catch _ => return (← x symm term)
-            let some eqThms ← getEqnsFor? declName (nonRec := true) | x symm term
+            let some eqThms ← getEqnsFor? declName | x symm term
+            let hint := if eqThms.size = 1 then m!"" else
+              m!" Try rewriting with '{Name.str declName unfoldThmSuffix}'."
             let rec go : List Name →  TacticM Unit
-              | [] => throwError "failed to rewrite using equation theorems for '{declName}'"
+              | [] => throwError "failed to rewrite using equation theorems for '{declName}'.{hint}"
               -- Remark: we prefix `eqThm` with `_root_` to ensure it is resolved correctly.
               -- See test: `rwPrioritizesLCtxOverEnv.lean`
               | eqThm::eqThms => (x symm (mkIdentFrom id (`_root_ ++ eqThm))) <|> go eqThms

src/Lean/Meta/Eqns.lean

@@ -11,6 +11,23 @@ import Lean.Meta.AppBuilder
 import Lean.Meta.Match.MatcherInfo
 
 namespace Lean.Meta
+
+register_builtin_option eqns.nonrecursive : Bool := {
+    defValue := true
+    descr    := "Create fine-grained equational lemmas even for non-recursive definitions."
+  }
+
+
+/--
+These options affect the generation of equational theorems in a significant way. For these, their
+value at definition time, not realization time, should matter.
+
+This is implemented by
+ * eagerly realizing the equations when they are set to a non-default vaule
+ * when realizing them lazily, reset the options to their default
+-/
+def eqnAffectingOptions : Array (Lean.Option Bool) := #[eqns.nonrecursive]
+
 /--
 Environment extension for storing which declarations are recursive.
 This information is populated by the `PreDefinition` module, but the simplifier
@@ -105,7 +122,8 @@ def registerGetEqnsFn (f : GetEqnsFn) : IO Unit := do
 /-- Returns `true` iff `declName` is a definition and its type is not a proposition. -/
 private def shouldGenerateEqnThms (declName : Name) : MetaM Bool := do
   if let some (.defnInfo info) := (← getEnv).find? declName then
-    return !(← isProp info.type)
+    if (← isProp info.type) then return false
+    return true
   else
     return false
 
@@ -170,12 +188,7 @@ private partial def alreadyGenerated? (declName : Name) : MetaM (Option (Array N
   else
     return none
 
-/--
-Returns equation theorems for the given declaration.
-By default, we do not create equation theorems for nonrecursive definitions.
-You can use `nonRec := true` to override this behavior, a dummy `rfl` proof is created on the fly.
--/
-def getEqnsFor? (declName : Name) (nonRec := false) : MetaM (Option (Array Name)) := withLCtx {} {} do
+private def getEqnsFor?Core (declName : Name) : MetaM (Option (Array Name)) := withLCtx {} {} do
   if let some eqs := eqnsExt.getState (← getEnv) |>.map.find? declName then
     return some eqs
   else if let some eqs ← alreadyGenerated? declName then
@@ -185,13 +198,25 @@ def getEqnsFor? (declName : Name) (nonRec := false) : MetaM (Option (Array Name)
       if let some r ← f declName then
         registerEqnThms declName r
         return some r
-    if nonRec then
-      let some eqThm ← mkSimpleEqThm declName (suffix := Name.mkSimple eqn1ThmSuffix) | return none
-      let r := #[eqThm]
-      registerEqnThms declName r
-      return some r
   return none
 
+/--
+Returns equation theorems for the given declaration.
+-/
+def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := withLCtx {} {} do
+  -- This is the entry point for lazy equaion generation. Ignore the current value
+  -- of the options, and revert to the default.
+  withOptions (eqnAffectingOptions.foldl fun os o => o.set os o.defValue) do
+    getEqnsFor?Core declName
+
+/--
+If any equation theorem affecting option is not the default value, create the equations now.
+-/
+def generateEagerEqns (declName : Name) : MetaM Unit := do
+  let opts ← getOptions
+  if eqnAffectingOptions.any fun o => o.get opts != o.defValue then
+    let _ ← getEqnsFor?Core declName
+
 def GetUnfoldEqnFn := Name → MetaM (Option Name)
 
 private builtin_initialize getUnfoldEqnFnsRef : IO.Ref (List GetUnfoldEqnFn) ← IO.mkRef []
@@ -251,7 +276,7 @@ builtin_initialize
     let .str p s := name | return false
     unless (← getEnv).isSafeDefinition p do return false
     if isEqnReservedNameSuffix s then
-      return (← MetaM.run' <| getEqnsFor? p (nonRec := true)).isSome
+      return (← MetaM.run' <| getEqnsFor? p).isSome
     if isUnfoldReservedNameSuffix s then
       return (← MetaM.run' <| getUnfoldEqnFor? p (nonRec := true)).isSome
     return false

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

@@ -30,11 +30,13 @@ def mkSimpAttr (attrName : Name) (attrDescr : String) (ext : SimpExtension)
           if (← isProp info.type) then
             addSimpTheorem ext declName post (inv := false) attrKind prio
           else if info.hasValue then
-            if let some eqns ← getEqnsFor? declName then
+            if (← SimpTheorems.ignoreEquations declName) then
+              ext.add (SimpEntry.toUnfold declName) attrKind
+            else if let some eqns ← getEqnsFor? declName then
               for eqn in eqns do
                 addSimpTheorem ext eqn post (inv := false) attrKind prio
               ext.add (SimpEntry.toUnfoldThms declName eqns) attrKind
-              if hasSmartUnfoldingDecl (← getEnv) declName then
+              if (← SimpTheorems.unfoldEvenWithEqns declName) then
                 ext.add (SimpEntry.toUnfold declName) attrKind
             else
               ext.add (SimpEntry.toUnfold declName) attrKind

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

@@ -463,8 +463,38 @@ def SimpTheorems.add (s : SimpTheorems) (id : Origin) (levelParams : Array Name)
     let simpThms ← mkSimpTheorems id levelParams proof post inv prio
     return simpThms.foldl addSimpTheoremEntry s
 
+/--
+Reducible functions and projection functions should always be put in `toUnfold`, instead
+of trying to use equational theorems.
+
+The simplifiers has special support for structure and class projections, and gets
+confused when they suddenly rewrite, so ignore equations for them
+-/
+def SimpTheorems.ignoreEquations (declName : Name) : CoreM Bool := do
+  return (← isProjectionFn declName) || (← isReducible declName)
+
+/--
+Even if a function has equation theorems,
+we also store it in the `toUnfold` set in the following two cases:
+1- It was defined by structural recursion and has a smart-unfolding associated declaration.
+2- It is non-recursive.
+
+Reason: `unfoldPartialApp := true` or conditional equations may not apply.
+
+Remark: In the future, we are planning to disable this
+behavior unless `unfoldPartialApp := true`.
+Moreover, users will have to use `f.eq_def` if they want to force the definition to be
+unfolded.
+-/
+def SimpTheorems.unfoldEvenWithEqns (declName : Name) : CoreM Bool := do
+  if hasSmartUnfoldingDecl (← getEnv) declName then return true
+  unless (← isRecursiveDefinition declName) do return true
+  return false
+
 def SimpTheorems.addDeclToUnfold (d : SimpTheorems) (declName : Name) : MetaM SimpTheorems := do
-  if let some eqns ← getEqnsFor? declName then
+  if (← ignoreEquations declName) then
+    return d.addDeclToUnfoldCore declName
+  else if let some eqns ← getEqnsFor? declName then
     let mut d := d
     for h : i in [:eqns.size] do
       let eqn := eqns[i]
@@ -484,20 +514,7 @@ def SimpTheorems.addDeclToUnfold (d : SimpTheorems) (declName : Name) : MetaM Si
       else
         100 - i
       d ← SimpTheorems.addConst d eqn (prio := prio)
-    /-
-    Even if a function has equation theorems,
-    we also store it in the `toUnfold` set in the following two cases:
-    1- It was defined by structural recursion and has a smart-unfolding associated declaration.
-    2- It is non-recursive.
-
-    Reason: `unfoldPartialApp := true` or conditional equations may not apply.
-
-    Remark: In the future, we are planning to disable this
-    behavior unless `unfoldPartialApp := true`.
-    Moreover, users will have to use `f.eq_def` if they want to force the definition to be
-    unfolded.
-    -/
-    if hasSmartUnfoldingDecl (← getEnv) declName || !(← isRecursiveDefinition declName) then
+    if (← unfoldEvenWithEqns declName) then
       d := d.addDeclToUnfoldCore declName
     return d
   else

src/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean

@@ -122,15 +122,11 @@ def hasAssignment (b : Bool) : Assignment → Bool :=
 
 theorem removePos_addPos_cancel {assignment : Assignment} (h : ¬(hasPosAssignment assignment)) :
   removePosAssignment (addPosAssignment assignment) = assignment := by
-  rw [removePosAssignment, addPosAssignment]
-  rw [hasPosAssignment] at h
-  cases assignment <;> simp_all
+  cases assignment <;> simp_all [removePosAssignment, addPosAssignment, hasPosAssignment]
 
 theorem removeNeg_addNeg_cancel {assignment : Assignment} (h : ¬(hasNegAssignment assignment)) :
   removeNegAssignment (addNegAssignment assignment) = assignment := by
-  rw [removeNegAssignment, addNegAssignment]
-  rw [hasNegAssignment] at h
-  cases assignment <;> simp_all
+  cases assignment <;> simp_all [removeNegAssignment, addNegAssignment, hasNegAssignment]
 
 theorem remove_add_cancel {assignment : Assignment} {b : Bool} (h : ¬(hasAssignment b assignment)) :
   removeAssignment b (addAssignment b assignment) = assignment := by
@@ -152,30 +148,21 @@ theorem has_both (b : Bool) : hasAssignment b both = true := by
 
 theorem has_add (assignment : Assignment) (b : Bool) :
     hasAssignment b (addAssignment b assignment) := by
-  rw [addAssignment, hasAssignment]
-  split
-  · rw [hasPosAssignment, addPosAssignment]
-    cases assignment <;> simp
-  · rw [hasNegAssignment, addNegAssignment]
-    cases assignment <;> simp
+  by_cases b <;> cases assignment <;> simp_all [hasAssignment, hasPosAssignment, addAssignment,
+    addPosAssignment, addNegAssignment, hasNegAssignment]
 
 theorem not_hasPos_removePos (assignment : Assignment) :
     ¬hasPosAssignment (removePosAssignment assignment) := by
-  simp only [removePosAssignment, hasPosAssignment, Bool.not_eq_true]
-  cases assignment <;> simp
+  cases assignment <;> simp [removePosAssignment, hasPosAssignment]
 
 theorem not_hasNeg_removeNeg (assignment : Assignment) :
     ¬hasNegAssignment (removeNegAssignment assignment) := by
-  simp only [removeNegAssignment, hasNegAssignment, Bool.not_eq_true]
-  cases assignment <;> simp
+  cases assignment <;> simp [removeNegAssignment, hasNegAssignment]
 
 theorem not_has_remove (assignment : Assignment) (b : Bool) :
     ¬hasAssignment b (removeAssignment b assignment) := by
-  by_cases hb : b
-  · have h := not_hasPos_removePos assignment
-    simp [hb, h, removeAssignment, hasAssignment]
-  · have h := not_hasNeg_removeNeg assignment
-    simp [hb, h, removeAssignment, hasAssignment]
+  by_cases b <;> cases assignment <;> simp_all [hasAssignment, removeAssignment,
+    removePosAssignment, hasPosAssignment, removeNegAssignment, hasNegAssignment]
 
 theorem has_remove_irrelevant (assignment : Assignment) (b : Bool) :
     hasAssignment b (removeAssignment (!b) assignment) → hasAssignment b assignment := by
@@ -194,13 +181,11 @@ theorem unassigned_of_has_neither (assignment : Assignment) (lacks_pos : ¬(hasP
 
 theorem hasPos_addNeg (assignment : Assignment) :
     hasPosAssignment (addNegAssignment assignment) = hasPosAssignment assignment := by
-  rw [hasPosAssignment, addNegAssignment]
-  cases assignment <;> simp (config := { decide := true })
+  cases assignment <;> simp [hasPosAssignment, addNegAssignment]
 
 theorem hasNeg_addPos (assignment : Assignment) :
     hasNegAssignment (addPosAssignment assignment) = hasNegAssignment assignment := by
-  rw [hasNegAssignment, addPosAssignment]
-  cases assignment <;> simp (config := { decide := true })
+  cases assignment <;> simp [hasNegAssignment, addPosAssignment]
 
 theorem has_iff_has_add_complement (assignment : Assignment) (b : Bool) :
     hasAssignment b assignment ↔ hasAssignment b (addAssignment (¬b) assignment) := by
@@ -208,13 +193,11 @@ theorem has_iff_has_add_complement (assignment : Assignment) (b : Bool) :
 
 theorem addPos_addNeg_eq_both (assignment : Assignment) :
     addPosAssignment (addNegAssignment assignment) = both := by
-  rw [addPosAssignment, addNegAssignment]
-  cases assignment <;> simp
+  cases assignment <;> simp [addPosAssignment, addNegAssignment]
 
 theorem addNeg_addPos_eq_both (assignment : Assignment) :
     addNegAssignment (addPosAssignment assignment) = both := by
-  rw [addNegAssignment, addPosAssignment]
-  cases assignment <;> simp
+  cases assignment <;> simp [addNegAssignment, addPosAssignment]
 
 instance {n : Nat} : Entails (PosFin n) (Array Assignment) where
   eval := fun p arr => ∀ i : PosFin n, ¬(hasAssignment (¬p i) arr[i.1]!)

src/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean

@@ -21,11 +21,11 @@ theorem sat_negate_iff_not_sat {p : α → Bool} {l : Literal α} : p ⊨ Litera
   simp only [Literal.negate, sat_iff]
   constructor
   · intro h pl
-    rw [sat_iff, h, not] at pl
+    rw [sat_iff, h, not.eq_def] at pl
     split at pl <;> simp_all
   · intro h
     rw [sat_iff] at h
-    rw [not]
+    rw [not.eq_def]
     split <;> simp_all
 
 theorem unsat_of_limplies_complement [Entails α t] (x : t) (l : Literal α) :
@@ -131,4 +131,3 @@ end Formula
 end Internal
 end LRAT
 end Std.Tactic.BVDecide
-

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

@@ -96,7 +96,7 @@ theorem ratUnits_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) :
 theorem size_ofArray_fold_fn {n : Nat} (assignments : Array Assignment)
     (cOpt : Option (DefaultClause n)) :
     (ofArray_fold_fn assignments cOpt).size = assignments.size := by
-  rw [ofArray_fold_fn]
+  rw [ofArray_fold_fn.eq_def]
   split
   · rfl
   · split <;> simp [Array.size_modify]
@@ -376,7 +376,7 @@ theorem mem_of_insertRupUnits {n : Nat} (f : DefaultFormula n) (units : CNF.Clau
     (unit : Literal (PosFin n)) (unit_in_units : unit ∈ units) :
     ∀ l : Literal (PosFin n), l ∈ (insertUnit acc unit).1.data → (l ∈ f.rupUnits.data ∨ l ∈ units) := by
     intro l hl
-    rw [insertUnit] at hl
+    rw [insertUnit.eq_def] at hl
     dsimp at hl
     split at hl
     · exact ih l hl
@@ -413,7 +413,7 @@ theorem mem_of_insertRatUnits {n : Nat} (f : DefaultFormula n) (units : CNF.Clau
     (unit : Literal (PosFin n)) (unit_in_units : unit ∈ units) :
     ∀ l : Literal (PosFin n), l ∈ (insertUnit acc unit).1.data → (l ∈ f.ratUnits.data ∨ l ∈ units) := by
     intro l hl
-    rw [insertUnit] at hl
+    rw [insertUnit.eq_def] at hl
     dsimp at hl
     split at hl
     · exact ih l hl

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

@@ -426,18 +426,15 @@ theorem c_without_negPivot_of_performRatCheck_success {n : Nat} (f : DefaultForm
   simp only [performRatCheck, hc, Bool.or_eq_true, Bool.not_eq_true'] at performRatCheck_success
   split at performRatCheck_success
   · next h =>
-    exact sat_of_insertRat f hf (DefaultClause.delete c negPivot) p pf h
+    exact sat_of_insertRat f hf (c.delete negPivot) p pf h
   · split at performRatCheck_success
     · exact False.elim performRatCheck_success
     · next h =>
       simp only [not_or, Bool.not_eq_true, Bool.not_eq_false] at h
-      have pfc := safe_insert_of_performRupCheck_insertRat f hf (DefaultClause.delete c negPivot) ratHint.2 h.2 p pf
-      simp only [( · ⊨ ·), Clause.eval, List.any_eq_true, Prod.exists, Bool.exists_bool,
-        Bool.decide_coe, List.all_eq_true] at pfc
-      have c_negPivot_in_fc : (DefaultClause.delete c negPivot) ∈ toList (insert f (DefaultClause.delete c negPivot)) := by
-        rw [insert_iff]
-        exact Or.inl rfl
-      exact of_decide_eq_true <| pfc (DefaultClause.delete c negPivot) c_negPivot_in_fc
+      have pfc : p ⊨ f.insert (c.delete negPivot) :=
+        safe_insert_of_performRupCheck_insertRat f hf (c.delete negPivot) ratHint.2 h.2 p pf
+      rw [DefaultFormula.formulaEntails_def, List.all_eq_true] at pfc
+      exact of_decide_eq_true (pfc (c.delete negPivot) (by simp [insert_iff]))
 
 theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n)
     (f_readyForRatAdd : ReadyForRatAdd f) (pivot : Literal (PosFin n))
@@ -569,8 +566,7 @@ theorem safe_insert_of_performRatCheck_fold_success {n : Nat} (f : DefaultFormul
       · rw [← c'_eq_c] at p'_entails_c
         exact p'_not_entails_c' p'_entails_c
       · have pc' : p ⊨ c' := by
-          simp only [(· ⊨ ·), Clause.eval, List.any_eq_true, Prod.exists, Bool.exists_bool,
-            Bool.decide_coe, List.all_eq_true] at pf
+          rw [DefaultFormula.formulaEntails_def, List.all_eq_true] at pf
           exact of_decide_eq_true <| pf c' c'_in_f
         have negPivot_in_c' : Literal.negate pivot ∈ Clause.toList c' := mem_of_necessary_assignment pc' p'_not_entails_c'
         have h : p ⊨ (c'.delete (Literal.negate pivot)) := by

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

@@ -369,7 +369,7 @@ theorem unsat_of_encounteredBoth {n : Nat} (c : DefaultClause n)
     (l : Literal (PosFin n)) (_ : l ∈ c.clause) :
     (reduce_fold_fn assignment res l) = encounteredBoth → Unsatisfiable (PosFin n) assignment := by
     intro h
-    rw [reduce_fold_fn] at h
+    rw [reduce_fold_fn.eq_def] at h
     split at h
     · exact ih rfl
     · split at h
@@ -408,7 +408,7 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi
   simp only [ReducePostconditionInductionMotive, Fin.getElem_fin, forall_exists_index, and_imp, Prod.forall]
   constructor
   · intro h p
-    rw [reduce_fold_fn] at h
+    rw [reduce_fold_fn.eq_def] at h
     split at h
     · simp only at h
     · split at h
@@ -460,7 +460,7 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi
       · simp only at h
     · simp only at h
   · intro i b h p hp j j_lt_idx_add_one p_entails_c_arr_j
-    rw [reduce_fold_fn] at h
+    rw [reduce_fold_fn.eq_def] at h
     split at h
     · simp only at h
     · split at h
@@ -831,4 +831,3 @@ end DefaultFormula
 end Internal
 end LRAT
 end Std.Tactic.BVDecide
-

tests/lean/run/946.lean

@@ -38,6 +38,9 @@ namespace DataEntry
   | NULL,      _       => True
   | _,         _       => False
 
+-- Needed since the introduction of the fine-grained lemmas
+@[simp] theorem isOf_lit (n : Nat) : isOf (no_index (OfNat.ofNat n)) TInt = True := rfl
+
 end DataEntry
 
 abbrev Header := List (DataType × String)

tests/lean/run/bv_math_lit_perf.lean

@@ -16,7 +16,12 @@ def f (x : BitVec 32) : Nat :=
   | 920#32 => 12
   | _      => 1000
 
-set_option maxHeartbeats 3000
+-- Generate the equational lemmas ahead of time, to avoid going
+-- over the hearbeat limit below
+#guard_msgs(drop all) in
+#print equations f
+
+set_option maxHeartbeats 300
 example : f 500#32 = x := by
   simp [f]
   sorry

tests/lean/run/constProp.lean

@@ -338,7 +338,9 @@ instance : Repr State where
   | e => e
 
 @[simp] theorem Expr.eval_simplify (e : Expr) : e.simplify.eval σ = e.eval σ := by
-  induction e with simp
+  induction e with
+    -- Due to fine-grained equational theorems we have to pass `eq_def` lemmas here
+    simp only [simplify, BinOp.simplify.eq_def, eval, UnaryOp.simplify.eq_def]
   | bin lhs op rhs ih_lhs ih_rhs =>
     simp [← ih_lhs, ← ih_rhs]
     split <;> simp [*]

tests/lean/run/dsimp1.lean

@@ -1,29 +1,38 @@
 def Nat.isZero (x : Nat) : Bool :=
   match x with
   | 0 => true
-  | x+1 => false
+  | _+1 => false
+
+axiom P : Bool → Prop
+axiom P_false : P false
 
 /--
 info: x : Nat
-⊢ (1 + x).isZero = false
+⊢ P (1 + x).isZero
 -/
 #guard_msgs in
-example (x : Nat) : (1 + id x.succ.pred).isZero = false := by
+example (x : Nat) : P (1 + id x.succ.pred).isZero := by
   dsimp
   trace_state
   simp [Nat.succ_add]
   dsimp [Nat.isZero]
+  apply P_false
 
-#check Nat.pred_succ
-
-example (x : Nat) : (id x.succ.succ).isZero = false := by
+example (x : Nat) : P (id x.succ.succ).isZero := by
   dsimp [Nat.isZero]
+  apply P_false
 
-example (x : Nat) : (id x.succ.succ).isZero = false := by
+example (x : Nat) : P (id x.succ.succ).isZero := by
+  dsimp [Nat.isZero.eq_2]
+  apply P_false
+
+example (x : Nat) : P (id x.succ.succ).isZero := by
   dsimp!
+  apply P_false
 
 @[simp] theorem isZero_succ (x : Nat) : (x + 1).isZero = false :=
   rfl
 
-theorem ex1 (x : Nat) : (id x.succ.succ.pred).isZero = false := by
+theorem ex1 (x : Nat) : P (id x.succ.succ.pred).isZero  := by
   dsimp
+  apply P_false

tests/lean/run/dsimp2.lean

@@ -0,0 +1,8 @@
+@[reducible, simp]
+def eval {β : α → Sort _} (x : α) (f : ∀ x, β x) : β x := f x
+
+-- For this to work, the above `simp` has to add `eval` also to the decls-to-unfold,
+-- as the `eval.eq_1` is not helpful, as `eval` is reducible
+theorem test [LE β] (x : α) (f : α → β) (P : β → Prop) (h : P (f x)) : P (eval x f) := by
+  dsimp
+  apply h

tests/lean/run/eqnOptions.lean

@@ -0,0 +1,55 @@
+/-! Tests that options affecting equational theorems work as expected. -/
+
+namespace Test1
+def nonrecfun : Bool → Nat
+  | false => 0
+  | true => 0
+
+/--
+info: equations:
+theorem Test1.nonrecfun.eq_1 : nonrecfun false = 0
+theorem Test1.nonrecfun.eq_2 : nonrecfun true = 0
+-/
+#guard_msgs in
+#print equations nonrecfun
+
+end Test1
+
+namespace Test2
+
+set_option eqns.nonrecursive false in
+def nonrecfun : Bool → Nat
+  | false => 0
+  | true => 0
+
+/--
+info: equations:
+theorem Test2.nonrecfun.eq_def : ∀ (x : Bool),
+  nonrecfun x =
+    match x with
+    | false => 0
+    | true => 0
+-/
+#guard_msgs in
+#print equations nonrecfun
+
+end Test2
+
+namespace Test3
+
+def nonrecfun : Bool → Nat
+  | false => 0
+  | true => 0
+
+-- should have no effect
+set_option eqns.nonrecursive false
+
+/--
+info: equations:
+theorem Test3.nonrecfun.eq_1 : nonrecfun false = 0
+theorem Test3.nonrecfun.eq_2 : nonrecfun true = 0
+-/
+#guard_msgs in
+#print equations nonrecfun
+
+end Test3

tests/lean/run/eqnsProjections.lean

@@ -0,0 +1,146 @@
+/-!
+This test should catch intentional or accidential changes to how projections are rewritten by
+various tactics
+-/
+
+structure S where
+  proj : Nat
+
+variable (P : Nat → Prop)
+
+section structure_abstract
+
+variable (s : S)
+
+/--
+error: tactic 'fail' failed
+P : Nat → Prop
+s : S
+⊢ P s.1
+-/
+#guard_msgs in
+example : P (s.proj) := by
+  rw [S.proj]
+  -- Cannot use
+  -- guard_target =ₛ P s.1
+  -- here as, as that elaborates as `P s.proj`
+  fail
+
+/--
+error: tactic 'fail' failed
+P : Nat → Prop
+s : S
+⊢ P s.1
+-/
+#guard_msgs in
+example : P (s.proj) := by
+  unfold S.proj
+  fail
+
+/-- error: simp made no progress -/
+#guard_msgs in
+example : P (s.proj) := by
+  simp [S.proj]
+  fail
+
+end structure_abstract
+
+section structure_concrete
+
+variable (n : Nat)
+/--
+error: tactic 'fail' failed
+P : Nat → Prop
+n : Nat
+⊢ P { proj := n }.1
+-/
+#guard_msgs in
+example : P (S.proj ⟨n⟩) := by rw [S.proj]; fail
+  -- Cannot use
+  -- guard_target =ₛ P s.1
+  -- here as, as that elaborates as `P s.proj`
+
+/--
+error: tactic 'fail' failed
+P : Nat → Prop
+n : Nat
+⊢ P { proj := n }.1
+-/
+#guard_msgs in
+example : P (S.proj ⟨n⟩) := by unfold S.proj; fail
+
+/--
+error: tactic 'fail' failed
+P : Nat → Prop
+n : Nat
+⊢ P n
+-/
+#guard_msgs in
+example : P (S.proj ⟨n⟩) := by simp [S.proj]; fail -- NB: reduces the projectino
+
+end structure_concrete
+
+class C (α : Type) where
+  meth : Nat
+
+section class_abstract
+
+instance : C Bool where
+  meth := 42
+
+variable (α : Type) [C α]
+
+/--
+error: tactic 'fail' failed
+P : Nat → Prop
+α : Type
+inst✝ : C α
+⊢ P inst✝.1
+-/
+#guard_msgs in
+example : P (C.meth α) := by rw [C.meth]; fail
+
+/--
+error: tactic 'fail' failed
+P : Nat → Prop
+α : Type
+inst✝ : C α
+⊢ P inst✝.1
+-/
+#guard_msgs in
+example : P (C.meth α) := by unfold C.meth; fail
+
+/-- error: simp made no progress -/
+#guard_msgs in
+example : P (C.meth α) := by simp [C.meth]; fail
+
+end class_abstract
+
+section class_concrete
+
+/--
+error: tactic 'fail' failed
+P : Nat → Prop
+⊢ P instCBool.1
+-/
+#guard_msgs in
+example : P (C.meth Bool) := by rw [C.meth]; fail
+
+/--
+error: tactic 'fail' failed
+P : Nat → Prop
+⊢ P instCBool.1
+-/
+#guard_msgs in
+example : P (C.meth Bool) := by unfold C.meth; fail
+
+/--
+error: tactic 'fail' failed
+P : Nat → Prop
+⊢ P 42
+-/
+#guard_msgs in
+example : P (C.meth Bool) := by simp [C.meth]; fail -- NB: Unfolds the instance `instCBool`!
+
+
+end class_concrete

tests/lean/run/eqnsReducible.lean

@@ -0,0 +1,102 @@
+import Lean.Elab.Command
+
+variable (P : Bool → Prop)
+variable (o : Option Nat)
+
+/-!
+This test checks that `simp [foo]` where `foo` is `reducible` uses the unfolding machinery,
+not the equations machinery.
+-/
+
+@[reducible] def red : Option α → Bool
+  | .some _ => true
+  | .none => false
+
+-- check that simp rewrites even without constants
+
+/--
+error: tactic 'fail' failed
+P : Bool → Prop
+o : Option Nat
+⊢ P
+    (match o with
+    | some val => true
+    | none => false)
+-/
+#guard_msgs in
+theorem ex1 : P (red o) := by simp [red]; fail
+
+-- check that the equational theorems have not been generated
+
+/-- info: false -/
+#guard_msgs in
+run_meta Lean.logInfo m!"{← Lean.hasConst `red.eq_1}"
+
+-- Again, the same for the `simp` attribute
+
+attribute [simp] red
+
+/-- info: false -/
+#guard_msgs in
+run_meta Lean.logInfo m!"{← Lean.hasConst `red.eq_1}"
+
+/--
+error: tactic 'fail' failed
+P : Bool → Prop
+o : Option Nat
+⊢ P
+    (match o with
+    | some val => true
+    | none => false)
+-/
+#guard_msgs in
+theorem ex1' : P (red o) := by simp; fail
+
+-- For comparison, the behavior for a semi-reducible function
+
+def semired : Option α → Bool
+  | .some _ => true
+  | .none => false
+
+-- At least for now, non-recursive functions are also unfolded by simp (as per
+-- `SimpTheorems.unfoldEvenWithEqns`), in addition to applying their rewrite rules:
+
+/--
+error: tactic 'fail' failed
+P : Bool → Prop
+o : Option Nat
+⊢ P
+    (match o with
+    | some val => true
+    | none => false)
+-/
+#guard_msgs in
+theorem ex2 : P (semired o) := by simp [semired]; fail
+
+-- check that the equational theorems have been generated
+
+/-- info: true -/
+#guard_msgs in
+run_meta Lean.logInfo m!"{← Lean.hasConst `semired.eq_1}"
+
+def semired2 : Option α → Bool
+  | .some _ => true
+  | .none => false
+
+attribute [simp] semired2
+
+/-- info: true -/
+#guard_msgs in
+run_meta Lean.logInfo m!"{← Lean.hasConst `semired2.eq_1}"
+
+/--
+error: tactic 'fail' failed
+P : Bool → Prop
+o : Option Nat
+⊢ P
+    (match o with
+    | some val => true
+    | none => false)
+-/
+#guard_msgs in
+theorem ex2' : P (semired2 o) := by simp; fail

tests/lean/run/reserved.lean

@@ -50,17 +50,14 @@ info: nonrecfun.eq_def :
 #guard_msgs in
 #check nonrecfun.eq_def
 
-/--
-info: nonrecfun.eq_1 :
-  ∀ (x : Bool),
-    nonrecfun x =
-      match x with
-      | false => 0
-      | true => 0
--/
+/-- info: nonrecfun.eq_1 : nonrecfun false = 0 -/
 #guard_msgs in
 #check nonrecfun.eq_1
 
+/-- info: nonrecfun.eq_2 : nonrecfun true = 0 -/
+#guard_msgs in
+#check nonrecfun.eq_2
+
 def fact : Nat → Nat
   | 0 => 1
   | n+1 => (n+1) * fact n
@@ -130,3 +127,10 @@ info: find.eq_def (as : Array Int) (i : Nat) (v : Int) :
 -/
 #guard_msgs in
 #check find.eq_def
+
+/--
+info: find.eq_1 (as : Array Int) (i : Nat) (v : Int) :
+  find as i v = if x : i < as.size then if as[i] = v then i else find as (i + 1) v else i
+-/
+#guard_msgs in
+#check find.eq_1