refactor: add Simp.tryLemma?

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

@@ -41,6 +41,36 @@ where
       trace[Meta.Tactic.simp.discharge] "{lemmaName}, failed to synthesize instance{indentExpr type}"
       return false
 
+def tryLemma? (e : Expr) (lemma : SimpLemma) (discharge? : Expr → SimpM (Option Expr)) : SimpM (Option Result) :=
+  withNewMCtxDepth do
+    let val  ← lemma.getValue
+    let type ← inferType val
+    let (xs, bis, type) ← forallMetaTelescopeReducing type
+    let type ← whnf (← instantiateMVars type)
+    let lhs := type.appFn!.appArg!
+    if (← isDefEq lhs e) then
+      unless (← synthesizeArgs lemma.getName xs bis discharge?) do
+        return none
+      let proof ← instantiateMVars (mkAppN val xs)
+      if ← hasAssignableMVar proof then
+        trace[Meta.Tactic.simp.rewrite] "{lemma}, has unassigned metavariables after unification"
+        return none
+      let rhs   ← instantiateMVars type.appArg!
+      if e == rhs then
+        return none
+      if lemma.perm && !Expr.lt rhs e then
+        trace[Meta.Tactic.simp.rewrite] "{lemma}, perm rejected {e} ==> {rhs}"
+        return none
+      trace[Meta.Tactic.simp.rewrite] "{lemma}, {e} ==> {rhs}"
+      return some { expr := rhs, proof? := proof }
+    else
+      unless lhs.isMVar do
+        -- We do not report unification failures when `lhs` is a metavariable
+        -- Example: `x = ()`
+        -- TODO: reconsider if we want lemmas such as `(x : Unit) → x = ()`
+        trace[Meta.Tactic.simp.unify] "{lemma}, failed to unify {lhs} with {e}"
+      return none
+
 /-
 Remark: the parameter tag is used for creating trace messages. It is irrelevant otherwise.
 -/
@@ -53,7 +83,7 @@ def rewrite (e : Expr) (s : DiscrTree SimpLemma) (erased : Std.PHashSet Name) (d
     let lemmas := lemmas.insertionSort fun e₁ e₂ => e₁.priority < e₂.priority
     for lemma in lemmas do
       unless inErasedSet lemma do
-        if let some result ← tryLemma? lemma then
+        if let some result ← tryLemma? e lemma discharge? then
           return result
     return { expr := e }
 where
@@ -62,36 +92,6 @@ where
     | none => false
     | some name => erased.contains name
 
-  tryLemma? (lemma : SimpLemma) : SimpM (Option Result) :=
-    withNewMCtxDepth do
-      let val  ← lemma.getValue
-      let type ← inferType val
-      let (xs, bis, type) ← forallMetaTelescopeReducing type
-      let type ← whnf (← instantiateMVars type)
-      let lhs := type.appFn!.appArg!
-      if (← isDefEq lhs e) then
-        unless (← synthesizeArgs lemma.getName xs bis discharge?) do
-          return none
-        let proof ← instantiateMVars (mkAppN val xs)
-        if ← hasAssignableMVar proof then
-          trace[Meta.Tactic.simp.rewrite] "{lemma}, has unassigned metavariables after unification"
-          return none
-        let rhs   ← instantiateMVars type.appArg!
-        if e == rhs then
-          return none
-        if lemma.perm && !Expr.lt rhs e then
-          trace[Meta.Tactic.simp.rewrite] "{lemma}, perm rejected {e} ==> {rhs}"
-          return none
-        trace[Meta.Tactic.simp.rewrite] "{lemma}, {e} ==> {rhs}"
-        return some { expr := rhs, proof? := proof }
-      else
-        unless lhs.isMVar do
-          -- We do not report unification failures when `lhs` is a metavariable
-          -- Example: `x = ()`
-          -- TODO: reconsider if we want lemmas such as `(x : Unit) → x = ()`
-          trace[Meta.Tactic.simp.unify] "{lemma}, failed to unify {lhs} with {e}"
-        return none
-
 def rewriteCtorEq? (e : Expr) : MetaM (Option Result) := withReducibleAndInstances do
   match e.eq? with
   | none => return none

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

@@ -21,12 +21,12 @@ namespace Lean.Meta
   Then, we use `abstractMVars` to abstract the universe metavariables and create new fresh universe parameters that are stored at the field `levelParams`.
 -/
 structure SimpLemma where
-  keys        : Array DiscrTree.Key
-  levelParams : Array Name -- non empty for local universe polymorhic proofs.
+  keys        : Array DiscrTree.Key := #[]
+  levelParams : Array Name := #[] -- non empty for local universe polymorhic proofs.
   proof       : Expr
-  priority    : Nat
-  post        : Bool
-  perm        : Bool -- true is lhs and rhs are identical modulo permutation of variables
+  priority    : Nat  := eval_prio default
+  post        : Bool := true
+  perm        : Bool := false -- true is lhs and rhs are identical modulo permutation of variables
   name?       : Option Name := none -- for debugging and tracing purposes
   deriving Inhabited