Prove `denv_merge` correct.

theories/vcgen/denv.v

@@ -34,7 +34,7 @@ Section denv.
     match dio1, dio2 with
     | None, dio | dio, None => dio
     | Some di1, Some di2 =>
-      Some (DenvItem (denv_level di1) ((denv_frac di1) + (denv_frac di2)) (denv_dval di1))
+      Some (DenvItem (denv_level di1 ⋅ denv_level di2) ((denv_frac di1) + (denv_frac di2)) (denv_dval di1))
     end.
 
   Fixpoint denv_merge (m1 m2 : denv) : denv :=
@@ -237,10 +237,37 @@ Section denv_spec.
      ∃ m', denv_interp E m ⊣⊢ dloc_interp E (dLoc i) ↦C{q} dval_interp E dv ∗ denv_interp E m'.
    Proof.  Admitted.
 
-   (* RK: this only holds in one direction *)
+   Lemma denv_merge_interp_aux E m1 m2 k :
+     denv_interp_aux E m1 k ∗ denv_interp_aux E m2 k ⊢ denv_interp_aux E (denv_merge m1 m2) k.
+   Proof.
+     iInduction m1 as [|dio1 m1] "IH1" forall (m2 k).
+     - destruct m2; iIntros "[_ $]".
+     - destruct m2 as [|dio2 m2]; simpl. iIntros "[$ _]".
+       iIntros "[[Hl1 H1] [Hl2 H2]]".
+       rewrite {4}/denv_interp_aux /=.
+       iSpecialize ("IH1" with "[H1 H2]").
+       { iSplitL "H1".
+         - iApply (big_sepL_mono with "H1"). intros n y ?. simpl.
+           assert ((k + S n)%nat = ((S k) + n)%nat) as -> by omega. reflexivity.
+         - iApply (big_sepL_mono with "H2"). intros n y ?. simpl.
+           assert ((k + S n)%nat = ((S k) + n)%nat) as -> by omega. reflexivity. }
+       (* TODO: this can be factored away *)
+       destruct dio1 as [d1|], dio2 as [d2|]; simpl; iFrame.
+       + destruct d1, d2. simpl. iDestruct (mapsto_value_agree with "Hl1 Hl2") as %->.
+         iDestruct (mapsto_combine with "Hl1 Hl2") as "$".
+         iApply (big_sepL_mono with "IH1"). intros n y ?. simpl.
+         assert ((k + S n)%nat = ((S k) + n)%nat) as -> by omega. done.
+       + iApply (big_sepL_mono with "IH1"). intros n y ?. simpl.
+         assert ((k + S n)%nat = ((S k) + n)%nat) as -> by omega. done.
+       + iApply (big_sepL_mono with "IH1"). intros n y ?. simpl.
+         assert ((k + S n)%nat = ((S k) + n)%nat) as -> by omega. done.
+       + iApply (big_sepL_mono with "IH1"). intros n y ?. simpl.
+         assert ((k + S n)%nat = ((S k) + n)%nat) as -> by omega. done.
+   Qed.
+
    Lemma denv_merge_interp E m1 m2 :
-     denv_interp E m1 ∗ denv_interp E m2 ⊣⊢ denv_interp E (denv_merge m1 m2).
-   Proof. Admitted.
+     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 E i m m' q dv :
      denv_delete_frac i m = Some (m', q, dv) →