derived.v 2.04 KB
 Ralf Jung committed Feb 11, 2016 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 ``````Require Export heap_lang.lifting. Import uPred. (** Define some derived forms, and derived lemmas about them. *) Notation Lam x e := (Rec "" x e). Notation Let x e1 e2 := (App (Lam x e2) e1). Notation Seq e1 e2 := (Let "" e1 e2). Notation LamV x e := (RecV "" x e). Notation LetCtx x e2 := (AppRCtx (LamV x e2)). Notation SeqCtx e2 := (LetCtx "" e2). Section derived. Context {Σ : iFunctor}. Implicit Types P : iProp heap_lang Σ. Implicit Types Q : val → iProp heap_lang Σ. (** Proof rules for the sugar *) Lemma wp_lam E x ef e v Q : to_val e = Some v → ▷ wp E (gsubst ef x e) Q ⊑ wp E (App (Lam x ef) e) Q. Proof. intros <-%of_to_val; rewrite -wp_rec ?to_of_val //. by rewrite (gsubst_correct _ _ (RecV _ _ _)) subst_empty. Qed. Lemma wp_let E x e1 e2 v Q : to_val e1 = Some v → ▷ wp E (gsubst e2 x e1) Q ⊑ wp E (Let x e1 e2) Q. Proof. apply wp_lam. Qed. Lemma wp_seq E e1 e2 Q : wp E e1 (λ _, ▷ wp E e2 Q) ⊑ wp E (Seq e1 e2) Q. Proof. rewrite -(wp_bind [LetCtx "" e2]). apply wp_mono=>v. by rewrite -wp_let //= ?gsubst_correct ?subst_empty ?to_of_val. Qed. `````` Ralf Jung committed Feb 11, 2016 35 ``````Lemma wp_le E (n1 n2 : Z) P Q : `````` Ralf Jung committed Feb 11, 2016 36 37 `````` (n1 ≤ n2 → P ⊑ ▷ Q (LitV \$ LitBool true)) → (n2 < n1 → P ⊑ ▷ Q (LitV \$ LitBool false)) → `````` Ralf Jung committed Feb 11, 2016 38 `````` P ⊑ wp E (BinOp LeOp (Lit \$ LitInt n1) (Lit \$ LitInt n2)) Q. `````` Ralf Jung committed Feb 11, 2016 39 40 41 42 43 ``````Proof. intros. rewrite -wp_bin_op //; []. destruct (bool_decide_reflect (n1 ≤ n2)); by eauto with omega. Qed. `````` Ralf Jung committed Feb 11, 2016 44 ``````Lemma wp_lt E (n1 n2 : Z) P Q : `````` Ralf Jung committed Feb 11, 2016 45 46 `````` (n1 < n2 → P ⊑ ▷ Q (LitV \$ LitBool true)) → (n2 ≤ n1 → P ⊑ ▷ Q (LitV \$ LitBool false)) → `````` Ralf Jung committed Feb 11, 2016 47 `````` P ⊑ wp E (BinOp LtOp (Lit \$ LitInt n1) (Lit \$ LitInt n2)) Q. `````` Ralf Jung committed Feb 11, 2016 48 49 50 51 52 ``````Proof. intros. rewrite -wp_bin_op //; []. destruct (bool_decide_reflect (n1 < n2)); by eauto with omega. Qed. `````` Ralf Jung committed Feb 11, 2016 53 ``````Lemma wp_eq E (n1 n2 : Z) P Q : `````` Ralf Jung committed Feb 11, 2016 54 55 `````` (n1 = n2 → P ⊑ ▷ Q (LitV \$ LitBool true)) → (n1 ≠ n2 → P ⊑ ▷ Q (LitV \$ LitBool false)) → `````` Ralf Jung committed Feb 11, 2016 56 `````` P ⊑ wp E (BinOp EqOp (Lit \$ LitInt n1) (Lit \$ LitInt n2)) Q. `````` Ralf Jung committed Feb 11, 2016 57 58 59 60 61 62 ``````Proof. intros. rewrite -wp_bin_op //; []. destruct (bool_decide_reflect (n1 = n2)); by eauto with omega. Qed. End derived.``````