wip

theories/vcgen/vcgen.v

@@ -354,9 +354,9 @@ Section vcg_spec.
 
   Lemma dce_subst_subst_comm E (x: string) (de: dcexpr) (dv: dval) :
     dcexpr_interp E (dce_subst E x dv de) =
-    (let: x := (dval_interp E dv) in (dcexpr_interp E de))%E.
+    (subst x (dval_interp E dv) (dcexpr_interp E de))%E.
   Proof.
-    Admitted.
+  Admitted.
 
   Lemma mapsto_wand_list_aux_spec E m Φ (k : nat) :
     mapsto_wand_list_aux E m Φ k -∗
@@ -519,22 +519,22 @@ Section vcg_spec.
           as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq /=.
         unfold popstack in Hsp.
         destruct ms2 as [|t ms2'] eqn:Houteq; simplify_eq/=.
-        (* specialize (IHn (mNew1 :: ms1)). *)
-        (* specialize (IHn de1). *)
         iPoseProof (IHn de1 ms) as "Hawp1"; first done.
         iPoseProof (IHn (dce_subst E s dv1 de2) (mNew1 :: ms1))
           as "Hawp2"; first done.
         iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
         iClear "Hawp1 Hawp2".
         iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
+        assert (Closed (s:b:[]) (dcexpr_interp E de2)). admit.
         iApply awp_bind.
-        * admit.
+        * exists (λ: s, dcexpr_interp E de2)%V. by unlock.
         * iApply (awp_wand with "Hawp1").
-        iIntros (?) "[% HmNew1]". simplify_eq/=. iClear "Hawp".
-        iDestruct ("Hawp2" with "HmNew1") as "[HmNew' Hawp2]".
-        rewrite dce_subst_subst_comm. iApply (awp_wand with "Hawp2").
-        iIntros (?) "[% HmNew1]". simplify_eq/=. iSplit; eauto.
-        rewrite- denv_merge_interp. iFrame.
+          iIntros (v) "[% HmNew1]". simplify_eq/=. iClear "Hawp".
+          iDestruct ("Hawp2" with "HmNew1") as "[HmNew' Hawp2]".
+          awp_let.
+          rewrite dce_subst_subst_comm. iApply (awp_wand with "Hawp2").
+          iIntros (?) "[% HmNew1]". simplify_eq/=. iSplit; eauto.
+          rewrite- denv_merge_interp. iFrame.
       + destruct (vcg_sp E ms de n)
           as [[[ms1 mNew1] dv1]|] eqn:Hsp'; simplify_eq /=.
         destruct (is_dloc _ _)