Prove `denv_delete_frac` and `denv_delete_frac_2` correct.

theories/vcgen/denv.v

@@ -75,7 +75,7 @@ Section denv.
       end
     end.
 
-  Fixpoint denv_delete_frac (i : nat) (m : denv) : option (denv * frac * dval) :=
+  Fixpoint denv_delete_frac (i : nat) (m : denv) {struct m} : option (denv * frac * dval) :=
     match m with
     | [] => None
     | dio :: m' =>
@@ -269,10 +269,38 @@ Section denv_spec.
      denv_interp E m1 ∗ denv_interp E m2 ⊢ denv_interp E (denv_merge m1 m2).
    Proof. by rewrite -!denv_interp_aux_0 denv_merge_interp_aux. Qed.
 
+   Lemma denv_delete_frac_interp_aux E i k m m' q dv :
+     denv_delete_frac 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']|].
+         * simpl in Ha.
+           case_option_guard; simplify_eq/=.
+           iIntros "[[Hl1 Hl2] Hm] /=". by iFrame.
+         * simpl in Ha. inversion Ha.
+       + destruct (denv_delete_frac i m) as [[[mf q'] dv']|] eqn:Hdenv; simplify_eq/=.
+         iIntros "[$ Hm]".
+         iSpecialize ("IHm" $! _ (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_frac_interp E i m m' q dv :
      denv_delete_frac i m = Some (m', q, dv) →
-     denv_interp E m' ∗ dloc_interp E (dLoc i) ↦C{q} dval_interp E dv ⊣⊢ denv_interp E m.
-   Proof. Admitted.
+     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 E i m m' dv :
      denv_delete_full i m = Some (m', dv) →
@@ -285,7 +313,14 @@ Section denv_spec.
      (denv_interp E mIn1 ∗ (denv_interp E mOut -∗ denv_interp E mOut1 ∗
        dloc_interp E (dLoc i) ↦C{q} dval_interp E dv)).
    Proof.
-   Admitted.
+     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) →