feat: iapply tactic

src/Iris/ProofMode/Classes.lean

@@ -16,7 +16,7 @@ declared as an `outParam`. Consequently, if type class instance search is suppos
 `AsEmpValid2` is used.
 -/
 
-class AsEmpValid1 (φ : outParam Prop) {PROP : Type _} (P : PROP) [BI PROP] where
+class AsEmpValid1 (φ : semiOutParam Prop) {PROP : Type _} (P : PROP) [BI PROP] where
   as_emp_valid : φ ↔ ⊢ P
 
 class AsEmpValid2 (φ : Prop) {PROP : outParam (Type _)} (P : outParam PROP) [BI PROP] where
@@ -40,6 +40,10 @@ proposition can be derived. Type classes with the prefix `Into` are used to gene
 *into* which the original proposition can be turned by derivation. Additional boolean flags are
 used to indicate that certain propositions should be intuitionistic. -/
 
+class IntoEmpValid (φ : Prop) {PROP : outParam (Type _)} (P : outParam PROP) [BI PROP] where
+  into_emp_valid : φ → ⊢ P
+export IntoEmpValid (into_emp_valid)
+
 class FromImp [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) where
   from_imp : (Q1 → Q2) ⊢ P
 export FromImp (from_imp)
@@ -48,7 +52,7 @@ class FromWand [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) where
   from_wand : (Q1 -∗ Q2) ⊢ P
 export FromWand (from_wand)
 
-class IntoWand [BI PROP] (p q : Bool) (R P : PROP) (Q : outParam PROP) where
+class IntoWand [BI PROP] (p q : Bool) (R : PROP) (P Q : outParam PROP) where
   into_wand : □?p R ⊢ □?q P -∗ Q
 export IntoWand (into_wand)
 
@@ -106,7 +110,7 @@ class IntoAbsorbingly [BI PROP] (P : outParam PROP) (Q : PROP) where
 export IntoAbsorbingly (into_absorbingly)
 
 
-class FromAssumption (p : Bool) [BI PROP] (P Q : PROP) where
+class FromAssumption (p : Bool) [BI PROP] (P : semiOutParam PROP) (Q : PROP) where
   from_assumption : □?p P ⊢ Q
 export FromAssumption (from_assumption)
 

src/Iris/ProofMode/Instances.lean

@@ -26,6 +26,16 @@ instance asEmpValid1_equiv [BI PROP] (P Q : PROP) : AsEmpValid1 (P ⊣⊢ Q) ipr
 instance asEmpValid2_equiv [BI PROP] (P Q : PROP) : AsEmpValid2 (P ⊣⊢ Q) iprop(P ∗-∗ Q) :=
   AsEmpValid1.to2
 
+-- IntoEmpValid
+instance intoEmpValid_emp_entails [BI PROP] (P : PROP) : IntoEmpValid (⊢ P) iprop(P) where
+  into_emp_valid := id
+
+instance intoEmpValid_entails [BI PROP] (P Q : PROP) : IntoEmpValid (P ⊢ Q) iprop(P -∗ Q) where
+  into_emp_valid := entails_wand
+
+instance intoEmpValid_equiv [BI PROP] (P Q : PROP) : IntoEmpValid (P ⊣⊢ Q) iprop(P ∗-∗ Q) where
+  into_emp_valid := equiv_wandIff
+
 -- FromImp
 instance fromImp_imp [BI PROP] (P1 P2 : PROP) : FromImp iprop(P1 → P2) P1 P2 := ⟨.rfl⟩
 -- FromWand
@@ -67,6 +77,10 @@ instance intoWand_intuitionistically (p q : Bool) [BI PROP] (R P Q : PROP)
     [h : IntoWand true q R P Q] : IntoWand p q iprop(□ R) P Q where
   into_wand := (intuitionisticallyIf_mono h.1).trans intuitionisticallyIf_elim
 
+instance intoWand_intuitionistically_wand (p : Bool) [BI PROP] (P Q : PROP) :
+    IntoWand p true iprop(□ P -∗ Q) P Q where
+  into_wand := intuitionisticallyIf_elim
+
 instance intoWand_persistently_true (q : Bool) [BI PROP] (R P Q : PROP)
     [h : IntoWand true q R P Q] : IntoWand true q iprop(<pers> R) P Q where
   into_wand := intuitionistically_persistently.1.trans h.1
