From 0a2f1938e23908a9e36c081d8944e5f71ce4f0e0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 7 Oct 2019 12:00:45 +0200
Subject: [PATCH] Prove that non-value WP is contractive.

---
 theories/program_logic/weakestpre.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 4cb5d9161..6d3a96670 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -79,6 +79,13 @@ Global Instance wp_proper s E e :
 Proof.
   by intros Φ Φ' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist.
 Qed.
+Lemma wp_contractive s E e n :
+  to_val e = None →
+  Proper (pointwise_relation _ (dist_later n) ==> dist n) (wp (PROP:=iProp Σ) s E e).
+Proof.
+  intros He Φ Ψ HΦ. rewrite !wp_unfold /wp_pre He.
+  by repeat (f_contractive || f_equiv).
+Qed.
 
 Lemma wp_value' s E Φ v : Φ v ⊢ WP of_val v @ s; E {{ Φ }}.
 Proof. iIntros "HΦ". rewrite wp_unfold /wp_pre to_of_val. auto. Qed.
-- 
GitLab