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