From 794c6660f312ee1c4fd95ea11eeab22d6fbe85b9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 18 Oct 2016 23:25:06 +0200
Subject: [PATCH] Define hoare triple and view shift in terms of wand.

---
 program_logic/hoare.v      | 4 ++--
 program_logic/viewshifts.v | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index 912f193a0..3b978b9f3 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 13a286abb..e975a02de 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.
-- 
GitLab