Commit e813e722 authored by Dan Frumin's avatar Dan Frumin
Browse files

Prove `mapsto_wand_list_spec`

parent 68afb0e1
......@@ -247,16 +247,31 @@ Section vcg_spec.
- simpl. intros E. by apply U_mono.
Qed.
Lemma mapsto_wand_list_aux_spec E m t (k : nat) :
wp_interp E (mapsto_wand_list_aux m t k) -
([ list] ndio m, from_option
(λ '{| denv_level := lv; denv_frac := q; denv_dval := dv |},
default 1%positive (E !! (k + n)%nat) C[lv]{q} dval_interp E dv) True dio) -
wp_interp E t.
Proof.
generalize dependent k.
induction m; simpl. eauto.
iIntros (k) "H1 [Hl H2]".
destruct a as [[x q dv]|]; simpl.
- rewrite -plus_n_O. iSpecialize ("H1" with "Hl").
iApply (IHm with "H1 [H2]"). iApply (big_sepL_mono with "H2").
intros n y ?. simpl. assert ((k + S n)%nat = (S k + n)%nat) as -> by omega. done.
- iApply (IHm with "H1 [H2]"). iApply (big_sepL_mono with "H2").
intros n y ?. simpl. assert ((k + S n)%nat = (S k + n)%nat) as -> by omega. done.
Qed.
Lemma mapsto_wand_list_spec E m t :
wp_interp E (mapsto_wand_list m t) - denv_interp E m - wp_interp E t.
Proof.
Admitted.
(* unfold env_ps_dv_interp.
induction s as [| [i [[x q] w]] s']; simpl.
- by iIntros "$ _".
- iIntros "H [H1 H2]".
iSpecialize ("H" with "H1"). iApply (IHs' with "H H2").
Qed. *)
unfold mapsto_wand_list, denv_interp.
iIntros "H1 H2". iApply (mapsto_wand_list_aux_spec with "H1 H2").
Qed.
Lemma vcg_sp_correct' E de mIn mOut mIn' mOut' dv R :
vcg_sp E mIn mOut de = Some (mIn', mOut', dv)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment