denv.v 35.9 KB
Newer Older
Dan Frumin's avatar
Dan Frumin committed
1
(** * Reified environments *)
2
From iris_c.vcgen Require Export dcexpr.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
From iris_c.lib Require Export Q.
4
Local Open Scope nat_scope.
Léon Gondelman's avatar
denv  
Léon Gondelman committed
5

Robbert Krebbers's avatar
Robbert Krebbers committed
6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170
(** The reified environment. The `DenvItem` at index `i` in the list
    denotes the value for the reified location under the index `i`. *)
Record denv_item := DenvItem {
  denv_level : lvl;
  denv_frac  : Q;
  denv_dval  : dval
}.
Add Printing Constructor denv_item.
Notation denv := (list (option denv_item)).

(** A reified environment is well-formed if every item is well
    formed and all the indices are contained in the set of known
    locations. *)
Definition denv_item_wf (E : known_locs) (dio : denv_item) : bool :=
  bool_decide (0 < denv_frac dio)%Q && dval_wf E (denv_dval dio).
Arguments denv_item_wf _ !_ /.

Fixpoint denv_wf_val (E : known_locs) (m : denv) : bool :=
  match m with
  | [] => true
  | dio :: m' => from_option (denv_item_wf E) true dio && denv_wf_val E m'
  end.

Definition denv_wf_len (E : known_locs) (m : denv) : bool :=
  bool_decide (length m  length E)%nat.

Definition denv_wf (E : known_locs) (m : denv) : bool :=
  denv_wf_val E m && denv_wf_len E m.

(** ** Merging of two reified environments *)
Definition denv_item_opt_merge
    (dio1 dio2 : option denv_item) : option denv_item :=
  match dio1, dio2 with
  | None, dio | dio, None => dio
  | Some di1, Some di2 =>
     Some (DenvItem (lvl_op (denv_level di1) (denv_level di2))
                    (denv_frac di1 + denv_frac di2)
                    (denv_dval di1))
  end.

Fixpoint denv_merge (m1 m2 : denv) : denv :=
  match m1, m2 with
  | m, [] | [], m => m
  | dio1 :: m1', dio2 :: m2' =>
    denv_item_opt_merge dio1 dio2 :: denv_merge m1' m2'
  end.
Arguments denv_merge !_ !_ /.

Definition denv_stack_merge (ms : list denv) : denv :=
  foldr denv_merge [] ms.

(** ** Operations on the reified environments.
    Singleton, insertion, two types of deletion. *)
Fixpoint denv_singleton (i : nat) (lv : lvl) (q : Q) (dv : dval) : denv :=
  match i with
  | O => [Some (DenvItem lv q dv)]
  | S i => None :: denv_singleton i lv q dv
  end.

Fixpoint denv_insert (i : nat) (x : lvl) (q : Q) (dv : dval)
    (m : denv) {struct m} : denv :=
  match m with
  | [] => denv_singleton i x q dv
  | dio :: m' =>
     match i with
     | O =>
        match dio with
        | None => Some (DenvItem x q dv) :: m'
        | Some di =>
           Some (DenvItem (lvl_op (denv_level di) x) (denv_frac di + q) dv) :: m'
        end
     | S i => dio :: denv_insert i x q dv m'
     end
  end.

(** Removing a permission for reading.
    If `(dLoc i) ↦U{q} v` is present in the environment,
    then remove half of it and return `(q,v)`. *)
