lifting.v 5.85 KB
Newer Older
1
From program_logic Require Export weakestpre.
2
From heap_lang Require Export lang.
3
4
5
From program_logic Require Import lifting.
From program_logic Require Import ownership. (* for ownP *)
From heap_lang Require Import tactics.
6
7
Export heap_lang. (* Prefer heap_lang names over language names. *)
Import uPred.
8
Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
9

10
Section lifting.
11
Context {Σ : iFunctor}.
12
13
Implicit Types P Q : iProp heap_lang Σ.
Implicit Types Φ : val  iProp heap_lang Σ.
14
Implicit Types K : ectx.
15
Implicit Types ef : option expr.
Ralf Jung's avatar
Ralf Jung committed
16
17

(** Bind. *)
18
Lemma wp_bind {E e} K Φ :
19
  || e @ E {{ λ v, || fill K (of_val v) @ E {{ Φ }}}}  || fill K e @ E {{ Φ }}.
20
Proof. apply weakestpre.wp_bind. Qed.
Ralf Jung's avatar
Ralf Jung committed
21
22
23
24
25

Lemma wp_bindi {E e} Ki Φ :
  || e @ E {{ λ v, || fill_item Ki (of_val v) @ E {{ Φ }}}}
      || fill_item Ki e @ E {{ Φ }}.
Proof. apply weakestpre.wp_bind. Qed.
Ralf Jung's avatar
Ralf Jung committed
26

27
(** Base axioms for core primitives of the language: Stateful reductions. *)
28
Lemma wp_alloc_pst E σ e v Φ :
29
  to_val e = Some v 
30
  (ownP σ   ( l, σ !! l = None  ownP (<[l:=v]>σ) - Φ (LocV l)))
31
   || Alloc e @ E {{ Φ }}.
