From 3e11b5fe154d6b4fede92ff16cf1f0c4af2d6cfd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 2 Jan 2024 06:07:28 -0800 Subject: [PATCH] fix: trace used builtin `simproc`s even if they are not in the environment --- src/Lean/Elab/Tactic/Simp.lean | 6 ++++++ tests/lean/builtinSimprocTrace.lean | 6 ++++++ tests/lean/builtinSimprocTrace.lean.expected.out | 1 + 3 files changed, 13 insertions(+) create mode 100644 tests/lean/builtinSimprocTrace.lean create mode 100644 tests/lean/builtinSimprocTrace.lean.expected.out diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean index ad3ead505f..f4018ac34f 100644 --- a/src/Lean/Elab/Tactic/Simp.lean +++ b/src/Lean/Elab/Tactic/Simp.lean @@ -311,6 +311,12 @@ def mkSimpOnly (stx : Syntax) (usedSimps : UsedSimps) : MetaM Syntax := do | false, true => `(Parser.Tactic.simpLemma| ↓ ← $decl:term) | false, false => `(Parser.Tactic.simpLemma| ↓ $decl:term) args := args.push arg + else if (← Simp.isBuiltinSimproc declName) then + let decl := mkIdent declName + let arg ← match post with + | true => `(Parser.Tactic.simpLemma| $decl:term) + | false => `(Parser.Tactic.simpLemma| ↓ $decl:term) + args := args.push arg | .fvar fvarId => -- local hypotheses in the context -- `simp_all` always uses all propositional hypotheses (and it can't use -- any others). So `simp_all only [h]`, where `h` is a hypothesis, would diff --git a/tests/lean/builtinSimprocTrace.lean b/tests/lean/builtinSimprocTrace.lean new file mode 100644 index 0000000000..73d656ae85 --- /dev/null +++ b/tests/lean/builtinSimprocTrace.lean @@ -0,0 +1,6 @@ +def f (_ : Nat) := 10 + +set_option tactic.simp.trace true +example : f x = (if true then 8 + 2 else 0) := by + simp + rw [f] diff --git a/tests/lean/builtinSimprocTrace.lean.expected.out b/tests/lean/builtinSimprocTrace.lean.expected.out new file mode 100644 index 0000000000..6439001ea8 --- /dev/null +++ b/tests/lean/builtinSimprocTrace.lean.expected.out @@ -0,0 +1 @@ +Try this: simp only [↓reduceIte, Nat.reduceAdd]