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

Prove `denv_wf_insert`

parent 1e50fc87
......@@ -49,18 +49,13 @@ Section denv.
| Some (DenvItem _ _ dv) :: m' => dval_wf E dv && denv_wf_val E m'
| None :: m' => denv_wf_val E m'
end.
Fixpoint denv_wf_len (E: known_locs) (m: denv) {struct m} : bool :=
match E, m with
| _, [] => true
| _ :: E', _ :: m' => denv_wf_len E' m'
| [], _ => false
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 :=
......@@ -210,13 +205,6 @@ Proof. by destruct dv as [| |[? []|]|]; intros; simplify_eq /=. Qed.
Lemma denv_merge_nil_r m : denv_merge m [] = m.
Proof. induction m; simpl; eauto. Qed.
Lemma denv_wf_len_spec E m :
denv_wf_len E m <-> length E >= length m.
Proof.
revert m. induction E; destruct m; intros; try (simpl; lia).
simpl. specialize (IHE m). rewrite IHE. lia.
Qed.
Section denv_spec.
Context `{amonadG Σ}.
......@@ -724,77 +712,107 @@ Section denv_spec.
(** ** Well-foundness of denv *)
Lemma denv_wf_len_mono E E' m :
denv_wf_len E m
E `prefix_of`E'
E `prefix_of` E'
denv_wf_len E' m.
Proof.
revert E E'. induction m as [| x m']; intros.
- by destruct E'.
- destruct E', E;
[ | by apply prefix_nil_not in H1 | | ]; try by eauto.
simpl. destruct m' ; try done. destruct E'; eauto.
eapply IHm'. done. by eapply prefix_cons_inv_2.
intros ? ?%prefix_length.
unfold denv_wf_len in *.
naive_solver lia.
Qed.
Lemma denv_wf_len_mono_r E m1 m2 :
denv_wf_len E (m1 ++ m2)
denv_wf_len E m2.
Proof.
revert m1 m2. induction E; intros m1 m2 Hwf.
- destruct m2; first by naive_solver.
simpl in Hwf. destruct (m1 ++ o :: m2) as [|] eqn:Hyp.
+ destruct m1; by inversion Hyp.
+ done.
- destruct m1; first by naive_solver.
destruct m2; first done.
* simpl in *. eapply IHE with (m1 ++ [o0]).
rewrite -app_assoc. naive_solver.
unfold denv_wf_len in *.
rewrite app_length.
naive_solver lia.
Qed.
Lemma denv_wf_val_mono_r E m1 m2 :
denv_wf_val E (m1 ++ m2)
denv_wf_val E m2.
Proof.
revert m2. induction m1; intros m2 Hwf.
revert m2. induction m1 as [|dio m1]=> m2 Hwf.
- naive_solver.
- apply IHm1. simpl in Hwf.
destruct a as [d|]; last done.
destruct d. by destruct_and!.
destruct dio as [[]|]; naive_solver.
Qed.
Lemma denv_wf_mono E E' m :
denv_wf E m E `prefix_of` E' denv_wf E' m.
Proof.
rewrite !andb_True. revert E E'.
induction m as [|[denv|] ms]; eauto.
- intros E E' [_ Hwf] Hpre; split; first done. by destruct E'.
- intros E E' [ Hwf1 Hwf2] Hpre.
split_and.
+ destruct E'.
* destruct E; simplify_eq; first by naive_solver.
Proof.
rewrite !andb_True. intros [Hm Hlen] Hpre.
split_and; last first.
{ by eapply denv_wf_len_mono. }
clear Hlen.
revert E E' Hm Hpre.
induction m as [|[[]|] ms] =>E E' Hwf Hpre; eauto.
- destruct E'.
+ destruct E; simplify_eq; first by naive_solver.
by apply prefix_nil_not in Hpre.
* simpl. destruct denv as [ lvl q dv].
rewrite andb_True. split.
** simpl in Hwf1. apply andb_True in Hwf1 as [Hwf11 Hwf12].
by eapply dval_wf_mono.
** eapply (IHms E (c::E')); last done. split.
*** apply (denv_wf_val_mono_r E
[Some {| denv_level := lvl; denv_frac := q; denv_dval := dv |}]).
naive_solver.
*** apply (denv_wf_len_mono_r E
[Some {| denv_level := lvl; denv_frac := q; denv_dval := dv |}]).
naive_solver.
+ by eapply denv_wf_len_mono.
- intros E E' [ Hwf1 Hwf2] Hpre.
split_and.
+ destruct E'.
* destruct E; simplify_eq; first by naive_solver.
+ simpl in Hwf. destruct_and!.
simpl. split_and. by eapply dval_wf_mono.
eapply IHms; eauto.
- destruct E'.
+ destruct E; simplify_eq; first by naive_solver.
by apply prefix_nil_not in Hpre.
* simpl. eapply (IHms E (c::E')); last done. split.
** by eapply (denv_wf_val_mono_r E [None]).
** by eapply (denv_wf_len_mono_r E [None]).
+ by eapply denv_wf_len_mono.
+ simpl. eapply IHms; eauto.
Qed.
Lemma denv_wf_cons E m dio :
denv_wf E (dio::m)
denv_wf E m.
Proof.
rewrite /denv_wf /denv_wf_len =>?.
destruct dio as [[]|]; naive_solver lia.
Qed.
Lemma denv_wf_lookup_dval_wf E (m : denv) (k : nat) (di : denv_item) :
denv_wf E m
lookup k m = Some (Some di)
dval_wf E (denv_dval di).
Proof.
revert k.
induction m as [|dio m]; simpl. inversion 2.
intros k Hwf. destruct k as [|k']; simpl.
- intros. simplify_eq/=.
unfold denv_wf in Hwf.
destruct_and!. simpl in *.
destruct di. destruct_and!. done.
- apply denv_wf_cons in Hwf.
by apply IHm.
Qed.
Lemma denv_wf_lookup_dloc_wf E (m : denv) (k : nat) (di : denv_item) :
denv_wf E m
lookup k m = Some (Some di)
dloc_wf E (dLoc k 0).
Proof.
rewrite /denv_wf /denv_wf_len => Hwf.
destruct_and!.
intros Hk%lookup_lt_Some.
apply bool_decide_pack.
apply lookup_lt_is_Some. lia.
Qed.
Lemma denv_interp_mono E E' m :
denv_wf E m E `prefix_of` E'
denv_interp E m - denv_interp E' m.
Proof.
intros Hwf Hpre.
rewrite /denv_interp.
apply big_sepL_mono.
iIntros (k dio Hk).
destruct dio as [[lv q dv]|]; simpl; last done.
pose (Hwf' := Hwf).
eapply denv_wf_lookup_dloc_wf in Hwf'; last eassumption.
eapply denv_wf_lookup_dval_wf in Hwf; last eassumption.
simpl in *.
rewrite (dval_interp_mono E E' dv Hwf Hpre).
rewrite (dloc_interp_mono E E' k _ Hwf' Hpre).
reflexivity.
Qed.
Lemma denv_wf_merge_val (E : known_locs) (m1 m2 : denv) :
denv_wf_val E m1 denv_wf_val E m2 denv_wf_val E (denv_merge m1 m2).
......@@ -805,12 +823,22 @@ Section denv_spec.
destruct m2 as [|[denv2|] ms2]; try (destruct denv2); naive_solver.
Qed.
Ltac bool_decide_unfold :=
rewrite ?bool_decide_spec;
repeat match goal with
| H : Is_true (bool_decide _) |- _ => apply (bool_decide_unpack _) in H
| |- Is_true (bool_decide _) => apply bool_decide_pack
end.
Lemma denv_wf_merge_len (E : known_locs) (m1 m2 : denv) :
denv_wf_len E m1
denv_wf_len E m2
denv_wf_len E (denv_merge m1 m2).
Proof.
revert m1 m2. induction E; destruct m1, m2; naive_solver.
rewrite /denv_wf_len. bool_decide_unfold.
revert m1 m2. induction E; destruct m1, m2; try naive_solver omega.
simpl. intros.
apply le_n_S. eapply IHE; omega.
Qed.
Lemma denv_wf_merge E m1 m2 :
......@@ -829,23 +857,22 @@ Section denv_spec.
denv_wf E (denv_stack_merge ms).
Proof.
induction ms as [|m ms]; simpl; eauto.
- intros; unfold denv_wf; by destruct E.
- rewrite Forall_cons =>Hm. destruct Hm as [Hm Hms].
apply denv_wf_merge; eauto.
rewrite Forall_cons =>Hm. destruct Hm as [Hm Hms].
apply denv_wf_merge; eauto.
Qed.
Lemma denv_wf_val_unlock E m :
denv_wf_val E m denv_wf_val E (denv_unlock m).
Proof.
induction m as [|[denv|] ms]; simpl; eauto.
- destruct denv; simpl. intros. destruct_and!.
split_and. eapply dval_wf_mono; eauto. apply IHms; eauto.
induction m as [|[[]|] ms]; simpl; naive_solver.
Qed.
Lemma denv_wf_len_unlock E m :
denv_wf_len E m denv_wf_len E (denv_unlock m).
Proof.
revert m; induction E; destruct m; try naive_solver.
rewrite /denv_wf_len. bool_decide_unfold.
revert m; induction E; destruct m; try naive_solver omega.
simpl. intros. apply le_n_S. eapply IHE. omega.
Qed.
Lemma denv_wf_unlock E m :
......@@ -895,21 +922,36 @@ Section denv_spec.
denv_wf_len E m denv_delete_full_aux i m = Some (m', q, dv)
denv_wf_len E m'.
Proof.
intros. apply denv_delete_full_len in H1.
apply denv_wf_len_spec in H0.
apply denv_wf_len_spec. lia.
rewrite /denv_wf_len.
intros ? ?%denv_delete_full_len.
bool_decide_unfold. omega.
Qed.
Lemma denv_delete_full_idx i m m' q dv :
denv_delete_full_aux i m = Some (m', q, dv)
i < length m.
Proof.
revert i m' q dv. induction m as [|dio m] =>i m' q dv/=//.
destruct i.
- destruct dio as [[]|]; naive_solver.
- destruct (denv_delete_full_aux i m) as [[[? ?] ?]|] eqn:Hm =>//.
simpl. naive_solver lia.
Qed.
Lemma denv_delete_full_aux_wf E i m m' q dv :
denv_wf E m denv_delete_full_aux i m = Some (m', q, dv)
denv_wf E m' dval_wf E dv.
denv_wf E m' dval_wf E dv dloc_wf E (dLoc i 0).
Proof.
intros Hwf Hdel.
unfold denv_wf in Hwf; apply andb_True in Hwf as [Haux Hlen].
specialize (denv_delete_full_val_aux_wf E i m m' q dv Haux Hdel)
as [Hdel1 Hdel2]. split; last done.
unfold denv_wf. apply andb_True. split; first done.
by eapply denv_delete_full_len_aux_wf.
as [Hdel1 Hdel2]. repeat split; try fast_done.
- unfold denv_wf.
split_and; eauto using denv_delete_full_len_aux_wf.
- rewrite /dloc_wf. unfold denv_wf_len in Hlen.
bool_decide_unfold.
apply lookup_lt_is_Some.
apply denv_delete_full_idx in Hdel. lia.
Qed.
Lemma denv_lookup_wf E i m q dv :
......@@ -922,13 +964,9 @@ Section denv_spec.
eapply denv_delete_full_aux_wf; eauto.
Qed.
Lemma denv_wf_insert E i x q dv m:
denv_wf E m dval_wf E dv denv_wf E (denv_insert i x q dv m).
Proof. Admitted.
Lemma denv_wf_delete_full E dv i m m':
denv_wf E m denv_delete_full i m = Some (m', dv)
denv_wf E m' dval_wf E dv.
denv_wf E m' dval_wf E dv dloc_wf E (dLoc i 0).
Proof.
rewrite /denv_delete_full.
destruct (denv_delete_full_aux i m)
......@@ -937,65 +975,73 @@ Section denv_spec.
eapply denv_delete_full_aux_wf; eauto.
Qed.
Lemma denv_wf_cons E m dio :
denv_wf E (dio::m)
denv_wf E m.
Lemma denv_singleton_length i x q dv :
length (denv_singleton i x q dv) = (i+1)%nat.
Proof. induction i; naive_solver. Qed.
Lemma denv_wf_val_singleton E i x q dv :
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 :
dloc_wf E (dLoc i 0)
dval_wf E dv
denv_wf E (denv_singleton i x q dv).
Proof.
rewrite /denv_wf =>?.
destruct_and!.
apply denv_wf_len_spec in H1. simpl in *.
split_and; simpl in *;
destruct dio as [di|]; try (destruct di);
destruct_and?; try naive_solver.
apply denv_wf_len_spec. lia.
apply denv_wf_len_spec. lia.
rewrite /denv_wf /denv_wf_len /dloc_wf.
bool_decide_unfold. intros Hi Hdv.
split_and; bool_decide_unfold;
eauto using denv_wf_val_singleton.
rewrite denv_singleton_length.
apply lookup_lt_is_Some in Hi. omega.
Qed.
Lemma denv_wf_lookup_dval_wf E (m : denv) (k : nat) (di : denv_item) :
denv_wf E m
lookup k m = Some (Some di)
dval_wf E (denv_dval di).
Lemma denv_insert_length i x q dv m:
(length (denv_insert i x q dv m) = max (S i) (length m))%nat.
Proof.
revert k.
induction m as [|dio m]; simpl. inversion 2.
intros k Hwf. destruct k as [|k']; simpl.
- intros. simplify_eq/=.
unfold denv_wf in Hwf.
destruct_and!. simpl in *.
destruct di. destruct_and!. done.
- apply denv_wf_cons in Hwf.
by apply IHm.
revert m. induction i as [|i']=>m.
+ destruct m as [|dio m]; simpl. omega.
destruct dio as [[]|]; naive_solver omega.
+ destruct m as [|dio m]; cbn-[max].
* rewrite denv_singleton_length. lia.
* rewrite -Nat.succ_max_distr. f_equal.
eapply IHi'.
Qed.
Lemma denv_wf_len_insert E i x q dv m:
dloc_wf E (dLoc i 0)
denv_wf_len E m
denv_wf_len E (denv_insert i x q dv m).
Proof.
rewrite /denv_wf /denv_wf_len /dloc_wf. intros Hi.
bool_decide_unfold.
rewrite denv_insert_length.
apply lookup_lt_is_Some in Hi. lia.
Qed.
Lemma denv_wf_lookup_dloc_wf E (m : denv) (k : nat) (di : denv_item) :
denv_wf E m
lookup k m = Some (Some di)
dloc_wf E (dLoc k 0).
Lemma denv_wf_val_insert E i x q dv m:
denv_wf_val E m
dval_wf E dv
denv_wf_val E (denv_insert i x q dv m).
Proof.
intros Hwf. unfold denv_wf in Hwf.
destruct_and!.
apply denv_wf_len_spec in H1. simpl.
intros Hk%lookup_lt_Some.
apply bool_decide_pack.
apply lookup_lt_is_Some. lia.
revert m. induction i as [|i']=>m.
- destruct m as [|dio m]; simpl. naive_solver.
destruct dio as [[]|]; naive_solver.
- destruct m as [|dio m]; simpl.
{ intros. by apply denv_wf_val_singleton. }
destruct dio as [[]|]; naive_solver.
Qed.
Lemma denv_interp_mono E E' m :
denv_wf E m E `prefix_of` E'
denv_interp E m - denv_interp E' m.
Lemma denv_wf_insert E i x q dv m:
dloc_wf E (dLoc i 0)
denv_wf E m
dval_wf E dv
denv_wf E (denv_insert i x q dv m).
Proof.
intros Hwf Hpre.
rewrite /denv_interp.
apply big_sepL_mono.
iIntros (k dio Hk).
destruct dio as [[lv q dv]|]; simpl; last done.
pose (Hwf' := Hwf).
eapply denv_wf_lookup_dloc_wf in Hwf'; last eassumption.
eapply denv_wf_lookup_dval_wf in Hwf; last eassumption.
simpl in *.
rewrite (dval_interp_mono E E' dv Hwf Hpre).
rewrite (dloc_interp_mono E E' k _ Hwf' Hpre).
reflexivity.
rewrite /denv_wf => Hi Hm Hdv.
destruct_and!. split_and;
eauto using denv_wf_len_insert, denv_wf_val_insert.
Qed.
Lemma denv_wf_delete_frac_2 ms m ms' m' i E q dv :
......@@ -1023,7 +1069,11 @@ Section denv_spec.
intros.
assert (E `prefix_of` E ++ [l]). by eapply prefix_app_l; done.
assert (dval_wf (E ++ [l]) dv). eapply dval_wf_mono; done.
apply denv_wf_insert; eauto. eapply denv_wf_mono; done.
apply denv_wf_insert; eauto.
{ rewrite /dloc_wf. bool_decide_unfold.
apply lookup_lt_is_Some. rewrite app_length /=.
omega. }
by eapply denv_wf_mono.
Qed.
End denv_spec.
......@@ -446,11 +446,13 @@ Section vcg_spec.
Proof.
revert de ms ms' mNew dv. induction n as [|n IH];
intros de ms ms' mNew dv Hwfms Hwfde Hsp; simplify_eq/=; eauto.
{ destruct de; simplify_option_eq. split_and?; auto; first by destruct E.
by eapply vcg_eval_dexpr_wf. }
{ destruct de; simplify_option_eq.
repeat split_and; eauto.
by eapply vcg_eval_dexpr_wf. }
destruct de; simplify_eq /=.
- simplify_option_eq. split_and?; auto; first by destruct E.
by eapply vcg_eval_dexpr_wf.
- simplify_option_eq.
repeat split_and; eauto.
by eapply vcg_eval_dexpr_wf.
- destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
destruct (vcg_sp E (mNew1 :: ms1) (dce_subst E s dv1 de2))
as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq/=.
......@@ -917,7 +919,8 @@ Section vcg_spec.
rewrite /vcg_wp_continuation. iExists E,dw,_. iFrame.
eapply denv_wf_delete_full in Hdel; eauto. destruct_and!.
apply dcbin_op_eval_Some_wf in Hop; eauto.
repeat iSplit; eauto using denv_wf_insert. }
repeat iSplit; eauto.
iPureIntro. eapply denv_wf_insert; eauto. }
rewrite mapsto_wand_list_spec.
iDestruct ("Hwp" with "Hm'") as (w' ?) "Hwp".
iExists (dloc_interp E (dLoc i 0)), (dval_interp E dw), w'. iFrame; eauto.
......@@ -961,8 +964,9 @@ Section vcg_spec.
iIntros "Hl".
iExists E, dv2, (denv_insert i LLvl 1 dv2 m');
repeat (iSplit; first done).
iSplit. iPureIntro. apply denv_wf_insert; last done.
by destruct (denv_wf_delete_full E dv_old i m m' Hwf Hdel) as [Hdelwf ?].
iSplit. iPureIntro.
apply denv_wf_insert; eauto;
apply (denv_wf_delete_full E dv_old i m m' Hwf Hdel).
rewrite -denv_insert_interp. eauto with iFrame.
+ rewrite mapsto_wand_list_spec.
iSpecialize ("Hwp" with "[Hm]"); iFrame.
......
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