sugar.v 2.51 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
Require Export barrier.heap_lang barrier.lifting.
Import uPred.

(** 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)].

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

19
Section suger.
20 21 22
Context {Σ : iFunctor}.
Implicit Types P : iProp heap_lang Σ.
Implicit Types Q : val heap_lang  iProp heap_lang Σ.
23

24 25
(** Proof rules for the sugar *)
Lemma wp_lam E ef e v Q :
26
  e2v e = Some v  wp E ef.[e/] Q  wp E (App (Lam ef) e) Q.
27 28 29 30 31 32 33 34
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.

Lemma wp_let e1 e2 E Q :
35
  wp E e1 (λ v, wp E (e2.[v2e v/]) Q)  wp E (Let e1 e2) Q.
36 37 38 39 40 41
Proof.
  rewrite -(wp_bind (LetCtx EmptyCtx e2)). apply wp_mono=>v.
  rewrite -wp_lam //. by rewrite v2v.
Qed.

Lemma wp_if_true e1 e2 E Q :
42
  wp E e1 Q  wp E (If LitTrue e1 e2) Q.
43 44 45 46 47
Proof.
  rewrite -wp_case_inl //. by asimpl.
Qed.

Lemma wp_if_false e1 e2 E Q :
48
  wp E e2 Q  wp E (If LitFalse e1 e2) Q.
49 50 51 52 53 54 55
Proof.
  rewrite -wp_case_inr //. by asimpl.
Qed.

Lemma wp_lt n1 n2 E P Q :
  (n1 < n2  P  Q LitTrueV) 
  (n1  n2  P  Q LitFalseV) 
56
  P  wp E (Lt (LitNat n1) (LitNat n2)) Q.
57 58 59 60 61 62 63 64 65
Proof.
  intros HPlt HPge.
  rewrite -(wp_bind (LeLCtx EmptyCtx _)) -wp_plus -later_intro. simpl.
  apply wp_le; intros; [apply HPlt|apply HPge]; omega.
Qed.

Lemma wp_eq n1 n2 E P Q :
  (n1 = n2  P  Q LitTrueV) 
  (n1  n2  P  Q LitFalseV) 
66
  P  wp E (Eq (LitNat n1) (LitNat n2)) Q.
67 68 69 70 71 72 73 74 75 76 77 78
Proof.
  intros HPeq HPne.
  rewrite -wp_let -wp_value' // -later_intro. asimpl.
  rewrite -wp_rec //. asimpl.
  rewrite -(wp_bind (CaseCtx EmptyCtx _ _)) -later_intro.
  apply wp_le; intros Hn12.
  - asimpl. rewrite -wp_case_inl // -!later_intro. apply wp_le; intros Hn12'.
    + apply HPeq; omega.
    + apply HPne; omega.
  - asimpl. rewrite -wp_case_inr // -later_intro -wp_value' //.
    apply HPne; omega.
Qed.
79
End suger.