lifting.v 5.31 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
Require Import prelude.gmap iris.lifting.
Ralf Jung's avatar
Ralf Jung committed
2
Require Export iris.weakestpre heap_lang.heap_lang_tactics.
3
Import uPred.
4
Import heap_lang.
5
Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
6

7
Section lifting.
8 9
Context {Σ : iFunctor}.
Implicit Types P : iProp heap_lang Σ.
10 11
Implicit Types Q : val  iProp heap_lang Σ.
Implicit Types K : ectx.
Ralf Jung's avatar
Ralf Jung committed
12 13

(** Bind. *)
14
Lemma wp_bind {E e} K Q :
15
  wp E e (λ v, wp E (fill K (of_val v)) Q)  wp E (fill K e) Q.
16
Proof. apply wp_bind. Qed.
Ralf Jung's avatar
Ralf Jung committed
17

18
(** Base axioms for core primitives of the language: Stateful reductions. *)
19
Lemma wp_alloc_pst E σ e v Q :
20 21
  to_val e = Some v 
  (ownP σ   ( l, (σ !! l = None)  ownP (<[l:=v]>σ) - Q (LocV l)))
22
        wp E (Alloc e) Q.
23
Proof.
24 25 26
  (* TODO RJ: This works around ssreflect bug #22. *)
  intros. set (φ v' σ' ef :=  l, ef = @None expr  v' = LocV l  σ' = <[l:=v]>σ  σ !! l = None).
  rewrite -(wp_lift_atomic_step (Alloc e) φ σ) // /φ;
Ralf Jung's avatar
Ralf Jung committed
27
    last by intros; inv_step; eauto 8.
28
  apply sep_mono, later_mono; first done.
29 30
  apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef.
  apply wand_intro_l.
31
  rewrite always_and_sep_l' -associative -always_and_sep_l'.
32 33
  apply const_elim_l=>-[l [-> [-> [-> ?]]]].
  by rewrite (forall_elim l) right_id const_equiv // left_id wand_elim_r.
34
Qed.
35

36
Lemma wp_load_pst E σ l v Q :
Ralf Jung's avatar
Ralf Jung committed
37
  σ !! l = Some v 
38
  (ownP σ   (ownP σ - Q v))  wp E (Load (Loc l)) Q.
Ralf Jung's avatar
Ralf Jung committed
39
Proof.
40
  intros; rewrite -(wp_lift_atomic_det_step σ v σ None) ?right_id //;
41
    last (by intros; inv_step; eauto).
Ralf Jung's avatar
Ralf Jung committed
42
Qed.
43

44
Lemma wp_store_pst E σ l e v v' Q :
45 46
  to_val e = Some v  σ !! l = Some v' 
  (ownP σ   (ownP (<[l:=v]>σ) - Q LitUnitV))  wp E (Store (Loc l) e) Q.
Ralf Jung's avatar
Ralf Jung committed
47
Proof.
48
  intros.
49
  rewrite -(wp_lift_atomic_det_step σ LitUnitV (<[l:=v]>σ) None) ?right_id //;
50
    last by intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
51
Qed.
52

53
Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Q :
54 55
  to_val e1 = Some v1  to_val e2 = Some v2  σ !! l = Some v'  v'  v1 
  (ownP σ   (ownP σ - Q LitFalseV))  wp E (Cas (Loc l) e1 e2) Q.
Ralf Jung's avatar
Ralf Jung committed
56
Proof.
57
  intros; rewrite -(wp_lift_atomic_det_step σ LitFalseV σ None) ?right_id //;
58
    last by intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
59
Qed.
60

61
Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Q :
62 63
  to_val e1 = Some v1  to_val e2 = Some v2  σ !! l = Some v1 
  (ownP σ   (ownP (<[l:=v2]>σ) - Q LitTrueV))  wp E (Cas (Loc l) e1 e2) Q.
Ralf Jung's avatar
Ralf Jung committed
64
Proof.
65
  intros.
66
  rewrite -(wp_lift_atomic_det_step σ LitTrueV (<[l:=v2]>σ) None) ?right_id //;
67
    last by intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
68 69
Qed.

70 71
(** Base axioms for core primitives of the language: Stateless reductions *)
Lemma wp_fork E e :
72
   wp (Σ:=Σ) coPset_all e (λ _, True)  wp E (Fork e) (λ v, (v = LitUnitV)).
73
Proof.
74
  rewrite -(wp_lift_pure_det_step (Fork e) LitUnit (Some e)) //=;
75
    last by intros; inv_step; eauto.
76 77
  apply later_mono, sep_intro_True_l; last done.
  by rewrite -(wp_value' _ _ LitUnit) //; apply const_intro.
78
Qed.
79

80
Lemma wp_rec E ef e v Q :
81 82
  to_val e = Some v 
   wp E ef.[Rec ef, e /] Q  wp E (App (Rec ef) e) Q.
83
Proof.
84 85
  intros; rewrite -(wp_lift_pure_det_step (App _ _) ef.[Rec ef, e /] None)
                     ?right_id //=;
86
    last by intros; inv_step; eauto.
87
Qed.
88

89
Lemma wp_plus E n1 n2 Q :
90
   Q (LitNatV (n1 + n2))  wp E (Plus (LitNat n1) (LitNat n2)) Q.
91
Proof.
92
  rewrite -(wp_lift_pure_det_step (Plus _ _) (LitNat (n1 + n2)) None) ?right_id //;
93 94
    last by intros; inv_step; eauto.
  by rewrite -wp_value'.
Ralf Jung's avatar
Ralf Jung committed
95
Qed.
96

97
Lemma wp_le_true E n1 n2 Q :
Ralf Jung's avatar
Ralf Jung committed
98
  n1  n2 
99
   Q LitTrueV  wp E (Le (LitNat n1) (LitNat n2)) Q.
Ralf Jung's avatar
Ralf Jung committed
100
Proof.
101
  intros; rewrite -(wp_lift_pure_det_step (Le _ _) LitTrue None) ?right_id //;
Ralf Jung's avatar
Ralf Jung committed
102
    last by intros; inv_step; eauto with omega.
103
  by rewrite -wp_value'.
Ralf Jung's avatar
Ralf Jung committed
104
Qed.
105

106
Lemma wp_le_false E n1 n2 Q :
Ralf Jung's avatar
Ralf Jung committed
107
  n1 > n2 
108
   Q LitFalseV  wp E (Le (LitNat n1) (LitNat n2)) Q.
Ralf Jung's avatar
Ralf Jung committed
109
Proof.
110
  intros; rewrite -(wp_lift_pure_det_step (Le _ _) LitFalse None) ?right_id //;
Ralf Jung's avatar
Ralf Jung committed
111
    last by intros; inv_step; eauto with omega.
112
  by rewrite -wp_value'.
113
Qed.
114

115
Lemma wp_fst E e1 v1 e2 v2 Q :
116
  to_val e1 = Some v1  to_val e2 = Some v2 
117
  Q v1  wp E (Fst (Pair e1 e2)) Q.
Ralf Jung's avatar
Ralf Jung committed
118
Proof.
119
  intros; rewrite -(wp_lift_pure_det_step (Fst _) e1 None) ?right_id //;
120 121
    last by intros; inv_step; eauto.
  by rewrite -wp_value'.
Ralf Jung's avatar
Ralf Jung committed
122
Qed.
123

124
Lemma wp_snd E e1 v1 e2 v2 Q :
125 126
  to_val e1 = Some v1  to_val e2 = Some v2 
   Q v2  wp E (Snd (Pair e1 e2)) Q.
Ralf Jung's avatar
Ralf Jung committed
127
Proof.
128
  intros; rewrite -(wp_lift_pure_det_step (Snd _) e2 None) ?right_id //;
129 130
    last by intros; inv_step; eauto.
  by rewrite -wp_value'.
Ralf Jung's avatar
Ralf Jung committed
131
Qed.
132

133
Lemma wp_case_inl E e0 v0 e1 e2 Q :
134 135
  to_val e0 = Some v0 
   wp E e1.[e0/] Q  wp E (Case (InjL e0) e1 e2) Q.
Ralf Jung's avatar
Ralf Jung committed
136
Proof.
137
  intros; rewrite -(wp_lift_pure_det_step (Case _ _ _) e1.[e0/] None) ?right_id //;
138
    last by intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
139
Qed.
140

141
Lemma wp_case_inr E e0 v0 e1 e2 Q :
142 143
  to_val e0 = Some v0 
   wp E e2.[e0/] Q  wp E (Case (InjR e0) e1 e2) Q.
Ralf Jung's avatar
Ralf Jung committed
144
Proof.
145
  intros; rewrite -(wp_lift_pure_det_step (Case _ _ _) e2.[e0/] None) ?right_id //;
146
    last by intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
147
Qed.
148

Ralf Jung's avatar
Ralf Jung committed
149
(** Some derived stateless axioms *)
150
Lemma wp_le E n1 n2 P Q :
151 152
  (n1  n2  P   Q LitTrueV) 
  (n1 > n2  P   Q LitFalseV) 
153
  P  wp E (Le (LitNat n1) (LitNat n2)) Q.
Ralf Jung's avatar
Ralf Jung committed
154
Proof.
155 156
  intros; destruct (decide (n1  n2)).
  * rewrite -wp_le_true; auto.
Ralf Jung's avatar
Ralf Jung committed
157
  * rewrite -wp_le_false; auto with omega.
Ralf Jung's avatar
Ralf Jung committed
158
Qed.
159

160
End lifting.