Commit 695e875f authored by Dan Frumin's avatar Dan Frumin
Browse files

Simplify `denv_stack_interp`, per Robbert's suggestion

parent 61dde255
......@@ -190,12 +190,12 @@ Section denv_spec.
from_option (λ '(DenvItem lv q dv),
dloc_interp L (dLoc i) C[lv]{q} dval_interp L dv) True dio)%I.
Fixpoint denv_stack_interp (mOut mOut' : list denv) E (P : iProp Σ) :=
match mOut,mOut' with
| m::ms,m'::ms' => (denv_interp E m - denv_interp E m' (denv_stack_interp ms ms' E P))%I
| ms,[] => (([ list] de ms, denv_interp E de) - P)%I
| [],ms' => (([ list] de ms', denv_interp E de) P)%I
end.
Fixpoint denv_stack_interp (ms1 ms2 : list denv) E (P : iProp Σ) :=
match ms1,ms2 with
| m::ms,m'::ms' => denv_stack_interp ms ms' E (denv_interp E m - denv_interp E m' P)
| [],[] => P
| _, _ => False
end%I.
Definition penv_interp (m : penv) : iProp Σ :=
([ list] p m, penv_loc p C[penv_level p]{penv_frac p} penv_val p)%I.
......@@ -498,27 +498,18 @@ Section denv_spec.
Qed.
(** *** Stack interpretation properties *)
Lemma denv_stack_interp_nil_r ms E P :
denv_stack_interp ms [] E P (([ list] de ms, denv_interp E de) - P).
Proof. induction ms as [|m ms]; simpl; eauto. Qed.
Lemma denv_stack_interp_nil_l ms E P :
denv_stack_interp [] ms E P (([ list] de ms, denv_interp E de) P).
Proof. induction ms as [|m ms]; simpl; eauto. by rewrite !left_id. Qed.
Lemma denv_stack_interp_mono ms1 ms2 E P Q :
denv_stack_interp ms1 ms2 E P -
(P - Q) -
denv_stack_interp ms1 ms2 E Q.
Proof.
iIntros "HP Hw".
iInduction (ms1) as [|m1 ms1] "IH1" forall (ms2); simpl.
- destruct ms2. iIntros "_". iApply "Hw". by iApply "HP".
iDestruct "HP" as "[$ HP]". by iApply "Hw".
- destruct ms2.
+ iIntros "Hm". iApply "Hw". by iApply "HP".
+ iIntros "Hm1". iDestruct ("HP" with "Hm1") as "[$ HP]".
iApply ("IH1" with "HP Hw").
iInduction (ms1) as [|m1 ms1] "IH1" forall (ms2 P Q); simpl.
- destruct ms2; eauto. by iApply "Hw".
- destruct ms2; eauto.
iApply ("IH1" with "HP [Hw]").
iIntros "HP Hm". iDestruct ("HP" with "Hm") as "[$ HP]".
by iApply "Hw".
Qed.
Lemma denv_stack_interp_frame ms1 ms2 E P Q :
......@@ -527,9 +518,7 @@ Section denv_spec.
denv_stack_interp ms1 ms2 E (PQ).
Proof.
iIntros "HP HQ".
iInduction ms1 as [|m1' ms1] "IH" forall (ms2); simpl; destruct ms2; iFrame.
iIntros "Hm1'". iDestruct ("HP" with "Hm1'") as "[$ HP]".
iApply ("IH" with "HP HQ").
iApply (denv_stack_interp_mono with "HP [HQ]"). eauto with iFrame.
Qed.
Lemma denv_stack_interp_intro ms1 E P :
......@@ -537,8 +526,8 @@ Section denv_spec.
denv_stack_interp ms1 ms1 E P.
Proof.
iIntros "HP".
iInduction ms1 as [|m1' ms1] "IH"; simpl; first by iFrame.
iIntros "$". by iApply "IH".
iInduction ms1 as [|m1' ms1] "IH" forall (P); simpl; first by iFrame.
iApply "IH". eauto with iFrame.
Qed.
(* DF: does not hold *)
......@@ -553,56 +542,14 @@ Section denv_spec.
denv_stack_interp ms1 ms3 E (PQ).
Proof.
iIntros "HP HQ".
iInduction ms1 as [|m1 ms1] "IH1" forall (ms2 ms3); simpl.
- iInduction ms2 as [|m2 ms2] "IH2" forall (ms3); simpl.
+ iSpecialize ("HP" with "[]"); first done.
destruct ms3; simpl; by iFrame.
+ destruct ms3; simpl.
* iDestruct "HP" as "[Hm $]". iIntros "_". by iApply "HQ".
* iDestruct "HP" as "[[Hm2 Hms2] HP]". iDestruct ("HQ" with "Hm2") as "[$ HQ]".
iAssert ( ms3, ([ list] de ms2, denv_interp E de) P
- denv_stack_interp ms2 ms3 E Q
- ([ list] de ms3, denv_interp E de) P Q)%I as "IH".
{ iIntros (ms0). destruct ms2,ms0 as [|m0 ms0]; simpl.
- iIntros "[_ $] HQ". by iApply "HQ".
- iIntros "[_ $] [$ $]".
- iIntros "[H $] HQ". by iApply "HQ".
- iIntros "HP HQ". iSpecialize ("IH2" $! (m0::ms0) with "HP"). simpl.
by iApply "IH2". }
iApply ("IH" with "[Hms2 HP] HQ"). iFrame.
- iInduction ms2 as [|m2 ms2] "IH2" forall (ms3); simpl.
+ destruct ms3; simpl.
{ iSpecialize ("HQ" with "[]"); first done. iIntros "H".
iFrame. by iApply "HP". }
iIntros "H". iDestruct "HQ" as "[[$ Hms3] HQ]".
iApply ("IH1" $! [] with "[H HP]").
{ iApply denv_stack_interp_nil_r. iIntros "H2". iApply "HP". iFrame. }
{ iApply denv_stack_interp_nil_l. iFrame. }
+ destruct ms3 as [|m3 ms3]; simpl.
* iIntros "[Hm1 Hms1]".
iDestruct ("HP" with "Hm1") as "[Hm2 HP]".
iSpecialize ("IH1" $! ms2 []). simpl.
rewrite !denv_stack_interp_nil_r.
iApply ("IH1" with "HP [HQ Hm2] Hms1").
iIntros "H". iApply "HQ". iFrame.
* iIntros "Hm1". iDestruct ("HP" with "Hm1") as "[Hm2 HP]".
iDestruct ("HQ" with "Hm2") as "[$ HQ]".
iApply ("IH1" with "HP HQ").
Qed.
(* The property that we need *)
Lemma denv_stack_interp_snoc m1 m2 ms1 ms2 E P :
length ms1 = length ms2
denv_stack_interp ms1 ms2 E (denv_interp E m1 - denv_interp E m2 P)
denv_stack_interp (ms1++[m1]) (ms2++[m2]) E P.
Proof.
revert ms2. induction ms1 as [|m1' ms1]; intros ms2; simpl.
- destruct ms2.
+ simpl. rewrite !left_id. eauto.
+ inversion 1.
- destruct ms2 as [|m2' ms2].
+ inversion 1.
+ intros ?. rewrite IHms1; eauto.
iInduction ms1 as [|m1 ms1] "IH1" forall (ms2 ms3 P Q); simpl;
destruct ms2 as [|m2 ms2]; eauto with iFrame;
destruct ms3 as [|m3 ms3]; eauto with iFrame.
simpl. iDestruct ("IH1" with "HP HQ") as "H".
iApply (denv_stack_interp_mono with "H").
iIntros "[HP HQ] Hm1".
iDestruct ("HP" with "Hm1") as "[Hm2 $]".
iDestruct ("HQ" with "Hm2") as "[$ $]".
Qed.
Lemma denv_delete_frac_stack_length i ms ms' q dv :
......@@ -652,15 +599,12 @@ Section denv_spec.
Lemma denv_delete_frac_stack_interp E i ms ms' q dv :
denv_delete_frac_stack i ms = Some (ms', q, dv)
denv_stack_interp (reverse ms) (reverse ms') E (dloc_interp E (dLoc i) C{q} dval_interp E dv)%I.
denv_stack_interp ms ms' E (dloc_interp E (dLoc i) C{q} dval_interp E dv)%I.
Proof.
iInduction ms as [|m ms] "IH" forall (ms'); iIntros (Hdel); simplify_eq/=.
destruct (denv_delete_frac i m) as [[[m' q'] dv']|] eqn:Hm; simplify_eq/=.
- rewrite !reverse_cons -denv_stack_interp_snoc; last done.
iApply denv_stack_interp_intro. iIntros "Hm". by iApply denv_delete_frac_interp.
- 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:Hms; simplify_eq/=.
rewrite !reverse_cons -denv_stack_interp_snoc; last first.
{ rewrite !reverse_length. eapply denv_delete_frac_stack_length. eassumption. }
iSpecialize ("IH" with "[]"). eauto.
iApply (denv_stack_interp_mono with "IH").
iIntros "$ $".
......@@ -668,26 +612,21 @@ Section denv_spec.
Lemma denv_delete_full_stack_interp E i ms ms' q dv :
denv_delete_full_stack_aux i ms = Some (ms', q, dv)
denv_stack_interp (reverse ms) (reverse ms') E (dloc_interp E (dLoc i) C{q} dval_interp E dv)%I.
denv_stack_interp ms ms' E (dloc_interp E (dLoc i) C{q} dval_interp E dv)%I.
Proof.
iInduction ms as [|m ms] "IH" forall (ms' q dv); iIntros (Hdel); 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:Hms; simplify_eq/=.
+ rewrite !reverse_cons -denv_stack_interp_snoc; last first.
{ rewrite !reverse_length. by eapply denv_delete_full_stack_aux_length. }
iSpecialize ("IH" with "[]"). eauto.
+ iSpecialize ("IH" with "[]"). eauto.
iApply (denv_stack_interp_mono with "IH").
iIntros "Hl Hm". rewrite -!denv_interp_aux_0 denv_delete_full_interp_aux /=; last done.
iDestruct "Hm" as "[$ Hl2]".
iDestruct (mapsto_value_agree with "Hl Hl2") as %->.
iCombine "Hl Hl2" as "$".
+ rewrite !reverse_cons -denv_stack_interp_snoc; last done.
iApply denv_stack_interp_intro.
+ 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:Hms; simplify_eq/=.
rewrite !reverse_cons -denv_stack_interp_snoc; last first.
{ rewrite !reverse_length. by eapply denv_delete_full_stack_aux_length. }
iSpecialize ("IH" with "[]"). eauto.
iApply (denv_stack_interp_mono with "IH").
iIntros "$ $".
......@@ -696,7 +635,7 @@ Section denv_spec.
Lemma denv_delete_full_3_interp E i mIn mOut mNew mIn1 mOut1 mNew1 dv :
denv_delete_full_3 i mIn mOut mNew = Some (mIn1, mOut1, mNew1, dv)
denv_interp E mIn -
(denv_interp E mIn1 (denv_stack_interp (reverse mOut) (reverse mOut1) E
(denv_interp E mIn1 (denv_stack_interp mOut mOut1 E
(denv_interp E mNew - denv_interp E mNew1 dloc_interp E (dLoc i) C dval_interp E dv))).
Proof.
rewrite /denv_delete_full_3. do 2 rewrite -denv_interp_aux_0. intros.
......@@ -751,7 +690,7 @@ Section denv_spec.
Lemma denv_delete_frac_3_interp E i mIn mOut mNew mIn1 mOut1 mNew1 q dv :
denv_delete_frac_3 i mIn mOut mNew = Some (mIn1, mOut1, mNew1, q, dv)
denv_interp E mIn -
(denv_interp E mIn1 (denv_stack_interp (reverse mOut) (reverse mOut1) E
(denv_interp E mIn1 (denv_stack_interp mOut mOut1 E
(denv_interp E mNew - denv_interp E mNew1 dloc_interp E (dLoc i) C{q} dval_interp E dv))).
Proof.
rewrite /denv_delete_frac_3. intros.
......@@ -774,16 +713,6 @@ Section denv_spec.
- iIntros "[Hm Hms]". rewrite -denv_merge_interp. iFrame. by iApply "IH".
Qed.
Lemma denv_stack_reverse E ms :
([ list] de (reverse ms), denv_interp E de) ([ list] de ms, denv_interp E de).
Proof.
iInduction ms as [|m ms] "IH"; simpl.
- iIntros "_". rewrite /denv_interp //.
- rewrite reverse_cons big_sepL_app big_sepL_singleton. iIntros "[Hms $]".
by iApply "IH".
Qed.
(** ** Well-foundness of denv *)
Lemma denv_wf_mono E E' m :
denv_wf E m E `prefix_of` E' denv_wf E' m.
......
......@@ -262,7 +262,7 @@ Section vcg_spec.
vcg_sp E mIn mOut de = Some (mIn', mOut', mNew', dv)
(denv_interp E mIn -
denv_interp E mIn'
denv_stack_interp (reverse mOut) (reverse mOut') E
denv_stack_interp mOut mOut' E
(awp (dcexpr_interp E de) R (λ v, v = dval_interp E dv denv_interp E mNew'))).
Proof.
revert mIn mOut mIn' mOut' mNew' dv. induction de;
......@@ -343,9 +343,7 @@ Section vcg_spec.
{ exists (λ: <>, dcexpr_interp E de2)%V. by unlock. }
unfold popstack in Hsp.
destruct mOut2 as [|t mOut2'] eqn:Houteq; simplify_eq/=.
iFrame "HmIn2". rewrite !reverse_cons.
rewrite -denv_stack_interp_snoc; last first.
{ rewrite !reverse_length. apply vcg_sp_length in Hsp2. eauto. }
iFrame "HmIn2".
iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
iApply a_sequence_spec. iApply (awp_wand with "Hawp1").
......@@ -363,11 +361,11 @@ Section vcg_spec.
denv_interp E m -
denv_interp E mIn denv_interp E (denv_stack_merge mOut) awp (dcexpr_interp E de) R (λ v, v = dval_interp E dv denv_interp E mNew).
Proof.
iIntros (?) "Hm".
iIntros (Hsp) "Hm".
iDestruct (vcg_sp_correct' with "Hm") as "[$ Hawp]"; first eassumption.
rewrite reverse_nil denv_stack_interp_nil_l.
iDestruct "Hawp" as "[HmOut $]". iApply denv_stack_merge_interp.
by iApply denv_stack_reverse.
pose (vcg_sp_length _ _ _ _ _ _ _ _ Hsp) as Hlen.
assert (mOut = []) as -> by (destruct mOut; eauto; inversion Hlen).
iFrame "Hawp". by rewrite /denv_interp //.
Qed.
Lemma denv_wf_stack_merge ms E :
......
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