derived.v 2.83 KB
Newer Older
1
From iris.heap_lang Require Export rules.
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 `{heapG Σ}.
16 17
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val  iProp Σ.
18 19

(** Proof rules for the sugar *)
20 21 22 23 24
Lemma wp_lam E x elam e1 e2 Φ :
  e1 = Lam x elam 
  is_Some (to_val e2) 
  Closed (x :b: []) elam 
   WP subst' x e2 elam @ E {{ Φ }}  WP App e1 e2 @ E {{ Φ }}.
25
Proof. intros. by rewrite -(wp_rec _ BAnon) //. Qed.
26

27 28
Lemma wp_let E x e1 e2 Φ :
  is_Some (to_val e1)  Closed (x :b: []) e2 
29
   WP subst' x e1 e2 @ E {{ Φ }}  WP Let x e1 e2 @ E {{ Φ }}.
30
Proof. by apply wp_lam. Qed.
31

32 33
Lemma wp_seq E e1 e2 Φ :
  is_Some (to_val e1)  Closed [] e2 
34
   WP e2 @ E {{ Φ }}  WP Seq e1 e2 @ E {{ Φ }}.
35
Proof. intros ??. by rewrite -wp_let. Qed.
36

37
Lemma wp_skip E Φ :  Φ (LitV LitUnit)  WP Skip @ E {{ Φ }}.
38
Proof. rewrite -wp_seq; last eauto. by rewrite -wp_value. Qed.
Ralf Jung's avatar
Ralf Jung committed
39

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

45 46
Lemma wp_match_inr E e0 x1 e1 x2 e2 Φ :
  is_Some (to_val e0)  Closed (x2 :b: []) e2 
47
   WP subst' x2 e0 e2 @ E {{ Φ }}  WP Match (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
48
Proof. intros. by rewrite -wp_case_inr // -[X in _  X]later_intro -wp_let. Qed.
49

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

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

68 69
Lemma wp_eq E e1 e2 v1 v2 P Φ :
  to_val e1 = Some v1  to_val e2 = Some v2 
70 71
  (v1 = v2  P   Φ (LitV (LitBool true))) 
  (v1  v2  P   Φ (LitV (LitBool false))) 
72
  P  WP BinOp EqOp e1 e2 @ E {{ Φ }}.
73 74
Proof.
  intros. rewrite -wp_bin_op //; [].
75
  destruct (bool_decide_reflect (v1 = v2)); by eauto.
76 77
Qed.
End derived.