derived.v 2.22 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).
Ralf Jung's avatar
Ralf Jung committed
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
Lemma wp_lam' E x ef e v Φ :
20
21
  to_val e = Some v 
   || subst ef x v @ E {{ Φ }}  || App (Lam x ef) e @ E {{ Φ }}.
22
Proof. intros. by rewrite -wp_rec' ?subst_empty. Qed.
23

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

29
30
Lemma wp_seq E e1 e2 Φ :
  || e1 @ E {{ λ _,  || e2 @ E {{ Φ }} }}  || Seq e1 e2 @ E {{ Φ }}.
31
32
Proof.
  rewrite -(wp_bind [LetCtx "" e2]). apply wp_mono=>v.
33
  by rewrite -wp_let' //= ?to_of_val ?subst_empty.
34
35
Qed.

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

39
Lemma wp_le E (n1 n2 : Z) P Φ :
40
41
42
  (n1  n2  P   Φ (LitV (LitBool true))) 
  (n2 < n1  P   Φ (LitV (LitBool false))) 
  P  || BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
43
44
45
46
47
Proof.
  intros. rewrite -wp_bin_op //; [].
  destruct (bool_decide_reflect (n1  n2)); by eauto with omega.
Qed.

48
Lemma wp_lt E (n1 n2 : Z) P Φ :
49
50
51
  (n1 < n2  P   Φ (LitV (LitBool true))) 
  (n2  n1  P   Φ (LitV (LitBool false))) 
  P  || BinOp LtOp (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_eq E (n1 n2 : Z) P Φ :
58
59
60
  (n1 = n2  P   Φ (LitV (LitBool true))) 
  (n1  n2  P   Φ (LitV (LitBool false))) 
  P  || BinOp EqOp (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.
End derived.