From fe231721aa08c8920d05124acfec6660a0e9050f Mon Sep 17 00:00:00 2001
From: arthur-adjedj <arthur.adjedj@ens-paris-saclay.fr>
Date: Thu, 28 May 2026 11:22:09 +0200
Subject: [PATCH 01/10] chore: add aesop dependency

---
 Iris/lake-manifest.json | 12 +++++++++++-
 Iris/lakefile.toml      |  5 +++++
 2 files changed, 16 insertions(+), 1 deletion(-)

diff --git a/Iris/lake-manifest.json b/Iris/lake-manifest.json
index d9fe3c60d..cc43a0ca3 100644
--- a/Iris/lake-manifest.json
+++ b/Iris/lake-manifest.json
@@ -1,7 +1,17 @@
 {"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/batteries",
+ [{"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "558915ae105bfd8074e22d597613d1961822adc2",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.30.0",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
diff --git a/Iris/lakefile.toml b/Iris/lakefile.toml
index 2239fdc58..73dfad968 100644
--- a/Iris/lakefile.toml
+++ b/Iris/lakefile.toml
@@ -11,6 +11,11 @@ name = "batteries"
 scope = "leanprover-community"
 rev = "v4.30.0"
 
+[[require]]
+name = "aesop"
+scope = "leanprover-community"
+rev = "v4.30.0"
+
 [[lean_lib]]
 name = "Iris"
 

From 3e9eb7a19022faf1c6f6a4876db01aa62613b6b2 Mon Sep 17 00:00:00 2001
From: arthur-adjedj <arthur.adjedj@ens-paris-saclay.fr>
Date: Thu, 28 May 2026 11:22:19 +0200
Subject: [PATCH 02/10] feat: `aesop_contractive` tactic

---
 Iris/Iris/Std/AesopContractive.lean | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 Iris/Iris/Std/AesopContractive.lean

diff --git a/Iris/Iris/Std/AesopContractive.lean b/Iris/Iris/Std/AesopContractive.lean
new file mode 100644
index 000000000..cf9f2e20f
--- /dev/null
+++ b/Iris/Iris/Std/AesopContractive.lean
@@ -0,0 +1,12 @@
+module
+public meta import Aesop
+
+declare_aesop_rule_sets [aesop_contractive]
+
+macro (name := aesop_cat) "aesop_contractive" c:Aesop.tactic_clause* : tactic =>
+`(tactic|
+  aesop $c* (config := { introsTransparency? := some .reducible, warnOnNonterminal := false })
+            (rule_sets := [$(Lean.mkIdent `aesop_contractive):ident]))
+
+--For some reason, it looks like builting rules cannot be removed from specific rulesets, only from the general aesop ruleset...
+erase_aesop_rules [Aesop.BuiltinRules.rfl, Exists]

From 7df65ca43199db3bc7a5415c3e83d7a3021ca6f8 Mon Sep 17 00:00:00 2001
From: arthur-adjedj <arthur.adjedj@ens-paris-saclay.fr>
Date: Thu, 28 May 2026 11:30:36 +0200
Subject: [PATCH 03/10] feat: add a few useful aesop_contractive annotations

---
 Iris/Iris/Algebra/OFE.lean             | 8 ++++++--
 Iris/Iris/BI/BI.lean                   | 6 ++++++
 Iris/Iris/BI/DerivedLaws.lean          | 1 +
 Iris/Iris/BI/Updates.lean              | 6 ++++++
 Iris/Iris/ProgramLogic/WeakestPre.lean | 2 +-
 Iris/Iris/Std/AesopContractive.lean    | 3 +--
 6 files changed, 21 insertions(+), 5 deletions(-)

diff --git a/Iris/Iris/Algebra/OFE.lean b/Iris/Iris/Algebra/OFE.lean
index 461c44d58..6242c2ed9 100644
--- a/Iris/Iris/Algebra/OFE.lean
+++ b/Iris/Iris/Algebra/OFE.lean
@@ -4,13 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 module
-
 public meta import Iris.Std.RocqPorting
+public meta import Iris.Std.AesopContractive
 
 @[expose] public section
 
 namespace Iris
 
+attribute [aesop unsafe 10% cases (rule_sets := [aesop_contractive])] Option
+
 /-- Ordered family of equivalences -/
 @[rocq_alias ofe]
 class OFE (α : Type _) where
