fix: avoid recursion in invariant side conditions

Iris/Iris/HeapLang/Lib/LandinsKnot.lean

@@ -51,14 +51,11 @@ theorem wp_landinsKnot (P : Val → IProp GF) (Q : Val → Val → IProp GF) (F
   iloeb as IH generalizing %v1 %Φ
   wp_rec
   wp_bind !_
-  iapply wp_atomic
-  imod inv_acc $$ Hinv with ⟨Hr, Hcl⟩
-  simp only [CoPset.subseteq_top]
-  imodintro
+  iinv Hinv with >Hr
+  · simp; infer_instance -- TODO: iinv should solve this
   wp_load
-  imod Hcl $$ Hr
-  iapply H $$ [HP] [$]
-  iframe HP
+  imodintro; iframe
+  iapply H $$ [$HP] [$]
   iintro %v3 !> %Φ HP HQ
   iapply IH $$ HP HQ
 

Iris/Iris/HeapLang/Lib/NondetBool.lean

@@ -26,7 +26,7 @@ theorem nondetBool.spec :
   unfold nondetBool
   wp_alloc l with Hl
   wp_pures
-  imod inv_alloc `n ⊤ iprop(∃ (b : Bool), l ↦ hl_val(#b)) $$ [$Hl] with #Hinv
+  imod inv_alloc `rnd ⊤ iprop(∃ (b : Bool), l ↦ hl_val(#b)) $$ [$Hl] with #Hinv
   wp_bind fork(_)
   iapply wp_fork $$ [K] []
   · inext

Iris/Iris/HeapLang/Lib/Spawn.lean

@@ -109,15 +109,12 @@ theorem spawn_spec (Ψ : Val → IProp GF) (f : Val) :
   iapply wp_wand $$ Hf
   iintro %v HΨ
   wp_pures
-  iapply wp_atomic
-  imod inv_acc (fun _ _ => CoPset.mem_full) $$ Hinv with ⟨Hpt, Hclose⟩
+  iinv Hinv with Hpt
+  · simp; infer_instance -- TODO: iinv should solve this
   unfold spawnInv
   icases Hpt with ⟨%_, Hl, _⟩
-  imodintro
   wp_store
-  iapply Hclose
-  inext
-  iexists _; iframe Hl
+  imodintro; iframe Hl; imodintro
   iright; iexists v; isplit
   · itrivial
   · iframe
@@ -134,33 +131,21 @@ theorem join_spec (Ψ : Val → IProp GF) (l : Loc) :
   iloeb as IH
   wp_rec
   wp_bind !_
-  iapply wp_atomic
-  imod inv_acc (fun _ _ => CoPset.mem_full) $$ Hinv with ⟨Hpt, Hclose⟩
+  iinv Hinv with Hpt
+  · simp; infer_instance -- TODO: iinv should solve this
   unfold spawnInv
   icases Hpt with ⟨%lv, Hl, Hcond⟩
-  imodintro
-  wp_load
+  wp_load; imodintro; iframe Hl
   icases Hcond with (%Heq | ⟨%w, %Heq, (HΨw | Hγ')⟩) <;> subst Heq
-  · imod Hclose $$ [Hl]
-    · inext
-      iexists _
-      iframe Hl
-      ileft; itrivial
-    imodintro
+  · isplitr
+    · ileft; itrivial
     wp_pures
     iapply IH $$ HΦ Hγ
-  · imod Hclose $$ [Hl Hγ]
-    · inext
-      iexists _; iframe Hl
-      iright; iexists w; isplit
-      · itrivial
-      · iframe
-    imodintro
+  · isplitl [Hγ]
+    · iright; iframe Hγ; itrivial
     wp_pures
     iapply HΦ $$ HΨw
-  · iexfalso
-    iapply token_exclusive
-    iframe
+  · icombine Hγ Hγ' gives %⟨⟩
 
 end Specs
 

Iris/Iris/HeapLang/Lib/SpinLock.lean

@@ -130,37 +130,29 @@ theorem try_acquire_spec (γ : GName) (lk : Val) (R : IProp GF) :
   icases Hlock with ⟨%l, %Heq, #Hinv⟩
   subst Heq
   wp_bind cmpXchg(_,_,_)
-  iapply wp_atomic
-  imod inv_acc $$ Hinv with ⟨G1, G2⟩
-  · simp
+  iinv Hinv with G1
+  · simp; infer_instance -- TODO: iinv should solve this
   unfold lockInv
-  imodintro
   icases G1 with ⟨%b, Hpt, Hcond⟩
   cases b
   · simp only [Bool.false_eq_true, ↓reduceIte]
     wp_cmpxchg_suc
-    imod G2 $$ [Hpt]
-    · iexists true
-      simp only [↓reduceIte]
-      iframe
-    · imodintro
-      wp_pure
-      imodintro
-      iapply Hcont $$ [Hcond]
-      simp only [↓reduceIte]
-      iframe
+    imodintro
+    isplitl [Hpt]
+    · iframe; simp; itrivial
+    wp_pures
+    imodintro
+    iapply Hcont $$ [Hcond]
+    simp only [↓reduceIte]; iframe
   · simp only [↓reduceIte]
     wp_cmpxchg_fail
-    imod G2 $$ [Hpt]
-    · iexists true
-      simp only [↓reduceIte]
-      iframe
-    · imodintro
-      wp_pure
-      imodintro
-      iapply Hcont
-      simp only [Bool.false_eq_true, ↓reduceIte]
-      itrivial
+    imodintro
+    isplitl [Hpt]
+    · iframe; simp; itrivial
+    wp_pures
+    imodintro
+    iapply Hcont $$ [Hcond]
+    simp only [Bool.false_eq_true, ↓reduceIte]; itrivial
 
 @[rocq_alias heap_lang.spin_lock.acquire_spec]
 theorem acquire_spec (γ : GName) (lk : Val) (R : IProp GF) :
@@ -195,21 +187,14 @@ theorem release_spec (γ : GName) (lk : Val) (R : IProp GF) :
   unfold isLock
   icases Hlock with ⟨%l, %Heq, #Hinv⟩
   subst Heq
-  iapply wp_atomic
-  imod inv_acc $$ Hinv with ⟨G1, G2⟩
-  · simp
+  iinv Hinv with G1
+  · simp; infer_instance -- TODO: iinv should solve this
   unfold lockInv
-  imodintro
   icases G1 with ⟨%b, Hpt, Hcond⟩
   wp_store
-  imod G2 $$ [- Hcont]
-  · inext
-    iexists false
-    simp only [Bool.false_eq_true, ↓reduceIte]
-    iframe
-  · imodintro
-    iapply Hcont
-    itrivial
+  imodintro; iframe Hpt
+  simp only [Bool.false_eq_true, ↓reduceIte]; iframe
+  iapply Hcont; itrivial
 
 end Specs
 

Iris/Iris/Std/CoPset.lean

@@ -492,20 +492,23 @@ theorem coPsetSuffixes_wf p : coPsetWf (CoPsetRaw.suffixesRaw p) := by
   induction p <;> simp [CoPsetRaw.suffixesRaw, coPsetWf] <;>
   apply node'_wf <;> simp_all [coPsetWf]
 
+-- `suffixes` is irreducible since computing `CoPsetRaw.suffixesRaw easily
+-- hits the recursion limit, see https://github.com/leanprover-community/iris-lean/issues/557
+@[irreducible]
 def suffixes (p : Pos) : CoPset :=
   ⟨CoPsetRaw.suffixesRaw p, coPsetSuffixes_wf p⟩
 
 theorem elem_suffixes {p q} : p ∈ suffixes q <-> ∃ q', p = q' ++ q := by
   constructor
   · induction q generalizing p with
     | xI q IH =>
-      simp only [suffixes, CoPsetRaw.suffixesRaw, Membership.mem, elem_of_node]
+      simp only [suffixes, CoPsetRaw.suffixesRaw, Membership.mem, elem_of_node] at IH |-
       intros Hin
       cases p <;> simp [CoPsetRaw.ElemOf] at Hin
       obtain ⟨q', rfl⟩ := IH Hin
       exact ⟨q', rfl⟩
     | xO q IH =>
-      simp only [suffixes, CoPsetRaw.suffixesRaw, Membership.mem, elem_of_node]
+      simp only [suffixes, CoPsetRaw.suffixesRaw, Membership.mem, elem_of_node] at IH |-
       intros Hin
       cases p <;> simp [CoPsetRaw.ElemOf] at Hin
       obtain ⟨q', rfl⟩ := IH Hin

Iris/Iris/Std/Namespaces.lean

@@ -42,7 +42,11 @@ infix:80 ".@" => ndot
 instance ndisjoint : Iris.Std.Disjoint Namespace where
   disjoint N1 N2 := nclose N1 ## nclose N2
 
-theorem nclose_root : ↑nroot = CoPset.full := by rfl
+theorem nclose_root : ↑nroot = CoPset.full := by
+  ext p
+  simp only [nclose, Pos.flatten, nroot, Pos.flattenGo, CoPset.elem_suffixes,
+    CoPset.mem_full, iff_true, HAppend.hAppend, Pos.app]
+  exists p
 
 theorem nclose_subseteq [Pos.Countable A] N (x : A) : (↑N.@x : CoPset) ⊆ (↑N : CoPset) := by
   intros p

Iris/Iris/Tests/Tactics.lean

@@ -3698,6 +3698,18 @@ example {P : IProp GF} : inv N iprop(<pers> P) ={⊤}=∗ ▷ P := by
     inext
     iexact H
 
+/-- Tests `iinv` with a concrete namespace whose closure is expensive to unfold.
+Regression test for https://github.com/leanprover-community/iris-lean/issues/557 -/
+example {P : IProp GF} : inv `long_name iprop(<pers> P) ={⊤}=∗ ▷ P := by
+  iintro #Hinv
+  iinv Hinv with #H
+  imodintro
+  isplit
+  · iexact H
+  · imodintro
+    inext
+    iexact H
+
 /--
   Tests `iinv` with `elimInv_acc_with_close`, `elimModal_fupd_fupd` and
   `intoAcc_inv` where the side condition is trivial.