Commit b2527d69 authored by Ralf Jung's avatar Ralf Jung

make Plus lemma more concise

parent 9a2e4b47
...@@ -188,11 +188,9 @@ Proof. ...@@ -188,11 +188,9 @@ Proof.
by asimpl. by asimpl.
Qed. Qed.
Lemma wp_plus n1 n2 E P Q : Lemma wp_plus n1 n2 E Q :
P Q (LitNatV (n1 + n2)) Q (LitNatV (n1 + n2)) wp (Σ:=Σ) E (Plus (LitNat n1) (LitNat n2)) Q.
P wp (Σ:=Σ) E (Plus (LitNat n1) (LitNat n2)) Q.
Proof. Proof.
intros HP.
etransitivity; last eapply wp_lift_pure_step with etransitivity; last eapply wp_lift_pure_step with
(φ := λ e', e' = LitNat (n1 + n2)); last first. (φ := λ e', e' = LitNat (n1 + n2)); last first.
- intros ? ? ? ? Hstep. inversion_clear Hstep; done. - intros ? ? ? ? Hstep. inversion_clear Hstep; done.
......
...@@ -47,7 +47,7 @@ Module LiftingTests. ...@@ -47,7 +47,7 @@ Module LiftingTests.
{ eapply wp_load. apply: lookup_insert. } (* RJ TODO: figure out why apply and eapply fail. *) { eapply wp_load. apply: lookup_insert. } (* RJ TODO: figure out why apply and eapply fail. *)
move=>v; apply const_elim_l; move=>-> {v}. move=>v; apply const_elim_l; move=>-> {v}.
rewrite -(wp_bind _ _ (SeqCtx (StoreRCtx (LocV _) EmptyCtx) (Load (Loc _)))). 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_bind _ _ (SeqCtx EmptyCtx (Load (Loc _)))).
rewrite -wp_mono. rewrite -wp_mono.
{ eapply wp_store; first reflexivity. apply: lookup_insert. } { eapply wp_store; first reflexivity. apply: lookup_insert. }
......
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