iApply attempt

src/Iris/ProofMode/Classes.lean

@@ -52,6 +52,12 @@ class IntoWand [BI PROP] (p q : Bool) (R P : PROP) (Q : outParam PROP) where
   into_wand : □?p R ⊢ □?q P -∗ Q
 export IntoWand (into_wand)
 
+/-- Another version of IntoWand which treats P like an outParam, used for iapply
+where P is a metavariable. Not sure if this is a good idea yet. -/
+class InferIntoWand [BI PROP] (p q : Bool) (R : PROP) (P : outParam PROP) (Q : PROP) where
+  into_wand : □?p R ⊢ □?q P -∗ Q
+export IntoWand (into_wand)
+
 class FromForall [BI PROP] (P : PROP) {α : outParam (Sort _)} (Ψ : outParam <| α → PROP) where
   from_forall : (∀ x, Ψ x) ⊢ P
 export FromForall (from_forall)
@@ -105,7 +111,6 @@ class IntoAbsorbingly [BI PROP] (P : outParam PROP) (Q : PROP) where
   into_absorbingly : P ⊢ <absorb> Q
 export IntoAbsorbingly (into_absorbingly)
 
-
 class FromAssumption (p : Bool) [BI PROP] (P Q : PROP) where
   from_assumption : □?p P ⊢ Q
 export FromAssumption (from_assumption)

src/Iris/ProofMode/Instances.lean

@@ -35,6 +35,10 @@ instance intoWand_wand (p q : Bool) [BI PROP] (P Q P' : PROP) [h : FromAssumptio
     IntoWand p q iprop(P' -∗ Q) P Q where
   into_wand := (intuitionisticallyIf_mono <| wand_mono_l h.1).trans intuitionisticallyIf_elim
 
+instance InferIntoWand_wand_exact [BI PROP] (P Q : PROP) :
+    InferIntoWand false false iprop(P -∗ Q) P Q where
+  into_wand := intuitionisticallyIf_elim
+
 instance intoWand_imp_false [BI PROP] (P Q P' : PROP) [Absorbing P'] [Absorbing iprop(P' → Q)]
     [h : FromAssumption b P P'] : IntoWand false b iprop(P' → Q) P Q where
   into_wand := wand_intro <| (sep_mono_r h.1).trans <| by dsimp; exact sep_and.trans imp_elim_l

src/Iris/ProofMode/Tactics.lean

@@ -1,5 +1,6 @@
 /- A description of the tactics can be found in `tactics.md`. -/
 import Iris.ProofMode.Tactics.Assumption
+import Iris.ProofMode.Tactics.Apply
 import Iris.ProofMode.Tactics.Basic
 import Iris.ProofMode.Tactics.Cases
 import Iris.ProofMode.Tactics.Clear

src/Iris/ProofMode/Tactics/Apply.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2025 Markus de Medeiros. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus de Medeiros
+-/
+
+import Iris.ProofMode.Tactics.Basic
+import Iris.ProofMode.Tactics.Remove
+
+namespace Iris.ProofMode
+open Lean Elab Tactic Meta Qq BI Std
+
+-- iApply
+-- - How to get the correct top-level syntax
+-- - Do we already have an analogue of tac_assumption?
+-- - What is our analouge of tac_apply?
+
+-- Like tac_apply
+theorem apply [BI PROP] (R P P1 Q D : PROP) [HW : InferIntoWand false false R P1 Q]
+    (Hc : P ⊣⊢ D ∗ R) (Hap : D ⊢ P1) : P ⊢ Q :=
+  Hc.mp.trans <| (sep_mono_l Hap).trans <| sep_symm.trans <| wand_elim (HW.into_wand)
+
+-- Right now, this tactic does not try to do iExact
+
+elab "iapply" colGt hyp:ident : tactic => do
+  let mvar ← getMainGoal
+  mvar.withContext do
+  let g ← instantiateMVars <| ← mvar.getType
+  let some { u, prop, bi, e := _, hyps, goal} := parseIrisGoal? g | throwError "not in proof mode"
+  let uniq ← hyps.findWithInfo hyp
+  let ⟨context', hyps', thm, _, _, _, Hcontext'⟩ := hyps.remove true uniq
+  let prec ← mkFreshExprMVarQ prop
+  let tc_inst ← synthInstanceQ q(InferIntoWand false false $thm $prec $goal)
+  let m : Q($context' ⊢ $prec) := ← mkFreshExprSyntheticOpaqueMVar <|
+    IrisGoal.toExpr { u, prop, bi, e := context', hyps := hyps', goal := q($prec) }
+  mvar.assign q(apply (HW := $tc_inst) (Hc := $Hcontext') (Hap := $m))
+  replaceMainGoal [m.mvarId!]

src/Iris/Tests/Tactics.lean

@@ -644,3 +644,11 @@ theorem exists_intuitionistic [BI PROP] (Q : Nat → PROP) : □ (∃ x, Q x) 
   iexists x
   ileft
   iexact H
+
+-- apply
+theorem wand_transitivity [BI PROP] (P Q R : PROP) : (P -∗ Q) ∗ (Q -∗ R) ⊢ (P -∗ R) := by
+  iintro ⟨H1, H2⟩
+  iintro H3
+  iapply H2
+  iapply H1
+  iexact H3