derived.v 2.67 KB
Newer Older
1
From heap_lang Require Export lifting.
2 3 4
Import uPred.

(** Define some derived forms, and derived lemmas about them. *)
5
Notation Lam x e := (Rec BAnon x e).
6
Notation Let x e1 e2 := (App (Lam x e2) e1).
7 8
Notation Seq e1 e2 := (Let BAnon e1 e2).
Notation LamV x e := (RecV BAnon x e).
9
Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
10
Notation SeqCtx e2 := (LetCtx BAnon e2).
Ralf Jung's avatar
Ralf Jung committed
11
Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
12
Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)).
13 14

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

(** Proof rules for the sugar *)
20
Lemma wp_lam E x ef e v Φ :
21
  to_val e = Some v 
22
   || subst' x e ef @ E {{ Φ }}  || App (Lam x ef) e @ E {{ Φ }}.
23
Proof. intros. by rewrite -wp_rec. Qed.
24

25
Lemma wp_let E x e1 e2 v Φ :
26
  to_val e1 = Some v 
27
   || subst' x e1 e2 @ E {{ Φ }}  || Let x e1 e2 @ E {{ Φ }}.
28
Proof. apply wp_lam. Qed.
29

30 31 32
Lemma wp_seq E e1 e2 v Φ :
  to_val e1 = Some v 
   || e2 @ E {{ Φ }}  || Seq e1 e2 @ E {{ Φ }}.
33
Proof. intros ?. by rewrite -wp_let. Qed.
34

35
Lemma wp_skip E Φ :  Φ (LitV LitUnit)  || Skip @ E {{ Φ }}.
36
Proof. rewrite -wp_seq // -wp_value //. Qed.
Ralf Jung's avatar
Ralf Jung committed
37

38 39
Lemma wp_match_inl E e0 v0 x1 e1 x2 e2 Φ :
  to_val e0 = Some v0 
40 41
   || subst' x1 e0 e1 @ E {{ Φ }}  || Match (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
Proof. intros. by rewrite -wp_case_inl // -[X in _  X]later_intro -wp_let. Qed.
42 43 44

Lemma wp_match_inr E e0 v0 x1 e1 x2 e2 Φ :
  to_val e0 = Some v0 
45 46
   || subst' x2 e0 e2 @ E {{ Φ }}  || Match (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
Proof. intros. by rewrite -wp_case_inr // -[X in _  X]later_intro -wp_let. Qed.
47

48
Lemma wp_le E (n1 n2 : Z) P Φ :
49 50 51
  (n1  n2  P   Φ (LitV (LitBool true))) 
  (n2 < n1  P   Φ (LitV (LitBool false))) 
  P  || BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
52 53 54 55 56
Proof.
  intros. rewrite -wp_bin_op //; [].
  destruct (bool_decide_reflect (n1  n2)); by eauto with omega.
Qed.

57
Lemma wp_lt E (n1 n2 : Z) P Φ :
58 59 60
  (n1 < n2  P   Φ (LitV (LitBool true))) 
  (n2  n1  P   Φ (LitV (LitBool false))) 
  P  || BinOp LtOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
61 62 63 64 65
Proof.
  intros. rewrite -wp_bin_op //; [].
  destruct (bool_decide_reflect (n1 < n2)); by eauto with omega.
Qed.

66
Lemma wp_eq E (n1 n2 : Z) P Φ :
67 68 69
  (n1 = n2  P   Φ (LitV (LitBool true))) 
  (n1  n2  P   Φ (LitV (LitBool false))) 
  P  || BinOp EqOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
70 71 72 73 74
Proof.
  intros. rewrite -wp_bin_op //; [].
  destruct (bool_decide_reflect (n1 = n2)); by eauto with omega.
Qed.
End derived.