derived.v 2.86 KB
 Robbert Krebbers committed Mar 10, 2016 1 ``````From iris.heap_lang Require Export lifting. `````` Ralf Jung committed Feb 11, 2016 2 3 4 ``````Import uPred. (** Define some derived forms, and derived lemmas about them. *) `````` Ralf Jung committed Mar 02, 2016 5 ``````Notation Lam x e := (Rec BAnon x e). `````` Ralf Jung committed Feb 11, 2016 6 ``````Notation Let x e1 e2 := (App (Lam x e2) e1). `````` Ralf Jung committed Mar 02, 2016 7 8 ``````Notation Seq e1 e2 := (Let BAnon e1 e2). Notation LamV x e := (RecV BAnon x e). `````` Ralf Jung committed Feb 11, 2016 9 ``````Notation LetCtx x e2 := (AppRCtx (LamV x e2)). `````` Ralf Jung committed Mar 02, 2016 10 ``````Notation SeqCtx e2 := (LetCtx BAnon e2). `````` Ralf Jung committed Feb 13, 2016 11 ``````Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)). `````` Ralf Jung committed Mar 02, 2016 12 ``````Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)). `````` Ralf Jung committed Feb 11, 2016 13 14 `````` Section derived. `````` Ralf Jung committed Mar 07, 2016 15 ``````Context {Σ : iFunctor}. `````` Robbert Krebbers committed Feb 18, 2016 16 17 ``````Implicit Types P Q : iProp heap_lang Σ. Implicit Types Φ : val → iProp heap_lang Σ. `````` Ralf Jung committed Feb 11, 2016 18 19 `````` (** Proof rules for the sugar *) `````` Robbert Krebbers committed Feb 27, 2016 20 ``````Lemma wp_lam E x ef e v Φ : `````` Robbert Krebbers committed Feb 19, 2016 21 `````` to_val e = Some v → `````` Robbert Krebbers committed Jul 15, 2016 22 `````` Closed (x :b: []) ef → `````` Ralf Jung committed Mar 10, 2016 23 `````` ▷ WP subst' x e ef @ E {{ Φ }} ⊢ WP App (Lam x ef) e @ E {{ Φ }}. `````` Robbert Krebbers committed May 10, 2016 24 ``````Proof. intros. by rewrite -(wp_rec _ BAnon) //. Qed. `````` Ralf Jung committed Feb 11, 2016 25 `````` `````` Robbert Krebbers committed Feb 27, 2016 26 ``````Lemma wp_let E x e1 e2 v Φ : `````` Robbert Krebbers committed Feb 19, 2016 27 `````` to_val e1 = Some v → `````` Robbert Krebbers committed Jul 15, 2016 28 `````` Closed (x :b: []) e2 → `````` Ralf Jung committed Mar 10, 2016 29 `````` ▷ WP subst' x e1 e2 @ E {{ Φ }} ⊢ WP Let x e1 e2 @ E {{ Φ }}. `````` Robbert Krebbers committed Feb 27, 2016 30 ``````Proof. apply wp_lam. Qed. `````` Ralf Jung committed Feb 11, 2016 31 `````` `````` 32 33 ``````Lemma wp_seq E e1 e2 v Φ : to_val e1 = Some v → `````` Robbert Krebbers committed Jul 15, 2016 34 `````` Closed [] e2 → `````` Ralf Jung committed Mar 10, 2016 35 `````` ▷ WP e2 @ E {{ Φ }} ⊢ WP Seq e1 e2 @ E {{ Φ }}. `````` Robbert Krebbers committed Jul 15, 2016 36 ``````Proof. intros ??. by rewrite -wp_let. Qed. `````` Ralf Jung committed Feb 11, 2016 37 `````` `````` Ralf Jung committed Mar 10, 2016 38 ``````Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) ⊢ WP Skip @ E {{ Φ }}. `````` 39 ``````Proof. rewrite -wp_seq // -wp_value //. Qed. `````` Ralf Jung committed Feb 13, 2016 40 `````` `````` Ralf Jung committed Mar 02, 2016 41 42 ``````Lemma wp_match_inl E e0 v0 x1 e1 x2 e2 Φ : to_val e0 = Some v0 → `````` Robbert Krebbers committed Jul 15, 2016 43 `````` Closed (x1 :b: []) e1 → `````` Ralf Jung committed Mar 10, 2016 44 `````` ▷ WP subst' x1 e0 e1 @ E {{ Φ }} ⊢ WP Match (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}. `````` Ralf Jung committed Mar 10, 2016 45 ``````Proof. intros. by rewrite -wp_case_inl // -[X in _ ⊢ X]later_intro -wp_let. Qed. `````` Ralf Jung committed Mar 02, 2016 46 47 48 `````` Lemma wp_match_inr E e0 v0 x1 e1 x2 e2 Φ : to_val e0 = Some v0 → `````` Robbert Krebbers committed Jul 15, 2016 49 `````` Closed (x2 :b: []) e2 → `````` Ralf Jung committed Mar 10, 2016 50 `````` ▷ WP subst' x2 e0 e2 @ E {{ Φ }} ⊢ WP Match (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}. `````` Ralf Jung committed Mar 10, 2016 51 ``````Proof. intros. by rewrite -wp_case_inr // -[X in _ ⊢ X]later_intro -wp_let. Qed. `````` Ralf Jung committed Mar 02, 2016 52 `````` `````` Robbert Krebbers committed Feb 18, 2016 53 ``````Lemma wp_le E (n1 n2 : Z) P Φ : `````` Robbert Krebbers committed Jun 30, 2016 54 55 `````` (n1 ≤ n2 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool true))) → (n2 < n1 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool false))) → `````` Ralf Jung committed Mar 10, 2016 56 `````` P ⊢ WP BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}. `````` Ralf Jung committed Feb 11, 2016 57 58 59 60 61 ``````Proof. intros. rewrite -wp_bin_op //; []. destruct (bool_decide_reflect (n1 ≤ n2)); by eauto with omega. Qed. `````` Robbert Krebbers committed Feb 18, 2016 62 ``````Lemma wp_lt E (n1 n2 : Z) P Φ : `````` Robbert Krebbers committed Jun 30, 2016 63 64 `````` (n1 < n2 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool true))) → (n2 ≤ n1 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool false))) → `````` Ralf Jung committed Mar 10, 2016 65 `````` P ⊢ WP BinOp LtOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}. `````` Ralf Jung committed Feb 11, 2016 66 67 68 69 70 ``````Proof. intros. rewrite -wp_bin_op //; []. destruct (bool_decide_reflect (n1 < n2)); by eauto with omega. Qed. `````` Robbert Krebbers committed Feb 18, 2016 71 ``````Lemma wp_eq E (n1 n2 : Z) P Φ : `````` Robbert Krebbers committed Jun 30, 2016 72 73 `````` (n1 = n2 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool true))) → (n1 ≠ n2 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool false))) → `````` Ralf Jung committed Mar 10, 2016 74 `````` P ⊢ WP BinOp EqOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}. `````` Ralf Jung committed Feb 11, 2016 75 76 77 78 79 ``````Proof. intros. rewrite -wp_bin_op //; []. destruct (bool_decide_reflect (n1 = n2)); by eauto with omega. Qed. End derived.``````