derived.v 2.04 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34
Require Export heap_lang.lifting.
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).

Section derived.
Context {Σ : iFunctor}.
Implicit Types P : iProp heap_lang Σ.
Implicit Types Q : val  iProp heap_lang Σ.

(** Proof rules for the sugar *)
Lemma wp_lam E x ef e v Q :
  to_val e = Some v   wp E (gsubst ef x e) Q  wp E (App (Lam x ef) e) Q.
Proof.
  intros <-%of_to_val; rewrite -wp_rec ?to_of_val //.
  by rewrite (gsubst_correct _ _ (RecV _ _ _)) subst_empty.
Qed.

Lemma wp_let E x e1 e2 v Q :
  to_val e1 = Some v   wp E (gsubst e2 x e1) Q  wp E (Let x e1 e2) Q.
Proof. apply wp_lam. Qed.

Lemma wp_seq E e1 e2 Q : wp E e1 (λ _,  wp E e2 Q)  wp E (Seq e1 e2) Q.
Proof.
  rewrite -(wp_bind [LetCtx "" e2]). apply wp_mono=>v.
  by rewrite -wp_let //= ?gsubst_correct ?subst_empty ?to_of_val.
Qed.

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

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

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

End derived.