feat: tactics imod and imodintro support fancy update

PORTING.md

@@ -239,8 +239,11 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
 - [ ] `sbi_unfold.v`
 - [ ] `telescopes.v`
 - [ ] `updates.v`
-  - [x] FUpd class
-  - [ ] Big op lemmas
+  - [x] Bupd laws 
+  - [x] Fupd basic laws 
+  - [ ] Fupd mask change laws
+  - [ ] Fupd step derived rules 
+  - [ ] Fupd plainly general laws
 - [ ] `weakestpre.v`
 - [ ] `lib/atomic.v`
 - [ ] `lib/core.v`
@@ -263,6 +266,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [ ] instances for big ops
   - [ ] MaybeCombineSepAs instances
   - [ ] CombineSepGives instances
+  - [x] FromModal instances
   - [x] ElimModal instances
   - [ ] AddModal instances
   - [ ] ElimInv instances
@@ -296,11 +300,11 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [ ] IntoLaterN
 - [ ] `class_instances_updates.v` (InstancesUpdates.lean)
   - [x] Basic instances for bupd
-  - [ ] Basic instances for fupd
+  - [x] Basic instances for fupd
   - [x] FromModal bupd
-  - [ ] FromModal fupd
+  - [x] FromModal fupd
   - [x] ElimModal bupd
-  - [ ] ElimModal fupd
+  - [x] ElimModal fupd
   - [ ] AddModal bupd
   - [ ] AddModal fupd
   - [ ] ElimAcc bupd
@@ -436,6 +440,8 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [ ] IClearFrame
 - [x] `modalities.v`
 - [ ] `modality_instances.v`
+  - [ ] modality_embed 
+  - [x] others
 - [ ] `monpred.v`
 - [x] `proofmode.v` (ProofMode.lean)
 - [-] `reduction.v` (not necessary in Lean)

src/Iris/BI/Updates.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Markus de Medeiros, Remy Seassau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus de Medeiros, Remy Seassau
+Authors: Markus de Medeiros, Remy Seassau, Yunsong Yang
 -/
 module
 
@@ -38,29 +38,46 @@ class FUpd (PROP : Type _) where
   fupd : CoPset → CoPset → PROP → PROP
 export FUpd (fupd)
 
-syntax "|={ " term " , " term " }=> " term : term
-syntax term "={ " term " , " term " }=∗ " term : term
-syntax "|={ " term " }=> " term : term
-syntax term "={ " term " }=∗ " term : term
+syntax "|={" term "," term "}=> " term : term
+syntax term "={" term "," term "}=∗ " term : term
+syntax "|={" term "}=> " term : term
+syntax term "={" term "}=∗ " term : term
 
 macro_rules