Fixpoint denv_delete_frac (i : nat) (m : denv) : option (denv * Q * dval) :=
  match m with
  | [] => None
  | dio :: m' =>
     match i with
     | O   =>
        ''(DenvItem lv q dv)  dio;
        guard (lv = ULvl);
        Some (Some (DenvItem lv (q / 2) dv) :: m', (q / 2)%Q, dv)
     | S i => ''(mf, q, dv)  denv_delete_frac i m'; Some (dio :: mf, q, dv)
     end
  end.

Fixpoint denv_delete_full_aux (i : nat) (m : denv) : option (denv * Q * dval) :=
  match m with
  | [] => None
  | dio :: m' =>
     match i with
     | O =>
        ''(DenvItem lv q dv)  dio;
        guard (lv = ULvl);
        Some (None :: m', q, dv)
     | S i => ''(mf, q, dv)  denv_delete_full_aux i m'; Some (dio :: mf, q, dv)
    end
  end.

Definition denv_lookup (i : nat) (m : denv) : option (Q * dval) :=
  ''(m', q, dv)  denv_delete_full_aux i m;
  Some (q, dv).

(** Removing a permission for writing.
    If `(dLoc i) ↦U v` is present in the environment,
    then remove it and return `v`. *)
Definition denv_delete_full (i : nat) (m : denv) : option (denv * dval) :=
  ''(m', q, dv)  denv_delete_full_aux i m;
  guard (q == 1)%Q;
  Some (m', dv).
Arguments denv_delete_full !_ !_ /.

(** Versions of `denv_delete_frac` and `denv_delete_full` for stacks
of environments. *)
Fixpoint denv_delete_frac_stack (i : nat)
    (ms : list denv) : option (list denv * Q * dval) :=
  match ms with
  | [] => None
  | m :: ms' =>
     match denv_delete_frac i m with
     | Some (m', q, dv) => Some (m' :: ms', q, dv)
     | None => ''(ms1, q, dv)  denv_delete_frac_stack i ms'; Some (m :: ms1, q, dv)
     end
  end.

Fixpoint denv_delete_full_stack_aux (i : nat)
    (ms : list denv) : option (list denv * Q * dval) :=
  match ms with
  | [] => None
  | m :: ms' =>
     match denv_delete_full_aux i m,denv_delete_full_stack_aux i ms' with
     | None, None => None
     | None, Some (ms1, q1, dv1) => Some (m :: ms1, q1, dv1)
     | Some (m1, q2, dv2), None => Some (m1 :: ms', q2, dv2)
     | Some (m1, q2, dv2), Some (ms1, q1, dv1) =>
        Some (m1 :: ms1, (q1 + q2)%Q, dv2)
     end
  end.

Definition denv_delete_frac_2 (i : nat)
    (ms : list denv) (m : denv) : option (list denv * denv * Q * dval) :=
  match denv_delete_frac_stack i ms with
  | Some (ms', q, dv) => Some (ms', m, q, dv)
  | None => ''(m', q, dv)  denv_delete_frac i m; Some (ms, m', q, dv)
  end.

Definition denv_delete_full_2 (i : nat)
    (ms : list denv) (m : denv) : option (list denv * denv * dval) :=
  match denv_delete_full_stack_aux i ms, denv_delete_full_aux i m with
  | None, Some (m', q, dv) => guard (q = 1)%Qp; Some (ms, m', dv)
  | Some (ms', q, dv), None => guard (q = 1)%Qp; Some (ms', m, dv)
  | Some (ms', q1, dv), Some (m', q2, _) =>
     guard (q1 + q2 = 1)%Q; Some (ms', m', dv)
  | _, _ => None
  end.

(** Turn all `(dLoc i) ↦L v` into `(dLoc i) ↦U v`. *)
Definition denv_unlock (m : denv) : denv :=
  map (λ dio, ''(DenvItem _ q dv)  dio; Some (DenvItem ULvl q dv)) m.

171
Definition denv_item_interp `{cmonadG Σ} (E : known_locs)
Robbert Krebbers's avatar
Robbert Krebbers committed
172 173 174 175 176 177
    (i : nat) (dio : denv_item) : iProp Σ :=
  (dloc_var_interp E i
     C[denv_level dio]{Q_to_Qp (denv_frac dio)}
   dval_interp E (denv_dval dio))%I.
Arguments denv_item_interp {_ _} _ _ !_ /.

178
Definition denv_interp `{cmonadG Σ} (E : known_locs) (m : denv) : iProp Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
179 180 181 182
  ([ list] i  dio  m, from_option (denv_item_interp E i) True dio)%I.

(** `denv_stack_interp E ms1 ms2 P`
    ~ `(ms1.n -∗ ms2.n ∗ (.... ∗ (ms1.1 -∗ ms2.1 ∗ P)))` *)
183
Fixpoint denv_stack_interp `{cmonadG Σ} (E : known_locs)
Robbert Krebbers's avatar
Robbert Krebbers committed
184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201
    (ms1 ms2 : list denv) (P : iProp Σ) :=
  match ms1, ms2 with
  | m :: ms, m' :: ms' =>
     denv_stack_interp E ms ms' (denv_interp E m - denv_interp E m'  P)
  | [], [] => P
  | _, _ => False
  end%I.
Arguments denv_stack_interp {_ _} _ !_ !_ _%I.

Definition pop_stack (ms : list denv) : option (list denv * denv) :=
  match ms with
  | [] => None
  | m :: ms => Some (ms, m)
  end.
Arguments pop_stack !_ /.

(** `wand_denv_interp_aux E [l1:=v1,l2:=v2,...ln:=vn] Φ`
     = `l1 ↦C v1 -∗ l2 ↦C v2 -∗ ... -∗ ln ↦C vn -∗ Φ` *)
202
Fixpoint wand_denv_interp_aux `{cmonadG Σ}
Robbert Krebbers's avatar
Robbert Krebbers committed
203 204 205 206 207 208 209 210
     (E: known_locs) (m : denv) (Φ : iProp Σ) (i : nat) : iProp Σ :=
  match m with
  | [] => Φ
  | None :: m' => wand_denv_interp_aux E m' Φ (S i)
  | Some dio :: m' =>
     denv_item_interp E i dio - wand_denv_interp_aux E m' Φ (S i)
  end%I.

211
Definition wand_denv_interp `{cmonadG Σ}
Robbert Krebbers's avatar
Robbert Krebbers committed
212 213 214
     (E: known_locs) (m : denv) (Φ : iProp Σ) : iProp Σ :=
  wand_denv_interp_aux E m Φ O.
Arguments wand_denv_interp {_ _} _ !_ _%I /.
Dan Frumin's avatar
Dan Frumin committed
215

Léon Gondelman's avatar
denv  
Léon Gondelman committed
216
Section denv.
217
  Context `{cmonadG Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
218 219 220
  Local Arguments Q_to_Qp : simpl never.
  Hint Resolve Q_plus_nonneg.
  Hint Resolve Q_div_nonneg.
221

Robbert Krebbers's avatar
Robbert Krebbers committed
222 223 224
  (* Well-formedness stuff *)
  Ltac simplify :=
    intros; repeat (case_match || simplify_option_eq).
Robbert Krebbers's avatar
Robbert Krebbers committed
225

Robbert Krebbers's avatar
Robbert Krebbers committed
226 227 228 229 230 231 232 233
  Lemma denv_wf_len_mono E E' m :
    denv_wf_len E m  E `prefix_of` E'  denv_wf_len E' m.
  Proof. rewrite /denv_wf_len !bool_decide_spec=> ? /prefix_length. lia. Qed.
  Lemma denv_item_wf_mono E E' dio :
    denv_item_wf E dio  E `prefix_of` E'  denv_item_wf E' dio.
  Proof. rewrite /denv_item_wf. naive_solver eauto using dval_wf_mono. Qed.
  Lemma denv_wf_val_mono E E' m :
    denv_wf_val E m  E `prefix_of` E'  denv_wf_val E' m.
Dan Frumin's avatar
Dan Frumin committed
234
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
235
    induction m as [|[?|] ?]; naive_solver eauto using denv_item_wf_mono.
Dan Frumin's avatar
Dan Frumin committed
236
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
237 238
  Lemma denv_wf_mono E E' m :
    denv_wf E m  E `prefix_of` E'  denv_wf E' m.
Dan Frumin's avatar
Dan Frumin committed
239
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
240
    rewrite /denv_wf; naive_solver eauto using denv_wf_len_mono, denv_wf_val_mono.
Dan Frumin's avatar
Dan Frumin committed
241
  Qed.
242

Robbert Krebbers's avatar
Robbert Krebbers committed
243 244
  Lemma denv_wf_val_lookup_wf E m k di :
    m !! k = Some (Some di)  denv_wf_val E m  dval_wf E (denv_dval di).
Dan Frumin's avatar
Dan Frumin committed
245
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
246 247
    revert k. induction m; intros [|?];
      simplify; unfold denv_item_wf in *; naive_solver.
Dan Frumin's avatar
Dan Frumin committed
248
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
249 250 251 252 253
  Lemma denv_wf_lookup_wf E m k di :
    m !! k = Some (Some di)  denv_wf E m  dval_wf E (denv_dval di).
  Proof. rewrite /denv_wf. naive_solver eauto using denv_wf_val_lookup_wf. Qed.
  Lemma denv_wf_lookup_dloc_wf E m k di :
    m !! k = Some (Some di)  denv_wf E m  dloc_var_wf E k.
Dan Frumin's avatar
Dan Frumin committed
254
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
255 256
    rewrite /denv_wf /denv_wf_len /dloc_var_wf. intros ?%lookup_lt_Some.
    rewrite bool_decide_spec lookup_lt_is_Some. naive_solver eauto with lia.
Dan Frumin's avatar
Dan Frumin committed
257
  Qed.
258

Robbert Krebbers's avatar
Robbert Krebbers committed
259 260 261
  Lemma denv_interp_mono E E' m :
    denv_wf E m  E `prefix_of` E' 
    denv_interp E m - denv_interp E' m.
Dan Frumin's avatar
Dan Frumin committed
262
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
263 264 265 266
    iIntros (??) "H". iApply (big_sepL_impl with "H").
    iIntros "!>" (k [?|] Hk) "//=". rewrite /denv_item_interp.
    rewrite (dloc_var_interp_mono _ E') //; eauto using denv_wf_lookup_dloc_wf.
    rewrite (dval_interp_mono _ E') //; eauto using denv_wf_lookup_wf.
Dan Frumin's avatar
Dan Frumin committed
267
  Qed.
268

Robbert Krebbers's avatar
Robbert Krebbers committed
269 270
  Lemma denv_wf_val_merge E m1 m2 :
    denv_wf_val E m1  denv_wf_val E m2  denv_wf_val E (denv_merge m1 m2).
Dan Frumin's avatar
Dan Frumin committed
271
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
272 273
    revert m2.
    induction m1 as [|[[???]|]]; intros [|[[???]|] ?] **; simplify; naive_solver.
Dan Frumin's avatar
Dan Frumin committed
274
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
275 276 277
  Lemma denv_wf_len_merge E m1 m2 :
    denv_wf_len E m1  denv_wf_len E m2 
    denv_wf_len E (denv_merge m1 m2).
Léon Gondelman's avatar
Léon Gondelman committed
278
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
279 280
    rewrite /denv_wf_len !bool_decide_spec. revert E m2.
    induction m1; intros [|??] [|??]; naive_solver eauto using Peano.le_n_S with lia.
Léon Gondelman's avatar
Léon Gondelman committed
281
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
282 283
  Lemma denv_wf_merge E m1 m2 :
    denv_wf E m1  denv_wf E m2  denv_wf E (denv_merge m1 m2).
Dan Frumin's avatar
Dan Frumin committed
284
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
285
    rewrite /denv_wf. naive_solver eauto using denv_wf_val_merge, denv_wf_len_merge.
Dan Frumin's avatar
Dan Frumin committed
286
  Qed.
287

Robbert Krebbers's avatar
Robbert Krebbers committed
288 289 290 291 292 293 294 295 296 297 298 299
  Lemma denv_wf_stack_merge ms E :
    Forall (denv_wf E) ms  denv_wf E (denv_stack_merge ms).
  Proof. induction 1; simpl; eauto using denv_wf_merge. Qed.

  Lemma denv_length_singleton i x q dv :
    length (denv_singleton i x q dv) = S i.
  Proof. induction i; naive_solver. Qed.
  Lemma denv_wf_val_singleton E i x q dv :
    (0 < q)%Q  dval_wf E dv  denv_wf_val E (denv_singleton i x q dv).
  Proof. induction i; naive_solver. Qed.
  Lemma denv_wf_singleton E i x q dv :
    (0 < q)%Q  dloc_var_wf E i  dval_wf E dv  denv_wf E (denv_singleton i x q dv).
Dan Frumin's avatar
Dan Frumin committed
300
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
301 302 303
    rewrite /denv_wf /denv_wf_len /dloc_var_wf denv_length_singleton.
    rewrite !bool_decide_spec. intros ??%lookup_lt_is_Some.
    naive_solver eauto using denv_wf_val_singleton with lia.
Dan Frumin's avatar
Dan Frumin committed
304
  Qed.
305

Robbert Krebbers's avatar
Robbert Krebbers committed
306 307
  Lemma denv_length_insert i x q dv m:
    length (denv_insert i x q dv m) = max (S i) (length m).
Dan Frumin's avatar
Dan Frumin committed
308
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
309 310
    revert i. induction m; intros [|?];
      simplify; f_equal/=; eauto using denv_length_singleton.
Dan Frumin's avatar
Dan Frumin committed
311
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
312 313 314
  Lemma denv_wf_len_insert E i x q dv m:
    (0 < q)%Q  dloc_var_wf E i  denv_wf_len E m 
    denv_wf_len E (denv_insert i x q dv m).
Dan Frumin's avatar
Dan Frumin committed
315
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
316 317
    rewrite /denv_wf /denv_wf_len /dloc_var_wf denv_length_insert.
    rewrite !bool_decide_spec. intros ??%lookup_lt_is_Some. lia.
Dan Frumin's avatar
Dan Frumin committed
318
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
319 320
  Lemma denv_wf_val_insert E i x q dv m:
    (0 < q)%Q  denv_wf_val E m  dval_wf E dv  denv_wf_val E (denv_insert i x q dv m).
Dan Frumin's avatar
Dan Frumin committed
321
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
322 323
    revert i. induction m; intros [|?]; simplify; unfold denv_item_wf in *;
      try naive_solver eauto using denv_wf_val_singleton.
Dan Frumin's avatar
Dan Frumin committed
324
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
325 326 327
  Lemma denv_wf_insert E i x q dv m:
    (0 < q)%Q  dloc_var_wf E i  denv_wf E m  dval_wf E dv 
    denv_wf E (denv_insert i x q dv m).
Dan Frumin's avatar
Dan Frumin committed
328
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
329
    rewrite /denv_wf. naive_solver eauto using denv_wf_len_insert, denv_wf_val_insert.
Dan Frumin's avatar
Dan Frumin committed
330 331
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
332 333 334
  Lemma denv_wf_insert_extend E m dv l x q :
    (0 < q)%Q  denv_wf E m  dval_wf E dv 
    denv_wf (E ++ [l]) (denv_insert (length E) x q dv m).
Dan Frumin's avatar
Dan Frumin committed
335
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
336 337 338 339 340 341
    intros. assert (E `prefix_of` E ++ [l]) by (by eapply prefix_app_l).
    apply denv_wf_insert=> //.
    - rewrite /dloc_var_wf !bool_decide_spec. apply lookup_lt_is_Some_2.
      rewrite app_length /=. lia.
    - by eapply denv_wf_mono.
    - by eapply dval_wf_mono.
Dan Frumin's avatar
Dan Frumin committed
342 343
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
344 345
  Lemma denv_delete_frac_idx i m m' q dv :
    denv_delete_frac i m = Some (m', q, dv)  i < length m.
Dan Frumin's avatar
Dan Frumin committed
346
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
347
    revert i m' q dv. induction m; intros [|?]; simplify; eauto using lt_n_S with lia.
Dan Frumin's avatar
Dan Frumin committed
348
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
349 350 351 352 353 354 355 356 357
  Lemma denv_delete_frac_len i m m' q dv :
    denv_delete_frac i m = Some (m', q, dv)  length m' = length m.
  Proof. revert i m' q dv. induction m; intros [|?]; simplify; eauto. Qed.
  Lemma denv_wf_len_delete_frac E i m m' q dv :
    denv_delete_frac i m = Some (m', q, dv) 
    denv_wf_len E m  denv_wf_len E m'.
  Proof. by rewrite /denv_wf_len=> /denv_delete_frac_len=> ->. Qed.
  Lemma denv_wf_val_delete_frac E i m m' q dv :
    denv_delete_frac i m = Some (m', q, dv)  denv_wf_val E m  denv_wf_val E m'.
Dan Frumin's avatar
Dan Frumin committed
358
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
359 360
    assert ( q, (0 < q)%Q  (0 < q / 2)%Q) by (by intros; apply Qlt_shift_div_l).
    revert i m'; induction m; intros [|?]; simplify; naive_solver.
Dan Frumin's avatar
Dan Frumin committed
361
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
362 363 364 365 366
  Lemma denv_wf_val_dval_wf_delete_frac E i m m' q dv :
    denv_delete_frac i m = Some (m', q, dv)  denv_wf_val E m  dval_wf E dv.
  Proof. revert i m'; induction m; intros [|?]; simplify; naive_solver. Qed.
  Lemma denv_wf_val_frac_wf_delete_frac E i m m' q dv :
    denv_delete_frac i m = Some (m', q, dv)  denv_wf_val E m  (0 < q)%Q.
Dan Frumin's avatar
Dan Frumin committed
367
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
368 369
    assert ( q, (0 < q)%Q  (0 < q / 2)%Q) by (by intros; apply Qlt_shift_div_l).
    revert i m'; induction m; intros [|?]; simplify; naive_solver.
Dan Frumin's avatar
Dan Frumin committed
370
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
371 372
  Lemma denv_wf_delete_frac E i m m' q dv :
    denv_delete_frac i m = Some (m', q, dv)  denv_wf E m  denv_wf E m'.
Dan Frumin's avatar
Dan Frumin committed
373
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
374 375
    rewrite /denv_wf; naive_solver eauto using denv_wf_val_delete_frac,
      denv_wf_len_delete_frac.
Dan Frumin's avatar
Dan Frumin committed
376
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
377 378 379 380 381 382
  Lemma denv_wf_dval_wf_delete_frac E i m m' q dv :
    denv_delete_frac i m = Some (m', q, dv)  denv_wf E m  dval_wf E dv.
  Proof. rewrite /denv_wf. naive_solver eauto using denv_wf_val_dval_wf_delete_frac. Qed.
  Lemma denv_wf_frac_wf_delete_frac E i m m' q dv :
    denv_delete_frac i m = Some (m', q, dv)  denv_wf E m  (0 < q)%Q.
  Proof. rewrite /denv_wf. naive_solver eauto using denv_wf_val_frac_wf_delete_frac. Qed.
Dan Frumin's avatar
Dan Frumin committed
383

Robbert Krebbers's avatar
Robbert Krebbers committed
384 385
  Lemma denv_delete_full_idx i m m' q dv :
    denv_delete_full_aux i m = Some (m', q, dv)  i < length m.
Dan Frumin's avatar
Dan Frumin committed
386
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
387
    revert i m' q dv. induction m; intros [|?]; simplify; eauto using lt_n_S with lia.
Dan Frumin's avatar
Dan Frumin committed
388
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419
  Lemma denv_delete_full_len i m m' q dv :
    denv_delete_full_aux i m = Some (m', q, dv)  length m' = length m.
  Proof. revert i m' q dv. induction m; intros [|?]; simplify; eauto. Qed.
  Lemma denv_wf_len_delete_full_aux E i m m' q dv :
    denv_delete_full_aux i m = Some (m', q, dv) 
    denv_wf_len E m  denv_wf_len E m'.
  Proof. by rewrite /denv_wf_len=> /denv_delete_full_len=> ->. Qed.
  Lemma denv_wf_val_delete_full_aux E i m m' q dv :
    denv_delete_full_aux i m = Some (m', q, dv)  denv_wf_val E m  denv_wf_val E m'.
  Proof. revert i m'; induction m; intros [|?]; simplify; naive_solver. Qed.
  Lemma denv_wf_val_dval_wf_delete_full_aux E i m m' q dv :
    denv_delete_full_aux i m = Some (m', q, dv)  denv_wf_val E m  dval_wf E dv.
  Proof. revert i m'; induction m; intros [|?]; simplify; naive_solver. Qed.
  Lemma denv_wf_val_frac_wf_delete_full_aux E i m m' q dv :
    denv_delete_full_aux i m = Some (m', q, dv)  denv_wf_val E m  (0 < q)%Q.
  Proof. revert i m'; induction m; intros [|?]; simplify; naive_solver. Qed.
  Lemma denv_wf_delete_full_aux E i m m' q dv :
    denv_delete_full_aux i m = Some (m', q, dv)  denv_wf E m  denv_wf E m'.
  Proof.
    rewrite /denv_wf; naive_solver eauto using denv_wf_val_delete_full_aux,
      denv_wf_len_delete_full_aux.
  Qed.
  Lemma denv_wf_dval_wf_delete_full_aux E i m m' q dv :
    denv_delete_full_aux i m = Some (m', q, dv)  denv_wf E m  dval_wf E dv.
  Proof. rewrite /denv_wf. naive_solver eauto using denv_wf_val_dval_wf_delete_full_aux. Qed.
  Lemma denv_wf_frac_wf_delete_full_aux E i m m' q dv :
    denv_delete_full_aux i m = Some (m', q, dv)  denv_wf E m  (0 < q)%Q.
  Proof. rewrite /denv_wf. naive_solver eauto using denv_wf_val_frac_wf_delete_full_aux. Qed.

  Lemma denv_wf_dval_wf_lookup E i m q dv :
    denv_lookup i m = Some (q, dv)  denv_wf E m  dval_wf E dv.
Dan Frumin's avatar
Dan Frumin committed
420
  Proof. rewrite /denv_lookup; simplify; eauto using denv_wf_dval_wf_delete_full_aux. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
421 422
  Lemma denv_wf_frac_wf_lookup E i m q dv :
    denv_lookup i m = Some (q, dv)  denv_wf E m  (0 < q)%Q.
Dan Frumin's avatar
Dan Frumin committed
423
  Proof. rewrite /denv_lookup; simplify; eauto using denv_wf_frac_wf_delete_full_aux. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
424 425 426

  Lemma denv_wf_delete_full E i m m' dv :
    denv_delete_full i m = Some (m', dv)  denv_wf E m  denv_wf E m'.
Dan Frumin's avatar
Dan Frumin committed
427
  Proof. rewrite /denv_delete_full; simplify; eauto using denv_wf_delete_full_aux. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
428 429 430
  Lemma denv_wf_dval_wf_delete_full E i m m' dv :
    denv_delete_full i m = Some (m', dv)  denv_wf E m  dval_wf E dv.
  Proof. rewrite /denv_delete_full; simplify; eauto using denv_wf_dval_wf_delete_full_aux. Qed.
Dan Frumin's avatar
Dan Frumin committed
431

Robbert Krebbers's avatar
Robbert Krebbers committed
432 433 434 435 436 437 438 439
  Lemma denv_wf_val_unlock E m :
    denv_wf_val E m  denv_wf_val E (denv_unlock m).
  Proof. induction m as [|[[]|] ms]; naive_solver. Qed.
  Lemma denv_wf_len_unlock E m :
    denv_wf_len E m  denv_wf_len E (denv_unlock m).
  Proof. by rewrite /denv_wf_len /denv_unlock map_length. Qed.
  Lemma denv_wf_unlock E m :
    denv_wf E m  denv_wf E (denv_unlock m).
Dan Frumin's avatar
Dan Frumin committed
440
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
441
    rewrite /denv_wf. naive_solver eauto using denv_wf_val_unlock, denv_wf_len_unlock.
Dan Frumin's avatar
Dan Frumin committed
442 443
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
444 445 446 447
  Lemma denv_length_delete_frac_stack i ms ms' q dv :
    denv_delete_frac_stack i ms = Some (ms', q, dv)  length ms = length ms'.
  Proof. revert ms'; induction ms; simplify; auto. Qed.
  Lemma denv_wf_delete_frac_stack ms ms' q i E dv :
Dan Frumin's avatar
Dan Frumin committed
448
    denv_delete_frac_stack i ms = Some (ms', q, dv) 
Robbert Krebbers's avatar
Robbert Krebbers committed
449
    Forall (denv_wf E) ms  Forall (denv_wf E) ms'.
Dan Frumin's avatar
Dan Frumin committed
450
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
451 452
    intros Hi Hms. revert ms' Hi.
    induction Hms; simplify; eauto using denv_wf_delete_frac.
Dan Frumin's avatar
Dan Frumin committed
453
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
454 455 456
  Lemma denv_wf_dval_wf_delete_frac_stack ms ms' q i E dv :
    denv_delete_frac_stack i ms = Some (ms', q, dv) 
    Forall (denv_wf E) ms  dval_wf E dv.
Dan Frumin's avatar
Dan Frumin committed
457
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
458 459
    intros Hi Hms. revert ms' Hi.
    induction Hms; simplify; eauto using denv_wf_dval_wf_delete_frac.
Dan Frumin's avatar
Dan Frumin committed
460
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
461 462 463
  Lemma denv_wf_frac_wf_delete_frac_stack ms ms' q i E dv :
    denv_delete_frac_stack i ms = Some (ms', q, dv) 
    Forall (denv_wf E) ms  (0 < q)%Q.
Dan Frumin's avatar
Dan Frumin committed
464
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
465 466 467
    intros Hi Hms. revert ms' Hi.
    induction Hms; simplify; eauto using denv_wf_frac_wf_delete_frac.
 Qed.
Dan Frumin's avatar
Dan Frumin committed
468

Robbert Krebbers's avatar
Robbert Krebbers committed
469 470 471 472 473 474
  Lemma denv_length_delete_full_stack_aux i ms ms' q dv :
    denv_delete_full_stack_aux i ms = Some (ms', q, dv)  length ms = length ms'.
  Proof. revert ms' q dv; induction ms; simplify; eauto. Qed.
  Lemma denv_wf_delete_full_stack_aux ms ms' q i E dv :
    denv_delete_full_stack_aux i ms = Some (ms', q, dv) 
    Forall (denv_wf E) ms  Forall (denv_wf E) ms'.
Dan Frumin's avatar
Dan Frumin committed
475
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
476 477
    intros Hi Hms. revert dv q ms' Hi.
    induction Hms; simplify; eauto using denv_wf_delete_full_aux.
Dan Frumin's avatar
Dan Frumin committed
478
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
479 480 481
  Lemma denv_wf_dval_wf_delete_full_stack_aux ms ms' q i E dv :
    denv_delete_full_stack_aux i ms = Some (ms', q, dv) 
    Forall (denv_wf E) ms  dval_wf E dv.
Dan Frumin's avatar
Dan Frumin committed
482
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
483 484
    intros Hi Hms. revert dv q ms' Hi.
    induction Hms; simplify; eauto using denv_wf_dval_wf_delete_full_aux.
Dan Frumin's avatar
Dan Frumin committed
485
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
486 487 488
  Lemma denv_wf_frac_wf_delete_full_stack_aux ms ms' q i E dv :
    denv_delete_full_stack_aux i ms = Some (ms', q, dv) 
    Forall (denv_wf E) ms  (0 < q)%Q.
Léon Gondelman's avatar
Léon Gondelman committed
489
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
490 491
    intros Hi Hms. revert dv q ms' Hi.
    induction Hms; simplify; eauto using denv_wf_frac_wf_delete_full_aux.
492 493
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
494 495
  Lemma denv_length_delete_frac_2 i ms m ms' m' q dv :
    denv_delete_frac_2 i ms m = Some (ms', m', q, dv)  length ms = length ms'.
496
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
497 498
    rewrite /denv_delete_frac_2.
    simplify; eauto using denv_length_delete_frac_stack.
Dan Frumin's avatar
Dan Frumin committed
499
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
500 501 502
  Lemma denv_wf_1_delete_frac_2 ms m ms' m' i E q dv :
    denv_delete_frac_2 i ms m = Some (ms', m', q, dv) 
    Forall (denv_wf E) ms  denv_wf E m  Forall (denv_wf E) ms'.
503
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
504 505
    rewrite /denv_delete_frac_2; intros; simplify;
      eauto using denv_wf_delete_frac_stack.
Léon Gondelman's avatar
Léon Gondelman committed
506
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
507 508 509
  Lemma denv_wf_2_delete_frac_2 ms m ms' m' i E q dv :
    denv_delete_frac_2 i ms m = Some (ms', m', q, dv) 
    Forall (denv_wf E) ms  denv_wf E m  denv_wf E m'.
Dan Frumin's avatar
Dan Frumin committed
510
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
511 512
    rewrite /denv_delete_frac_2; intros; simplify;
      eauto using denv_wf_delete_frac.
Dan Frumin's avatar
Dan Frumin committed
513
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
514 515 516
  Lemma denv_wf_dval_wf_delete_frac_2 ms m ms' m' i E q dv :
    denv_delete_frac_2 i ms m = Some (ms', m', q, dv) 
    Forall (denv_wf E) ms  denv_wf E m  dval_wf E dv.
Dan Frumin's avatar
Dan Frumin committed
517
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
518 519
    rewrite /denv_delete_frac_2; intros; simplify;
      eauto using denv_wf_dval_wf_delete_frac, denv_wf_dval_wf_delete_frac_stack.
Dan Frumin's avatar
Dan Frumin committed
520
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
521 522 523
  Lemma denv_wf_frac_wf_delete_frac_2 ms m ms' m' i E q dv :
    denv_delete_frac_2 i ms m = Some (ms', m', q, dv) 
    Forall (denv_wf E) ms  denv_wf E m  (0 < q)%Q.
Dan Frumin's avatar
Dan Frumin committed
524
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
525 526
    rewrite /denv_delete_frac_2; intros; simplify;
      eauto using denv_wf_frac_wf_delete_frac, denv_wf_frac_wf_delete_frac_stack.
527
  Qed.
Dan Frumin's avatar
Dan Frumin committed
528

Robbert Krebbers's avatar
Robbert Krebbers committed
529 530
  Lemma denv_length_delete_full_2 i ms m ms' m' dv :
    denv_delete_full_2 i ms m = Some (ms', m', dv)  length ms = length ms'.
Dan Frumin's avatar
Dan Frumin committed
531
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
532 533
    rewrite /denv_delete_full_2.
    simplify; eauto using denv_length_delete_full_stack_aux.
Dan Frumin's avatar
Dan Frumin committed
534
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
535 536 537
  Lemma denv_wf_1_delete_full_2 ms m ms' m' i E dv :
    denv_delete_full_2 i ms m = Some (ms', m', dv) 
    Forall (denv_wf E) ms  denv_wf E m  Forall (denv_wf E) ms'.
Dan Frumin's avatar
Dan Frumin committed
538
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
539 540
    rewrite /denv_delete_full_2; intros; simplify;
      eauto using denv_wf_delete_full_stack_aux.
Dan Frumin's avatar
Dan Frumin committed
541
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
542 543 544
  Lemma denv_wf_2_delete_full_2 ms m ms' m' i E dv :
    denv_delete_full_2 i ms m = Some (ms', m', dv) 
    Forall (denv_wf E) ms  denv_wf E m  denv_wf E m'.
545
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
546 547
    rewrite /denv_delete_full_2; intros; simplify;
      eauto using denv_wf_delete_full_aux.
548
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
549 550 551
  Lemma denv_wf_dval_wf_delete_full_2 ms m ms' m' i E dv :
    denv_delete_full_2 i ms m = Some (ms', m', dv) 
    Forall (denv_wf E) ms  denv_wf E m  dval_wf E dv.
Dan Frumin's avatar
Dan Frumin committed
552
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
553 554
    rewrite /denv_delete_full_2; intros; simplify;
      eauto using denv_wf_dval_wf_delete_full_aux, denv_wf_dval_wf_delete_full_stack_aux.
Dan Frumin's avatar
Dan Frumin committed
555 556
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
557 558 559 560 561
  (** Auxiliary interpretation function.
  * This is only used for doing proofs by induction. *)
  Definition denv_interp_aux (E : known_locs) (m : denv) (k : nat) : iProp Σ :=
    ([ list] i  dio  m, from_option (denv_item_interp E (k + i)) True dio)%I.
  Arguments denv_interp_aux _ !_ _ /.
Dan Frumin's avatar
Dan Frumin committed
562

Robbert Krebbers's avatar
Robbert Krebbers committed
563 564 565 566
  Lemma denv_merge_nil_r m : denv_merge m [] = m.
  Proof. induction m=> //=. Qed.
  Lemma denv_merge_nil_l m : denv_merge [] m = m.
  Proof. induction m=> //=. Qed.
Léon Gondelman's avatar
Léon Gondelman committed
567

Robbert Krebbers's avatar
Robbert Krebbers committed
568 569
  Lemma denv_interp_aux_0 E m : denv_interp_aux E m 0  denv_interp E m.
  Proof. reflexivity. Qed.
Léon Gondelman's avatar
Léon Gondelman committed
570

Robbert Krebbers's avatar
Robbert Krebbers committed
571 572 573 574
  Lemma denv_singleton_lookup i j x q dv di :
    lookup j (denv_singleton i x q dv) = Some (Some di) 
    di = DenvItem x q dv  i = j.
  Proof. revert j. induction i as [|i IH]=> -[|j]; naive_solver. Qed.
575

Robbert Krebbers's avatar
Robbert Krebbers committed
576 577 578 579
  (** ** Correctness of the `denv_` functions w.r.t. the interpretation *)
  Lemma denv_interp_singleton_aux E i k x q dv :
    dloc_var_interp E (k + i) C[x]{Q_to_Qp q} dval_interp E dv
     denv_interp_aux E (denv_singleton i x q dv) k.
580
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
581 582 583 584 585 586 587 588
    assert (denv_singleton i x q dv !! i = Some (Some (DenvItem x q dv))) as Hdi.
    { induction i=> //=. }
    rewrite /denv_interp_aux big_sepL_delete' //; simpl. iSplit.
    - iIntros "$". iApply (big_sepL_impl (λ _ _, True)%I).
      { by iApply big_sepL_forall. }
      iIntros "!>" (? [dio|] Hk _ ?) "//=".
      by apply denv_singleton_lookup in Hk as [? ->].
    - iIntros "[$ _]".
589
  Qed.
Dan Frumin's avatar
Dan Frumin committed
590

Robbert Krebbers's avatar
Robbert Krebbers committed
591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608
  Lemma denv_insert_interp_aux E m i k x q dv :
    denv_wf_val E m  (0 < q)%Q 
    denv_interp_aux E m k  dloc_var_interp E (k+i) C[x]{Q_to_Qp q} dval_interp E dv -
    denv_interp_aux E (denv_insert i x q dv m) k.
  Proof.
    intros Hval ?. iInduction m as [|[[x' q' dv']|] m] "IH" forall (i k Hval);
      simpl in *; destruct_and?.
    - rewrite denv_interp_singleton_aux. iIntros "[_ $]".
    - destruct i as [|i].
      + iIntros "[[H1 $] H2] /=".
        rewrite Q_to_Qp_plus //. iDestruct (mapsto_value_agree with "H1 H2") as %->.
        by iCombine "H1 H2" as "H".
      + iIntros "[[$ H1] H2]". setoid_rewrite Nat.add_succ_r; simpl.
        iApply ("IH" $! _ (S _)); auto with iFrame.
    - destruct i as [|i].
      + iIntros "[[_ $] $]".
      + iIntros "[[$ H1] H2]". setoid_rewrite Nat.add_succ_r; simpl.
        iApply ("IH" $! _ (S _)); auto with iFrame.
609
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
610 611 612 613
  Lemma denv_insert_interp E m i x q dv :
    denv_wf E m  (0 < q)%Q 
    denv_interp E m  dloc_var_interp E i C[x]{Q_to_Qp q} dval_interp E dv -
    denv_interp E (denv_insert i x q dv m).
614
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
615 616
    rewrite /denv_wf. intros.
    rewrite -denv_interp_aux_0 denv_insert_interp_aux; naive_solver.
617 618
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
619 620 621 622
  Lemma denv_merge_interp_aux E m1 m2 k :
    denv_wf_val E m1  denv_wf_val E m2 
    denv_interp_aux E m1 k  denv_interp_aux E m2 k -
    denv_interp_aux E (denv_merge m1 m2) k.
Léon Gondelman's avatar
Léon Gondelman committed
623
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
624 625 626 627 628 629 630 631 632 633 634
    intros H1 H2. rewrite /denv_interp_aux.
    iInduction m1 as [|dio1 m1] "IH" forall (m2 k H1 H2).
    { rewrite denv_merge_nil_l. iIntros "[_ $]". }
    destruct m2 as [|dio2 m2]; simpl in *; destruct_and?.
    { iIntros "[$ _]". }
    iIntros "[[Hl1 H1] [Hl2 H2]] /=". iSplitL "Hl1 Hl2".
    { destruct dio1 as [[x1 q1 dv1]|], dio2 as [[x2 q2 dv2]|]=> //=; simpl in *; destruct_and?.
      rewrite Q_to_Qp_plus //. iDestruct (mapsto_value_agree with "Hl1 Hl2") as %->.
      by iCombine "Hl1 Hl2" as "Hl". }
    setoid_rewrite Nat.add_succ_r; simpl.
    iApply ("IH" $! _ (S _)); auto with iFrame.
Léon Gondelman's avatar
Léon Gondelman committed
635
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
636 637 638
  Lemma denv_merge_interp E m1 m2 :
    denv_wf E m1  denv_wf E m2 
    denv_interp E m1  denv_interp E m2 - denv_interp E (denv_merge m1 m2).
639
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
640 641
    rewrite /denv_wf. intros.
    intros. rewrite -!denv_interp_aux_0 denv_merge_interp_aux; naive_solver.
642 643
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
644 645 646 647 648 649 650 651 652 653 654 655 656 657
  Lemma denv_delete_frac_interp_aux E i k m m' q dv :
    denv_delete_frac i m = Some (m', q, dv)  denv_wf_val E m 
    denv_interp_aux E m k -
    denv_interp_aux E m' k  dloc_var_interp E (k + i) C{Q_to_Qp q} dval_interp E dv.
  Proof.
    intros Hi Hm. iInduction m as [|dio m] "IH"
      forall (i k m' Hi Hm); simpl in *; destruct_and?.
    { by destruct i. }
    destruct i as [|i]; simpl in *.
    - destruct dio as [[x q' dv']|]; simplify_option_eq; destruct_and?.
      iIntros "[[Hl1 Hl2] $] /=". rewrite -!Q_to_Qp_div //. iFrame.
    - destruct (denv_delete_frac i m) as [[[mf q'] dv']|] eqn:Hdenv; simplify_eq/=.
      iIntros "[$ Hm]". setoid_rewrite Nat.add_succ_r; simpl.
      by iApply ("IH" $! _ (S _)).
Dan Frumin's avatar
Dan Frumin committed
658
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
659 660 661 662
  Lemma denv_delete_frac_interp E i m m' q dv :
    denv_delete_frac i m = Some (m', q, dv)  denv_wf E m 
    denv_interp E m -
    denv_interp E m'  dloc_var_interp E i C{Q_to_Qp q} dval_interp E dv.
663
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
664 665
    rewrite /denv_wf. intros.
    rewrite -!denv_interp_aux_0 denv_delete_frac_interp_aux; naive_solver.
666 667
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
668
  Lemma denv_delete_full_interp_aux E i k m m' q dv :
Dan Frumin's avatar
Dan Frumin committed
669
    denv_delete_full_aux i m = Some (m', q, dv) 
Robbert Krebbers's avatar
Robbert Krebbers committed
670 671 672 673 674 675 676 677 678 679 680
    denv_interp_aux E m k -
    denv_interp_aux E m' k  dloc_var_interp E (k+i) C{Q_to_Qp q} dval_interp E dv.
  Proof.
    intros Hi. iInduction m as [|dio m] "IH" forall (i k m' Hi); simpl.
    { by destruct i. }
    destruct i as [|i]; simpl in *.
    - destruct dio as [[x q' dv']|]; simplify_option_eq; destruct_and?.
      iIntros "[$$]".
    - destruct (denv_delete_full_aux i m) as [[[mf q'] dv']|] eqn:?; simplify_eq/=.
      iIntros "[$ Hm]". setoid_rewrite Nat.add_succ_r; simpl.
      by iApply ("IH" $! _ (S _)).
Léon Gondelman's avatar
Léon Gondelman committed
681
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
682 683 684 685
  Lemma denv_delete_full_interp E i m m' dv :
    denv_delete_full i m = Some (m', dv) 
    denv_interp E m -
    denv_interp E m'  dloc_var_interp E i C{1} dval_interp E dv.
686
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
687 688 689 690
    rewrite /denv_delete_full. intros.
    destruct (denv_delete_full_aux i m) as [[[??] ?]|] eqn:?; simplify_option_eq.
    rewrite -!denv_interp_aux_0 denv_delete_full_interp_aux //.
    by match goal with H : _ == _ |- _ => rewrite H end.
691
  Qed.
Dan Frumin's avatar
Dan Frumin committed
692

Robbert Krebbers's avatar
Robbert Krebbers committed
693 694 695 696
  Lemma denv_delete_full_interp_aux_flip E i k m m' q dv :
    denv_delete_full_aux i m = Some (m', q, dv) 
    denv_interp_aux E m' k  dloc_var_interp E (k+i) C{Q_to_Qp q} dval_interp E dv -
    denv_interp_aux E m k.
697
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
698 699 700 701 702 703 704 705
    intros Hi. iInduction m as [|dio m] "IH" forall (i k m' Hi); simpl.
    { by destruct i. }
    destruct i as [|i]; simpl in *.
    - destruct dio as [[x q' dv']|]; simplify_option_eq; destruct_and?.
      iIntros "[[_ $] $]".
    - destruct (denv_delete_full_aux i m) as [[[mf q'] dv']|] eqn:?; simplify_eq/=.
      iIntros "[[$ Hmf] Hm]". setoid_rewrite Nat.add_succ_r; simpl.
      iApply ("IH" $! _ (S _)); eauto with iFrame.
706
  Qed.
Dan Frumin's avatar
Dan Frumin committed
707

Robbert Krebbers's avatar
Robbert Krebbers committed
708 709 710 711
  Lemma denv_lookup_interp E i q dv m:
    denv_lookup i m = Some (q, dv) 
     mf, denv_interp E m 
          denv_interp E mf  dloc_var_interp E i C{Q_to_Qp q} dval_interp E dv.
Léon Gondelman's avatar
Léon Gondelman committed
712
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
713 714 715 716 717
    rewrite /denv_lookup=> ?.
    destruct (denv_delete_full_aux i m) as [[[mf qf] dvf]|] eqn:?; simplify_eq/=.
    exists mf. apply (anti_symm _).
    - by rewrite -!denv_interp_aux_0 denv_delete_full_interp_aux.
    - by rewrite -!denv_interp_aux_0 denv_delete_full_interp_aux_flip.
Dan Frumin's avatar
Dan Frumin committed
718
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
719

Robbert Krebbers's avatar
Robbert Krebbers committed
720 721
  Lemma denv_unlock_interp E m :
    denv_interp E m - U (denv_interp E (denv_unlock m)).
Léon Gondelman's avatar
Léon Gondelman committed
722
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
723 724 725
    unfold denv_interp. iIntros "H". iApply U_big_sepL.
    rewrite /denv_unlock big_sepL_fmap. iApply (big_sepL_mono with "H").
    by iIntros (k [[x q dv]|] ?) "H /= !>".
Dan Frumin's avatar
Dan Frumin committed
726
  Qed.
Dan Frumin's avatar
Dan Frumin committed
727

Robbert Krebbers's avatar
Robbert Krebbers committed
728 729
  (** *** Stack interpretation properties *)
  Lemma denv_stack_interp_intro ms E P : P - denv_stack_interp E ms ms P.
Dan Frumin's avatar
Dan Frumin committed
730
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
731 732 733
    iIntros "HP".
    iInduction ms as [|m ms] "IH" forall (P); simpl; first by iFrame.
    iApply "IH"; eauto with iFrame.
Dan Frumin's avatar
Dan Frumin committed
734 735
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
736 737
  Lemma denv_stack_interp_wand E ms1 ms2 P Q :
    denv_stack_interp E ms1 ms2 P - (P - Q) - denv_stack_interp E ms1 ms2 Q.
Dan Frumin's avatar
Dan Frumin committed
738
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
739 740 741 742
    iIntros "HP H". iInduction (ms1) as [|m1 ms1] "IH" forall (ms2 P Q); simpl.
    { destruct ms2=> //=. by iApply "H". }
    destruct ms2 as [|m2 ms2]=> //=. iApply ("IH" with "HP [H]").
    iIntros "HP Hm". iDestruct ("HP" with "Hm") as "[$ HP]". by iApply "H".
Dan Frumin's avatar
Dan Frumin committed
743
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
744

Robbert Krebbers's avatar
Robbert Krebbers committed
745 746
  Lemma denv_stack_interp_frame E ms1 ms2 P Q :
    denv_stack_interp E ms1 ms2 P - Q - denv_stack_interp E ms1 ms2 (P  Q).
Léon Gondelman's avatar
Léon Gondelman committed
747
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
748 749
    iIntros "HP HQ".
    iApply (denv_stack_interp_wand with "HP [HQ]"). eauto with iFrame.
Léon Gondelman's avatar
Léon Gondelman committed
750 751
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
752 753 754
  Lemma denv_stack_interp_trans ms1 ms2 ms3 E P Q :
    denv_stack_interp E ms1 ms2 P - denv_stack_interp E ms2 ms3 Q -
    denv_stack_interp E ms1 ms3 (P  Q).
755
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
756 757 758 759 760 761 762
    iIntros "HP HQ".
    iInduction ms1 as [|m1 ms1] "IH" forall (ms2 ms3 P Q);
      destruct ms2 as [|m2 ms2], ms3 as [|m3 ms3]=> //=; first by iFrame.
    iDestruct ("IH" with "HP HQ") as "H".
    iApply (denv_stack_interp_wand with "H"); iIntros "[HP HQ] Hm1".
    iDestruct ("HP" with "Hm1") as "[Hm2 $]".
    iDestruct ("HQ" with "Hm2") as "[$ $]".
763 764
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
765 766 767
  Lemma denv_delete_frac_stack_interp E i ms ms' q dv :
    denv_delete_frac_stack i ms = Some (ms', q, dv)  Forall (denv_wf E) ms 
    denv_stack_interp E ms ms' (dloc_var_interp E i C{Q_to_Qp q} dval_interp E dv).
768
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
769 770 771 772 773 774 775 776
    intros Hi Hms. iInduction Hms as [|m ms] "IH" forall (ms' Hi); simplify_eq/=.
    destruct (denv_delete_frac i m) as [[[m' q'] dv']|] eqn:?; simplify_eq/=.
    - iApply denv_stack_interp_intro. iIntros "Hm".
      by iApply denv_delete_frac_interp.
    - destruct (denv_delete_frac_stack i ms)
        as [[[m' q'] dv']|] eqn:?; simplify_eq/=.
      iSpecialize ("IH" with "[//]").
      iApply (denv_stack_interp_wand with "IH"); by iIntros "$ $".
777 778
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
779 780
  Lemma denv_delete_full_stack_interp E i ms ms' q dv :
    denv_delete_full_stack_aux i ms = Some (ms', q, dv) 
781
    Forall (denv_wf E) ms 
Robbert Krebbers's avatar
Robbert Krebbers committed
782
    denv_stack_interp E ms ms' (dloc_var_interp E i C{Q_to_Qp q} dval_interp E dv).
783
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802
    intros Hi Hms. iInduction Hms as [|m ms] "IH" forall (ms' q dv Hi); simplify_eq/=.
    destruct (denv_delete_full_aux i m) as [[[m' q'] dv']|] eqn:Hm; simplify_eq/=.
    - destruct (denv_delete_full_stack_aux i ms)
        as [[[ms1 q1] ?]|] eqn:?; simplify_eq/=.
      + iSpecialize ("IH" with "[//]").
        iApply (denv_stack_interp_wand with "IH"); iIntros "Hl Hm".
        rewrite -!denv_interp_aux_0 denv_delete_full_interp_aux /=; last done.
        iDestruct "Hm" as "[$ Hl2]".
        rewrite Q_to_Qp_plus; eauto using denv_wf_frac_wf_delete_full_aux,
          denv_wf_frac_wf_delete_full_stack_aux.
        iDestruct (mapsto_value_agree with "Hl Hl2") as %->.
        iCombine "Hl Hl2" as "$".
      + iApply denv_stack_interp_intro. iIntros "Hm".
        rewrite -!denv_interp_aux_0 denv_delete_full_interp_aux; last done.
        iDestruct "Hm" as "[$ $]".
    - destruct (denv_delete_full_stack_aux i ms) as [[[ms1 q1] ?]|] eqn:?; simplify_eq/=.
      iSpecialize ("IH" with "[//]").
      iApply (denv_stack_interp_wand with "IH").
      iIntros "$ $".
803 804
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
805 806 807 808 809
  Lemma denv_delete_frac_2_interp E i ms m ms' m' q dv :
    denv_delete_frac_2 i ms m = Some (ms', m', q, dv) 
    Forall (denv_wf E) ms  denv_wf E m 
    denv_stack_interp E ms ms' (denv_interp E m -
      denv_interp E m'  dloc_var_interp E i C{Q_to_Qp q} dval_interp E dv).
810
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
811 812 813 814 815 816 817 818 819 820
    rewrite /denv_delete_frac_2 /denv_wf. intros ?? [??]%andb_True.
    destruct (denv_delete_frac_stack i ms)
      as [[[ms1 q1] dv1]|] eqn:?; simplify_eq/=.
    - iApply denv_stack_interp_wand;
        first by iApply denv_delete_frac_stack_interp.
      eauto with iFrame.
    - destruct (denv_delete_frac i m) as [[[m2 q2] dv2]|] eqn:?; simplify_eq/=.
      iApply denv_stack_interp_intro.
      rewrite -!denv_interp_aux_0 denv_delete_frac_interp_aux //.
      eauto with iFrame.
821 822
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847
  Lemma denv_delete_full_2_interp E i ms m ms' m' dv :
    denv_delete_full_2 i ms m = Some (ms', m', dv) 
    Forall (denv_wf E) ms  denv_wf E m 
    denv_stack_interp E ms ms' (denv_interp E m -
      denv_interp E m'  dloc_var_interp E i C dval_interp E dv).
  Proof.
    rewrite /denv_delete_full_2 /denv_wf. intros ???.
    destruct (denv_delete_full_stack_aux i ms) as [[[ms1 q1] dv1]|] eqn:?,
      (denv_delete_full_aux i m) as [[[m2 q2] dv2]|] eqn:?; simplify_option_eq.
    - iApply denv_stack_interp_wand;
        first by iApply denv_delete_full_stack_interp.
      iIntros "Hl1". rewrite -!denv_interp_aux_0.
      rewrite denv_delete_full_interp_aux //.
      iIntros "[$ Hl2]".
      iDestruct (mapsto_value_agree with "Hl1 Hl2") as %->.
      iCombine "Hl1 Hl2" as "Hl".
      rewrite -Q_to_Qp_plus; eauto using denv_wf_frac_wf_delete_full_aux,
        denv_wf_frac_wf_delete_full_stack_aux.
      rewrite (_ : (_ + _)%Q = 1%Q) //.
    - iApply denv_stack_interp_wand;
        first by iApply denv_delete_full_stack_interp.
      eauto with iFrame.
    - iApply denv_stack_interp_intro.
      rewrite -!denv_interp_aux_0 denv_delete_full_interp_aux; last done.
      eauto with iFrame.
848
  Qed.
Dan Frumin's avatar
Dan Frumin committed
849

Robbert Krebbers's avatar
Robbert Krebbers committed
850 851 852 853 854 855 856 857
  Lemma denv_wf_1_stack_pop E ms ms' m :
    pop_stack ms = Some (ms', m)  Forall (denv_wf E) ms  Forall (denv_wf E) ms'.
  Proof. destruct 2; simplify_eq/=; eauto. Qed.
  Lemma denv_wf_2_stack_pop E ms ms' m :
    pop_stack ms = Some (ms', m)  Forall (denv_wf E) ms  denv_wf E m.
  Proof. destruct 2; simplify_eq/=; eauto. Qed.

  Lemma denv_stack_merge_interp E ms :
Robbert Krebbers's avatar
Robbert Krebbers committed
858
    Forall (denv_wf E) ms 
Robbert Krebbers's avatar
Robbert Krebbers committed
859
    ([ list] de  ms, denv_interp E de) - denv_interp E (denv_stack_merge ms).
860
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
861 862 863 864
    induction 1 as [|m ms ?? IH]; simpl.
    { iIntros "_". rewrite /denv_interp //. }
    iIntros "[Hm Hms]". iApply denv_merge_interp; eauto using denv_wf_stack_merge.
    iFrame "Hm". by iApply IH.
865
  Qed.
866

Robbert Krebbers's avatar
Robbert Krebbers committed
867 868
  Lemma wand_denv_interp_aux_spec E m Φ k :
    wand_denv_interp_aux E m Φ k - denv_interp_aux E m k - Φ.
Dan Frumin's avatar
Dan Frumin committed
869
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
870 871 872 873 874 875 876
    rewrite /denv_interp_aux. iIntros "HmΦ Hm".
    iInduction m as [|[dio|]] "IH" forall (k)=> /=; auto.
    - rewrite Nat.add_0_r. setoid_rewrite Nat.add_succ_r; simpl.
      iDestruct "Hm" as "[H Hm]". iSpecialize ("HmΦ" with "H").
      iApply ("IH" $! (S _) with "HmΦ Hm").
    - iDestruct "Hm" as "[_ Hm]". setoid_rewrite Nat.add_succ_r; simpl.
      iApply ("IH" $! (S _) with "HmΦ Hm").
Dan Frumin's avatar
Dan Frumin committed
877
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
878 879 880 881 882

  Lemma wand_denv_interp_spec E m Φ :
    wand_denv_interp E m Φ - denv_interp E m - Φ.
  Proof. apply wand_denv_interp_aux_spec. Qed.
End denv.