### Correctness proofs for `denv_delete_full` and `denv_delete_full_2`.

parent ea904806
 ... ... @@ -278,11 +278,9 @@ Section denv_spec. - simpl. iIntros (Hz). inversion Hz. - iIntros (Ha). simpl in Ha. destruct i as [|i]. + destruct dio as [[x q' dv']|]. * simpl in Ha. case_option_guard; simplify_eq/=. iIntros "[[Hl1 Hl2] Hm] /=". by iFrame. * simpl in Ha. inversion Ha. + destruct dio as [[x q' dv']|]; simplify_eq/=. case_option_guard; simplify_eq/=. iIntros "[[Hl1 Hl2] Hm] /=". by iFrame. + destruct (denv_delete_frac i m) as [[[mf q'] dv']|] eqn:Hdenv; simplify_eq/=. iIntros "[\$ Hm]". iSpecialize ("IHm" \$! _ (k+1)%nat with "[] [Hm]"); eauto. ... ... @@ -302,10 +300,40 @@ Section denv_spec. denv_interp E m ⊢ denv_interp E m' ∗ dloc_interp E (dLoc i) ↦C{q} dval_interp E dv. Proof. intros ?. by rewrite -!denv_interp_aux_0 denv_delete_frac_interp_aux. Qed. Lemma denv_delete_full_interp_aux E i k m m' q dv : denv_delete_full_aux i m = Some (m', q, dv) → denv_interp_aux E m k ⊢ denv_interp_aux E m' k ∗ dloc_interp E (dLoc (k+i)) ↦C{q} dval_interp E dv. Proof. iInduction m as [|dio m] "IHm" forall (i k m'). - simpl. iIntros (Hz). inversion Hz. - iIntros (Ha). simpl in Ha. destruct i as [|i]. + destruct dio as [[x q' dv']|]; simplify_eq/=. case_option_guard; simplify_eq/=. iIntros "[[Hl1 Hl2] Hm] /=". by iFrame. + destruct (denv_delete_full_aux i m) as [[[mf q'] dv']|] eqn:Hdenv; simplify_eq/=. iIntros "[\$ Hm]". iSpecialize ("IHm" \$! i (k+1)%nat with "[] [Hm]"); eauto. * iApply (big_sepL_mono with "Hm"). intros n y ?. simpl. assert ((k+1+n)%nat = (k + S n)%nat) as -> by omega. done. * assert ((k+1+i)%nat = (k + S i)%nat) as -> by omega. iDestruct "IHm" as "[H \$]". iApply (big_sepL_mono with "H"). intros n y ?. simpl. assert ((k+1+n)%nat = (k + S n)%nat) as -> by omega. done. Qed. 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_interp E (dLoc i) ↦C{1} dval_interp E dv. Proof. Admitted. Proof. rewrite /denv_delete_full. destruct (denv_delete_full_aux i m) as [[[??]?]|] eqn:Hm; intros ?; simplify_eq/=. case_option_guard; simplify_eq/=. by rewrite -!denv_interp_aux_0 denv_delete_full_interp_aux. 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) → ... ... @@ -328,7 +356,18 @@ Section denv_spec. (denv_interp E mIn1 ∗ (denv_interp E mOut -∗ denv_interp E mOut1 ∗ dloc_interp E (dLoc i) ↦C{1} dval_interp E dv)). Proof. Admitted. 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)). ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!