feat: Implement mrevert ∀ (#9755)

This PR implements a `mrevert ∀n` tactic that "eta-reduces" the stateful
goal and is adjoint to `mintro ∀x1 ... ∀xn`.

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

@@ -26,7 +26,7 @@ def mStart (goal : Expr) : MetaM MStartResult := do
     return { goal := mgoal }
 
   let u ← mkFreshLevelMVar
-  let σs ← mkFreshExprMVar (σs.mkType u)
+  let σs ← mkFreshExprMVar (TypeList.mkType u)
   let P ← mkFreshExprMVar (mkApp (mkConst ``SPred [u]) σs)
   let inst ← synthInstance (mkApp3 (mkConst ``PropAsSPredTautology [u]) goal σs P)
   let u ← instantiateLevelMVars u

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

@@ -48,7 +48,7 @@ partial def mIntroForall [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m]
   | `(binderIdent| $_) => liftMetaM <| mkFreshUserName `s
   withLocalDeclD name σ fun s => do
     addLocalVarInfo ident (← getLCtx) s σ (isBinder := true)
-    let H := betaRevPreservingHypNames σs' goal.hyps #[s]
+    let H := pushForallContextIntoHyps σs' (mkApp goal.hyps s)
     let T := goal.target.betaRev #[s]
     map do
       let (a, prf) ← k { u := goal.u, σs:=σs', hyps:=H, target:=T }
@@ -58,7 +58,7 @@ partial def mIntroForall [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m]
 def mIntroForallN [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] (goal : MGoal) (n : Nat) (k : MGoal → m (α × Expr)) : m (α × Expr) :=
   match n with
   | 0 => k goal
-  | n+1 => do mIntroForall goal (← liftM (m := MetaM) `(binderIdent| _)) fun g =>
+  | n+1 => do mIntroForall goal (← liftMetaM `(binderIdent| _)) fun g =>
               mIntroForallN g n k
 
 macro_rules

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

@@ -35,12 +35,26 @@ def parseHyp? : Expr → Option Hyp
 def Hyp.toExpr (hyp : Hyp) : Expr :=
   .mdata ⟨[(nameAnnotation, .ofName hyp.name), (uniqAnnotation, .ofName hyp.uniq)]⟩ hyp.p
 
+def SPred.mkType (u : Level) (σs : Expr) : Expr :=
+  mkApp (mkConst ``SPred [u]) σs
+
 -- set_option pp.all true in
 -- #check ⌜True⌝
+def SPred.mkPure (u : Level) (σs : Expr) (p : Expr) : Expr :=
+  mkApp3 (mkConst ``SVal.curry [u]) (mkApp (mkConst ``ULift [u, 0]) (.sort .zero)) σs <|
+    mkLambda `tuple .default (mkApp (mkConst ``SVal.StateTuple [u]) σs) <|
+      mkApp2 (mkConst ``ULift.up [u, 0]) (.sort .zero) (Expr.liftLooseBVars p 0 1)
+
+def SPred.isPure? : Expr → Option (Level × Expr × Expr)
+  | mkApp3 (.const ``SVal.curry [u]) (mkApp (.const ``ULift _) (.sort .zero)) σs <|
+      .lam _ _ (mkApp2 (.const ``ULift.up _) _ p) _ => some (u, σs, (Expr.lowerLooseBVars p 0 1))
+  | _ => none
+
 def emptyHyp (u : Level) (σs : Expr) : Expr := -- ⌜True⌝ standing in for an empty conjunction of hypotheses
-  mkApp3 (mkConst ``SVal.curry [u]) (mkApp (mkConst ``ULift [u, 0]) (.sort .zero)) σs <| mkLambda `tuple .default (mkApp (mkConst ``SVal.StateTuple [u]) σs) (mkApp2 (mkConst ``ULift.up [u, 0]) (.sort .zero) (mkConst ``True))
-def parseEmptyHyp? : Expr → Option (Level × Expr)
-  | mkApp3 (.const ``SVal.curry [u]) (mkApp (.const ``ULift _) (.sort .zero)) σs (.lam _ _ (mkApp2 (.const ``ULift.up _) _ (.const ``True _)) _) => some (u, σs)
+  SPred.mkPure u σs (mkConst ``True)
+
+def parseEmptyHyp? (e : Expr) : Option (Level × Expr) := match SPred.isPure? e with
+  | some (u, σs, .const ``True _) => some (u, σs)
   | _ => none
 
 def pushLeftConjunct (pos : SubExpr.Pos) : SubExpr.Pos :=
@@ -65,12 +79,13 @@ def mkAnd (u : Level) (σs lhs rhs : Expr) : Expr × Expr :=
     let result := mkAnd! u σs lhs rhs
     (result, mkApp2 (mkConst ``SPred.bientails.refl [u]) σs result)
 
-def σs.mkType (u : Level) : Expr := mkApp (mkConst ``List [.succ u]) (mkSort (.succ u))
-def σs.mkNil (u : Level) : Expr := mkApp (mkConst ``List.nil [.succ u]) (mkSort (.succ u))
+def TypeList.mkType (u : Level) : Expr := mkApp (mkConst ``List [.succ u]) (mkSort (.succ u))
+def TypeList.mkNil (u : Level) : Expr := mkApp (mkConst ``List.nil [.succ u]) (mkSort (.succ u))
+def TypeList.mkCons (u : Level) (hd tl : Expr) : Expr := mkApp3 (mkConst ``List.cons [.succ u]) (mkSort (.succ u)) hd tl
 
 def parseAnd? (e : Expr) : Option (Level × Expr × Expr × Expr) :=
       (e.getAppFn.constLevels![0]!, ·) <$> e.app3? ``SPred.and
-  <|> (0, σs.mkNil 0, ·) <$> e.app2? ``And
+  <|> (0, TypeList.mkNil 0, ·) <$> e.app2? ``And
 
 structure MGoal where
   u : Level
@@ -127,19 +142,30 @@ def getFreshHypName : TSyntax ``binderIdent → CoreM (Name × Syntax)
   | `(binderIdent| $name:ident) => pure (name.getId, name)
   | stx => return (← mkFreshUserName `h, stx)
 
-partial def betaRevPreservingHypNames (σs' e : Expr) (args : Array Expr) : Expr :=
-  if let some (u, _) := parseEmptyHyp? e then
-    emptyHyp u σs'
-  else if let some hyp := parseHyp? e then
-    { hyp with p := hyp.p.betaRev args }.toExpr
-  else if let some (u, _σs, lhs, rhs) := parseAnd? e then
-    -- _σs = σ :: σs'
-    mkAnd! u σs' (betaRevPreservingHypNames σs' lhs args) (betaRevPreservingHypNames σs' rhs args)
-  else
-    e.betaRev args
+partial def pushForallContextIntoHyps (σs hyps : Expr) : Expr := go #[] #[] hyps
+  where
+    wrap (revLams : Array (Name × Expr × BinderInfo)) (revAppArgs : Array Expr) (body : Expr) : Expr :=
+      revLams.foldr (fun (x, ty, info) e => .lam x ty e info) (body.betaRev revAppArgs)
+
+    go (revLams : Array (Name × Expr × BinderInfo)) (revAppArgs : Array Expr) (e : Expr) : Expr :=
+      if let some (u, _σs) := parseEmptyHyp? e then
+        emptyHyp u σs
+      else if let some hyp := parseHyp? e then
+        { hyp with p := wrap revLams revAppArgs hyp.p }.toExpr
+      else if let some (u, _σs, lhs, rhs) := parseAnd? e then
+        mkAnd! u σs (go revLams revAppArgs lhs) (go revLams revAppArgs rhs)
+      else if let .lam x ty body info := e then
+        if let some a := revAppArgs.back? then
+          go revLams revAppArgs.pop (body.instantiate1 a)
+        else
+          go (revLams.push (x, ty, info)) revAppArgs body
+      else if let .app f a := e then
+        go revLams (revAppArgs.push a) f
+      else
+        wrap revLams revAppArgs e
 
 def betaPreservingHypNames (σs' e : Expr) (args : Array Expr) : Expr :=
-  betaRevPreservingHypNames σs' e args.reverse
+  pushForallContextIntoHyps σs' (mkAppN e args)
 
 def dropStateList (σs : Expr) (n : Nat) : MetaM Expr := do
   let mut σs := σs

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

@@ -16,7 +16,9 @@ namespace Lean.Elab.Tactic.Do.ProofMode
 open Std.Do SPred.Tactic
 open Lean Elab Tactic Meta
 
-partial def mRevertStep (goal : MGoal) (ref : TSyntax `ident) (k : MGoal → MetaM Expr) : MetaM Expr := do
+variable {m : Type → Type u} [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m]
+
+partial def mRevert (goal : MGoal) (ref : TSyntax `ident) (k : MGoal → m Expr) : m Expr := do
   let res ← goal.focusHypWithInfo ref
   let P := goal.hyps
   let Q := res.restHyps
@@ -26,14 +28,78 @@ partial def mRevertStep (goal : MGoal) (ref : TSyntax `ident) (k : MGoal → Met
   let prf := mkApp7 (mkConst ``Revert.revert [goal.u]) goal.σs P Q H T res.proof prf
   return prf
 
+/--
+Turn goal
+  hᵢ : Hᵢ
+  ⊢ₛ T e₁ ... eₙ
+into
+  hᵢ : fun sₙ ... s₁ => Hᵢ
+  h : fun sₙ ... s₁ => ⌜s₁ = e₁ ∧ ... ∧ sₙ = eₙ⌝
+  ⊢ₛ T
+-/
+partial def mRevertForallN (goal : MGoal) (n : Nat) (hypName : Name) (k : MGoal → m Expr) : m Expr := do
+  if n = 0 then return ← k goal
+  let H := goal.hyps
+  let T := goal.target.consumeMData
+  let f := T.getAppFn
+  let args := T.getAppRevArgs
+  let revertArgs := args[0:n].toArray.reverse
+  unless revertArgs.size = n do
+    liftMetaM <| throwError "mrevert: expected {n} excess arguments in {T}, got {revertArgs.size}"
+  let revertArgsTypes ← liftMetaM <| revertArgs.mapM inferType
+
+  let declInfos ← revertArgsTypes.mapIdxM fun i ty => do
+    return ((← liftMetaM <| mkFreshUserName `s).appendIndexAfter (i+1), ty)
+
+  -- Build `fun s₁ ... sₙ => H ∧ ⌜s₁ = e₁ ∧ ... ∧ sₙ = eₙ⌝`
+  let (H, φ) ← withLocalDeclsDND declInfos fun ss => do
+    let eqs ← (revertArgs.zip ss).mapM fun (e, s) => mkEq s e
+    let eqs := eqs.toList
+    let φ := mkAndN eqs
+    let φ := SPred.mkPure goal.u goal.σs φ
+    let uniq ← liftMetaM <| mkFreshUserName hypName
+    let φ := Hyp.toExpr ⟨hypName, uniq, ← mkLambdaFVars ss φ⟩
+    return (← mkLambdaFVars ss H, φ)
+
+  -- Build `⟨rfl, ..., rfl⟩ : e₁ = e₁ ∧ ... ∧ eₙ = eₙ`
+  let prfs ← liftMetaM <| revertArgs.mapM mkEqRefl
+  let h ← mkAndIntroN prfs.toList
+
+  -- Push `fun s₁ ... sₙ =>` into the hyps in `H`
+  let u := goal.u
+  let σs' := revertArgsTypes.foldr (TypeList.mkCons u) goal.σs
+  let H ← instantiateMVarsIfMVarApp H
+  let H := pushForallContextIntoHyps σs' H
+  let (H, hand) := mkAnd u σs' H φ
+
+  -- Prove `((fun s₁ ... sₙ => H) ∧ (fun s₁ ... sₙ => ⌜s₁ = e₁ ∧ ... ∧ sₙ = eₙ⌝)) ⊢ₛ T`
+  let goal' := { u, σs := σs', hyps := H, target := mkAppRev f args[n:] }
+  let prf ← k goal'
+
+  -- Build the proof for `H ⊢ₛ T e₁ ... eₙ`
+  let prf := mkApp8 (mkConst ``Revert.and_pure_intro_r [goal.u]) goal.σs (← inferType h) goal.hyps (mkAppN H revertArgs) goal.target h (mkAppN hand revertArgs) (mkAppN prf revertArgs)
+  -- goal.checkProof prf
+  return prf
+
 @[builtin_tactic Lean.Parser.Tactic.mrevert]
 def elabMRevert : Tactic
-  | `(tactic| mrevert $h) => do
+  | `(tactic| mrevert $h:ident) => do
+  let mvar ← getMainGoal
+  let some goal := parseMGoal? (← mvar.getType)
+    | throwError "Not in proof mode"
+  mvar.withContext do
+  let goals ← IO.mkRef []
+  mvar.assign (← mRevert goal h fun newGoal => do
+    let m ← mkFreshExprSyntheticOpaqueMVar newGoal.toExpr
+    goals.modify (m.mvarId! :: ·)
+    return m)
+  replaceMainGoal (← goals.get)
+  | `(tactic| mrevert ∀ $[$n]?) => do
   let (mvar, goal) ← mStartMVar (← getMainGoal)
   mvar.withContext do
-
+  let n := ((·.getNat) <$> n).getD 1
   let goals ← IO.mkRef []
-  mvar.assign (← mRevertStep goal h fun newGoal => do
+  mvar.assign (← mRevertForallN goal n (← mkFreshUserName `h) fun newGoal => do
     let m ← mkFreshExprSyntheticOpaqueMVar newGoal.toExpr
     goals.modify (m.mvarId! :: ·)
     return m)

