leanprover-community · alvinylt · Jul 4, 2026 · Jul 4, 2026 · Jul 4, 2026 · Jul 4, 2026
diff --git a/Iris/Iris/BI/BIBase.lean b/Iris/Iris/BI/BIBase.lean
@@ -54,6 +54,8 @@ syntax "⌜" term "⌝" : term
 syntax:35 term:36 " ∗ " term:35 : term
 /-- Separating implication. -/
 syntax:25 term:26 " -∗ " term:25 : term
+/-- Separating implication with an optional wand premise. -/
+syntax:25 term:26 " -∗? " term:25 : term
 /-- Persistency modality. `persistently` is a primitive of BI. -/
 syntax:max "<pers> " term:40 : term
 /-- Later modality. `later` is a primitive of BI. -/
@@ -163,6 +165,18 @@ delab_rule iff
 delab_rule wandIff
   | `($_ $P $Q) => do ``(iprop($(← unpackIprop P) ∗-∗ $(← unpackIprop Q)))
 
+@[simp, rocq_alias bi_wandM]
+def wandM [BIBase PROP] (mP : Option PROP) (Q : PROP) : PROP :=
+  match mP with
+  | none => Q
+  | some P => iprop(P -∗ Q)
+
+macro_rules
+  | `(iprop($mP -∗? $Q)) => ``(wandM $mP iprop($Q))
+
+delab_rule wandM
+  | `($_ $mP $Q) => do ``(iprop($mP -∗? $(← unpackIprop Q)))
+
 /-- Affine modality.
 ```
 def affinely (P) := emp ∧ P

diff --git a/Iris/Iris/BI/DerivedLaws.lean b/Iris/Iris/BI/DerivedLaws.lean
@@ -1041,6 +1041,12 @@ theorem emp_or [BI PROP] {P : PROP} [Affine P] : emp ∨ P ⊣⊢ emp := ⟨or_e
 theorem emp_wand [BI PROP] {P : PROP} : (emp -∗ P) ⊣⊢ P :=
   ⟨emp_sep.mpr.trans wand_elim_right, wand_intro_left emp_sep.mp⟩
 
+@[rocq_alias bi.wandM_sound]
+theorem wandM_sound [BI PROP] {mP : Option PROP} {Q : PROP} :
+    (mP -∗? Q) ⊣⊢ (mP.getD emp -∗ Q) := by
+  cases mP <;> simp [BIBase.wandM]
+  exact emp_wand.symm
+
 @[rocq_alias bi.or_emp]
 theorem or_emp [BI PROP] {P : PROP} [Affine P] : P ∨ emp ⊣⊢ emp := or_comm.trans emp_or
 

diff --git a/Iris/Iris/ProgramLogic/WeakestPre.lean b/Iris/Iris/ProgramLogic/WeakestPre.lean
@@ -681,4 +681,11 @@ instance elimModalFupdWpAtomic_wrongMask :
     p false iprop(|={E₁,E₂}=> P) iprop(False) (WP e @ s ; E₁ {{ Φ }}) iprop(False) where
   elim_modal := nofun
 
+@[rocq_alias add_modal_fupd_wp]
+instance addModalFupdWp : AddModal iprop(|={E}=> P) P (WP e @ s ; E {{ Φ }}) where
+  add_modal := by
+    iintro ⟨H1, H2⟩
+    imod H1
+    iapply H2 $$ H1
+
 end ProofModeClasses
