From 152a84c468f4c2a7deb25553e7e41618debcf28f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 3 Mar 2021 19:59:27 -0800 Subject: [PATCH] perf: reject rewrites that produce same expr --- src/Lean/Meta/Tactic/Simp/Rewrite.lean | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean index 7a28411d4a..a3441f6558 100644 --- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean +++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean @@ -84,14 +84,20 @@ where if ← hasAssignableMVar proof then return none let rhs ← instantiateMVars (← getRHS lemma.kind type) + if e == rhs then + return none if lemma.perm && !Expr.lt rhs e then - trace[Meta.Tactic.simp.unify]! "{lemma}, perm rejected {e} ==> {rhs}" + trace[Meta.Tactic.simp.rewrite]! "{lemma}, perm rejected {e} ==> {rhs}" return none let proof ← finalizeProof lemma.kind proof trace[Meta.Tactic.simp.rewrite]! "{lemma}, {e} ==> {rhs}" return some { expr := rhs, proof? := proof } else - trace[Meta.Tactic.simp.unify]! "{lemma}, failed to unify {lhs} with {e}" + 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