feat: port HeapLang heap tactics

Iris/Iris/HeapLang/Lib/LandinsKnot.lean

@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2026. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alex Bai, Klaus Kraßnitzer
+-/
 module
 
 public import Iris.Instances.Lib.Invariants
@@ -37,17 +42,9 @@ theorem wp_landinsKnot (P : Val → IProp GF) (Q : Val → Val → IProp GF) (F
   iintro !> %Φ ⟨#H, HP⟩ HQ
   wp_bind &landinsKnot _
   wp_rec
-  wp_bind ref(_)
-  wp_pures
-  iapply wp_alloc
-  iintro !> %r Hr
-  wp_pures
-  wp_bind (_ ← _)
-  iapply wp_store $$ Hr
-  iintro !> Hr
-  wp_pures
-  iapply wp_load $$ Hr
-  iintro !> Hr
+  wp_alloc r as Hr
+  wp_store
+  wp_load
   imod inv_alloc landinN ⊤ _ $$ Hr with #Hinv
   ihave HQ : ▷ (∀ u, Q u v1 -∗ Φ u) $$ [HQ]
   · inext; iexact HQ
@@ -58,8 +55,7 @@ theorem wp_landinsKnot (P : Val → IProp GF) (Q : Val → Val → IProp GF) (F
   imod inv_acc $$ Hinv with ⟨Hr, Hcl⟩
   simp only [CoPset.subseteq_top]
   imodintro
-  iapply wp_load $$ Hr
-  iintro !> Hr
+  wp_load
   imod Hcl $$ Hr
   iapply H $$ [HP] [$]
   iframe HP

Iris/Iris/HeapLang/Lib/Quicksort.lean

@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2026. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus de Medeiros, Michael Sammler, Klaus Kraßnitzer
+-/
 module
 
 public import Iris.HeapLang.PrimitiveLaws
@@ -115,9 +120,7 @@ theorem cons_spec x l ls Φ :
     WP hl(&cons #x &l) {{ Φ }} := by
   iintro Hl HΦ
   wp_rec; wp_pures
-  wp_bind ref(_)
-  iapply wp_alloc
-  iintro !> %l Hl
+  wp_alloc l
   wp_pures
   imodintro
   iapply HΦ
@@ -142,9 +145,7 @@ theorem append_spec l1 ls1 l2 ls2 Φ :
   | cons x xs =>
     icases isList_cons $$ Hl1 with ⟨%l, %tl, %heq, Hpt, Hl⟩
     subst heq; wp_pures
-    wp_bind !_
-    iapply wp_load $$ Hpt
-    iintro !> Hpt
+    wp_load
     wp_pures
     wp_bind &append _ _
     iapply IH $$ Hl Hl2
@@ -177,9 +178,7 @@ theorem partition_spec x l ls Φ :
     dsimp only
     icases Hl with ⟨%_, %tl, %hl, Hpt, Hl⟩; subst hl
     wp_pures
-    wp_bind !_
-    iapply wp_load $$ [$]
-    iintro !> Hpt
+    wp_load
     wp_pures
     wp_bind &partition _ _
     iapply IH $$ Hl
@@ -231,9 +230,7 @@ theorem quicksort_spec l ls Φ :
     dsimp only
     icases Hl with ⟨%l, %tl, %heq, Hpt, Hl⟩; subst heq
     wp_pures
-    wp_bind !_
-    iapply wp_load $$ [$]
-    iintro !> Hpt
+    wp_load
     wp_pures
     wp_bind &partition _ _
     iapply partition_spec $$ [$]
@@ -318,9 +315,7 @@ theorem wp_checkSorted (v vacc : Val) (l : List Int) (Φ : Val → IProp GF) :
     icases isList_cons $$ H with ⟨%loc, %tlv, %heq, Hpt, Htl⟩
     subst heq
     wp_pures
-    wp_bind !_
-    iapply wp_load $$ Hpt
-    iintro !> Hpt
+    wp_load
     rcases hinv with rfl | ⟨va, rfl, hva⟩
     · wp_pures
       iapply IH $$ %_ %tl %_ %((List.pairwise_cons.mp hsorted).2)

Iris/Iris/HeapLang/Lib/Spawn.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2026. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Zongyuan Liu
+Authors: Zongyuan Liu, Klaus Kraßnitzer
 -/
 module
 
@@ -73,10 +73,7 @@ theorem spawn_spec (Ψ : Val → IProp GF) (f : Val) :
       WP hl(&spawn &f) {{ Φ }} := by
   iintro !> %Φ Hf HΦ
   wp_rec
-  wp_bind ref(_)
-  wp_pures
-  iapply wp_alloc
-  iintro !> %l Hl
+  wp_alloc l as Hl
   imod token_alloc with ⟨%γ, Hγ⟩
   iapply fupd_wp
   imod inv_alloc N ⊤ (spawnInv γ l Ψ) $$ [Hl] with #Hinv
@@ -106,11 +103,10 @@ theorem spawn_spec (Ψ : Val → IProp GF) (f : Val) :
   unfold spawnInv
   icases Hpt with ⟨%_, Hl, _⟩
   imodintro
-  iapply wp_store $$ Hl
-  iintro !> Hpt
+  wp_store
   iapply Hclose
   inext
-  iexists _; iframe Hpt
+  iexists _; iframe Hl
   iright; iexists v; isplit
   · itrivial
   · iframe
@@ -131,8 +127,7 @@ theorem join_spec (Ψ : Val → IProp GF) (l : Loc) :
   unfold spawnInv
   icases Hpt with ⟨%lv, Hl, Hcond⟩
   imodintro
-  iapply wp_load $$ Hl
-  iintro !> Hl
+  wp_load
   icases Hcond with (%Heq | ⟨%w, %Heq, (HΨw | Hγ')⟩) <;> subst Heq
   · imod Hclose $$ [Hl]
     · inext

Iris/Iris/HeapLang/Lib/SpinLock.lean

@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2026. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Sammler, ayhon, Klaus Kraßnitzer
+-/
 module
 
 public import Iris.HeapLang.Lib.Lock
@@ -85,8 +90,8 @@ theorem newlock_spec :
   iintro !> %Φ Hcont
   wp_rec
   imod token_alloc with ⟨%γ, Hγ⟩
-  iapply wp_alloc
-  iintro !> %l Hpt
+  wp_alloc l as Hpt
+  imodintro
   iapply Hcont
   iintro %R %E HR
   imod inv_alloc spinlockN E (lockInv γ l R) $$ [Hpt HR Hγ] with H
@@ -118,11 +123,7 @@ theorem try_acquire_spec (γ : GName) (lk : Val) (R : IProp GF) :
   icases G1 with ⟨%b, Hpt, Hcond⟩
   cases b
   · simp only [Bool.false_eq_true, ↓reduceIte]
-    iapply wp_wand $$ [Hpt]
-    · iapply wp_cmpXchg_true rfl rfl $$ Hpt <;>
-        simp [Val.compareSafe, Val.isUnboxed, BaseLit.isUnboxed]
-    iintro %v ⟨%Heq, Hpt⟩
-    subst Heq
+    wp_cmpxchg_suc
     imod G2 $$ [Hpt]
     · iexists true
       simp only [↓reduceIte]
@@ -134,11 +135,7 @@ theorem try_acquire_spec (γ : GName) (lk : Val) (R : IProp GF) :
       simp only [↓reduceIte]
       iframe
   · simp only [↓reduceIte]
-    iapply wp_wand $$ [Hpt]
-    · iapply wp_cmpXchg_fail rfl rfl $$ Hpt <;>
-        simp [Val.compareSafe, Val.isUnboxed, BaseLit.isUnboxed]
-    iintro %v ⟨%Heq, Hpt⟩
-    subst Heq
+    wp_cmpxchg_fail
     imod G2 $$ [Hpt]
     · iexists true
       simp only [↓reduceIte]
@@ -187,8 +184,7 @@ theorem release_spec (γ : GName) (lk : Val) (R : IProp GF) :
   unfold lockInv
   imodintro
   icases G1 with ⟨%b, Hpt, Hcond⟩
-  iapply wp_store $$ Hpt
-  iintro !> Hpt
+  wp_store
   imod G2 $$ [- Hcont]
   · inext
     iexists false