From 155a869bf6646282b842b452c542403b9ad5aa0e Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Wed, 27 Jan 2016 16:45:23 +0100
Subject: [PATCH] more concise lambda lemmas

---
 barrier/lifting.v | 13 +++++--------
 barrier/tests.v   |  4 ++--
 2 files changed, 7 insertions(+), 10 deletions(-)

diff --git a/barrier/lifting.v b/barrier/lifting.v
index 0e0dd24fc..6f831b50d 100644
--- a/barrier/lifting.v
+++ b/barrier/lifting.v
@@ -164,11 +164,9 @@ Proof.
     rewrite right_id. done.
 Qed.
 
-Lemma wp_rec' E e v P Q :
-  P ⊑ wp (Σ:=Σ) E (e.[Rec e, v2e v /]) Q →
-  ▷P ⊑ wp (Σ:=Σ) E (App (Rec e) (v2e v)) Q.
+Lemma wp_rec' E e v Q :
+  ▷wp (Σ:=Σ) E (e.[Rec e, v2e v /]) Q ⊑ wp (Σ:=Σ) E (App (Rec e) (v2e v)) Q.
 Proof.
-  intros HP.
   etransitivity; last eapply wp_lift_pure_step with
     (φ := λ e', e' = e.[Rec e, v2e v /]); last first.
   - intros ? ? ? ? Hstep. inversion_clear Hstep. done.
@@ -178,11 +176,10 @@ Proof.
     apply const_elim_l=>->. done.
 Qed.
 
-Lemma wp_lam E e v P Q :
-  P ⊑ wp (Σ:=Σ) E (e.[v2e v/]) Q →
-  ▷P ⊑ wp (Σ:=Σ) E (App (Lam e) (v2e v)) Q.
+Lemma wp_lam E e v Q :
+  ▷wp (Σ:=Σ) E (e.[v2e v/]) Q ⊑ wp (Σ:=Σ) E (App (Lam e) (v2e v)) Q.
 Proof.
-  intros HP. rewrite -wp_rec'; first (intros; apply later_mono; eassumption).
+  rewrite -wp_rec'.
   (* RJ: This pulls in functional extensionality. If that bothers us, we have
      to talk to the Autosubst guys. *)
   by asimpl.
diff --git a/barrier/tests.v b/barrier/tests.v
index ee8aeefff..2981f3235 100644
--- a/barrier/tests.v
+++ b/barrier/tests.v
@@ -40,7 +40,7 @@ Module LiftingTests.
     rewrite -(wp_bind _ _ (LetCtx EmptyCtx e2)). rewrite -wp_mono.
     { eapply wp_alloc; done. }
     move=>v; apply exist_elim=>l. apply const_elim_l; move=>[-> _] {v}.
-    rewrite (later_intro (ownP _)); apply wp_lam. asimpl.
+    rewrite -wp_lam -later_intro. asimpl.
     rewrite -(wp_bind _ _ (SeqCtx (StoreRCtx (LocV _)
                                    (PlusLCtx EmptyCtx _)) (Load (Loc _)))).
     rewrite -wp_mono.
@@ -52,7 +52,7 @@ Module LiftingTests.
     rewrite -wp_mono.
     { eapply wp_store; first reflexivity. apply: lookup_insert. }
     move=>v; apply const_elim_l; move=>-> {v}.
-    rewrite (later_intro (ownP _)); apply wp_lam. asimpl.
+    rewrite -wp_lam -later_intro. asimpl.
     rewrite -wp_mono.
     { eapply wp_load. apply: lookup_insert. }
     move=>v; apply const_elim_l; move=>-> {v}.
-- 
GitLab