chore: simp tracing reports ← (#2621)

* chore: simp tracing reports ← --------- Co-authored-by: Mario Carneiro <[email protected]>
leanprover · Oct 15, 2023 · 66ab016 · 66ab016
1 parent 6df09d1
commit 66ab016
Show file tree

Hide file tree

Showing 4 changed files with 25 additions and 9 deletions.
diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
@@ -138,7 +138,7 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (eraseLocal : Bool) (kind :
     /-
     syntax simpPre := "↓"
     syntax simpPost := "↑"
-    syntax simpLemma := (simpPre <|> simpPost)? term
+    syntax simpLemma := (simpPre <|> simpPost)? "← "? term
 
     syntax simpErase := "-" ident
     -/
@@ -259,9 +259,12 @@ def traceSimpCall (stx : Syntax) (usedSimps : UsedSimps) : MetaM Unit := do
   let env ← getEnv
   for (thm, _) in usedSimps.toArray.qsort (·.2 < ·.2) do
     match thm with
-    | .decl declName => -- global definitions in the environment
-      if env.contains declName && !simpOnlyBuiltins.contains declName then
-        args := args.push (← `(Parser.Tactic.simpLemma| $(mkIdent (← unresolveNameGlobal declName)):ident))
+    | .decl declName inv => -- global definitions in the environment
+      if env.contains declName && (inv || !simpOnlyBuiltins.contains declName) then
+        args := args.push (if inv then
+          (← `(Parser.Tactic.simpLemma| ← $(mkIdent (← unresolveNameGlobal declName)):ident))
+        else
+          (← `(Parser.Tactic.simpLemma| $(mkIdent (← unresolveNameGlobal declName)):ident)))
     | .fvar fvarId => -- local hypotheses in the context
       if let some ldecl := lctx.find? fvarId then
         localsOrStar := localsOrStar.bind fun locals =>

diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
@@ -18,7 +18,7 @@ what action the user took which lead to this theorem existing in the simp set.
 -/
 inductive Origin where
   /-- A global declaration in the environment. -/
-  | decl (declName : Name)
+  | decl (declName : Name) (inv := false)
   /--
   A local hypothesis.
   When `contextual := true` is enabled, this fvar may exist in an extension
@@ -42,7 +42,7 @@ inductive Origin where
 
 /-- A unique identifier corresponding to the origin. -/
 def Origin.key : Origin → Name
-  | .decl declName => declName
+  | .decl declName _ => declName
   | .fvar fvarId => fvarId.name
   | .stx id _ => id
   | .other name => name
@@ -136,7 +136,7 @@ instance : ToFormat SimpTheorem where
     name ++ prio ++ perm
 
 def ppOrigin [Monad m] [MonadEnv m] [MonadError m] : Origin → m MessageData
-  | .decl n => mkConstWithLevelParams n
+  | .decl n inv => do let r ← mkConstWithLevelParams n; if inv then return m!"← {r}" else return r
   | .fvar n => return mkFVar n
   | .stx _ ref => return ref
   | .other n => return n
@@ -318,7 +318,7 @@ private def mkSimpTheoremsFromConst (declName : Name) (post : Bool) (inv : Bool)
       let mut r := #[]
       for (val, type) in (← preprocess val type inv (isGlobal := true)) do
         let auxName ← mkAuxLemma cinfo.levelParams type val
-        r := r.push <| (← mkSimpTheoremCore (.decl declName) (mkConst auxName (cinfo.levelParams.map mkLevelParam)) #[] (mkConst auxName) post prio)
+        r := r.push <| (← mkSimpTheoremCore (.decl declName inv) (mkConst auxName (cinfo.levelParams.map mkLevelParam)) #[] (mkConst auxName) post prio)
       return r
     else
       return #[← mkSimpTheoremCore (.decl declName) (mkConst declName (cinfo.levelParams.map mkLevelParam)) #[] (mkConst declName) post prio]
@@ -403,7 +403,7 @@ def getSimpTheorems : CoreM SimpTheorems :=
 
 /-- Auxiliary method for adding a global declaration to a `SimpTheorems` datastructure. -/
 def SimpTheorems.addConst (s : SimpTheorems) (declName : Name) (post := true) (inv := false) (prio : Nat := eval_prio default) : MetaM SimpTheorems := do
-  let s := { s with erased := s.erased.erase (.decl declName) }
+  let s := { s with erased := s.erased.erase (.decl declName inv) }
   let simpThms ← mkSimpTheoremsFromConst declName post inv prio
   return simpThms.foldl addSimpTheoremEntry s
 

diff --git a/tests/lean/simp_trace.lean b/tests/lean/simp_trace.lean
@@ -126,3 +126,11 @@ instance : HasProp Nat where
 
 example : HasProp.toProp 0 := by
   simp [HasProp.toProp]
+
+example (P Q : Prop) (h : P ↔ Q) (p : P) : Q := by
+  simp [← h]
+  exact p
+
+theorem my_thm' : a ↔ a ∧ a := my_thm.symm
+
+example (P : Prop) : P ∧ P ↔ P := by simp only [← my_thm']
diff --git a/tests/lean/simp_trace.lean.expected.out b/tests/lean/simp_trace.lean.expected.out
@@ -115,3 +115,8 @@ Try this: simp only [bla, h] at *
     | Sum.inr val => 0
 [Meta.Tactic.simp.rewrite] unfold h, h x ==> Sum.inl (x, x)
 Try this: simp only [HasProp.toProp]
+Try this: simp only [← h]
+[Meta.Tactic.simp.rewrite] ← h:1000, Q ==> P
+Try this: simp only [← my_thm']
+[Meta.Tactic.simp.rewrite] ← @my_thm':1000, P ∧ P ==> P
+[Meta.Tactic.simp.rewrite] iff_self:1000, P ↔ P ==> True