derived.v 2.14 KB
Newer Older
1
From heap_lang Require Export lifting.
2 3 4 5 6 7 8 9 10
Import uPred.

(** Define some derived forms, and derived lemmas about them. *)
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
Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
12 13 14

Section derived.
Context {Σ : iFunctor}.
15 16
Implicit Types P Q : iProp heap_lang Σ.
Implicit Types Φ : val  iProp heap_lang Σ.
17 18

(** Proof rules for the sugar *)
19 20
Lemma wp_lam' E x ef e v Φ :
  to_val e = Some v   wp E (subst ef x v) Φ  wp E (App (Lam x ef) e) Φ.
21
Proof. intros. by rewrite -wp_rec' ?subst_empty. Qed.
22

23 24
Lemma wp_let' E x e1 e2 v Φ :
  to_val e1 = Some v   wp E (subst e2 x v) Φ  wp E (Let x e1 e2) Φ.
25
Proof. apply wp_lam'. Qed.
26

27
Lemma wp_seq E e1 e2 Φ : wp E e1 (λ _,  wp E e2 Φ)  wp E (Seq e1 e2) Φ.
28 29
Proof.
  rewrite -(wp_bind [LetCtx "" e2]). apply wp_mono=>v.
30
  by rewrite -wp_let' //= ?to_of_val ?subst_empty.
31 32
Qed.

33
Lemma wp_skip E Φ :  (Φ (LitV LitUnit))  wp E Skip Φ.
34 35
Proof. rewrite -wp_seq -wp_value // -wp_value //. Qed.

36 37 38 39
Lemma wp_le E (n1 n2 : Z) P Φ :
  (n1  n2  P   Φ (LitV $ LitBool true)) 
  (n2 < n1  P   Φ (LitV $ LitBool false)) 
  P  wp E (BinOp LeOp (Lit $ LitInt n1) (Lit $ LitInt n2)) Φ.
40 41 42 43 44
Proof.
  intros. rewrite -wp_bin_op //; [].
  destruct (bool_decide_reflect (n1  n2)); by eauto with omega.
Qed.

45 46 47 48
Lemma wp_lt E (n1 n2 : Z) P Φ :
  (n1 < n2  P   Φ (LitV $ LitBool true)) 
  (n2  n1  P   Φ (LitV $ LitBool false)) 
  P  wp E (BinOp LtOp (Lit $ LitInt n1) (Lit $ LitInt n2)) Φ.
49 50 51 52 53
Proof.
  intros. rewrite -wp_bin_op //; [].
  destruct (bool_decide_reflect (n1 < n2)); by eauto with omega.
Qed.

54 55 56 57
Lemma wp_eq E (n1 n2 : Z) P Φ :
  (n1 = n2  P   Φ (LitV $ LitBool true)) 
  (n1  n2  P   Φ (LitV $ LitBool false)) 
  P  wp E (BinOp EqOp (Lit $ LitInt n1) (Lit $ LitInt n2)) Φ.
58 59 60 61 62
Proof.
  intros. rewrite -wp_bin_op //; [].
  destruct (bool_decide_reflect (n1 = n2)); by eauto with omega.
Qed.
End derived.