fix: Make mframe, mspec and mvcgen hygienic (#9512)

This PR makes `mframe`, `mspec` and `mvcgen` respect hygiene.
Inaccessible stateful hypotheses can now be named with a new tactic
`mrename_i` that works analogously to `rename_i`.

src/Init/Tactics.lean

@@ -1996,6 +1996,13 @@ macro (name := mrevertMacro) (priority:=low) "mrevert" : tactic =>
   Macro.throwError "to use `mrevert`, please include `import Std.Tactic.Do`"
 
 
+/--
+`mrename_i` is like `rename_i`, but names inaccessible stateful hypotheses in a `Std.Do.SPred` goal.
+-/
+macro (name := mrenameIMacro) (priority:=low) "mrename_i" : tactic =>
+  Macro.throwError "to use `mrename_i`, please include `import Std.Tactic.Do`"
+
+
 /--
 `mspecialize` is like `specialize`, but operating on a stateful `Std.Do.SPred` goal.
 It specializes a hypothesis from the stateful context with hypotheses from either the pure

src/Lean/Elab/Tactic/Do/ProofMode.lean

@@ -16,6 +16,7 @@ import Lean.Elab.Tactic.Do.ProofMode.Pure
 import Lean.Elab.Tactic.Do.ProofMode.Frame
 import Lean.Elab.Tactic.Do.ProofMode.LeftRight
 import Lean.Elab.Tactic.Do.ProofMode.Constructor
+import Lean.Elab.Tactic.Do.ProofMode.RenameI
 import Lean.Elab.Tactic.Do.ProofMode.Specialize
 import Lean.Elab.Tactic.Do.ProofMode.Cases
 import Lean.Elab.Tactic.Do.ProofMode.Exfalso

src/Lean/Elab/Tactic/Do/ProofMode/Delab.lean

@@ -15,28 +15,43 @@ open Lean Expr Meta PrettyPrinter Delaborator SubExpr
 @[builtin_delab app.Std.Tactic.Do.MGoalEntails]
 private partial def delabMGoal : Delab := do
   -- delaborate
-  let (_, hyps) ← withAppFn ∘ withAppArg <| delabHypotheses ({}, #[])
+  let (_, _, hyps) ← withAppFn ∘ withAppArg <| delabHypotheses ({}, {}, #[])
   let target ← SPred.Notation.unpack (← withAppArg <| delab)
 
   -- build syntax
   return ⟨← `(Std.Tactic.Do.mgoalStx| $hyps.reverse* ⊢ₛ $target:term)⟩
 where
   delabHypotheses
-      (acc : NameMap Nat × Array (TSyntax ``mgoalHyp)) :
-      DelabM (NameMap Nat × Array (TSyntax ``mgoalHyp)) := do
+      (acc : NameMap Nat × NameMap Nat × Array (TSyntax ``mgoalHyp)) :
+      DelabM (NameMap Nat × NameMap Nat × Array (TSyntax ``mgoalHyp)) := do
     let hyps ← getExpr
     if let some _ := parseEmptyHyp? hyps then
       return acc
     if let some hyp := parseHyp? hyps then
-      let mut (map, lines) := acc
-      let (idx, name') :=
-        if let some idx := map.find? hyp.name then
-          (idx + 1, hyp.name.appendAfter <| if idx == 0 then "✝" else "✝" ++ idx.toSuperscriptString)
+      let mut (accessibles, inaccessibles, lines) := acc
+      let name := hyp.name.eraseMacroScopes
+      -- `mintro _ _` will give fresh inaccessible names `h✝` and `h✝₁` to the hypotheses.
+      -- Note that we want to mirror `intro _ _` where it's actually displayed as `h✝₁` and `h✝`.
+      -- Since neither name equates to the other, we erase the macro scopes here and look up `h` in
+      -- a separate map, adding back the default `✝` suffix by unconditionally starting from idx 0.
+      let mIdx :=
+        if hyp.name.hasMacroScopes then
+          -- NB: inaccessibles always start with 0 for the initial ✝
+          .some (inaccessibles.getD name 0)
         else
-          (0, hyp.name)
+          accessibles.find? name
+      let (idx, name') :=
+        if let some idx := mIdx then
+          (idx + 1, name.appendAfter <| if idx == 0 then "✝" else "✝" ++ idx.toSuperscriptString)
+        else
+          (0, name)
       let name' := mkIdent name'
       let stx ← `(Std.Tactic.Do.mgoalHyp| $name' : $(← SPred.Notation.unpack (← withMDataExpr <| delab)))
-      return (map.insert hyp.name idx, lines.push stx)
+      if hyp.name.hasMacroScopes then
+        inaccessibles := inaccessibles.insert name idx
+      else
+        accessibles := accessibles.insert name idx
+      return (accessibles, inaccessibles, lines.push stx)
     if (parseAnd? hyps).isSome then
       let acc_rhs ← withAppArg <| delabHypotheses acc
       let acc_lhs ← withAppFn ∘ withAppArg <| delabHypotheses acc_rhs

src/Lean/Elab/Tactic/Do/ProofMode/Frame.lean

@@ -39,8 +39,9 @@ partial def transferHypNames (P P' : Expr) : MetaM Expr := (·.snd) <$> label (c
         repeat
           -- If we cannot find the hyp, it might be in a nested conjunction.
           -- Just pick a default name for it.
+          let name ← mkFreshUserName `h
           let uniq ← mkFreshId
-          let P :: Ps'' := Ps' | return (Ps, { name := `h, uniq, p := P' : Hyp }.toExpr)
+          let P :: Ps'' := Ps' | return (Ps, { name, uniq, p := P' : Hyp }.toExpr)
           Ps' := Ps''
           if ← isDefEq P.p P' then
             return (Ps, { P with p := P' }.toExpr)
@@ -56,7 +57,7 @@ def mFrameCore [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m]
     -- copy the name of P to P' if it is a named hypothesis
     let P' ← transferHypNames P P'
     let goal := { goal with hyps := P' }
-    withLocalDeclD `h φ fun hφ => do
+    withLocalDeclD (← liftMetaM <| mkFreshUserName `h) φ fun hφ => do
       let (a, prf) ← kSuccess φ hφ goal
       let prf ← mkLambdaFVars #[hφ] prf
       let prf := mkApp7 (mkConst ``Frame.frame [goal.u]) goal.σs P P' goal.target φ inst prf

src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean

@@ -144,6 +144,33 @@ def dropStateList (σs : Expr) (n : Nat) : MetaM Expr := do
     σs := σs'
   return σs
 
+partial def MGoal.renameInaccessibleHyps (goal : MGoal) (idents : Array (TSyntax ``binderIdent)) : MetaM MGoal := do
+  let (hyps, (_, idents)) ← StateT.run (go goal.hyps) ({}, idents) -- NB: idents in reverse order
+  unless idents.isEmpty do
+    throwError "mrename_i: Could not find inaccessible hypotheses for {idents} in {goal.toExpr}"
+  return { goal with hyps := hyps }
+  where
+    go (H : Expr) : StateT (NameSet × Array (TSyntax ``binderIdent)) MetaM Expr := do
+      let mut (shadowed, idents) ← StateT.get
+      if idents.isEmpty then
+        return H
+      if let some _ := parseEmptyHyp? H then
+        return H
+      if let some hyp := parseHyp? H then
+        if hyp.name.hasMacroScopes || shadowed.contains hyp.name then
+          if let `(binderIdent| $name:ident) := idents.back! then
+            let hyp := { hyp with name := name.getId }
+            StateT.set (shadowed, idents.pop)
+            return hyp.toExpr
+          idents := idents.pop
+        StateT.set (shadowed.insert hyp.name, idents)
+        return H
+      if let some (u, σs, lhs, rhs) := parseAnd? H then
+        let rhs ← go rhs -- NB: First go right because those are the "most recent" hypotheses
+        let lhs ← go lhs
+        return mkAnd! u σs lhs rhs
+      return H
+
 def addLocalVarInfo (stx : Syntax) (lctx : LocalContext)
     (expr : Expr) (expectedType? : Option Expr) (isBinder := false) : MetaM Unit := do
   Elab.withInfoContext' (pure ())

src/Lean/Elab/Tactic/Do/ProofMode/RenameI.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König, Mario Carneiro, Sebastian Graf
+-/
+prelude
+import Std.Tactic.Do.Syntax
+import Lean.Elab.Tactic.Do.ProofMode.Basic
+
+namespace Lean.Elab.Tactic.Do.ProofMode
+open Std.Do SPred.Tactic
+open Lean Elab Tactic Meta
+
+partial def mRenameI [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] (goal : MGoal)
+    (idents : Array (TSyntax ``binderIdent)) (k : MGoal → m (α × Expr)) : m (α × Expr) := do
+  let goal ← goal.renameInaccessibleHyps idents
+  k goal
+
+@[builtin_tactic Lean.Parser.Tactic.mrenameI]
+def elabMRenameI : Tactic
+  | `(tactic| mrename_i $idents:binderIdent*) => do
+    let (mvar, goal) ← mStartMVar (← getMainGoal)
+    mvar.withContext do
+    let goals ← IO.mkRef []
+    mvar.assign (← Prod.snd <$> mRenameI goal idents fun newGoal => do
+      let m ← mkFreshExprSyntheticOpaqueMVar newGoal.toExpr
+      goals.modify (m.mvarId! :: ·)
+      return ((), m))
+    replaceMainGoal (← goals.get)
+  | _ => throwUnsupportedSyntax

src/Lean/Elab/Tactic/Do/Spec.lean

@@ -82,7 +82,8 @@ partial def dischargePostEntails (α : Expr) (ps : Expr) (Q : Expr) (Q' : Expr)
     let Q'1a := (← mkProj' ``Prod 0 Q').betaRev #[a]
     let σs := mkApp (mkConst ``PostShape.args [u]) ps
     let uniq ← liftMetaM mkFreshId
-    let goal := MGoal.mk u σs (Hyp.mk `h uniq Q1a).toExpr Q'1a
+    let name ← liftMetaM <| mkFreshUserName `h
+    let goal := MGoal.mk u σs (Hyp.mk name uniq Q1a).toExpr Q'1a
     mkLambdaFVars #[a] (← mkFreshExprSyntheticOpaqueMVar goal.toExpr (goalTag ++ `success))
   let prf₂ ← dischargeFailEntails u ps (← mkProj' ``Prod 1 Q) (← mkProj' ``Prod 1 Q') (goalTag ++ `except)
   mkAppM ``And.intro #[prf₁, prf₂]
@@ -107,7 +108,7 @@ partial def dischargeFailEntails (u : Level) (ps : Expr) (Q : Expr) (Q' : Expr)
       let Q'1e := (← mkProj' ``Prod 0 Q').betaRev #[e]
       let σs := mkApp (mkConst ``PostShape.args [u]) ps
       let uniq ← liftMetaM mkFreshId
-      let goal := MGoal.mk u σs (Hyp.mk `h uniq Q1e).toExpr Q'1e
+      let goal := MGoal.mk u σs (Hyp.mk (← liftMetaM <| mkFreshUserName `h) uniq Q1e).toExpr Q'1e
       mkLambdaFVars #[e] (← mkFreshExprSyntheticOpaqueMVar goal.toExpr (goalTag ++ `handle))
     let prf₂ ← dischargeFailEntails u ps (← mkProj' ``Prod 1 Q) (← mkProj' ``Prod 1 Q') (goalTag ++ `except)
     return ← mkAppM ``And.intro #[prf₁, prf₂] -- This is just a bit too painful to construct by hand

src/Std/Tactic/Do/Syntax.lean

@@ -78,6 +78,9 @@ macro (name := mpureIntro) "mpure_intro" : tactic =>
 @[inherit_doc Lean.Parser.Tactic.mrevertMacro]
 syntax (name := mrevert) "mrevert" colGt ident : tactic
 
+@[inherit_doc Lean.Parser.Tactic.mrenameIMacro]
+syntax (name := mrenameI) "mrename_i" (ppSpace colGt binderIdent)+ : tactic
+
 @[inherit_doc Lean.Parser.Tactic.mspecializeMacro]
 syntax (name := mspecialize) "mspecialize" ident (colGt term:max)* : tactic
 

tests/lean/run/bhaviksSampler.lean

@@ -156,6 +156,7 @@ theorem sampler_correct {m : Type → Type u} {k h} [Monad m] [WPMonad m ps] :
   -- case step => simp_all
   case post.success =>
     dsimp
+    mrename_i h
     mpure h
     mpure_intro
     have h := h.nodup_take
@@ -166,6 +167,7 @@ theorem sampler_correct {m : Type → Type u} {k h} [Monad m] [WPMonad m ps] :
   case step.success r =>
     dsimp
     mintro ∀s
+    mrename_i h
     mcases h with ⌜hinv⌝
     mpure_intro
     simp_all

tests/lean/run/doLogicTests.lean

@@ -134,9 +134,11 @@ theorem mkFreshPair_spec :
   mintro -
   mspec mkFreshNat_spec
   mintro ∀s
+  mrename_i h
   mcases h with ⌜h₁⌝
   mspec mkFreshNat_spec
   mintro ∀s
+  mrename_i h
   mcases h with ⌜h₂⌝
   simp_all
 
@@ -172,7 +174,8 @@ theorem throwing_loop_spec :
     mspec
     mspec
     mspec
-    simp at h
+    simp_all only [List.sum_nil, Nat.add_zero, gt_iff_lt, SVal.curry_nil, SPred.entails_nil,
+      imp_false, not_true_eq_false]
     omega
   case post.except => simp
   case pre1 => simp_all +decide
@@ -371,8 +374,10 @@ theorem program_spec (n k) : ⦃⌜True⌝⦄ program n k ⦃⇓r => ⌜r % 2 =
   unfold program
   mintro -
   mspec (addRandomEvens_spec n k)
+  mrename_i h
   mpure h
   mspec /- registered spec is taken -/
+  mrename_i h
   mpure h
   mspec
   mpure_intro
@@ -402,6 +407,7 @@ theorem prog.spec : ⦃isValid⦄ prog n ⦃⇓r => ⌜r > 100⌝ ∧ isValid⦄
   unfold prog
   mintro h
   mspec op.spec
+  mrename_i h
   mcases h with ⟨⌜hr₁⌝, □h⟩
   /-
   n r : Nat
@@ -416,8 +422,10 @@ theorem prog.spec : ⦃isValid⦄ prog n ⦃⇓r => ⌜r > 100⌝ ∧ isValid⦄
     (⇓r => ⌜r > 100⌝ ∧ isValid)
   -/
   mspec op.spec
+  mrename_i h
   mcases h with ⟨⌜hr₂⌝, □h⟩
   mspec op.spec
+  mrename_i h
   mcases h with ⟨⌜hr₃⌝, □h⟩
   mspec
   mrefine ⟨?_, h⟩
@@ -545,6 +553,7 @@ theorem test_loop_break :
   case isFalse => intro _; simp_all only [SVal.curry_nil, SPred.entails_nil]; grind
   case post.success =>
     simp_all
+    rename_i h
     conv at h in (List.sum _) => whnf
     simp at h
     grind
@@ -560,6 +569,7 @@ theorem test_loop_early_return :
   case pre1 => simp_all
   case h_1 =>
     simp_all
+    rename_i h
     conv at h in (List.sum _) => whnf
     simp at h
     grind
@@ -799,6 +809,7 @@ theorem max_and_sum_spec (xs : Array Nat) :
   all_goals simp_all
   · rw [Nat.left_distrib]
     simp
+    rename_i h
     apply Nat.le_trans h
     apply Nat.mul_le_mul_right
     omega

tests/lean/run/spredProofMode.lean

@@ -31,8 +31,26 @@ theorem clear (P Q : SPred σs) : P ⊢ₛ Q → Q := by
   mclear HP
   mexact HQ
 
+/--
+trace: σs : List Type
+P Q : SPred σs
+⊢ ⏎
+  h✝¹ : Q
+  h✝ : P
+  ⊢ₛ Q
+-/
+#guard_msgs in
 theorem assumption (P Q : SPred σs) : Q ⊢ₛ P → Q := by
-  mintro _ _
+  mintro _
+  mintro _
+  -- NB: We want
+  --   h✝¹ : Q
+  --   h✝ : P
+  -- Not
+  --   h✝ : Q
+  --   h✝¹ : P
+  -- just like for `intro _ _`.
+  trace_state
   massumption
 
 theorem assumption_pure (P Q : SPred σs) (hP : ⊢ₛ P): Q ⊢ₛ P := by
@@ -46,10 +64,22 @@ theorem move (Q : SPred σs) (ψ : φ → ⊢ₛ Q): ⌜φ⌝ ⊢ₛ Q := by
   mpure Hφ
   mexact (ψ Hφ)
 
+/--
+trace: σs : List Type
+φ₁ φ₂ : Prop
+Q : SPred σs
+⊢ ⏎
+  Hφ1 : ⌜φ₁⌝
+  Hφ2 : ⌜φ₂⌝
+  HQ : Q
+  ⊢ₛ Q
+-/
+#guard_msgs in
 theorem move_multiple (Q : SPred σs) : ⌜φ₁⌝ ⊢ₛ ⌜φ₂⌝ → Q → Q := by
   mintro Hφ1
   mintro Hφ2
   mintro HQ
+  trace_state
   mpure Hφ1
   mpure Hφ2
   mexact HQ
@@ -60,6 +90,16 @@ theorem move_conjunction (Q : SPred σs) : (⌜φ₁⌝ ∧ ⌜φ₂⌝) ⊢ₛ
   mpure Hφ
   mexact HQ
 
+theorem rename_i1 (P Q R : SPred σs) : ⊢ₛ P → Q → R → Q := by
+  mintro _ _ _
+  mrename_i HQ _
+  mexact HQ
+
+theorem rename_i2 (P Q R : SPred σs) : ⊢ₛ P → Q → R → R → Q := by
+  mintro H H H H
+  mrename_i _ HQ _
+  mexact HQ
+
 end pure
 
 namespace pureintro
@@ -85,8 +125,9 @@ namespace frame
 theorem move (P Q : SPred σs) : ⊢ₛ ⌜p⌝ ∧ Q ∧ ⌜q⌝ ∧ ⌜r⌝ ∧ P ∧ ⌜s⌝ ∧ ⌜t⌝ → Q := by
   mintro _
   mframe
-  mcases h with hP
-  mexact h
+  mrename_i HQ H
+  mcases H with HP
+  mexact HQ
 
 theorem move_multiple (P Q : SPred σs) : ⊢ₛ ⌜p⌝ ∧ Q ∧ ⌜q⌝ ∧ ⌜r⌝ ∧ P ∧ ⌜s⌝ ∧ ⌜t⌝ → Q := by
   mintro h