feat: add delta tactic

src/Init/Notation.lean

@@ -364,6 +364,11 @@ syntax simpStar  := "*"
 syntax (name := simp) "simp " ("(" &"config" " := " term ")")? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic
 syntax (name := simpAll) "simp_all " ("(" &"config" " := " term ")")? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? : tactic
 
+/--
+  Delta expand the given definition.
+  This is a low-level tactic, it will expose how recursive definitions have been compiled by Lean. -/
+syntax (name := delta) "delta " ident (location)? : tactic
+
 -- Auxiliary macro for lifting have/suffices/let/...
 -- It makes sure the "continuation" `?_` is the main goal after refining
 macro "refineLift " e:term : tactic => `(focus (refine noImplicitLambda% $e; rotateRight))

src/Lean/Elab/Tactic.lean

@@ -16,3 +16,4 @@ import Lean.Elab.Tactic.Simp
 import Lean.Elab.Tactic.BuiltinTactic
 import Lean.Elab.Tactic.Split
 import Lean.Elab.Tactic.Conv
+import Lean.Elab.Tactic.Delta

src/Lean/Elab/Tactic/Delta.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Tactic.Delta
+import Lean.Elab.Tactic.Basic
+import Lean.Elab.Tactic.Location
+
+namespace Lean.Elab.Tactic
+open Meta
+
+def deltaLocalDecl (declName : Name) (fvarId : FVarId) : TacticM Unit := do
+  let mvarId ← getMainGoal
+  let localDecl ← getLocalDecl fvarId
+  let typeNew ← deltaExpand localDecl.type (. == declName)
+  if typeNew == localDecl.type then
+    throwTacticEx `delta mvarId m!"did not delta reduce '{declName}' at '{localDecl.userName}'"
+  replaceMainGoal [← replaceLocalDeclDefEq mvarId fvarId typeNew]
+
+def deltaTarget (declName : Name) : TacticM Unit := do
+  let mvarId ← getMainGoal
+  let target ← getMainTarget
+  let targetNew ← deltaExpand target (. == declName)
+  if targetNew == target then
+    throwTacticEx `delta mvarId m!"did not delta reduce '{declName}'"
+  replaceMainGoal [← replaceTargetDefEq mvarId targetNew]
+
+/--
+  "delta " ident (location)?
+-/
+@[builtinTactic Lean.Parser.Tactic.delta] def evalDelta : Tactic := fun stx => do
+  let declName ← resolveGlobalConstNoOverload stx[1]
+  let loc := expandOptLocation stx[2]
+  withLocation loc (deltaLocalDecl declName) (deltaTarget declName) (throwTacticEx `delta . m!"did not delta reduce '{declName}'")
+
+end Lean.Elab.Tactic

tests/lean/delta.lean

@@ -0,0 +1,23 @@
+def f (x : Nat) : Nat := x + 1
+
+example (x y : Nat) (h : f x = 0) : False := by
+  delta f at h
+  traceState
+  contradiction
+
+example (x y : Nat) (h : f x = 0) : False := by
+  delta f -- Error
+
+example (x y : Nat) (h1 : f x = 0) (h2 : 0 = 0) : False := by
+  delta f at h2 -- Error
+
+example (x y : Nat) (h1 : f x = 0) (h2 : 0 = 0) : False := by
+  delta f at h1 h2 -- Error
+
+example (x y : Nat) (h1 : f x = 0) (h2 : 0 = 0) : False := by
+  delta f at *
+  traceState
+  contradiction
+
+example (x y : Nat) (h2 : 0 = 0) : False := by
+  delta f at *

tests/lean/delta.lean.expected.out

@@ -0,0 +1,25 @@
+x y : Nat
+h : x + 1 = 0
+⊢ False
+delta.lean:9:2-9:9: error: tactic 'delta' failed, did not delta reduce 'f'
+x y : Nat
+h : f x = 0
+⊢ False
+delta.lean:12:2-12:15: error: tactic 'delta' failed, did not delta reduce 'f' at 'h2'
+x y : Nat
+h1 : f x = 0
+h2 : 0 = 0
+⊢ False
+delta.lean:15:2-15:18: error: tactic 'delta' failed, did not delta reduce 'f' at 'h2'
+x y : Nat
+h1 : x + 1 = 0
+h2 : 0 = 0
+⊢ False
+x y : Nat
+h1 : x + 1 = 0
+h2 : 0 = 0
+⊢ False
+delta.lean:23:2-23:14: error: tactic 'delta' failed, did not delta reduce 'f'
+x y : Nat
+h2 : 0 = 0
+⊢ False