sugar.v 3.87 KB
 Ralf Jung committed Feb 03, 2016 1 ``````Require Export heap_lang.heap_lang heap_lang.lifting. `````` Robbert Krebbers committed Feb 08, 2016 2 ``````Import uPred heap_lang. `````` Ralf Jung committed Jan 30, 2016 3 4 5 6 7 8 9 10 11 12 13 14 15 `````` (** 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)]. `````` Robbert Krebbers committed Feb 02, 2016 16 17 ``````Definition LetCtx (e2 : {bind expr}) := AppRCtx (LamV e2). Definition SeqCtx (e2 : expr) := LetCtx (e2.[ren(+1)]). `````` Ralf Jung committed Jan 30, 2016 18 `````` `````` Robbert Krebbers committed Feb 08, 2016 19 20 21 22 ``````Module notations. Delimit Scope lang_scope with L. Bind Scope lang_scope with expr. Arguments wp {_ _} _ _%L _. `````` Ralf Jung committed Feb 05, 2016 23 `````` `````` Robbert Krebbers committed Feb 08, 2016 24 25 26 27 28 `````` Coercion LitNat : nat >-> expr. Coercion LitNatV : nat >-> val. Coercion Loc : loc >-> expr. Coercion LocV : loc >-> val. Coercion App : expr >-> Funclass. `````` Ralf Jung committed Feb 05, 2016 29 `````` `````` Robbert Krebbers committed Feb 08, 2016 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 `````` (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come first. *) (* What about Arguments for hoare triples?. *) (* The colons indicate binders. "let" is not consistent here though, thing are only bound in the "in". *) Notation "# n" := (Var n) (at level 1, format "# n") : lang_scope. Notation "! e" := (Load e%L) (at level 10, format "! e") : lang_scope. Notation "'ref' e" := (Alloc e%L) (at level 30) : lang_scope. Notation "e1 + e2" := (Plus e1%L e2%L) (at level 50, left associativity) : lang_scope. Notation "e1 ≤ e2" := (Le e1%L e2%L) (at level 70) : lang_scope. Notation "e1 < e2" := (Lt e1%L e2%L) (at level 70) : lang_scope. (* The unicode ← is already part of the notation "_ ← _; _" for bind. *) Notation "e1 <- e2" := (Store e1%L e2%L) (at level 80) : lang_scope. Notation "e1 ; e2" := (Seq e1%L e2%L) (at level 100) : lang_scope. Notation "'let:' e1 'in' e2" := (Let e1%L e2%L) (at level 102) : lang_scope. Notation "'λ:' e" := (Lam e%L) (at level 102) : lang_scope. Notation "'rec::' e" := (Rec e%L) (at level 102) : lang_scope. Notation "'if' e1 'then' e2 'else' e3" := (If e1%L e2%L e3%L) (at level 200, e1, e2, e3 at level 200, only parsing) : lang_scope. End notations. `````` Ralf Jung committed Feb 05, 2016 51 `````` `````` Robbert Krebbers committed Feb 01, 2016 52 ``````Section suger. `````` Robbert Krebbers committed Feb 01, 2016 53 54 ``````Context {Σ : iFunctor}. Implicit Types P : iProp heap_lang Σ. `````` Robbert Krebbers committed Feb 02, 2016 55 ``````Implicit Types Q : val → iProp heap_lang Σ. `````` Robbert Krebbers committed Feb 01, 2016 56 `````` `````` Ralf Jung committed Jan 30, 2016 57 58 ``````(** Proof rules for the sugar *) Lemma wp_lam E ef e v Q : `````` Robbert Krebbers committed Feb 02, 2016 59 `````` to_val e = Some v → ▷ wp E ef.[e/] Q ⊑ wp E (App (Lam ef) e) Q. `````` Ralf Jung committed Jan 30, 2016 60 61 62 63 64 65 ``````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. `````` Robbert Krebbers committed Feb 02, 2016 66 ``````Lemma wp_let E e1 e2 Q : `````` Robbert Krebbers committed Feb 02, 2016 67 `````` wp E e1 (λ v, ▷wp E (e2.[of_val v/]) Q) ⊑ wp E (Let e1 e2) Q. `````` Ralf Jung committed Jan 30, 2016 68 ``````Proof. `````` Robbert Krebbers committed Feb 02, 2016 69 70 `````` rewrite -(wp_bind [LetCtx e2]). apply wp_mono=>v. by rewrite -wp_lam //= to_of_val. `````` Ralf Jung committed Jan 30, 2016 71 ``````Qed. `````` Robbert Krebbers committed Feb 02, 2016 72 ``````Lemma wp_if_true E e1 e2 Q : ▷ wp E e1 Q ⊑ wp E (If LitTrue e1 e2) Q. `````` Robbert Krebbers committed Feb 02, 2016 73 ``````Proof. rewrite -wp_case_inl //. by asimpl. Qed. `````` Robbert Krebbers committed Feb 02, 2016 74 ``````Lemma wp_if_false E e1 e2 Q : ▷ wp E e2 Q ⊑ wp E (If LitFalse e1 e2) Q. `````` Robbert Krebbers committed Feb 02, 2016 75 ``````Proof. rewrite -wp_case_inr //. by asimpl. Qed. `````` Robbert Krebbers committed Feb 02, 2016 76 ``````Lemma wp_lt E n1 n2 P Q : `````` Robbert Krebbers committed Feb 02, 2016 77 78 `````` (n1 < n2 → P ⊑ ▷ Q LitTrueV) → (n1 ≥ n2 → P ⊑ ▷ Q LitFalseV) → `````` Robbert Krebbers committed Feb 01, 2016 79 `````` P ⊑ wp E (Lt (LitNat n1) (LitNat n2)) Q. `````` Ralf Jung committed Jan 30, 2016 80 ``````Proof. `````` Robbert Krebbers committed Feb 02, 2016 81 82 `````` intros; rewrite -(wp_bind [LeLCtx _]) -wp_plus -later_intro /=. auto using wp_le with lia. `````` Ralf Jung committed Jan 30, 2016 83 ``````Qed. `````` Robbert Krebbers committed Feb 02, 2016 84 ``````Lemma wp_eq E n1 n2 P Q : `````` Robbert Krebbers committed Feb 02, 2016 85 86 `````` (n1 = n2 → P ⊑ ▷ Q LitTrueV) → (n1 ≠ n2 → P ⊑ ▷ Q LitFalseV) → `````` Robbert Krebbers committed Feb 01, 2016 87 `````` P ⊑ wp E (Eq (LitNat n1) (LitNat n2)) Q. `````` Ralf Jung committed Jan 30, 2016 88 89 ``````Proof. intros HPeq HPne. `````` Robbert Krebbers committed Feb 02, 2016 90 91 92 93 94 95 `````` rewrite -wp_let -wp_value' // -later_intro; asimpl. rewrite -wp_rec //; asimpl. rewrite -(wp_bind [CaseCtx _ _]) -later_intro; asimpl. apply wp_le; intros; asimpl. * rewrite -wp_case_inl // -!later_intro. apply wp_le; auto with lia. * rewrite -wp_case_inr // -later_intro -wp_value' //; auto with lia. `````` Ralf Jung committed Jan 30, 2016 96 ``````Qed. `````` Robbert Krebbers committed Feb 01, 2016 97 ``End suger.``