From 66ab016723adf233f0c511e2e82cd5884d740614 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Sun, 15 Oct 2023 12:12:10 +1100 Subject: [PATCH] =?UTF-8?q?chore:=20simp=20tracing=20reports=20=E2=86=90?= =?UTF-8?q?=20(#2621)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * chore: simp tracing reports ← --------- Co-authored-by: Mario Carneiro --- src/Lean/Elab/Tactic/Simp.lean | 11 +++++++---- src/Lean/Meta/Tactic/Simp/SimpTheorems.lean | 10 +++++----- tests/lean/simp_trace.lean | 8 ++++++++ tests/lean/simp_trace.lean.expected.out | 5 +++++ 4 files changed, 25 insertions(+), 9 deletions(-) diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean index 79c46e2ebc86..3529e1d5f923 100644 --- 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 index 7921193c44e1..77444359e0d2 100644 --- 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 index d9a442be541c..54cb70de899c 100644 --- 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 index 2c33d3740a92..4e66a9dad0f3 100644 --- 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