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/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/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/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 (DisjointLeibnizSet CoPset)) (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
 
@@ -681,4 +682,40 @@ instance elimModalFupdWpAtomic_wrongMask :
     p 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
 
@@ -180,8 +181,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)
+    (p' : outParam $ uncheckedInParam Bool) (P : PROP)
+    (P' : outParam $ uncheckedInParam PROP) (Q : PROP) (Q' : outParam $ PROP) where
   elim_modal : φ → □?p P ∗ (□?p' P' -∗ Q') ⊢ Q
 export ElimModal (elim_modal)
 
@@ -224,6 +226,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)
+
 #rocq_ignore elim_inv_tc_opaque "No tc_opaque in Lean"
 #rocq_ignore elim_modal_tc_opaque "No tc_opaque in Lean"
 #rocq_ignore from_and_tc_opaque "No tc_opaque in Lean"

Iris/Iris/ProofMode/Instances.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Lars König, Mario Carneiro, Alvin Tang
+Authors: Lars König, Mario Carneiro, Michael Sammler, Alvin Tang
 -/
 module
 
@@ -10,6 +10,8 @@ public import Iris.ProofMode.Classes
 public import Iris.ProofMode.ModalityInstances
 public import Iris.Std.TC
 public import Iris.Std.RocqPorting
+public import Iris.ProofMode.Tactics
+public import Iris.ProofMode.Display
 
 @[expose] public section
 
@@ -51,6 +53,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"
@@ -84,6 +92,13 @@ instance intoWand_and_r (p q : Bool) [BI PROP] (R1 R2 P' Q' : PROP)
 instance intoWand_wandIff (p q : Bool) [BI PROP] (R1 R2 P' Q' : PROP)
     [h : IntoWand p q iprop((R1 -∗ R2) ∧ (R2 -∗ R1)) ioP P' ioQ Q'] : IntoWand p q iprop(R1 ∗-∗ R2) ioP P' ioQ Q' := h
 
+@[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
+
 -- The set_option is ok since this is an instance for an IPM class and thus can create mvars.
 set_option synthInstance.checkSynthOrder false in
 @[rocq_alias into_wand_forall]
@@ -846,6 +861,14 @@ instance elimModal_wand [BI PROP] φ p p' (P P' Q Q' R : PROP) [h : ElimModal φ
        wand_intro_left $ sep_assoc.2.trans _).trans (h.1 hφ))
      apply (sep_mono_left sep_comm.1).trans (sep_assoc.1.trans $ wand_elim_swap $ wand_elim_swap .rfl)
 
+@[rocq_alias elim_modal_wandM]
+instance elimModal_wandM [BI PROP] φ p p' (P P' Q Q' : PROP) (mR : Option PROP)
+    [h : ElimModal φ p p' P P' Q Q'] :
+    ElimModal φ p p' P P' iprop(mR -∗? Q) iprop(mR -∗? Q') where
+  elim_modal hφ :=
+    (sep_mono_right <| wand_mono_right wandM_sound.mp).trans <|
+    ((elimModal_wand φ p p' P P' Q Q' (mR.getD emp)).elim_modal hφ).trans wandM_sound.mpr
+
 @[rocq_alias elim_modal_forall]
 instance elimModal_forall [BI PROP] φ p p' P P' (Φ Ψ : α → PROP) [h : ∀ x, ElimModal φ p p' P P' (Φ x) (Ψ x)] :
   ElimModal φ p p' P P' iprop(∀ x, Φ x) iprop(∀ x, Ψ x) where
@@ -918,3 +941,34 @@ instance combineSepGives_persistently [BI PROP] (Q1 Q2 P : PROP)
     [h : CombineSepGives Q1 Q2 P] :
     CombineSepGives iprop(<pers> Q1) iprop(<pers> Q2) iprop(<pers> P) where
   combine_sep_gives := persistently_sep_mpr.trans (persistently_mono h.combine_sep_gives)
+
+@[rocq_alias elim_inv_acc_without_close]
+instance elimInv_acc_without_close [BI PROP] {X : Type}
+    ϕ1 ϕ2 Pinv Pin (M1 M2 : PROP → PROP) α β mγ Q (Q' : X → PROP)
+    [h1 : IntoAcc Pinv ϕ1 Pin M1 M2 α β mγ]
+    [h2 : ElimAcc ϕ2 M1 M2 α β mγ Q Q'] :
+    ElimInv (ϕ1 ∧ ϕ2) X Pinv Pin α false none Q Q' where
+  elim_inv := by
+    intro ⟨hϕ1, _⟩
+    iintro ⟨Hinv, Hin, Hcont⟩
+    iapply h2.elim_acc $$ [Hcont]
+    · assumption
+    · iassumption
+    · iapply h1.into_acc hϕ1 $$ Hinv Hin
+
+@[rocq_alias elim_inv_acc_with_close]
+instance elimInv_acc_with_close [BI PROP] {X : Type}
+    ϕ1 ϕ2 Pinv Pin (M1 M2 : PROP → PROP) α β mγ Q (Q' : PROP)
+    [h1 : IntoAcc Pinv ϕ1 Pin M1 M2 α β mγ]
+    [h2 : ∀ R, ElimModal ϕ2 false false (M1 R) R Q Q'] :
+    ElimInv (ϕ1 ∧ ϕ2) X Pinv Pin α true
+            (some (fun x => iprop(β x -∗ M2 (mγ x |>.getD emp))))
+            Q (fun _ => Q') where
+  elim_inv := by
+    intro ⟨hϕ1, _⟩
+    have hAcc := h1.into_acc
+    unfold accessor at hAcc
+    iintro ⟨Hinv, Hin, Hcont⟩
+    imod hAcc hϕ1 $$ Hinv Hin with ⟨%_, Hα, Hclose⟩
+    iapply Hcont
+    isplitl [Hα] <;> iassumption