Prove denv_interp_mono.

theories/vcgen/dcexpr.v

@@ -294,7 +294,7 @@ Fixpoint dcexpr_interp (E: known_locs) (de: dcexpr) : expr :=
 
 (** Well-foundness of dcexpr w.r.t. known_locs *)
 
-Fixpoint dloc_wf (E: known_locs) (dl : dloc) : bool :=
+Definition dloc_wf (E: known_locs) (dl : dloc) : bool :=
   match dl with
   | dLoc i _ => bool_decide (is_Some (E !! i))
   | _  => true

theories/vcgen/denv.v

@@ -725,7 +725,6 @@ Section denv_spec.
       destruct d. naive_solver.
   Qed.
 
-
   Lemma denv_wf_mono E E' m :
     denv_wf E m → E `prefix_of` E' → denv_wf E' m.
   Proof.
@@ -778,7 +777,6 @@ Section denv_spec.
     revert m1 m2. induction E; destruct m1, m2; naive_solver.
   Qed.
 
-
   Lemma denv_wf_merge E m1 m2 :
     denv_wf E m1 → denv_wf E m2 → denv_wf E (denv_merge m1 m2).
   Proof.
@@ -903,99 +901,67 @@ Section denv_spec.
     eapply denv_delete_full_aux_wf; eauto.
   Qed.
 
