diff --git a/program_logic/hoare.v b/program_logic/hoare.v index 912f193a0453b2acdb67303a0f4ca6af0b6fb3b9..3b978b9f319901d2c8dacc4c2584a28d940aa8d6 100644 --- a/program_logic/hoare.v +++ b/program_logic/hoare.v @@ -3,7 +3,7 @@ From iris.proofmode Require Import tactics. Definition ht `{irisG Λ Σ} (E : coPset) (P : iProp Σ) (e : expr Λ) (Φ : val Λ → iProp Σ) : iProp Σ := - (□ (P → WP e @ E {{ Φ }}))%I. + (□ (P -★ WP e @ E {{ Φ }}))%I. Instance: Params (@ht) 4. Notation "{{ P } } e @ E {{ Φ } }" := (ht E P e%E Φ) @@ -47,7 +47,7 @@ Global Instance ht_proper E : Proof. solve_proper. Qed. Lemma ht_mono E P P' Φ Φ' e : (P ⊢ P') → (∀ v, Φ' v ⊢ Φ v) → {{ P' }} e @ E {{ Φ' }} ⊢ {{ P }} e @ E {{ Φ }}. -Proof. by intros; apply always_mono, impl_mono, wp_mono. Qed. +Proof. by intros; apply always_mono, wand_mono, wp_mono. Qed. Global Instance ht_mono' E : Proper (flip (⊢) ==> eq ==> pointwise_relation _ (⊢) ==> (⊢)) (ht E). Proof. solve_proper. Qed. diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v index 13a286abb4d8a7a7f021bef08356d73bd79ed810..e975a02de4f7892e278086f4823a9af0cdda1335 100644 --- a/program_logic/viewshifts.v +++ b/program_logic/viewshifts.v @@ -2,7 +2,7 @@ From iris.program_logic Require Export invariants. From iris.proofmode Require Import tactics. Definition vs `{irisG Λ Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ := - (□ (P → |={E1,E2}=> Q))%I. + (□ (P -★ |={E1,E2}=> Q))%I. Arguments vs {_ _ _} _ _ _%I _%I. Instance: Params (@vs) 5.