From 496c6a224990e249aea26ac45378feb088fd236f Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Thu, 16 Jul 2026 13:41:42 +0200
Subject: [PATCH 01/13] Start porting `BI/Lib/Core.lean`

---
 Iris/Iris/BI/Lib/Core.lean | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)
 create mode 100644 Iris/Iris/BI/Lib/Core.lean

diff --git a/Iris/Iris/BI/Lib/Core.lean b/Iris/Iris/BI/Lib/Core.lean
new file mode 100644
index 000000000..ba6c70b3d
--- /dev/null
+++ b/Iris/Iris/BI/Lib/Core.lean
@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2026 Alvin Tang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alvin Tang
+-/
+
+module
+
+public import Iris.BI
+public import Iris.ProofMode
+
+@[expose] public section
+
+namespace Iris
+
+@[rocq_alias coreP]
+def coreP [Sbi PROP] (P : PROP) : PROP :=
+  iprop(∀ Q, <affine> ■ (Q -∗ <pers> Q) -∗ <affine> ■ (P -∗ Q) -∗ Q)
+
+section Core
+
+variable [Sbi PROP] {P Q : PROP}
+
+@[rocq_alias coreP_intro]
+theorem coreP_intro : P -∗ coreP P := by
+  unfold coreP
+  iintro HP %Q HQ HPQ
+  iapply BI.affinely_plainly_elim $$ HPQ HP
+
+end Core

From d79d250e81347d51f02417d2343ea5c4adacf96f Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Thu, 16 Jul 2026 14:59:03 +0200
Subject: [PATCH 02/13] Towards implementing `Core.lean`

---
 Iris/Iris/BI/Lib/Core.lean | 92 +++++++++++++++++++++++++++++++++++---
 1 file changed, 87 insertions(+), 5 deletions(-)

diff --git a/Iris/Iris/BI/Lib/Core.lean b/Iris/Iris/BI/Lib/Core.lean
index ba6c70b3d..04ee5deb6 100644
--- a/Iris/Iris/BI/Lib/Core.lean
+++ b/Iris/Iris/BI/Lib/Core.lean
@@ -13,18 +13,100 @@ public import Iris.ProofMode
 
 namespace Iris
 
+section Core
+open BI OFE
+
 @[rocq_alias coreP]
 def coreP [Sbi PROP] (P : PROP) : PROP :=
   iprop(∀ Q, <affine> ■ (Q -∗ <pers> Q) -∗ <affine> ■ (P -∗ Q) -∗ Q)
 
-section Core
-
-variable [Sbi PROP] {P Q : PROP}
+variable [Sbi PROP]
 
 @[rocq_alias coreP_intro]
-theorem coreP_intro : P -∗ coreP P := by
+theorem coreP_intro {P : PROP} : P -∗ coreP P := by
   unfold coreP
   iintro HP %Q HQ HPQ