diff --git a/Iris/Iris/ProofMode/Classes.lean b/Iris/Iris/ProofMode/Classes.lean
@@ -185,6 +185,19 @@ class ElimModal {PROP} [BI PROP] (φ : outParam $ Prop) (p : Bool) (p' : outPara
   elim_modal : φ → □?p P ∗ (□?p' P' -∗ Q') ⊢ Q
 export ElimModal (elim_modal)
 
+/--
+`AddModal` is used by `ispecialize` and `iassert` to add a modality to the
+goal corresponding to the premise/asserted proposition.
+-/
+@[ipm_class, rocq_alias AddModal]
+class AddModal {PROP} [BI PROP] (P : outParam $ PROP) (P' Q : PROP) where
+  add_modal : P ∗ (P' -∗ Q) ⊢ Q
+export AddModal (add_modal)
+
+@[rocq_alias add_modal_id]
+theorem addModal_id {PROP} [BI PROP] (P Q : PROP) : AddModal P P Q where
+  add_modal := wand_elim_right
+
 @[ipm_class, rocq_alias Frame]
 class Frame {PROP} [BI PROP] (p : Bool) (R P : PROP) (Q : outParam $ PROP) where
   frame : □?p R ∗ Q ⊢ P

diff --git a/Iris/Iris/ProofMode/Instances.lean b/Iris/Iris/ProofMode/Instances.lean
@@ -51,6 +51,12 @@ instance fromImp_imp [BI PROP] (P1 P2 : PROP) : FromImp iprop(P1 → P2) P1 P2 :
 @[rocq_alias from_wand_wand]
 instance fromWand_wand [BI PROP] (P1 P2 : PROP) : FromWand iprop(P1 -∗ P2) io P1 P2 := ⟨.rfl⟩
 
+-- FromWandM
+@[rocq_alias from_wand_wandM]
+instance fromWand_wandM [BI PROP] (mP1 : Option PROP) (P2 : PROP) :
+    FromWand iprop(mP1 -∗? P2) io (mP1.getD emp) P2 where
+  from_wand := wandM_sound.mpr
+
 -- IntoWand
 #rocq_ignore into_wand_wand' "IntoWand' is not used in Lean"
 #rocq_ignore into_wand_impl' "IntoWand' is not used in Lean"
@@ -61,6 +67,13 @@ instance intoWand_wand (p q : Bool) [BI PROP] (P Q P' : PROP) [h : FromAssumptio
     IntoWand p q iprop(P' -∗ Q) ioP P ioQ Q where
   into_wand := (intuitionisticallyIf_mono <| wand_mono_left h.1).trans intuitionisticallyIf_elim
 
+@[rocq_alias into_wand_wandM]
+instance intoWand_wandM (p q : Bool) [BI PROP] (mP' : Option PROP) (P Q : PROP)
+    [h : FromAssumption q ioP P (mP'.getD emp)] :
+    IntoWand p q iprop(mP' -∗? Q) ioP P ioQ Q where
+  into_wand := (intuitionisticallyIf_mono wandM_sound.mp).trans <|
+    (intuitionisticallyIf_mono <| wand_mono_left h.1).trans intuitionisticallyIf_elim
+
 -- TODO: compare this with into_wand_impl_false_false, into_wand_impl_false_true, ... in Rocq
 instance intoWand_imp_false [BI PROP] (P Q P' : PROP) [Absorbing P'] [Absorbing iprop(P' → Q)]
     [h : FromAssumption b ioP P P'] : IntoWand false b iprop(P' → Q) ioP P ioQ Q where
@@ -321,12 +334,12 @@ instance intoAnd_and_affine_r [BI PROP] (P P' Q : PROP) [Affine Q]
   into_and := (and_mono_right (affine_affinely _).2).trans <|
     affinely_and_right.1.trans <| affinely_and.1.trans <| and_mono h.1 (affine_affinely _).1
 
-@[rocq_alias into_and_sep]
+@[ipm_backtrack, rocq_alias into_and_sep]
 instance intoAnd_sep [BI PROP] [BIPositive PROP] (P Q : PROP) :
     IntoAnd true iprop(P ∗ Q) P Q where
   into_and := intuitionistically_sep.1.trans <| and_sep_intuitionistically.2.trans <| intuitionistically_and.2
 
-@[rocq_alias into_and_sep_affine]
+@[ipm_backtrack, rocq_alias into_and_sep_affine]
 instance intoAnd_sep_affine (p : Bool) [BI PROP] (P Q : PROP)
     [TCOr (Affine P) (Absorbing Q)] [TCOr (Affine Q) (Absorbing P)] :
     IntoAnd p iprop(P ∗ Q) P Q where
@@ -573,7 +586,7 @@ instance (priority := default + 30) intoAbsorbingly_true [BI PROP] :
     IntoAbsorbingly (PROP := PROP) iprop(True) emp where
   into_absorbingly := absorbingly_emp.2
 
-@[rocq_alias into_absorbingly_absorbing]
+@[ipm_backtrack, rocq_alias into_absorbingly_absorbing]
 instance (priority := default + 20) intoAbsorbingly_absorbing [BI PROP] (P : PROP) [Absorbing P] :
     IntoAbsorbingly P P where
   into_absorbingly := absorbing_absorbingly.2
@@ -856,6 +869,46 @@ instance elimModal_absorbingly_here [BI PROP] p (P Q : PROP) [Absorbing Q] :
   ElimModal True p false iprop(<absorb> P) P Q Q where
   elim_modal _ := (sep_mono_left intuitionisticallyIf_elim).trans $ absorbingly_sep_left.1.trans $ absorbing_absorbingly.1.trans wand_elim_right
 
+theorem addModal_wand_mp [BI PROP] {P P' Q R : PROP} [h : AddModal P P' Q] :
+    P ∗ (P' -∗ R -∗ Q) ⊢ R -∗ Q := by
+  have h1 : (P' -∗ R -∗ Q) ∗ R ⊢ P' -∗ Q := by
+    apply wand_intro
+    calc
+      _ ⊢ (P' -∗ R -∗ Q) ∗ R ∗ P'   := sep_assoc.mp
+      _ ⊢ (P' -∗ R -∗ Q) ∗ P' ∗ R   := sep_mono_right sep_comm.mp
+      _ ⊢ ((P' -∗ R -∗ Q) ∗ P') ∗ R := sep_assoc.mpr
+      _ ⊢ (R -∗ Q) ∗ R              := sep_mono_left wand_elim_left
+      _ ⊢ Q                         := wand_elim_left
+  apply wand_intro
+  calc
+    _ ⊢ P ∗ (P' -∗ R -∗ Q) ∗ R := sep_assoc.mp
+    _ ⊢ P ∗ (P' -∗ Q)          := sep_mono_right h1
+    _ ⊢ Q                      := h.add_modal
+
+-- AddModal
+@[rocq_alias add_modal_wand]
+instance addModal_wand [BI PROP] (P P' Q R : PROP) [h : AddModal P P' Q] :
+    AddModal P P' iprop(R -∗ Q) where
+  add_modal := addModal_wand_mp
+
+@[rocq_alias add_modal_wandM]
+instance addModal_wandM [BI PROP] (P P' Q : PROP) (mR : Option PROP)
+    [h : AddModal P P' Q] : AddModal P P' iprop(mR -∗? Q) where
+  add_modal := by
+    cases mR with
+    | none => exact h.add_modal
+    | some R => exact addModal_wand_mp
+
+@[rocq_alias add_modal_forall]
+instance addModal_forall {A : Type} [BI PROP] (P P' : PROP) (Φ : A → PROP)
+    [h : ∀ x, AddModal P P' (Φ x)] : AddModal P P' iprop(∀ x, Φ x) where
+  add_modal := by
+    apply forall_intro
+    intro a
+    exact (sep_mono_right (wand_mono .rfl (forall_elim a))).trans (h a).add_modal
+
+#rocq_ignore add_modal_tforall "Rocq-specific telescope infrastructure not needed in the Lean metaprogram"
+
 -- CombineSepAs
 @[rocq_alias maybe_combine_sep_as_default]
 instance (priority := default - 20) combineSepAs_default [BI PROP] (P Q : PROP) :

diff --git a/Iris/Iris/ProofMode/InstancesLater.lean b/Iris/Iris/ProofMode/InstancesLater.lean
@@ -318,6 +318,42 @@ instance (priority := default - 10) elimModal_timeless [BI PROP] p (P P' Q : PRO
   ElimModal True p p P P' Q Q where
   elim_modal _ := ((sep_mono ((intuitionisticallyIf_mono into_except0).trans except0_intuitionisticallyIf) except0_intro).trans $ except0_sep.2.trans (except0_mono wand_elim_right)).trans is_except0
 
+/-- AddModal -/
+@[rocq_alias add_modal_later_except_0]
+instance (priority := default + 10) addModal_later_except_0 [BI PROP] (P Q : PROP) [h : Timeless P] :
+    AddModal iprop(▷ P) P iprop(◇ Q) where
+  add_modal := calc
+    _ ⊢ ◇ P ∗ (P -∗ ◇ Q)   := sep_mono_left h.timeless
+    _ ⊢ ◇ (P ∗ (P -∗ ◇ Q)) := except0_frame_right
+    _ ⊢ ◇ (◇ Q)            := except0_mono wand_elim_right
+    _ ⊢ ◇ Q                 := except0_idem.mp
+
+@[rocq_alias add_modal_later]
+instance (priority := default + 10) addModal_later [BI PROP] (P Q : PROP) [h : Timeless P] :
+    AddModal iprop(▷ P) P iprop(▷ Q) where
+  add_modal := calc
+    _ ⊢ ◇ P ∗ (P -∗ ▷ Q)   := sep_mono_left h.timeless
+    _ ⊢ ◇ (P ∗ (P -∗ ▷ Q)) := except0_frame_right
+    _ ⊢ ◇ (▷ Q)            := except0_mono wand_elim_right
+    _ ⊢ ▷ Q                 := except0_later
+
+@[rocq_alias add_modal_except_0]
+instance addModal_except_0 [BI PROP] (P Q : PROP) :
+    AddModal iprop(◇ P) P iprop(◇ Q) where
+  add_modal :=
+    calc
+    _ ⊢ ◇ (P ∗ (P -∗ ◇ Q)) := except0_frame_right
+    _ ⊢ ◇ (◇ Q)            := except0_mono wand_elim_right
+    _ ⊢ ◇ Q                 := except0_idem.mp
+
+@[rocq_alias add_modal_except_0_later]
+instance addModal_except_0_later [BI PROP] (P Q : PROP) :
+    AddModal iprop(◇ P) P iprop(▷ Q) where
+  add_modal := calc
+    _ ⊢ ◇ (P ∗ (P -∗ ▷ Q)) := except0_frame_right
+    _ ⊢ ◇ (▷ Q)            := except0_mono wand_elim_right
+    _ ⊢ ▷ Q                 := except0_later
+
 /-- IntoLaterN -/
 @[rocq_alias maybe_into_laterN_default]
 instance (priority := low) intoLaterN_default [BI PROP] only_head n (P : PROP) :

diff --git a/Iris/Iris/ProofMode/InstancesUpdates.lean b/Iris/Iris/ProofMode/InstancesUpdates.lean
@@ -88,6 +88,11 @@ instance elimModal_bupd p (P Q : PROP) :
   elim_modal _ := (sep_mono_left intuitionisticallyIf_elim).trans <|
     bupd_frame_right.trans <| (BIUpdate.mono wand_elim_right).trans BIUpdate.trans
 
+@[rocq_alias add_modal_bupd]
+instance addModal_bupd (P Q : PROP) :
+    AddModal iprop(|==> P) P iprop(|==> Q) where
+  add_modal := bupd_wand_right.trans bupd_trans
+
 end BIBasicUpdate
 
 section SBIBasicUpdate
@@ -200,6 +205,16 @@ instance (priority := low) elimModal_fupd_fupd_wrongMask p E0 E1 E2 E3 (P Q : PR
       p false iprop(|={E1,E2}=> P) iprop(False) iprop(|={E0,E3}=> Q) iprop(False) where
   elim_modal h := by cases h
 
+@[rocq_alias add_modal_fupd]
+instance addModal_fupd E1 E2 (P Q : PROP) :
+    AddModal iprop(|={E1}=> P) P iprop(|={E1,E2}=> Q) where
+  add_modal := by
+    calc
+      _ ⊢ (P ={E1, E2}=∗ Q) ∗ (|={E1}=> P)    := sep_comm.mp
+      _ ⊢ |={E1}=> ((P -∗ |={E1,E2}=> Q) ∗ P) := fupd_frame_left
+      _ ⊢ |={E1}=> (|={E1,E2}=> Q)            := BIFUpdate.mono wand_elim_left
+      _ ⊢ |={E1, E2}=> Q                      := BIFUpdate.trans
+
 end BIFancyUpdate
 
 section SBIFancyUpdate

diff --git a/Iris/Iris/ProofMode/Patterns.lean b/Iris/Iris/ProofMode/Patterns.lean
@@ -2,6 +2,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
diff --git a/Iris/Iris/ProofMode/Patterns/ProofModeTerm.lean b/Iris/Iris/ProofMode/Patterns/ProofModeTerm.lean