feat: selection patterns and iclear/irevert support (#189)

* feat: selection patterns and iclear refactor

---------

Co-authored-by: Michael Sammler <noreply@sammler.me>

Author: HaleOIC

PORTING.md

@@ -361,9 +361,9 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
     - [ ] with bi specified
   - [x] iStopProof
   - [x] iRename
-  - [ ] iClear
+  - [x] iClear
     - [x] basic
-    - [ ] selection patterns
+    - [x] selection patterns
   - [ ] iEval
   - [ ] iSimpl
   - [ ] iUnfold
@@ -381,7 +381,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [ ] iRevert
     - [x] basic
     - [ ] `intoIH` revert
-    - [ ] selection patterns
+    - [x] selection patterns
   - [x] iPoseProof (Lean: ihave _ := _)
   - [ ] iSpecialize
     - [x] basic functionality
@@ -437,7 +437,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
 - [ ] `monpred.v`
 - [x] `proofmode.v` (ProofMode.lean)
 - [-] `reduction.v` (not necessary in Lean)
-- [ ] `sel_patterns.v`
+- [x] `sel_patterns.v`
 - [ ] `spec_patterns.v`
   - [x] SIdent
   - [x] SPureGoal

src/Iris/ProofMode/Expr.lean

@@ -97,6 +97,18 @@ partial def Hyps.find? {u prop bi} (name : Name) :
   | _, .hyp _ name' uniq p ty _ => if name == name' then (uniq, p, ty) else none
   | _, .sep _ _ _ _ lhs rhs => rhs.find? name <|> lhs.find? name
 
+partial def Hyps.spatialUniqs {u prop bi} :
+    ∀ {s}, @Hyps u prop bi s → List Name
+  | _, .emp _ => []
+  | _, .hyp _ _ uniq p _ _ => if isTrue p then [] else [uniq]
+  | _, .sep _ _ _ _ lhs rhs => lhs.spatialUniqs ++ rhs.spatialUniqs
+
+partial def Hyps.intuitionisticUniqs {u prop bi} :
+    ∀ {s}, @Hyps u prop bi s → List Name
+  | _, .emp _ => []
+  | _, .hyp _ _ uniq p _ _ => if isTrue p then [uniq] else []
+  | _, .sep _ _ _ _ lhs rhs => lhs.intuitionisticUniqs ++ rhs.intuitionisticUniqs
+
 variable (oldUniq new : Name) {prop : Q(Type u)} {bi : Q(BI $prop)} in
 def Hyps.rename : ∀ {e}, Hyps bi e → Option (Hyps bi e)
   | _, .emp _ => none
@@ -331,6 +343,25 @@ partial def Hyps.findDependencyOnFVar {prop : Q(Type u)} {bi : Q(BI $prop)}
       if (ty : Expr).containsFVar fvarId then some (name, uniq, p, ty)
       else none
 
+/-- Check that removing the Lean local `fvarId` leaves no dangling dependencies in the
+proofmode context, an optional goal, or remaining Lean locals not accepted by `allowedDep`. -/
+def Hyps.checkRemovableFVar {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+    (hyps : Hyps bi e) (tac : String) (fvarId : FVarId)
+    (goal? : Option Expr := none) (allowedDep : FVarId → Bool := fun _ => false) :
+    MetaM LocalDecl := do
+  let ldecl ← fvarId.getDecl
+  if let some (name, _, _, _) := hyps.findDependencyOnFVar fvarId then
+    throwError "{tac}: proofmode hypothesis {name} depends on {ldecl.userName}"
+  if let some goal := goal? then
+    let goal ← instantiateMVars goal
+    if goal.containsFVar fvarId then
+      throwError "{tac}: goal depends on {ldecl.userName}"
+  let deps ← collectForwardDeps #[mkFVar fvarId] false
+  if let some dep := deps.find? (fun e => e.fvarId! != fvarId && !allowedDep e.fvarId!) then
+    let depDecl := (← getLCtx).getFVar! dep
+    throwError "{tac}: Lean hypothesis {depDecl.userName} depends on {ldecl.userName}"
+  return ldecl
+
 end dependency
 
 end hyps

src/Iris/ProofMode/Patterns.lean

@@ -3,4 +3,5 @@ module
 public import Iris.ProofMode.Patterns.CasesPattern
 public import Iris.ProofMode.Patterns.IntroPattern
 public import Iris.ProofMode.Patterns.ProofModeTerm
+public import Iris.ProofMode.Patterns.SelPattern
 public import Iris.ProofMode.Patterns.SpecPattern

src/Iris/ProofMode/Patterns/SelPattern.lean

@@ -0,0 +1,79 @@
+/-
+Copyright (c) 2026 Yunsong Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yunsong Yang
+-/
+module
+
+public meta import Iris.ProofMode.ProofModeM
+
+@[expose] public section
+
+namespace Iris.ProofMode
+open Lean Meta Std
+
+declare_syntax_cat selPat
+
+syntax ident : selPat
+syntax "%" : selPat
+syntax "%" noWs ident : selPat
+syntax "#" : selPat
+syntax "∗" : selPat
+
+inductive SelPat
+  | pure
+  | intuitionistic
+  | spatial
+  | ident (name : Ident)
+  | leanIdent (name : Ident)
+  deriving Repr, Inhabited
+
+partial def SelPat.parseOne (pat : TSyntax `selPat) : MacroM SelPat := do
+  match go ⟨← expandMacros pat⟩ with
+  | none => Macro.throwUnsupported
+  | some pat => return pat
+where
+  go : TSyntax `selPat → Option SelPat
+  | `(selPat| %$name:ident) => some <| .leanIdent name
+  | `(selPat| %) => some .pure
+  | `(selPat| #) => some .intuitionistic
+  | `(selPat| ∗) => some .spatial
+  | `(selPat| $name:ident) => some <| .ident name
+  | _ => none
+
+partial def SelPat.parse (pats : TSyntaxArray `selPat) : MacroM (List SelPat) := do
+  return (← pats.mapM SelPat.parseOne).toList
+
+public meta section
+
+abbrev SelTarget := Name ⊕ FVarId
+
+/-- Resolve selection patterns to concrete proofmode hypotheses (`.inl`) and Lean locals (`.inr`). -/
+def SelPat.resolveOne (hyps : Hyps bi e) : SelPat → ProofModeM (List SelTarget)
+  | .ident name =>
+      return [.inl (← hyps.findWithInfo name)]
+  | .leanIdent name => do
+      let ldecl ← getLocalDeclFromUserName name.getId
+      return [.inr ldecl.fvarId]
+  | .intuitionistic =>
+      return hyps.intuitionisticUniqs.map .inl
+  | .spatial =>
+      return hyps.spatialUniqs.map .inl
+  | .pure => do
+      -- `%` selects user-facing Lean pure assumptions, so we keep only `Prop` hypotheses.
+      let mut hyps := #[]
+      for ldecl in ← getLCtx do
+        if ldecl.isAuxDecl || ldecl.isImplementationDetail then
+          continue
+        if ! (← isProp ldecl.type) then
+          continue
+        hyps := hyps.push (.inr ldecl.fvarId)
+      return hyps.toList
+
+def SelPat.resolve (hyps : Hyps bi e) (pats : List SelPat) :
+    ProofModeM (List SelTarget) := do
+  return (← pats.flatMapM (SelPat.resolveOne hyps)).eraseDups
+
+end
+
+end Iris.ProofMode

src/Iris/ProofMode/ProofModeM.lean

@@ -45,6 +45,19 @@ def addBIGoal {prop : Q(Type u)} {bi : Q(BI $prop)}
   modify ({goals := ·.goals.push m.mvarId!})
   pure m
 
+/-- Create a new BI goal with the given hypotheses and goal, but without some fvars, and add it to the proof mode state.
+It is the responsibility of the user of this function to check that the variables to clear can actually be cleared (e.g. using
+`Hyps.checkRemovableFVar`). -/
+def addBIGoalWithoutFVars {prop : Q(Type u)} {bi : Q(BI $prop)}
+    {e} (hyps : Hyps bi e) (goal : Q($prop)) (toClear : Array FVarId) (name : Name := .anonymous) : ProofModeM Q($e ⊢ $goal) := do
+  let goal ← mkBIGoal hyps goal name
+  let (clearedGoalId, cleared) ← goal.mvarId!.tryClearMany' toClear
+  unless cleared.size == toClear.size do
+    -- this should not happen since the caller of this function should call Hyps.checkRemovableFVar first
+    throwError "internal error: failed to clear all selected Lean hypotheses"
+  modify ({goals := ·.goals.push clearedGoalId})
+  return Expr.mvar clearedGoalId
+
 /-- Add an existing metavariable as a goal to the proof mode state if it is not already assigned or present. -/
 def addMVarGoal (m : MVarId) (name : Name := .anonymous) : ProofModeM Unit := do
   if ← m.isAssignedOrDelayedAssigned then

src/Iris/ProofMode/Tactics/Clear.lean

@@ -1,12 +1,13 @@
 /-
 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, Michael Sammler
+Authors: Lars König, Mario Carneiro, Michael Sammler, Yunsong Yang
 -/
 module
 
 import Iris.BI
 import Iris.ProofMode.Classes
+public meta import Iris.ProofMode.Patterns.SelPattern
 public meta import Iris.ProofMode.Tactics.Basic
 
 namespace Iris.ProofMode
@@ -34,10 +35,32 @@ def iClearCore {prop : Q(Type u)} (_bi : Q(BI $prop)) (e e' : Q($prop))
         | throwError "iclear: {out} is not affine and the goal not absorbing"
       return q(clear_spatial (A:=$out) $pf)
 
-elab "iclear" colGt hyp:ident : tactic => do
-  ProofModeM.runTactic λ mvar { bi, e, hyps, goal, .. } => do
+private structure ClearState {u} {prop : Q(Type u)} {bi : Q(BI $prop)} (origE goal : Q($prop)) where
+  (e : Q($prop)) (hyps : Hyps bi e)
+  pf : Q(($e ⊢ $goal) → ($origE ⊢ $goal))
 
-  let uniq ← hyps.findWithInfo hyp
-  let ⟨e', hyps', _, out', p, _, pf⟩ := hyps.remove true uniq
-  let m ← addBIGoal hyps' goal
-  mvar.assign ((← iClearCore bi e e' p out' goal pf).app m)
+private def ClearState.clearProofModeHyp {u prop bi origE goal} :
+    @ClearState u prop bi origE goal → Name →
+    ProofModeM (@ClearState u prop bi origE goal)
+  | { e, hyps, pf }, uniq => do
+      let ⟨e', hyps', _, out', p, _, hrem⟩ := hyps.remove true uniq
+      let step ← iClearCore bi e e' p out' goal hrem
+      let pf' : Q(($e' ⊢ $goal) → ($origE ⊢ $goal)) := q(λ h => $pf ($step h))
+      return {  e := e', hyps := hyps', pf := pf' }
+
+elab "iclear" pats:(colGt selPat)+ : tactic => do
+  let pats ← liftMacroM <| SelPat.parse pats
+
+  ProofModeM.runTactic λ mvar { e, hyps, goal, .. } => do
+  let (uniqs, fvars) := (← SelPat.resolve hyps pats).partitionMap id
+
+  -- Clear the selected Iris hypotheses first, updating the proof-mode context and proof term.
+  let mut st : ClearState e goal := { e, hyps, pf := q(fun h => h) }
+  for uniq in uniqs do st ← st.clearProofModeHyp uniq
+
+  -- Lean locals are cleared afterwards; first ensure no remaining hypothesis or goal depends on them.
+  for fvar in fvars do
+    let _ ← st.hyps.checkRemovableFVar "iclear" fvar (some goal) fvars.contains
+
+  let pf' ← addBIGoalWithoutFVars st.hyps goal fvars.reverse.toArray
+  mvar.assign q($(st.pf) $pf')

src/Iris/ProofMode/Tactics/Revert.lean

@@ -6,6 +6,7 @@ Authors: Oliver Soeser, Yunsong Yang
 module
 
 public import Iris.ProofMode.ClassesMake
+public meta import Iris.ProofMode.Patterns.SelPattern
 public meta import Iris.ProofMode.Tactics.Basic
 
 namespace Iris.ProofMode
@@ -36,40 +37,24 @@ open Lean Elab Tactic Meta Qq
   `reverted` collects lean variables already reverted. This is necessary for dependency checks
   since they are only cleared from the Lean context for the final goal.
 -/
-private structure RevertState {prop : Q(Type u)} (bi : Q(BI $prop)) (origE origGoal : Q($prop)) where
+private structure RevertState {prop : Q(Type u)} {bi : Q(BI $prop)} (origE origGoal : Q($prop)) where
   (e : Q($prop)) (hyps : Hyps bi e) (goal : Q($prop))
   (reverted : Array FVarId := #[])
   pf : Q(($e ⊢ $goal) → ($origE ⊢ $origGoal))
 
 /-- Revert a proofmode hypothesis by turning it into a wand premise. -/
 private def RevertState.revertProofModeHyp
-    : @RevertState u prop bi origE origGoal → TSyntax `ident →
-      ProofModeM (RevertState bi origE origGoal)
-  | { hyps, goal, reverted, pf, .. }, hyp => do
-    let uniq ← hyps.findWithInfo hyp
+    : @RevertState u prop bi origE origGoal → Name →
+      ProofModeM (@RevertState u prop bi origE origGoal)
+  | { hyps, goal, reverted, pf, .. }, uniq => do
     let ⟨e', hyps', out, _, _, _, hΔ⟩ := hyps.remove true uniq
     return { e := e', hyps := hyps', goal := q(wand $out $goal), reverted,
              pf := q(fun h => $pf (wand_revert $hΔ h)) }
 
-/-- Check that reverting the Lean local named by `hyp` will not leave dangling dependencies. -/
-private def RevertState.checkLeanDependencies
-    : @RevertState u prop bi origE origGoal → TSyntax `ident → MetaM LocalDecl
-  | { hyps, reverted, .. }, hyp => do
-    let ldecl ← getLocalDeclFromUserName hyp.getId
-    let f := ldecl.fvarId
-    if let some (name, _, _, _) := hyps.findDependencyOnFVar f then
-      throwError "irevert: proofmode hypothesis {name} depends on {hyp.getId}"
-    let deps ← collectForwardDeps #[mkFVar f] false
-    -- check if there is a dependency on a variable that has not been reverted before
-    if let some dep := deps.find? (fun e => e.fvarId! != f && !reverted.contains e.fvarId!) then
-      let depDecl := (← getLCtx).getFVar! dep
-      throwError "irevert: Lean hypothesis {depDecl.userName} depends on {hyp.getId}"
-    return ldecl
-
 /-- Revert a Lean proposition by turning it into the `MakeAffinely` pure premise. -/
 private def RevertState.revertLeanPropHyp
     (st : @RevertState u prop bi origE origGoal) (f : FVarId) (φ : Q(Prop)) :
-    ProofModeM (RevertState bi origE origGoal) := do
+    ProofModeM (@RevertState u prop bi origE origGoal) := do
   let { e, hyps, goal, reverted, pf } := st
   let P ← mkFreshExprMVarQ prop
   let _hA : Q(MakeAffinely iprop(⌜$φ⌝) $P) ← synthInstanceQ q(MakeAffinely iprop(⌜$φ⌝) $P)
@@ -81,7 +66,7 @@ private def RevertState.revertLeanPropHyp
 /-- Revert a Lean non-`Prop` local by turning the current goal into a forall. -/
 private def RevertState.revertLeanForallHyp
     (st : @RevertState u prop bi origE origGoal) (f : FVarId) (α : Q(Sort v)) :
-    ProofModeM (RevertState bi origE origGoal) := do
+    ProofModeM (@RevertState u prop bi origE origGoal) := do
   let { e, hyps, goal, reverted, pf } := st
   let x : Q($α) := mkFVar f
   have Φ : Q($α → $prop) := ← mkLambdaFVars #[x] goal
@@ -93,10 +78,9 @@ private def RevertState.revertLeanForallHyp
 
 /-- Revert a Lean local after checking proofmode and local-context dependencies. -/
 private def RevertState.revertLeanHyp
-    (st : @RevertState u prop bi origE origGoal) (hyp : TSyntax `ident) :
-    ProofModeM (RevertState bi origE origGoal) := do
-  let ldecl ← st.checkLeanDependencies hyp
-  let f := ldecl.fvarId
+    (st : @RevertState u prop bi origE origGoal) (f : FVarId) :
+    ProofModeM (@RevertState u prop bi origE origGoal) := do
+  let ldecl ← st.hyps.checkRemovableFVar "irevert" f none st.reverted.contains
   let v : Level ← Meta.getLevel ldecl.type
   have α : Q(Sort v) := ldecl.type
   if ← Meta.isProp α then
@@ -105,17 +89,16 @@ private def RevertState.revertLeanHyp
   else
     st.revertLeanForallHyp f α
 
--- TODO: when extending this to selection patterns, consider adding a selection pattern %x for pure hypotheses such that it is syntactically clear whether an argument of irevert refers to a pure or an Iris hypothesis
-elab "irevert" hs:(colGt ident)+ : tactic => do
-  ProofModeM.runTactic fun mvar { bi, e, hyps, goal, .. } => do
-    let init : RevertState bi e goal := { e, hyps, goal, pf := q(id) }
-    let st ← hs.reverse.toList.foldlM (init := init) fun st hyp => do
-      if let some _ := st.hyps.find? hyp.getId then
-        st.revertProofModeHyp hyp
-      else
-        st.revertLeanHyp hyp
+elab "irevert" pats:(colGt selPat)+ : tactic => do
+  let pats ← liftMacroM <| SelPat.parse pats
+
+  ProofModeM.runTactic fun mvar { e, hyps, goal, .. } => do
+    let targets ← SelPat.resolve hyps pats
+    let init : RevertState e goal := { e, hyps, goal, pf := q(id) }
+    let st ← targets.reverse.foldlM (init := init) fun st target => do
+      match target with
+      | .inl uniq => st.revertProofModeHyp uniq
+      | .inr fvar => st.revertLeanHyp fvar
 
-    -- Clear Lean locals already reverted into the accumulated BI goal from the final generated subgoal.
-    let finalGoalId ← (← mkBIGoal st.hyps st.goal).mvarId!.tryClearMany st.reverted.reverse
-    addMVarGoal finalGoalId
-    mvar.assign (mkApp st.pf (Expr.mvar finalGoalId))
+    let pf' ← addBIGoalWithoutFVars st.hyps st.goal st.reverted.reverse
+    mvar.assign q($(st.pf) $pf')