-  iapply BI.affinely_plainly_elim $$ HPQ HP
+  iapply affinely_plainly_elim $$ HPQ HP
+
+@[rocq_alias coreP_persistent]
+instance coreP_persistent [BIPersistentlyForall PROP] (P : PROP) : Persistent (coreP P) where
+  persistent := by
+    unfold coreP
+    iintro HC %Q
+    iapply persistently_wand_affinely_plainly
+    iintro #HQ
+    iapply persistently_wand_affinely_plainly
+    iintro #HPQ
+    ispecialize HC $$ %Q HQ
+    iapply HQ
+    iapply HC
+    iapply HPQ
+
+@[rocq_alias coreP_affine]
+instance coreP_affine (P : PROP) [Affine P] : Affine (coreP P) where
+  affine := by
+    unfold coreP
+    iintro HC
+    iapply HC <;> iintro !> !> _ //
+
+@[rocq_alias coreP_ne]
+instance coreP_ne : NonExpansive (coreP (PROP := PROP)) where
+  ne n P Q H := by
+    sorry
+
+@[rocq_alias coreP_wand]
+theorem coreP_wand (P Q : PROP) : <affine> ■ (P -∗ Q) -∗ coreP P -∗ coreP Q := by
+  unfold coreP
+  iintro #HPQ HP %R #HR #HQR
+  iapply HP $$ HR
+  iintro !> !> HP
+  iapply HQR
+  iapply HPQ $$ HP
+
+@[rocq_alias coreP_elim]
+theorem coreP_elim (P : PROP) [inst : Persistent P] : coreP P -∗ P := by
+  unfold coreP
+  iintro HCP
+  iapply HCP
+  · iintro !> !> #HP //
+  · iintro !> !> HP //
+
+@[rocq_alias coreP_entails]
+theorem coreP_entails [inst : BIPersistentlyForall PROP] {P Q : PROP} :
+    (<affine> coreP P ⊢ Q) ↔ (P ⊢ <pers> Q) := by
+  constructor <;> intro h
+  · iintro HP
+    ihave HP := coreP_intro $$ HP
+    unfold coreP
+    iapply HP
+    · iintro !> !> #HQ //
+    · iintro !> !> HP
+      ihave #H := h
+      imodintro
+      iapply H
+      unfold coreP
+      iintro !> %A HH AA
+      sorry
+  · iintro HP
+    have b := inst.persistently_sForall_2
+    have a : Persistent P := sorry
+    ihave #HP := coreP_elim $$ HP
+    iapply h $$ HP
+
+@[rocq_alias coreP_entails']
+theorem coreP_entails' [BIPersistentlyForall PROP] {P Q : PROP} [inst : Affine P] :
+    (coreP P ⊢ Q) ↔ (P ⊢ □ Q) := by
+  constructor <;> intro h
+  · iintro HP
+    ihave a := inst.affine $$ HP
+    unfold coreP at h
+    ihave H := h
+    sorry
+  · unfold coreP
+    iintro HP
+    iapply HP
+    · iintro !> !>
+      sorry
+    · sorry
 
 end Core

From cc96a62ea5ccebd985b938214425f34942cd2e00 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Thu, 16 Jul 2026 15:52:30 +0200
Subject: [PATCH 03/13] Ignore theorems related to the `Proper` type class

---
 Iris/Iris/BI/Lib/Core.lean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/Iris/Iris/BI/Lib/Core.lean b/Iris/Iris/BI/Lib/Core.lean
index 04ee5deb6..1b12e1031 100644
--- a/Iris/Iris/BI/Lib/Core.lean
+++ b/Iris/Iris/BI/Lib/Core.lean
@@ -52,6 +52,9 @@ instance coreP_affine (P : PROP) [Affine P] : Affine (coreP P) where
 @[rocq_alias coreP_ne]
 instance coreP_ne : NonExpansive (coreP (PROP := PROP)) where
   ne n P Q H := by
+    unfold coreP
+    refine forall_ne ?_
+    intro R
     sorry
 
 @[rocq_alias coreP_wand]
@@ -109,4 +112,8 @@ theorem coreP_entails' [BIPersistentlyForall PROP] {P Q : PROP} [inst : Affine P
       sorry
     · sorry
 
+#rocq_ignore coreP_proper "No Proper type class in Lean"
+#rocq_ignore coreP_mono "No Proper type class in Lean"
+#rocq_ignore coreP_flip_mono "No Proper type class in Lean"
+
 end Core

From 31eb240b0ff55d0c6ec7155e0e7a94832504cdb9 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Thu, 16 Jul 2026 15:57:49 +0200
Subject: [PATCH 04/13] Some progress with `coreP_ne`

---
 Iris/Iris/BI/Lib/Core.lean | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/Iris/Iris/BI/Lib/Core.lean b/Iris/Iris/BI/Lib/Core.lean
index 1b12e1031..217f413d2 100644
--- a/Iris/Iris/BI/Lib/Core.lean
+++ b/Iris/Iris/BI/Lib/Core.lean
@@ -55,7 +55,11 @@ instance coreP_ne : NonExpansive (coreP (PROP := PROP)) where
     unfold coreP
     refine forall_ne ?_
     intro R
-    sorry
+    apply wand_ne.ne
+    · rfl
+    · apply wand_ne.ne
+      · sorry
+      · rfl
 
 @[rocq_alias coreP_wand]
 theorem coreP_wand (P Q : PROP) : <affine> ■ (P -∗ Q) -∗ coreP P -∗ coreP Q := by

From d4d92c071848c95537e74aab9b30809e3096c388 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Thu, 16 Jul 2026 16:18:25 +0200
Subject: [PATCH 05/13] Finish proving `coreP_ne`

---
 Iris/Iris/BI/Lib/Core.lean | 30 +++++++++++++++---------------
 1 file changed, 15 insertions(+), 15 deletions(-)

diff --git a/Iris/Iris/BI/Lib/Core.lean b/Iris/Iris/BI/Lib/Core.lean
index 217f413d2..226e7f3ae 100644
--- a/Iris/Iris/BI/Lib/Core.lean
+++ b/Iris/Iris/BI/Lib/Core.lean
@@ -58,7 +58,11 @@ instance coreP_ne : NonExpansive (coreP (PROP := PROP)) where
     apply wand_ne.ne
     · rfl
     · apply wand_ne.ne
-      · sorry
+      · apply affinely_ne.ne
+        apply instPlainly_ne.ne
+        apply wand_ne.ne
+        assumption
+        rfl
       · rfl
 
 @[rocq_alias coreP_wand]
@@ -83,22 +87,18 @@ theorem coreP_entails [inst : BIPersistentlyForall PROP] {P Q : PROP} :
     (<affine> coreP P ⊢ Q) ↔ (P ⊢ <pers> Q) := by
   constructor <;> intro h
   · iintro HP
-    ihave HP := coreP_intro $$ HP
+    ihave #HP := coreP_intro $$ HP
     unfold coreP
+    imodintro
     iapply HP
-    · iintro !> !> #HQ //
-    · iintro !> !> HP
-      ihave #H := h
-      imodintro
-      iapply H
-      unfold coreP
-      iintro !> %A HH AA
-      sorry
-  · iintro HP
-    have b := inst.persistently_sForall_2
-    have a : Persistent P := sorry
-    ihave #HP := coreP_elim $$ HP
-    iapply h $$ HP
+    · sorry
+    · sorry
+  · iintro #HP
+    ihave H := h
+    unfold coreP
+    iapply HP
+    · sorry
+    · sorry
 
 @[rocq_alias coreP_entails']
 theorem coreP_entails' [BIPersistentlyForall PROP] {P Q : PROP} [inst : Affine P] :

From 91cc2a83d8069405a663a2319662674356e1e7dd Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Thu, 16 Jul 2026 17:14:23 +0200
Subject: [PATCH 06/13] Finish proof for `coreP_entails`

---
 Iris/Iris/BI/Lib/Core.lean | 35 +++++++++++++++++++++++------------
 1 file changed, 23 insertions(+), 12 deletions(-)

diff --git a/Iris/Iris/BI/Lib/Core.lean b/Iris/Iris/BI/Lib/Core.lean
index 226e7f3ae..f3ec759dc 100644
--- a/Iris/Iris/BI/Lib/Core.lean
+++ b/Iris/Iris/BI/Lib/Core.lean
@@ -83,27 +83,38 @@ theorem coreP_elim (P : PROP) [inst : Persistent P] : coreP P -∗ P := by
   · iintro !> !> HP //
 
 @[rocq_alias coreP_entails]
-theorem coreP_entails [inst : BIPersistentlyForall PROP] {P Q : PROP} :
+theorem coreP_entails [inst : BIPersistentlyForall PROP] (P Q : PROP) :
     (<affine> coreP P ⊢ Q) ↔ (P ⊢ <pers> Q) := by
   constructor <;> intro h
   · iintro HP
-    ihave #HP := coreP_intro $$ HP
-    unfold coreP
+    ihave #HPQ := coreP_intro $$ HP
     imodintro
-    iapply HP
-    · sorry
-    · sorry
-  · iintro #HP
-    ihave H := h
-    unfold coreP
-    iapply HP
-    · sorry
-    · sorry
+    iapply h
+    iassumption
+  · have a : <affine> coreP P ⊢ <affine> coreP iprop(<pers> Q) := by
+      iintro #HP
+      imodintro
+      unfold coreP
+      iintro %R H1 H2
+      ispecialize HP $$ %R H1
+      iapply HP
+      iintuitionistic H2
+      imodintro
+      iapply plainly_mono
+      · apply wand_mono
+        apply h
+        apply BIBase.Entails.rfl
+      · iexact H2
+    iapply a.trans
+    iintro #HcQ
+    iapply coreP_elim $$ HcQ
 
 @[rocq_alias coreP_entails']
 theorem coreP_entails' [BIPersistentlyForall PROP] {P Q : PROP} [inst : Affine P] :
     (coreP P ⊢ Q) ↔ (P ⊢ □ Q) := by
   constructor <;> intro h
+  ihave H := affine_affinely (coreP P)
+  have HH := coreP_entails P (coreP P)
   · iintro HP
     ihave a := inst.affine $$ HP
     unfold coreP at h

From 73f4488942760e980907c3dd192b4454f0f44cd5 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Thu, 16 Jul 2026 17:27:31 +0200
Subject: [PATCH 07/13] Towards proving `coreP_entails'`

---
 Iris/Iris/BI/Lib/Core.lean | 37 +++++++++++++++++++++++--------------
 1 file changed, 23 insertions(+), 14 deletions(-)

diff --git a/Iris/Iris/BI/Lib/Core.lean b/Iris/Iris/BI/Lib/Core.lean
index f3ec759dc..b2ca9d0f0 100644
--- a/Iris/Iris/BI/Lib/Core.lean
+++ b/Iris/Iris/BI/Lib/Core.lean
@@ -109,23 +109,32 @@ theorem coreP_entails [inst : BIPersistentlyForall PROP] (P Q : PROP) :
     iintro #HcQ
     iapply coreP_elim $$ HcQ
 
+theorem coreP_entails'_aux {P Q : PROP} [Affine P] :
+    (P ⊢ <pers> Q) ↔ (P ⊢ □ Q) := by
+  constructor
+  · have a := affine_affinely (PROP := PROP) P
+    intro h
+    iintro H
+    have a := a.mpr
+    ihave H := a $$ H
+    iintuitionistic h
+    ihave a := affinely_mono h
+    ispecialize a $$ H
+    iexact a
+  · intro h
+    iintro HP
+    ihave #HQ := h $$ HP
+    iexact HQ
+
 @[rocq_alias coreP_entails']
 theorem coreP_entails' [BIPersistentlyForall PROP] {P Q : PROP} [inst : Affine P] :
     (coreP P ⊢ Q) ↔ (P ⊢ □ Q) := by
-  constructor <;> intro h
-  ihave H := affine_affinely (coreP P)
-  have HH := coreP_entails P (coreP P)
-  · iintro HP
-    ihave a := inst.affine $$ HP
-    unfold coreP at h
-    ihave H := h
-    sorry
-  · unfold coreP
-    iintro HP
-    iapply HP
-    · iintro !> !>
-      sorry
-    · sorry
+  have h1 := affine_affinely (coreP P)
+  have h2 := coreP_entails P Q
+
+
+
+  sorry
 
 #rocq_ignore coreP_proper "No Proper type class in Lean"
 #rocq_ignore coreP_mono "No Proper type class in Lean"

From b4bd11d8b813a7105ecab794f97ab14565917667 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Thu, 16 Jul 2026 17:51:03 +0200
Subject: [PATCH 08/13] Finish proof for `coreP_entails'`

---
 Iris/Iris/BI/Lib/Core.lean | 17 +++++++++++++----
 1 file changed, 13 insertions(+), 4 deletions(-)

diff --git a/Iris/Iris/BI/Lib/Core.lean b/Iris/Iris/BI/Lib/Core.lean
index b2ca9d0f0..2df986d59 100644
--- a/Iris/Iris/BI/Lib/Core.lean
+++ b/Iris/Iris/BI/Lib/Core.lean
@@ -131,10 +131,19 @@ theorem coreP_entails' [BIPersistentlyForall PROP] {P Q : PROP} [inst : Affine P
     (coreP P ⊢ Q) ↔ (P ⊢ □ Q) := by
   have h1 := affine_affinely (coreP P)
   have h2 := coreP_entails P Q
-
-
-
-  sorry
+  constructor
+  · intro h
+    apply coreP_entails'_aux.mp
+    apply h2.mp
+    iintro HP
+    ihave a := h $$ HP
+    iexact a
+  · intro h
+    have hh := affinely_intro .rfl (P := coreP P)
+    have hhh := h.trans affinely_elim
+    have hhhh : <affine> coreP P ⊢ Q := h2.mpr hhh
+    apply h1.mpr.trans
+    apply hhhh
 
 #rocq_ignore coreP_proper "No Proper type class in Lean"
 #rocq_ignore coreP_mono "No Proper type class in Lean"

From 62df05a8b95a0a5ef4328fc65724b0d4bac1b957 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Thu, 16 Jul 2026 18:03:52 +0200
Subject: [PATCH 09/13] Proof simplifications

---
 Iris/Iris/BI/Lib/Core.lean | 45 +++++++++++---------------------------
 1 file changed, 13 insertions(+), 32 deletions(-)

diff --git a/Iris/Iris/BI/Lib/Core.lean b/Iris/Iris/BI/Lib/Core.lean
index 2df986d59..0e8b31f95 100644
--- a/Iris/Iris/BI/Lib/Core.lean
+++ b/Iris/Iris/BI/Lib/Core.lean
@@ -37,9 +37,9 @@ instance coreP_persistent [BIPersistentlyForall PROP] (P : PROP) : Persistent (c
     iintro #HQ
     iapply persistently_wand_affinely_plainly
     iintro #HPQ
-    ispecialize HC $$ %Q HQ
     iapply HQ
     iapply HC
+    iapply HQ
     iapply HPQ
 
 @[rocq_alias coreP_affine]
@@ -53,17 +53,14 @@ instance coreP_affine (P : PROP) [Affine P] : Affine (coreP P) where
 instance coreP_ne : NonExpansive (coreP (PROP := PROP)) where
   ne n P Q H := by
     unfold coreP
-    refine forall_ne ?_
+    apply forall_ne
     intro R
+    apply wand_ne.ne; rfl
     apply wand_ne.ne
+    · apply affinely_ne.ne
+      apply instPlainly_ne.ne
+      apply wand_ne.ne H; rfl
     · rfl
-    · apply wand_ne.ne
-      · apply affinely_ne.ne
-        apply instPlainly_ne.ne
-        apply wand_ne.ne
-        assumption
-        rfl
-      · rfl
 
 @[rocq_alias coreP_wand]
 theorem coreP_wand (P Q : PROP) : <affine> ■ (P -∗ Q) -∗ coreP P -∗ coreP Q := by
@@ -110,21 +107,10 @@ theorem coreP_entails [inst : BIPersistentlyForall PROP] (P Q : PROP) :
     iapply coreP_elim $$ HcQ
 
 theorem coreP_entails'_aux {P Q : PROP} [Affine P] :
-    (P ⊢ <pers> Q) ↔ (P ⊢ □ Q) := by
-  constructor
-  · have a := affine_affinely (PROP := PROP) P
-    intro h
-    iintro H
-    have a := a.mpr
-    ihave H := a $$ H
-    iintuitionistic h
-    ihave a := affinely_mono h
-    ispecialize a $$ H
-    iexact a
-  · intro h
-    iintro HP
-    ihave #HQ := h $$ HP
-    iexact HQ
+    (P ⊢ <pers> Q) → (P ⊢ □ Q) := by
+  iintro %h H
+  ihave H := (affine_affinely P).mpr $$ H
+  iapply affinely_mono h $$ H
 
 @[rocq_alias coreP_entails']
 theorem coreP_entails' [BIPersistentlyForall PROP] {P Q : PROP} [inst : Affine P] :
@@ -133,17 +119,12 @@ theorem coreP_entails' [BIPersistentlyForall PROP] {P Q : PROP} [inst : Affine P
   have h2 := coreP_entails P Q
   constructor
   · intro h
-    apply coreP_entails'_aux.mp
+    apply coreP_entails'_aux
     apply h2.mp
     iintro HP
-    ihave a := h $$ HP
-    iexact a
+    iapply h $$ HP
   · intro h
-    have hh := affinely_intro .rfl (P := coreP P)
-    have hhh := h.trans affinely_elim
-    have hhhh : <affine> coreP P ⊢ Q := h2.mpr hhh
-    apply h1.mpr.trans
-    apply hhhh
+    apply h1.mpr.trans (h2.mpr (h.trans affinely_elim))
 
 #rocq_ignore coreP_proper "No Proper type class in Lean"
 #rocq_ignore coreP_mono "No Proper type class in Lean"

From 108451018105feb0a22dd7bf306b7c46e66920ba Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Thu, 16 Jul 2026 18:29:21 +0200
Subject: [PATCH 10/13] Proof cleanup

---
 Iris/Iris/BI/Lib/Core.lean | 49 ++++++++++++++++----------------------
 1 file changed, 21 insertions(+), 28 deletions(-)

diff --git a/Iris/Iris/BI/Lib/Core.lean b/Iris/Iris/BI/Lib/Core.lean
index 0e8b31f95..c32fb1b12 100644
--- a/Iris/Iris/BI/Lib/Core.lean
+++ b/Iris/Iris/BI/Lib/Core.lean
@@ -72,15 +72,27 @@ theorem coreP_wand (P Q : PROP) : <affine> ■ (P -∗ Q) -∗ coreP P -∗ core
   iapply HPQ $$ HP
 
 @[rocq_alias coreP_elim]
-theorem coreP_elim (P : PROP) [inst : Persistent P] : coreP P -∗ P := by
+theorem coreP_elim (P : PROP) [Persistent P] : coreP P -∗ P := by
   unfold coreP
   iintro HCP
   iapply HCP
   · iintro !> !> #HP //
   · iintro !> !> HP //
 
+theorem coreP_entails_aux [BIPersistentlyForall PROP] {P Q : PROP}
+    (h : P ⊢ <pers> Q):
+    <affine> coreP P ⊢ <affine> coreP iprop(<pers> Q) := by
+  iintro #HP !>
+  unfold coreP
+  iintro %R #HR #HQR
+  ispecialize HP $$ %R HR
+  iapply HP
+  imodintro
+  iapply plainly_mono <| wand_mono h .rfl
+  iassumption
+
 @[rocq_alias coreP_entails]
-theorem coreP_entails [inst : BIPersistentlyForall PROP] (P Q : PROP) :
+theorem coreP_entails [BIPersistentlyForall PROP] (P Q : PROP) :
     (<affine> coreP P ⊢ Q) ↔ (P ⊢ <pers> Q) := by
   constructor <;> intro h
   · iintro HP
@@ -88,21 +100,7 @@ theorem coreP_entails [inst : BIPersistentlyForall PROP] (P Q : PROP) :
     imodintro
     iapply h
     iassumption
-  · have a : <affine> coreP P ⊢ <affine> coreP iprop(<pers> Q) := by
-      iintro #HP
-      imodintro
-      unfold coreP
-      iintro %R H1 H2
-      ispecialize HP $$ %R H1
-      iapply HP
-      iintuitionistic H2
-      imodintro
-      iapply plainly_mono
-      · apply wand_mono
-        apply h
-        apply BIBase.Entails.rfl
-      · iexact H2
-    iapply a.trans
+  · iapply (coreP_entails_aux h).trans
     iintro #HcQ
     iapply coreP_elim $$ HcQ
 
@@ -113,18 +111,13 @@ theorem coreP_entails'_aux {P Q : PROP} [Affine P] :
   iapply affinely_mono h $$ H
 
 @[rocq_alias coreP_entails']
-theorem coreP_entails' [BIPersistentlyForall PROP] {P Q : PROP} [inst : Affine P] :
+theorem coreP_entails' [BIPersistentlyForall PROP] {P Q : PROP} [Affine P] :
     (coreP P ⊢ Q) ↔ (P ⊢ □ Q) := by
-  have h1 := affine_affinely (coreP P)
-  have h2 := coreP_entails P Q
-  constructor
-  · intro h
-    apply coreP_entails'_aux
-    apply h2.mp
-    iintro HP
-    iapply h $$ HP
-  · intro h
-    apply h1.mpr.trans (h2.mpr (h.trans affinely_elim))
+  constructor <;> intro h
+  · apply coreP_entails'_aux
+    apply coreP_entails P Q |>.mp
+    exact affinely_elim.trans h
+  · exact affine_affinely _ |>.mpr.trans (coreP_entails P Q |>.mpr (h.trans affinely_elim))
 
 #rocq_ignore coreP_proper "No Proper type class in Lean"
 #rocq_ignore coreP_mono "No Proper type class in Lean"

From 572fba070247e876758f427797ffb09064d2b76f Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Thu, 16 Jul 2026 18:56:45 +0200
Subject: [PATCH 11/13] Use `affinely_intro`

---
 Iris/Iris/BI/Lib/Core.lean | 12 +++---------
 1 file changed, 3 insertions(+), 9 deletions(-)

diff --git a/Iris/Iris/BI/Lib/Core.lean b/Iris/Iris/BI/Lib/Core.lean
index c32fb1b12..0dc6c706f 100644
--- a/Iris/Iris/BI/Lib/Core.lean
+++ b/Iris/Iris/BI/Lib/Core.lean
@@ -104,20 +104,14 @@ theorem coreP_entails [BIPersistentlyForall PROP] (P Q : PROP) :
     iintro #HcQ
     iapply coreP_elim $$ HcQ
 
-theorem coreP_entails'_aux {P Q : PROP} [Affine P] :
-    (P ⊢ <pers> Q) → (P ⊢ □ Q) := by
-  iintro %h H
-  ihave H := (affine_affinely P).mpr $$ H
-  iapply affinely_mono h $$ H
-
 @[rocq_alias coreP_entails']
 theorem coreP_entails' [BIPersistentlyForall PROP] {P Q : PROP} [Affine P] :
     (coreP P ⊢ Q) ↔ (P ⊢ □ Q) := by
   constructor <;> intro h
-  · apply coreP_entails'_aux
-    apply coreP_entails P Q |>.mp
+  · apply affinely_intro
+    apply (coreP_entails P Q).mp
     exact affinely_elim.trans h
-  · exact affine_affinely _ |>.mpr.trans (coreP_entails P Q |>.mpr (h.trans affinely_elim))
+  · exact (affine_affinely _).mpr.trans ((coreP_entails P Q).mpr (h.trans affinely_elim))
 
 #rocq_ignore coreP_proper "No Proper type class in Lean"
 #rocq_ignore coreP_mono "No Proper type class in Lean"

From 21fd066b089b0b9506d37444bedffb33c9cbf937 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Thu, 16 Jul 2026 21:56:36 +0200
Subject: [PATCH 12/13] Fix bug in `rw'` and simplify proofs in
 `BI/Lib/Core.lean`

---
 Iris/Iris/BI/Lib/Core.lean | 26 ++++++++++++++------------
 Iris/Iris/Std/Tactic.lean  |  6 ++----
 2 files changed, 16 insertions(+), 16 deletions(-)

diff --git a/Iris/Iris/BI/Lib/Core.lean b/Iris/Iris/BI/Lib/Core.lean
index 0dc6c706f..a2f099627 100644
--- a/Iris/Iris/BI/Lib/Core.lean
+++ b/Iris/Iris/BI/Lib/Core.lean
@@ -79,18 +79,21 @@ theorem coreP_elim (P : PROP) [Persistent P] : coreP P -∗ P := by
   · iintro !> !> #HP //
   · iintro !> !> HP //
 
-theorem coreP_entails_aux [BIPersistentlyForall PROP] {P Q : PROP}
-    (h : P ⊢ <pers> Q):
-    <affine> coreP P ⊢ <affine> coreP iprop(<pers> Q) := by
-  iintro #HP !>
+/- This is an instance of `Proper` in the Rocq version. -/
+@[rw_mono_rule, rocq_alias coreP_mono]
+theorem coreP_mono {P Q : PROP} (h : P ⊢ Q) : coreP P ⊢ coreP Q := by
   unfold coreP
-  iintro %R #HR #HQR
-  ispecialize HP $$ %R HR
-  iapply HP
+  iintro HPQ %R HR HQR
+  iapply HPQ $$ HR
   imodintro
   iapply plainly_mono <| wand_mono h .rfl
   iassumption
 
+/- This is an instance of `Proper` in the Rocq version. -/
+@[rocq_alias coreP_proper]
+theorem coreP_proper {P Q : PROP} (h : P ⊣⊢ Q) : coreP P ⊣⊢ coreP Q :=
+  BIBase.BiEntails.ofMono coreP_mono h
+
 @[rocq_alias coreP_entails]
 theorem coreP_entails [BIPersistentlyForall PROP] (P Q : PROP) :
     (<affine> coreP P ⊢ Q) ↔ (P ⊢ <pers> Q) := by
@@ -100,7 +103,7 @@ theorem coreP_entails [BIPersistentlyForall PROP] (P Q : PROP) :
     imodintro
     iapply h
     iassumption
-  · iapply (coreP_entails_aux h).trans
+  · rw' [h] -- Same as `iapply (affinely_mono <| coreP_mono h).trans`
     iintro #HcQ
     iapply coreP_elim $$ HcQ
 
@@ -111,10 +114,9 @@ theorem coreP_entails' [BIPersistentlyForall PROP] {P Q : PROP} [Affine P] :
   · apply affinely_intro
     apply (coreP_entails P Q).mp
     exact affinely_elim.trans h
-  · exact (affine_affinely _).mpr.trans ((coreP_entails P Q).mpr (h.trans affinely_elim))
+  · rw' [h]
+    apply (wand_entails <| coreP_elim iprop(□ Q)).trans intuitionistically_elim
 
-#rocq_ignore coreP_proper "No Proper type class in Lean"
-#rocq_ignore coreP_mono "No Proper type class in Lean"
-#rocq_ignore coreP_flip_mono "No Proper type class in Lean"
+#rocq_ignore coreP_flip_mono "No `Proper` type class in Lean, `rw'` works both ways"
 
 end Core
diff --git a/Iris/Iris/Std/Tactic.lean b/Iris/Iris/Std/Tactic.lean
index ac69f46e8..b2da2bac0 100644
--- a/Iris/Iris/Std/Tactic.lean
+++ b/Iris/Iris/Std/Tactic.lean
@@ -17,10 +17,8 @@ open Lean Lean.Elab.Tactic Lean.Meta
 and the transparency mode is set to `reducible`. Only non-dependent arguments of the applied
 theorem are turned into goals. -/
 def apply' (goal : MVarId) (name : Name) : TacticM <| Option <| List MVarId := do
-  let some ci := (← getEnv).find? name
-    | return none
-  let some value := ci.value?
-    | return none
+  unless (← getEnv).contains name do return none
+  let value ← mkConstWithFreshMVarLevels name   -- reference, not body; needs only the type
 
   let goals ← withoutRecover <| withReducible <| goal.apply value { newGoals := .nonDependentOnly }
   setGoals <| goals ++ (← getUnsolvedGoals)

From c403beca75ccbe452e4ad0d5182dc3891e1b5a1e Mon Sep 17 00:00:00 2001
From: Zongyuan Liu <liuzongyuan0505@gmail.com>
Date: Mon, 20 Jul 2026 18:53:20 +0200
Subject: [PATCH 13/13] Pass

---
 Iris/Iris/BI/Lib/Core.lean | 31 ++++++++++---------------------
 1 file changed, 10 insertions(+), 21 deletions(-)

diff --git a/Iris/Iris/BI/Lib/Core.lean b/Iris/Iris/BI/Lib/Core.lean
index a2f099627..533565113 100644
--- a/Iris/Iris/BI/Lib/Core.lean
+++ b/Iris/Iris/BI/Lib/Core.lean
@@ -18,7 +18,7 @@ open BI OFE
 
 @[rocq_alias coreP]
 def coreP [Sbi PROP] (P : PROP) : PROP :=
-  iprop(∀ Q, <affine> ■ (Q -∗ <pers> Q) -∗ <affine> ■ (P -∗ Q) -∗ Q)
+  iprop% ∀ Q, <affine> ■ (Q -∗ <pers> Q) -∗ <affine> ■ (P -∗ Q) -∗ Q
 
 variable [Sbi PROP]
 
@@ -51,16 +51,9 @@ instance coreP_affine (P : PROP) [Affine P] : Affine (coreP P) where
 
 @[rocq_alias coreP_ne]
 instance coreP_ne : NonExpansive (coreP (PROP := PROP)) where
-  ne n P Q H := by
-    unfold coreP
-    apply forall_ne
-    intro R
-    apply wand_ne.ne; rfl
-    apply wand_ne.ne
-    · apply affinely_ne.ne
-      apply instPlainly_ne.ne
-      apply wand_ne.ne H; rfl
-    · rfl
+  ne _ _ _ H :=
+    forall_ne fun _ => wand_ne.ne .rfl (wand_ne.ne
+      (affinely_ne.ne (instPlainly_ne.ne (wand_ne.ne H .rfl))) .rfl)
 
 @[rocq_alias coreP_wand]
 theorem coreP_wand (P Q : PROP) : <affine> ■ (P -∗ Q) -∗ coreP P -∗ coreP Q := by
@@ -86,13 +79,12 @@ theorem coreP_mono {P Q : PROP} (h : P ⊢ Q) : coreP P ⊢ coreP Q := by
   iintro HPQ %R HR HQR
   iapply HPQ $$ HR
   imodintro
-  iapply plainly_mono <| wand_mono h .rfl
-  iassumption
+  iapply plainly_mono <| wand_mono h .rfl $$ HQR
 
 /- This is an instance of `Proper` in the Rocq version. -/
 @[rocq_alias coreP_proper]
 theorem coreP_proper {P Q : PROP} (h : P ⊣⊢ Q) : coreP P ⊣⊢ coreP Q :=
-  BIBase.BiEntails.ofMono coreP_mono h
+  .ofMono coreP_mono h
 
 @[rocq_alias coreP_entails]
 theorem coreP_entails [BIPersistentlyForall PROP] (P Q : PROP) :
@@ -101,8 +93,7 @@ theorem coreP_entails [BIPersistentlyForall PROP] (P Q : PROP) :
   · iintro HP
     ihave #HPQ := coreP_intro $$ HP
     imodintro
-    iapply h
-    iassumption
+    iapply h $$ HPQ
   · rw' [h] -- Same as `iapply (affinely_mono <| coreP_mono h).trans`
     iintro #HcQ
     iapply coreP_elim $$ HcQ
@@ -111,11 +102,9 @@ theorem coreP_entails [BIPersistentlyForall PROP] (P Q : PROP) :
 theorem coreP_entails' [BIPersistentlyForall PROP] {P Q : PROP} [Affine P] :
     (coreP P ⊢ Q) ↔ (P ⊢ □ Q) := by
   constructor <;> intro h
-  · apply affinely_intro
-    apply (coreP_entails P Q).mp
-    exact affinely_elim.trans h
-  · rw' [h]
-    apply (wand_entails <| coreP_elim iprop(□ Q)).trans intuitionistically_elim
+  · exact affinely_intro <| (coreP_entails P Q).mp <| affinely_elim.trans h
+  · refine (coreP_mono h).trans ?_
+    exact (wand_entails <| coreP_elim iprop(□ Q)).trans intuitionistically_elim
 
 #rocq_ignore coreP_flip_mono "No `Proper` type class in Lean, `rw'` works both ways"