merge master

We previously had the syntax for `change` and `change at`, but no
implementation.

This moves Kyle's implementation from Std.

This also changes the `changeLocalDecl` function to push nodes to the
infotree about FVar aliases.

---------

Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>

src/Init/Tactics.lean

@@ -207,6 +207,28 @@ the first matching constructor, or else fails.
 -/
 syntax (name := constructor) "constructor" : tactic
 
+/--
+Applies the second constructor when
+the goal is an inductive type with exactly two constructors, or fails otherwise.
+```
+example : True ∨ False := by
+  left
+  trivial
+```
+-/
+syntax (name := left) "left" : tactic
+
+/--
+Applies the second constructor when
+the goal is an inductive type with exactly two constructors, or fails otherwise.
+```
+example {p q : Prop} (h : q) : p ∨ q := by
+  right
+  exact h
+```
+-/
+syntax (name := right) "right" : tactic
+
 /--
 * `case tag => tac` focuses on the goal with case name `tag` and solves it using `tac`,
   or else fails.
@@ -872,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

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

src/Lean/Elab/BuiltinCommand.lean

@@ -722,6 +722,8 @@ opaque elabEval : CommandElab
   match stx with
   | `($doc:docComment add_decl_doc $id) =>
     let declName ← resolveGlobalConstNoOverloadWithInfo id
+    unless ((← getEnv).getModuleIdxFor? declName).isNone do
+      throwError "invalid 'add_decl_doc', declaration is in an imported module"
     if let .none ← findDeclarationRangesCore? declName then
       -- this is only relevant for declarations added without a declaration range
       -- in particular `Quot.mk` et al which are added by `init_quot`

src/Lean/Elab/Command.lean

@@ -1,10 +1,11 @@
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
+Authors: Leonardo de Moura, Gabriel Ebner
 -/
 import Lean.Elab.Binders
 import Lean.Elab.SyntheticMVars
+import Lean.Elab.SetOption
 
 namespace Lean.Elab.Command
 
@@ -503,6 +504,49 @@ def expandDeclId (declId : Syntax) (modifiers : Modifiers) : CommandElabM Expand
 
 end Elab.Command
 
+open Elab Command MonadRecDepth
+
+/--
+Lifts an action in `CommandElabM` into `CoreM`, updating the traces and the environment.
+
+Commands that modify the processing of subsequent commands,
+such as `open` and `namespace` commands,
+only have an effect for the remainder of the `CommandElabM` computation passed here,
+and do not affect subsequent commands.
+-/
+def liftCommandElabM (cmd : CommandElabM α) : CoreM α := do
+  let (a, commandState) ←
+    cmd.run {
+      fileName := ← getFileName
+      fileMap := ← getFileMap
+      ref := ← getRef
+      tacticCache? := none
+    } |>.run {
+      env := ← getEnv
+      maxRecDepth := ← getMaxRecDepth
+      scopes := [{ header := "", opts := ← getOptions }]
+    }
+  modify fun coreState => { coreState with
+    traceState.traces := coreState.traceState.traces ++ commandState.traceState.traces
+    env := commandState.env
+  }
+  if let some err := commandState.messages.msgs.toArray.find? (·.severity matches .error) then
+    throwError err.data
+  pure a
+
+/--
+Given a command elaborator `cmd`, returns a new command elaborator that
+first evaluates any local `set_option ... in ...` clauses and then invokes `cmd` on what remains.
+-/
+partial def withSetOptionIn (cmd : CommandElab) : CommandElab := fun stx => do
+  if stx.getKind == ``Lean.Parser.Command.in &&
+     stx[0].getKind == ``Lean.Parser.Command.set_option then
+      let opts ← Elab.elabSetOption stx[0][1] stx[0][2]
+      Command.withScope (fun scope => { scope with opts }) do
+        withSetOptionIn cmd stx[1]
+  else
+    cmd stx
+
 export Elab.Command (Linter addLinter)
 
 end Lean

src/Lean/Elab/Inductive.lean

@@ -524,14 +524,14 @@ private def updateResultingUniverse (views : Array InductiveView) (numParams : N
 register_builtin_option bootstrap.inductiveCheckResultingUniverse : Bool := {
     defValue := true,
     group    := "bootstrap",
-    descr    := "by default the `inductive/structure commands report an error if the resulting universe is not zero, but may be zero for some universe parameters. Reason: unless this type is a subsingleton, it is hardly what the user wants since it can only eliminate into `Prop`. In the `Init` package, we define subsingletons, and we use this option to disable the check. This option may be deleted in the future after we improve the validator"
+    descr    := "by default the `inductive`/`structure` commands report an error if the resulting universe is not zero, but may be zero for some universe parameters. Reason: unless this type is a subsingleton, it is hardly what the user wants since it can only eliminate into `Prop`. In the `Init` package, we define subsingletons, and we use this option to disable the check. This option may be deleted in the future after we improve the validator"
 }
 
 def checkResultingUniverse (u : Level) : TermElabM Unit := do
   if bootstrap.inductiveCheckResultingUniverse.get (← getOptions) then
     let u ← instantiateLevelMVars u
     if !u.isZero && !u.isNeverZero then
