Commit 155a869b authored by Ralf Jung's avatar Ralf Jung

more concise lambda lemmas

parent b2527d69
......@@ -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.
......
......@@ -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}.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment