feat: iinv

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

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
 

Iris/Iris/HeapLang/ProofMode.lean

@@ -230,7 +230,7 @@ public meta def iWpValueHead {u}
   let p' : Q(Bool) ← mkFreshExprMVarQ q(Bool)
   let A' : Q(IProp $GF) ← mkFreshExprMVarQ q(IProp $GF)
   let Q' : Q(IProp $GF) ← mkFreshExprMVarQ q(IProp $GF)
-  if let .some _ ← ProofModeM.trySynthInstanceQ q(ElimModal $c false $p' iprop(|={$E}=> $goal) $A' $goal $Q') then
+  if let .some _ ← ProofModeM.trySynthInstanceQ q(ElimModal $c false .out $p' iprop(|={$E}=> $goal) $A' $goal $Q') then
     if let some _ ← try? <| iSolveSidecondition c then
       let pf ← addBIGoal hyps q($goal)
       return some q(tac_wp_value_nofupd (s:=$s) (E:=$E) $pf)

Iris/Iris/Instances/Lib/CInvariants.lean

@@ -20,7 +20,7 @@ public import Iris.Std.List
 
 namespace Iris
 
-open BI CMRA OFE Iris Std LawfulSet Excl COFE
+open BI CMRA OFE Iris Std LawfulSet Excl COFE ProofMode
 
 /-! # Cancelable Invariants -/
 
@@ -289,6 +289,27 @@ theorem cancel (E : CoPset) {N : Namespace} {γ : GName} {P : IProp GF} (Hsub :
   imodintro
   iexact HP
 
+@[rocq_alias into_inv_cinv]
+instance intoInv_cinv (N : Namespace) (γ : GName) (P : IProp GF) :
+    IntoInv (cinv N γ P) N := {}
+
+set_option synthInstance.checkSynthOrder false in
+@[rocq_alias into_acc_cinv]
+instance intoAcc_cinv (E : CoPset) (N : Namespace) (γ : GName) (P : IProp GF) (p : Qp) :
+    IntoAcc (X := Unit) (cinv N γ P) (↑N ⊆ E) (own γ p) (fupd E (E \ ↑N)) (fupd (E \ ↑N) E)
+      (fun _ => iprop(▷ P ∗ own γ p)) (fun _ => iprop(▷ P)) (λ _ => none) where
+  into_acc := by
+    dsimp only [accessor, Option.getD]
+    iintro %x #Hinv Hown
+    imod acc x $$ Hinv Hown with ⟨HP, Hγ, Hcl⟩
+    imodintro
+    iexists ()
+    isplitl [HP Hγ]
+    · iframe
+    · iintro HP
+      iapply (BIFUpdate.mono true_emp.mp)
+      iapply Hcl $$ HP
+
 end CancelableInvariant
 end Iris
 end

Iris/Iris/Instances/Lib/FUpd.lean

@@ -379,8 +379,8 @@ instance isExcept0_fupd_finally (E : CoPset) (P : IProp GF) : IsExcept0 iprop(|=
     iapply except0_mono fupd_intro $$ H
 
 @[rocq_alias elim_modal_bupd_fupd_finally]
-instance elimModal_bupd_fupd_finally p (E : CoPset) (P Q : IProp GF) :
-    ElimModal True p false iprop(|==> P) P iprop(|={E|}=> Q) iprop(|={E|}=> Q) where
+instance elimModal_bupd_fupd_finally p io (E : CoPset) (P Q : IProp GF) :
+    ElimModal True p io false iprop(|==> P) P iprop(|={E|}=> Q) iprop(|={E|}=> Q) where
   elim_modal _ := by
     iintro ⟨H1, H2⟩
     iapply fupd_fupd_finally E E
@@ -390,8 +390,8 @@ instance elimModal_bupd_fupd_finally p (E : CoPset) (P Q : IProp GF) :
     iapply H2 $$ H1
 
 @[rocq_alias elim_modal_fupd_fupd_finally]
-instance elimModal_fupd_fupd_finally p (E1 E2 : CoPset) (P Q : IProp GF) :
-    ElimModal True p false iprop(|={E1,E2}=> P) P iprop(|={E1|}=> Q) iprop(|={E2|}=> Q) where
+instance elimModal_fupd_fupd_finally p io (E1 E2 : CoPset) (P Q : IProp GF) :
+    ElimModal True p io false iprop(|={E1,E2}=> P) P iprop(|={E1|}=> Q) iprop(|={E2|}=> Q) where
   elim_modal _ := by
     iintro ⟨H1, H2⟩
     iapply fupd_fupd_finally E1 E2

Iris/Iris/Instances/Lib/Invariants.lean

@@ -87,7 +87,26 @@ theorem except_0_inv (N : Namespace) (P : IProp GF) : ⊢ ◇ inv N P -∗ inv N
 instance is_except_0_inv (N : Namespace) (P : IProp GF) : IsExcept0 (inv N P) where
   is_except0 := by iintro H; iapply except_0_inv $$ H
 
--- TODO: into_inv_inv, into_acc_inv
+@[rocq_alias into_inv_inv]
+instance intoInv_inv (N : Namespace) (P : IProp GF) : IntoInv (inv N P) N := {}
+
+set_option synthInstance.checkSynthOrder false in
+@[rocq_alias into_acc_inv]
+instance intoAcc_inv (N : Namespace) (P : IProp GF) E :
+    IntoAcc (X := Unit) (inv N P) (↑N ⊆ E) iprop(True) (fupd E (E \ ↑N)) (fupd (E \ ↑N) E)
+      (λ _ => iprop(▷ P)) (λ _ => iprop(▷ P)) (λ _ => none) where
+  into_acc := by
+    dsimp only [inv, accessor, Option.getD]
+    iintro %x #Hinv -
+    imod Hinv $$ %E [] with ⟨HP, Hclose⟩
+    · itrivial
+    · iexists ()
+      imodintro
+      isplitl [HP]
+      · iassumption
+      · iintro HP
+        iapply (BIFUpdate.mono true_emp.mp)
+        iapply Hclose $$ HP
 
 end Instances
 

Iris/Iris/Instances/Lib/LaterCredits.lean

@@ -429,7 +429,7 @@ open ProofMode
 variable {GF : BundledGFunctors} {hlc : HasLC} [LcGS hlc GF]
 
 @[rocq_alias le_upd.elim_bupd_le_upd]
-instance {P : IProp GF} : ElimModal True p false (bupd P) P (le_upd Q) (le_upd Q) where
+instance {P Q : IProp GF} : ElimModal True p io false (bupd P) P (le_upd Q) (le_upd Q) where
   elim_modal := by
     cases p <;> (dsimp; intro _)
     · iintro ⟨H1, H2⟩
@@ -466,7 +466,7 @@ instance {P : IProp GF} : FromModal True modality_id (le_upd P) (le_upd P) P whe
     iapply le_upd_intro
 
 @[rocq_alias le_upd.elim_modal_le_upd]
-instance {P : IProp GF} : ElimModal True p false (le_upd P) P (le_upd Q) (le_upd Q) where
+instance {P Q : IProp GF} : ElimModal True p io false (le_upd P) P (le_upd Q) (le_upd Q) where
   elim_modal := by
     intro _
     cases p <;> dsimp

Iris/Iris/Instances/Lib/NaInvariants.lean

@@ -17,7 +17,7 @@ public import Iris.Std.CoPset
 
 namespace Iris
 
-open BI CMRA OFE Iris Std LawfulSet DisjointLeibnizSet COFE
+open BI CMRA OFE Iris Std LawfulSet DisjointLeibnizSet COFE ProofMode
 
 abbrev NaInvF : OFunctorPre :=
   ProdOF (constOF CoPsetDisjL) (constOF (DisjointLeibnizSet PosSet))
@@ -221,6 +221,24 @@ nonrec theorem inv_acc {p : NaInvPoolName} {E F : CoPset} {N : Namespace} {P : I
     icases Hbad with %Hbad
     exact Hbad i ⟨mem_singleton.mpr rfl, mem_singleton.mpr rfl⟩ |>.elim
 
+@[rocq_alias into_inv_na]
+instance intoInv_na (N : Namespace) (P : IProp GF) :
+    IntoInv (inv p N P) N := {}
+
+set_option synthInstance.checkSynthOrder false in
+@[rocq_alias into_acc_na]
+instance intoAcc_na (p : NaInvPoolName) (E F : CoPset) (N : Namespace) (P : IProp GF) :
+    IntoAcc (X := Unit) (inv p N P) (↑N ⊆ E ∧ ↑N ⊆ F) (own p F) (fupd E E) (fupd E E)
+    (fun _ => iprop(▷ P ∗ own p (F \ ↑N))) (fun _ => iprop(▷ P ∗ own p (F \ ↑N)))
+              (λ _ => some (own p F)) where
+  into_acc := by
+    dsimp only [accessor, Option.getD]
+    intro ⟨hE, hF⟩
+    iintro #Hinv Hown
+    imod inv_acc hE hF $$ Hinv Hown with ⟨_, Hown, _⟩
+    iexists ()
+    iframe
+
 end NonAtomicInvariant
 end Iris
 end

Iris/Iris/ProgramLogic/WeakestPre.lean

@@ -8,13 +8,14 @@ public import Iris.Algebra
 public import Iris.Instances.Lib.FUpd
 public import Iris.BI
 public import Iris.BI.WeakestPre
+public import Iris.BI.DerivedLaws
 public import Iris.ProofMode
 public import Iris.ProgramLogic.Language
 public import Iris.Std.CoPset
 
 namespace Iris
 
-open ProgramLogic Language.Notation Std
+open ProgramLogic Language.Notation Std Iris.BI
 
 @[expose] public section
 
@@ -638,7 +639,7 @@ instance isExcept0Wp : IsExcept0 (WP e @ s ; E {{ Φ }}) where
 -- this should have higher priority than elimModalFupdWpAtomic
 @[rocq_alias elim_modal_fupd_wp]
 instance (priority := default + 10) elimModalFupdWp p :
-    ElimModal True p false iprop(|={E}=> P) P (WP e @ s ; E {{ Φ }}) (WP e @ s ; E {{ Φ }}) where
+    ElimModal True p io false iprop(|={E}=> P) P (WP e @ s ; E {{ Φ }}) (WP e @ s ; E {{ Φ }}) where
   elim_modal := by
     iintro %_ ⟨H, G⟩
     icases BI.intuitionisticallyIf_elim $$ H with H
@@ -648,11 +649,11 @@ instance (priority := default + 10) elimModalFupdWp p :
 
 @[rocq_alias elim_modal_bupd_wp]
 instance elimModalBupdWp p :
-    ElimModal True p false iprop(|==> P) P (WP e @ s ; E {{ Φ }}) (WP e @ s ; E {{ Φ }}) where
+    ElimModal True p io false iprop(|==> P) P (WP e @ s ; E {{ Φ }}) (WP e @ s ; E {{ Φ }}) where
   elim_modal := by
     rintro ⟨⟩
     refine BI.sep_mono (BI.intuitionisticallyIf_mono (BIUpdateFUpdate.fupd_of_bupd (E := E))) .rfl |>.trans ?_
-    apply elimModalFupdWp _ |>.elim_modal ⟨⟩
+    exact elimModalFupdWp _ |>.elim_modal ⟨⟩ (io := io)
 
 /-- Error message instance for non-mask-changing view shifts.  Also uses a slightly
 different error: we cannot apply `fupd_mask_subseteq` if `e` is not atomic, so
@@ -661,12 +662,12 @@ we tell the user to first add a leading `fupd` and then change the mask of that.
 instance elimModalFupdWp_wrongMask :
     ElimModal (PMError "Goal and eliminated modality must have the same mask.
     Use `iapply fupd_wp; imod (fupd_mask_subseteq E₂)` to adjust the mask of your goal to `E₂`")
-    p false iprop(|={E₂}=> P) iprop(False) (WP e @ s ; E₁ {{ Φ }}) iprop(False) where
+    p io false iprop(|={E₂}=> P) iprop(False) (WP e @ s ; E₁ {{ Φ }}) iprop(False) where
   elim_modal := nofun
 
 @[rocq_alias elim_modal_fupd_wp_atomic]
 instance elimModalFupdWpAtomic :
-    ElimModal (Language.Atomic ↑s e) p false iprop(|={E₁,E₂}=> P) P (WP e @ s ; E₁ {{ Φ }}) (WP e @ s ; E₂ {{ v, |={E₂,E₁}=> Φ v}}) where
+    ElimModal (Language.Atomic ↑s e) p io false iprop(|={E₁,E₂}=> P) P (WP e @ s ; E₁ {{ Φ }}) (WP e @ s ; E₂ {{ v, |={E₂,E₁}=> Φ v}}) where
   elim_modal := by
     rintro atomic; iintro ⟨H, G⟩
     icases BI.intuitionisticallyIf_elim $$ H with H
@@ -678,7 +679,43 @@ instance elimModalFupdWpAtomic :
 instance elimModalFupdWpAtomic_wrongMask :
     ElimModal (PMError "Goal and eliminated modality must have the same mask.
     Use `iapply fupd_wp; imod (fupd_mask_subseteq E₂)` to adjust the mask of your goal to `E₂`")
-    p false iprop(|={E₁,E₂}=> P) iprop(False) (WP e @ s ; E₁ {{ Φ }}) iprop(False) where
+    p io false iprop(|={E₁,E₂}=> P) iprop(False) (WP e @ s ; E₁ {{ Φ }}) iprop(False) where
   elim_modal := nofun
 
+@[rocq_alias elim_acc_wp_atomic]
+instance (priority := low) elimAcc_wp_atomic {X} (E₁ E₂ : CoPset) α β (γ : X → Option (IProp GF)) :
+    ElimAcc (Language.Atomic ↑s e) (fupd E₁ E₂) (fupd E₂ E₁) α β γ
+      (WP e @ s ; E₁ {{ Φ }})
+      (fun x => WP e @ s ; E₂ {{ v, |={E₂}=> β x ∗ (γ x -∗? Φ v) }}) where
+  elim_acc := by
+    dsimp only [accessor, BIBase.wandM, Option.getD]
+    iintro %atomic Hinner >⟨%x, Hα, Hclose⟩
+    iapply wp_wand $$ [Hinner Hα]
+    · iapply Hinner $$ Hα
+    · iintro %v >⟨Hβ, HΦ⟩
+      ispecialize Hclose $$ Hβ
+      imod Hclose
+      imodintro
+      cases (γ x) with
+      | none => iexact HΦ
+      | some P => iapply HΦ $$ Hclose
+
+@[rocq_alias elim_acc_wp_nonatomic]
+instance elimAcc_wp_nonatomic {X} E (α β : X → IProp GF) (γ : X → Option (IProp GF)) :
+    ElimAcc True (fupd E E) (fupd E E) α β γ (WP e @ s ; E {{ Φ }})
+    (fun x => WP e @ s ; E {{ v, |={E}=> β x ∗ (γ x -∗? Φ v) }}) where
+  elim_acc := by
+    dsimp only [accessor, BIBase.wandM, Option.getD]
+    iintro %_ Hinner >⟨%x, Hα, Hclose⟩
+    iapply wp_fupd
+    iapply wp_wand $$ [Hinner Hα]
+    · iapply Hinner $$ Hα
+    · iintro %v >⟨Hβ, HΦ⟩
+      ispecialize Hclose $$ Hβ
+      imod Hclose
+      imodintro
+      cases (γ x) with
+      | none => iexact HΦ
+      | some P => iapply HΦ $$ Hclose
+
 end ProofModeClasses

Iris/Iris/ProofMode/Classes.lean

@@ -8,6 +8,7 @@ module
 public import Iris.BI
 public meta import Iris.ProofMode.SynthInstance
 public import Iris.ProofMode.Modalities
+public import Iris.Std.Namespaces
 
 @[expose] public section
 
@@ -205,8 +206,9 @@ export FromModal (from_modal)
 
 /-- `ElimModal` turns `□?p P` into `□?p' P'` and `Q` into `Q'` under condition `φ`. -/
 @[ipm_class, rocq_alias ElimModal]
-class ElimModal {PROP} [BI PROP] (φ : outParam $ Prop) (p : Bool) (p' : outParam $ Bool) (P : PROP)
-    (P' : outParam $ PROP) (Q : PROP) (Q' : outParam $ PROP) where
+class ElimModal {PROP} [BI PROP] (φ : outParam $ Prop) (p : Bool) (io : InOut)
+    (p' : semiOutParamIPM io Bool) (P : PROP)
+    (P' : semiOutParamIPM io PROP) (Q : PROP) (Q' : outParam $ PROP) where
   elim_modal : φ → □?p P ∗ (□?p' P' -∗ Q') ⊢ Q
 export ElimModal (elim_modal)
 
@@ -249,6 +251,38 @@ class CombineSepGives [BI PROP] (P Q : PROP) (R : outParam PROP) where
   combine_sep_gives : P ∗ Q ⊢ <pers> R
 export CombineSepGives (combine_sep_gives)
 
+@[ipm_class, rocq_alias IntoInv]
+class IntoInv [BI PROP] (P : PROP) (N : Namespace)
+
+@[rocq_alias accessor]
+def accessor [BI PROP] {X : Type} (M1 M2 : PROP → PROP) (α β : X → PROP)
+    (mγ : X → Option  PROP) : PROP :=
+  M1 iprop(∃ x, α x ∗ (β x -∗ M2 (mγ x |>.getD emp)))
+
+@[ipm_class, rocq_alias ElimAcc]
+class ElimAcc [BI PROP] {X : Type} (ϕ : outParam Prop) (M1 M2 : PROP → PROP)
+    (α β : X → PROP) (mγ : X → Option PROP) (Q : PROP) (Q' : outParam <| X → PROP) where
+  elim_acc : ϕ → ((∀ x, α x -∗ Q' x) -∗ accessor M1 M2 α β mγ -∗ Q)
+
+@[ipm_class, rocq_alias IntoAcc]
+class IntoAcc [BI PROP] {X : outParam Type} (Pacc : PROP)
+    (ϕ : outParam Prop) (Pin : outParam <| PROP)
+    (M1 M2 : outParam <| PROP → PROP) (α β : outParam <| X → PROP)
+    (mγ : outParam <| X → Option PROP) where
+  into_acc : ϕ → Pacc -∗ Pin -∗ accessor M1 M2 α β mγ
+
+set_option synthInstance.checkSynthOrder false in
+/-- The type class used for the `iinv` tactic. -/
+@[ipm_class, rocq_alias ElimInv]
+class ElimInv [BI PROP] (φ : outParam Prop) (X : outParam Type)
+    (Pinv : PROP) (Pin : outParam PROP) (Pout : outParam <| X → PROP)
+    (close : Bool) (mPclose : outParam <| Option <| X → PROP)
+    (Q : PROP) (Q' : outParam <| X → PROP) where
+  elim_inv : φ → Pinv ∗ Pin ∗ (∀ x, (match mPclose with
+    | some Pclose => iprop(Pout x ∗ Pclose x -∗ Q' x)
+    | none => iprop(Pout x -∗ Q' x))) ⊢ Q
+export ElimInv (elim_inv)
+
 /-
   `IntoIH φ P Q` describes how to turn a pure induction hypothesis `φ` into a proofmode
   hypothesis `Q` under an intuitionistic BI context `□ P`.

Iris/Iris/ProofMode/Expr.lean

@@ -184,6 +184,20 @@ partial def Hyps.find? {u prop bi} (name : Name) :
   | _, .hyp _ name' ivar _ ty _ => if name == name' then (ivar, ty) else none
   | _, .sep _ _ _ _ lhs rhs => rhs.find? name <|> lhs.find? name
 
+partial def Hyps.findM? [Monad m] {prop : Q(Type u)} {bi : Q(BI $prop)}
+    (p : Name → IVarId → Q(Bool) → Q($prop) → m Bool) :
+    ∀ {e}, Hyps bi e → m (Option (Name × IVarId × Q(Bool) × Q($prop)))
+  | _, .emp _ => return none
+  | _, .hyp _ name ivar bp ty _ => do
+    if ← p name ivar bp ty then
+      return some (name, ivar, bp, ty)
+    else
+      return none
+  | _, .sep _ _ _ _ lhs rhs => do
+    match ← rhs.findM? p with
+    | some res => return some res
+    | none => lhs.findM? p
+
 partial def Hyps.getDecl? {u prop bi} (ivar : IVarId) {s}:
     @Hyps u prop bi s → Option (Name × IVarId × Q(Bool) × Q($prop))
   | .emp _ => none