Commit 13e12a32 by Dan Frumin

### Prove `denv_insert_interp`.

parent 2e56ccb9
 ... ... @@ -156,15 +156,17 @@ Section properties. AsFractional (mapsto l x q v) (λ q, l ↦C[x]{q} v)%I q. Proof. split. done. apply _. Qed. Lemma mapsto_downgrade x l q v : l ↦C{q} v -∗ l ↦C[x]{q} v. Lemma mapsto_downgrade' x y l q v : x ≼ y → l ↦C[y]{q} v -∗ l ↦C[x]{q} v. Proof. rewrite mapsto_eq /mapsto_def. iDestruct 1 as (b' ?) "[\$ Ho]". iExists b'. iSplit; eauto. iPureIntro. transitivity ULvl; last done. apply lvl_included. destruct x; eauto. iPureIntro. transitivity y; done. Qed. Lemma mapsto_downgrade x l q v : l ↦C{q} v -∗ l ↦C[x]{q} v. Proof. apply mapsto_downgrade'. apply lvl_included. destruct x; eauto. Qed. Lemma mapsto_value_agree x x' l q q' v v' : l ↦C[x]{q} v -∗ l ↦C[x']{q'} v' -∗ ⌜v = v'⌝. Proof. rewrite mapsto_eq /mapsto_def. ... ...
 ... ... @@ -62,14 +62,14 @@ Section denv. end end. Fixpoint denv_insert (i : nat) (x: lvl) (q: frac) (dv: dval) (m: denv) : denv := Fixpoint denv_insert (i : nat) (x: lvl) (q: frac) (dv: dval) (m: denv) {struct m} : denv := match m with | [] => denv_singleton i x q dv | dio :: m' => match i with | O => match dio with | None => Some (DenvItem x q dv) :: m' | Some di => Some (DenvItem x ((denv_frac di) + q) dv) :: m' | Some di => Some (DenvItem ((denv_level di)⋅x) ((denv_frac di) + q) dv) :: m' end | S i => dio :: denv_insert i x q dv m' end ... ... @@ -88,7 +88,7 @@ Section denv. end end. Fixpoint denv_delete_full_aux (i : nat) (m : denv) : option (denv * frac * dval) := Fixpoint denv_delete_full_aux (i : nat) (m : denv) {struct m} : option (denv * frac * dval) := match m with | [] => None | dio :: m' => ... ... @@ -142,14 +142,100 @@ Section denv_spec. Definition penv_interp (m : penv) : iProp Σ := ([∗ list] p ∈ m, penv_loc p ↦C[penv_level p]{penv_frac p} penv_val p)%I. Definition denv_interp_aux (L : known_locs) (m : denv) (k : nat) : iProp Σ := ([∗ list] i ↦ dio ∈ m, from_option (λ '(DenvItem lv q dv), dloc_interp L (dLoc (k+i)) ↦C[lv]{q} dval_interp L dv) True dio)%I. (** helper lemmas *) Lemma denv_interp_aux_0 L m : denv_interp_aux L m 0 ≡ denv_interp L m. Proof. reflexivity. Qed. Lemma big_sepL_True {A} (l : list A) : ([∗ list] i ↦ x ∈ l, (True : iProp Σ)) ⊣⊢ True. Proof. induction l; simpl; eauto. by rewrite IHl left_id. Qed. Lemma denv_singleton_lookup i j x q dv di : lookup j (denv_singleton i x q dv) = Some (Some di) → (di = DenvItem x q dv ∧ i = j). Proof. revert j. induction i; intros j. - simpl. unfold lookup, list_lookup. destruct j; inversion 1. eauto. - simpl. destruct j; simpl; first by inversion 1. intros Hij. apply IHi in Hij as [-> ->]; eauto. Qed. (** / helper lemmas *) Lemma denv_interp_singleton_aux E i k x q dv : dloc_interp E (dLoc (k+i)) ↦C[x]{q} dval_interp E dv ⊣⊢ denv_interp_aux E (denv_singleton i x q dv) k. Proof. assert ((lookup i (denv_singleton i x q dv)) = Some (Some (DenvItem x q dv))) as Hdi. { induction i; simpl; eauto. } rewrite /denv_interp_aux. rewrite (big_sepL_delete' _ _ i); last eassumption. simpl. iFrame. iSplit. - iIntros "\$". iApply (big_sepL_impl (λ _ _, True)%I); first by rewrite big_sepL_True. iAlways. iIntros (? dio Hk) "_ %". destruct dio; eauto. apply denv_singleton_lookup in Hk as [? ->]. omega. - iIntros "[\$ _]". Qed. Lemma denv_insert_interp_aux E m i k x q dv : denv_interp_aux E m k ∗ dloc_interp E (dLoc (k+i)) ↦C[x]{q} dval_interp E dv ⊢ denv_interp_aux E (denv_insert i x q dv m) k. Proof. Opaque dval_interp dloc_interp. unfold denv_interp. iInduction m as [|dio m] "IHm" forall (i k). - simpl. rewrite denv_interp_singleton_aux. iIntros "[_ \$]". - Opaque denv_insert. destruct dio as [[x' q' dv']|]; simpl. + destruct i as [|i]. * iIntros "[H1 H2]". rewrite /denv_interp_aux. simpl. Transparent denv_insert. iDestruct "H1" as "[H1 \$]". iDestruct (mapsto_value_agree with "H1 H2") as %->. iDestruct (mapsto_combine with "H1 H2") as "H". iApply (mapsto_downgrade' with "H"). apply lvl_included. destruct x,x'; eauto. * iIntros "[H1 H2]". rewrite /denv_interp_aux. simpl. iDestruct "H1" as "[\$ H1]". iDestruct ("IHm" \$! i (k+1)%nat with "[H1 H2]") as "H". { assert ((k + 1 + i)%nat = (k + S i)%nat) as -> by omega. iFrame "H2". iApply (big_sepL_mono with "H1"). intros n y ?. simpl. assert ((k + 1 + n)%nat = (k + S n)%nat) as -> by omega. done. } iApply (big_sepL_mono with "H"). intros n y ?. simpl. assert ((k + 1 + n)%nat = (k + S n)%nat) as -> by omega. done. + destruct i as [|i]. * iIntros "[H1 H2]". rewrite /denv_interp_aux. simpl. iDestruct "H1" as "[_ H1]". iFrame. * iIntros "[H1 H2]". rewrite /denv_interp_aux. simpl. iDestruct "H1" as "[\$ H1]". iDestruct ("IHm" \$! i (k+1)%nat with "[H1 H2]") as "H". { assert ((k + 1 + i)%nat = (k + S i)%nat) as -> by omega. iFrame "H2". iApply (big_sepL_mono with "H1"). intros n y ?. simpl. assert ((k + 1 + n)%nat = (k + S n)%nat) as -> by omega. done. } 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_insert_interp E m i x q dv : denv_interp E (denv_insert i x q dv m) ⊣⊢ denv_interp E m ∗ dloc_interp E (dLoc i) ↦C[x]{q} dval_interp E dv. Proof. Admitted. denv_interp E m ∗ dloc_interp E (dLoc i) ↦C[x]{q} dval_interp E dv ⊢ denv_interp E (denv_insert i x q dv m). Proof. by rewrite -!denv_interp_aux_0 denv_insert_interp_aux. Qed. Lemma denv_lookup_interp i q dv m: denv_lookup i m = Some (q, dv) → exists m', m = (denv_insert i ULvl q dv m'). Proof. Admitted. Lemma denv_lookup_interp E i q dv m: denv_lookup i m = Some (q, dv) → ∃ 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 E m1 m2 : ... ... @@ -163,7 +249,7 @@ Section denv_spec. Lemma denv_delete_full_interp E i m m' dv : denv_delete_full i m = Some (m', dv) → denv_interp E m' ∗ dloc_interp E (dLoc i) ↦C{1} dval_interp E dv ⊣⊢ denv_interp E m. denv_interp E m ⊢ denv_interp E m' ∗ dloc_interp E (dLoc i) ↦C{1} dval_interp E dv. Proof. Admitted. Lemma denv_delete_frac_2_interp E i mIn mOut mIn1 mOut1 q dv : ... ...
 ... ... @@ -62,7 +62,7 @@ Section splitenv. rewrite /ListOfMapsto => HΓls /=. iDestruct 1 as "[Hl H]". cbn. rewrite Hlit. unfold penv_interp in *. rewrite HΓls. rewrite denv_insert_interp. iFrame. simpl. rewrite Hi. done. rewrite -denv_insert_interp. iFrame. simpl. rewrite Hi. done. Qed. Global Instance list_of_mapsto_cons_dValUnknown E Γls ps v i l x q : ... ... @@ -75,7 +75,7 @@ Section splitenv. rewrite /ListOfMapsto => HΓls /=. iDestruct 1 as "[Hl H]". cbn. unfold penv_interp in *. rewrite HΓls. rewrite denv_insert_interp. iFrame. simpl. rewrite Hi. done. rewrite -denv_insert_interp. iFrame. simpl. rewrite Hi. done. Qed. Lemma tac_envs_split_mapsto Γs_in Γs_out Γls Γp c ps P: ... ...
 ... ... @@ -294,7 +294,7 @@ Section vcg_spec. iApply (awp_wand with "Hawp"). iIntros (?) "[% HmOut1]". simplify_eq/=. iExists _, _. iSplit; eauto. iDestruct ("Hm" with "HmOut1") as "[HmOut2 \$]". iIntros "Hl". iSplit; eauto. rewrite denv_insert_interp. rewrite -denv_insert_interp. by iFrame. - specialize (IHde1 mIn mOut). destruct (vcg_sp E mIn mOut de1) as [[[mIn1 mOut1] dv1]|]; simplify_eq /=. ... ... @@ -318,7 +318,7 @@ Section vcg_spec. iExists _. rewrite -denv_merge_interp. iDestruct ("Hl" with "[\$HmOut1 \$HmOut2]") as "[HmOut3 \$]". iIntros "Hl". iSplit; eauto. rewrite denv_insert_interp. rewrite -denv_insert_interp. iFrame "Hl HmOut3". - specialize (IHde1 mIn mOut). destruct (vcg_sp E mIn mOut de1) as [[[mIn1 mOut1] dv1]|]; simplify_eq /=. ... ... @@ -391,13 +391,12 @@ Section vcg_spec. Proof. rewrite /vcg_wp_load. destruct (is_dloc E dv) as [i|] eqn:Hdloc. + destruct (denv_lookup i m) as [[q dv'] |] eqn:Hlkp; simpl; simplify_eq /=. * apply (denv_lookup_interp i q dv' m) in Hlkp. apply is_dloc_some in Hdloc. destruct Hlkp as [m0 Hlkp]. subst. iIntros "Hm Hwp". iExists (dloc_interp E (dLoc i)), q, (dval_interp E dv'). rewrite denv_insert_interp. iDestruct "Hm" as "[Hm0 Hi]". iFrame. iSplit. by simplify_eq /=. iIntros "Hl". iExists E, dv', (denv_insert i ULvl q dv' m0); iSplit; first done. rewrite denv_insert_interp. iFrame. * destruct (denv_lookup_interp E i q dv' m) as [m0 Hm0]; first assumption. rewrite Hm0. iIntros "[Hi Hm0] HΦ". apply is_dloc_some in Hdloc. simplify_eq/=. iExists (dloc_interp E (dLoc i)), q, (dval_interp E dv'). iSplit. simplify_eq /=; done. iFrame. iIntros "Hl". iExists E, dv', m; iSplit; first done. iFrame. rewrite Hm0. iFrame. * rewrite mapsto_wand_list_spec. iIntros "Hm Hwp". iSpecialize ("Hwp" with "Hm"). simpl. iDestruct "Hwp" as (q dv') "[Hl Hwp]". apply is_dloc_some in Hdloc. subst. iExists (dloc_interp E (dLoc i)), q, (dval_interp E dv'). iSplit; first done. ... ... @@ -423,156 +422,12 @@ Section vcg_spec. iApply (a_load_spec_exists_frac with "[Hm]"). iApply (awp_wand with "Hm"). iIntros (v) "H". iDestruct "H" as (E' dv m' <-) "(Hm & Hwp)". iApply (vcg_wp_load_correct with "Hm Hwp"). - admit. - admit. - admit. - admit. - iApply (vcg_wp_unknown_correct with "Hm Hwp"). Admitted. (* - iIntros "H". rewrite /vcg_wp. destruct (vcg_sp E m [] de1) as [[[mIn mOut] dv]|] eqn:Heqsp; last first. { destruct (vcg_sp E m [] de2) as [[[mIn mOut] dv]|] eqn:Heqsp2; last first. { iApply (vcg_wp_unknown_correct with "[\$Hm] [\$H]"). } fold vcg_wp. iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption. iDestruct ("Hsp" with "Hm") as "[Hm Hde2]". iClear "Hsp". clear Heqsp2 Heqsp. rewrite IHde1. iSpecialize ("Hm" with "H"). iApply (a_store_spec _ _ (λ l, ∃ (E' : known_locs) (dv0 : dval) (m' : denv), ⌜dval_interp E' dv0 = #l⌝ ∧ denv_interp E' m' ∗ wp_interp E' (vcg_wp_store E' dv0 dv (denv_merge mOut m') (Φ E')) )%I (λ v : val, ⌜v = dval_interp E dv⌝ ∧ denv_interp E mOut)%I with "[Hm] [\$Hde2]"); fold dcexpr_interp. * iApply (awp_wand with "Hm"). iIntros (v) "H". iDestruct "H" as (E' dv1 m') "(<- & Hdv1 & Hwp)". unfold vcg_wp_store. destruct (is_dloc E' dv1) as [i|] eqn:Hdloc. ** apply is_dloc_some in Hdloc. subst. iExists (dloc_interp E' (dLoc i)); iSplit; first done. destruct (denv_delete_full i (denv_merge mOut m')) as [[m'0 dv_old]|] eqn:Hdel; simplify_eq/=. *** apply (denv_delete_full_interp E') in Hdel. rewrite denv_insert_interp. rewrite IHde; last done. iDestruct "HmIn" as "[HmIn1 Hawp]". admit. * admit. (*wp_interp E' (MapstoStarFull (dLoc i) (λ _ : dval, MapstoWand (dLoc i) dv LLvl 1 (Φ E' [] dv)))*) * rewrite IHde1. } fold vcg_wp. iApply (awp_wand with "H"). iIntros (v) "H". iExists (dValUnknown v). eauto 30 with iFrame. } rewrite mapsto_star_list_spec. iDestruct "H" as "[Henv Hde1]". rewrite mapsto_wand_list_spec IHde1. iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption. iDestruct ("Hsp" with "Henv") as "[Hm1 Hde2]". iSpecialize ("Hde1" with "Hm1"). iApply (a_store_spec _ _ (λ l, ∃ dl m', ⌜dloc_interp E dl = l⌝ ∧ wp_interp E (mapsto_wand_list mOut (MapstoStarFull dl (λ _ : dval, MapstoWand dl dv LLvl 1 (Φ m' dv)))))%I with "[Hde1] [\$Hde2]"). { iApply (awp_wand with "Hde1"). iIntros (v) "Hex". iDestruct "Hex" as (dv0 m' <-) "Hwp"; simplify_eq /=. iDestruct "Hwp" as (dl ->) "Hwp"; simplify_eq /=. iExists (dloc_interp E dl); iSplit; first done. iExists dl, m'; iSplit; first auto. eauto with iFrame. } iNext. iIntros (l w) "Hex". iDestruct "Hex" as (dl m' <-) "Hwp"; simplify_eq /=. rewrite mapsto_wand_list_spec. iIntros "[-> H]". iSpecialize ("Hwp" with "[\$H]"); simpl. iDestruct "Hwp" as (w) "(Hdl & Hwp)". iExists (dval_interp E w). iFrame. iIntros "Hdl". iExists _, m'; iSplit; first done. by iApply "Hwp". } destruct dv; last first. { simpl. iDestruct "H" as (dl ->) "H". rewrite mapsto_star_list_spec. iDestruct "H" as "[Henv Hde2]". rewrite mapsto_wand_list_spec IHde2. iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption. iDestruct ("Hsp" with "Henv") as "[Hm1 Hde1]". iClear "Hsp". iSpecialize ("Hde2" with "Hm1"). iApply (a_store_spec _ _ (λ l, ⌜dloc_interp E dl = l⌝ ∧ denv_interp E mOut)%I with "[Hde1] [\$Hde2]"). { iApply (awp_wand with "Hde1"). iIntros (v) "Hex". iDestruct "Hex" as (->) "Hwp"; simplify_eq /=. iExists (dloc_interp E dl); iSplit; first done. eauto with iFrame. } iNext. iIntros (l w) "[<- Hout] Hex". iDestruct "Hex" as (dv m' <-) "Hwp"; simplify_eq /=. rewrite mapsto_wand_list_spec. iSpecialize ("Hwp" with "[\$Hout]"); simpl. iDestruct "Hwp" as (w) "(Hdl & Hwp)". iExists (dval_interp E w). iFrame. iIntros "Hdl". iExists dv, m'; iSplit; first done; eauto with iFrame. by iApply "Hwp". } destruct d; simpl; try by iExFalso. { destruct d as [i|]. + rewrite mapsto_star_list_spec. iDestruct "H" as "[Henv Hde2]". rewrite mapsto_wand_list_spec IHde2. iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption. iDestruct ("Hsp" with "Henv") as "[Hm1 Hde1]". iClear "Hsp". iSpecialize ("Hde2" with "Hm1"). iApply ((a_store_spec _ _ (λ l, ⌜l = dloc_interp E (dLoc i)⌝ ∧ denv_interp E mOut)%I (λ v : val, (∃ (dv : dval) (m' : denv), ⌜dval_interp E dv = v⌝ ∧ wp_interp E (mapsto_wand_list mOut (MapstoStarFull (dLoc i) (λ _ : dval, MapstoWand (dLoc i) dv LLvl 1 match denv_replace_full i dv m' with | Some mf => Φ mf dv | None => Base False end))))%I)) with "[Hde1] [\$Hde2]"). { iApply (awp_wand with "Hde1"). iIntros (v) "Hex". iDestruct "Hex" as (->) "Hwp". by iExists (dloc_interp E (dLoc i)); repeat (iSplit; first done). } iNext. iIntros (l w) "[-> Hout] Hex". iDestruct "Hex" as (dv m' <-) "Hwp"; simplify_eq /=. rewrite mapsto_wand_list_spec. iSpecialize ("Hwp" with "[\$Hout]"). simpl. iDestruct "Hwp" as (dv0) "[Hl Hwp]". iExists (dval_interp E dv0). iFrame. iIntros "Hl". iSpecialize ("Hwp" with "Hl"). destruct (denv_replace_full i dv m') as [mf |]; last first; try by iExFalso. iExists dv, mf; iSplit; first auto. done. + simpl. iDestruct "H" as (dl Hdl) "H". rewrite mapsto_star_list_spec. iDestruct "H" as "[Henv Hde2]". rewrite mapsto_wand_list_spec IHde2. iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption. iDestruct ("Hsp" with "Henv") as "[Hm1 Hde1]". iClear "Hsp". iSpecialize ("Hde2" with "Hm1"). iApply (a_store_spec _ _ (λ l, ⌜dloc_interp E dl = l⌝ ∧ denv_interp E mOut)%I with "[Hde1] [\$Hde2]"). { iApply (awp_wand with "Hde1"). iIntros (v) "Hex". iDestruct "Hex" as (->) "Hwp"; simplify_eq /=. iExists (dloc_interp E dl); iSplit; first done. eauto with iFrame. } iNext. iIntros (l0 w) "[<- Hout] Hex". iDestruct "Hex" as (dv m' <-) "Hwp"; simplify_eq /=. rewrite mapsto_wand_list_spec. iSpecialize ("Hwp" with "[\$Hout]"); simpl. iDestruct "Hwp" as (w) "(Hdl & Hwp)". iExists (dval_interp E w). iFrame. iIntros "Hdl". iExists dv, m'; iSplit; first done; eauto with iFrame. by iApply "Hwp". } iDestruct "H" as (dl Hdl) "H". rewrite mapsto_star_list_spec. iDestruct "H" as "[Henv Hde2]". rewrite mapsto_wand_list_spec IHde2. iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption. iDestruct ("Hsp" with "Henv") as "[Hm1 Hde1]". iClear "Hsp". iSpecialize ("Hde2" with "Hm1"). iApply (a_store_spec _ _ (λ l, ⌜dloc_interp E dl = l⌝ ∧ denv_interp E mOut)%I with "[Hde1] [\$Hde2]"). { iApply (awp_wand with "Hde1"). iIntros (v) "Hex". iDestruct "Hex" as (->) "Hwp"; simplify_eq /=. iExists (dloc_interp E dl); iSplit; first done. eauto with iFrame. } iNext. iIntros (l w) "[<- Hout] Hex". iDestruct "Hex" as (dv m' <-) "Hwp"; simplify_eq /=. rewrite mapsto_wand_list_spec. iSpecialize ("Hwp" with "[\$Hout]"); simpl. iDestruct "Hwp" as (w) "(Hdl & Hwp)". iExists (dval_interp E w). iFrame. iIntros "Hdl". iExists dv, m'; iSplit; first done; eauto with iFrame. by iApply "Hwp". - iIntros "H". simpl. destruct (vcg_sp E m de1) as [[[m1 m2] dv]|] eqn:Heqsp; last first. { destruct (vcg_sp E m de2) as [[[m1 m2] dv]|] eqn:Heqsp'; last first. { iApply (awp_wand with "H"). iIntros (v) "H". iExists (dValUnknown v). eauto 30 with iFrame. } rewrite mapsto_star_list_spec. iDestruct "H" as "[Henv Hde1]". rewrite mapsto_wand_list_spec IHde1. iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption. iDestruct ("Hsp" with "Henv") as "[Hm1 Hde2]". iSpecialize ("Hde1" with "Hm1"). iApply (a_bin_op_spec with "[\$Hde1] [\$Hde2]"). iNext. iIntros (? ?) "Hex". iDestruct "Hex" as (? ? <-) "Hwp"; simplify_eq /=. rewrite mapsto_wand_list_spec. iIntros "[-> H]". iSpecialize ("Hwp" with "[\$H]"). simpl. iDestruct "Hwp" as (w) "(% & Hwp)". iExists (dval_interp E w). iSplit. iPureIntro. by apply dbin_op_eval_correct. iExists _, _; iSplit; first done. eauto with iFrame. } rewrite mapsto_star_list_spec. iDestruct "H" as "[Henv Hde2]". rewrite mapsto_wand_list_spec IHde2. iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption. iDestruct ("Hsp" with "Henv") as "[Hm1 Hde1]". iSpecialize ("Hde2" with "Hm1"). iApply (a_bin_op_spec with "[\$Hde1] [\$Hde2]"). iNext. iIntros (? ?) "(% & H) Hex". iDestruct "Hex" as (? ? <-) "Hwp"; simplify_eq /=. rewrite mapsto_wand_list_spec. iSpecialize ("Hwp" with "[\$H]"). simpl. iDestruct "Hwp" as (w) "(% & Hwp)". iExists (dval_interp E w). iSplit. iPureIntro. by apply dbin_op_eval_correct. eauto with iFrame. - iIntros "H". rewrite IHde. iApply a_un_op_spec. iApply (awp_wand with "H"). iIntros (v) "Hex". iDestruct "Hex" as (dv m' <-) "H /=". iDestruct "H" as (dw) "[% H]". iExists _; iFrame. iSplit; eauto. iPureIntro. by apply dun_op_eval_correct. - iIntros "H". rewrite IHde1. iApply (a_sequence_spec with "[H]"). { exists (λ: <>, dcexpr_interp E de2)%V. by unlock. } iApply (awp_wand with "H"). iIntros (v) "Hex". iDestruct "Hex" as (? ? <-) "H". simpl. iModIntro. rewrite IHde2. awp_seq. iApply (awp_wand with "H"). eauto. - iIntros "Hawp". iApply (awp_wand with "Hawp"). iIntros (v) "H". rewrite wp_interp_sane_sound. iExists _,_; iFrame; eauto. Qed. *) Lemma tac_vcg_sound Γs_in Γs_out Γls Γp m c e R Φ E dce : MapstoListFromEnv Γs_in Γs_out Γls → ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!