feat: istart with BI specified

Iris/Iris/ProofMode/Classes.lean

@@ -30,13 +30,13 @@ inductive AsEmpValid.Direction where
 class AsEmpValid (d : AsEmpValid.Direction) (φ : Prop) (_ : InOut) (PROP : semiOutParam $ Type _)
 (_ : InOut) (bi : semiOutParam $ BI PROP) (P : outParam $ PROP) where
   as_emp_valid : (d = .into → φ → ⊢ P) ∧ (d = .from → (⊢ P) → φ)
-
 @[rocq_alias as_emp_valid_1]
 theorem asEmpValid_1 {PROP} [bi : BI PROP] {φ : Prop} (P : PROP) [AsEmpValid .into φ .in PROP .in bi P]
 : φ → ⊢ P := (AsEmpValid.as_emp_valid .in .in).1 rfl
 @[rocq_alias as_emp_valid_2]
-theorem asEmpValid_2 {PROP} [bi : BI PROP] {P: PROP} (φ : Prop) [AsEmpValid .from φ .out PROP .out bi P]
-: (⊢ P) → φ := (AsEmpValid.as_emp_valid .out .out).2 rfl
+theorem asEmpValid_2 {PROP} [bi : BI PROP] {P: PROP} {io : InOut}
+    (φ : Prop) (inst : AsEmpValid .from φ io PROP .out bi P) : (⊢ P) → φ :=
+  (AsEmpValid.as_emp_valid io .out).2 rfl
 
 /- Depending on the use case, type classes with the prefix `From` or `Into` are used. Type classes
 with the prefix `From` are used to generate one or more propositions *from* which the original

Iris/Iris/ProofMode/Porting.lean

@@ -15,7 +15,7 @@ import Iris.Std.RocqPorting
 #rocq_concept proofmode "Tactics" missing "tactics"
 #rocq_concept proofmode "Tactics" "iSolveSideCondition" ported "iSolveSideconditionAt"
 #rocq_concept proofmode "Tactics" "iStartProof (basic)" ported "istart"
-#rocq_concept proofmode "Tactics" "iStartProof (with bi specified)" missing ""
+#rocq_concept proofmode "Tactics" "iStartProof (with bi specified)" ported "istart"
 #rocq_concept proofmode "Tactics" "iStopProof" ported "istop"
 #rocq_concept proofmode "Tactics" "iRename" ported "irename"
 #rocq_concept proofmode "Tactics" "iClear" ported "iclear"

Iris/Iris/ProofMode/ProofModeM.lean

@@ -109,29 +109,45 @@ def ProofModeM.synthInstanceQ (α : Q(Sort v)) : ProofModeM Q($α) := do
   return e
 
 /-- Initialize proof mode for a metavariable, converting it to an Iris goal. -/
-def startProofMode (mvar : MVarId) : MetaM (MVarId × IrisGoal) := mvar.withContext do
+def startProofMode (mvar : MVarId) (customProp : Option Expr := none) :
+    MetaM (MVarId × IrisGoal) := mvar.withContext do
   -- parse goal
   let goal ← instantiateMVars <| ← mvar.getType
 
   -- check if already in proof mode
   if let some irisGoal := parseIrisGoal? goal then
+    customProp.forM <| fun customProp => do
+      let eq ← isDefEq irisGoal.prop customProp
+      if !eq then throwError m!"istart: currently in the Iris Proof Mode with \
+        {irisGoal.prop} rather than {customProp}"
     return (mvar, irisGoal)
 
   let some goal ← checkTypeQ goal q(Prop)
     | throwError "type mismatch\n{← mkHasTypeButIsExpectedMsg (← inferType goal) q(Prop)}"
   let u ← mkFreshLevelMVar
   let prop ← mkFreshExprMVarQ q(Type u)
+
+  customProp.forM <| fun customProp => do
+    let eq ← isDefEq prop customProp
+    if !eq then throwError "istart: {customProp} is not a valid BI instance type"
+
   let P ← mkFreshExprMVarQ q($prop)
   let bi ← mkFreshExprMVarQ q(BI $prop)
