From b2527d69bf97f166a9d345c86e28f10c32be0ab2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Wed, 27 Jan 2016 16:40:31 +0100
Subject: [PATCH] make Plus lemma more concise
---
barrier/lifting.v | 6 ++----
barrier/tests.v | 2 +-
2 files changed, 3 insertions(+), 5 deletions(-)
diff --git a/barrier/lifting.v b/barrier/lifting.v
index 43a1f3c3e..0e0dd24fc 100644
--- a/barrier/lifting.v
+++ b/barrier/lifting.v
@@ -188,11 +188,9 @@ Proof.
by asimpl.
Qed.
-Lemma wp_plus n1 n2 E P Q :
- P ⊑ Q (LitNatV (n1 + n2)) →
- ▷P ⊑ wp (Σ:=Σ) E (Plus (LitNat n1) (LitNat n2)) Q.
+Lemma wp_plus n1 n2 E Q :
+ ▷Q (LitNatV (n1 + n2)) ⊑ wp (Σ:=Σ) E (Plus (LitNat n1) (LitNat n2)) Q.
Proof.
- intros HP.
etransitivity; last eapply wp_lift_pure_step with
(φ := λ e', e' = LitNat (n1 + n2)); last first.
- intros ? ? ? ? Hstep. inversion_clear Hstep; done.
diff --git a/barrier/tests.v b/barrier/tests.v
index f00b22461..ee8aeefff 100644
--- a/barrier/tests.v
+++ b/barrier/tests.v
@@ -47,7 +47,7 @@ Module LiftingTests.
{ eapply wp_load. apply: lookup_insert. } (* RJ TODO: figure out why apply and eapply fail. *)
move=>v; apply const_elim_l; move=>-> {v}.
rewrite -(wp_bind _ _ (SeqCtx (StoreRCtx (LocV _) EmptyCtx) (Load (Loc _)))).
- rewrite (later_intro (ownP _)); apply wp_plus.
+ rewrite -wp_plus -later_intro.
rewrite -(wp_bind _ _ (SeqCtx EmptyCtx (Load (Loc _)))).
rewrite -wp_mono.
{ eapply wp_store; first reflexivity. apply: lookup_insert. }
--
GitLab