32
Proof.
33
  (* TODO RJ: This works around ssreflect bug #22. *)
34
35
  intros. set (φ v' σ' ef :=  l,
    ef = None  v' = LocV l  σ' = <[l:=v]>σ  σ !! l = None).
36
  rewrite -(wp_lift_atomic_step (Alloc e) φ σ) // /φ;
Ralf Jung's avatar
Ralf Jung committed
37
    last by intros; inv_step; eauto 8.
38
  apply sep_mono, later_mono; first done.
39
40
  apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef.
  apply wand_intro_l.
41
  rewrite always_and_sep_l -assoc -always_and_sep_l.
42
43
  apply const_elim_l=>-[l [-> [-> [-> ?]]]].
  by rewrite (forall_elim l) right_id const_equiv // left_id wand_elim_r.
44
Qed.
45

46
Lemma wp_load_pst E σ l v Φ :
Ralf Jung's avatar
Ralf Jung committed
47
  σ !! l = Some v 
48
  (ownP σ   (ownP σ - Φ v))  || Load (Loc l) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
49
Proof.
50
51
  intros. rewrite -(wp_lift_atomic_det_step σ v σ None) ?right_id //;
    last by intros; inv_step; eauto using to_of_val.
Ralf Jung's avatar
Ralf Jung committed
52
Qed.
53

54
Lemma wp_store_pst E σ l e v v' Φ :
55
  to_val e = Some v  σ !! l = Some v' 
56
57
  (ownP σ   (ownP (<[l:=v]>σ) - Φ (LitV LitUnit)))
   || Store (Loc l) e @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
58
Proof.
59
  intros. rewrite -(wp_lift_atomic_det_step σ (LitV LitUnit) (<[l:=v]>σ) None)
60
    ?right_id //; last by intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
61
Qed.
62

63
Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Φ :
64
  to_val e1 = Some v1  to_val e2 = Some v2  σ !! l = Some v'  v'  v1 
65
66
  (ownP σ   (ownP σ - Φ (LitV $ LitBool false)))
   || Cas (Loc l) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
67
Proof.
Ralf Jung's avatar
Ralf Jung committed
68
  intros. rewrite -(wp_lift_atomic_det_step σ (LitV $ LitBool false) σ None)
69
    ?right_id //; last by intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
70
Qed.
71

72
Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ :
73
  to_val e1 = Some v1  to_val e2 = Some v2  σ !! l = Some v1 
74
  (ownP σ   (ownP (<[l:=v2]>σ) - Φ (LitV $ LitBool true)))
75
   || Cas (Loc l) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
76
Proof.
77
78
  intros. rewrite -(wp_lift_atomic_det_step σ (LitV $ LitBool true)
    (<[l:=v2]>σ) None) ?right_id //; last by intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
79
80
Qed.

81
(** Base axioms for core primitives of the language: Stateless reductions *)
82
Lemma wp_fork E e Φ :
83
  ( Φ (LitV LitUnit)   || e {{ λ _, True }})  || Fork e @ E {{ Φ }}.
84
Proof.
85
  rewrite -(wp_lift_pure_det_step (Fork e) (Lit LitUnit) (Some e)) //=;
86
    last by intros; inv_step; eauto.
87
  rewrite later_sep -(wp_value _ _ (Lit _)) //.
88
Qed.
89

90
91
(* For the lemmas involving substitution, we only derive a preliminary version.
   The final version is defined in substitution.v. *)
92
Lemma wp_rec' E f x e1 e2 v Φ :
93
  to_val e2 = Some v 
94
95
   || subst (subst e1 f (RecV f x e1)) x v @ E {{ Φ }}
   || App (Rec f x e1) e2 @ E {{ Φ }}.
96
Proof.
97
  intros. rewrite -(wp_lift_pure_det_step (App _ _)
98
    (subst (subst e1 f (RecV f x e1)) x v) None) ?right_id //=;
99
    intros; inv_step; eauto.
100
Qed.
101

102
Lemma wp_un_op E op l l' Φ :
103
  un_op_eval op l = Some l' 
104
   Φ (LitV l')  || UnOp op (Lit l) @ E {{ Φ }}.
105
Proof.
106
  intros. rewrite -(wp_lift_pure_det_step (UnOp op _) (Lit l') None)
107
    ?right_id -?wp_value //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
108
Qed.
109

110
Lemma wp_bin_op E op l1 l2 l' Φ :
111
  bin_op_eval op l1 l2 = Some l' 
112
   Φ (LitV l')  || BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
113
Proof.
114
  intros Heval. rewrite -(wp_lift_pure_det_step (BinOp op _ _) (Lit l') None)
115
    ?right_id -?wp_value //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
116
Qed.
117

118
Lemma wp_if_true E e1 e2 Φ :
119
   || e1 @ E {{ Φ }}  || If (Lit (LitBool true)) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
120
Proof.
121
  rewrite -(wp_lift_pure_det_step (If _ _ _) e1 None)
122
    ?right_id //; intros; inv_step; eauto.
123
124
Qed.

125
Lemma wp_if_false E e1 e2 Φ :
126
   || e2 @ E {{ Φ }}  || If (Lit (LitBool false)) e1 e2 @ E {{ Φ }}.
127
128
Proof.
  rewrite -(wp_lift_pure_det_step (If _ _ _) e2 None)
129
    ?right_id //; intros; inv_step; eauto.
130
Qed.
131

132
Lemma wp_fst E e1 v1 e2 v2 Φ :
133
  to_val e1 = Some v1  to_val e2 = Some v2 
134
   Φ v1  || Fst (Pair e1 e2) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
135
Proof.
136
  intros. rewrite -(wp_lift_pure_det_step (Fst _) e1 None)
137
    ?right_id -?wp_value //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
138
Qed.
139

140
Lemma wp_snd E e1 v1 e2 v2 Φ :
141
  to_val e1 = Some v1  to_val e2 = Some v2 
142
   Φ v2  || Snd (Pair e1 e2) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
143
Proof.
144
  intros. rewrite -(wp_lift_pure_det_step (Snd _) e2 None)
145
    ?right_id -?wp_value //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
146
Qed.
147

148
Lemma wp_case_inl' E e0 v0 x1 e1 x2 e2 Φ :
149
  to_val e0 = Some v0 
150
   || subst e1 x1 v0 @ E {{ Φ }}  || Case (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
151
Proof.
152
153
  intros. rewrite -(wp_lift_pure_det_step (Case _ _ _ _ _)
    (subst e1 x1 v0) None) ?right_id //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
154
Qed.
155

156
Lemma wp_case_inr' E e0 v0 x1 e1 x2 e2 Φ :
157
  to_val e0 = Some v0 
158
   || subst e2 x2 v0 @ E {{ Φ }}  || Case (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
159
Proof.
160
161
  intros. rewrite -(wp_lift_pure_det_step (Case _ _ _ _ _)
    (subst e2 x2 v0) None) ?right_id //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
162
Qed.
163

164
End lifting.