derived.v 2.14 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 `````` Section derived. Context {Σ : iFunctor}. `````` Robbert Krebbers committed Feb 18, 2016 15 16 ``````Implicit Types P Q : iProp heap_lang Σ. Implicit Types Φ : val → iProp heap_lang Σ. `````` Ralf Jung committed Feb 11, 2016 17 18 `````` (** Proof rules for the sugar *) `````` Robbert Krebbers committed Feb 18, 2016 19 20 ``````Lemma wp_lam' E x ef e v Φ : to_val e = Some v → ▷ wp E (subst ef x v) Φ ⊑ wp E (App (Lam x ef) e) Φ. `````` Ralf Jung committed Feb 12, 2016 21 ``````Proof. intros. by rewrite -wp_rec' ?subst_empty. Qed. `````` Ralf Jung committed Feb 11, 2016 22 `````` `````` Robbert Krebbers committed Feb 18, 2016 23 24 ``````Lemma wp_let' E x e1 e2 v Φ : to_val e1 = Some v → ▷ wp E (subst e2 x v) Φ ⊑ wp E (Let x e1 e2) Φ. `````` Ralf Jung committed Feb 12, 2016 25 ``````Proof. apply wp_lam'. Qed. `````` Ralf Jung committed Feb 11, 2016 26 `````` `````` Robbert Krebbers committed Feb 18, 2016 27 ``````Lemma wp_seq E e1 e2 Φ : wp E e1 (λ _, ▷ wp E e2 Φ) ⊑ wp E (Seq e1 e2) Φ. `````` Ralf Jung committed Feb 11, 2016 28 29 ``````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 18, 2016 33 ``````Lemma wp_skip E Φ : ▷ (Φ (LitV LitUnit)) ⊑ wp E Skip Φ. `````` Ralf Jung committed Feb 13, 2016 34 35 ``````Proof. rewrite -wp_seq -wp_value // -wp_value //. Qed. `````` Robbert Krebbers committed Feb 18, 2016 36 37 38 39 ``````Lemma wp_le E (n1 n2 : Z) P Φ : (n1 ≤ n2 → P ⊑ ▷ Φ (LitV \$ LitBool true)) → (n2 < n1 → P ⊑ ▷ Φ (LitV \$ LitBool false)) → P ⊑ wp E (BinOp LeOp (Lit \$ LitInt n1) (Lit \$ LitInt n2)) Φ. `````` 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. `````` Robbert Krebbers committed Feb 18, 2016 45 46 47 48 ``````Lemma wp_lt E (n1 n2 : Z) P Φ : (n1 < n2 → P ⊑ ▷ Φ (LitV \$ LitBool true)) → (n2 ≤ n1 → P ⊑ ▷ Φ (LitV \$ LitBool false)) → P ⊑ wp E (BinOp LtOp (Lit \$ LitInt n1) (Lit \$ LitInt n2)) Φ. `````` 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. `````` Robbert Krebbers committed Feb 18, 2016 54 55 56 57 ``````Lemma wp_eq E (n1 n2 : Z) P Φ : (n1 = n2 → P ⊑ ▷ Φ (LitV \$ LitBool true)) → (n1 ≠ n2 → P ⊑ ▷ Φ (LitV \$ LitBool false)) → P ⊑ wp E (BinOp EqOp (Lit \$ LitInt n1) (Lit \$ LitInt n2)) Φ. `````` 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.``````