sugar.v 3.97 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

(** Define some syntactic sugar. LitTrue and LitFalse are defined in heap_lang.v. *)
5
Notation Lam x e := (Rec "" x e).
6
Notation Let x e1 e2 := (App (Lam x e2) e1).
7 8
Notation Seq e1 e2 := (Let "" e1 e2).
Notation LamV x e := (RecV "" x e).
9
Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
10
Notation SeqCtx e2 := (LetCtx "" e2).
11

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

17 18
  Coercion LitNat : nat >-> base_lit.
  Coercion LitBool : bool >-> base_lit.
19
  (** No coercion from base_lit to expr. This makes is slightly easier to tell
20
     apart language and Coq expressions. *)
21
  Coercion Var : string >-> expr.
22
  Coercion App : expr >-> Funclass.
23

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.
29
  Notation "e1 + e2" := (BinOp PlusOp e1%L e2%L)
30
    (at level 50, left associativity) : lang_scope.
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.
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.
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.
40
  Notation "'if' e1 'then' e2 'else' e3" := (If e1%L e2%L e3%L)
41
    (at level 200, e1, e2, e3 at level 200) : lang_scope.
42

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. *)
47 48
  Notation "λ: x , e" := (Lam x e%L)
    (at level 102, x at level 1, e at level 200) : lang_scope.
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.
53
End notations.
54

55
Section suger.
56 57
Context {Σ : iFunctor}.
Implicit Types P : iProp heap_lang Σ.
58
Implicit Types Q : val  iProp heap_lang Σ.
59

60
(** Proof rules for the sugar *)
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.
64

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.

69
Lemma wp_seq E e1 e2 Q : wp E e1 (λ _,  wp E e2 Q)  wp E (Seq e1 e2) Q.
70
Proof.
71 72
  rewrite -(wp_bind [LetCtx "" e2]). apply wp_mono=>v.
  by rewrite -wp_let //= ?subst_empty ?to_of_val.
73
Qed.
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.
80
  intros. rewrite -wp_bin_op //; [].
Robbert Krebbers's avatar
Robbert Krebbers committed
81
  destruct (bool_decide_reflect (n1  n2)); by eauto with omega.
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.
88
Proof.
89
  intros. rewrite -wp_bin_op //; [].
Robbert Krebbers's avatar
Robbert Krebbers committed
90
  destruct (bool_decide_reflect (n1 < n2)); by eauto with omega.
91
Qed.
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.
97
Proof.
98
  intros. rewrite -wp_bin_op //; [].
Robbert Krebbers's avatar
Robbert Krebbers committed
99
  destruct (bool_decide_reflect (n1 = n2)); by eauto with omega.
100
Qed.
101

102
End suger.