- (*  Lemma denv_interp_aux_mono E E' m (i:nat) :
-    dloc_wf E (dLoc i 0) →
-    denv_wf E m → E `prefix_of` E' →
-    denv_interp_aux E m i -∗ denv_interp_aux E' m i.
+  Lemma denv_wf_cons E m dio :
+    denv_wf E (dio::m) →
+    denv_wf E m.
   Proof.
-    iInduction m as [|dio m i] "IHm" forall (i);
-    iIntros (Hdl Hwf Hpre) "H";
-    unfold denv_wf in Hwf; apply andb_True in Hwf as [Hval Hlen].
-    - by unfold denv_interp_aux.
-    - specialize (denv_wf_len_mono_r E [dio] m Hlen) as H1.
-      specialize (denv_wf_val_mono_r E [dio] m Hval) as H2.
-      iAssert (⌜denv_wf_len E m⌝)%I as "H1". done.
-      iAssert (⌜denv_wf_val E m⌝)%I as "H2". done.
-      iSpecialize ("IHm" with "[H1] [H2]" ); eauto.
-      iPureIntro. unfold denv_wf. eauto.
-      unfold denv_interp_aux.
-      rewrite !big_sepL_cons.
-      iDestruct "H" as "[H1 H2]".
-      iSplitL "H1".
-      + destruct dio as  [[lvl q] dv|] ; simplify_eq /=; last done.
-        assert (dval_interp E denv_dval0 = dval_interp E' denv_dval0).
-        apply andb_True in Hval as [Haux1 Haux2].
-        apply dval_interp_mono; done. rewrite H0.
-        assert (dloc_interp E (dLoc (i + 0) 0) =
-                dloc_interp E' (dLoc (i + 0) 0)).
-        apply dloc_interp_mono; last done.
-        by rewrite PeanoNat.Nat.add_0_r.
-        rewrite H3. iFrame.
-      + iSpecialize ("IHm" $! Hpre).
-        iAssert ([∗ list] i0↦dio0 ∈ m, from_option
-         (λ '{| denv_level := lv; denv_frac := q; denv_dval := dv |},
-          dloc_interp E
-           (dLoc (i + 1 + (i0) 0) ↦C[lv]{q} dval_interp E dv) True dio0)%I
-          with "[H2]" as "H".
-        * iApply (big_sepL_mono with "H2").
-          { intros n y ?. simpl.
-            assert ((i + S n)%nat = (S (i + n))%nat) as -> by omega. admit.  }
-        * iSpecialize ("IHm" with "H").
-        iApply (big_sepL_mono with "IHm").
-        intros n y ?. simpl.
-        assert ((i + S n)%nat = (S (i + n))%nat) as -> by omega. done.
-  Admitted. *)
+    rewrite /denv_wf =>?.
+    destruct_and!.
+    apply denv_wf_len_spec in H1. simpl in *.
+    split_and; simpl in *;
+      destruct dio as [di|]; try (destruct di);
+      destruct_and?; try naive_solver.
+    apply denv_wf_len_spec. lia.
+    apply denv_wf_len_spec. lia.
+  Qed.
 
-  Lemma denv_interp_aux_mono E E' m (i:nat) :
-    denv_wf E m → E `prefix_of` E' →
-    denv_interp_aux E m i -∗ denv_interp_aux E' m i.
+  Lemma denv_wf_lookup_dval_wf E (m : denv) (k : nat) (di : denv_item) :
+    denv_wf E m →
+    lookup k m = Some (Some di) →
+    dval_wf E (denv_dval di).
   Proof.
-    iIntros (Hwf Hpre) "H".
-    unfold denv_wf in Hwf; apply andb_True in Hwf as [Haux Hlen].
-    iInduction m as [|dio m i] "IHm" forall (i).
-    - by unfold denv_interp_aux.
-    - specialize (denv_wf_len_mono_r E [dio] m Hlen) as H1.
-      specialize (denv_wf_val_mono_r E [dio] m Haux) as H2.
-      iAssert (⌜denv_wf_len E m⌝)%I as "H1". done.
-      iAssert (⌜denv_wf_len E m⌝)%I as "H2". done.
-      iSpecialize ("IHm" with "[H1] [H2]" ); eauto.
-      unfold denv_interp_aux.
-      rewrite !big_sepL_cons.
-      iDestruct "H" as "[H1 H2]".
-      iSplitL "H1".
-      + destruct dio as  [[lvl q dv]|] ; simplify_eq /=; last done.
-        assert (dval_interp E dv = dval_interp E' dv) as ->.
-        { destruct_and!. by apply dval_interp_mono. }
-        assert (dloc_interp E (dLoc (i + 0) 0) =
-                dloc_interp E' (dLoc (i + 0) 0)) as ->.
-        { apply dloc_interp_mono; auto.
-          rewrite !Nat.add_0_r. admit. }
-        iFrame.
-      + iSpecialize ("IHm" $! (S i)).
-        iAssert ([∗ list] i0↦dio0 ∈ m, from_option
-         (λ '{| denv_level := lv; denv_frac := q; denv_dval := dv |},
-          dloc_interp E
-           (dLoc (S i + i0) 0) ↦C[lv]{q} dval_interp E dv) True dio0)%I
-          with "[H2]" as "H".
-        iApply (big_sepL_mono with "H2").
-        { intros n y ?. simpl.
-          assert ((i + S n)%nat = (S (i + n))%nat) as -> by omega. done. }
-        iSpecialize ("IHm" with "H").
-        iApply (big_sepL_mono with "IHm").
-        intros n y ?. simpl.
-        assert ((i + S n)%nat = (S (i + n))%nat) as -> by omega. done.
-  Admitted.
+    revert k.
+    induction m as [|dio m]; simpl. inversion 2.
+    intros k Hwf. destruct k as [|k']; simpl.
+    - intros. simplify_eq/=.
+      unfold denv_wf in Hwf.
+      destruct_and!. simpl in *.
+      destruct di. destruct_and!. done.
+    - apply denv_wf_cons in Hwf.
+      by apply IHm.
+  Qed.
+
+  Lemma denv_wf_lookup_dloc_wf E (m : denv) (k : nat) (di : denv_item) :
+    denv_wf E m →
+    lookup k m = Some (Some di) →
+    dloc_wf E (dLoc k 0).
+  Proof.
+    intros Hwf. unfold denv_wf in Hwf.
+    destruct_and!.
+    apply denv_wf_len_spec in H1. simpl.
+    intros Hk%lookup_lt_Some.
+    apply bool_decide_pack.
+    apply lookup_lt_is_Some. lia.
+  Qed.
 
-  (* This shoud be fixed *)
   Lemma denv_interp_mono E E' m :
     denv_wf E m → E `prefix_of` E' →
     denv_interp E m -∗ denv_interp E' m.
   Proof.
-    intros. destruct m; first by naive_solver.
-    rewrite -!denv_interp_aux_0 denv_interp_aux_mono //.
+    intros Hwf Hpre.
+    rewrite /denv_interp.
+    apply big_sepL_mono.
+    iIntros (k dio Hk).
+    destruct dio as [[lv q dv]|]; simpl; last done.
+    pose (Hwf' := Hwf).
+    eapply denv_wf_lookup_dloc_wf in Hwf'; last eassumption.
+    eapply denv_wf_lookup_dval_wf in Hwf; last eassumption.
+    simpl in *.
+    rewrite (dval_interp_mono E E' dv Hwf Hpre).
+    rewrite (dloc_interp_mono E E' k _ Hwf' Hpre).
+    reflexivity.
   Qed.
 
-
   Lemma denv_wf_delete_frac_2 ms m ms' m' i E q dv :
     Forall (denv_wf E) ms →
     denv_wf E m →