sugar.v 2.51 KB
 Ralf Jung committed Jan 30, 2016 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 ``````Require Export barrier.heap_lang barrier.lifting. Import uPred. (** Define some syntactic sugar. LitTrue and LitFalse are defined in heap_lang.v. *) Definition Lam (e : {bind expr}) := Rec e.[ren(+1)]. Definition Let (e1 : expr) (e2: {bind expr}) := App (Lam e2) e1. Definition Seq (e1 e2 : expr) := Let e1 e2.[ren(+1)]. Definition If (e0 e1 e2 : expr) := Case e0 e1.[ren(+1)] e2.[ren(+1)]. Definition Lt e1 e2 := Le (Plus e1 \$ LitNat 1) e2. Definition Eq e1 e2 := Let e1 (Let e2.[ren(+1)] (If (Le (Var 0) (Var 1)) (Le (Var 1) (Var 0)) LitFalse)). Definition LamV (e : {bind expr}) := RecV e.[ren(+1)]. Definition LetCtx (K1 : ectx) (e2 : {bind expr}) := AppRCtx (LamV e2) K1. Definition SeqCtx (K1 : ectx) (e2 : expr) := LetCtx K1 (e2.[ren(+1)]). `````` Robbert Krebbers committed Feb 01, 2016 19 ``````Section suger. `````` Robbert Krebbers committed Feb 01, 2016 20 21 22 ``````Context {Σ : iFunctor}. Implicit Types P : iProp heap_lang Σ. Implicit Types Q : val heap_lang → iProp heap_lang Σ. `````` Robbert Krebbers committed Feb 01, 2016 23 `````` `````` Ralf Jung committed Jan 30, 2016 24 25 ``````(** Proof rules for the sugar *) Lemma wp_lam E ef e v Q : `````` Robbert Krebbers committed Feb 01, 2016 26 `````` e2v e = Some v → ▷wp E ef.[e/] Q ⊑ wp E (App (Lam ef) e) Q. `````` Ralf Jung committed Jan 30, 2016 27 28 29 30 31 32 33 34 ``````Proof. intros Hv. rewrite -wp_rec; last eassumption. (* RJ: This pulls in functional extensionality. If that bothers us, we have to talk to the Autosubst guys. *) by asimpl. Qed. Lemma wp_let e1 e2 E Q : `````` Robbert Krebbers committed Feb 01, 2016 35 `````` wp E e1 (λ v, ▷wp E (e2.[v2e v/]) Q) ⊑ wp E (Let e1 e2) Q. `````` Ralf Jung committed Jan 30, 2016 36 37 38 39 40 41 ``````Proof. rewrite -(wp_bind (LetCtx EmptyCtx e2)). apply wp_mono=>v. rewrite -wp_lam //. by rewrite v2v. Qed. Lemma wp_if_true e1 e2 E Q : `````` Robbert Krebbers committed Feb 01, 2016 42 `````` ▷wp E e1 Q ⊑ wp E (If LitTrue e1 e2) Q. `````` Ralf Jung committed Jan 30, 2016 43 44 45 46 47 ``````Proof. rewrite -wp_case_inl //. by asimpl. Qed. Lemma wp_if_false e1 e2 E Q : `````` Robbert Krebbers committed Feb 01, 2016 48 `````` ▷wp E e2 Q ⊑ wp E (If LitFalse e1 e2) Q. `````` Ralf Jung committed Jan 30, 2016 49 50 51 52 53 54 55 ``````Proof. rewrite -wp_case_inr //. by asimpl. Qed. Lemma wp_lt n1 n2 E P Q : (n1 < n2 → P ⊑ ▷Q LitTrueV) → (n1 ≥ n2 → P ⊑ ▷Q LitFalseV) → `````` Robbert Krebbers committed Feb 01, 2016 56 `````` P ⊑ wp E (Lt (LitNat n1) (LitNat n2)) Q. `````` Ralf Jung committed Jan 30, 2016 57 58 59 60 61 62 63 64 65 ``````Proof. intros HPlt HPge. rewrite -(wp_bind (LeLCtx EmptyCtx _)) -wp_plus -later_intro. simpl. apply wp_le; intros; [apply HPlt|apply HPge]; omega. Qed. Lemma wp_eq n1 n2 E P Q : (n1 = n2 → P ⊑ ▷Q LitTrueV) → (n1 ≠ n2 → P ⊑ ▷Q LitFalseV) → `````` Robbert Krebbers committed Feb 01, 2016 66 `````` P ⊑ wp E (Eq (LitNat n1) (LitNat n2)) Q. `````` Ralf Jung committed Jan 30, 2016 67 68 69 70 71 72 73 74 75 76 77 78 ``````Proof. intros HPeq HPne. rewrite -wp_let -wp_value' // -later_intro. asimpl. rewrite -wp_rec //. asimpl. rewrite -(wp_bind (CaseCtx EmptyCtx _ _)) -later_intro. apply wp_le; intros Hn12. - asimpl. rewrite -wp_case_inl // -!later_intro. apply wp_le; intros Hn12'. + apply HPeq; omega. + apply HPne; omega. - asimpl. rewrite -wp_case_inr // -later_intro -wp_value' //. apply HPne; omega. Qed. `````` Robbert Krebbers committed Feb 01, 2016 79 ``End suger.``