src/Lean/Meta/AppBuilder.lean

@@ -716,6 +716,20 @@ def mkIffOfEq (h : Expr) : MetaM Expr := do
   else
     mkAppM ``Iff.of_eq #[h]
 
+/--
+Given proofs `hᵢ : pᵢ`, returns a proof for `p₁ ∧ ... ∧ pₙ`.
+Roughly, `mkAndIntroN hs : mkAndN (← hs.mapM inferType)`.
+-/
+def mkAndIntroN (hs : List Expr) : MetaM Expr := (·.1) <$> go hs
+  where
+    go : List Expr → MetaM (Expr × Expr)
+      | [] => return (mkConst ``True.intro, mkConst ``True)
+      | [h] => return (h, ← inferType h)
+      | h :: hs => do
+        let (h', p') ← go hs
+        let p ← inferType h
+        return (mkApp4 (mkConst ``And.intro) p p' h h', mkApp2 (mkConst ``And) p p')
+
 builtin_initialize do
   registerTraceClass `Meta.appBuilder
   registerTraceClass `Meta.appBuilder.result (inherited := true)

src/Std/Do/SPred/DerivedLaws.lean

@@ -33,6 +33,8 @@ theorem bientails.mpr {P Q : SPred σs} : (P ⊣⊢ₛ Q) → (Q ⊢ₛ P) := fu
 
 /-! # Connectives -/
 
+theorem and_intro_l (h : P ⊢ₛ Q) : P ⊢ₛ Q ∧ P := and_intro h .rfl
+theorem and_intro_r (h : P ⊢ₛ Q) : P ⊢ₛ P ∧ Q := and_intro .rfl h
 theorem and_elim_l' (h : P ⊢ₛ R) : P ∧ Q ⊢ₛ R := and_elim_l.trans h
 theorem and_elim_r' (h : Q ⊢ₛ R) : P ∧ Q ⊢ₛ R := and_elim_r.trans h
 theorem or_intro_l' (h : P ⊢ₛ Q) : P ⊢ₛ Q ∨ R := h.trans or_intro_l
@@ -216,6 +218,7 @@ theorem Have.dup {P Q H T : SPred σs} (hfoc : P ⊣⊢ₛ Q ∧ H) (hgoal : P
 theorem Have.have {P H PH T : SPred σs} (hand : P ∧ H ⊣⊢ₛ PH) (hhave : P ⊢ₛ H) (hgoal : PH ⊢ₛ T) : P ⊢ₛ T := (and_intro .rfl hhave).trans (hand.mp.trans hgoal)
 theorem Have.replace {P H H' PH PH' T : SPred σs} (hfoc : PH ⊣⊢ₛ P ∧ H ) (hand : P ∧ H' ⊣⊢ₛ PH') (hhave : PH ⊢ₛ H') (hgoal : PH' ⊢ₛ T) : PH ⊢ₛ T := (and_intro (hfoc.mp.trans and_elim_l) hhave).trans (hand.mp.trans hgoal)
 theorem Intro.intro {P Q H T : SPred σs} (hand : Q ∧ H ⊣⊢ₛ P) (h : P ⊢ₛ T) : Q ⊢ₛ H → T := imp_intro (hand.mp.trans h)
+theorem Revert.and_pure_intro_r {φ : Prop} {P P' Q : SPred σs} (h₁ : φ) (hand : P ∧ ⌜φ⌝ ⊣⊢ₛ P') (h₂ : P' ⊢ₛ Q) : P ⊢ₛ Q := (SPred.and_intro_r (SPred.pure_intro h₁)).trans (hand.mp.trans h₂)
 theorem Pure.thm {P Q T : SPred σs} {φ : Prop} [IsPure Q φ] (h : φ → P ⊢ₛ T) : P ∧ Q ⊢ₛ T := by
   apply pure_elim
   · exact and_elim_r.trans IsPure.to_pure.mp
@@ -252,7 +255,6 @@ instance (σs) (P : SPred σs) : SimpAnd ⌜True⌝ P P where simp_and := true_a
 
 class HasFrame (P : SPred σs) (P' : outParam (SPred σs)) (φ : outParam Prop) : Prop where
   reassoc : P ⊣⊢ₛ P' ∧ ⌜φ⌝
-instance (σs) : HasFrame (σs:=σs) ⌜φ⌝ ⌜True⌝ φ where reassoc := true_and.symm
 instance (σs) (P P' Q QP : SPred σs) [HasFrame P Q φ] [SimpAnd Q P' QP]: HasFrame (σs:=σs) spred(P ∧ P') QP φ where reassoc := ((and_congr_l HasFrame.reassoc).trans and_right_comm).trans (and_congr_l SimpAnd.simp_and)
 instance (σs) (P P' Q' PQ : SPred σs) [HasFrame P' Q' φ] [SimpAnd P Q' PQ]: HasFrame (σs:=σs) spred(P ∧ P') PQ φ where reassoc := ((and_congr_r HasFrame.reassoc).trans and_assoc.symm).trans (and_congr_l SimpAnd.simp_and)
 instance (σs) (P P' : SVal.StateTuple σs → Prop) (Q : SPred σs) [HasFrame spred(SVal.curry (fun t => ⟨P t⟩) ∧ SVal.curry (fun t => ⟨P' t⟩)) Q φ] : HasFrame (σs:=σs) (SVal.curry fun t => ⟨P t ∧ P' t⟩) Q φ where reassoc := and_curry.symm.trans HasFrame.reassoc
@@ -281,7 +283,7 @@ instance (σs) (P Q : SPred σs) [HasFrame P Q ψ] : HasFrame (σs:=σs) spred(P
              <| and_congr_r (and_comm.trans pure_and)
 -- The following instance comes last so that it gets the highest priority.
 -- It's the most efficient and best solution if valid
-instance {φ : Prop} : HasFrame (σs:=[]) ⌜φ⌝ ⌜True⌝ φ where reassoc := true_and.symm
+instance (σs) : HasFrame (σs:=σs) ⌜φ⌝ ⌜True⌝ φ where reassoc := true_and.symm
 instance {P : SPred []} : HasFrame (σs:=[]) P ⌜True⌝ P.down where reassoc := true_and.symm
 
 theorem Frame.frame {P Q T : SPred σs} {φ : Prop} [HasFrame P Q φ]

src/Std/Tactic/Do/Syntax.lean

@@ -75,9 +75,6 @@ syntax (name := mpure) "mpure" colGt ident : tactic
 macro (name := mpureIntro) "mpure_intro" : tactic =>
   `(tactic| apply $(mkIdent ``Std.Do.SPred.Tactic.Pure.intro))
 
-@[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
 
@@ -224,6 +221,17 @@ macro_rules
     | `(mintroPat| $pat:mcasesPat) => `(tactic| mintro h; mcases h with $pat)
     | _ => Macro.throwUnsupported -- presently unreachable
 
+declare_syntax_cat mrevertPat
+
+syntax ident : mrevertPat
+syntax "∀" optional(num) : mrevertPat
+
+@[inherit_doc Lean.Parser.Tactic.mrevertMacro]
+syntax (name := mrevert) "mrevert" (ppSpace colGt mrevertPat)+ : tactic
+
+macro_rules
+  | `(tactic| mrevert $pat₁ $pat₂ $pats:mrevertPat*) => `(tactic| mrevert $pat₁; mrevert $pat₂ $pats*)
+
 /--
 `mspec_no_simp $spec` first tries to decompose `Bind.bind`s before applying `$spec`.
 This variant of `mspec_no_simp` does not; `mspec_no_bind $spec` is defined as

tests/lean/run/spredProofMode.lean

@@ -145,6 +145,13 @@ theorem revert (P Q R : SPred σs) : P ∧ Q ∧ R ⊢ₛ R := by
   mintro HR'
   mexact HR'
 
+theorem revert_forall (H : SPred σs) (T : SPred (α::β::σs))
+    (h : (fun _ _ => H) ∧ (fun s₁ s₂ => ⌜s₁ = e₁ ∧ s₂ = e₂⌝) ⊢ₛ T) :
+    H ⊢ₛ T e₁ e₂ := by
+  mintro h
+  mrevert ∀2
+  exact h
+
 namespace constructor
 
 theorem and (Q : SPred σs) : Q ⊢ₛ Q ∧ Q := by