sugar.v 3.97 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 `````` (** Define some syntactic sugar. LitTrue and LitFalse are defined in heap_lang.v. *) `````` Robbert Krebbers committed Feb 09, 2016 5 ``````Notation Lam x e := (Rec "" x e). `````` Robbert Krebbers committed Feb 10, 2016 6 ``````Notation Let x e1 e2 := (App (Lam x e2) e1). `````` Robbert Krebbers committed Feb 09, 2016 7 8 ``````Notation Seq e1 e2 := (Let "" e1 e2). Notation LamV x e := (RecV "" x e). `````` Robbert Krebbers committed Feb 10, 2016 9 ``````Notation LetCtx x e2 := (AppRCtx (LamV x e2)). `````` Robbert Krebbers committed Feb 09, 2016 10 ``````Notation SeqCtx e2 := (LetCtx "" e2). `````` Ralf Jung committed Feb 09, 2016 11 `````` `````` Robbert Krebbers committed Feb 08, 2016 12 13 14 15 ``````Module notations. Delimit Scope lang_scope with L. Bind Scope lang_scope with expr. Arguments wp {_ _} _ _%L _. `````` Ralf Jung committed Feb 05, 2016 16 `````` `````` Ralf Jung committed Feb 09, 2016 17 18 `````` Coercion LitNat : nat >-> base_lit. Coercion LitBool : bool >-> base_lit. `````` Robbert Krebbers committed Feb 10, 2016 19 `````` (** No coercion from base_lit to expr. This makes is slightly easier to tell `````` Ralf Jung committed Feb 09, 2016 20 `````` apart language and Coq expressions. *) `````` Robbert Krebbers committed Feb 09, 2016 21 `````` Coercion Var : string >-> expr. `````` Robbert Krebbers committed Feb 08, 2016 22 `````` Coercion App : expr >-> Funclass. `````` Ralf Jung committed Feb 05, 2016 23 `````` `````` Robbert Krebbers committed Feb 08, 2016 24 25 26 27 28 `````` (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come first. *) (* What about Arguments for hoare triples?. *) Notation "! e" := (Load e%L) (at level 10, format "! e") : lang_scope. Notation "'ref' e" := (Alloc e%L) (at level 30) : lang_scope. `````` Ralf Jung committed Feb 09, 2016 29 `````` Notation "e1 + e2" := (BinOp PlusOp e1%L e2%L) `````` Robbert Krebbers committed Feb 08, 2016 30 `````` (at level 50, left associativity) : lang_scope. `````` Ralf Jung committed Feb 09, 2016 31 32 33 34 35 `````` Notation "e1 - e2" := (BinOp MinusOp e1%L e2%L) (at level 50, left associativity) : lang_scope. Notation "e1 ≤ e2" := (BinOp LeOp e1%L e2%L) (at level 70) : lang_scope. Notation "e1 < e2" := (BinOp LtOp e1%L e2%L) (at level 70) : lang_scope. Notation "e1 = e2" := (BinOp EqOp e1%L e2%L) (at level 70) : lang_scope. `````` Robbert Krebbers committed Feb 08, 2016 36 37 `````` (* The unicode ← is already part of the notation "_ ← _; _" for bind. *) Notation "e1 <- e2" := (Store e1%L e2%L) (at level 80) : lang_scope. `````` Robbert Krebbers committed Feb 09, 2016 38 39 `````` Notation "'rec:' f x := e" := (Rec f x e%L) (at level 102, f at level 1, x at level 1, e at level 200) : lang_scope. `````` Robbert Krebbers committed Feb 08, 2016 40 `````` Notation "'if' e1 'then' e2 'else' e3" := (If e1%L e2%L e3%L) `````` Ralf Jung committed Feb 09, 2016 41 `````` (at level 200, e1, e2, e3 at level 200) : lang_scope. `````` Robbert Krebbers committed Feb 09, 2016 42 `````` `````` Robbert Krebbers committed Feb 10, 2016 43 44 45 46 `````` (** Derived notions, in order of declaration. The notations for let and seq are stated explicitly instead of relying on the Notations Let and Seq as defined above. This is needed because App is now a coercion, and these notations are otherwise not pretty printed back accordingly. *) `````` Robbert Krebbers committed Feb 09, 2016 47 48 `````` Notation "λ: x , e" := (Lam x e%L) (at level 102, x at level 1, e at level 200) : lang_scope. `````` Robbert Krebbers committed Feb 10, 2016 49 50 51 52 `````` Notation "'let:' x := e1 'in' e2" := (Lam x e2%L e1%L) (at level 102, x at level 1, e1 at level 1, e2 at level 200) : lang_scope. Notation "e1 ; e2" := (Lam "" e2%L e1%L) (at level 100, e2 at level 200) : lang_scope. `````` Robbert Krebbers committed Feb 08, 2016 53 ``````End notations. `````` Ralf Jung committed Feb 05, 2016 54 `````` `````` Robbert Krebbers committed Feb 01, 2016 55 ``````Section suger. `````` Robbert Krebbers committed Feb 01, 2016 56 57 ``````Context {Σ : iFunctor}. Implicit Types P : iProp heap_lang Σ. `````` Robbert Krebbers committed Feb 02, 2016 58 ``````Implicit Types Q : val → iProp heap_lang Σ. `````` Robbert Krebbers committed Feb 01, 2016 59 `````` `````` Ralf Jung committed Jan 30, 2016 60 ``````(** Proof rules for the sugar *) `````` Robbert Krebbers committed Feb 09, 2016 61 62 63 ``````Lemma wp_lam E x ef e v Q : to_val e = Some v → ▷ wp E (subst ef x v) Q ⊑ wp E (App (Lam x ef) e) Q. Proof. intros. by rewrite -wp_rec ?subst_empty; eauto. Qed. `````` Ralf Jung committed Feb 09, 2016 64 `````` `````` Robbert Krebbers committed Feb 10, 2016 65 66 67 68 ``````Lemma wp_let E x e1 e2 v Q : to_val e1 = Some v → ▷ wp E (subst e2 x v) Q ⊑ wp E (Let x e1 e2) Q. Proof. apply wp_lam. Qed. `````` Robbert Krebbers committed Feb 10, 2016 69 ``````Lemma wp_seq E e1 e2 Q : wp E e1 (λ _, ▷ wp E e2 Q) ⊑ wp E (Seq e1 e2) Q. `````` Ralf Jung committed Jan 30, 2016 70 ``````Proof. `````` Robbert Krebbers committed Feb 10, 2016 71 72 `````` rewrite -(wp_bind [LetCtx "" e2]). apply wp_mono=>v. by rewrite -wp_let //= ?subst_empty ?to_of_val. `````` Ralf Jung committed Jan 30, 2016 73 ``````Qed. `````` Ralf Jung committed Feb 09, 2016 74 75 76 77 78 79 `````` Lemma wp_le E (n1 n2 : nat) P Q : (n1 ≤ n2 → P ⊑ ▷ Q (LitV true)) → (n1 > n2 → P ⊑ ▷ Q (LitV false)) → P ⊑ wp E (BinOp LeOp (Lit n1) (Lit n2)) Q. Proof. `````` Robbert Krebbers committed Feb 09, 2016 80 `````` intros. rewrite -wp_bin_op //; []. `````` Robbert Krebbers committed Feb 09, 2016 81 `````` destruct (bool_decide_reflect (n1 ≤ n2)); by eauto with omega. `````` Ralf Jung committed Feb 09, 2016 82 83 84 85 86 87 ``````Qed. Lemma wp_lt E (n1 n2 : nat) P Q : (n1 < n2 → P ⊑ ▷ Q (LitV true)) → (n1 ≥ n2 → P ⊑ ▷ Q (LitV false)) → P ⊑ wp E (BinOp LtOp (Lit n1) (Lit n2)) Q. `````` Ralf Jung committed Jan 30, 2016 88 ``````Proof. `````` Robbert Krebbers committed Feb 09, 2016 89 `````` intros. rewrite -wp_bin_op //; []. `````` Robbert Krebbers committed Feb 09, 2016 90 `````` destruct (bool_decide_reflect (n1 < n2)); by eauto with omega. `````` Ralf Jung committed Jan 30, 2016 91 ``````Qed. `````` Ralf Jung committed Feb 09, 2016 92 93 94 95 96 `````` Lemma wp_eq E (n1 n2 : nat) P Q : (n1 = n2 → P ⊑ ▷ Q (LitV true)) → (n1 ≠ n2 → P ⊑ ▷ Q (LitV false)) → P ⊑ wp E (BinOp EqOp (Lit n1) (Lit n2)) Q. `````` Ralf Jung committed Jan 30, 2016 97 ``````Proof. `````` Robbert Krebbers committed Feb 09, 2016 98 `````` intros. rewrite -wp_bin_op //; []. `````` Robbert Krebbers committed Feb 09, 2016 99 `````` destruct (bool_decide_reflect (n1 = n2)); by eauto with omega. `````` Ralf Jung committed Jan 30, 2016 100 ``````Qed. `````` Ralf Jung committed Feb 09, 2016 101 `````` `````` Robbert Krebbers committed Feb 01, 2016 102 ``End suger.``