From a14ba8957fd18ab8696cd24cc42617a31d35ce02 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Fri, 16 Jul 2021 15:16:16 +0200 Subject: [PATCH] =?UTF-8?q?State=20`bi=5Fmono=5Fpred`=20using=20`=E2=96=A1?= =?UTF-8?q?`/`-=E2=88=97`=20instead=20of=20`<pers>`/`=E2=86=92`.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- iris/bi/lib/fixpoint.v | 2 +- iris/program_logic/total_adequacy.v | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/iris/bi/lib/fixpoint.v b/iris/bi/lib/fixpoint.v index 52d8fb0ee..9b242866f 100644 --- a/iris/bi/lib/fixpoint.v +++ b/iris/bi/lib/fixpoint.v @@ -6,7 +6,7 @@ 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 Φ Ψ : ⊢ <pers> (∀ x, Φ x -∗ Ψ x) → ∀ x, F Φ x -∗ F Ψ x; + bi_mono_pred Φ Ψ : □ (∀ x, Φ x -∗ Ψ x) -∗ ∀ x, F Φ x -∗ F Ψ x; bi_mono_pred_ne Φ : NonExpansive Φ → NonExpansive (F Φ) }. Global Arguments bi_mono_pred {_ _ _ _} _ _. diff --git a/iris/program_logic/total_adequacy.v b/iris/program_logic/total_adequacy.v index ed100b2d8..288e51380 100644 --- a/iris/program_logic/total_adequacy.v +++ b/iris/program_logic/total_adequacy.v @@ -16,8 +16,8 @@ Definition twptp_pre (twptp : list (expr Λ) → iProp Σ) ∃ nt', ⌜κ = []⌠∗ state_interp σ2 (S ns) κs nt' ∗ twptp t2. Lemma twptp_pre_mono (twptp1 twptp2 : list (expr Λ) → iProp Σ) : - ⊢ <pers> (∀ t, twptp1 t -∗ twptp2 t) → - ∀ t, twptp_pre twptp1 t -∗ twptp_pre twptp2 t. + □ (∀ t, twptp1 t -∗ twptp2 t) -∗ + ∀ t, twptp_pre twptp1 t -∗ twptp_pre twptp2 t. Proof. iIntros "#H"; iIntros (t) "Hwp". rewrite /twptp_pre. iIntros (t2 σ1 ns κ κs σ2 nt1) "Hstep Hσ". -- GitLab