-      throwError "invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u'{indentD u}"
+      throwError "invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u'){indentD u}"
 
 private def checkResultingUniverses (views : Array InductiveView) (numParams : Nat) (indTypes : List InductiveType) : TermElabM Unit := do
   let u := (← instantiateLevelMVars (← getResultingUniverse indTypes)).normalize

src/Lean/Elab/Tactic.lean

@@ -25,3 +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

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Lean.Meta.Tactic.Apply
 import Lean.Meta.Tactic.Assumption
 import Lean.Meta.Tactic.Contradiction
 import Lean.Meta.Tactic.Refl
@@ -323,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.
@@ -468,4 +475,10 @@ where
   | none    => throwIllFormedSyntax
   | some ms => IO.sleep ms.toUInt32
 
+@[builtin_tactic left] def evalLeft : Tactic := fun _stx => do
+  liftMetaTactic (fun g => g.nthConstructor `left 0 (some 2))
+
+@[builtin_tactic right] def evalRight : Tactic := fun _stx => do
+  liftMetaTactic (fun g => g.nthConstructor `right 1 (some 2))
+
 end Lean.Elab.Tactic

src/Lean/Elab/Tactic/Change.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2023 Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+import Lean.Meta.Tactic.Replace
+import Lean.Elab.Tactic.Location
+
+namespace Lean.Elab.Tactic
+open Meta
+/-!
+# Implementation of the `change` tactic
+-/
+
+/-- `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))
+      (atLocal := fun h => do
+        let hTy ← h.getType
+        -- This is a hack to get the new type to elaborate in the same sort of way that
+        -- it would for a `show` expression for the goal.
+        let mvar ← mkFreshExprMVar none
+        let (_, mvars) ← elabTermWithHoles
+                          (← `(term | show $newType from $(← Term.exprToSyntax mvar))) hTy `change
+        liftMetaTactic fun mvarId => do
+          return (← mvarId.changeLocalDecl h (← inferType mvar)) :: mvars)
+      (atTarget := evalTactic <| ← `(tactic| refine_lift show $newType from ?_))
+      (failed := fun _ => throwError "change tactic failed")
+
+end Lean.Elab.Tactic

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

src/Lean/Meta/DiscrTree.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
+Authors: Leonardo de Moura, Jannis Limperg, Scott Morrison
 -/
 import Lean.Meta.WHNF
 import Lean.Meta.Transform
