feat: generate equational theorems uniformly (#10734)

This PR follows upon #10606 and creates equational theorems uniformly
from the unfold theorem, there is only one handler registered in
`registerGetEqnsFn`.

For now we keep `registerGetEqnsFn`, because it’s used by mathlib’s
`irreducible_def`, but I’d like to get rid of it in the long term,
relying only on `registerGetUnfoldEqnFn` for constructions that should
unfold differently.

Author: nomeata

src/Lean/Elab/PreDefinition.lean

@@ -11,6 +11,6 @@ public import Lean.Elab.PreDefinition.Structural
 public import Lean.Elab.PreDefinition.Main
 public import Lean.Elab.PreDefinition.MkInhabitant
 public import Lean.Elab.PreDefinition.WF
+public import Lean.Elab.PreDefinition.EqnsUtils
 public import Lean.Elab.PreDefinition.Eqns
-public import Lean.Elab.PreDefinition.Nonrec.Eqns
 public import Lean.Elab.PreDefinition.EqUnfold

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -0,0 +1,66 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+
+
+prelude
+public import Lean.Meta.Basic
+import Lean.Meta.Tactic.Split
+import Lean.Meta.Match.MatchEqs
+import Lean.Meta.Tactic.SplitIf
+
+/-!
+This module contains helpers useful to prove unfolding and/or equational theorems.
+-/
+
+namespace Lean.Elab.Eqns
+open Meta
+
+public def simpMatch? (mvarId : MVarId) : MetaM (Option MVarId) := do
+  let mvarId' ← Split.simpMatchTarget mvarId
+  if mvarId != mvarId' then return some mvarId' else return none
+
+/--
+Simplify `if-then-expression`s in the goal target.
+If `useNewSemantics` is `true`, the flag `backward.split` is ignored.
+-/
+public def simpIf? (mvarId : MVarId) (useNewSemantics := false) : MetaM (Option MVarId) := do
+  let mvarId' ← simpIfTarget mvarId (useDecide := true) (useNewSemantics := useNewSemantics)
+  if mvarId != mvarId' then return some mvarId' else return none
+
+/-- Try to close goal using `rfl` with smart unfolding turned off. -/
+public def tryURefl (mvarId : MVarId) : MetaM Bool :=
+  withOptions (smartUnfolding.set · false) do
+    try mvarId.refl; return true catch _ => return false
+
+/-- Delta reduce the equation left-hand-side -/
+public def deltaLHS (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
+  let target ← mvarId.getType'
+  let some (_, lhs, rhs) := target.eq? | throwTacticEx `deltaLHS mvarId "equality expected"
+  let some lhs ← delta? lhs | throwTacticEx `deltaLHS mvarId "failed to delta reduce lhs"
+  mvarId.replaceTargetDefEq (← mkEq lhs rhs)
+
+public def tryContradiction (mvarId : MVarId) : MetaM Bool := do
+  mvarId.contradictionCore { genDiseq := true }
+
+partial def whnfAux (e : Expr) : MetaM Expr := do
+  let e ← whnfI e -- Must reduce instances too, otherwise it will not be able to reduce `(Nat.rec ... ... (OfNat.ofNat 0))`
+  let f := e.getAppFn
+  match f with
+  | .proj _ _ s => return mkAppN (f.updateProj! (← whnfAux s)) e.getAppArgs
+  | _ => return e
+
+/-- Apply `whnfR` to lhs, return `none` if `lhs` was not modified -/
+public def whnfReducibleLHS? (mvarId : MVarId) : MetaM (Option MVarId) := mvarId.withContext do
+  let target ← mvarId.getType'
+  let some (_, lhs, rhs) := target.eq? | return none
+  let lhs' ← whnfAux lhs
+  if lhs' != lhs then
+    return some (← mvarId.replaceTargetDefEq (← mkEq lhs' rhs))
+  else
+    return none
+
+end Lean.Elab.Eqns

src/Lean/Elab/PreDefinition/EqnsUtils.lean

@@ -6,8 +6,8 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Lean.Elab.PreDefinition.Eqns
 public import Lean.Elab.PreDefinition.FixedParams
+import Lean.Elab.PreDefinition.EqnsUtils
 import Lean.Meta.ArgsPacker.Basic
 import Init.Data.Array.Basic
 import Init.Internal.Order.Basic
@@ -19,7 +19,11 @@ namespace Lean.Elab.PartialFixpoint
 open Meta
 open Eqns
 
-public structure EqnInfo extends EqnInfoCore where
+public structure EqnInfo where
+  declName    : Name
+  levelParams : List Name
+  type        : Expr
+  value       : Expr
   declNames       : Array Name
   declNameNonRec  : Name
   fixedParamPerms : FixedParamPerms
@@ -118,14 +122,7 @@ def getUnfoldFor? (declName : Name) : MetaM (Option Name) := do
   let some info := eqnInfoExt.find? env declName | return none
   return some (← mkUnfoldEq declName info)
 
-def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
-  if let some info := eqnInfoExt.find? (← getEnv) declName then
-    mkEqns declName info.declNames (tryRefl := false)
-  else
-    return none
-
 builtin_initialize
-  registerGetEqnsFn getEqnsFor?
   registerGetUnfoldEqnFn getUnfoldFor?
 
 end Lean.Elab.PartialFixpoint

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

@@ -7,8 +7,8 @@ module
 
 prelude
 public import Lean.Meta.Basic
-public import Lean.Elab.PreDefinition.Eqns
 public import Lean.Elab.PreDefinition.FixedParams
+import Lean.Elab.PreDefinition.EqnsUtils
 import Lean.Meta.Eqns
 import Lean.Meta.Tactic.Split
 import Lean.Meta.Tactic.Simp.Main
@@ -24,7 +24,11 @@ open Eqns
 
 namespace Structural
 
-public structure EqnInfo extends EqnInfoCore where
+public structure EqnInfo where
+  declName    : Name
+  levelParams : List Name
+  type        : Expr
+  value       : Expr
   recArgPos : Nat
   declNames : Array Name
   fixedParamPerms : FixedParamPerms
@@ -53,6 +57,12 @@ where
             k brecOnApp x (mkAppN x extraArgs)
     throwError "could not find `.brecOn` application in{indentExpr e}"
 
+def deltaRHS? (mvarId : MVarId) (declName : Name) : MetaM (Option MVarId) := mvarId.withContext do
+  let target ← mvarId.getType'
+  let some (_, lhs, rhs) := target.eq? | return none
+  let some rhs ← delta? rhs.consumeMData (· == declName) | return none
+  mvarId.replaceTargetDefEq (← mkEq lhs rhs)
+
 /--
 Creates the proof of the unfolding theorem for `declName` with type `type`. It
 
@@ -151,12 +161,6 @@ public def registerEqnsInfo (preDef : PreDefinition) (declNames : Array Name) (r
   modifyEnv fun env => eqnInfoExt.insert env preDef.declName
     { preDef with recArgPos, declNames, fixedParamPerms }
 
-def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
-  if let some info := eqnInfoExt.find? (← getEnv) declName then
-    mkEqns declName info.declNames
-  else
-    return none
-
 /-- Generate the "unfold" lemma for `declName`. -/
 def mkUnfoldEq (declName : Name) (info : EqnInfo) : MetaM Name := do
   let name := mkEqLikeNameFor (← getEnv) info.declName unfoldThmSuffix
@@ -190,7 +194,6 @@ def getStructuralRecArgPosImp? (declName : Name) : CoreM (Option Nat) := do
 
 
 builtin_initialize
-  registerGetEqnsFn getEqnsFor?
   registerGetUnfoldEqnFn getUnfoldFor?
   registerTraceClass `Elab.definition.structural.eqns
 

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

@@ -6,9 +6,9 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Lean.Elab.PreDefinition.Eqns
 public import Lean.Elab.PreDefinition.FixedParams
 public import Lean.Meta.ArgsPacker.Basic
+import Lean.Elab.PreDefinition.EqnsUtils
 import Lean.Meta.Tactic.Rewrite
 import Lean.Meta.Tactic.Split
 import Lean.Elab.PreDefinition.Basic
@@ -18,7 +18,11 @@ namespace Lean.Elab.WF
 open Meta
 open Eqns
 
-public structure EqnInfo extends EqnInfoCore where
+public structure EqnInfo where
+  declName    : Name
+  levelParams : List Name
+  type        : Expr
+  value       : Expr
   declNames       : Array Name
   declNameNonRec  : Name
   argsPacker      : ArgsPacker
@@ -46,16 +50,6 @@ public def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Na
           eqnInfoExt.insert env preDef.declName { preDef with
             declNames, declNameNonRec, argsPacker, fixedParamPerms }
 
-def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
-  if let some info := eqnInfoExt.find? (← getEnv) declName then
-    mkEqns declName info.declNames (tryRefl := false)
-  else
-    return none
-
-builtin_initialize
-  registerGetEqnsFn getEqnsFor?
-
-
 /--
 This is a hack to fix fallout from #8519, where a non-exposed wfrec definition `foo`
 in a module would cause `foo.eq_def` to be defined eagerly and privately,

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

@@ -7,10 +7,10 @@ module
 
 prelude
 public import Lean.Elab.PreDefinition.Basic
-import Lean.Elab.PreDefinition.Eqns
+public import Lean.Meta.Tactic.Simp.Types
+import Lean.Elab.PreDefinition.EqnsUtils
 import Lean.Meta.Tactic.Apply
 import Lean.Meta.Tactic.Split
-public import Lean.Meta.Tactic.Simp.Types
 import Lean.Meta.Tactic.Simp.Main
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs
 import Lean.Meta.Tactic.Delta

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

@@ -172,9 +172,8 @@ builtin_initialize eqnsExt : EnvExtension EqnsExtState ←
 /--
 Simple equation theorem for nonrecursive definitions.
 -/
-private def mkSimpleEqThm (declName : Name) : MetaM (Option Name) := do
+def mkSimpleEqThm (declName : Name) (name : Name) : MetaM (Option Name) := do
   if let some (.defnInfo info) := (← getEnv).find? declName then
-    let name := mkEqLikeNameFor (← getEnv) declName unfoldThmSuffix
     realizeConst declName name (doRealize name info)
     return some name
   else
@@ -313,7 +312,8 @@ def getUnfoldEqnFor? (declName : Name) (nonRec := false) : MetaM (Option Name) :
             return some r
       else
         if nonRec then
-          return (← mkSimpleEqThm declName)
+          let name := mkEqLikeNameFor (← getEnv) declName unfoldThmSuffix
+          return (← mkSimpleEqThm declName name)
     return none
   if let some r := r? then
     unless r == unfoldName do
@@ -331,4 +331,7 @@ builtin_initialize
             return (← MetaM.run' <| getUnfoldEqnFor? declName (nonRec := true)).isSome
       return false
 
+  registerTraceClass `Elab.definition.eqns
+
+
 end Lean.Meta

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

@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// please update me
+
 namespace lean {
 options get_default_options() {
     options opts;