From c9239bfaa8f4afc7d309a4916d3b2808c97dfb57 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sat, 7 Sep 2024 14:48:08 -0700 Subject: [PATCH] feat: let `unfold` do zeta-delta reduction of local definitions (#4834) This is "upstreaming" mathlib's `unfold_let` tactic by incorporating its functionality into `unfold`. Now `unfold` can, in addition to unfolding global definitions, unfold local definitions. The PR also updates the `conv` version of the tactic. An improvement over `unfold_let` is that it beta reduces unfolded local functions. Two features not present in `unfold` are that (1) `unfold_let` with no arguments does zeta delta reduction of *all* local definitions, and also (2) `unfold_let` can interleave unfoldings (in contrast, `unfold a b c` is exactly the same as `unfold a; unfold b; unfold c`). Closes RFC #4090 --- src/Init/Conv.lean | 15 +++-- src/Init/Tactics.lean | 12 ++-- src/Lean/Elab/Tactic/Conv/Unfold.lean | 10 ++- src/Lean/Elab/Tactic/Unfold.lean | 17 ++++- src/Lean/Meta/Tactic/Unfold.lean | 12 ++++ src/Lean/Meta/Transform.lean | 16 +++++ tests/lean/run/unfoldTactic.lean | 95 +++++++++++++++++++++++++++ 7 files changed, 164 insertions(+), 13 deletions(-) create mode 100644 tests/lean/run/unfoldTactic.lean diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean index 904bc28b9b..3ca904f59b 100644 --- a/src/Init/Conv.lean +++ b/src/Init/Conv.lean @@ -97,11 +97,18 @@ Users should prefer `unfold` for unfolding definitions. -/ syntax (name := delta) "delta" (ppSpace colGt ident)+ : conv /-- -* `unfold foo` unfolds all occurrences of `foo` in the target. +* `unfold id` unfolds all occurrences of definition `id` in the target. * `unfold id1 id2 ...` is equivalent to `unfold id1; unfold id2; ...`. -Like the `unfold` tactic, this uses equational lemmas for the chosen definition -to rewrite the target. For recursive definitions, -only one layer of unfolding is performed. -/ + +Definitions can be either global or local definitions. + +For non-recursive global definitions, this tactic is identical to `delta`. +For recursive global definitions, it uses the "unfolding lemma" `id.eq_def`, +which is generated for each recursive definition, to unfold according to the recursive definition given by the user. +Only one level of unfolding is performed, in contrast to `simp only [id]`, which unfolds definition `id` recursively. + +This is the `conv` version of the `unfold` tactic. +-/ syntax (name := unfold) "unfold" (ppSpace colGt ident)+ : conv /-- diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 0f1c715cd0..b3efac9234 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -676,12 +676,16 @@ compiled by Lean. syntax (name := delta) "delta" (ppSpace colGt ident)+ (location)? : tactic /-- -* `unfold id` unfolds definition `id`. +* `unfold id` unfolds all occurrences of definition `id` in the target. * `unfold id1 id2 ...` is equivalent to `unfold id1; unfold id2; ...`. +* `unfold id at h` unfolds at the hypothesis `h`. -For non-recursive definitions, this tactic is identical to `delta`. For recursive definitions, -it uses the "unfolding lemma" `id.eq_def`, which is generated for each recursive definition, -to unfold according to the recursive definition given by the user. +Definitions can be either global or local definitions. + +For non-recursive global definitions, this tactic is identical to `delta`. +For recursive global definitions, it uses the "unfolding lemma" `id.eq_def`, +which is generated for each recursive definition, to unfold according to the recursive definition given by the user. +Only one level of unfolding is performed, in contrast to `simp only [id]`, which unfolds definition `id` recursively. -/ syntax (name := unfold) "unfold" (ppSpace colGt ident)+ (location)? : tactic diff --git a/src/Lean/Elab/Tactic/Conv/Unfold.lean b/src/Lean/Elab/Tactic/Conv/Unfold.lean index 01ee6fdfbc..aa791a4d38 100644 --- a/src/Lean/Elab/Tactic/Conv/Unfold.lean +++ b/src/Lean/Elab/Tactic/Conv/Unfold.lean @@ -12,7 +12,13 @@ open Meta @[builtin_tactic Lean.Parser.Tactic.Conv.unfold] def evalUnfold : Tactic := fun stx => withMainContext do for declNameId in stx[1].getArgs do - let declName ← realizeGlobalConstNoOverloadWithInfo declNameId - applySimpResult (← unfold (← getLhs) declName) + let e ← elabTermForApply declNameId (mayPostpone := false) + match e with + | .const declName _ => + applySimpResult (← unfold (← getLhs) declName) + | .fvar declFVarId => + let lhs ← instantiateMVars (← getLhs) + changeLhs (← Meta.zetaDeltaFVars lhs #[declFVarId]) + | _ => throwErrorAt declNameId m!"'unfold' conv tactic failed, expression {e} is not a global or local constant" end Lean.Elab.Tactic.Conv diff --git a/src/Lean/Elab/Tactic/Unfold.lean b/src/Lean/Elab/Tactic/Unfold.lean index 7ad2b05203..7e77caa324 100644 --- a/src/Lean/Elab/Tactic/Unfold.lean +++ b/src/Lean/Elab/Tactic/Unfold.lean @@ -17,14 +17,25 @@ def unfoldLocalDecl (declName : Name) (fvarId : FVarId) : TacticM Unit := do def unfoldTarget (declName : Name) : TacticM Unit := do replaceMainGoal [← Meta.unfoldTarget (← getMainGoal) declName] +def zetaDeltaLocalDecl (declFVarId : FVarId) (fvarId : FVarId) : TacticM Unit := do + replaceMainGoal [← Meta.zetaDeltaLocalDecl (← getMainGoal) fvarId declFVarId] + +def zetaDeltaTarget (declFVarId : FVarId) : TacticM Unit := do + replaceMainGoal [← Meta.zetaDeltaTarget (← getMainGoal) declFVarId] + /-- "unfold " ident+ (location)? -/ @[builtin_tactic Lean.Parser.Tactic.unfold] def evalUnfold : Tactic := fun stx => do let loc := expandOptLocation stx[2] for declNameId in stx[1].getArgs do go declNameId loc where - go (declNameId : Syntax) (loc : Location) : TacticM Unit := do - let declName ← realizeGlobalConstNoOverloadWithInfo declNameId - withLocation loc (unfoldLocalDecl declName) (unfoldTarget declName) (throwTacticEx `unfold · m!"did not unfold '{declName}'") + go (declNameId : Syntax) (loc : Location) : TacticM Unit := withMainContext do + let e ← elabTermForApply declNameId (mayPostpone := false) + match e with + | .const declName _ => + withLocation loc (unfoldLocalDecl declName) (unfoldTarget declName) (throwTacticEx `unfold · m!"did not unfold '{declName}'") + | .fvar declFVarId => + withLocation loc (zetaDeltaLocalDecl declFVarId) (zetaDeltaTarget declFVarId) (throwTacticEx `unfold · m!"did not unfold '{e}'") + | _ => withRef declNameId <| throwTacticEx `unfold (← getMainGoal) m!"expression {e} is not a global or local constant" end Lean.Elab.Tactic diff --git a/src/Lean/Meta/Tactic/Unfold.lean b/src/Lean/Meta/Tactic/Unfold.lean index 773df7f2ba..eb95630fba 100644 --- a/src/Lean/Meta/Tactic/Unfold.lean +++ b/src/Lean/Meta/Tactic/Unfold.lean @@ -43,4 +43,16 @@ def unfoldLocalDecl (mvarId : MVarId) (fvarId : FVarId) (declName : Name) : Meta let some (_, mvarId) ← applySimpResultToLocalDecl mvarId fvarId r (mayCloseGoal := false) | unreachable! return mvarId +def zetaDeltaTarget (mvarId : MVarId) (declFVarId : FVarId) : MetaM MVarId := mvarId.withContext do + let target ← instantiateMVars (← mvarId.getType) + let target' ← Meta.zetaDeltaFVars target #[declFVarId] + if target' == target then throwError "tactic 'unfold' failed to unfold '{Expr.fvar declFVarId}' at{indentExpr target}" + mvarId.replaceTargetDefEq target' + +def zetaDeltaLocalDecl (mvarId : MVarId) (fvarId : FVarId) (declFVarId : FVarId) : MetaM MVarId := mvarId.withContext do + let type ← fvarId.getType + let type' ← Meta.zetaDeltaFVars (← instantiateMVars type) #[declFVarId] + if type' == type then throwError "tactic 'unfold' failed to unfold '{Expr.fvar fvarId}' at{indentExpr type}" + mvarId.replaceLocalDeclDefEq fvarId type' + end Lean.Meta diff --git a/src/Lean/Meta/Transform.lean b/src/Lean/Meta/Transform.lean index 6a10848ff1..8d0f513842 100644 --- a/src/Lean/Meta/Transform.lean +++ b/src/Lean/Meta/Transform.lean @@ -151,6 +151,22 @@ def zetaReduce (e : Expr) : MetaM Expr := do | _ => return .continue transform e (pre := pre) (usedLetOnly := true) +/-- +Zeta reduces only the provided fvars, beta reducing the substitutions. +-/ +def zetaDeltaFVars (e : Expr) (fvars : Array FVarId) : MetaM Expr := + let unfold? (fvarId : FVarId) : MetaM (Option Expr) := do + if fvars.contains fvarId then + fvarId.getValue? + else + return none + let pre (e : Expr) : MetaM TransformStep := do + if let .fvar fvarId := e.getAppFn then + if let some val ← unfold? fvarId then + return .visit <| (← instantiateMVars val).beta e.getAppArgs + return .continue + transform e (pre := pre) + /-- Unfold definitions and theorems in `e` that are not in the current environment, but are in `biggerEnv`. -/ def unfoldDeclsFrom (biggerEnv : Environment) (e : Expr) : CoreM Expr := do withoutModifyingEnv do diff --git a/tests/lean/run/unfoldTactic.lean b/tests/lean/run/unfoldTactic.lean new file mode 100644 index 0000000000..eaa26190e5 --- /dev/null +++ b/tests/lean/run/unfoldTactic.lean @@ -0,0 +1,95 @@ +/-! +# Tests of the `unfold` tactic +-/ + +/-! +Tests adapted from mathlib's `unfold_let` tactic +-/ + +example : let x := 1; let y := 2; x + y = y + x := by + intro x y + unfold x + guard_target =ₛ 1 + y = y + 1 + let z := 3 + have h : z - 3 = 0 := rfl + unfold z at h + guard_hyp h :ₛ 3 - 3 = 0 + unfold y + guard_target =ₛ 1 + 2 = 2 + 1 + rfl + +example : let x := 1; let y := 2; x + y = y + x := by + intro x y + unfold x y + guard_target =ₛ 1 + 2 = 2 + 1 + rfl + +example : let x := 1; let y := 2 + x; y = 3 := by + intro x y + unfold y + guard_target =ₛ 2 + x = 3 + unfold x + guard_target =ₛ 2 + 1 = 3 + rfl + +example : let x := 1; let y := 2 + x; y = 3 := by + intro x y + fail_if_success unfold x y -- wrong order + unfold y x + guard_target =ₛ 2 + 1 = 3 + rfl + +/-! +Do not reorder hypotheses. (`unfold` makes a change) +-/ +set_option linter.unusedVariables false in +example : let ty := Int; ty → Nat → Nat := by + intro ty a a + unfold ty at * + exact a + +/-! +Beta reduction of unfolded local functions +-/ +example : True := by + let f (x y : Nat) := x + y + have : f 1 2 = 3 := by + unfold f + guard_target =ₛ 1 + 2 = 3 + rfl + trivial + +/-! +Nothing to unfold +-/ +/-- +error: tactic 'unfold' failed to unfold 'id' at + True +-/ +#guard_msgs in +example : True := by + unfold id +/-- +error: tactic 'unfold' failed to unfold 'x' at + True +-/ +#guard_msgs in +example : True := by + let x := 2 + unfold x + + +/-! +Conv tactic +-/ + +example (h : False) : id true = false := by + conv => unfold id + guard_target =ₛ true = false + exact h.elim + +example : let x := 1; let y := 2; x + y = y + x := by + intro x y + conv => unfold x + guard_target =ₛ 1 + y = y + 1 + rfl