@@ -450,6 +450,18 @@ def insert [BEq α] (d : DiscrTree α) (e : Expr) (v : α) (config : WhnfCoreCon
   let keys ← mkPath e config
   return d.insertCore keys v
 
+/--
+Inserts a value into a discrimination tree,
+but only if its key is not of the form `#[*]` or `#[=, *, *, *]`.
+-/
+def insertIfSpecific [BEq α] (d : DiscrTree α) (e : Expr) (v : α) (config : WhnfCoreConfig) : MetaM (DiscrTree α) := do
+  let keys ← mkPath e config
+  return if keys == #[Key.star] || keys == #[Key.const `Eq 3, Key.star, Key.star, Key.star] then
+    d
+  else
+    d.insertCore keys v
+
+
 private def getKeyArgs (e : Expr) (isMatch root : Bool) (config : WhnfCoreConfig) : MetaM (Key × Array Expr) := do
   let e ← reduceDT e root config
   unless root do
@@ -676,4 +688,124 @@ where
         | .arrow => visitNonStar .other #[] (← visitNonStar k args (← visitStar result))
         | _      => visitNonStar k args (← visitStar result)
 
-end Lean.Meta.DiscrTree
+namespace Trie
+
+-- `Inhabited` instance to allow `partial` definitions below.
+private local instance [Monad m] : Inhabited (σ → β → m σ) := ⟨fun s _ => pure s⟩
+
+/--
+Monadically fold the keys and values stored in a `Trie`.
+-/
+partial def foldM [Monad m] (initialKeys : Array Key)
+    (f : σ → Array Key → α → m σ) : (init : σ) → Trie α → m σ
+  | init, Trie.node vs children => do
+    let s ← vs.foldlM (init := init) fun s v => f s initialKeys v
+    children.foldlM (init := s) fun s (k, t) =>
+      t.foldM (initialKeys.push k) f s
+
+/--
+Fold the keys and values stored in a `Trie`.
+-/
+@[inline]
+def fold (initialKeys : Array Key) (f : σ → Array Key → α → σ) (init : σ) (t : Trie α) : σ :=
+  Id.run <| t.foldM initialKeys (init := init) fun s k a => return f s k a
+
+/--
+Monadically fold the values stored in a `Trie`.
+-/
+partial def foldValuesM [Monad m] (f : σ → α → m σ) : (init : σ) → Trie α → m σ
+  | init, node vs children => do
+    let s ← vs.foldlM (init := init) f
+    children.foldlM (init := s) fun s (_, c) => c.foldValuesM (init := s) f
+
+/--
+Fold the values stored in a `Trie`.
+-/
+@[inline]
+def foldValues (f : σ → α → σ) (init : σ) (t : Trie α) : σ :=
+  Id.run <| t.foldValuesM (init := init) f
+
+/--
+The number of values stored in a `Trie`.
+-/
+partial def size : Trie α → Nat
+  | Trie.node vs children =>
+    children.foldl (init := vs.size) fun n (_, c) => n + size c
+
+end Trie
+
+
+/--
+Monadically fold over the keys and values stored in a `DiscrTree`.
+-/
+@[inline]
+def foldM [Monad m] (f : σ → Array Key → α → m σ) (init : σ)
+    (t : DiscrTree α) : m σ :=
+  t.root.foldlM (init := init) fun s k t => t.foldM #[k] (init := s) f
+
+/--
+Fold over the keys and values stored in a `DiscrTree`
+-/
+@[inline]
+def fold (f : σ → Array Key → α → σ) (init : σ) (t : DiscrTree α) : σ :=
+  Id.run <| t.foldM (init := init) fun s keys a => return f s keys a
+
+/--
+Monadically fold over the values stored in a `DiscrTree`.
+-/
+@[inline]
+def foldValuesM [Monad m] (f : σ → α → m σ) (init : σ) (t : DiscrTree α) :
+    m σ :=
+  t.root.foldlM (init := init) fun s _ t => t.foldValuesM (init := s) f
+
+/--
+Fold over the values stored in a `DiscrTree`.
+-/
+@[inline]
+def foldValues (f : σ → α → σ) (init : σ) (t : DiscrTree α) : σ :=
+  Id.run <| t.foldValuesM (init := init) f
+
+/--
+Check for the presence of a value satisfying a predicate.
+-/
+@[inline]
+def containsValueP [BEq α] (t : DiscrTree α) (f : α → Bool) : Bool :=
+  t.foldValues (init := false) fun r a => r || f a
+
+/--
+Extract the values stored in a `DiscrTree`.
+-/
+@[inline]
+def values (t : DiscrTree α) : Array α :=
+  t.foldValues (init := #[]) fun as a => as.push a
+
+/--
+Extract the keys and values stored in a `DiscrTree`.
+-/
+@[inline]
+def toArray (t : DiscrTree α) : Array (Array Key × α) :=
+  t.fold (init := #[]) fun as keys a => as.push (keys, a)
+
+/--
+Get the number of values stored in a `DiscrTree`. O(n) in the size of the tree.
+-/
+@[inline]
+def size (t : DiscrTree α) : Nat :=
+  t.root.foldl (init := 0) fun n _ t => n + t.size
+
+variable {m : Type → Type} [Monad m]
+
+/-- Apply a monadic function to the array of values at each node in a `DiscrTree`. -/
+partial def Trie.mapArraysM (t : DiscrTree.Trie α) (f : Array α → m (Array β)) :
+    m (DiscrTree.Trie β) :=
+  match t with
+  | .node vs children =>
+    return .node (← f vs) (← children.mapM fun (k, t') => do pure (k, ← t'.mapArraysM f))
+
+/-- Apply a monadic function to the array of values at each node in a `DiscrTree`. -/
+def mapArraysM (d : DiscrTree α) (f : Array α → m (Array β)) : m (DiscrTree β) := do
+  pure { root := ← d.root.mapM (fun t => t.mapArraysM f) }
+
+/-- Apply a function to the array of values at each node in a `DiscrTree`. -/
+def mapArrays (d : DiscrTree α) (f : Array α → Array β) : DiscrTree β :=
+  Id.run <| d.mapArraysM fun A => pure (f A)

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
+import Lean.Meta.Tactic.Congr
+import Lean.Meta.Tactic.Repeat

src/Lean/Meta/Tactic/Apply.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
+Authors: Leonardo de Moura, Siddhartha Gadgil
 -/
 import Lean.Util.FindMVar
 import Lean.Meta.SynthInstance
@@ -230,4 +230,25 @@ def _root_.Lean.MVarId.exfalso (mvarId : MVarId) : MetaM MVarId :=
     mvarId.assign (mkApp2 (mkConst ``False.elim [u]) target mvarIdNew)
     return mvarIdNew.mvarId!
 
+/--
+Apply the `n`-th constructor of the target type,
+checking that it is an inductive type,
+and that there are the expected number of constructors.
+-/
+def _root_.Lean.MVarId.nthConstructor
+    (name : Name) (idx : Nat) (expected? : Option Nat := none) (goal : MVarId) :
+    MetaM (List MVarId) := do
+  goal.withContext do
+    goal.checkNotAssigned name
+    matchConstInduct (← goal.getType').getAppFn
+      (fun _ => throwTacticEx name goal "target is not an inductive datatype")
+      fun ival us => do
+        if let some e := expected? then unless ival.ctors.length == e do
+          throwTacticEx name goal
+            s!"{name} tactic works for inductive types with exactly {e} constructors"
+        if h : idx < ival.ctors.length then
+          goal.apply <| mkConst ival.ctors[idx] us
+        else
+          throwTacticEx name goal s!"index {idx} out of bounds, only {ival.ctors.length} constructors"
+
 end Lean.Meta

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

src/Lean/Meta/Tactic/Replace.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Util.ForEachExpr
+import Lean.Elab.InfoTree.Main
 import Lean.Meta.AppBuilder
 import Lean.Meta.MatchUtil
 import Lean.Meta.Tactic.Util
@@ -139,29 +140,54 @@ def _root_.Lean.MVarId.change (mvarId : MVarId) (targetNew : Expr) (checkDefEq :
 def change (mvarId : MVarId) (targetNew : Expr) (checkDefEq := true) : MetaM MVarId := mvarId.withContext do
   mvarId.change targetNew checkDefEq
 
-/--
-Replace the type of the free variable `fvarId` with `typeNew`.
-If `checkDefEq = false`, this method assumes that `typeNew` is definitionally equal to `fvarId` type.
-If `checkDefEq = true`, throw an error if `typeNew` is not definitionally equal to `fvarId` type.
--/
-def _root_.Lean.MVarId.changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (checkDefEq := true) : MetaM MVarId := do
-  mvarId.checkNotAssigned `changeLocalDecl
-  let (xs, mvarId) ← mvarId.revert #[fvarId] true
+/-- Runs the continuation `k` after temporarily reverting some variables from the local context of a metavariable (identified by `mvarId`), then reintroduces local variables as specified by `k`.
+
+The argument `fvarIds` is an array of `fvarIds` to revert in the order specified. An error is thrown if they cannot be reverted in order.
+
+Once the local variables have been reverted, `k` is passed `mvarId` along with an array of local variables that were reverted. This array always has `fvarIds` as a prefix, but it may contain additional variables that were reverted due to dependencies. `k` returns a value, a goal, an array of _link variables_.
+
+Once `k` has completed, one variable is introduced for each link variable returned by `k`. If the returned variable is `none`, the variable is just introduced. If it is `some fv`, the variable is introduced and then linked as an alias of `fv` in the info tree. For example, having `k` return `fvars.map .some` as the link variables causes all reverted variables to be introduced and linked.
+
+Returns the value returned by `k` along with the resulting goal.
+ -/
+def _root_.Lean.MVarId.withReverted (mvarId : MVarId) (fvarIds : Array FVarId)
+    (k : MVarId → Array FVarId → MetaM (α × Array (Option FVarId) × MVarId))
+    (clearAuxDeclsInsteadOfRevert := false) : MetaM (α × MVarId) := do
+  let (xs, mvarId) ← mvarId.revert fvarIds true clearAuxDeclsInsteadOfRevert
+  let (r, xs', mvarId) ← k mvarId xs
+  let (ys, mvarId) ← mvarId.introNP xs'.size
   mvarId.withContext do
-    let numReverted := xs.size
-    let target ← mvarId.getType
+    for x? in xs', y in ys do
+      if let some x := x? then
+        Elab.pushInfoLeaf (.ofFVarAliasInfo { id := y, baseId := x, userName := ← y.getUserName })
+  return (r, mvarId)
+
+/--
+Replaces the type of the free variable `fvarId` with `typeNew`.
+
+If `checkDefEq` is `true` then an error is thrown if `typeNew` is not definitionally
+equal to the type of `fvarId`. Otherwise this function assumes `typeNew` and the type
+of `fvarId` are definitionally equal.
+
+This function is the same as `Lean.MVarId.changeLocalDecl` but makes sure to push substitution
+information into the info tree.
+-/
+def _root_.Lean.MVarId.changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr)
+    (checkDefEq := true) : MetaM MVarId := do
+  mvarId.checkNotAssigned `changeLocalDecl
+  let (_, mvarId) ← mvarId.withReverted #[fvarId] fun mvarId fvars => mvarId.withContext do
     let check (typeOld : Expr) : MetaM Unit := do
       if checkDefEq then
-        unless (← isDefEq typeNew typeOld) do
-          throwTacticEx `changeHypothesis mvarId m!"given type{indentExpr typeNew}\nis not definitionally equal to{indentExpr typeOld}"
-    let finalize (targetNew : Expr) : MetaM MVarId := do
-      let mvarId ← mvarId.replaceTargetDefEq targetNew
-      let (_, mvarId) ← mvarId.introNP numReverted
-      pure mvarId
-    match target with
-    | .forallE n d b c => do check d; finalize (mkForall n c typeNew b)
-    | .letE n t v b _  => do check t; finalize (mkLet n typeNew v b)
-    | _ => throwTacticEx `changeHypothesis mvarId "unexpected auxiliary target"
+        unless ← isDefEq typeNew typeOld do
+          throwTacticEx `changeLocalDecl mvarId
+            m!"given type{indentExpr typeNew}\nis not definitionally equal to{indentExpr typeOld}"
+    let finalize (targetNew : Expr) := do
+      return ((), fvars.map .some, ← mvarId.replaceTargetDefEq targetNew)
+    match ← mvarId.getType with
+    | .forallE n d b bi => do check d; finalize (.forallE n typeNew b bi)
+    | .letE n t v b ndep => do check t; finalize (.letE n typeNew v b ndep)
+    | _ => throwTacticEx `changeLocalDecl mvarId "unexpected auxiliary target"
+  return mvarId
 
 @[deprecated MVarId.changeLocalDecl]
 def changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (checkDefEq := true) : MetaM MVarId := do

tests/lean/docStr.lean

@@ -102,3 +102,6 @@ def printRangesTest : MetaM Unit := do
   printRanges `g.foo
 
 #eval printRangesTest
+
+/-- no dice -/
+add_decl_doc Nat.add

tests/lean/docStr.lean.expected.out

@@ -189,3 +189,4 @@ g.foo :=
                         charUtf16 := 44,
                         endPos := { line := 42, column := 47 },
                         endCharUtf16 := 47 } }
+docStr.lean:106:0-107:20: error: invalid 'add_decl_doc', declaration is in an imported module

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

tests/lean/run/change_tac.lean

@@ -0,0 +1,76 @@
+private axiom test_sorry : ∀ {α}, α
+
+example : n + 2 = m := by
+  change n + 1 + 1 = _
+  guard_target =ₛ n + 1 + 1 = m
+  exact test_sorry
+
+example (h : n + 2 = m) : False := by
+  change _ + 1 = _ at h
+  guard_hyp h :ₛ n + 1 + 1 = m
+  exact test_sorry
+
+example : n + 2 = m := by
+  fail_if_success change true
+  fail_if_success change _ + 3 = _
+  fail_if_success change _ * _ = _
+  change (_ : Nat) + _ = _
+  exact test_sorry
+
+-- `change ... at ...` allows placeholders to mean different things at different hypotheses
+example (h : n + 3 = m) (h' : n + 2 = m) : False := by
+  change _ + 1 = _ at h h'
+  guard_hyp h :ₛ n + 2 + 1 = m
+  guard_hyp h' :ₛ n + 1 + 1 = m
+  exact test_sorry
+
+-- `change ... at ...` preserves dependencies
+example (p : n + 2 = m → Type) (h : n + 2 = m) (x : p h) : false := by
+  change _ + 1 = _ at h
+  guard_hyp x :ₛ p h
+  exact test_sorry
+
+noncomputable example : Nat := by
+  fail_if_success change Type 1
+  exact test_sorry
+
+def foo (a b c : Nat) := if a < b then c else 0
+
+example : foo 1 2 3 = 3 := by
+  change (if _ then _ else _) = _
+  change ite _ _ _ = _
+  change (if _ < _ then _ else _) = _
+  change _ = (if true then 3 else 4)
+  rfl
+
+example (h : foo 1 2 3 = 4) : True := by
+  change ite _ _ _ = _ at h
+  guard_hyp h :ₛ ite (1 < 2) 3 0 = 4
+  trivial
+
+example (h : foo 1 2 3 = 4) : True := by
+  change (if _ then _ else _) = _ at h
+  guard_hyp h : (if 1 < 2 then 3 else 0) = 4
+  trivial
+
+example (α : Type) [LT α] (x : α) (h : x < x) : x < id x := by
+  change _ < _ -- can defer LT typeclass lookup, just like `show`
+  change _ < _ at h -- can defer LT typeclass lookup at h too
+  guard_target =ₛ x < id x
+  change _ < x
+  guard_target =ₛ x < x
+  exact h
+
+-- This example shows using named and anonymous placeholders to create a new goal.
+example (x y : Nat) (h : x = y) : True := by
+  change (if 1 < 2 then x else ?z + ?_) = y at h
+  rotate_left
+  · exact 4
+  · exact 37
+  guard_hyp h : (if 1 < 2 then x else 4 + 37) = y
+  · trivial
+
+example : let x := 22; let y : Nat := x; let z : Fin (y + 1) := 0; z.1 < y + 1 := by
+  intro x y z -- `z` was previously erroneously marked as unused
+  change _ at y
+  exact z.2

tests/lean/univInference.lean.expected.out

@@ -4,7 +4,7 @@ structure resulting type
   Type ?u
 recall that Lean only infers the resulting universe level automatically when there is a unique solution for the universe level constraints, consider explicitly providing the structure resulting universe level
 S6 : Sort (max w₁ w₂) → Type w₂ → Sort (max w₁ (w₂ + 1))
-univInference.lean:45:0-46:17: error: invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u'
+univInference.lean:45:0-46:17: error: invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u')
   max u v
 univInference.lean:65:2-65:22: error: failed to compute resulting universe level of inductive datatype, constructor 'Induct.S4.mk' has type
   {α : Sort u} → {β : Sort v} → α → β → S4 α β
@@ -13,7 +13,7 @@ parameter 'a' has type
 inductive type resulting type
   Type ?u
 recall that Lean only infers the resulting universe level automatically when there is a unique solution for the universe level constraints, consider explicitly providing the inductive type resulting universe level
-univInference.lean:73:0-74:22: error: invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u'
+univInference.lean:73:0-74:22: error: invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u')
   max u v
-univInference.lean:81:0-82:22: error: invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u'
+univInference.lean:81:0-82:22: error: invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u')
   max u v