sugar.v 3.75 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
Require Export heap_lang.heap_lang heap_lang.lifting.
2
Import uPred heap_lang.
3 4 5 6 7 8 9 10

(** 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 LamV (e : {bind expr}) := RecV e.[ren(+1)].

11 12
Definition LetCtx (e2 : {bind expr}) := AppRCtx (LamV e2).
Definition SeqCtx (e2 : expr) := LetCtx (e2.[ren(+1)]).
13

14 15 16 17
Module notations.
  Delimit Scope lang_scope with L.
  Bind Scope lang_scope with expr.
  Arguments wp {_ _} _ _%L _.
18

19 20 21 22
  Coercion LitNat : nat >-> base_lit.
  Coercion LitBool : bool >-> base_lit.
  (* No coercion from base_lit to expr. This makes is slightly easier to tell
     apart language and Coq expressions. *)
23 24 25
  Coercion Loc : loc >-> expr.
  Coercion LocV : loc >-> val.
  Coercion App : expr >-> Funclass.
26

27 28 29 30 31 32 33 34
  (** 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.
35
  Notation "e1 + e2" := (BinOp PlusOp e1%L e2%L)
36
    (at level 50, left associativity) : lang_scope.
37 38 39 40 41
  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.
42 43 44 45 46 47 48
  (* 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)
49
    (at level 200, e1, e2, e3 at level 200) : lang_scope.
50
End notations.
51

52
Section suger.
53 54
Context {Σ : iFunctor}.
Implicit Types P : iProp heap_lang Σ.
55
Implicit Types Q : val  iProp heap_lang Σ.
56

57 58
(** Proof rules for the sugar *)
Lemma wp_lam E ef e v Q :
59
  to_val e = Some v   wp E ef.[e/] Q  wp E (App (Lam ef) e) Q.
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.
66

67
Lemma wp_let E e1 e2 Q :
68
  wp E e1 (λ v, wp E (e2.[of_val v/]) Q)  wp E (Let e1 e2) Q.
69
Proof.
70 71
  rewrite -(wp_bind [LetCtx e2]). apply wp_mono=>v.
  by rewrite -wp_lam //= to_of_val.
72
Qed.
73 74 75 76 77 78 79 80 81 82 83 84 85 86

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.
  intros ? ?. rewrite -wp_bin_op //; [].
  destruct (decide _); by eauto with omega.
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.
87
Proof.
88 89
  intros ? ?. rewrite -wp_bin_op //; [].
  destruct (decide _); by eauto with omega.
90
Qed.
91 92 93 94 95

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.
96
Proof.
97 98
  intros ? ?. rewrite -wp_bin_op //; [].
  destruct (decide _); by eauto with omega.
99
Qed.
100

101
End suger.