From 232b2b63005ea741805608c9e9ea19b93ef06f56 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Wed, 14 Feb 2024 12:53:25 +1100 Subject: [PATCH] chore: upstream replace tactic (#3321) Co-authored-by: Leonardo de Moura --- src/Init/Tactics.lean | 31 +++++++++++++++++ src/Lean/Elab/Tactic/BuiltinTactic.lean | 15 ++++++++ tests/lean/run/replace_tac.lean | 46 +++++++++++++++++++++++++ 3 files changed, 92 insertions(+) create mode 100644 tests/lean/run/replace_tac.lean diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index a515882605..fd6874160e 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -894,6 +894,37 @@ The tactic `nomatch h` is shorthand for `exact nomatch h`. macro "nomatch " es:term,+ : tactic => `(tactic| exact nomatch $es:term,*) +/-- +Acts like `have`, but removes a hypothesis with the same name as +this one if possible. For example, if the state is: + +```lean +f : α → β +h : α +⊢ goal +``` + +Then after `replace h := f h` the state will be: + +```lean +f : α → β +h : β +⊢ goal +``` + +whereas `have h := f h` would result in: + +```lean +f : α → β +h† : α +h : β +⊢ goal +``` + +This can be used to simulate the `specialize` and `apply at` tactics of Coq. +-/ +syntax (name := replace) "replace" haveDecl : tactic + /-- `repeat' tac` runs `tac` on all of the goals to produce a new list of goals, then runs `tac` again on all of those goals, and repeats until `tac` fails on all remaining goals. diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean index 792ab0573d..41c2c198a2 100644 --- a/src/Lean/Elab/Tactic/BuiltinTactic.lean +++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean @@ -12,6 +12,7 @@ import Lean.Elab.Open import Lean.Elab.SetOption import Lean.Elab.Tactic.Basic import Lean.Elab.Tactic.ElabTerm +import Lean.Elab.Do namespace Lean.Elab.Tactic open Meta @@ -481,4 +482,18 @@ where @[builtin_tactic right] def evalRight : Tactic := fun _stx => do liftMetaTactic (fun g => g.nthConstructor `right 1 (some 2)) +@[builtin_tactic replace] def evalReplace : Tactic := fun stx => do + match stx with + | `(tactic| replace $decl:haveDecl) => + withMainContext do + let vars ← Elab.Term.Do.getDoHaveVars <| mkNullNode #[.missing, decl] + let origLCtx ← getLCtx + evalTactic $ ← `(tactic| have $decl:haveDecl) + let mut toClear := #[] + for fv in vars do + if let some ldecl := origLCtx.findFromUserName? fv.getId then + toClear := toClear.push ldecl.fvarId + liftMetaTactic1 (·.tryClearMany toClear) + | _ => throwUnsupportedSyntax + end Lean.Elab.Tactic diff --git a/tests/lean/run/replace_tac.lean b/tests/lean/run/replace_tac.lean new file mode 100644 index 0000000000..040f0df299 --- /dev/null +++ b/tests/lean/run/replace_tac.lean @@ -0,0 +1,46 @@ +/- +Copyright (c) 2022 Arthur Paulino. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Arthur Paulino +-/ + +example (h : Int) : Nat := by + replace h : Nat := 0 + exact h + +example (h : Nat) : Nat := by + have h : Int := 0 + assumption -- original `h` is not absent but... + +example (h : Nat) : Nat := by + replace h : Int := 0 + fail_if_success assumption -- original `h` is absent now + replace h : Nat := 0 + exact h + +-- tests with `this` + +example : Nat := by + have : Int := 0 + replace : Nat := 0 + assumption + +example : Nat := by + have : Nat := 0 + have : Int := 0 + assumption -- original `this` is not absent but... + +example : Nat := by + have : Nat := 0 + replace : Int := 0 + fail_if_success assumption -- original `this` is absent now + replace : Nat := 0 + assumption + +-- trying to replace the type of a variable when the goal depends on it + +example {a : Nat} : a = a := by + replace a : Int := 0 + have : Nat := by assumption -- old `a` is not gone + have : Int := by exact a -- new `a` is of type `Int` + simp