Commit 86b94266 by Hai Dang

Minor cleanup with subjectively

parent 592f1ae4
 ... @@ -630,21 +630,6 @@ Proof. ... @@ -630,21 +630,6 @@ Proof. - eauto with iFrame. - eauto with iFrame. Qed. Qed. (* TODO: move *) Lemma own_loc_na_own_loc_prim_subjectively n q v : n ↦{q} v ⊢ ∃ (q' : Qp) (C' : cell), ▷ n p↦{q'} C'. Proof. rewrite own_loc_na_own_loc_prim. iDestruct 1 as (C) "En". iExists q, C. iNext. by iApply monPred_subjectively_intro. Qed. Lemma own_loc_na_view_at_prim n q v V : @{V} n ↦{q} v ⊢ ∃ (q' : Qp) (C' : cell), ▷ n p↦{q'} C'. Proof. rewrite own_loc_na_own_loc_prim_subjectively. iDestruct 1 as (q' C) "En". iExists q', C. iNext. by rewrite view_at_subjectively monPred_subjectively_idemp. Qed. Lemma all_slocs_node_access_prim t0 LVs t (l' : loc) Vb : Lemma all_slocs_node_access_prim t0 LVs t (l' : loc) Vb : fst <\$> toHeadHist t0 LVs !! t = Some #l' → fst <\$> toHeadHist t0 LVs !! t = Some #l' → @{Vb} all_slocs LVs ⊢ ∃ (q' : Qp) (C' : cell), ▷ l' p↦{q'} C'. @{Vb} all_slocs LVs ⊢ ∃ (q' : Qp) (C' : cell), ▷ l' p↦{q'} C'. ... @@ -656,7 +641,7 @@ Proof. ... @@ -656,7 +641,7 @@ Proof. apply elem_of_list_lookup_2 in Eq2. apply elem_of_list_lookup_2 in Eq2. rewrite (all_slocs_node_next_access _ _ _ Eq2). rewrite (all_slocs_node_next_access _ _ _ Eq2). iIntros "[As En]". iDestruct "En" as (q' on) "En". iIntros "[As En]". iDestruct "En" as (q' on) "En". by rewrite view_at_view_at (shift_0 l') own_loc_na_view_at_prim. by rewrite view_at_view_at (shift_0 l') own_loc_na_view_at_own_loc_prim_subjectively. Qed. Qed. Lemma all_slocs_app LVs LVs' : Lemma all_slocs_app LVs LVs' : ... @@ -1058,7 +1043,7 @@ Proof. ... @@ -1058,7 +1043,7 @@ Proof. move : Eq1. by apply elem_of_list_lookup_2. } move : Eq1. by apply elem_of_list_lookup_2. } iDestruct "As" as "[As oN]". iDestruct "oN" as (qn' on') "oN". iDestruct "As" as "[As oN]". iDestruct "oN" as (qn' on') "oN". rewrite (view_at_view_at _ V0). iSplitL "oN". rewrite (view_at_view_at _ V0). iSplitL "oN". - by rewrite (shift_0 n') own_loc_na_view_at_prim. - by rewrite (shift_0 n') own_loc_na_view_at_own_loc_prim_subjectively. - iIntros (?? (_ & ? & _)). by iApply (all_slocs_node_access_prim with "As"). } - iIntros (?? (_ & ? & _)). by iApply (all_slocs_node_access_prim with "As"). } iIntros (b t' v' Vr V2 ζ2 ζn) "(F & #sV2 & #sH2 & H & As & CASE)". iIntros (b t' v' Vr V2 ζ2 ζn) "(F & #sV2 & #sH2 & H & As & CASE)". ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!