sugar.v 3.81 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
6
7
8
9
10
Notation Lam x e := (Rec "" x e).
Notation Let x e1 e2 := (App (Lam x e2) e1).
Notation Seq e1 e2 := (Let "" e1 e2).
Notation LamV x e := (RecV "" x e).
Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
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
19
20
  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. *)
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
47
48
49
50

  (* derived notions, in order of declaration *)
  Notation "λ: x , e" := (Lam x e%L)
    (at level 102, x at level 1, e at level 200) : lang_scope.
  (* FIXME: the ones below are not being pretty printed *)
  Notation "'let:' x := e1 'in' e2" := (Let x e1%L e2%L)
    (at level 102, x at level 1, e1 at level 1, e2 at level 200) : lang_scope.
  Notation "e1 ; e2" := (Seq e1%L e2%L)
    (at level 100, e2 at level 200) : lang_scope.
51
End notations.
52

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

58
(** Proof rules for the sugar *)
59
60
61
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.
62

63
64
Lemma wp_let E x e1 e2 Q :
  wp E e1 (λ v,  wp E (subst e2 x v) Q)  wp E (Let x e1 e2) Q.
65
Proof.
66
  rewrite -(wp_bind [LetCtx x e2]). apply wp_mono=>v.
67
  by rewrite -wp_lam //= to_of_val.
68
Qed.
69

70
71
Lemma wp_seq E e1 e2 Q : wp E e1 (λ _, wp E e2 Q)  wp E (Seq e1 e2) Q.
Proof. rewrite -wp_let. apply wp_mono=>v. by rewrite subst_empty. Qed.
72

73
74
75
76
77
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.
78
  intros. rewrite -wp_bin_op //; [].
Robbert Krebbers's avatar
Robbert Krebbers committed
79
  destruct (bool_decide_reflect (n1  n2)); by eauto with omega.
80
81
82
83
84
85
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.
86
Proof.
87
  intros. rewrite -wp_bin_op //; [].
Robbert Krebbers's avatar
Robbert Krebbers committed
88
  destruct (bool_decide_reflect (n1 < n2)); by eauto with omega.
89
Qed.
90
91
92
93
94

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.
95
Proof.
96
  intros. rewrite -wp_bin_op //; [].
Robbert Krebbers's avatar
Robbert Krebbers committed
97
  destruct (bool_decide_reflect (n1 = n2)); by eauto with omega.
98
Qed.
99

100
End suger.