@@ -106,7 +108,7 @@ theorem NonExpansive₂.ne_left [OFE α] [OFE β] [OFE γ] (f : α → β → γ
   ⟨fun {_ _ _} h => ne h Dist.rfl⟩
 
 /-- `DistLater n x y` means that `x` and `y` are `m`-equivalent for all `m < n`. -/
-@[rocq_alias dist_later]
+@[rocq_alias dist_later, aesop safe unfold (rule_sets := [aesop_contractive])]
 def DistLater [OFE α] (n : Nat) (x y : α) : Prop := ∀ m, m < n → x ≡{m}≡ y
 
 @[simp, refl] theorem DistLater.rfl [OFE α] {n} {x : α} : DistLater n x x := fun _ _ => .rfl
@@ -151,6 +153,8 @@ theorem distLater_soundness [OFE α] {x y : α} (H : ∀ n, DistLater n x y →
 class Contractive [OFE α] [OFE β] (f : α → β) where
   distLater_dist : DistLater n x y → f x ≡{n}≡ f y
 
+attribute [aesop safe apply (rule_sets := [aesop_contractive])] Contractive.distLater_dist
+
 @[simp, rocq_alias contractive_0] theorem Contractive.zero [OFE α] [OFE β] (f : α → β)
     [Contractive f] {x y} : f x ≡{0}≡ f y :=
   Contractive.distLater_dist distLater_zero
diff --git a/Iris/Iris/BI/BI.lean b/Iris/Iris/BI/BI.lean
index fd33d508b..faaafa867 100644
--- a/Iris/Iris/BI/BI.lean
+++ b/Iris/Iris/BI/BI.lean
@@ -89,6 +89,12 @@ attribute [instance] BI.entails_preorder
 theorem BIBase.Entails.trans [BI PROP] {P Q R : PROP} (h1 : P ⊢ Q) (h2 : Q ⊢ R) : P ⊢ R :=
   Transitive.trans h1 h2
 
+@[aesop safe apply (rule_sets := [aesop_contractive])]
+theorem wand_ne_ne [h : BI PROP] :  ∀ ⦃n x₁ x₂⦄, x₁ ≡{n}≡ x₂ → ∀ ⦃y₁ y₂⦄, y₁ ≡{n}≡ y₂ → h.wand x₁ y₁ ≡{n}≡ h.wand x₂ y₂ := wand_ne.ne
+
+@[aesop safe apply (rule_sets := [aesop_contractive])]
+theorem sep_ne_ne [h : BI PROP] :  ∀ ⦃n x₁ x₂⦄, x₁ ≡{n}≡ x₂ → ∀ ⦃y₁ y₂⦄, y₁ ≡{n}≡ y₂ → h.sep x₁ y₁ ≡{n}≡ h.sep x₂ y₂ := sep_ne.ne
+
 @[simp] theorem BIBase.Entails.rfl [BI PROP] {P : PROP} : P ⊢ P := refl
 
 theorem BIBase.Entails.of_eq [BI PROP] {P Q : PROP} (h : P = Q) : P ⊢ Q := h ▸ .rfl
diff --git a/Iris/Iris/BI/DerivedLaws.lean b/Iris/Iris/BI/DerivedLaws.lean
index 20b20b55b..cde59f01c 100644
--- a/Iris/Iris/BI/DerivedLaws.lean
+++ b/Iris/Iris/BI/DerivedLaws.lean
@@ -119,6 +119,7 @@ theorem imp_congr_l [BI PROP] {P P' Q : PROP} (h : P ⊣⊢ P') : (P → Q) ⊣
 theorem imp_congr_r [BI PROP] {P Q Q' : PROP} (h : Q ⊣⊢ Q') : (P → Q) ⊣⊢ (P → Q') :=
   imp_congr .rfl h
 
+@[aesop safe apply (rule_sets := [aesop_contractive])]
 theorem forall_ne [BI PROP] {Φ Ψ : α → PROP} (h : ∀ a, Φ a ≡{n}≡ Ψ a) :
     iprop(∀ a, Φ a) ≡{n}≡ iprop(∀ a, Ψ a) := sForall_ne <| by
   constructor <;> rintro _ ⟨a, rfl⟩ <;> exact ⟨_, ⟨a, rfl⟩, h _⟩
diff --git a/Iris/Iris/BI/Updates.lean b/Iris/Iris/BI/Updates.lean
index e1c67fb11..25aa1f08f 100644
--- a/Iris/Iris/BI/Updates.lean
+++ b/Iris/Iris/BI/Updates.lean
@@ -170,6 +170,9 @@ class BIFUpdate (PROP : Type _) [BI PROP] extends FUpd PROP where
     E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ⊢ |={E1 ∪ Ef,E2 ∪ Ef}=> P
   frame_r {E1 E2 : CoPset} {P R : PROP} : (|={E1,E2}=> P) ∗ R ⊢ |={E1,E2}=> P ∗ R
 
+@[aesop safe apply (rule_sets := [aesop_contractive])]
+theorem BIFUpdate.ne_ne [BI PROP] [h : BIFUpdate PROP] : ∀ ⦃n x₁ x₂⦄, x₁ ≡{n}≡ x₂ → iprop(|={E1,E2}=> x₁ : PROP) ≡{n}≡ iprop(|={E1,E2}=> x₂ : PROP) := ne.ne
+
 class BIUpdateFUpdate (PROP : Type _) [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] where
   fupd_of_bupd {P : PROP} {E : CoPset} : (|==> P) ⊢ |={E}=> P
 
@@ -414,6 +417,9 @@ theorem step_fupdN_ne {E1 E2 : CoPset} {n : Nat} :
     | zero => simp [Nat.repeat, xy_i]
     | succ n IH => exact ne.ne (later_ne.ne (ne.ne IH))
 
+@[aesop safe apply (rule_sets := [aesop_contractive])]
+def step_fupdN_ne_ne {E1 E2 : CoPset} ⦃n : Nat⦄ := (@step_fupdN_ne PROP _ _  E1 E2 n).ne
+
 theorem step_fupd_mono {Eo Ei : CoPset} {P Q : PROP} :
     (Q ⊢ P) → (|={Eo}[Ei]▷=> Q) ⊢ |={Eo}[Ei]▷=> P :=
   (mono <| later_mono <| mono ·)
diff --git a/Iris/Iris/ProgramLogic/WeakestPre.lean b/Iris/Iris/ProgramLogic/WeakestPre.lean
index ee9669866..7b0a4586f 100644
--- a/Iris/Iris/ProgramLogic/WeakestPre.lean
+++ b/Iris/Iris/ProgramLogic/WeakestPre.lean
@@ -65,7 +65,7 @@ abbrev Stuckness.MaybeReducible : Stuckness → Expr × State → Prop
 | .NotStuck, (e₁, σ₁) => PrimStep.Reducible (e₁, σ₁)
 | _, _ => True
 
-@[rocq_alias wp_pre]
+@[rocq_alias wp_pre, aesop safe unfold (rule_sets := [aesop_contractive])]
 def wp.pre (s : Stuckness) (wp : CoPset -> Expr -> (Val -> IProp GF) -> IProp GF) (E : CoPset)
     (e₁ : Expr) (Φ : Val -> IProp GF) : IProp GF :=
   match toVal e₁ with
diff --git a/Iris/Iris/Std/AesopContractive.lean b/Iris/Iris/Std/AesopContractive.lean
index cf9f2e20f..79369e065 100644
--- a/Iris/Iris/Std/AesopContractive.lean
+++ b/Iris/Iris/Std/AesopContractive.lean
@@ -8,5 +8,4 @@ macro (name := aesop_cat) "aesop_contractive" c:Aesop.tactic_clause* : tactic =>
   aesop $c* (config := { introsTransparency? := some .reducible, warnOnNonterminal := false })
             (rule_sets := [$(Lean.mkIdent `aesop_contractive):ident]))
 
---For some reason, it looks like builting rules cannot be removed from specific rulesets, only from the general aesop ruleset...
-erase_aesop_rules [Aesop.BuiltinRules.rfl, Exists]
+attribute [simp] Nat.repeat

From 67eb2ed20579126108272712676a95dc03c8c7d1 Mon Sep 17 00:00:00 2001
From: arthur-adjedj <arthur.adjedj@ens-paris-saclay.fr>
Date: Thu, 28 May 2026 11:30:53 +0200
Subject: [PATCH 04/10] feat: use `aesop_contractive on a few examples`

---
 Iris/Iris/ProgramLogic/WeakestPre.lean | 75 ++++----------------------
 1 file changed, 11 insertions(+), 64 deletions(-)

diff --git a/Iris/Iris/ProgramLogic/WeakestPre.lean b/Iris/Iris/ProgramLogic/WeakestPre.lean
index 7b0a4586f..bfb5fdf73 100644
--- a/Iris/Iris/ProgramLogic/WeakestPre.lean
+++ b/Iris/Iris/ProgramLogic/WeakestPre.lean
@@ -78,37 +78,17 @@ def wp.pre (s : Stuckness) (wp : CoPset -> Expr -> (Val -> IProp GF) -> IProp GF
       stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗
       wp E e₂ Φ ∗ [∗list] e' ∈ eₜ, wp ⊤ e' ι.forkPost)
 
+/-For some reason, it looks like builting rules cannot be removed from specific rulesets, only from the general aesop ruleset...
+  These rules also seem to get re-integrated in the ruleset when imported from another file.. ?
+-/
+erase_aesop_rules [Aesop.BuiltinRules.rfl, Exists]
 @[rocq_alias wp_pre_contractive]
 instance wp.pre.contractive s : OFE.Contractive (wp.pre s (ι := ι)) where
   distLater_dist := by
     intros n wp wp' Hwp E e₁ Φ
-    unfold pre
-    cases toVal e₁
-    case some _ =>
-      exact .rfl
-    case none =>
-      refine BI.forall_ne (fun σ₁ => ?_)
-      refine BI.forall_ne (fun ns => ?_)
-      refine BI.forall_ne (fun obs => ?_)
-      refine BI.forall_ne (fun obs' => ?_)
-      refine BI.forall_ne (fun nt => ?_)
-      refine BI.wand_ne.ne .rfl ?_
-      refine BIFUpdate.ne.ne ?_
-      refine BI.sep_ne.ne .rfl ?_
-      refine BI.forall_ne (fun e₂  => ?_)
-      refine BI.forall_ne (fun σ₂ => ?_)
-      refine BI.forall_ne (fun eₜ => ?_)
-      refine BI.wand_ne.ne .rfl ?_
-      refine BI.wand_ne.ne .rfl ?_
-      refine BIFUpdate.ne.ne ?_
-      refine OFE.Contractive.distLater_dist fun m m_n => ?_
-      refine BIFUpdate.ne.ne ?_
-      refine step_fupdN_ne.ne ?_
-      refine BIFUpdate.ne.ne ?_
-      refine BI.sep_ne.ne .rfl ?_
-      refine BI.sep_ne.ne ?_ ?_
-      · exact Hwp m m_n _ _ _
-      · exact BI.BigSepL.bigSepL_dist <| fun _ => Hwp m m_n _ _ _
+    aesop_contractive
+    · exact Hwp m ‹_› _ _ _
+    · exact BI.BigSepL.bigSepL_dist <| fun _ => Hwp m ‹_› _ _ _
 
 @[rocq_alias wp_def]
 instance wp.def : Wp (IProp GF) (Expr) (Val) Stuckness where
@@ -136,24 +116,8 @@ instance wp_ne {s : Stuckness} {E} {e : Expr} :
     case some v =>
       exact BIFUpdate.ne.ne <| HΦ v
     case none =>
-      refine BI.forall_ne fun σ₁ => ?_
-      refine BI.forall_ne fun ns => ?_
-      refine BI.forall_ne fun obs => ?_
-      refine BI.forall_ne fun obs' => ?_
-      refine BI.forall_ne fun nt => ?_
-      refine BI.wand_ne.ne .rfl ?_
-      refine BIFUpdate.ne.ne ?_
-      refine BI.sep_ne.ne .rfl ?_
-      refine BI.forall_ne fun e₂  => ?_
-      refine BI.forall_ne fun σ₂ => ?_
-      refine BI.forall_ne fun eₜ => ?_
-      refine BI.wand_ne.ne .rfl ?_
-      refine BI.wand_ne.ne .rfl ?_
-      refine step_fupdN_contractive.distLater_dist fun m n_m => ?_
-      refine BIFUpdate.ne.ne ?_
-      refine BI.sep_ne.ne .rfl ?_
-      refine BI.sep_ne.ne ?_ .rfl
-      exact IH m n_m <| OFE.dist_lt HΦ n_m
+      aesop_contractive
+      exact IH m ‹_›  <| OFE.dist_lt HΦ ‹_›
 
 #rocq_ignore wp_proper "Derivable using NonExpansive.eqv"
 
@@ -162,26 +126,9 @@ instance wp_contractive (s : Stuckness) E (e : Expr) (h : toVal e = none) :
     OFE.Contractive (Wp.wp (PROP := IProp GF) s E e) where
   distLater_dist {n Φ₁ Φ₂} HΦ := by
     simp only [IProp.ext wp_unfold]
-    simp only [wp.pre, h]
-    refine BI.forall_ne fun σ₁ => ?_
-    refine BI.forall_ne fun ns => ?_
-    refine BI.forall_ne fun obs => ?_
-    refine BI.forall_ne fun obs' => ?_
-    refine BI.forall_ne fun nt => ?_
-    refine BI.wand_ne.ne .rfl ?_
-    refine BIFUpdate.ne.ne ?_
-    refine BI.sep_ne.ne .rfl ?_
-    refine BI.forall_ne fun e₂  => ?_
-    refine BI.forall_ne fun σ₂ => ?_
-    refine BI.forall_ne fun eₜ => ?_
-    refine BI.wand_ne.ne .rfl ?_
-    refine BI.wand_ne.ne .rfl ?_
-    refine step_fupdN_contractive.distLater_dist fun m n_m => ?_
-    refine BIFUpdate.ne.ne ?_
-    refine BI.sep_ne.ne .rfl ?_
-    refine BI.sep_ne.ne ?_ .rfl
+    aesop_contractive
     refine wp_ne.ne ?_
-    exact HΦ m n_m
+    exact HΦ m ‹_›
 
 @[rocq_alias wp_value_fupd']
 theorem wp_value_fupd' {s : Stuckness} {E} {Φ : Val → IProp GF} {v : Val} :

From 041cbdd695d2871d641f948c2a656cdb170d9416 Mon Sep 17 00:00:00 2001
From: arthur-adjedj <arthur.adjedj@ens-paris-saclay.fr>
Date: Thu, 28 May 2026 12:28:49 +0200
Subject: [PATCH 05/10] fix: remove `erase_aesop_rules` This is done by 1.
 weakening `introsTransparency?` to `none` and 2. erasing
 `Aesop.BuiltinRules.rfl` at call-site in the tactic-macro

---
 Iris/Iris/ProgramLogic/WeakestPre.lean | 4 ----
 Iris/Iris/Std/AesopContractive.lean    | 4 ++--
 2 files changed, 2 insertions(+), 6 deletions(-)

diff --git a/Iris/Iris/ProgramLogic/WeakestPre.lean b/Iris/Iris/ProgramLogic/WeakestPre.lean
index bfb5fdf73..b6b42de4a 100644
--- a/Iris/Iris/ProgramLogic/WeakestPre.lean
+++ b/Iris/Iris/ProgramLogic/WeakestPre.lean
@@ -78,10 +78,6 @@ def wp.pre (s : Stuckness) (wp : CoPset -> Expr -> (Val -> IProp GF) -> IProp GF
       stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗
       wp E e₂ Φ ∗ [∗list] e' ∈ eₜ, wp ⊤ e' ι.forkPost)
 
-/-For some reason, it looks like builting rules cannot be removed from specific rulesets, only from the general aesop ruleset...
-  These rules also seem to get re-integrated in the ruleset when imported from another file.. ?
--/
-erase_aesop_rules [Aesop.BuiltinRules.rfl, Exists]
 @[rocq_alias wp_pre_contractive]
 instance wp.pre.contractive s : OFE.Contractive (wp.pre s (ι := ι)) where
   distLater_dist := by
diff --git a/Iris/Iris/Std/AesopContractive.lean b/Iris/Iris/Std/AesopContractive.lean
index 79369e065..172ae03df 100644
--- a/Iris/Iris/Std/AesopContractive.lean
+++ b/Iris/Iris/Std/AesopContractive.lean
@@ -5,7 +5,7 @@ declare_aesop_rule_sets [aesop_contractive]
 
 macro (name := aesop_cat) "aesop_contractive" c:Aesop.tactic_clause* : tactic =>
 `(tactic|
-  aesop $c* (config := { introsTransparency? := some .reducible, warnOnNonterminal := false })
-            (rule_sets := [$(Lean.mkIdent `aesop_contractive):ident]))
+  aesop $c* (config := { introsTransparency? := some .none, warnOnNonterminal := false })
+            (rule_sets := [$(Lean.mkIdent `aesop_contractive):ident]) (erase Aesop.BuiltinRules.rfl))
 
 attribute [simp] Nat.repeat

From a237b966bb905e8d3467022bfc70498e5264ad66 Mon Sep 17 00:00:00 2001
From: arthur-adjedj <arthur.adjedj@ens-paris-saclay.fr>
Date: Thu, 28 May 2026 13:37:02 +0200
Subject: [PATCH 06/10] feta: add `aesop_contractive` attribute TODO: make it
 smarter on `NonExpansive` theorems

---
 Iris/Iris/Algebra/OFE.lean             |  6 ++--
 Iris/Iris/BI/BI.lean                   |  4 +--
 Iris/Iris/BI/DerivedLaws.lean          |  2 +-
 Iris/Iris/BI/Updates.lean              |  4 +--
 Iris/Iris/ProgramLogic/WeakestPre.lean |  2 +-
 Iris/Iris/Std/AesopContractive.lean    | 38 ++++++++++++++++++++++++++
 6 files changed, 47 insertions(+), 9 deletions(-)

diff --git a/Iris/Iris/Algebra/OFE.lean b/Iris/Iris/Algebra/OFE.lean
index 6242c2ed9..c3673e20b 100644
--- a/Iris/Iris/Algebra/OFE.lean
+++ b/Iris/Iris/Algebra/OFE.lean
@@ -11,7 +11,7 @@ public meta import Iris.Std.AesopContractive
 
 namespace Iris
 
-attribute [aesop unsafe 10% cases (rule_sets := [aesop_contractive])] Option
+attribute [aesop_contractive unsafe 10% cases] Option
 
 /-- Ordered family of equivalences -/
 @[rocq_alias ofe]
@@ -108,7 +108,7 @@ theorem NonExpansive₂.ne_left [OFE α] [OFE β] [OFE γ] (f : α → β → γ
   ⟨fun {_ _ _} h => ne h Dist.rfl⟩
 
 /-- `DistLater n x y` means that `x` and `y` are `m`-equivalent for all `m < n`. -/
-@[rocq_alias dist_later, aesop safe unfold (rule_sets := [aesop_contractive])]
+@[rocq_alias dist_later, aesop_contractive safe unfold]
 def DistLater [OFE α] (n : Nat) (x y : α) : Prop := ∀ m, m < n → x ≡{m}≡ y
 
 @[simp, refl] theorem DistLater.rfl [OFE α] {n} {x : α} : DistLater n x x := fun _ _ => .rfl
@@ -153,7 +153,7 @@ theorem distLater_soundness [OFE α] {x y : α} (H : ∀ n, DistLater n x y →
 class Contractive [OFE α] [OFE β] (f : α → β) where
   distLater_dist : DistLater n x y → f x ≡{n}≡ f y
 
-attribute [aesop safe apply (rule_sets := [aesop_contractive])] Contractive.distLater_dist
+attribute [aesop_contractive safe apply] Contractive.distLater_dist
 
 @[simp, rocq_alias contractive_0] theorem Contractive.zero [OFE α] [OFE β] (f : α → β)
     [Contractive f] {x y} : f x ≡{0}≡ f y :=
diff --git a/Iris/Iris/BI/BI.lean b/Iris/Iris/BI/BI.lean
index faaafa867..bedb19087 100644
--- a/Iris/Iris/BI/BI.lean
+++ b/Iris/Iris/BI/BI.lean
@@ -89,10 +89,10 @@ attribute [instance] BI.entails_preorder
 theorem BIBase.Entails.trans [BI PROP] {P Q R : PROP} (h1 : P ⊢ Q) (h2 : Q ⊢ R) : P ⊢ R :=
   Transitive.trans h1 h2
 
-@[aesop safe apply (rule_sets := [aesop_contractive])]
+@[aesop_contractive safe apply]
 theorem wand_ne_ne [h : BI PROP] :  ∀ ⦃n x₁ x₂⦄, x₁ ≡{n}≡ x₂ → ∀ ⦃y₁ y₂⦄, y₁ ≡{n}≡ y₂ → h.wand x₁ y₁ ≡{n}≡ h.wand x₂ y₂ := wand_ne.ne
 
-@[aesop safe apply (rule_sets := [aesop_contractive])]
+@[aesop_contractive safe apply]
 theorem sep_ne_ne [h : BI PROP] :  ∀ ⦃n x₁ x₂⦄, x₁ ≡{n}≡ x₂ → ∀ ⦃y₁ y₂⦄, y₁ ≡{n}≡ y₂ → h.sep x₁ y₁ ≡{n}≡ h.sep x₂ y₂ := sep_ne.ne
 
 @[simp] theorem BIBase.Entails.rfl [BI PROP] {P : PROP} : P ⊢ P := refl
diff --git a/Iris/Iris/BI/DerivedLaws.lean b/Iris/Iris/BI/DerivedLaws.lean
index cde59f01c..2c0246442 100644
--- a/Iris/Iris/BI/DerivedLaws.lean
+++ b/Iris/Iris/BI/DerivedLaws.lean
@@ -119,7 +119,7 @@ theorem imp_congr_l [BI PROP] {P P' Q : PROP} (h : P ⊣⊢ P') : (P → Q) ⊣
 theorem imp_congr_r [BI PROP] {P Q Q' : PROP} (h : Q ⊣⊢ Q') : (P → Q) ⊣⊢ (P → Q') :=
   imp_congr .rfl h
 
-@[aesop safe apply (rule_sets := [aesop_contractive])]
+@[aesop_contractive safe apply]
 theorem forall_ne [BI PROP] {Φ Ψ : α → PROP} (h : ∀ a, Φ a ≡{n}≡ Ψ a) :
     iprop(∀ a, Φ a) ≡{n}≡ iprop(∀ a, Ψ a) := sForall_ne <| by
   constructor <;> rintro _ ⟨a, rfl⟩ <;> exact ⟨_, ⟨a, rfl⟩, h _⟩
diff --git a/Iris/Iris/BI/Updates.lean b/Iris/Iris/BI/Updates.lean
index 25aa1f08f..fcd795f0a 100644
--- a/Iris/Iris/BI/Updates.lean
+++ b/Iris/Iris/BI/Updates.lean
@@ -170,7 +170,7 @@ class BIFUpdate (PROP : Type _) [BI PROP] extends FUpd PROP where
     E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ⊢ |={E1 ∪ Ef,E2 ∪ Ef}=> P
   frame_r {E1 E2 : CoPset} {P R : PROP} : (|={E1,E2}=> P) ∗ R ⊢ |={E1,E2}=> P ∗ R
 
-@[aesop safe apply (rule_sets := [aesop_contractive])]
+@[aesop_contractive safe apply]
 theorem BIFUpdate.ne_ne [BI PROP] [h : BIFUpdate PROP] : ∀ ⦃n x₁ x₂⦄, x₁ ≡{n}≡ x₂ → iprop(|={E1,E2}=> x₁ : PROP) ≡{n}≡ iprop(|={E1,E2}=> x₂ : PROP) := ne.ne
 
 class BIUpdateFUpdate (PROP : Type _) [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] where
@@ -417,7 +417,7 @@ theorem step_fupdN_ne {E1 E2 : CoPset} {n : Nat} :
     | zero => simp [Nat.repeat, xy_i]
     | succ n IH => exact ne.ne (later_ne.ne (ne.ne IH))
 
-@[aesop safe apply (rule_sets := [aesop_contractive])]
+@[aesop_contractive safe apply]
 def step_fupdN_ne_ne {E1 E2 : CoPset} ⦃n : Nat⦄ := (@step_fupdN_ne PROP _ _  E1 E2 n).ne
 
 theorem step_fupd_mono {Eo Ei : CoPset} {P Q : PROP} :
diff --git a/Iris/Iris/ProgramLogic/WeakestPre.lean b/Iris/Iris/ProgramLogic/WeakestPre.lean
index b6b42de4a..e9be62f27 100644
--- a/Iris/Iris/ProgramLogic/WeakestPre.lean
+++ b/Iris/Iris/ProgramLogic/WeakestPre.lean
@@ -65,7 +65,7 @@ abbrev Stuckness.MaybeReducible : Stuckness → Expr × State → Prop
 | .NotStuck, (e₁, σ₁) => PrimStep.Reducible (e₁, σ₁)
 | _, _ => True
 
-@[rocq_alias wp_pre, aesop safe unfold (rule_sets := [aesop_contractive])]
+@[rocq_alias wp_pre, aesop_contractive safe unfold]
 def wp.pre (s : Stuckness) (wp : CoPset -> Expr -> (Val -> IProp GF) -> IProp GF) (E : CoPset)
     (e₁ : Expr) (Φ : Val -> IProp GF) : IProp GF :=
   match toVal e₁ with
diff --git a/Iris/Iris/Std/AesopContractive.lean b/Iris/Iris/Std/AesopContractive.lean
index 172ae03df..63aaaded2 100644
--- a/Iris/Iris/Std/AesopContractive.lean
+++ b/Iris/Iris/Std/AesopContractive.lean
@@ -1,5 +1,8 @@
 module
 public meta import Aesop
+public meta import Lean
+
+open Lean Elab
 
 declare_aesop_rule_sets [aesop_contractive]
 
@@ -9,3 +12,38 @@ macro (name := aesop_cat) "aesop_contractive" c:Aesop.tactic_clause* : tactic =>
             (rule_sets := [$(Lean.mkIdent `aesop_contractive):ident]) (erase Aesop.BuiltinRules.rfl))
 
 attribute [simp] Nat.repeat
+
+syntax (name := aesop_contractive_attr) "aesop_contractive " Aesop.attr_rules : attr
+
+open Aesop Frontend
+
+meta def elabConfig (stx : Syntax) : TermElabM AttrConfig :=
+  withRef stx do
+    match stx with
+    | `(attr| aesop_contractive $e:Aesop.rule_expr) => do
+      let e ← `(Aesop.rule_expr| (rule_sets := [$(Lean.mkIdent `aesop_contractive):ident]) $e:Aesop.rule_expr)
+      let r ← RuleExpr.elab e |>.run $ ← ElabM.Context.forAdditionalGlobalRules
+      return { rules := #[r] }
+    | `(attr| aesop_contractive [ $es:Aesop.rule_expr,* ]) => do
+      let es ← es.getElems.mapM fun e => `(Aesop.rule_expr| (rule_sets := [$(Lean.mkIdent `aesop_contractive):ident]) $e:Aesop.rule_expr)
+      let ctx ← ElabM.Context.forAdditionalGlobalRules
+      let rs ← (es : Array Syntax).mapM λ e => RuleExpr.elab e |>.run ctx
+      return { rules := rs }
+    | _ => throwUnsupportedSyntax
+
+meta initialize registerBuiltinAttribute {
+    name := `aesop_contractive_attr
+    descr := "Adds a given declaration to the ruleset for the `aesop_contractive` tactic."
+    applicationTime := .afterCompilation
+    add := fun src stx kind ↦ withRef stx do Aesop.runTermElabMAsCoreM do
+      let config ← elabConfig stx
+      let decl ← getConstInfo src
+      let rules ← config.rules.flatMapM (·.buildAdditionalGlobalRules src)
+      for (rule, rsNames) in rules do
+        for rsName in rsNames do
+          addGlobalRule rsName rule kind (checkNotExists := true)
+    erase := λ decl =>
+      let ruleFilter :=
+        { name := decl, scope := .global, builders := #[], phases := #[] }
+      eraseGlobalRules RuleSetNameFilter.all ruleFilter (checkExists := true)
+  }

From 4f6cc668747fbb913496a342fa2475c4140d1ac2 Mon Sep 17 00:00:00 2001
From: arthur-adjedj <arthur.adjedj@ens-paris-saclay.fr>
Date: Thu, 28 May 2026 14:36:28 +0200
Subject: [PATCH 07/10] feat: smarter `aesop_contractive` attribute when
 tagging `NonExpansive` theorems

---
 Iris/Iris/Algebra/OFE.lean             | 10 +++++-----
 Iris/Iris/BI/BI.lean                   |  8 ++------
 Iris/Iris/BI/Updates.lean              |  7 ++-----
 Iris/Iris/ProgramLogic/WeakestPre.lean |  6 +++---
 Iris/Iris/Std/AesopContractive.lean    | 25 +++++++++++++++++++++----
 5 files changed, 33 insertions(+), 23 deletions(-)

diff --git a/Iris/Iris/Algebra/OFE.lean b/Iris/Iris/Algebra/OFE.lean
index c3673e20b..f9828d40c 100644
--- a/Iris/Iris/Algebra/OFE.lean
+++ b/Iris/Iris/Algebra/OFE.lean
@@ -155,27 +155,27 @@ class Contractive [OFE α] [OFE β] (f : α → β) where
 
 attribute [aesop_contractive safe apply] Contractive.distLater_dist
 
-@[simp, rocq_alias contractive_0] theorem Contractive.zero [OFE α] [OFE β] (f : α → β)
+@[simp, aesop_contractive safe apply, rocq_alias contractive_0] theorem Contractive.zero [OFE α] [OFE β] (f : α → β)
     [Contractive f] {x y} : f x ≡{0}≡ f y :=
   Contractive.distLater_dist distLater_zero
 
-@[rocq_alias contractive_S]
+@[aesop_contractive safe apply, rocq_alias contractive_S]
 theorem Contractive.succ [OFE α] [OFE β] (f : α → β) [Contractive f] {n x y}
     (h : x ≡{n}≡ y) : f x ≡{n.succ}≡ f y :=
   Contractive.distLater_dist (distLater_succ.2 h)
 
 /-- A contractive function is non-expansive. -/
-@[rocq_alias contractive_ne]
+@[aesop_contractive safe apply, rocq_alias contractive_ne]
 instance ne_of_contractive [OFE α] [OFE β] (f : α → β) [Contractive f] : NonExpansive f where
   ne := fun _ _ _ h => Contractive.distLater_dist (Dist.distLater h)
 
 /-- A contractive function preserves equivalence. -/
-@[rocq_alias contractive_proper]
+@[aesop_contractive safe apply, rocq_alias contractive_proper]
 theorem Contractive.eqv [OFE α] [OFE β] (f : α → β) [Contractive f] ⦃x y : α⦄ (h : x ≡ y) :
     f x ≡ f y := NonExpansive.eqv h
 
 /-- Constant functions are contractive. -/
-@[rocq_alias const_contractive]
+@[aesop_contractive safe apply, rocq_alias const_contractive]
 instance [OFE α] [OFE β] {x : β} : Contractive (fun _ : α => x) where
   distLater_dist := fun _ => Dist.rfl
 
diff --git a/Iris/Iris/BI/BI.lean b/Iris/Iris/BI/BI.lean
index bedb19087..fc55d20f1 100644
--- a/Iris/Iris/BI/BI.lean
+++ b/Iris/Iris/BI/BI.lean
@@ -85,16 +85,12 @@ class BI (PROP : Type _) extends COFE PROP, BI.BIBase PROP where
 namespace BI
 
 attribute [instance] BI.entails_preorder
+attribute [aesop_contractive safe apply] and_ne or_ne imp_ne sForall_ne sExists_ne sep_ne wand_ne persistently_ne
+attribute [aesop_contractive unsafe 90% apply] later_ne
 
 theorem BIBase.Entails.trans [BI PROP] {P Q R : PROP} (h1 : P ⊢ Q) (h2 : Q ⊢ R) : P ⊢ R :=
   Transitive.trans h1 h2
 
-@[aesop_contractive safe apply]
-theorem wand_ne_ne [h : BI PROP] :  ∀ ⦃n x₁ x₂⦄, x₁ ≡{n}≡ x₂ → ∀ ⦃y₁ y₂⦄, y₁ ≡{n}≡ y₂ → h.wand x₁ y₁ ≡{n}≡ h.wand x₂ y₂ := wand_ne.ne
-
-@[aesop_contractive safe apply]
-theorem sep_ne_ne [h : BI PROP] :  ∀ ⦃n x₁ x₂⦄, x₁ ≡{n}≡ x₂ → ∀ ⦃y₁ y₂⦄, y₁ ≡{n}≡ y₂ → h.sep x₁ y₁ ≡{n}≡ h.sep x₂ y₂ := sep_ne.ne
-
 @[simp] theorem BIBase.Entails.rfl [BI PROP] {P : PROP} : P ⊢ P := refl
 
 theorem BIBase.Entails.of_eq [BI PROP] {P Q : PROP} (h : P = Q) : P ⊢ Q := h ▸ .rfl
diff --git a/Iris/Iris/BI/Updates.lean b/Iris/Iris/BI/Updates.lean
index fcd795f0a..13a6c9211 100644
--- a/Iris/Iris/BI/Updates.lean
+++ b/Iris/Iris/BI/Updates.lean
@@ -170,8 +170,7 @@ class BIFUpdate (PROP : Type _) [BI PROP] extends FUpd PROP where
     E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ⊢ |={E1 ∪ Ef,E2 ∪ Ef}=> P
   frame_r {E1 E2 : CoPset} {P R : PROP} : (|={E1,E2}=> P) ∗ R ⊢ |={E1,E2}=> P ∗ R
 
-@[aesop_contractive safe apply]
-theorem BIFUpdate.ne_ne [BI PROP] [h : BIFUpdate PROP] : ∀ ⦃n x₁ x₂⦄, x₁ ≡{n}≡ x₂ → iprop(|={E1,E2}=> x₁ : PROP) ≡{n}≡ iprop(|={E1,E2}=> x₂ : PROP) := ne.ne
+attribute [aesop_contractive safe apply] BIFUpdate.ne
 
 class BIUpdateFUpdate (PROP : Type _) [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] where
   fupd_of_bupd {P : PROP} {E : CoPset} : (|==> P) ⊢ |={E}=> P
@@ -410,6 +409,7 @@ theorem step_fupdN_contractive {E1 E2 : CoPset} {n : Nat} [ι : BILaterContracti
     | zero => exact ne.ne (ι.distLater_dist (ne.ne <| xy_i · ·))
     | succ n IH => exact ne.ne (later_ne.ne (ne.ne IH))
 
+@[aesop_contractive safe apply]
 theorem step_fupdN_ne {E1 E2 : CoPset} {n : Nat} :
     OFE.NonExpansive (iprop(|={E1}[E2]▷=>^[n] · : PROP)) where
   ne {i x y} xy_i := by
@@ -417,9 +417,6 @@ theorem step_fupdN_ne {E1 E2 : CoPset} {n : Nat} :
     | zero => simp [Nat.repeat, xy_i]
     | succ n IH => exact ne.ne (later_ne.ne (ne.ne IH))
 
-@[aesop_contractive safe apply]
-def step_fupdN_ne_ne {E1 E2 : CoPset} ⦃n : Nat⦄ := (@step_fupdN_ne PROP _ _  E1 E2 n).ne
-
 theorem step_fupd_mono {Eo Ei : CoPset} {P Q : PROP} :
     (Q ⊢ P) → (|={Eo}[Ei]▷=> Q) ⊢ |={Eo}[Ei]▷=> P :=
   (mono <| later_mono <| mono ·)
diff --git a/Iris/Iris/ProgramLogic/WeakestPre.lean b/Iris/Iris/ProgramLogic/WeakestPre.lean
index e9be62f27..d18de15bc 100644
--- a/Iris/Iris/ProgramLogic/WeakestPre.lean
+++ b/Iris/Iris/ProgramLogic/WeakestPre.lean
@@ -83,8 +83,8 @@ instance wp.pre.contractive s : OFE.Contractive (wp.pre s (ι := ι)) where
   distLater_dist := by
     intros n wp wp' Hwp E e₁ Φ
     aesop_contractive
-    · exact Hwp m ‹_› _ _ _
-    · exact BI.BigSepL.bigSepL_dist <| fun _ => Hwp m ‹_› _ _ _
+    · exact Hwp _ ‹_› _ _ _
+    · exact BI.BigSepL.bigSepL_dist <| fun _ => Hwp _ ‹_› _ _ _
 
 @[rocq_alias wp_def]
 instance wp.def : Wp (IProp GF) (Expr) (Val) Stuckness where
@@ -124,7 +124,7 @@ instance wp_contractive (s : Stuckness) E (e : Expr) (h : toVal e = none) :
     simp only [IProp.ext wp_unfold]
     aesop_contractive
     refine wp_ne.ne ?_
-    exact HΦ m ‹_›
+    exact HΦ _ ‹_›
 
 @[rocq_alias wp_value_fupd']
 theorem wp_value_fupd' {s : Stuckness} {E} {Φ : Val → IProp GF} {v : Val} :
diff --git a/Iris/Iris/Std/AesopContractive.lean b/Iris/Iris/Std/AesopContractive.lean
index 63aaaded2..4ea7c741b 100644
--- a/Iris/Iris/Std/AesopContractive.lean
+++ b/Iris/Iris/Std/AesopContractive.lean
@@ -2,7 +2,7 @@ module
 public meta import Aesop
 public meta import Lean
 
-open Lean Elab
+open Lean Elab Meta
 
 declare_aesop_rule_sets [aesop_contractive]
 
@@ -31,14 +31,31 @@ meta def elabConfig (stx : Syntax) : TermElabM AttrConfig :=
       return { rules := rs }
     | _ => throwUnsupportedSyntax
 
+meta def auxIfIsNonExpansiveDecl (declName : Name) : TermElabM Name := do
+  let decl ← getConstInfo declName
+  forallTelescope decl.type fun xs ty => ty.withApp fun fn _ => do
+    if let .const fnName _ := fn then
+      unless fnName = `Iris.OFE.NonExpansive || fnName = `Iris.OFE.NonExpansive₂ do
+        return declName
+      let declLvls := decl.levelParams.map Level.param
+      let declWithArgs := mkAppN (mkConst declName declLvls) xs
+      let proj ←  mkProjection declWithArgs `ne
+      withDeclNameForAuxNaming declName do
+        let auxName ← mkAuxDeclName
+        let e ← mkAuxDefinitionFor auxName proj
+        trace[aesop] m!"{e}"
+        return auxName
+    else
+      return declName
+
 meta initialize registerBuiltinAttribute {
     name := `aesop_contractive_attr
     descr := "Adds a given declaration to the ruleset for the `aesop_contractive` tactic."
     applicationTime := .afterCompilation
-    add := fun src stx kind ↦ withRef stx do Aesop.runTermElabMAsCoreM do
+    add := fun declName stx kind ↦ withRef stx do Aesop.runTermElabMAsCoreM do
+      let declName ← auxIfIsNonExpansiveDecl declName
       let config ← elabConfig stx
-      let decl ← getConstInfo src
-      let rules ← config.rules.flatMapM (·.buildAdditionalGlobalRules src)
+      let rules ← config.rules.flatMapM (·.buildAdditionalGlobalRules declName)
       for (rule, rsNames) in rules do
         for rsName in rsNames do
           addGlobalRule rsName rule kind (checkNotExists := true)

From c4d8c8efaac2bf84fb11250a197cb85dd626896a Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Mon, 1 Jun 2026 14:29:16 +0200
Subject: [PATCH 08/10] clean up annotations and fully solve the examples

---
 Iris/Iris/Algebra/OFE.lean             | 14 +++-----
 Iris/Iris/BI/BI.lean                   |  2 --
 Iris/Iris/BI/Updates.lean              |  7 ++--
 Iris/Iris/ProgramLogic/WeakestPre.lean | 44 +++++++++++++++++---------
 Iris/Iris/Std/AesopContractive.lean    | 36 +++++++++++----------
 5 files changed, 59 insertions(+), 44 deletions(-)

diff --git a/Iris/Iris/Algebra/OFE.lean b/Iris/Iris/Algebra/OFE.lean
index f9828d40c..f98cf6ddb 100644
--- a/Iris/Iris/Algebra/OFE.lean
+++ b/Iris/Iris/Algebra/OFE.lean
@@ -11,8 +11,6 @@ public meta import Iris.Std.AesopContractive
 
 namespace Iris
 
-attribute [aesop_contractive unsafe 10% cases] Option
-
 /-- Ordered family of equivalences -/
 @[rocq_alias ofe]
 class OFE (α : Type _) where
@@ -153,29 +151,27 @@ theorem distLater_soundness [OFE α] {x y : α} (H : ∀ n, DistLater n x y →
 class Contractive [OFE α] [OFE β] (f : α → β) where
   distLater_dist : DistLater n x y → f x ≡{n}≡ f y
 
-attribute [aesop_contractive safe apply] Contractive.distLater_dist
-
-@[simp, aesop_contractive safe apply, rocq_alias contractive_0] theorem Contractive.zero [OFE α] [OFE β] (f : α → β)
+@[simp, rocq_alias contractive_0] theorem Contractive.zero [OFE α] [OFE β] (f : α → β)
     [Contractive f] {x y} : f x ≡{0}≡ f y :=
   Contractive.distLater_dist distLater_zero
 
-@[aesop_contractive safe apply, rocq_alias contractive_S]
+@[rocq_alias contractive_S]
 theorem Contractive.succ [OFE α] [OFE β] (f : α → β) [Contractive f] {n x y}
     (h : x ≡{n}≡ y) : f x ≡{n.succ}≡ f y :=
   Contractive.distLater_dist (distLater_succ.2 h)
 
 /-- A contractive function is non-expansive. -/
-@[aesop_contractive safe apply, rocq_alias contractive_ne]
+@[rocq_alias contractive_ne]
 instance ne_of_contractive [OFE α] [OFE β] (f : α → β) [Contractive f] : NonExpansive f where
   ne := fun _ _ _ h => Contractive.distLater_dist (Dist.distLater h)
 
 /-- A contractive function preserves equivalence. -/
-@[aesop_contractive safe apply, rocq_alias contractive_proper]
+@[rocq_alias contractive_proper]
 theorem Contractive.eqv [OFE α] [OFE β] (f : α → β) [Contractive f] ⦃x y : α⦄ (h : x ≡ y) :
     f x ≡ f y := NonExpansive.eqv h
 
 /-- Constant functions are contractive. -/
-@[aesop_contractive safe apply, rocq_alias const_contractive]
+@[rocq_alias const_contractive]
 instance [OFE α] [OFE β] {x : β} : Contractive (fun _ : α => x) where
   distLater_dist := fun _ => Dist.rfl
 
diff --git a/Iris/Iris/BI/BI.lean b/Iris/Iris/BI/BI.lean
index fc55d20f1..fd33d508b 100644
--- a/Iris/Iris/BI/BI.lean
+++ b/Iris/Iris/BI/BI.lean
@@ -85,8 +85,6 @@ class BI (PROP : Type _) extends COFE PROP, BI.BIBase PROP where
 namespace BI
 
 attribute [instance] BI.entails_preorder
-attribute [aesop_contractive safe apply] and_ne or_ne imp_ne sForall_ne sExists_ne sep_ne wand_ne persistently_ne
-attribute [aesop_contractive unsafe 90% apply] later_ne
 
 theorem BIBase.Entails.trans [BI PROP] {P Q R : PROP} (h1 : P ⊢ Q) (h2 : Q ⊢ R) : P ⊢ R :=
   Transitive.trans h1 h2
diff --git a/Iris/Iris/BI/Updates.lean b/Iris/Iris/BI/Updates.lean
index 13a6c9211..e42b11805 100644
--- a/Iris/Iris/BI/Updates.lean
+++ b/Iris/Iris/BI/Updates.lean
@@ -160,6 +160,8 @@ class BIUpdate (PROP : Type _) [BI PROP] extends BUpd PROP where
   trans {P : PROP} : |==> |==> P ⊢ |==> P
   frame_r {P R : PROP} : (|==> P) ∗ R ⊢ |==> (P ∗ R)
 
+attribute [instance] BIUpdate.bupd_ne
+
 class BIFUpdate (PROP : Type _) [BI PROP] extends FUpd PROP where
   [ne {E1 E2 : CoPset} : OFE.NonExpansive (iprop(|={E1,E2}=> · : PROP))]
   subset {E1 E2 : CoPset} : E2 ⊆ E1 → ⊢ |={E1,E2}=> |={E2,E1}=> (emp : PROP)
@@ -170,7 +172,7 @@ class BIFUpdate (PROP : Type _) [BI PROP] extends FUpd PROP where
     E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ⊢ |={E1 ∪ Ef,E2 ∪ Ef}=> P
   frame_r {E1 E2 : CoPset} {P R : PROP} : (|={E1,E2}=> P) ∗ R ⊢ |={E1,E2}=> P ∗ R
 
-attribute [aesop_contractive safe apply] BIFUpdate.ne
+attribute [instance] BIFUpdate.ne
 
 class BIUpdateFUpdate (PROP : Type _) [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] where
   fupd_of_bupd {P : PROP} {E : CoPset} : (|==> P) ⊢ |={E}=> P
@@ -409,7 +411,8 @@ theorem step_fupdN_contractive {E1 E2 : CoPset} {n : Nat} [ι : BILaterContracti
     | zero => exact ne.ne (ι.distLater_dist (ne.ne <| xy_i · ·))
     | succ n IH => exact ne.ne (later_ne.ne (ne.ne IH))
 
-@[aesop_contractive safe apply]
+-- unsafe since it can make contractive goals unprovable if n > 0
+-- @[aesop_contractive unsafe 90% apply]
 theorem step_fupdN_ne {E1 E2 : CoPset} {n : Nat} :
     OFE.NonExpansive (iprop(|={E1}[E2]▷=>^[n] · : PROP)) where
   ne {i x y} xy_i := by
diff --git a/Iris/Iris/ProgramLogic/WeakestPre.lean b/Iris/Iris/ProgramLogic/WeakestPre.lean
index d18de15bc..cbc981ce3 100644
--- a/Iris/Iris/ProgramLogic/WeakestPre.lean
+++ b/Iris/Iris/ProgramLogic/WeakestPre.lean
@@ -65,7 +65,7 @@ abbrev Stuckness.MaybeReducible : Stuckness → Expr × State → Prop
 | .NotStuck, (e₁, σ₁) => PrimStep.Reducible (e₁, σ₁)
 | _, _ => True
 
-@[rocq_alias wp_pre, aesop_contractive safe unfold]
+@[rocq_alias wp_pre]
 def wp.pre (s : Stuckness) (wp : CoPset -> Expr -> (Val -> IProp GF) -> IProp GF) (E : CoPset)
     (e₁ : Expr) (Φ : Val -> IProp GF) : IProp GF :=
   match toVal e₁ with
@@ -78,13 +78,25 @@ def wp.pre (s : Stuckness) (wp : CoPset -> Expr -> (Val -> IProp GF) -> IProp GF
       stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗
       wp E e₂ Φ ∗ [∗list] e' ∈ eₜ, wp ⊤ e' ι.forkPost)
 
-@[rocq_alias wp_pre_contractive]
+open BI
+
+attribute [aesop_contractive safe apply] wand_ne sep_ne BIFUpdate.ne step_fupdN_contractive BigSepL.bigSepL_dist
+-- the following makes aesop_contractive quite slow and does not allow prioritization of Contractive instances over NonExpansive instances
+-- attribute [aesop_contractive safe apply] OFE.NonExpansive.ne OFE.NonExpansive₂.ne
+attribute [aesop_contractive safe forward (immediate := [h])] OFE.Dist.le
+attribute [aesop_contractive simp] Nat.le_iff_lt_or_eq
+
+-- time: 445ms
+#time @[rocq_alias wp_pre_contractive, aesop_contractive safe apply]
 instance wp.pre.contractive s : OFE.Contractive (wp.pre s (ι := ι)) where
   distLater_dist := by
-    intros n wp wp' Hwp E e₁ Φ
+    intros; unfold pre; intros _ _ _;
     aesop_contractive
-    · exact Hwp _ ‹_› _ _ _
-    · exact BI.BigSepL.bigSepL_dist <| fun _ => Hwp _ ‹_› _ _ _
+    -- set_option trace.aesop true in
+    -- aesop (config := { introsTransparency? := none, warnOnNonterminal := false })
+            -- (rule_sets := [aesop_contractive]) (erase Aesop.BuiltinRules.rfl)
+    -- · exact Hwp _ ‹_› _ _ _
+    -- · exact BI.BigSepL.bigSepL_dist <| fun _ => Hwp _ ‹_› _ _ _
 
 @[rocq_alias wp_def]
 instance wp.def : Wp (IProp GF) (Expr) (Val) Stuckness where
@@ -101,30 +113,32 @@ theorem wp_unfold {s E} {e : Expr} {Φ : Val → IProp GF} :
     WP e @ s ; E {{ Φ }} ⊣⊢ wp.pre s (Wp.wp (PROP := IProp GF) s) E e Φ :=
   BI.equiv_iff.1 <| fixpoint_unfold (f := (wp.pre s).toContractiveHom) E e Φ
 
-@[rocq_alias wp_ne]
+-- time: 648ms
+#time @[rocq_alias wp_ne, aesop_contractive safe apply]
 instance wp_ne {s : Stuckness} {E} {e : Expr} :
     OFE.NonExpansive (Wp.wp (PROP := IProp GF) s E e) where
   ne {n Φ₁ Φ₂} HΦ := by
     induction n using Nat.strongRecOn generalizing e E Φ₁ Φ₂ with | ind n IH =>
     simp only [IProp.ext wp_unfold]
     dsimp only [wp.pre]
-    cases toVal e
-    case some v =>
-      exact BIFUpdate.ne.ne <| HΦ v
-    case none =>
-      aesop_contractive
-      exact IH m ‹_›  <| OFE.dist_lt HΦ ‹_›
+    aesop_contractive
+    -- · aesop_contractive
+    -- · apply IH
+      -- · aesop_contractive
+      -- · apply fwd; aesop_contractive
 
 #rocq_ignore wp_proper "Derivable using NonExpansive.eqv"
 
-@[rocq_alias wp_contractive]
+-- time: 393ms
+#time @[rocq_alias wp_contractive]
 instance wp_contractive (s : Stuckness) E (e : Expr) (h : toVal e = none) :
     OFE.Contractive (Wp.wp (PROP := IProp GF) s E e) where
   distLater_dist {n Φ₁ Φ₂} HΦ := by
     simp only [IProp.ext wp_unfold]
+    unfold wp.pre
     aesop_contractive
-    refine wp_ne.ne ?_
-    exact HΦ _ ‹_›
+    -- refine wp_ne.ne ?_
+    -- exact HΦ _ ‹_›
 
 @[rocq_alias wp_value_fupd']
 theorem wp_value_fupd' {s : Stuckness} {E} {Φ : Val → IProp GF} {v : Val} :
diff --git a/Iris/Iris/Std/AesopContractive.lean b/Iris/Iris/Std/AesopContractive.lean
index 4ea7c741b..54c1fe8a6 100644
--- a/Iris/Iris/Std/AesopContractive.lean
+++ b/Iris/Iris/Std/AesopContractive.lean
@@ -8,10 +8,10 @@ declare_aesop_rule_sets [aesop_contractive]
 
 macro (name := aesop_cat) "aesop_contractive" c:Aesop.tactic_clause* : tactic =>
 `(tactic|
-  aesop $c* (config := { introsTransparency? := some .none, warnOnNonterminal := false })
+  aesop $c* (config := { warnOnNonterminal := true })
             (rule_sets := [$(Lean.mkIdent `aesop_contractive):ident]) (erase Aesop.BuiltinRules.rfl))
 
-attribute [simp] Nat.repeat
+-- attribute [simp] Nat.repeat
 
 syntax (name := aesop_contractive_attr) "aesop_contractive " Aesop.attr_rules : attr
 
@@ -33,20 +33,24 @@ meta def elabConfig (stx : Syntax) : TermElabM AttrConfig :=
 
 meta def auxIfIsNonExpansiveDecl (declName : Name) : TermElabM Name := do
   let decl ← getConstInfo declName
-  forallTelescope decl.type fun xs ty => ty.withApp fun fn _ => do
-    if let .const fnName _ := fn then
-      unless fnName = `Iris.OFE.NonExpansive || fnName = `Iris.OFE.NonExpansive₂ do
-        return declName
-      let declLvls := decl.levelParams.map Level.param
-      let declWithArgs := mkAppN (mkConst declName declLvls) xs
-      let proj ←  mkProjection declWithArgs `ne
-      withDeclNameForAuxNaming declName do
-        let auxName ← mkAuxDeclName
-        let e ← mkAuxDefinitionFor auxName proj
-        trace[aesop] m!"{e}"
-        return auxName
-    else
-      return declName
+  forallTelescope decl.type fun xs ty => do
+    let .const fnName _ := ty.getAppFn | return declName
+    let projName ←
+      if fnName == `Iris.OFE.NonExpansive ||
+         fnName == `Iris.OFE.NonExpansive₂ then
+        pure `ne
+      else if fnName == `Iris.OFE.Contractive then
+        pure `distLater_dist
+      else
+        do return declName
+    let declLvls := decl.levelParams.map Level.param
+    let declWithArgs := mkAppN (mkConst declName declLvls) xs
+    let proj ←  mkProjection declWithArgs projName
+    withDeclNameForAuxNaming declName do
+      let auxName ← mkAuxDeclName
+      let e ← mkAuxDefinitionFor auxName proj
+      trace[aesop] m!"{e}"
+      return auxName
 
 meta initialize registerBuiltinAttribute {
     name := `aesop_contractive_attr

From 0445fdad9b080b249ebc21f0119b9ee9d3cf32ac Mon Sep 17 00:00:00 2001
From: arthur-adjedj <arthur.adjedj@gmail.com>
Date: Mon, 1 Jun 2026 16:17:40 +0200
Subject: [PATCH 09/10] perf: turn off `useDefaultSimpSet`

---
 Iris/Iris/Algebra/OFE.lean             | 2 +-
 Iris/Iris/ProgramLogic/WeakestPre.lean | 6 +++---
 Iris/Iris/Std/AesopContractive.lean    | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/Iris/Iris/Algebra/OFE.lean b/Iris/Iris/Algebra/OFE.lean
index f98cf6ddb..9ac34da65 100644
--- a/Iris/Iris/Algebra/OFE.lean
+++ b/Iris/Iris/Algebra/OFE.lean
@@ -43,7 +43,7 @@ theorem Dist.le [OFE α] {m n} {x y : α} (h : x ≡{n}≡ y) (h' : m ≤ n) : x
 #rocq_ignore dist_le' "Use Dist.le"
 #rocq_ignore dist_S "Subsumed by `Dist.lt`/`Dist.le`."
 
-@[simp, refl] theorem Dist.rfl [OFE α] {n} {x : α} : x ≡{n}≡ x := dist_eqv.1 _
+@[simp, aesop_contractive simp, refl] theorem Dist.rfl [OFE α] {n} {x : α} : x ≡{n}≡ x := dist_eqv.1 _
 @[symm] theorem Dist.symm [OFE α] {n} {x : α} : x ≡{n}≡ y → y ≡{n}≡ x := dist_eqv.2
 theorem Dist.trans [OFE α] {n} {x : α} : x ≡{n}≡ y → y ≡{n}≡ z → x ≡{n}≡ z := dist_eqv.3
 theorem Dist.of_eq [OFE α] {x y : α} : x = y → x ≡{n}≡ y := (· ▸ .rfl)
diff --git a/Iris/Iris/ProgramLogic/WeakestPre.lean b/Iris/Iris/ProgramLogic/WeakestPre.lean
index cbc981ce3..7702aa988 100644
--- a/Iris/Iris/ProgramLogic/WeakestPre.lean
+++ b/Iris/Iris/ProgramLogic/WeakestPre.lean
@@ -86,7 +86,7 @@ attribute [aesop_contractive safe apply] wand_ne sep_ne BIFUpdate.ne step_fupdN_
 attribute [aesop_contractive safe forward (immediate := [h])] OFE.Dist.le
 attribute [aesop_contractive simp] Nat.le_iff_lt_or_eq
 
--- time: 445ms
+-- time: was 580ms, is 350ms now
 #time @[rocq_alias wp_pre_contractive, aesop_contractive safe apply]
 instance wp.pre.contractive s : OFE.Contractive (wp.pre s (ι := ι)) where
   distLater_dist := by
@@ -113,7 +113,7 @@ theorem wp_unfold {s E} {e : Expr} {Φ : Val → IProp GF} :
     WP e @ s ; E {{ Φ }} ⊣⊢ wp.pre s (Wp.wp (PROP := IProp GF) s) E e Φ :=
   BI.equiv_iff.1 <| fixpoint_unfold (f := (wp.pre s).toContractiveHom) E e Φ
 
--- time: 648ms
+-- time: was 780ms, is 540ms now
 #time @[rocq_alias wp_ne, aesop_contractive safe apply]
 instance wp_ne {s : Stuckness} {E} {e : Expr} :
     OFE.NonExpansive (Wp.wp (PROP := IProp GF) s E e) where
@@ -129,7 +129,7 @@ instance wp_ne {s : Stuckness} {E} {e : Expr} :
 
 #rocq_ignore wp_proper "Derivable using NonExpansive.eqv"
 
--- time: 393ms
+-- time: was 480ms, is 260ms now
 #time @[rocq_alias wp_contractive]
 instance wp_contractive (s : Stuckness) E (e : Expr) (h : toVal e = none) :
     OFE.Contractive (Wp.wp (PROP := IProp GF) s E e) where
diff --git a/Iris/Iris/Std/AesopContractive.lean b/Iris/Iris/Std/AesopContractive.lean
index 54c1fe8a6..25092becb 100644
--- a/Iris/Iris/Std/AesopContractive.lean
+++ b/Iris/Iris/Std/AesopContractive.lean
@@ -8,7 +8,7 @@ declare_aesop_rule_sets [aesop_contractive]
 
 macro (name := aesop_cat) "aesop_contractive" c:Aesop.tactic_clause* : tactic =>
 `(tactic|
-  aesop $c* (config := { warnOnNonterminal := true })
+  aesop $c* (config := { warnOnNonterminal := true, useDefaultSimpSet := false})
             (rule_sets := [$(Lean.mkIdent `aesop_contractive):ident]) (erase Aesop.BuiltinRules.rfl))
 
 -- attribute [simp] Nat.repeat

From 20fcf8f029e080b220042abaa5704afc3d173f9a Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Mon, 1 Jun 2026 17:35:29 +0200
Subject: [PATCH 10/10] more aesop_contractive annotation

---
 Iris/Iris/Algebra/OFE.lean             | 2 +-
 Iris/Iris/ProgramLogic/WeakestPre.lean | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/Iris/Iris/Algebra/OFE.lean b/Iris/Iris/Algebra/OFE.lean
index 9ac34da65..f98cf6ddb 100644
--- a/Iris/Iris/Algebra/OFE.lean
+++ b/Iris/Iris/Algebra/OFE.lean
@@ -43,7 +43,7 @@ theorem Dist.le [OFE α] {m n} {x y : α} (h : x ≡{n}≡ y) (h' : m ≤ n) : x
 #rocq_ignore dist_le' "Use Dist.le"
 #rocq_ignore dist_S "Subsumed by `Dist.lt`/`Dist.le`."
 
-@[simp, aesop_contractive simp, refl] theorem Dist.rfl [OFE α] {n} {x : α} : x ≡{n}≡ x := dist_eqv.1 _
+@[simp, refl] theorem Dist.rfl [OFE α] {n} {x : α} : x ≡{n}≡ x := dist_eqv.1 _
 @[symm] theorem Dist.symm [OFE α] {n} {x : α} : x ≡{n}≡ y → y ≡{n}≡ x := dist_eqv.2
 theorem Dist.trans [OFE α] {n} {x : α} : x ≡{n}≡ y → y ≡{n}≡ z → x ≡{n}≡ z := dist_eqv.3
 theorem Dist.of_eq [OFE α] {x y : α} : x = y → x ≡{n}≡ y := (· ▸ .rfl)
diff --git a/Iris/Iris/ProgramLogic/WeakestPre.lean b/Iris/Iris/ProgramLogic/WeakestPre.lean
index 7702aa988..a20eca06a 100644
--- a/Iris/Iris/ProgramLogic/WeakestPre.lean
+++ b/Iris/Iris/ProgramLogic/WeakestPre.lean
@@ -85,6 +85,7 @@ attribute [aesop_contractive safe apply] wand_ne sep_ne BIFUpdate.ne step_fupdN_
 -- attribute [aesop_contractive safe apply] OFE.NonExpansive.ne OFE.NonExpansive₂.ne
 attribute [aesop_contractive safe forward (immediate := [h])] OFE.Dist.le
 attribute [aesop_contractive simp] Nat.le_iff_lt_or_eq
+attribute [aesop_contractive simp] OFE.Dist.rfl
 
 -- time: was 580ms, is 350ms now
 #time @[rocq_alias wp_pre_contractive, aesop_contractive safe apply]