proved substitution lemma

theories/vcgen/vcgen.v

@@ -352,13 +352,35 @@ Section vcg_spec.
   Context `{amonadG Σ}.
 
 
+  Arguments subst _ _ !_ /.
+
+
+  Lemma de_subst_subst_comm E x de dv :
+    (dexpr_interp E (de_subst E x dv de)) =
+    (subst x (dval_interp E dv) (dexpr_interp E de)).
+  Proof.
+    induction de; simplify_eq /=;  simpl_subst;
+      try (repeat match goal with | [ H: _ = subst _ _ _ |- _  ] => rewrite H
+                  end; by simpl_subst);
+        by destruct (decide (x = s)).
+  Qed.
+
   Lemma dce_subst_subst_comm E (x: string) (de: dcexpr) (dv: dval) :
     dcexpr_interp E (dce_subst E x dv de) =
     (subst x (dval_interp E dv) (dcexpr_interp E de))%E.
   Proof.
-  Admitted.
+    induction de; simplify_eq /=; simpl_subst;
+      try (repeat match goal with | [ H: _ = subst _ _ _ |- _  ] => rewrite H
+                  end; by simpl_subst).
+    - by rewrite de_subst_subst_comm.
+    - destruct (decide (x = s)); simplify_eq /=; rewrite IHde1.
+      + rewrite decide_False; naive_solver.
+      + rewrite IHde2 decide_True; naive_solver.
+  Qed.
+
+  Arguments subst : simpl never.
 
-  Lemma mapsto_wand_list_aux_spec E m Φ (k : nat) :
+Lemma mapsto_wand_list_aux_spec E m Φ (k : nat) :
     mapsto_wand_list_aux E m Φ k -∗
     ([∗ list] n↦dio ∈ m, from_option
         (λ '{| denv_level := lv; denv_frac := q; denv_dval := dv |},