From iris.algebra Require Import cmra auth gmap frac agree. From iris.bi.lib Require Import fractional. From iris.base_logic.lib Require Export own. From iris.proofmode Require Import tactics. From iris_c.lib Require Import list. Set Default Proof Using "Type". Local Open Scope nat_scope. Inductive lvl := | LLvl : lvl | ULvl : lvl. Canonical Structure lvlC := leibnizC lvl. Instance lvl_EqDecision : EqDecision lvl. Proof. solve_decision. Defined. Instance lvl_op : Op lvl := λ lv1 lv2, match lv1, lv2 with | ULvl,_ => ULvl | _,ULvl => ULvl | _,_ => LLvl end. Instance lvl_valid : Valid lvl := λ _, True. Instance lvl_unit : Unit lvl := LLvl. Instance lvl_pcore : PCore lvl := λ _, Some LLvl. Lemma lvl_included lv1 lv2 : lv1 ≼ lv2 ↔ match lv2 with | ULvl => True | LLvl => if lv1 is LLvl then True else False end. Proof. split. - intros [[] ->%leibniz_equiv]; by destruct lv1. - exists lv2. by destruct lv1, lv2. Qed. Lemma lvl_idemp (lv : lvl) : lv ⋅ lv = lv. Proof. by destruct lv. Qed. Lemma lvl_ra_mixin : RAMixin lvl. Proof. apply ra_total_mixin; try by eauto. - solve_proper. - by intros [] [] []. - by intros [] []. - by intros []. - intros lv1 lv2 ?%lvl_included. apply lvl_included. destruct lv1, lv2; compute; firstorder. Qed. Canonical Structure lvlR : cmraT := discreteR lvl lvl_ra_mixin. Global Instance lvl_cmra_discrete : CmraDiscrete lvlR. Proof. apply discrete_cmra_discrete. Qed. Lemma lvl_ucmra_mixin : UcmraMixin lvl. Proof. split; try (apply _ || done). by intros []. Qed. Canonical Structure lvlUR : ucmraT := UcmraT lvl lvl_ucmra_mixin. (* Auth (Loc -> (Q * Level)) *) Definition cloc : Type := loc * nat. Instance cloc_eq_dec : EqDecision cloc | 0 := _. Instance cloc_countable : Countable cloc | 0 := _. Instance cloc_inhabited : Inhabited cloc | 0 := _. Definition locking_heapUR : ucmraT := gmapUR cloc (prodR (prodR fracR lvlUR) (agreeR valC)). (** The CMRA we need. *) Class locking_heapG (Σ : gFunctors) := LHeapG { lheap_inG :> inG Σ (authR locking_heapUR); lheap_name : gname }. Class locking_heapPreG (Σ : gFunctors) := { lheap_preG_inG :> inG Σ (authR locking_heapUR) }. Definition locking_heapΣ : gFunctors := #[GFunctor (authR locking_heapUR)]. Instance subG_heapPreG {Σ} : subG locking_heapΣ Σ → locking_heapPreG Σ. Proof. solve_inG. Qed. Section definitions. Context `{hG : locking_heapG Σ, !heapG Σ}. Definition to_locking_heap (σ : gmap cloc (lvl * val)) : locking_heapUR := fmap (λ '(lv,v), (1%Qp, lv, to_agree v)) σ. (* σ^{-1}(L) *) Definition locked_locs (σ : gmap cloc (lvl * val)) : gset cloc := dom _ (filter (λ x, x.2.1 = LLvl) σ). (** Pointer arithmetic *) Definition cloc_lt (p q : cloc) : bool := bool_decide (p.1 = q.1 ∧ p.2 < q.2). Definition cloc_add (cl : cloc) (i : nat) : cloc := (cl.1, cl.2 + i). Definition cloc_to_val (cl : cloc) : val := (#cl.1, #cl.2). Definition cloc_of_val (v : val) : option cloc := match v return option (loc * nat) with | (LitV (LitLoc l), LitV (LitInt i))%V => guard (0 ≤ i)%Z; Some (l, Z.to_nat i) | _ => None end. Definition full_locking_heap (σ : gmap cloc (lvl * val)) := (∃ τ : gmap loc (list (lvl * val)), ⌜ ∀ cl, σ !! cl = τ !! cl.1 ≫= lookup (M:=list _) cl.2 ⌝ ∧ own lheap_name (● (to_locking_heap σ)) ∗ [∗ map] l↦lvvs ∈ τ, ∃ lv, l ↦ SOMEV lv ∧ ⌜ is_list lv (snd <\$> lvvs) ⌝)%I. Definition mapsto_def (cl : cloc) (lv : lvl) (q : frac) (v: val) : iProp Σ := (∃ lv', ⌜lv ≼ lv'⌝ ∧ own lheap_name (◯ {[ cl := (q, lv', to_agree v) ]}))%I. Definition mapsto_aux : seal (@mapsto_def). by eexists. Qed. Definition mapsto := unseal mapsto_aux. Definition mapsto_eq : @mapsto = @mapsto_def := seal_eq mapsto_aux. End definitions. Notation "cl ↦C[ lv ]{ q } v" := (mapsto cl lv q%Qp v%V) (at level 20, lv, q at level 50, format "cl ↦C[ lv ]{ q } v") : bi_scope. Notation "cl ↦C[ lv ] v" := (cl ↦C[lv]{1} v)%I (at level 20, lv at level 50, format "cl ↦C[ lv ] v") : bi_scope. Notation "cl ↦C{ q } v" := (cl ↦C[ULvl]{q} v)%I (at level 20, q at level 50, format "cl ↦C{ q } v") : bi_scope. Notation "cl ↦C v" := (cl ↦C[ULvl]{1} v)%I (at level 20, format "cl ↦C v") : bi_scope. Notation "cl ↦C{ q }∗ vs" := ([∗ list] i ↦ v ∈ vs, cloc_add cl i ↦C{q} v)%I (at level 20, q at level 50, format "cl ↦C{ q }∗ vs") : bi_scope. Notation "cl ↦C∗ vs" := ([∗ list] i ↦ v ∈ vs, cloc_add cl i ↦C v)%I (at level 20, format "cl ↦C∗ vs") : bi_scope. Lemma to_locking_heap_valid (σ : gmap cloc (lvl * val)) : ✓ to_locking_heap σ. Proof. intros cl. rewrite lookup_fmap. by destruct (σ !! cl) as [[]|]. Qed. Lemma locking_heap_init `{locking_heapPreG Σ, !heapG Σ} : (|==> ∃ _ : locking_heapG Σ, full_locking_heap ∅)%I. Proof. iMod (own_alloc (● to_locking_heap ∅)) as (γ) "Hh". { apply: auth_auth_valid. exact: to_locking_heap_valid. } iModIntro. iExists (LHeapG Σ _ γ), ∅. auto. Qed. Section properties. Context `{hG : locking_heapG Σ, !heapG Σ}. Implicit Type σ : gmap cloc (lvl * val). Implicit Type lv : lvl. Implicit Type l : loc. Implicit Type i : nat. Implicit Type cl : cloc. Lemma mapsto_value_agree lv lv' cl q q' v v' : cl ↦C[lv]{q} v -∗ cl ↦C[lv']{q'} v' -∗ ⌜v = v'⌝. Proof. rewrite mapsto_eq /mapsto_def. iDestruct 1 as (lv1 ?) "Hl1". iDestruct 1 as (lv2 ?) "Hl2". iDestruct (own_valid_2 with "Hl1 Hl2") as %Ho%auth_own_valid. iPureIntro. revert Ho. rewrite /= op_singleton singleton_valid. by intros [_ ?%agree_op_invL']. Qed. Lemma mapsto_combine lv lv' cl q q' v : cl ↦C[lv]{q} v -∗ cl ↦C[lv']{q'} v -∗ cl ↦C[lv⋅lv']{q+q'} v. Proof. rewrite mapsto_eq /mapsto_def. iDestruct 1 as (lv1 ?) "Hl1". iDestruct 1 as (lv2 ?) "Hl2". iExists (lv1 ⋅ lv2). iSplitR. { iPureIntro. by apply: cmra_mono. } iCombine "Hl1 Hl2" as "Hl". rewrite frac_op'. by iFrame. Qed. Global Instance from_sep_mapsto cl lv lv' q q' v : FromSep (cl ↦C[lv⋅lv']{q+q'} v) (cl ↦C[lv]{q} v) (cl ↦C[lv']{q'} v). Proof. rewrite /FromSep. iIntros "[Hl1 Hl2]". iApply (mapsto_combine with "Hl1 Hl2"). Qed. Global Instance mapsto_timeless cl lv q v : Timeless (cl ↦C[lv]{q} v). Proof. rewrite mapsto_eq /mapsto_def. apply _. Qed. Global Instance mapsto_fractional cl lv v : Fractional (λ q, cl ↦C[lv]{q} v)%I. Proof. intros p q. iSplit. - rewrite mapsto_eq /mapsto_def. iDestruct 1 as (lv' ?) "Hl". rewrite -(lvl_idemp lv'). iDestruct "Hl" as "[Hl Hl']". iSplitL "Hl"; eauto 10. - iIntros "[H1 H2]". iDestruct (mapsto_combine with "H1 H2") as "H". by rewrite lvl_idemp. Qed. Global Instance mapsto_as_fractional cl q lv v : AsFractional (cl ↦C[lv]{q} v) (λ q, cl ↦C[lv]{q} v)%I q. Proof. split. done. apply _. Qed. Lemma mapsto_downgrade' lv lv' cl q v : lv ≼ lv' → cl ↦C[lv']{q} v -∗ cl ↦C[lv]{q} v. Proof. rewrite mapsto_eq /mapsto_def. iDestruct 1 as (lv'' ?) "Hl". iExists lv''. iSplit; eauto. iPureIntro. by transitivity lv'. Qed. Lemma mapsto_downgrade lv cl q v : cl ↦C{q} v -∗ cl ↦C[lv]{q} v. Proof. apply mapsto_downgrade'. by apply lvl_included. Qed. Lemma cloc_of_to_val cl : cloc_of_val (cloc_to_val cl) = Some cl. Proof. destruct cl. by rewrite /= option_guard_True ?Nat2Z.id; last lia. Qed. Lemma cloc_to_of_val v cl : cloc_of_val v = Some cl → cloc_to_val cl = v. Proof. rewrite /cloc_of_val /cloc_to_val=> ?. destruct cl; repeat (case_match || simplify_option_eq); auto. by rewrite Z2Nat.inj_pos positive_nat_Z. Qed. Lemma to_locking_heap_insert σ cl lv v : to_locking_heap (<[cl:=(lv,v)]> σ) = <[cl:=(1%Qp, lv, to_agree v)]>(to_locking_heap σ). Proof. by rewrite /to_locking_heap fmap_insert. Qed. Lemma to_locking_heap_lookup_Some σ li lv v : σ !! li = Some (lv,v) → to_locking_heap σ !! li = Some (1%Qp, lv, to_agree v). Proof. rewrite /to_locking_heap lookup_fmap => -> //. Qed. Lemma to_locking_heap_lookup_None σ li : σ !! li = None → to_locking_heap σ !! li = None. Proof. rewrite /to_locking_heap lookup_fmap => -> //. Qed. Lemma locked_locs_lock σ cl v : locked_locs (<[cl:=(LLvl,v)]>σ) = {[cl]} ∪ locked_locs σ. Proof. rewrite /locked_locs -map_filter_lookup_insert; last done. apply dom_insert_L. Qed. Lemma locked_locs_unlock σ cl v : σ !! cl = Some (LLvl,v) → locked_locs (<[cl:=(ULvl,v)]>σ) = locked_locs σ ∖ {[cl]}. Proof. intros Hl. rewrite /locked_locs -dom_delete_L. f_equal. apply map_eq=> j. apply option_eq=> x. rewrite lookup_delete_Some !map_filter_lookup_Some lookup_insert_Some. naive_solver. Qed. Lemma locked_locs_alloc_unlocked σ cl v : σ !! cl = None → locked_locs (<[cl:=(ULvl,v)]>σ) = locked_locs σ. Proof. intros Hl. rewrite /locked_locs. f_equal. apply map_eq => j. apply option_eq=> x. rewrite !map_filter_lookup_Some lookup_insert_Some. naive_solver. Qed. Lemma heap_singleton_included σ cl lv q v : {[cl := (q, lv, to_agree v)]} ≼ to_locking_heap σ → ∃ lv', lv ≼ lv' ∧ σ !! cl = Some (lv', v). Proof. rewrite singleton_included=> -[[[q' lv'] av] []]. rewrite /to_gen_heap lookup_fmap fmap_Some_equiv => -[[lv'' av'] [Hl [/= -> ->]]]. move=> /Some_pair_included_total_2 [/Some_pair_included_total_2] [_] Hxb'. move=> /to_agree_included /leibniz_equiv_iff=> ->. by exists lv''. Qed. Lemma locked_locs_unlocked σ cl v q : cl ↦C{q} v -∗ full_locking_heap σ -∗ ⌜cl ∉ locked_locs σ⌝. Proof. rewrite mapsto_eq /mapsto_def /full_locking_heap. iDestruct 1 as (lv ?%lvl_included) "Hl". iDestruct 1 as (τ Hτ) "[Hfull Hmap]". iDestruct (own_valid_2 with "Hfull Hl") as %[[lv' [?%lvl_included Hl]]%heap_singleton_included _]%auth_valid_discrete_2. assert (lv' = ULvl) as -> by (by destruct lv', lv). iPureIntro. rewrite /locked_locs. apply not_elem_of_dom, map_filter_lookup_None. right. intros [??]. by rewrite Hl=>[= <- <-]. Qed. Lemma full_locking_heap_unlocked σ cl v q : cl ↦C{q} v -∗ full_locking_heap σ -∗ ⌜σ !! cl = Some (ULvl,v)⌝. Proof. rewrite mapsto_eq /mapsto_def /full_locking_heap. iDestruct 1 as ([] []%lvl_included) "Hl". iDestruct 1 as (τ Hτ) "[Hfull Hmap]". iDestruct (own_valid_2 with "Hfull Hl") as %[[[] [[]%lvl_included Hl]]%heap_singleton_included _]%auth_valid_discrete_2; auto. Qed. Lemma full_locking_heap_present σ cl v q : cl ↦C[LLvl]{q} v -∗ full_locking_heap σ -∗ ⌜is_Some (σ !! cl)⌝. Proof. rewrite mapsto_eq /mapsto_def /full_locking_heap. iDestruct 1 as (lv _) "Hl". iDestruct 1 as (τ Hτ) "[Hfull Hmap]". iDestruct (own_valid_2 with "Hfull Hl") as %[[y [? ?]]%heap_singleton_included _]%auth_valid_discrete_2; eauto. Qed. Lemma locking_heap_load cl lv q v σ : full_locking_heap σ -∗ cl ↦C[lv]{q} v ==∗ ∃ ll vs, ⌜ is_list ll vs ⌝ ∧ ⌜ vs !! cl.2 = Some v ⌝ ∗ cl.1 ↦ SOMEV ll ∗ (cl.1 ↦ SOMEV ll -∗ full_locking_heap σ ∗ cl ↦C[lv]{q} v). Proof. iDestruct 1 as (τ Hτ) "[Hσ Hτ]". rewrite mapsto_eq /mapsto_def; iDestruct 1 as (lv' ?) "Hl". iDestruct (own_valid_2 with "Hσ Hl") as %[(lv''&?&Hσ)%heap_singleton_included _]%auth_valid_discrete_2. move: (Hσ); rewrite Hτ=> /bind_Some [lvvs [? Hi]]. iDestruct (big_sepM_lookup_acc with "Hτ") as "[H Hclose]"; first done. iDestruct "H" as (ll) "[Hll %]". iModIntro. iExists ll, lvvs.*2. repeat iSplit; auto. { iPureIntro. by rewrite list_lookup_fmap Hi. } iIntros "{\$Hll} Hll". iDestruct ("Hclose" with "[Hll]") as "Hτ"; eauto. iSplitL "Hσ Hτ"; first (iExists τ; by eauto with iFrame). iExists lv'. auto. Qed. Lemma locking_heap_store cl lv v σ : full_locking_heap σ -∗ cl ↦C[lv] v ==∗ ∃ ll vs, ⌜ is_list ll vs ⌝ ∧ ⌜ vs !! cl.2 = Some v ⌝ ∗ cl.1 ↦ SOMEV ll ∗ (∀ ll' lv' v', ⌜ is_list ll' (<[cl.2:=v']>vs) ⌝ -∗ cl.1 ↦ SOMEV ll' ==∗ full_locking_heap (<[cl:=(lv',v')]>σ) ∗ cl ↦C[lv'] v'). Proof. iDestruct 1 as (τ Hτ) "[Hσ Hτ]". rewrite mapsto_eq /mapsto_def; iDestruct 1 as (lv' ?) "Hl". iDestruct (own_valid_2 with "Hσ Hl") as %[(lv''&?&Hσ)%heap_singleton_included _]%auth_valid_discrete_2. move: (Hσ); rewrite Hτ=> /bind_Some [lvvs [Hτl Hi]]. iDestruct (big_sepM_delete with "Hτ") as "[H Hτ]"; first done. iDestruct "H" as (ll) "[Hll %]". iModIntro. iExists ll, lvvs.*2. repeat iSplit; auto. { iPureIntro. by rewrite list_lookup_fmap Hi. } iIntros "{\$Hll}" (ll' lv''' v' ?) "Hll". iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]". { by eapply auth_update, singleton_local_update, (exclusive_local_update _ (1%Qp, lv''', to_agree v')); first by apply to_locking_heap_lookup_Some. } iModIntro. iSplitL "Hσ Hτ Hll"; last auto. iExists (<[cl.1:=(<[cl.2:=(lv''',v')]> lvvs)]>τ). rewrite to_locking_heap_insert. iFrame "Hσ". iSplit. { destruct cl as [l i]; iPureIntro=> -[l' i']; simpl in *. destruct (decide (l' = l)) as [->|?]. { destruct (decide (i' = i)) as [->|?]. - rewrite !lookup_insert /= list_lookup_insert //. by eapply lookup_lt_Some. - rewrite lookup_insert /= list_lookup_insert_ne //. rewrite lookup_insert_ne; last congruence. by rewrite Hτ Hτl. } rewrite !lookup_insert_ne; [|congruence..]. by rewrite Hτ. } rewrite -insert_delete. iApply (big_sepM_insert with "[\$Hτ Hll]"); first by rewrite lookup_delete. iExists ll'. iFrame. by rewrite list_fmap_insert. Qed. Definition alloc_heap (σ : gmap cloc (lvl * val)) (l : loc) : list val → nat → gmap cloc (lvl * val) := foldr (λ v go i, <[(l,i):=(ULvl,v)]> (go (S i))) (λ _, σ). Lemma alloc_heap_None σ l vs j1 j2 : (∀ i, σ !! (l,i) = None) → j2 < j1 → alloc_heap σ l vs j1 !! (l, j2) = None. Proof. intros Hσi. revert j1 j2. induction vs as [|v' vs IH]=> j1 j2 ?; csimpl. { by rewrite Hσi. } rewrite lookup_insert_ne; last (intros [=]; lia). by rewrite IH; last lia. Qed. Lemma alloc_heap_lookup σ l vs i j : (∀ i, σ !! (l,i) = None) → alloc_heap σ l vs j !! (l, j + i) = ((ULvl,) <\$> vs) !! i. Proof. intros Hσi. revert i j. induction vs as [|v vs IH]=> i j; csimpl. { by rewrite Hσi. } destruct i as [|i]; simpl. { by rewrite Nat.add_0_r lookup_insert. } rewrite Nat.add_succ_r lookup_insert_ne; last (intros [=]; lia). apply (IH i (S j)). Qed. Lemma alloc_heap_lookup_ne σ l l' vs i j : l ≠ l' → alloc_heap σ l vs j !! (l', i) = σ !! (l', i). Proof. intros Hl. revert i j. induction vs as [|v vs IH]=> i j //; csimpl. by rewrite lookup_insert_ne; last congruence. Qed. Lemma locked_locs_alloc_heap σ l vs j : (∀ i, σ !! (l,i) = None) → locked_locs (alloc_heap σ l vs j) = locked_locs σ. Proof. intros ?. revert j. induction vs as [|v vs IH]=> j //=. rewrite locked_locs_alloc_unlocked // alloc_heap_None //; lia. Qed. Lemma locking_heap_alloc l ll vs σ : is_list ll vs → full_locking_heap σ -∗ l ↦ SOMEV ll ==∗ ⌜ ∀ i, σ !! (l,i) = None ⌝ ∧ full_locking_heap (alloc_heap σ l vs O) ∗ (l,0) ↦C∗ vs. Proof. intros Hll. iDestruct 1 as (τ Hτ) "[Hσ Hτ]". iIntros "Hll". set (f := foldr (λ v go i, <[(l,i):=(ULvl,v)]> (go (S i))) (λ _, σ)). iAssert ⌜ τ !! l = None ⌝%I as %Hτi. { rewrite eq_None_not_Some. iIntros ([lvv ?]). iDestruct (big_sepM_lookup with "Hτ") as (ll') "[Hll' _]"; first done. by iDestruct (mapsto_valid_2 with "Hll Hll'") as %[]. } iAssert ⌜ ∀ i, σ !! (l,i) = None ⌝%I as %Hσi. { iIntros (i). by rewrite Hτ Hτi. } iAssert (|==> own lheap_name (● to_locking_heap (f vs 0)) ∗ [∗ list] i↦v ∈ vs, own lheap_name (◯ {[ (l,0 + i) := (1%Qp, ULvl,to_agree v) ]}))%I with "[Hσ]" as ">[Hσ Hl]". { clear Hll. generalize 0=> j. iInduction vs as [|v vs] "IH" forall (j); simpl; first by iFrame. iMod ("IH" \$! (S j) with "Hσ") as "[Hσ Hls]". iMod (own_update with "Hσ") as "[Hσ Hl]". { eapply auth_update_alloc, (alloc_singleton_local_update _ (l,j) (1%Qp, ULvl, to_agree v)); try done. apply to_locking_heap_lookup_None. rewrite alloc_heap_None //. lia. } iModIntro. rewrite -to_locking_heap_insert Nat.add_0_r; iFrame "Hσ Hl". iApply (big_sepL_impl with "Hls"); iIntros "!>" (k w _) "?". by rewrite Nat.add_succ_r. } iModIntro. iSplit; first done. iSplitL "Hσ Hτ Hll". { iExists (<[l:=(ULvl,) <\$> vs]> τ). iFrame "Hσ". iSplit. - iPureIntro=> -[l' i] /=. destruct (decide (l' = l)) as [->|]. + rewrite lookup_insert /=. by apply (alloc_heap_lookup _ _ _ _ 0). + by rewrite lookup_insert_ne //= alloc_heap_lookup_ne // Hτ. - iApply (big_sepM_insert with "[\$Hτ Hll]"); first done. iExists _. iFrame "Hll". by rewrite -list_fmap_compose (list_fmap_ext _ id _ vs) ?list_fmap_id. } iApply (big_sepL_impl with "Hl"); iIntros "!>" (i v _) "Hl". rewrite mapsto_eq /mapsto_def. eauto. Qed. Lemma locking_heap_unlock cl v lv q σ : full_locking_heap σ -∗ cl ↦C[lv]{q} v ==∗ full_locking_heap (<[cl:=(ULvl,v)]>σ) ∗ cl ↦C{q} v. Proof. iDestruct 1 as (τ Hτ) "[Hσ Hτ]". rewrite mapsto_eq /mapsto_def; iDestruct 1 as (lv' ?) "Hl". iDestruct (own_valid_2 with "Hσ Hl") as %[(lv''&?&Hσ)%heap_singleton_included _]%auth_valid_discrete_2. move: (Hσ); rewrite Hτ=> /bind_Some [lvvs [Hτl Hi]]. iDestruct (big_sepM_delete with "Hτ") as "[H Hτ]"; first done. iDestruct "H" as (ll) "[Hll %]". iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]". { eapply auth_update, singleton_local_update, prod_local_update_1, prod_local_update_2, (local_update_unital_discrete _ _ ULvl ULvl); first by apply to_locking_heap_lookup_Some. intros h Hh. fold_leibniz. intros ->. split; eauto. } iModIntro. iSplitR "Hl"; last by eauto with iFrame. iExists (<[cl.1:=(<[cl.2:=(ULvl,v)]> lvvs)]>τ). rewrite to_locking_heap_insert. iFrame "Hσ". iSplit. { destruct cl as [l i]; iPureIntro=> -[l' i']; simpl in *. destruct (decide (l' = l)) as [->|?]. { destruct (decide (i' = i)) as [->|?]. - rewrite !lookup_insert /= list_lookup_insert //. by eapply lookup_lt_Some. - rewrite lookup_insert /= list_lookup_insert_ne //. rewrite lookup_insert_ne; last congruence. by rewrite Hτ Hτl. } rewrite !lookup_insert_ne; [|congruence..]. by rewrite Hτ. } rewrite -insert_delete. iApply (big_sepM_insert with "[\$Hτ Hll]"); first by rewrite lookup_delete. iExists ll. iFrame. by rewrite list_fmap_insert /= list_insert_id ?list_lookup_fmap ?Hi. Qed. End properties.