Commit 76d85093 authored by Dan Frumin's avatar Dan Frumin
Browse files

Fix up Robbert's changes.

parents 695e875f e31372f3
......@@ -88,11 +88,11 @@ Section denv.
Fixpoint denv_delete_frac_stack (i : nat) (ms : list denv) : option (list denv * frac * 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
| 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_aux (i : nat) (m : denv) {struct m} : option (denv * frac * dval) :=
......@@ -108,7 +108,7 @@ Section denv.
end
end.
Fixpoint denv_delete_full_stack_aux (i : nat) (ms : list denv) {struct ms} : option (list denv * frac * dval) :=
Fixpoint denv_delete_full_stack_aux (i : nat) (ms : list denv) : option (list denv * frac * dval) :=
match ms with
| [] => None
| m::ms' =>
......@@ -132,58 +132,38 @@ Section denv.
Definition denv_unlock (m: denv) : denv :=
map (λ dio, ''(DenvItem _ q dv) dio; Some (DenvItem ULvl q dv)) m.
Definition denv_delete_frac_2 (i : nat) (m1 m2 : denv) : option (denv * denv * frac * dval) :=
match denv_delete_frac i m1 with
| Some (m1', q, dv) => Some (m1', m2, q, dv)
| None =>
match denv_delete_frac i m2 with
| Some (m2', q, dv) => Some (m1, m2', q, dv)
| None => None
end
end.
Definition denv_delete_full_2 (i : nat) (m1 m2: denv) : option (denv * denv * dval) :=
match denv_delete_full_aux i m1, denv_delete_full_aux i m2 with
| None, Some (m2', q, dv) => guard (q = 1)%Qp; Some (m1, m2', dv)
| Some (m1', q, dv), None => guard (q = 1)%Qp; Some (m1', m2, dv)
| Some (m1', q1, dv), Some (m2', q2, _) => guard (q1 + q2 = 1)%Qp; Some (m1', m2', dv)
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)%Qp; Some (ms', m', dv)
| _, _ => None
end.
Definition denv_delete_frac_3 (i : nat) (m1 : denv) (m2 : list denv) (m3 : denv) : option (denv * list denv * denv * frac * dval) :=
match denv_delete_frac i m1 with
| Some (m1', q, dv) => Some (m1', m2, m3, q, dv)
Definition denv_delete_frac_2 (i : nat) (ms : list denv) (m : denv) : option (list denv * denv * frac * dval) :=
match denv_delete_frac_stack i ms with
| Some (ms', q, dv) => Some (ms', m, q, dv)
| None =>
match denv_delete_frac_stack i m2 with
| Some (m2', q, dv) => Some (m1, m2', m3, q, dv)
| None =>
match denv_delete_frac i m3 with
| Some (m3', q, dv) => Some (m1, m2, m3', q, dv)
| None => None
end
end
match denv_delete_frac i m with
| Some (m', q, dv) => Some (ms, m', q, dv)
| None => None
end
end.
End denv.
Definition denv_delete_full_3 (i : nat) (m1 : denv) (m2 : list denv) (m3 : denv) : option (denv * list denv * denv * dval) :=
match denv_delete_full_aux i m1, denv_delete_full_stack_aux i m2, denv_delete_full_aux i m3 with
| Some (m1', q, dv), None, None => guard (q = 1)%Qp; Some (m1', m2, m3, dv)
| None, Some (m2', q, dv),None => guard (q = 1)%Qp; Some (m1, m2', m3, dv)
| None, None, Some (m3', q, dv) => guard (q = 1)%Qp; Some (m1, m2, m3', dv)
| Some (m1', q1, dv), Some (m2', q2, _), None => guard (q1 + q2 = 1)%Qp; Some (m1', m2', m3, dv)
| Some (m1', q1, dv), None, Some (m3', q2, _) => guard (q1 + q2 = 1)%Qp; Some (m1', m2, m3', dv)
| None, Some (m2', q1, dv), Some (m3', q2, _) => guard (q1 + q2 = 1)%Qp; Some (m1, m2', m3', dv)
| Some (m1', q1, dv), Some (m2', q2, _), Some (m3', q3, _) => guard (q1 + q2 + q3 = 1)%Qp; Some (m1', m2', m3', dv)
| None, None, None => None
end.
Lemma is_dloc_some E dv i: is_dloc E dv = Some i dv = dLitV (dLitLoc (dLoc i)).
Proof.
destruct dv as [d|]; [destruct d|]; intros; simplify_eq /=.
by destruct d; simplify_eq.
Qed.
End denv.
Lemma denv_merge_nil_r m :
denv_merge m [] = m.
Proof. induction m; simpl; eauto. Qed.
Section denv_spec.
Context `{amonadG Σ}.
Lemma is_dloc_some E dv i: is_dloc E dv = Some i dv = dLitV (dLitLoc (dLoc i)).
Proof. destruct dv as [d|]; [destruct d|]; intros; simplify_eq /=. by destruct d; simplify_eq. Qed.
(** ** Interpretations *)
Definition denv_interp (L : known_locs) (m : denv) : iProp Σ :=
([ list] i dio m,
......@@ -214,7 +194,7 @@ Section denv_spec.
Lemma big_sepL_True {A} (l : list A) :
([ list] i x l, (True : iProp Σ)) True.
Proof. induction l; simpl; eauto. by rewrite IHl left_id. Qed.
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).
......@@ -451,40 +431,6 @@ Section denv_spec.
iIntros "[Hl Hm]". iApply denv_delete_full_interp_aux_flip; eauto with iFrame.
Qed.
Lemma denv_delete_frac_2_interp E i mIn mOut mIn1 mOut1 q dv :
denv_delete_frac_2 i mIn mOut = Some (mIn1, mOut1, q, dv)
denv_interp E mIn -
(denv_interp E mIn1 (denv_interp E mOut - denv_interp E mOut1
dloc_interp E (dLoc i) C{q} dval_interp E dv)).
Proof.
rewrite /denv_delete_frac_2. intros.
destruct (denv_delete_frac i mIn) as [[[m1' q'] dv']|] eqn:Hin; simplify_eq/=.
- rewrite (denv_delete_frac_interp _ _ mIn mIn1); eauto.
iIntros "[$ $] $".
- destruct (denv_delete_frac i mOut) as [[[m1' q'] dv']|] eqn:Hout; simplify_eq/=.
rewrite (denv_delete_frac_interp _ _ mOut mOut1); eauto.
iIntros "$ [$ $]".
Qed.
Lemma denv_delete_full_2_interp E i mIn mOut mIn1 mOut1 dv :
denv_delete_full_2 i mIn mOut = Some (mIn1, mOut1, dv)
denv_interp E mIn -
(denv_interp E mIn1 (denv_interp E mOut - denv_interp E mOut1
dloc_interp E (dLoc i) C{1} dval_interp E dv)).
Proof.
rewrite /denv_delete_full_2 -!denv_interp_aux_0. intros.
destruct (denv_delete_full_aux i mIn) as [[[m1 q1] dv1]|] eqn:Hin; simplify_eq/=;
destruct (denv_delete_full_aux i mOut) as [[[m2 q2] dv2]|] eqn:Hout; simplify_eq;
case_option_guard; simplify_eq/=.
- rewrite denv_delete_full_interp_aux; eauto.
iIntros "[$ Hl1] Hm". iDestruct (denv_delete_full_interp_aux with "Hm") as "[$ Hl2]"; eauto.
iDestruct (mapsto_value_agree with "Hl1 Hl2") as %->.
iCombine "Hl1 Hl2" as "Hl". simplify_eq/=. rewrite H1. iFrame.
- rewrite denv_delete_full_interp_aux; eauto.
iIntros "[$ $] $".
- iIntros "$". rewrite denv_delete_full_interp_aux; eauto.
Qed.
Lemma denv_unlock_interp E m :
denv_interp E m - U (denv_interp E (denv_unlock m)).
Proof.
......@@ -574,27 +520,20 @@ Section denv_spec.
- f_equal. by eapply IHms.
Qed.
Lemma denv_delete_frac_3_length i m1 m2 m3 m1' m2' m3' q dv :
denv_delete_frac_3 i m1 m2 m3 = Some (m1', m2', m3', q, dv)
length m2 = length m2'.
Lemma denv_delete_frac_2_length i ms m ms' m' q dv :
denv_delete_frac_2 i ms m = Some (ms', m', q, dv)
length ms = length ms'.
Proof.
rewrite /denv_delete_frac_3.
destruct (denv_delete_frac i m1) as [[[m' q'] dv']|]; first by inversion 1; eauto.
destruct (denv_delete_frac_stack i m2) as [[[m' q'] dv']|] eqn:Hms; intros; simplify_eq/=.
- eapply denv_delete_frac_stack_length. eassumption.
- destruct (denv_delete_frac i m3) as [[[m' q'] dv']|]; simplify_eq/=. done.
rewrite /denv_delete_frac_2. intros.
repeat case_match; simplify_eq/=; eauto using denv_delete_frac_stack_length.
Qed.
Lemma denv_delete_full_3_length i m1 m2 m3 m1' m2' m3' dv :
denv_delete_full_3 i m1 m2 m3 = Some (m1', m2', m3', dv)
length m2 = length m2'.
Lemma denv_delete_full_2_length i ms m ms' m' dv :
denv_delete_full_2 i ms m = Some (ms', m', dv)
length ms = length ms'.
Proof.
rewrite /denv_delete_full_3.
destruct (denv_delete_full_aux i m1) as [[[m1'' q1'] dv1']|];
destruct (denv_delete_full_stack_aux i m2) as [[[m2'' q2'] dv2']|] eqn:Heq;
destruct (denv_delete_full_aux i m3) as [[[m3'' q3'] dv3']|];
try (case_option_guard); intros; simplify_eq/=; eauto;
eapply denv_delete_full_stack_aux_length; eauto.
rewrite /denv_delete_full_2. intros.
repeat case_match; simplify_option_eq; eauto using denv_delete_full_stack_aux_length.
Qed.
Lemma denv_delete_frac_stack_interp E i ms ms' q dv :
......@@ -632,77 +571,43 @@ Section denv_spec.
iIntros "$ $".
Qed.
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 mOut mOut1 E
(denv_interp E mNew - denv_interp E mNew1 dloc_interp E (dLoc i) C dval_interp E dv))).
Lemma denv_delete_full_2_interp E i ms m ms' m' dv :
denv_delete_full_2 i ms m = Some (ms', m', dv)
denv_stack_interp ms ms' E
(denv_interp E m - denv_interp E m' dloc_interp E (dLoc i) C dval_interp E dv)%I.
Proof.
rewrite /denv_delete_full_3. do 2 rewrite -denv_interp_aux_0. intros.
destruct (denv_delete_full_aux i mIn) as [[[m1 q1] dv1]|] eqn:Hin;
destruct (denv_delete_full_stack_aux i mOut) as [[[m2 q2] dv2]|] eqn:Hout;
destruct (denv_delete_full_aux i mNew) as [[[m3 q3] dv3]|] eqn:Hnew; simplify_eq;
rewrite /denv_delete_full_2. intros.
destruct (denv_delete_full_stack_aux i ms) as [[[ms1 q1] dv1]|] eqn:Hms;
destruct (denv_delete_full_aux i m) as [[[m2 q2] dv2]|] eqn:Hm; simplify_eq;
case_option_guard; simplify_eq/=.
- rewrite denv_delete_full_interp_aux; eauto.
iIntros "[$ Hl1] /=". iPoseProof denv_delete_full_stack_interp as "H"; first eassumption.
iApply (denv_stack_interp_mono with "H").
iIntros "Hl2". rewrite -!denv_interp_aux_0.
- iApply denv_stack_interp_mono; first by iApply denv_delete_full_stack_interp.
iIntros "Hl1". rewrite -!denv_interp_aux_0.
rewrite denv_delete_full_interp_aux; last done.
iIntros "[$ Hl3]".
iDestruct (mapsto_value_agree with "Hl1 Hl2") as %->.
iDestruct (mapsto_value_agree with "Hl2 Hl3") as %->.
iCombine "Hl1 Hl2 Hl3" as "Hl".
(* STUPID: cannnot rewrite by associativity in BI *)
assert ((q1 + (q2 + q3))%Qp = 1%Qp) as ->.
{ transitivity (q1+q2+q3)%Qp; last done.
by rewrite (assoc Qp_plus q1 q2 q3). }
iFrame.
- rewrite denv_delete_full_interp_aux; eauto.
iIntros "[$ Hl1] /=". iPoseProof denv_delete_full_stack_interp as "H"; first eassumption.
iApply (denv_stack_interp_mono with "H").
iIntros "Hl2". rewrite -!denv_interp_aux_0.
iIntros "$".
iDestruct (mapsto_value_agree with "Hl1 Hl2") as %->.
iCombine "Hl1 Hl2" as "Hl". rewrite H1. done.
- rewrite denv_delete_full_interp_aux; last done.
iIntros "[$ Hl1] /=". iApply denv_stack_interp_intro.
rewrite -!denv_interp_aux_0 denv_delete_full_interp_aux; last done.
iIntros "[$ Hl2]".
iDestruct (mapsto_value_agree with "Hl1 Hl2") as %->.
iCombine "Hl1 Hl2" as "Hl". rewrite H1. done.
- rewrite denv_delete_full_interp_aux; last done.
iIntros "[$ Hl2]". iApply denv_stack_interp_intro.
iIntros "$". iFrame.
- iIntros "$". iPoseProof denv_delete_full_stack_interp as "H"; first eassumption.
iApply (denv_stack_interp_mono with "H").
iIntros "Hl1". rewrite -!denv_interp_aux_0 denv_delete_full_interp_aux; last done.
iIntros "[$ Hl2]".
iDestruct (mapsto_value_agree with "Hl1 Hl2") as %->.
iCombine "Hl1 Hl2" as "Hl". rewrite H1. done.
- iIntros "$". iPoseProof denv_delete_full_stack_interp as "H"; first eassumption.
iApply (denv_stack_interp_mono with "H").
iIntros "$ $".
- iIntros "$". iApply denv_stack_interp_intro.
iCombine "Hl1 Hl2" as "Hl". rewrite H1.
iFrame.
- iApply denv_stack_interp_mono; 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.
iIntros "$".
eauto with iFrame.
Qed.
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 mOut mOut1 E
(denv_interp E mNew - denv_interp E mNew1 dloc_interp E (dLoc i) C{q} dval_interp E dv))).
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)
denv_stack_interp ms ms' E
(denv_interp E m - denv_interp E m' dloc_interp E (dLoc i) C{q} dval_interp E dv)%I.
Proof.
rewrite /denv_delete_frac_3. intros.
destruct (denv_delete_frac i mIn) as [[[m1' q'] dv']|] eqn:Hin; simplify_eq/=.
- rewrite (denv_delete_frac_interp _ _ mIn mIn1); eauto.
iIntros "[$ Hl]". iApply denv_stack_interp_intro. eauto with iFrame.
- destruct (denv_delete_frac_stack i mOut) as [[[m2' q'] dv']|] eqn:Hout; simplify_eq/=.
+ iIntros "$". iPoseProof (denv_delete_frac_stack_interp) as "H"; first eassumption.
iApply (denv_stack_interp_mono with "H"). iIntros "$ $".
+ destruct (denv_delete_frac i mNew) as [[[m3' q'] dv']|] eqn:Hnew; simplify_eq/=.
iIntros "$". iApply denv_stack_interp_intro.
rewrite (denv_delete_frac_interp _ _ mNew mNew1); eauto.
rewrite /denv_delete_frac_2. intros.
destruct (denv_delete_frac_stack i ms) as [[[ms1 q1] dv1]|] eqn:Hms; simplify_eq/=.
- iApply denv_stack_interp_mono;
first by iApply denv_delete_frac_stack_interp.
eauto with iFrame.
- destruct (denv_delete_frac i m) as [[[m2 q2] dv2]|] eqn:Hnew; simplify_eq/=.
iApply denv_stack_interp_intro.
rewrite -!denv_interp_aux_0 denv_delete_frac_interp_aux; last done.
eauto with iFrame.
Qed.
Lemma denv_stack_merge_interp E ms :
......@@ -730,7 +635,15 @@ Section denv_spec.
- destruct denv1; simpl. intros. destruct_and!.
destruct m2 as [|doenv2 ms2]; simpl.
+ split_and; eauto.
Admitted.
Admitted.
Lemma denv_wf_stack_merge ms E :
Forall (denv_wf E) ms
denv_wf E (denv_stack_merge ms).
Proof.
induction ms as [|m ms]; simpl; eauto. rewrite Forall_cons =>Hm. destruct Hm as [Hm Hms].
apply denv_wf_merge; eauto.
Qed.
Lemma denv_wf_unlock E m :
denv_wf E m denv_wf E (denv_unlock m).
......@@ -761,26 +674,21 @@ Section denv_spec.
denv_interp E m - denv_interp E' m.
Proof. Admitted.
Lemma denv_wf_delete_frac_3 mIn mOut mNew mIn' mOut' mNew' i E q dv :
denv_wf E mIn
Forall (denv_wf E) mOut
denv_wf E mNew
denv_delete_frac_3 i mIn mOut mNew = Some (mIn', mOut', mNew', q, dv)
denv_wf E mIn'
Forall (denv_wf E) mOut'
denv_wf E mNew'
Lemma denv_wf_delete_frac_2 ms m ms' m' i E q dv :
Forall (denv_wf E) ms
denv_wf E m
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.
Proof. Admitted.
Lemma denv_wf_delete_full_3 mIn mOut mNew mIn' mOut' mNew' i E dv :
denv_wf E mIn
Forall (denv_wf E) mOut
denv_wf E mNew
denv_delete_full_3 i mIn mOut mNew = Some (mIn', mOut', mNew', dv)
denv_wf E mIn'
Forall (denv_wf E) mOut'
denv_wf E mNew'
Lemma denv_wf_delete_full_2 ms m ms' m' i E dv :
Forall (denv_wf E) ms
denv_wf E m
denv_delete_full_2 i ms m = Some (ms', m', dv)
Forall (denv_wf E) ms'
denv_wf E m'
dval_wf E dv.
Proof. Admitted.
End denv_spec.
This diff is collapsed.
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