-  | `(iprop(|={ $E1 , $E2 }=> $P))  => ``(FUpd.fupd $E1 $E2 iprop($P))
-  | `(iprop($P ={ $E1 , $E2 }=∗ $Q))  => ``(BIBase.wand iprop($P) (FUpd.fupd $E1 $E2 iprop($Q)))
-  | `(iprop(|={ $E1 }=> $P))  => ``(FUpd.fupd $E1 $E1 iprop($P))
-  | `(iprop($P ={ $E1 }=∗ $Q))  => ``(BIBase.wand iprop($P) (FUpd.fupd $E1 $E1 iprop($Q)))
+  | `(iprop(|={$E1,$E2}=> $P))  => ``(FUpd.fupd $E1 $E2 iprop($P))
+  | `(iprop($P ={$E1,$E2}=∗ $Q))  => ``(BIBase.wand iprop($P) (FUpd.fupd $E1 $E2 iprop($Q)))
+  | `(iprop(|={$E1}=> $P))  => ``(FUpd.fupd $E1 $E1 iprop($P))
+  | `(iprop($P ={$E1}=∗ $Q))  => ``(BIBase.wand iprop($P) (FUpd.fupd $E1 $E1 iprop($Q)))
+
+delab_rule FUpd.fupd
+  | `($_ $E1 $E2 $P) => do
+      let P ← Iris.BI.unpackIprop P
+      if E1 == E2 then ``(iprop(|={$E1}=> $P))
+      else ``(iprop(|={$E1,$E2}=> $P))
+
+syntax "|={" term "}[" term "]▷=> " term : term
+syntax term "={" term "}[" term "]▷=∗ " term : term
+syntax "|={" term "}▷=> " term : term
+syntax term "={" term "}▷=∗ " term : term
+
+macro_rules
+  | `(iprop(|={$E1}[$E2]▷=> $P))  => ``(iprop(|={$E1,$E2}=> ▷ (|={$E2,$E1}=> iprop($P))))
+  | `(iprop($P ={$E1}[$E2]▷=∗ $Q))  => ``(iprop(iprop($P) -∗ |={$E1}[$E2]▷=> iprop($Q)))
+  | `(iprop(|={$E1}▷=> $P))  => ``(iprop(|={$E1}[$E1]▷=> iprop($P)))
+  | `(iprop($P ={$E1}▷=∗ $Q))  => ``(iprop(iprop($P) ={$E1}[$E1]▷=∗ iprop($Q)))
 
 -- Delab rules
 
-syntax "|={ " term " }[ " term " ]▷=> " term : term
-syntax term "={ " term " }[ " term " ]▷=∗ " term : term
-syntax "|={ " term " }▷=> " term : term
-syntax term "={ " term " }▷=∗ " term : term
+syntax "|={" term "}[" term "]▷^" term "=> " term : term
+syntax term "={" term "}[" term "]▷^" term "=∗ " term : term
+syntax "|={" term "}▷^" term "=> " term : term
+syntax term "={" term "}▷^" term "=∗ " term : term
 
 macro_rules
-  | `(iprop(|={ $E1 }[ $E2 ]▷=> $P))  => ``(iprop(|={$E1, $E2}=> ▷ (|={ $E2, $E1 }=> iprop($P))))
-  | `(iprop($P ={ $E1 }[ $E2 ]▷=∗ $Q))  => ``(iprop(iprop($P) -∗ |={$E1}[$E2]▷=> iprop($Q)))
-  | `(iprop(|={ $E1 }▷=> $P))  => ``(iprop(|={$E1}[$E1]▷=> iprop($P)))
-  | `(iprop($P ={ $E1 }▷=∗ $Q))  => ``(iprop(iprop($P) ={$E1}[$E1]▷=∗ iprop($Q)))
+  | `(iprop(|={$E1}[$E2]▷^$n=> $P))  => ``(iprop(|={$E1,$E2}=> ▷^[$n] (|={$E2,$E1}=> iprop($P))))
+  | `(iprop($P ={$E1}[$E2]▷^$n=∗ $Q))  => ``(iprop(iprop($P) -∗ |={$E1}[$E2]▷^$n=> iprop($Q)))
+  | `(iprop(|={$E1}▷^$n=> $P))  => ``(iprop(|={$E1}[$E1]▷^$n=> iprop($P)))
+  | `(iprop($P ={$E1}▷^$n=∗ $Q))  => ``(iprop(iprop($P) ={$E1}[$E1]▷^$n=∗ iprop($Q)))
 
 -- Delab rules
 
@@ -79,26 +96,26 @@ macro_rules
 
 class BIUpdate (PROP : Type _) [BI PROP] extends BUpd PROP where
   [bupd_ne : OFE.NonExpansive (BUpd.bupd (PROP := PROP))]
-  intro {P : PROP} : iprop(P ⊢ |==> P)
-  mono {P Q : PROP} : iprop(P ⊢ Q) → iprop(|==> P ⊢ |==> Q)
-  trans {P : PROP} : iprop(|==> |==> P ⊢ |==> P)
-  frame_r {P R : PROP} : iprop((|==> P) ∗ R ⊢ |==> (P ∗ R))
+  intro {P : PROP} : P ⊢ |==> P
+  mono {P Q : PROP} : (P ⊢ Q) → |==> P ⊢ |==> Q
+  trans {P : PROP} : |==> |==> P ⊢ |==> P
+  frame_r {P R : PROP} : (|==> P) ∗ R ⊢ |==> (P ∗ R)
 
 class BIFUpdate (PROP : Type _) [BI PROP] extends FUpd PROP where
   [ne {E1 E2 : CoPset} : OFE.NonExpansive (FUpd.fupd E1 E2 (PROP := PROP))]
-  subset {E1 E2 : CoPset} : Subset E2 E1 → ⊢ |={E1, E2}=> |={E2, E1}=> (emp : PROP)
-  except0 {E1 E2 : CoPset} (P : PROP) : (◇ |={E1, E2}=> P) ⊢ |={E1, E2}=> P
-  trans {E1 E2 E3 : CoPset} (P : PROP) : (|={E1, E2}=> |={E2, E3}=> P) ⊢ |={E1, E3}=> P
-  mask_frame_r' {E1 E2 Ef : CoPset} (P : PROP) :
-    E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ⊢ |={CoPset.union E1 Ef, CoPset.union E2 Ef}=> P
-  frame_r {E1 E2 : CoPset} (P R : PROP) :
-    iprop((|={E1, E2}=> P) ∗ R ⊢ |={E1, E2}=> P ∗ R)
+  subset {E1 E2 : CoPset} : E2 ⊆ E1 → ⊢ |={E1,E2}=> |={E2,E1}=> (emp : PROP)
+  except0 {E1 E2 : CoPset} {P : PROP} : (◇ |={E1,E2}=> P) ⊢ |={E1,E2}=> P
+  mono {E1 E2 : CoPset} {P Q : PROP} : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q
+  trans {E1 E2 E3 : CoPset} {P : PROP} : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P
+  mask_frame_r' {E1 E2 Ef : CoPset} {P : PROP} :
+    E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ⊢ |={E1 ∪ Ef,E2 ∪ Ef}=> P
+  frame_r {E1 E2 : CoPset} {P R : PROP} : (|={E1,E2}=> P) ∗ R ⊢ |={E1,E2}=> P ∗ R
 
 class BIUpdateFUpdate (PROP : Type _) [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] where
-  fupd_of_bupd {P : PROP} {E : CoPset} : iprop(⊢ |==> P) → iprop(⊢ |={E}=> P)
+  fupd_of_bupd {P : PROP} {E : CoPset} : (|==> P) ⊢ |={E}=> P
 
 class BIBUpdatePlainly (PROP : Type _) [BI PROP] [BIUpdate PROP] [Sbi PROP] where
-  bupd_plainly {P : PROP} : iprop((|==> ■ P)) ⊢ P
+  bupd_plainly {P : PROP} : (|==> ■ P) ⊢ P
 
 class BIFUpdatePlainly (PROP : Type _) [BI PROP] [BIFUpdate PROP] [Sbi PROP] where
   fupd_plainly_keep_l (E E' : CoPset) (P R : PROP) : (R ={E,E'}=∗ ■ P) ∗ R ⊢ |={E}=> P ∗ R
@@ -112,38 +129,38 @@ variable [BI PROP] [BIUpdate PROP]
 
 open BIUpdate
 
-theorem bupd_frame_l {P Q : PROP} : iprop(P ∗ |==> Q ⊢ |==> (P ∗ Q)) :=
+theorem bupd_frame_l {P Q : PROP} : P ∗ |==> Q ⊢ |==> (P ∗ Q) :=
   sep_symm.trans <| frame_r.trans <| mono sep_symm
 
-theorem bupd_frame_r {P Q : PROP} : iprop(|==> P ∗ Q ⊢ |==> (P ∗ Q)) :=
+theorem bupd_frame_r {P Q : PROP} : |==> P ∗ Q ⊢ |==> (P ∗ Q) :=
   frame_r
 
-theorem bupd_wand_l {P Q : PROP} : iprop((P -∗ Q) ∗ (|==> P) ⊢ |==> Q) :=
+theorem bupd_wand_l {P Q : PROP} : (P -∗ Q) ∗ (|==> P) ⊢ |==> Q :=
   bupd_frame_l.trans <| mono <| wand_elim .rfl
 
-theorem bupd_wand_r {P Q : PROP} : iprop((|==> P) ∗ (P -∗ Q) ⊢ |==> Q) :=
+theorem bupd_wand_r {P Q : PROP} : (|==> P) ∗ (P -∗ Q) ⊢ |==> Q :=
   sep_symm.trans bupd_wand_l
 
-theorem bupd_sep {P Q : PROP} : iprop((|==> P) ∗ (|==> Q) ⊢ |==> (P ∗ Q)) :=
+theorem bupd_sep {P Q : PROP} : (|==> P) ∗ (|==> Q) ⊢ |==> (P ∗ Q) :=
   bupd_frame_l.trans <| (mono <| frame_r).trans BIUpdate.trans
 
-theorem bupd_idem {P : PROP} : iprop((|==> |==> P) ⊣⊢ |==> P) :=
+theorem bupd_idem {P : PROP} : (|==> |==> P) ⊣⊢ |==> P :=
   ⟨BIUpdate.trans, BIUpdate.intro⟩
 
-theorem bupd_or {P Q: PROP} : iprop((|==> P) ∨ (|==> Q) ⊢ |==> (P ∨ Q)) :=
+theorem bupd_or {P Q: PROP} : (|==> P) ∨ (|==> Q) ⊢ |==> (P ∨ Q) :=
   or_elim (mono or_intro_l) (mono or_intro_r)
 
-theorem bupd_and {P Q : PROP} : iprop((|==> (P ∧ Q)) ⊢ (|==> P) ∧ (|==> Q)) :=
+theorem bupd_and {P Q : PROP} : (|==> (P ∧ Q)) ⊢ (|==> P) ∧ (|==> Q) :=
   and_intro (mono and_elim_l) (mono and_elim_r)
 
 theorem bupd_exist {Φ : A → PROP} : (∃ x : A, |==> Φ x) ⊢ |==> ∃ x : A, Φ x :=
   exists_elim (mono <| exists_intro ·)
 
 theorem bupd_forall {Φ : A → PROP} :
-    iprop(|==> «forall» fun x : A => Φ x) ⊢ «forall» fun x : A => iprop(|==> Φ x) :=
+    (|==> «forall» fun x : A => Φ x) ⊢ «forall» fun x : A => iprop(|==> Φ x) :=
   forall_intro (mono <| forall_elim ·)
 
-theorem bupd_except0 {P : PROP} : iprop(◇ (|==> P) ⊢ (|==> ◇ P)) :=
+theorem bupd_except0 {P : PROP} : ◇ (|==> P) ⊢ (|==> ◇ P) :=
   or_elim (or_intro_l.trans intro) (mono or_intro_r)
 
 instance {P : PROP} [Absorbing P] : Absorbing iprop(|==> P) :=
@@ -170,3 +187,114 @@ instance {P : PROP} [Plain P] : Plain iprop(|==> P) :=
   ⟨(mono Plain.plain).trans <| (bupd_elim).trans <| plainly_mono intro⟩
 
 end BUpdPlainlyLaws
+
+section FUpdLaws
+
+variable [BI PROP] [BIFUpdate PROP]
+
+open BIFUpdate LawfulSet
+
+theorem fupd_mask_intro_subseteq {E1 E2 : CoPset} {P : PROP} : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P :=
+  λ h => (emp_sep.2.trans <| sep_mono_l <| subset h).trans <|
+    frame_r.trans <| mono <| frame_r.trans <| mono emp_sep.1
+
+theorem fupd_intro {E : CoPset} {P : PROP} : P ⊢ |={E}=> P :=
+  (fupd_mask_intro_subseteq λ _ => id).trans trans
+
+-- Introduction lemma for a mask-chaging fupd
+theorem fupd_mask_intro {E1 E2 : CoPset} {P : PROP} :
+    E2 ⊆ E1 → ((|={E2,E1}=> emp) -∗ P) ⊢ |={E1,E2}=> P :=
+  λ h => (wand_mono_r fupd_intro).trans <|
+    (emp_sep.2.trans <| sep_mono_l <| subset h).trans <|
+    frame_r.trans <| (mono wand_elim_r).trans trans
+
+theorem fupd_mask_intro_discard {E1 E2 : CoPset} {P : PROP} [Absorbing P] : E2 ⊆ E1 → P ⊢ |={E1,E2}=> P :=
+  λ h => (wand_intro' sep_elim_r).trans <| fupd_mask_intro h
+
+theorem fupd_elim {E1 E2 E3 : CoPset} {P Q : PROP} : (Q ⊢ |={E2,E3}=> P) → (|={E1,E2}=> Q) ⊢ |={E1,E3}=> P :=
+  λ h => (mono h).trans trans
+
+theorem fupd_frame_l {E1 E2 : CoPset} {P Q : PROP} : P ∗ (|={E1,E2}=> Q) ⊢ |={E1,E2}=> P ∗ Q :=
+  sep_symm.trans <| frame_r.trans <| mono sep_symm
+
+theorem fupd_frame_r {E1 E2 : CoPset} {P Q : PROP} : (|={E1,E2}=> P) ∗ Q ⊢ |={E1,E2}=> P ∗ Q :=
+  frame_r
+
+theorem fupd_wand_l {E1 E2 : CoPset} {P Q : PROP} : (P -∗ Q) ∗ (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q :=
+  fupd_frame_l.trans <| mono <| wand_elim .rfl
+
+theorem fupd_wand_r {E1 E2 : CoPset} {P Q : PROP} : (|={E1,E2}=> P) ∗ (P -∗ Q) ⊢ |={E1,E2}=> Q :=
+  sep_symm.trans fupd_wand_l
+
+theorem fupd_sep {E : CoPset} {P Q : PROP} : (|={E}=> P) ∗ (|={E}=> Q) ⊢ |={E}=> P ∗ Q :=
+  fupd_frame_l.trans <| (mono frame_r).trans trans
+
+theorem fupd_idem {E : CoPset} {P : PROP} : (|={E}=> |={E}=> P) ⊣⊢ |={E}=> P := ⟨trans, fupd_intro⟩
+
+theorem fupd_or {E1 E2 : CoPset} {P Q : PROP} : (|={E1,E2}=> P) ∨ (|={E1,E2}=> Q) ⊢ |={E1,E2}=> P ∨ Q :=
+  or_elim (mono or_intro_l) (mono or_intro_r)
+
+theorem fupd_and {E1 E2 : CoPset} {P Q : PROP} : (|={E1,E2}=> P ∧ Q) ⊢ (|={E1,E2}=> P) ∧ (|={E1,E2}=> Q) :=
+  and_intro (mono and_elim_l) (mono and_elim_r)
+
+theorem fupd_exist {E1 E2 : CoPset} {Φ : A → PROP} : (∃ a : A, |={E1,E2}=> Φ a) ⊢ |={E1,E2}=> ∃ a : A, Φ a :=
+  exists_elim (mono <| exists_intro ·)
+
+theorem fupd_forall {E1 E2 : CoPset} {Φ : A → PROP} :
+    (|={E1,E2}=> «forall» λ a : A => Φ a) ⊢ «forall» λ a : A => iprop(|={E1,E2}=> Φ a) :=
+  forall_intro (mono <| forall_elim ·)
+
+theorem fupd_except0 {E1 E2 : CoPset} {P : PROP} : (◇ |={E1,E2}=> P) ⊢ |={E1,E2}=> ◇ P :=
+  except0.trans (mono except0_intro)
+
+instance {E1 E2 : CoPset} {P : PROP} [Absorbing P] : Absorbing iprop(|={E1,E2}=> P) :=
+  ⟨fupd_frame_l.trans <| mono sep_elim_r⟩
+
+theorem fupd_mask_frame_r {E1 E2 Ef : CoPset} {P : PROP} :
+    E1 ## Ef → (|={E1,E2}=> P) ⊢ |={E1 ∪ Ef,E2 ∪ Ef}=> P :=
+  λ h => (mono <| imp_intro' and_elim_r).trans <| mask_frame_r' h
+
+theorem fupd_mask_mono {E1 E2 : CoPset} {P : PROP} :
+    E1 ⊆ E2 → (|={E1}=> P) ⊢ |={E2}=> P :=
+  λ h => by simpa [subset_union_diff h] using
+    (fupd_mask_frame_r (E2 := E1) (Ef := E2 \ E1) disjoint_diff_right)
+
+theorem fupd_mask_frame {E E' E1 E2 : CoPset} {P : PROP} :
+    E1 ⊆ E → (|={E1,E2}=> |={E2 ∪ (E \ E1),E'}=> P) ⊢ |={E,E'}=> P :=
+  λ h => by simpa [subset_union_diff h] using
+    ((fupd_mask_frame_r (P := iprop(|={E2 ∪ (E \ E1),E'}=> P)) disjoint_diff_right).trans trans)
+
+/-- A variant of [fupd_mask_frame] that works well for accessors:
+  Tailored to eliminate updates of the form [|={E1,E1∖E2}=> Q] and provides a way to transform the
+  closing view shift instead of letting you prove the same side-conditions twice. -/
+theorem fupd_mask_frame_acc {E E' E1 E2 : CoPset} {P Q : PROP}:
+    E1 ⊆ E → (|={E1,E1 \ E2}=> Q) ⊢
+    (Q -∗ |={E \ E2,E'}=> (∀ R, (|={E1 \ E2,E1}=> R) -∗ |={E \ E2,E}=> R) -∗  P) -∗
+    (|={E,E'}=> P) := λ hE => by
+  have hmask : E \ E2 ⊆ (E1 \ E2) ∪ (E \ E1) := by
+    intro x hx; rw [mem_diff] at hx
+    by_cases hx1 : x ∈ E1
+    · exact mem_union.2 <| .inl <| mem_diff.2 ⟨hx1, hx.2⟩
+    · exact mem_union.2 <| .inr <| mem_diff.2 ⟨hx.1, hx1⟩
+  have hdisj : (E1 \ E2) ## (E \ E1) := disjoint_subset_left diff_subset_left disjoint_diff_right
+  refine wand_intro <| fupd_frame_r.trans <| (BIFUpdate.mono wand_elim_r).trans ?_
+  refine (BIFUpdate.mono ?_).trans <| fupd_mask_frame hE
+  refine sep_emp.2.trans <| (sep_mono_r <| fupd_mask_intro_subseteq hmask).trans ?_
+  refine fupd_frame_l.trans <| (BIFUpdate.mono fupd_frame_r).trans <| fupd_elim ?_
+  refine BIFUpdate.mono <| sep_symm.trans ?_
+  refine (sep_mono ?_ .rfl).trans wand_elim_r
+  refine forall_intro λ R => wand_intro <| fupd_frame_r.trans <| fupd_elim ?_
+  exact emp_sep.1.trans <| (fupd_mask_frame_r hdisj).trans <| by simp [subset_union_diff hE]
+
+theorem fupd_mask_subseteq_emptyset_difference {E1 E2 : CoPset} :
+    E2 ⊆ E1 → ⊢@{PROP} |={E1,E2}=> |={∅,E1\E2}=> emp :=
+  λ h => by
+    simpa [union_comm, subset_union_diff h] using (fupd_mask_intro_subseteq empty_subset).trans <|
+      fupd_mask_frame_r (P := iprop(|={∅,E1 \ E2}=> (emp : PROP))) (disjoint_symm <| disjoint_diff_right)
+
+theorem fupd_trans_frame {E1 E2 E3 : CoPset} {P Q : PROP} :
+    ((Q ={E2,E3}=∗ emp) ∗ |={E1,E2}=> (Q ∗ P)) ⊢ |={E1,E3}=> P :=
+  fupd_frame_l.trans <| fupd_elim <| ((sep_assoc.2.trans <| sep_mono_l sep_comm.1).trans <|
+    sep_mono_l wand_elim_r).trans <| fupd_frame_r.trans <| BIFUpdate.mono emp_sep.1
+
+end FUpdLaws

src/Iris/Examples/Proofs.lean

@@ -16,7 +16,7 @@ open Iris.BI
 theorem proof_example_1 [BI PROP] (P Q R : PROP) (Φ : α → PROP) :
   P ∗ Q ∗ □ R ⊢ □ (R -∗ ∃ x, Φ x) -∗ ∃ x, Φ x ∗ P ∗ Q
 := by
-  iintro ⟨HP, HQ, □HR⟩ □HRΦ
+  iintro ⟨HP, HQ, #HR⟩ #HRΦ
   ihave HΦ := HRΦ $$ HR
   icases HΦ with ⟨%x, _HΦ⟩
   iexists x

src/Iris/ProofMode/Classes.lean

@@ -14,6 +14,10 @@ public import Iris.ProofMode.Modalities
 namespace Iris.ProofMode
 open Iris.BI
 
+/-- [PMError] is used as precondition on "failing" instances of typeclasses
+  that have pure preconditions (such as [ElimModal]) -/
+inductive PMError (msg : String) : Prop
+
 /-- [InOut] is used to dynamically determine whether a type class
 parameter is an input or an output. This is important for classes that
 are used with multiple modings, e.g., IntoWand. Instances can match on
@@ -36,7 +40,6 @@ theorem asEmpValid_1 [BI PROP] (P : PROP) [AsEmpValid .into φ P] : φ → ⊢ P
 theorem asEmpValid_2 [BI PROP] (φ : Prop) [AsEmpValid .from φ (P : PROP)] : (⊢ P) → φ :=
   AsEmpValid.as_emp_valid.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
 proposition can be derived. Type classes with the prefix `Into` are used to generate propositions
@@ -126,7 +129,6 @@ class IntoAbsorbingly [BI PROP] (P : outParam PROP) (Q : PROP) where
   into_absorbingly : P ⊢ <absorb> Q
 export IntoAbsorbingly (into_absorbingly)
 
-
 @[ipm_class]
 class FromAssumption (p : Bool) [BI PROP] (ioP : InOut) (P : semiOutParam PROP) (Q : PROP) where
   from_assumption : □?p P ⊢ Q