From c318d5817de75b023107de0e371ba069e75ce1a3 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Mon, 28 Aug 2023 21:59:04 +1000 Subject: [PATCH] feat: allow configuring occs in rw --- src/Init/Meta.lean | 16 ++++++ src/Init/Tactics.lean | 9 ++++ src/Lean/Data.lean | 1 - src/Lean/Data/Occurrences.lean | 23 --------- src/Lean/Elab/Tactic/Rewrite.lean | 5 +- src/Lean/Meta/KAbstract.lean | 10 +++- src/Lean/Meta/Tactic/Rewrite.lean | 8 +-- tests/lean/interactive/1403.lean.expected.out | 2 +- tests/lean/rewrite.lean | 50 +++++++++++++++++++ tests/lean/rewrite.lean.expected.out | 18 +++++++ 10 files changed, 109 insertions(+), 33 deletions(-) delete mode 100644 src/Lean/Data/Occurrences.lean diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index dcd3471c7a..bf42bdddfd 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -1280,11 +1280,27 @@ def neutralConfig : Simp.Config := { end Simp +inductive Occurrences where + | all + | pos (idxs : List Nat) + | neg (idxs : List Nat) + deriving Inhabited, BEq + +def Occurrences.contains : Occurrences → Nat → Bool + | all, _ => true + | pos idxs, idx => idxs.contains idx + | neg idxs, idx => !idxs.contains idx + +def Occurrences.isAll : Occurrences → Bool + | all => true + | _ => false + namespace Rewrite structure Config where transparency : TransparencyMode := TransparencyMode.reducible offsetCnstrs : Bool := true + occs : Occurrences := Occurrences.all end Rewrite diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index a5c9981ece..246756a972 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -350,6 +350,15 @@ This provides a convenient way to unfold `e`. - `rewrite [e] at l` rewrites `e` at location(s) `l`, where `l` is either `*` or a list of hypotheses in the local context. In the latter case, a turnstile `⊢` or `|-` can also be used, to signify the target of the goal. + +Using `rw (config := {occs := .pos L}) [e]`, +where `L : List Nat`, you can control which "occurrences" are rewritten. +(This option applies to each rule, so usually this will only be used with a single rule.) +Occurrences count from `1`. +At the first occurrence, whether allowed or not, +arguments of the rewrite rule `e` may be instantiated, +restricting which later rewrites can be found. +`{occs := .neg L}` allows skipping specified occurrences. -/ syntax (name := rewriteSeq) "rewrite" (config)? rwRuleSeq (location)? : tactic diff --git a/src/Lean/Data.lean b/src/Lean/Data.lean index 047f522f7a..7ff9a08ee5 100644 --- a/src/Lean/Data.lean +++ b/src/Lean/Data.lean @@ -15,7 +15,6 @@ import Lean.Data.LOption import Lean.Data.Lsp import Lean.Data.Name import Lean.Data.NameMap -import Lean.Data.Occurrences import Lean.Data.OpenDecl import Lean.Data.Options import Lean.Data.Parsec diff --git a/src/Lean/Data/Occurrences.lean b/src/Lean/Data/Occurrences.lean deleted file mode 100644 index 02109c7c71..0000000000 --- a/src/Lean/Data/Occurrences.lean +++ /dev/null @@ -1,23 +0,0 @@ -/- -Copyright (c) 2020 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura --/ -namespace Lean - -inductive Occurrences where - | all - | pos (idxs : List Nat) - | neg (idxs : List Nat) - deriving Inhabited, BEq - -def Occurrences.contains : Occurrences → Nat → Bool - | all, _ => true - | pos idxs, idx => idxs.contains idx - | neg idxs, idx => !idxs.contains idx - -def Occurrences.isAll : Occurrences → Bool - | all => true - | _ => false - -end Lean diff --git a/src/Lean/Elab/Tactic/Rewrite.lean b/src/Lean/Elab/Tactic/Rewrite.lean index 55de56b798..f0451531b1 100644 --- a/src/Lean/Elab/Tactic/Rewrite.lean +++ b/src/Lean/Elab/Tactic/Rewrite.lean @@ -11,14 +11,15 @@ import Lean.Elab.Tactic.Config namespace Lean.Elab.Tactic open Meta -def rewriteTarget (stx : Syntax) (symm : Bool) (config : Rewrite.Config) : TacticM Unit := do +def rewriteTarget (stx : Syntax) (symm : Bool) (config : Rewrite.Config := {}) : TacticM Unit := do Term.withSynthesize <| withMainContext do let e ← elabTerm stx none true let r ← (← getMainGoal).rewrite (← getMainTarget) e symm (config := config) let mvarId' ← (← getMainGoal).replaceTargetEq r.eNew r.eqProof replaceMainGoal (mvarId' :: r.mvarIds) -def rewriteLocalDecl (stx : Syntax) (symm : Bool) (fvarId : FVarId) (config : Rewrite.Config) : TacticM Unit := do +def rewriteLocalDecl (stx : Syntax) (symm : Bool) (fvarId : FVarId) (config : Rewrite.Config := {}) : + TacticM Unit := do Term.withSynthesize <| withMainContext do let e ← elabTerm stx none true let localDecl ← fvarId.getDecl diff --git a/src/Lean/Meta/KAbstract.lean b/src/Lean/Meta/KAbstract.lean index aed457f853..692fa27c2e 100644 --- a/src/Lean/Meta/KAbstract.lean +++ b/src/Lean/Meta/KAbstract.lean @@ -3,7 +3,6 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ -import Lean.Data.Occurrences import Lean.HeadIndex import Lean.Meta.Basic @@ -12,7 +11,14 @@ namespace Lean.Meta /-- Abstract occurrences of `p` in `e`. We detect subterms equivalent to `p` using key-matching. That is, only perform `isDefEq` tests when the head symbol of substerm is equivalent to head symbol of `p`. -By default, all occurrences are abstracted, but this behavior can be controlled using the `occs` parameter. + +By default, all occurrences are abstracted, +but this behavior can be controlled using the `occs` parameter. + +All matches of `p` in `e` are considered for occurrences, +but at the first match (whether included in the occurrences or not) +metavariables appearing in `p` (or `e`) may become instantiated, +affecting the possibility of subsequent matches. -/ def kabstract (e : Expr) (p : Expr) (occs : Occurrences := .all) : MetaM Expr := do let e ← instantiateMVars e diff --git a/src/Lean/Meta/Tactic/Rewrite.lean b/src/Lean/Meta/Tactic/Rewrite.lean index 449430f4f3..78daecb526 100644 --- a/src/Lean/Meta/Tactic/Rewrite.lean +++ b/src/Lean/Meta/Tactic/Rewrite.lean @@ -20,7 +20,7 @@ structure RewriteResult where Rewrite goal `mvarId` -/ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr) - (symm : Bool := false) (occs : Occurrences := Occurrences.all) (config := { : Rewrite.Config }) : MetaM RewriteResult := + (symm : Bool := false) (config := { : Rewrite.Config }) : MetaM RewriteResult := mvarId.withContext do mvarId.checkNotAssigned `rewrite let heqType ← instantiateMVars (← inferType heq) @@ -34,7 +34,7 @@ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr) if lhs.getAppFn.isMVar then throwTacticEx `rewrite mvarId m!"pattern is a metavariable{indentExpr lhs}\nfrom equation{indentExpr heqType}" let e ← instantiateMVars e - let eAbst ← withConfig (fun oldConfig => { config, oldConfig with }) <| kabstract e lhs occs + let eAbst ← withConfig (fun oldConfig => { config, oldConfig with }) <| kabstract e lhs config.occs unless eAbst.hasLooseBVars do throwTacticEx `rewrite mvarId m!"did not find instance of the pattern in the target expression{indentExpr lhs}" -- construct rewrite proof @@ -69,7 +69,7 @@ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr) @[deprecated MVarId.rewrite] def rewrite (mvarId : MVarId) (e : Expr) (heq : Expr) - (symm : Bool := false) (occs : Occurrences := Occurrences.all) (config := { : Rewrite.Config }) : MetaM RewriteResult := - mvarId.rewrite e heq symm occs config + (symm : Bool := false) (config := { : Rewrite.Config }) : MetaM RewriteResult := + mvarId.rewrite e heq symm config end Lean.Meta diff --git a/tests/lean/interactive/1403.lean.expected.out b/tests/lean/interactive/1403.lean.expected.out index a00fbddf06..2a50da1c88 100644 --- a/tests/lean/interactive/1403.lean.expected.out +++ b/tests/lean/interactive/1403.lean.expected.out @@ -4,5 +4,5 @@ {"start": {"line": 1, "character": 2}, "end": {"line": 1, "character": 12}}, "contents": {"value": - "`rewrite [e]` applies identity `e` as a rewrite rule to the target of the main goal.\nIf `e` is preceded by left arrow (`←` or `<-`), the rewrite is applied in the reverse direction.\nIf `e` is a defined constant, then the equational theorems associated with `e` are used.\nThis provides a convenient way to unfold `e`.\n- `rewrite [e₁, ..., eₙ]` applies the given rules sequentially.\n- `rewrite [e] at l` rewrites `e` at location(s) `l`, where `l` is either `*` or a\n list of hypotheses in the local context. In the latter case, a turnstile `⊢` or `|-`\n can also be used, to signify the target of the goal.\n", + "`rewrite [e]` applies identity `e` as a rewrite rule to the target of the main goal.\nIf `e` is preceded by left arrow (`←` or `<-`), the rewrite is applied in the reverse direction.\nIf `e` is a defined constant, then the equational theorems associated with `e` are used.\nThis provides a convenient way to unfold `e`.\n- `rewrite [e₁, ..., eₙ]` applies the given rules sequentially.\n- `rewrite [e] at l` rewrites `e` at location(s) `l`, where `l` is either `*` or a\n list of hypotheses in the local context. In the latter case, a turnstile `⊢` or `|-`\n can also be used, to signify the target of the goal.\n\nUsing `rw (config := {occs := .pos L}) [e]`,\nwhere `L : List Nat`, you can control which \"occurrences\" are rewritten.\n(This option applies to each rule, so usually this will only be used with a single rule.)\nOccurrences count from `1`.\nAt the first occurrence, whether allowed or not,\narguments of the rewrite rule `e` may be instantiated,\nrestricting which later rewrites can be found.\n`{occs := .neg L}` allows skipping specified occurrences.\n", "kind": "markdown"}} diff --git a/tests/lean/rewrite.lean b/tests/lean/rewrite.lean index 7edc31e821..b088fa0df9 100644 --- a/tests/lean/rewrite.lean +++ b/tests/lean/rewrite.lean @@ -54,3 +54,53 @@ exact h₁ h₃ example (α : Type) (p : Prop) (a b c : α) (h : p → a = b) : a = c := by rw [h _] -- should manifest goal `⊢ p`, like `rw [h]` would + +/-! +Testing the `occs` configuration argument. +-/ + +variable (f : Nat → Nat) (w : ∀ n, f n = 0) + +example : [f 1, f 2, f 1, f 2] = [0, 0, 0, 0] := by + rw (config := {occs := .pos [2]}) [w] + -- Because the metavariables are instantiated after finding the first occurrence, + -- even though this is rejected, with the current behaviour this rewrites the second `f 1`, + -- rather than the first `f 2`. + -- Arguably this behaviour should be changed. + trace_state + rw [w, w] + +example : [f 1, f 2, f 1, f 2] = [0, 0, 0, 0] := by + rw (config := {occs := .all}) [w] + trace_state -- expecting [0, f 2, 0, f 2] = [0, 0, 0, 0] + rw [w] + +example : [f 1, f 2, f 1, f 2] = [0, 0, 0, 0] := by + rw (config := {occs := .pos [1, 2]}) [w] + trace_state -- expecting [0, f 2, 0, f 2] = [0, 0, 0, 0] + -- After the first rewrite, the argument of `w` have been instantiated as `1`, + -- so the second eligible rewrite is the second `f 1`. + rw [w] + +example : [f 1, f 2, f 1, f 2] = [0, 0, 0, 0] := by + rw (config := {occs := .neg [1]}) [w] + -- Again, the rejected first occurrence nevertheless instantiates the metavariables. + -- Argubly the state here should be `[f 1, 0, f 1, 0] = [0, 0, 0, 0]`, + -- but for now if `[f 1, f 2, 0, f 2] = [0, 0, 0, 0]` + trace_state + rw [w, w] + +example : [f 1, f 2, f 1, f 2] = [0, 0, 0, 0] := by + -- Arguably should succeed giving `[f 1, f 2, 0, f 2] = [0, 0, 0, 0]` + -- but currently fails. + fail_if_success rw (config := {occs := .neg [1, 2]}) [w] + trace_state + rw [w, w] + +example : [f 1, f 2, f 1, f 2] = [0, 0, 0, 0] := by + rw (config := {occs := .neg [1, 3]}) [w] + -- Arguably should give `[f 1, 0, f 1, f 2] = [0, 0, 0, 0]` + -- but currently gives `[f 1, f 2, 0, f 2] = [0, 0, 0, 0]` + trace_state + rw [w, w] + diff --git a/tests/lean/rewrite.lean.expected.out b/tests/lean/rewrite.lean.expected.out index 058a43f1c8..3ffcdc373b 100644 --- a/tests/lean/rewrite.lean.expected.out +++ b/tests/lean/rewrite.lean.expected.out @@ -31,3 +31,21 @@ p : Prop a b c : α h : p → a = b ⊢ p +f : Nat → Nat +w : ∀ (n : Nat), f n = 0 +⊢ [f 1, f 2, 0, f 2] = [0, 0, 0, 0] +f : Nat → Nat +w : ∀ (n : Nat), f n = 0 +⊢ [0, f 2, 0, f 2] = [0, 0, 0, 0] +f : Nat → Nat +w : ∀ (n : Nat), f n = 0 +⊢ [0, f 2, 0, f 2] = [0, 0, 0, 0] +f : Nat → Nat +w : ∀ (n : Nat), f n = 0 +⊢ [f 1, f 2, 0, f 2] = [0, 0, 0, 0] +f : Nat → Nat +w : ∀ (n : Nat), f n = 0 +⊢ [f 1, f 2, f 1, f 2] = [0, 0, 0, 0] +f : Nat → Nat +w : ∀ (n : Nat), f n = 0 +⊢ [f 1, f 2, 0, f 2] = [0, 0, 0, 0]