Commit 0a593561 authored by Ralf Jung's avatar Ralf Jung

add a derived 'skip' to heap_lang

parent 960ac942
...@@ -8,6 +8,7 @@ Notation Seq e1 e2 := (Let "" e1 e2). ...@@ -8,6 +8,7 @@ Notation Seq e1 e2 := (Let "" e1 e2).
Notation LamV x e := (RecV "" x e). Notation LamV x e := (RecV "" x e).
Notation LetCtx x e2 := (AppRCtx (LamV x e2)). Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
Notation SeqCtx e2 := (LetCtx "" e2). Notation SeqCtx e2 := (LetCtx "" e2).
Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
Section derived. Section derived.
Context {Σ : iFunctor}. Context {Σ : iFunctor}.
...@@ -29,6 +30,9 @@ Proof. ...@@ -29,6 +30,9 @@ Proof.
by rewrite -wp_let' //= ?to_of_val ?subst_empty. by rewrite -wp_let' //= ?to_of_val ?subst_empty.
Qed. Qed.
Lemma wp_skip E Q : (Q (LitV LitUnit)) wp E Skip Q.
Proof. rewrite -wp_seq -wp_value // -wp_value //. Qed.
Lemma wp_le E (n1 n2 : Z) P Q : Lemma wp_le E (n1 n2 : Z) P Q :
(n1 n2 P Q (LitV $ LitBool true)) (n1 n2 P Q (LitV $ LitBool true))
(n2 < n1 P Q (LitV $ LitBool false)) (n2 < n1 P Q (LitV $ LitBool false))
......
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