From 3a6ebd88bb1d3cc181d0939b52b03a9c79041d4c Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 13 Feb 2024 23:21:14 +1100 Subject: [PATCH] chore: upstream repeat/split_ands/subst_eqs (#3305) Small tactics used in the implementation of `ext`. --------- Co-authored-by: Leonardo de Moura --- src/Init/Tactics.lean | 16 +++++++ src/Init/TacticsExtra.lean | 22 +++++++++ src/Lean/Elab/Tactic.lean | 1 + src/Lean/Elab/Tactic/BuiltinTactic.lean | 6 +++ src/Lean/Elab/Tactic/Repeat.lean | 25 ++++++++++ src/Lean/Meta/Tactic.lean | 3 +- src/Lean/Meta/Tactic/Repeat.lean | 64 +++++++++++++++++++++++++ tests/lean/run/and_intros.lean | 7 +++ 8 files changed, 143 insertions(+), 1 deletion(-) create mode 100644 src/Lean/Elab/Tactic/Repeat.lean create mode 100644 src/Lean/Meta/Tactic/Repeat.lean create mode 100644 tests/lean/run/and_intros.lean diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 8cdd481c88..44f05ade78 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -894,6 +894,22 @@ The tactic `nomatch h` is shorthand for `exact nomatch h`. macro "nomatch " es:term,+ : tactic => `(tactic| exact nomatch $es:term,*) +/-- +`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. +-/ +syntax (name := repeat') "repeat' " tacticSeq : tactic + +/-- +`repeat1' tac` applies `tac` to main goal at least once. If the application succeeds, +the tactic is applied recursively to the generated subgoals until it eventually fails. +-/ +syntax (name := repeat1') "repeat1' " tacticSeq : tactic + +/-- `and_intros` applies `And.intro` until it does not make progress. -/ +syntax "and_intros" : tactic +macro_rules | `(tactic| and_intros) => `(tactic| repeat' refine And.intro ?_ ?_) + end Tactic namespace Attr diff --git a/src/Init/TacticsExtra.lean b/src/Init/TacticsExtra.lean index 1fb5666bb9..5fc210a96d 100644 --- a/src/Init/TacticsExtra.lean +++ b/src/Init/TacticsExtra.lean @@ -41,4 +41,26 @@ macro_rules | `(tactic| if%$tk $c then%$ttk $pos else%$etk $neg) => expandIfThenElse tk ttk etk pos neg fun pos neg => `(if h : $c then $pos else $neg) +/-- +`iterate n tac` runs `tac` exactly `n` times. +`iterate tac` runs `tac` repeatedly until failure. + +`iterate`'s argument is a tactic sequence, +so multiple tactics can be run using `iterate n (tac₁; tac₂; ⋯)` or +```lean +iterate n + tac₁ + tac₂ + ⋯ +``` +-/ +syntax "iterate" (ppSpace num)? ppSpace tacticSeq : tactic +macro_rules + | `(tactic| iterate $seq:tacticSeq) => + `(tactic| try ($seq:tacticSeq); iterate $seq:tacticSeq) + | `(tactic| iterate $n $seq:tacticSeq) => + match n.1.toNat with + | 0 => `(tactic| skip) + | n+1 => `(tactic| ($seq:tacticSeq); iterate $(quote n) $seq:tacticSeq) + end Lean.Parser.Tactic diff --git a/src/Lean/Elab/Tactic.lean b/src/Lean/Elab/Tactic.lean index 81b79e3abb..b0dc3647c3 100644 --- a/src/Lean/Elab/Tactic.lean +++ b/src/Lean/Elab/Tactic.lean @@ -25,4 +25,5 @@ import Lean.Elab.Tactic.Calc import Lean.Elab.Tactic.Congr import Lean.Elab.Tactic.Guard import Lean.Elab.Tactic.RCases +import Lean.Elab.Tactic.Repeat import Lean.Elab.Tactic.Change diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean index 31eaff0903..792ab0573d 100644 --- a/src/Lean/Elab/Tactic/BuiltinTactic.lean +++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean @@ -324,6 +324,12 @@ def forEachVar (hs : Array Syntax) (tac : MVarId → FVarId → MetaM MVarId) : @[builtin_tactic Lean.Parser.Tactic.substVars] def evalSubstVars : Tactic := fun _ => liftMetaTactic fun mvarId => return [← substVars mvarId] +/-- +`subst_eq` repeatedly substitutes according to the equality proof hypotheses in the context, +replacing the left side of the equality with the right, until no more progress can be made. +-/ +elab "subst_eqs" : tactic => Elab.Tactic.liftMetaTactic1 (·.substEqs) + /-- Searches for a metavariable `g` s.t. `tag` is its exact name. If none then searches for a metavariable `g` s.t. `tag` is a suffix of its name. diff --git a/src/Lean/Elab/Tactic/Repeat.lean b/src/Lean/Elab/Tactic/Repeat.lean new file mode 100644 index 0000000000..b703105620 --- /dev/null +++ b/src/Lean/Elab/Tactic/Repeat.lean @@ -0,0 +1,25 @@ +/- +Copyright (c) 2022 Mario Carneiro. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mario Carneiro, Scott Morrison +-/ +import Lean.Meta.Tactic.Repeat +import Lean.Elab.Tactic.Basic + +namespace Lean.Elab.Tactic + +@[builtin_tactic repeat'] +def evalRepeat' : Tactic := fun stx => do + match stx with + | `(tactic| repeat' $tac:tacticSeq) => + setGoals (← Meta.repeat' (evalTacticAtRaw tac) (← getGoals)) + | _ => throwUnsupportedSyntax + +@[builtin_tactic repeat1'] +def evalRepeat1' : Tactic := fun stx => do + match stx with + | `(tactic| repeat1' $tac:tacticSeq) => + setGoals (← Meta.repeat1' (evalTacticAtRaw tac) (← getGoals)) + | _ => throwUnsupportedSyntax + +end Lean.Elab.Tactic diff --git a/src/Lean/Meta/Tactic.lean b/src/Lean/Meta/Tactic.lean index c5e7469c83..bedd0800fc 100644 --- a/src/Lean/Meta/Tactic.lean +++ b/src/Lean/Meta/Tactic.lean @@ -28,4 +28,5 @@ import Lean.Meta.Tactic.Rename import Lean.Meta.Tactic.LinearArith import Lean.Meta.Tactic.AC import Lean.Meta.Tactic.Refl -import Lean.Meta.Tactic.Congr \ No newline at end of file +import Lean.Meta.Tactic.Congr +import Lean.Meta.Tactic.Repeat diff --git a/src/Lean/Meta/Tactic/Repeat.lean b/src/Lean/Meta/Tactic/Repeat.lean new file mode 100644 index 0000000000..86d0490955 --- /dev/null +++ b/src/Lean/Meta/Tactic/Repeat.lean @@ -0,0 +1,64 @@ +/- +Copyright (c) 2022 Mario Carneiro. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mario Carneiro, Scott Morrison +-/ +import Lean.Meta.Basic + +namespace Lean.Meta +/-- +Implementation of `repeat'` and `repeat1'`. + +`repeat'Core f` runs `f` on all of the goals to produce a new list of goals, +then runs `f` again on all of those goals, and repeats until `f` fails on all remaining goals, +or until `maxIters` total calls to `f` have occurred. + +Returns a boolean indicating whether `f` succeeded at least once, and +all the remaining goals (i.e. those on which `f` failed). +-/ +def repeat'Core [Monad m] [MonadExcept ε m] [MonadBacktrack s m] [MonadMCtx m] + (f : MVarId → m (List MVarId)) (goals : List MVarId) (maxIters := 100000) : + m (Bool × List MVarId) := do + let (progress, acc) ← go maxIters false goals [] #[] + pure (progress, (← acc.filterM fun g => not <$> g.isAssigned).toList) +where + /-- Auxiliary for `repeat'Core`. `repeat'Core.go f maxIters progress goals stk acc` evaluates to + essentially `acc.toList ++ repeat' f (goals::stk).join maxIters`: that is, `acc` are goals we will + not revisit, and `(goals::stk).join` is the accumulated todo list of subgoals. -/ + go : Nat → Bool → List MVarId → List (List MVarId) → Array MVarId → m (Bool × Array MVarId) + | _, p, [], [], acc => pure (p, acc) + | n, p, [], goals::stk, acc => go n p goals stk acc + | n, p, g::goals, stk, acc => do + if ← g.isAssigned then + go n p goals stk acc + else + match n with + | 0 => pure <| (p, acc.push g ++ goals |> stk.foldl .appendList) + | n+1 => + match ← observing? (f g) with + | some goals' => go n true goals' (goals::stk) acc + | none => go n p goals stk (acc.push g) +termination_by n p goals stk _ => (n, stk, goals) + +/-- +`repeat' f` runs `f` on all of the goals to produce a new list of goals, +then runs `f` again on all of those goals, and repeats until `f` fails on all remaining goals, +or until `maxIters` total calls to `f` have occurred. +Always succeeds (returning the original goals if `f` fails on all of them). +-/ +def repeat' [Monad m] [MonadExcept ε m] [MonadBacktrack s m] [MonadMCtx m] + (f : MVarId → m (List MVarId)) (goals : List MVarId) (maxIters := 100000) : m (List MVarId) := + repeat'Core f goals maxIters <&> (·.2) + +/-- +`repeat1' f` runs `f` on all of the goals to produce a new list of goals, +then runs `f` again on all of those goals, and repeats until `f` fails on all remaining goals, +or until `maxIters` total calls to `f` have occurred. +Fails if `f` does not succeed at least once. +-/ +def repeat1' [Monad m] [MonadError m] [MonadExcept ε m] [MonadBacktrack s m] [MonadMCtx m] + (f : MVarId → m (List MVarId)) (goals : List MVarId) (maxIters := 100000) : m (List MVarId) := do + let (.true, goals) ← repeat'Core f goals maxIters | throwError "repeat1' made no progress" + pure goals + +end Lean.Meta diff --git a/tests/lean/run/and_intros.lean b/tests/lean/run/and_intros.lean new file mode 100644 index 0000000000..27e7f46901 --- /dev/null +++ b/tests/lean/run/and_intros.lean @@ -0,0 +1,7 @@ +example (hp : p) (hq : q) (hr : r) : (p ∧ q) ∧ (q ∧ (r ∧ p)) := by + and_intros + · exact hp + · exact hq + · exact hq + · exact hr + · exact hp