From 5a57398f9ea0c7a0aeda68c3ea8ff2cab9bcc81b Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sat, 9 Nov 2024 10:30:04 -0800 Subject: [PATCH 1/2] feat: `change ... with` tactic This PR implements the `change ... with` tactic. Doing `change p with r` is essentially equivalent to `rewrite [show p = r by rfl]`. Closes #5116 --- src/Init/Conv.lean | 4 + src/Init/Tactics.lean | 27 +++- src/Lean/Elab/Tactic/Change.lean | 64 ++++++--- src/Lean/Elab/Tactic/Conv/Change.lean | 10 ++ tests/lean/run/change.lean | 199 ++++++++++++++++++++++++++ 5 files changed, 278 insertions(+), 26 deletions(-) diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean index 323abdf177e5..a776cc99828b 100644 --- a/src/Init/Conv.lean +++ b/src/Init/Conv.lean @@ -103,6 +103,10 @@ syntax (name := ext) "ext" (ppSpace colGt ident)* : conv assuming `t` and `t'` are definitionally equal. -/ syntax (name := change) "change " term : conv +/-- `change p with t` replaces all occurrences of `p` in the target with `t`, +assuming `p` and `t` are definitionally equal. -/ +syntax (name := changeWith) "change " term " with " term : conv + /-- `delta id1 id2 ...` unfolds all occurrences of `id1`, `id2`, ... in the target. Like the `delta` tactic, this ignores any definitional equations and uses primitive delta-reduction instead, which may result in leaking implementation details. diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 5550bf9673a0..175b25faed91 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -469,17 +469,36 @@ hypotheses or the goal. It can have one of the forms: syntax location := withPosition(ppGroup(" at" (locationWildcard <|> locationHyp))) /-- -* `change tgt'` will change the goal from `tgt` to `tgt'`, - assuming these are definitionally equal. -* `change t' at h` will change hypothesis `h : t` to have type `t'`, assuming +* `change tgt'` changes the target of the goal from `tgt` to `tgt'`, + assuming `tgt` and `tgt'` are definitionally equal. +* `change t' at h` will change the hypothesis `h : t` to have type `t'`, assuming `t` and `t'` are definitionally equal. + +The types `tgt'` and `t'` may contain placeholders. +The tactic `change tgt'` is equivalent to `refine show tgt' from ?_`. + +## Examples + +For example, if `n : Nat` and the current goal is `⊢ n + 2 = 2`, then +```lean +change _ + 1 = _ +``` +changes the goal to `⊢ n + 1 + 1 = 2`. + +The tactic also applies to hypotheses. If `h : n + 2 = 2` and `h' : n + 3 = 4` +are hypotheses, then +```lean +change _ + 1 = _ at h h' +``` +changes their types to be `h : n + 1 + 1 = 2` and `h' : n + 2 + 1 = 4`. +Notice that the placeholders in `_ + 1 = _` are not constant across hypotheses. -/ syntax (name := change) "change " term (location)? : tactic /-- * `change a with b` will change occurrences of `a` to `b` in the goal, assuming `a` and `b` are definitionally equal. -* `change a with b at h` similarly changes `a` to `b` in the type of hypothesis `h`. +* `change a with b at h` similarly changes occurrences of `a` to `b` in the type of hypothesis `h`. -/ syntax (name := changeWith) "change " term " with " term (location)? : tactic diff --git a/src/Lean/Elab/Tactic/Change.lean b/src/Lean/Elab/Tactic/Change.lean index 03796f739213..5e1e85f58630 100644 --- a/src/Lean/Elab/Tactic/Change.lean +++ b/src/Lean/Elab/Tactic/Change.lean @@ -4,13 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Kyle Miller -/ prelude +import Lean.Meta.KAbstract import Lean.Meta.Tactic.Replace import Lean.Elab.Tactic.Location namespace Lean.Elab.Tactic open Meta /-! -# Implementation of the `change` tactic +# Implementations of the `change` tactics -/ /-- @@ -38,27 +39,6 @@ def elabChange (e : Expr) (p : Term) : TacticM Expr := do is not definitionally equal to target{indentExpr tgt}" instantiateMVars p -/-- `change` can be used to replace the main goal or its hypotheses with -different, yet definitionally equal, goal or hypotheses. - -For example, if `n : Nat` and the current goal is `⊢ n + 2 = 2`, then -```lean -change _ + 1 = _ -``` -changes the goal to `⊢ n + 1 + 1 = 2`. - -The tactic also applies to hypotheses. If `h : n + 2 = 2` and `h' : n + 3 = 4` -are hypotheses, then -```lean -change _ + 1 = _ at h h' -``` -changes their types to be `h : n + 1 + 1 = 2` and `h' : n + 2 + 1 = 4`. - -Change is like `refine` in that every placeholder needs to be solved for by unification, -but using named placeholders or `?_` results in `change` to creating new goals. - -The tactic `show e` is interchangeable with `change e`, where the pattern `e` is applied to -the main goal. -/ @[builtin_tactic change] elab_rules : tactic | `(tactic| change $newType:term $[$loc:location]?) => do withLocation (expandOptLocation (Lean.mkOptionalNode loc)) @@ -72,4 +52,44 @@ the main goal. -/ return (← mvarId.replaceTargetDefEq tgt') :: mvars) (failed := fun _ => throwError "'change' tactic failed") +/-- +Replaces each occurrence of `p` in `e` with `t`. +This is roughly the same as doing `rewrite [show p = t by rfl]` on `e`. +-/ +def elabChangeWith (e : Expr) (p t : Term) : TacticM Expr := do + -- Set `mayPostpone := true` like when elaborating `rewrite` rules. + let (p, t) ← runTermElab (mayPostpone := true) do + let p ← Term.elabTerm p none + let t ← Term.elabTermEnsuringType t (← inferType p) + return (p, t) + let p ← instantiateMVars p + let e' ← kabstract e p + unless e'.hasLooseBVars do + throwError "\ + 'change with' tactic failed, did not find instance of the pattern{indentExpr p}\n\ + in the expression{indentExpr e}" + Term.synthesizeSyntheticMVarsNoPostponing + withAssignableSyntheticOpaque do + unless ← isDefEq p t do + let (p, t) ← addPPExplicitToExposeDiff p t + throwError "\ + 'change with' tactic failed, pattern{indentExpr p}\n\ + is not definitionally equal to replacement{indentExpr t}" + instantiateMVars (e'.instantiate1 t) + +@[builtin_tactic changeWith] elab_rules : tactic + | `(tactic| change $p:term with $t:term $[$loc:location]?) => do + withLocation (expandOptLocation (mkOptionalNode loc)) + (atLocal := fun h => do + let hTy ← h.getType + let (hTy', mvars) ← withCollectingNewGoalsFrom (elabChangeWith hTy p t) (← getMainTag) `change + liftMetaTactic fun mvarId => do + return (← mvarId.changeLocalDecl h hTy') :: mvars) + (atTarget := do + let g ← popMainGoal + let (e', mvars) ← withCollectingNewGoalsFrom (elabChangeWith (← g.getType) p t) (← g.getTag) `change + let g ← g.replaceTargetDefEq e' + pushGoals (g :: mvars)) + (failed := fun _ => throwError "'change with' tactic failed") + end Lean.Elab.Tactic diff --git a/src/Lean/Elab/Tactic/Conv/Change.lean b/src/Lean/Elab/Tactic/Conv/Change.lean index 2daa813e92f0..3d79fc1cda72 100644 --- a/src/Lean/Elab/Tactic/Conv/Change.lean +++ b/src/Lean/Elab/Tactic/Conv/Change.lean @@ -7,6 +7,7 @@ prelude import Lean.Elab.Tactic.ElabTerm import Lean.Elab.Tactic.Change import Lean.Elab.Tactic.Conv.Basic +import Lean.Elab.Tactic.Change namespace Lean.Elab.Tactic.Conv open Meta @@ -21,4 +22,13 @@ open Meta changeLhs lhs' | _ => throwUnsupportedSyntax +@[builtin_tactic Lean.Parser.Tactic.Conv.changeWith] def evalChangeWith : Tactic + | `(conv| change $p:term with $t:term) => do + let lhs ← getLhs + let mvarCounterSaved := (← getMCtx).mvarCounter + let lhs' ← elabChangeWith lhs p t + logUnassignedAndAbort (← filterOldMVars (← getMVars lhs') mvarCounterSaved) + changeLhs lhs' + | _ => throwUnsupportedSyntax + end Lean.Elab.Tactic.Conv diff --git a/tests/lean/run/change.lean b/tests/lean/run/change.lean index 4f5d9eb00e21..0cb36ac76784 100644 --- a/tests/lean/run/change.lean +++ b/tests/lean/run/change.lean @@ -1,3 +1,6 @@ +/-! +# Tests for the `change` tactics +-/ private axiom test_sorry : ∀ {α}, α @@ -209,3 +212,199 @@ example (a b c d : Nat) : a + b + c = d := by let e := ?mvar trace_state exact test_sorry + + +/-! +`change with`, basic test +-/ +example : 1 + 2 = 3 := by + change 2 with 1 + 1 + guard_target =ₛ 1 + (1 + 1) = 3 + rfl + +/-! +`change with`, new `let` binding +-/ +example : 1 + 2 = 3 := by + let x := 2 + change 2 with x + guard_target =ₛ 1 + x = 3 + rfl + +/-! +`change with`, no change throws error +-/ +/-- +error: 'change with' tactic failed, did not find instance of the pattern + 4 +in the expression + 1 + 2 = 3 +-/ +#guard_msgs in example : 1 + 2 = 3 := by + change 4 with 2 + 2 + +/-! +`change with`, basic test at hypothesis +-/ +example (h : 1 + 2 = 3) : True := by + change 2 with 1 + 1 at h + guard_hyp h :ₛ 1 + (1 + 1) = 3 + trivial + +/-! +`change with`, new `let` binding at hypothesis +-/ +example (h : 1 + 2 = 3) : True := by + let x := 2 + change 2 with x at h + guard_hyp h :ₛ 1 + x = 3 + trivial + +/-! +`change with`, no change at hypothesis throws error +-/ +/-- +error: 'change with' tactic failed, did not find instance of the pattern + 4 +in the expression + 1 + 2 = 3 +-/ +#guard_msgs in example (h : 1 + 2 = 3) : True := by + change 4 with 2 + 2 at h + +/-! +`change with at *` +-/ +/-- +info: x : Nat := 2 +h : 1 + x = 3 +⊢ 1 + x = 3 +-/ +#guard_msgs in example (h : 1 + 2 = 3) : 1 + 2 = 3 := by + let x := 2 + change 2 with x at * + trace_state + exact h + +/-! +`change with at *`, no change at hypothesis, no permutation of hypotheses +-/ +/-- +info: _h : 1 + 2 = 3 +x : Nat := 2 +⊢ 4 + 2 = 6 +-/ +#guard_msgs in example (_h : 1 + 2 = 3) : 4 + 2 = 6 := by + let x := 2 + change 4 with 4 at * + trace_state + rfl + +/-! +`change with`, not-defeq replacement +-/ +/-- +error: 'change with' tactic failed, pattern + 1 +is not definitionally equal to replacement + 2 +-/ +#guard_msgs in example : 1 = 2 := by + change 1 with 2 + +/-! +`change with`, replacement doesn't have correct type +-/ +/-- +error: type mismatch + Nat.zero +has type + Nat : Type +but is expected to have type + Bool : Type +-/ +#guard_msgs in example : true = true := by + change true with Nat.zero + fail "should not get here" + +/-! +`change with`, replacement has a metavariable +-/ +example : 1 + 2 = 3 := by + change 2 with _ + 1 + guard_target =ₛ 1 + (1 + 1) = 3 + rfl + +/-! +`change with at *`, pattern and replacement have metavariables, different solutions each time +-/ +/-- +info: h : 4 + 1 + 6 = 11 +⊢ 0 + 1 + 2 = 3 +-/ +#guard_msgs in example (h : 5 + 6 = 11) : 1 + 2 = 3 := by + change OfNat.ofNat _ with _ + 1 at * + trace_state + rfl + +/-! +`change with` can get the type from the target expression +-/ +example : (1 : Int) + 2 = 3 := by + change 2 with 1 + 1 + guard_target =ₛ (1 : Int) + (1 + 1) = 3 + rfl + +/-! +## Conv mode +-/ + +/-! +conv `change with` +-/ + +example (a : Nat) : 2 + (2 + 2) = a := by + conv => + enter [1,2] + change 2 with 1 + 1 + guard_target =ₛ 2 + ((1 + 1) + (1 + 1)) = a + conv => + enter [1,2,1] + change 1 with 0 + 1 + guard_target =ₛ 2 + (((0 + 1) + (0 + 1)) + (1 + 1)) = a + exact test_sorry + +/-! +conv `change with` doesn't allow unsolved metavariables +-/ +/-- +error: don't know how to synthesize placeholder for argument 'e' +context: +case foo +a : Nat +⊢ Nat +--- +error: unsolved goals +a : Nat +⊢ 2 = a +-/ +#guard_msgs in +example (a : Nat) : 2 = a := by + conv => + change 2 with (if True then 2 else ?foo) + +/-! +conv `change with` allows metavariables if they're solved for +-/ +/-- +info: a : Nat +x : Nat := 2 +⊢ 2 = a +-/ +#guard_msgs in +example (a : Nat) : 2 = a := by + conv => + change 2 with ?two + let x := ?two + trace_state + exact test_sorry From 0f1bfecedeecaaa00cacb48ec0983ec7ca41f963 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sat, 16 Nov 2024 19:20:24 -0800 Subject: [PATCH 2/2] change with -> change_matching with --- src/Init/Conv.lean | 4 +- src/Init/Tactics.lean | 6 +- src/Lean/Elab/Tactic/Change.lean | 46 +++--- src/Lean/Elab/Tactic/Conv/Change.lean | 6 +- stage0/src/stdlib_flags.h | 2 +- tests/lean/run/change.lean | 197 -------------------------- 6 files changed, 38 insertions(+), 223 deletions(-) diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean index a776cc99828b..4f4cac070ffc 100644 --- a/src/Init/Conv.lean +++ b/src/Init/Conv.lean @@ -103,9 +103,9 @@ syntax (name := ext) "ext" (ppSpace colGt ident)* : conv assuming `t` and `t'` are definitionally equal. -/ syntax (name := change) "change " term : conv -/-- `change p with t` replaces all occurrences of `p` in the target with `t`, +/-- `change_matching p with t` replaces all occurrences of `p` in the target with `t`, assuming `p` and `t` are definitionally equal. -/ -syntax (name := changeWith) "change " term " with " term : conv +syntax (name := changeMatching) "change_matching " term " with " term : conv /-- `delta id1 id2 ...` unfolds all occurrences of `id1`, `id2`, ... in the target. Like the `delta` tactic, this ignores any definitional equations and uses diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 175b25faed91..e11aaf0ff341 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -496,11 +496,11 @@ Notice that the placeholders in `_ + 1 = _` are not constant across hypotheses. syntax (name := change) "change " term (location)? : tactic /-- -* `change a with b` will change occurrences of `a` to `b` in the goal, +* `change_matching a with b` will change occurrences of `a` to `b` in the goal, assuming `a` and `b` are definitionally equal. -* `change a with b at h` similarly changes occurrences of `a` to `b` in the type of hypothesis `h`. +* `change_matching a with b at h` similarly changes occurrences of `a` to `b` in the type of hypothesis `h`. -/ -syntax (name := changeWith) "change " term " with " term (location)? : tactic +syntax (name := changeMatching) "change_matching " term " with " term (location)? : tactic /-- If `thm` is a theorem `a = b`, then as a rewrite rule, diff --git a/src/Lean/Elab/Tactic/Change.lean b/src/Lean/Elab/Tactic/Change.lean index 5e1e85f58630..c44fe9f075ea 100644 --- a/src/Lean/Elab/Tactic/Change.lean +++ b/src/Lean/Elab/Tactic/Change.lean @@ -33,10 +33,10 @@ def elabChange (e : Expr) (p : Term) : TacticM Expr := do pure p withAssignableSyntheticOpaque do unless ← isDefEq p e do - let (p, tgt) ← addPPExplicitToExposeDiff p e + let (p, e) ← addPPExplicitToExposeDiff p e throwError "\ 'change' tactic failed, pattern{indentExpr p}\n\ - is not definitionally equal to target{indentExpr tgt}" + is not definitionally equal to target{indentExpr e}" instantiateMVars p @[builtin_tactic change] elab_rules : tactic @@ -45,18 +45,24 @@ def elabChange (e : Expr) (p : Term) : TacticM Expr := do (atLocal := fun h => do let (hTy', mvars) ← withCollectingNewGoalsFrom (elabChange (← h.getType) newType) (← getMainTag) `change liftMetaTactic fun mvarId => do - return (← mvarId.changeLocalDecl h hTy') :: mvars) + if ← occursCheck mvarId hTy' then + return (← mvarId.changeLocalDecl h hTy') :: mvars + else + throwError "occurs check failed, expression{indentExpr hTy'}\ncontains the goal {Expr.mvar mvarId}") (atTarget := do let (tgt', mvars) ← withCollectingNewGoalsFrom (elabChange (← getMainTarget) newType) (← getMainTag) `change liftMetaTactic fun mvarId => do - return (← mvarId.replaceTargetDefEq tgt') :: mvars) + if ← occursCheck mvarId tgt' then + return (← mvarId.replaceTargetDefEq tgt') :: mvars + else + throwError "occurs check failed, expression{indentExpr tgt'}\ncontains the goal {Expr.mvar mvarId}") (failed := fun _ => throwError "'change' tactic failed") /-- Replaces each occurrence of `p` in `e` with `t`. -This is roughly the same as doing `rewrite [show p = t by rfl]` on `e`. +This is roughly like doing `rewrite [show p = t by rfl]` on `e`, but it does not require a type-correct motive. -/ -def elabChangeWith (e : Expr) (p t : Term) : TacticM Expr := do +def elabChangeMatching (e : Expr) (p t : Term) : TacticM Expr := do -- Set `mayPostpone := true` like when elaborating `rewrite` rules. let (p, t) ← runTermElab (mayPostpone := true) do let p ← Term.elabTerm p none @@ -66,30 +72,36 @@ def elabChangeWith (e : Expr) (p t : Term) : TacticM Expr := do let e' ← kabstract e p unless e'.hasLooseBVars do throwError "\ - 'change with' tactic failed, did not find instance of the pattern{indentExpr p}\n\ + 'change_matching' tactic failed, did not find instance of the pattern{indentExpr p}\n\ in the expression{indentExpr e}" + -- Now that `kabstract` has unified `p` with a subterm of `e`, make sure elaboration is complete. Term.synthesizeSyntheticMVarsNoPostponing withAssignableSyntheticOpaque do unless ← isDefEq p t do let (p, t) ← addPPExplicitToExposeDiff p t throwError "\ - 'change with' tactic failed, pattern{indentExpr p}\n\ + 'change_matching' tactic failed, pattern{indentExpr p}\n\ is not definitionally equal to replacement{indentExpr t}" instantiateMVars (e'.instantiate1 t) -@[builtin_tactic changeWith] elab_rules : tactic - | `(tactic| change $p:term with $t:term $[$loc:location]?) => do +@[builtin_tactic changeMatching] elab_rules : tactic + | `(tactic| change_matching $p:term with $t:term $[$loc:location]?) => do withLocation (expandOptLocation (mkOptionalNode loc)) (atLocal := fun h => do let hTy ← h.getType - let (hTy', mvars) ← withCollectingNewGoalsFrom (elabChangeWith hTy p t) (← getMainTag) `change + let (hTy', mvars) ← withCollectingNewGoalsFrom (elabChangeMatching hTy p t) (← getMainTag) `change_matching liftMetaTactic fun mvarId => do - return (← mvarId.changeLocalDecl h hTy') :: mvars) + if ← occursCheck mvarId hTy' then + return (← mvarId.changeLocalDecl h hTy') :: mvars + else + throwError "occurs check failed, expression{indentExpr hTy'}\ncontains the goal {Expr.mvar mvarId}") (atTarget := do - let g ← popMainGoal - let (e', mvars) ← withCollectingNewGoalsFrom (elabChangeWith (← g.getType) p t) (← g.getTag) `change - let g ← g.replaceTargetDefEq e' - pushGoals (g :: mvars)) - (failed := fun _ => throwError "'change with' tactic failed") + let (tgt', mvars) ← withCollectingNewGoalsFrom (elabChangeMatching (← getMainTarget) p t) (← getMainTag) `change_matching + liftMetaTactic fun mvarId => do + if ← occursCheck mvarId tgt' then + return (← mvarId.replaceTargetDefEq tgt') :: mvars + else + throwError "occurs check failed, expression{indentExpr tgt'}\ncontains the goal {Expr.mvar mvarId}") + (failed := fun _ => throwError "'change_matching' tactic failed") end Lean.Elab.Tactic diff --git a/src/Lean/Elab/Tactic/Conv/Change.lean b/src/Lean/Elab/Tactic/Conv/Change.lean index 3d79fc1cda72..0c7f3a9ab736 100644 --- a/src/Lean/Elab/Tactic/Conv/Change.lean +++ b/src/Lean/Elab/Tactic/Conv/Change.lean @@ -22,11 +22,11 @@ open Meta changeLhs lhs' | _ => throwUnsupportedSyntax -@[builtin_tactic Lean.Parser.Tactic.Conv.changeWith] def evalChangeWith : Tactic - | `(conv| change $p:term with $t:term) => do +@[builtin_tactic Lean.Parser.Tactic.Conv.changeMatching] def evalChangeMatching : Tactic + | `(conv| change_matching $p:term with $t:term) => do let lhs ← getLhs let mvarCounterSaved := (← getMCtx).mvarCounter - let lhs' ← elabChangeWith lhs p t + let lhs' ← elabChangeMatching lhs p t logUnassignedAndAbort (← filterOldMVars (← getMVars lhs') mvarCounterSaved) changeLhs lhs' | _ => throwUnsupportedSyntax diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 0699845ba452..658ab0874e68 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -8,7 +8,7 @@ options get_default_options() { // switch to `true` for ABI-breaking changes affecting meta code opts = opts.update({"interpreter", "prefer_native"}, false); // switch to `true` for changing built-in parsers used in quotations - opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false); + opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true); // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax // with custom precheck hooks were affected opts = opts.update({"quotPrecheck"}, true); diff --git a/tests/lean/run/change.lean b/tests/lean/run/change.lean index 0cb36ac76784..8966413471e2 100644 --- a/tests/lean/run/change.lean +++ b/tests/lean/run/change.lean @@ -4,7 +4,6 @@ private axiom test_sorry : ∀ {α}, α -set_option linter.missingDocs false set_option pp.mvars false example : n + 2 = m := by @@ -212,199 +211,3 @@ example (a b c d : Nat) : a + b + c = d := by let e := ?mvar trace_state exact test_sorry - - -/-! -`change with`, basic test --/ -example : 1 + 2 = 3 := by - change 2 with 1 + 1 - guard_target =ₛ 1 + (1 + 1) = 3 - rfl - -/-! -`change with`, new `let` binding --/ -example : 1 + 2 = 3 := by - let x := 2 - change 2 with x - guard_target =ₛ 1 + x = 3 - rfl - -/-! -`change with`, no change throws error --/ -/-- -error: 'change with' tactic failed, did not find instance of the pattern - 4 -in the expression - 1 + 2 = 3 --/ -#guard_msgs in example : 1 + 2 = 3 := by - change 4 with 2 + 2 - -/-! -`change with`, basic test at hypothesis --/ -example (h : 1 + 2 = 3) : True := by - change 2 with 1 + 1 at h - guard_hyp h :ₛ 1 + (1 + 1) = 3 - trivial - -/-! -`change with`, new `let` binding at hypothesis --/ -example (h : 1 + 2 = 3) : True := by - let x := 2 - change 2 with x at h - guard_hyp h :ₛ 1 + x = 3 - trivial - -/-! -`change with`, no change at hypothesis throws error --/ -/-- -error: 'change with' tactic failed, did not find instance of the pattern - 4 -in the expression - 1 + 2 = 3 --/ -#guard_msgs in example (h : 1 + 2 = 3) : True := by - change 4 with 2 + 2 at h - -/-! -`change with at *` --/ -/-- -info: x : Nat := 2 -h : 1 + x = 3 -⊢ 1 + x = 3 --/ -#guard_msgs in example (h : 1 + 2 = 3) : 1 + 2 = 3 := by - let x := 2 - change 2 with x at * - trace_state - exact h - -/-! -`change with at *`, no change at hypothesis, no permutation of hypotheses --/ -/-- -info: _h : 1 + 2 = 3 -x : Nat := 2 -⊢ 4 + 2 = 6 --/ -#guard_msgs in example (_h : 1 + 2 = 3) : 4 + 2 = 6 := by - let x := 2 - change 4 with 4 at * - trace_state - rfl - -/-! -`change with`, not-defeq replacement --/ -/-- -error: 'change with' tactic failed, pattern - 1 -is not definitionally equal to replacement - 2 --/ -#guard_msgs in example : 1 = 2 := by - change 1 with 2 - -/-! -`change with`, replacement doesn't have correct type --/ -/-- -error: type mismatch - Nat.zero -has type - Nat : Type -but is expected to have type - Bool : Type --/ -#guard_msgs in example : true = true := by - change true with Nat.zero - fail "should not get here" - -/-! -`change with`, replacement has a metavariable --/ -example : 1 + 2 = 3 := by - change 2 with _ + 1 - guard_target =ₛ 1 + (1 + 1) = 3 - rfl - -/-! -`change with at *`, pattern and replacement have metavariables, different solutions each time --/ -/-- -info: h : 4 + 1 + 6 = 11 -⊢ 0 + 1 + 2 = 3 --/ -#guard_msgs in example (h : 5 + 6 = 11) : 1 + 2 = 3 := by - change OfNat.ofNat _ with _ + 1 at * - trace_state - rfl - -/-! -`change with` can get the type from the target expression --/ -example : (1 : Int) + 2 = 3 := by - change 2 with 1 + 1 - guard_target =ₛ (1 : Int) + (1 + 1) = 3 - rfl - -/-! -## Conv mode --/ - -/-! -conv `change with` --/ - -example (a : Nat) : 2 + (2 + 2) = a := by - conv => - enter [1,2] - change 2 with 1 + 1 - guard_target =ₛ 2 + ((1 + 1) + (1 + 1)) = a - conv => - enter [1,2,1] - change 1 with 0 + 1 - guard_target =ₛ 2 + (((0 + 1) + (0 + 1)) + (1 + 1)) = a - exact test_sorry - -/-! -conv `change with` doesn't allow unsolved metavariables --/ -/-- -error: don't know how to synthesize placeholder for argument 'e' -context: -case foo -a : Nat -⊢ Nat ---- -error: unsolved goals -a : Nat -⊢ 2 = a --/ -#guard_msgs in -example (a : Nat) : 2 = a := by - conv => - change 2 with (if True then 2 else ?foo) - -/-! -conv `change with` allows metavariables if they're solved for --/ -/-- -info: a : Nat -x : Nat := 2 -⊢ 2 = a --/ -#guard_msgs in -example (a : Nat) : 2 = a := by - conv => - change 2 with ?two - let x := ?two - trace_state - exact test_sorry