From c0e8dc2310321059c2fae8654a745113856a7957 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 21 Jul 2021 20:13:11 +0200
Subject: [PATCH] Strengthen `bi_mono_pred` to ensure that functions are
 non-expansive.

---
 iris/bi/lib/atomic.v                  |  2 +-
 iris/bi/lib/fixpoint.v                | 12 ++++++++----
 iris/bi/lib/relations.v               |  2 +-
 iris/program_logic/total_adequacy.v   |  2 +-
 iris/program_logic/total_weakestpre.v |  2 +-
 5 files changed, 12 insertions(+), 8 deletions(-)

diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index f67fc975c..e89a695e8 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -73,7 +73,7 @@ Section definition.
   Local Instance atomic_update_pre_mono : BiMonoPred atomic_update_pre.
   Proof.
     constructor.
-    - iIntros (P1 P2) "#HP12". iIntros ([]) "AU".
+    - iIntros (P1 P2 ??) "#HP12". iIntros ([]) "AU".
       iApply (make_laterable_intuitionistic_wand with "[] AU").
       iIntros "!> AA". iApply (atomic_acc_wand with "[HP12] AA").
       iSplit; last by eauto. iApply "HP12".
diff --git a/iris/bi/lib/fixpoint.v b/iris/bi/lib/fixpoint.v
index 32aafcc6f..45ca41fcb 100644
--- a/iris/bi/lib/fixpoint.v
+++ b/iris/bi/lib/fixpoint.v
@@ -6,7 +6,10 @@ Import bi.
 (** Least and greatest fixpoint of a monotone function, defined entirely inside
     the logic.  *)
 Class BiMonoPred {PROP : bi} {A : ofe} (F : (A → PROP) → (A → PROP)) := {
-  bi_mono_pred Φ Ψ : □ (∀ x, Φ x -∗ Ψ x) -∗ ∀ x, F Φ x -∗ F Ψ x;
+  bi_mono_pred Φ Ψ :
+    NonExpansive Φ →
+    NonExpansive Ψ →
+    □ (∀ x, Φ x -∗ Ψ x) -∗ ∀ x, F Φ x -∗ F Ψ x;
   bi_mono_pred_ne Φ : NonExpansive Φ → NonExpansive (F Φ)
 }.
 Global Arguments bi_mono_pred {_ _ _ _} _ _.
@@ -37,7 +40,7 @@ Section least.
   Lemma least_fixpoint_unfold_2 x : F (bi_least_fixpoint F) x ⊢ bi_least_fixpoint F x.
   Proof using Type*.
     rewrite /bi_least_fixpoint /=. iIntros "HF" (Φ) "#Hincl".
-    iApply "Hincl". iApply (bi_mono_pred _ Φ with "[#]"); last done.
+    iApply "Hincl". iApply (bi_mono_pred _ Φ with "[#] HF"); [solve_proper|].
     iIntros "!>" (y) "Hy". iApply ("Hy" with "[# //]").
   Qed.
 
@@ -45,7 +48,7 @@ Section least.
     bi_least_fixpoint F x ⊢ F (bi_least_fixpoint F) x.
   Proof using Type*.
     iIntros "HF". iApply ("HF" $! (OfeMor (F (bi_least_fixpoint F))) with "[#]").
-    iIntros "!>" (y) "Hy /=". iApply (bi_mono_pred with "[#]"); last done.
+    iIntros "!>" (y) "Hy /=". iApply (bi_mono_pred with "[#] Hy").
     iIntros "!>" (z) "?". by iApply least_fixpoint_unfold_2.
   Qed.
 
@@ -68,7 +71,8 @@ Section least.
     trans (∀ x, bi_least_fixpoint F x -∗ Φ x ∧ bi_least_fixpoint F x)%I.
     { iIntros "#HΦ". iApply (least_fixpoint_ind with "[]"); first solve_proper.
       iIntros "!>" (y) "H". iSplit; first by iApply "HΦ".
-      iApply least_fixpoint_unfold_2. iApply (bi_mono_pred with "[#] H").
+      iApply least_fixpoint_unfold_2.
+      iApply (bi_mono_pred with "[#] H"); [solve_proper|].
       by iIntros "!> * [_ ?]". }
     by setoid_rewrite and_elim_l.
   Qed.
diff --git a/iris/bi/lib/relations.v b/iris/bi/lib/relations.v
index 9d7a37635..a00a710d9 100644
--- a/iris/bi/lib/relations.v
+++ b/iris/bi/lib/relations.v
@@ -17,7 +17,7 @@ Global Instance bi_rtc_pre_mono `{!BiInternalEq PROP}
   BiMonoPred (bi_rtc_pre R x).
 Proof.
   constructor; [|solve_proper].
-  iIntros (rec1 rec2) "#H". iIntros (x1) "[Hrec | Hrec]".
+  iIntros (rec1 rec2 ??) "#H". iIntros (x1) "[Hrec | Hrec]".
   { by iLeft. }
   iRight.
   iDestruct "Hrec" as (x') "[HP Hrec]".
diff --git a/iris/program_logic/total_adequacy.v b/iris/program_logic/total_adequacy.v
index 288e51380..3070bdc5d 100644
--- a/iris/program_logic/total_adequacy.v
+++ b/iris/program_logic/total_adequacy.v
@@ -27,7 +27,7 @@ Qed.
 
 Local Instance twptp_pre_mono' : BiMonoPred twptp_pre.
 Proof.
-  constructor; first apply twptp_pre_mono.
+  constructor; first (intros ????; apply twptp_pre_mono).
   intros wp Hwp n t1 t2 ?%(discrete_iff _ _)%leibniz_equiv; solve_proper.
 Qed.
 
diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index d6152e97b..3b8c9d06c 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -50,7 +50,7 @@ Definition twp_pre' `{!irisGS Λ Σ} (s : stuckness) :
 Local Instance twp_pre_mono' `{!irisGS Λ Σ} s : BiMonoPred (twp_pre' s).
 Proof.
   constructor.
-  - iIntros (wp1 wp2) "#H"; iIntros ([[E e1] Φ]); iRevert (E e1 Φ).
+  - iIntros (wp1 wp2 ??) "#H"; iIntros ([[E e1] Φ]); iRevert (E e1 Φ).
     iApply twp_pre_mono. iIntros "!>" (E e Φ). iApply ("H" $! (E,e,Φ)).
   - intros wp Hwp n [[E1 e1] Φ1] [[E2 e2] Φ2]
       [[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=.
-- 
GitLab