-  let .some (_, mvars) ← ProofMode.trySynthInstanceQ q(AsEmpValid .from $goal .out $prop .out $bi $P)
-    | throwError "istart: {goal} is not an emp valid"
-  if !mvars.isEmpty then throwError "istart does not support creating mvars"
-
-  let irisGoal := { u, prop, bi, hyps := .mkEmp bi, goal := P, .. }
-  let subgoal : Quoted q(⊢ $P) ←
-    mkFreshExprSyntheticOpaqueMVar (IrisGoal.toExpr irisGoal) (← mvar.getTag)
-  mvar.assign q(asEmpValid_2 $goal $subgoal)
-  pure (subgoal.mvarId!, irisGoal)
+  let io : Q(InOut) := if customProp.isSome then q(.in) else q(.out)
+  let synthResult ← ProofMode.trySynthInstanceQ q(AsEmpValid .from $goal $io $prop .out $bi $P)
+
+  match synthResult, customProp with
+  | .some (inst, mvars), _ =>
+    if !mvars.isEmpty then throwError "istart does not support creating mvars"
+    let irisGoal := { u, prop, bi, hyps := .mkEmp bi, goal := P, .. }
+    let subgoal : Quoted q(⊢ $P) ←
+      mkFreshExprSyntheticOpaqueMVar (IrisGoal.toExpr irisGoal) (← mvar.getTag)
+    mvar.assign q(asEmpValid_2 $goal $inst $subgoal)
+    pure (subgoal.mvarId!, irisGoal)
+  | _, none =>
+    throwError "istart: {goal} is not an emp valid"
+  | _, some _ =>
+    throwError "istart: {goal} is not an emp valid in {customProp}"
 
 /-- Run a ProofModeM computation on the main goal, ordering resulting goals with dependencies last. -/
 def ProofModeM.runTactic (x : MVarId → IrisGoal → ProofModeM α) (s : ProofModeM.State := {}) : TacticM α := do

Iris/Iris/ProofMode/Tactics/Basic.lean

@@ -13,7 +13,7 @@ public meta import Iris.ProofMode.ProofModeM
 public meta section
 
 namespace Iris.ProofMode
-open Lean Elab.Tactic Meta Qq BI Std
+open Lean Elab.Tactic Meta Qq BI Std Lean.Elab Term
 
 /-- `itrivial` collects tactics to solve trivial Iris goals. It is used by the `//` specialization
 and introduction patterns. One can add new tactics using
@@ -44,6 +44,15 @@ elab "istart" : tactic => do
   let (mvar, _) ← startProofMode (← getMainGoal)
   replaceMainGoal [mvar]
 
+/--
+  `istart prop` starts the Iris Proof Mode with a specific `prop`.
+-/
+elab "istart " colGt prop:term : tactic => do
+  let mvar ← getMainGoal
+  let customProp ← mvar.withContext do elabType prop >>= (instantiateMVars ·)
+  let (mvar, _) ← startProofMode mvar (some customProp)
+  replaceMainGoal [mvar]
+
 /--
   `istop` stops the Iris Proof Mode by turning the goal back
   into plain entailment.

Iris/Iris/Tests/Tactics.lean

@@ -24,10 +24,48 @@ open BI CMRA DFrac
 example [BI PROP] (Q : PROP) (H : Q ⊢ Q) : Q ⊢ Q := by
   istart
   iintro _HQ
-  have HH: True := by trivial
+  have HH : True := by trivial
   istop
   exact H
 
+/-- Tests `istart` with a BI instance specified. -/
+example [BI PROP1] [BI PROP2] (P1 : PROP1) (P2 : PROP2)
+    (_ : ⊢@{PROP1} P1) : ⊢@{PROP2} P2 -∗ P2 := by
+  istart PROP2
+  iintro HP
+  iassumption
+
+/- Tests `istart` with the wrong BI instance specified. -/
+/-- error: istart: ⊢ P2 is not an emp valid in PROP1 -/
+#guard_msgs in
+example [BI PROP1] [BI PROP2] (P1 : PROP1) (P2 : PROP2)
+    (h : ⊢@{PROP1} P1) : ⊢@{PROP2} P2 := by
+  istart PROP1
+
+/- Tests `istart` with an invalid type specified as the BI instance. -/
+/-- error: istart: True is not a valid BI instance type -/
+#guard_msgs in
+example [BI PROP1] [BI PROP2] (P1 : PROP1) (P2 : PROP2)
+    (h : ⊢@{PROP1} P1) : ⊢@{PROP2} P2 := by
+  istart True
+
+/- Tests `istart` within the Iris Proof Mode. -/
+example [BI PROP1] [BI PROP2] (P1 : PROP1) (P2 : PROP2)
+    (_ : ⊢@{PROP1} P1) : ⊢@{PROP2} P2 -∗ P2 := by
+  iintro P2
+  istart PROP2
+  istart
+  istart PROP2
+  iassumption
+
+/- Tests `istart` within the Iris Proof Mode with the wrong BI instance specified. -/
+/-- error: istart: currently in the Iris Proof Mode with PROP2 rather than PROP1 -/
+#guard_msgs in
+example [BI PROP1] [BI PROP2] (P1 : PROP1) (P2 : PROP2)
+    (_ : ⊢@{PROP1} P1) : ⊢@{PROP2} P2 -∗ P2 := by
+  iintro P2
+  istart PROP1
+
 -- rename
 namespace rename
 

Iris/tactics.md

@@ -5,6 +5,7 @@ The proof mode maintains three contexts: the *pure* (Lean) context, the *intuiti
 ## Proof Mode Management
 
 - `istart` — Start the proof mode. (Most tactics start the proof mode automatically.)
+- `istart` *prop* — Start the proof mode, specifying the BI instance *prop*.
 - `istop` — Stop the proof mode, turning the goal back into a plain entailment.
 
 ## Context Management