@@ -429,6 +443,10 @@ instance (priority := default + 10) fromAssumption_forall (p : Bool) [BI PROP] (
     (x : α) (Q : PROP) [h : FromAssumption p (Φ x) Q] : FromAssumption p iprop(∀ x, Φ x) Q where
   from_assumption := (intuitionisticallyIf_mono <| forall_elim x).trans h.1
 
+instance fromAssumption_later [BI PROP] (p : Bool) (P Q : PROP)
+    [h : FromAssumption p P Q] : FromAssumption p P iprop(▷ Q) where
+  from_assumption := h.1.trans later_intro
+
 -- IntoPure
 instance intoPure_pure (φ : Prop) [BI PROP] : IntoPure (PROP := PROP) iprop(⌜φ⌝) φ := ⟨.rfl⟩
 

src/Iris/ProofMode/Patterns.lean

@@ -1 +1,3 @@
 import Iris.ProofMode.Patterns.CasesPattern
+import Iris.ProofMode.Patterns.ProofModeTerm
+import Iris.ProofMode.Patterns.SpecPattern

src/Iris/ProofMode/Patterns/ProofModeTerm.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2025 Oliver Soeser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Soeser
+-/
+import Iris.ProofMode.Patterns.SpecPattern
+
+namespace Iris.ProofMode
+open Lean
+
+declare_syntax_cat pmTerm
+
+syntax term : pmTerm
+syntax term "with" specPat,+ : pmTerm
+syntax term "$!" term,+ : pmTerm
+syntax term "$!" term,+ "with" specPat,+ : pmTerm
+
+structure PMTerm where
+  term : Term
+  terms : List Term
+  spats : List SpecPat
+  deriving Repr, Inhabited
+
+partial def PMTerm.parse (term : Syntax) : MacroM PMTerm := do
+  match ← expandMacros term with
+  | `(pmTerm| $trm:term) => return ⟨trm, [], []⟩
+  | `(pmTerm| $trm:term with $spats,*) => return ⟨trm, [], ← parseSpats spats⟩
+  | `(pmTerm| $trm:term $! $ts,*) => return ⟨trm, ts.getElems.toList, []⟩
+  | `(pmTerm| $trm:term $! $ts,* with $spats,*) =>
+    return ⟨trm, ts.getElems.toList, ← parseSpats spats⟩
+  | _ => Macro.throwUnsupported
+where
+  parseSpats (spats : Syntax.TSepArray `specPat ",") : MacroM (List SpecPat) :=
+      return (← spats.getElems.toList.mapM fun pat => SpecPat.parse pat.raw)

src/Iris/ProofMode/Patterns/SpecPattern.lean

@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2025 Oliver Soeser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Soeser
+-/
+namespace Iris.ProofMode
+open Lean
+
+declare_syntax_cat specPat
+
+syntax binderIdent : specPat
+syntax "[" binderIdent,* "]" optional(" as " ident) : specPat
+
+inductive SpecPat
+  | ident (name : TSyntax ``binderIdent)
+  | idents (names : List (TSyntax ``binderIdent)) (goalName : Name)
+  deriving Repr, Inhabited
+
+partial def SpecPat.parse (pat : Syntax) : MacroM SpecPat := do
+  match go ⟨← expandMacros pat⟩ with
+  | none => Macro.throwUnsupported
+  | some pat => return pat
+where
+  go : TSyntax `specPat → Option SpecPat
+  | `(specPat| $name:binderIdent) => some <| .ident name
+  | `(specPat| [$[$names:binderIdent],*]) => some <| .idents names.toList .anonymous
+  | `(specPat| [$[$names:binderIdent],*] as $goal:ident) => match goal.raw with
+    | .ident _ _ val _ => some <| .idents names.toList val
+    | _ => none
+  | _ => none
+
+def headName (spats : List SpecPat) : Name :=
+  match spats.head? with
+    | some <| .ident _ => .anonymous
+    | some <| .idents _ name => name
+    | _ => .anonymous

src/Iris/ProofMode/Tactics.lean

@@ -1,4 +1,5 @@
 /- A description of the tactics can be found in `tactics.md`. -/
+import Iris.ProofMode.Tactics.Apply
 import Iris.ProofMode.Tactics.Assumption
 import Iris.ProofMode.Tactics.Basic
 import Iris.ProofMode.Tactics.Cases
@@ -9,6 +10,7 @@ import Iris.ProofMode.Tactics.Exists
 import Iris.ProofMode.Tactics.Intro
 import Iris.ProofMode.Tactics.LeftRight
 import Iris.ProofMode.Tactics.Move
+import Iris.ProofMode.Tactics.Pose
 import Iris.ProofMode.Tactics.Pure
 import Iris.ProofMode.Tactics.Remove
 import Iris.ProofMode.Tactics.Rename

src/Iris/ProofMode/Tactics/Apply.lean

@@ -0,0 +1,126 @@
+/-
+Copyright (c) 2025 Oliver Soeser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Soeser
+-/
+import Iris.ProofMode.Patterns.ProofModeTerm
+import Iris.ProofMode.Tactics.Split
+import Iris.ProofMode.Tactics.Pose
+
+namespace Iris.ProofMode
+open Lean Elab Tactic Meta Qq BI Std
+
+theorem apply [BI PROP] {P Q1 Q2 R : PROP}
+    (h : P ⊢ Q1) [inst : IntoWand false false R Q1 Q2] : P ∗ R ⊢ Q2 :=
+  (sep_mono h inst.1).trans wand_elim_r
+
+theorem rec_apply [BI PROP] {P Q P' Q' Q1 Q2 R : PROP}
+    (h1 : P ⊣⊢ P' ∗ Q') (h2 : Q' ⊢ Q1) (h3 : P' ∗ Q2 ⊢ R)
+    [IntoWand false false Q Q1 Q2] : P ∗ Q ⊢ R :=
+  (sep_congr h1 .rfl).mp.trans <| sep_assoc.mp.trans <| (sep_mono_r <| apply h2).trans h3
+
+theorem apply_lean [BI PROP] {P Q R : PROP} (h1 : ⊢ Q) (h2 : P ∗ Q ⊢ R) : P ⊢ R :=
+  sep_emp.mpr.trans <| (sep_mono_r h1).trans h2
+
+variable {prop : Q(Type u)} {bi : Q(BI $prop)} in
+def specPatGoal
+    (A1 : Q($prop)) (hyps : Hyps bi e) (spats : List SpecPat)
+    (addGoal : ∀ {e}, Name → Hyps bi e → (goal : Q($prop)) → MetaM Q($e ⊢ $goal)) :
+    MetaM Q($e ⊢ $A1) := do
+  return ← if let (some <| .ident _, some inst) := (spats.head?,
+      ← try? (synthInstanceQ q(FromAssumption false $e $A1))) then
+    pure q(($inst).from_assumption)
+  else
+    addGoal (headName spats) hyps A1
+
+variable {prop : Q(Type u)} {bi : Q(BI $prop)} in
+def processSpecPats
+    (A1 : Q($prop)) (hypsl : Hyps bi el) (spats : List SpecPat)
+    (addGoal : ∀ {e}, Name → Hyps bi e → (goal : Q($prop)) → MetaM Q($e ⊢ $goal)) :
+    MetaM ((el' er' : Q($prop)) × Q($er' ⊢ $A1) × Hyps bi el' × Q($el ⊣⊢ $el' ∗ $er')) := do
+  let splitPat := fun name _ => match spats.head? with
+    | some <| .ident bIdent => binderIdentHasName name bIdent
+    | some <| .idents bIdents _ => bIdents.any <| binderIdentHasName name
+    | _ => false
+
+  let ⟨el', er', hypsl', hypsr', h'⟩ := Hyps.split bi splitPat hypsl
+  let m ← specPatGoal A1 hypsr' spats addGoal
+  return ⟨el', er', m, hypsl', h'⟩
+
+variable {prop : Q(Type u)} {bi : Q(BI $prop)} in
+partial def iApplyCore
+    (goal el er : Q($prop)) (hypsl : Hyps bi el) (spats : List SpecPat)
+    (addGoal : ∀ {e}, Name → Hyps bi e → (goal : Q($prop)) → MetaM Q($e ⊢ $goal)) :
+    MetaM (Q($el ∗ $er ⊢ $goal)) := do
+  let A1 ← mkFreshExprMVarQ q($prop)
+  let A2 ← mkFreshExprMVarQ q($prop)
+
+  let _ ← isDefEq er goal
+  if let (some _, some _) := (← try? <| synthInstanceQ q(FromAssumption false $er $goal),
+                              ← try? <| synthInstanceQ q(TCOr (Affine $el) (Absorbing $goal))) then
+    -- iexact case
+    return q(assumption (p := false) .rfl)
+  else if let some _ ← try? <| synthInstanceQ q(IntoWand false false $er $A1 $goal) then
+    -- iapply base case
+    let m ← specPatGoal A1 hypsl spats addGoal
+    return q(apply $m)
+  else if let some _ ← try? <| synthInstanceQ q(IntoWand false false $er $A1 $A2) then
+    -- iapply recursive case
+    let ⟨el', _, m, hypsl', h'⟩ ← processSpecPats A1 hypsl spats addGoal
+    let res : Q($el' ∗ $A2 ⊢ $goal) ← iApplyCore goal el' A2 hypsl' spats.tail addGoal
+    return q(rec_apply $h' $m $res)
+  else
+    throwError "iapply: cannot apply {er} to {goal}"
+
+theorem apply_forall [BI PROP] (x : α) (P : α → PROP) {Q : PROP}
+    [H1 : IntoForall Q P] (H2 : E ⊢ E' ∗ Q) : E ⊢ E' ∗ P x :=
+  Entails.trans H2 <| sep_mono_r <| H1.into_forall.trans <| forall_elim x
+
+partial def instantiateForalls' {prop : Q(Type u)} (e e' : Q($prop)) (bi : Q(BI $prop))
+    (out : Q($prop)) (pf : Q($e ⊢ $e' ∗ $out)) (terms : List Term) :
+    TacticM (Expr × Expr) := do
+  if let some t := terms.head? then
+    let texpr ← mkAppM' (← elabTerm t none) #[]
+    let ⟨_, ttype, texpr⟩ ← inferTypeQ texpr
+    let Φ ← mkFreshExprMVarQ q($ttype → $prop)
+    let _ ← synthInstanceQ q(IntoForall $out $Φ)
+    let res ← mkAppM' Φ #[texpr]
+    let pf' ← mkAppM ``apply_forall #[texpr, Φ, pf]
+    return ← instantiateForalls' e e' bi res pf' terms.tail
+  else
+    return ⟨out, pf⟩
+
+elab "iapply" colGt pmt:pmTerm : tactic => do
+  let pmt ← liftMacroM <| PMTerm.parse pmt
+  let mvar ← getMainGoal
+
+  mvar.withContext do
+    let g ← instantiateMVars <| ← mvar.getType
+    let some { u, prop, e, bi, hyps, goal, .. } := parseIrisGoal? g | throwError "not in proof mode"
+    if let some uniq ← try? do pure (← hyps.findWithInfo ⟨pmt.term⟩) then
+      -- lemma from iris context
+      let ⟨e', hyps', out, _, _, _, pf⟩ := hyps.remove false uniq
+
+      let ⟨out, pf⟩ := ← instantiateForalls' e e' bi out q(($pf).mp) pmt.terms
+
+      let goals ← IO.mkRef #[]
+      let res ← iApplyCore goal e' out hyps' pmt.spats <| goalTracker goals
+      mvar.assign <| ← mkAppM ``Entails.trans #[pf, res]
+      replaceMainGoal (← goals.get).toList
+    else
+      -- lemma from lean context
+      let A1 ← mkFreshExprMVarQ q($prop)
+      let A2 ← mkFreshExprMVarQ q($prop)
+
+      let expected : Q(Prop) := if let some _ := ← try? <|
+        synthInstanceQ q(IntoWand false false $goal $A1 $A2)
+        then q($e ⊢ $A1 -∗ $A2) else q($e ⊢ $goal)
+
+      let expr ← mkAppM' (← elabTerm pmt.term (some expected)) #[]
+
+      let goals ← IO.mkRef #[]
+      let ⟨hyp, pf⟩ ← iPoseCore bi expr pmt.terms goals
+
+      let res ← iApplyCore goal e hyp hyps pmt.spats <| goalTracker goals
+      mvar.assign <| ← mkAppM ``apply_lean #[pf, res]
+      replaceMainGoal (← goals.get).toList

src/Iris/ProofMode/Tactics/Basic.lean

@@ -53,9 +53,23 @@ def getFreshName : TSyntax ``binderIdent → CoreM (Name × Syntax)
   | `(binderIdent| $name:ident) => pure (name.getId, name)
   | stx => return (← mkFreshUserName `x, stx)
 
+def binderIdentHasName (name : Name) (id : TSyntax ``binderIdent) : Bool :=
+  match id with
+  | `(binderIdent| $name':ident) => name'.getId == name
+  | _ => false
+
 def selectHyp (ty : Expr) : ∀ {s}, @Hyps u prop bi s → MetaM (Name × Q(Bool) × Q($prop))
   | _, .emp _ => failure
   | _, .hyp _ _ uniq p ty' _ => do
     let .true ← isDefEq ty ty' | failure
     pure (uniq, p, ty')
   | _, .sep _ _ _ _ lhs rhs => try selectHyp ty rhs catch _ => selectHyp ty lhs
+
+variable {prop : Q(Type u)} {bi : Q(BI $prop)} in
+def goalTracker {P} (goals : IO.Ref (Array MVarId)) (name : Name) (hyps : Hyps bi P)
+    (goal : Q($prop)) : MetaM Q($P ⊢ $goal) := do
+  let m : Q($P ⊢ $goal) ← mkFreshExprSyntheticOpaqueMVar <|
+    IrisGoal.toExpr { prop, bi, hyps, goal, .. }
+  m.mvarId!.setUserName name
+  goals.modify (·.push m.mvarId!)
+  pure m

src/Iris/ProofMode/Tactics/Cases.lean

@@ -286,11 +286,7 @@ elab "icases" colGt hyp:ident "with" colGt pat:icasesPat : tactic => do
 
   -- process pattern
   let goals ← IO.mkRef #[]
-  let pf2 ← iCasesCore bi hyps' goal b A A' h pat fun hyps => do
-    let m : Q($e ⊢ $goal) ← mkFreshExprSyntheticOpaqueMVar <|
-      IrisGoal.toExpr { u, prop, bi, hyps, goal, .. }
-    goals.modify (·.push m.mvarId!)
-    pure m
+  let pf2 ← iCasesCore bi hyps' goal b A A' h pat (λ hyps => goalTracker goals .anonymous hyps goal)
 
   mvar.assign q(($pf).1.trans $pf2)
   replaceMainGoal (← goals.get).toList

src/Iris/ProofMode/Tactics/Intro.lean

@@ -102,16 +102,12 @@ elab "iintro" pats:(colGt icasesPat)* : tactic => do
   -- parse syntax
   let pats ← liftMacroM <| pats.mapM <| iCasesPat.parse
 
-  let (mvar, { prop, bi, hyps, goal, .. }) ← istart (← getMainGoal)
+  let (mvar, { bi, hyps, goal, .. }) ← istart (← getMainGoal)
   mvar.withContext do
 
   -- process patterns
   let goals ← IO.mkRef #[]
-  let pf ← iIntroCore bi hyps goal pats.toList fun {P} hyps goal => do
-    let m : Q($P ⊢ $goal) ← mkFreshExprSyntheticOpaqueMVar <|
-      IrisGoal.toExpr { prop, bi, hyps, goal, .. }
-    goals.modify (·.push m.mvarId!)
-    pure m
+  let pf ← iIntroCore bi hyps goal pats.toList <| goalTracker goals .anonymous
 
   mvar.assign pf
   replaceMainGoal (← goals.get).toList