derived.v 2.15 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 27, 2016 19 ``````Lemma wp_lam E x ef e v Φ : `````` Robbert Krebbers committed Feb 19, 2016 20 21 `````` to_val e = Some v → ▷ || subst ef x v @ E {{ Φ }} ⊑ || App (Lam x ef) e @ E {{ Φ }}. `````` Robbert Krebbers committed Feb 27, 2016 22 ``````Proof. intros. by rewrite -wp_rec ?subst_empty. Qed. `````` Ralf Jung committed Feb 11, 2016 23 `````` `````` Robbert Krebbers committed Feb 27, 2016 24 ``````Lemma wp_let E x e1 e2 v Φ : `````` Robbert Krebbers committed Feb 19, 2016 25 26 `````` to_val e1 = Some v → ▷ || subst e2 x v @ E {{ Φ }} ⊑ || Let x e1 e2 @ E {{ Φ }}. `````` Robbert Krebbers committed Feb 27, 2016 27 ``````Proof. apply wp_lam. Qed. `````` Ralf Jung committed Feb 11, 2016 28 `````` `````` 29 30 31 ``````Lemma wp_seq E e1 e2 v Φ : to_val e1 = Some v → ▷ || e2 @ E {{ Φ }} ⊑ || Seq e1 e2 @ E {{ Φ }}. `````` Robbert Krebbers committed Feb 27, 2016 32 ``````Proof. intros ?. rewrite -wp_let // subst_empty //. Qed. `````` Ralf Jung committed Feb 11, 2016 33 `````` `````` Robbert Krebbers committed Feb 19, 2016 34 ``````Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) ⊑ || Skip @ E {{ Φ }}. `````` 35 ``````Proof. rewrite -wp_seq // -wp_value //. Qed. `````` Ralf Jung committed Feb 13, 2016 36 `````` `````` Robbert Krebbers committed Feb 18, 2016 37 ``````Lemma wp_le E (n1 n2 : Z) P Φ : `````` Robbert Krebbers committed Feb 19, 2016 38 39 40 `````` (n1 ≤ n2 → P ⊑ ▷ Φ (LitV (LitBool true))) → (n2 < n1 → P ⊑ ▷ Φ (LitV (LitBool false))) → P ⊑ || BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}. `````` Ralf Jung committed Feb 11, 2016 41 42 43 44 45 ``````Proof. intros. rewrite -wp_bin_op //; []. destruct (bool_decide_reflect (n1 ≤ n2)); by eauto with omega. Qed. `````` Robbert Krebbers committed Feb 18, 2016 46 ``````Lemma wp_lt E (n1 n2 : Z) P Φ : `````` Robbert Krebbers committed Feb 19, 2016 47 48 49 `````` (n1 < n2 → P ⊑ ▷ Φ (LitV (LitBool true))) → (n2 ≤ n1 → P ⊑ ▷ Φ (LitV (LitBool false))) → P ⊑ || BinOp LtOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}. `````` Ralf Jung committed Feb 11, 2016 50 51 52 53 54 ``````Proof. intros. rewrite -wp_bin_op //; []. destruct (bool_decide_reflect (n1 < n2)); by eauto with omega. Qed. `````` Robbert Krebbers committed Feb 18, 2016 55 ``````Lemma wp_eq E (n1 n2 : Z) P Φ : `````` Robbert Krebbers committed Feb 19, 2016 56 57 58 `````` (n1 = n2 → P ⊑ ▷ Φ (LitV (LitBool true))) → (n1 ≠ n2 → P ⊑ ▷ Φ (LitV (LitBool false))) → P ⊑ || BinOp EqOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}. `````` Ralf Jung committed Feb 11, 2016 59 60 61 62 63 ``````Proof. intros. rewrite -wp_bin_op //; []. destruct (bool_decide_reflect (n1 = n2)); by eauto with omega. Qed. End derived.``````