Commit cc712c90 by Ralf Jung

### more nits

parent 25ed5c9c
 ... @@ -52,8 +52,8 @@ Section coinflip. ... @@ -52,8 +52,8 @@ Section coinflip. <<< ∃ (b: bool), x ↦ #0, RET #b >>>. <<< ∃ (b: bool), x ↦ #0, RET #b >>>. Proof. Proof. iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam. iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam. wp_bind (rand _)%E. iApply rand_spec; first done. wp_apply rand_spec; first done. iIntros (b) "!> _". wp_let. iIntros (b) "_". wp_let. wp_bind (_ <- _)%E. wp_bind (_ <- _)%E. iMod "AU" as "[Hl [_ Hclose]]". iMod "AU" as "[Hl [_ Hclose]]". iDestruct "Hl" as (v) "Hl". iDestruct "Hl" as (v) "Hl". ... ...
 ... @@ -29,7 +29,7 @@ Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I ... @@ -29,7 +29,7 @@ Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I (at level 20, q at level 50, format "l ↦{ q } -") : bi_scope. (at level 20, q at level 50, format "l ↦{ q } -") : bi_scope. Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : bi_scope. Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : bi_scope. Notation "p ⥱ v" := (p_mapsto p v) (at level 20, format "p ⥱ v") : bi_scope. Notation "p ⥱ v" := (proph_mapsto p v) (at level 20, format "p ⥱ v") : bi_scope. Notation "p ⥱ -" := (∃ v, p ⥱ v)%I (at level 20) : bi_scope. Notation "p ⥱ -" := (∃ v, p ⥱ v)%I (at level 20) : bi_scope. (** The tactic [inv_head_step] performs inversion on hypotheses of the shape (** The tactic [inv_head_step] performs inversion on hypotheses of the shape ... ...
 ... @@ -89,15 +89,16 @@ Section definitions. ... @@ -89,15 +89,16 @@ Section definitions. dom (gset _) R ⊆ ps⌝ ∗ dom (gset _) R ⊆ ps⌝ ∗ proph_map_auth R)%I. proph_map_auth R)%I. Definition p_mapsto_def (p : P) (v: option V) : iProp Σ := Definition proph_mapsto_def (p : P) (v: option V) : iProp Σ := own (proph_map_name pG) (◯ {[ p := Excl (v : option \$ leibnizC V) ]}). own (proph_map_name pG) (◯ {[ p := Excl (v : option \$ leibnizC V) ]}). Definition p_mapsto_aux : seal (@p_mapsto_def). by eexists. Qed. Definition proph_mapsto_aux : seal (@proph_mapsto_def). by eexists. Qed. Definition p_mapsto := p_mapsto_aux.(unseal). Definition proph_mapsto := proph_mapsto_aux.(unseal). Definition p_mapsto_eq : @p_mapsto = @p_mapsto_def := p_mapsto_aux.(seal_eq). Definition proph_mapsto_eq : @proph_mapsto = @proph_mapsto_def := proph_mapsto_aux.(seal_eq). End definitions. End definitions. Local Notation "p ⥱ v" := (p_mapsto p v) (at level 20, format "p ⥱ v") : bi_scope. Local Notation "p ⥱ v" := (proph_mapsto p v) (at level 20, format "p ⥱ v") : bi_scope. Local Notation "p ⥱ -" := (∃ v, p ⥱ v)%I (at level 20) : bi_scope. Local Notation "p ⥱ -" := (∃ v, p ⥱ v)%I (at level 20) : bi_scope. Section to_proph_map. Section to_proph_map. ... @@ -148,13 +149,13 @@ Section proph_map. ... @@ -148,13 +149,13 @@ Section proph_map. (** General properties of mapsto *) (** General properties of mapsto *) Global Instance p_mapsto_timeless p v : Timeless (p ⥱ v). Global Instance p_mapsto_timeless p v : Timeless (p ⥱ v). Proof. rewrite p_mapsto_eq /p_mapsto_def. apply _. Qed. Proof. rewrite proph_mapsto_eq /proph_mapsto_def. apply _. Qed. Lemma proph_map_alloc R p v : Lemma proph_map_alloc R p v : p ∉ dom (gset _) R → p ∉ dom (gset _) R → proph_map_auth R ==∗ proph_map_auth (<[p := v]> R) ∗ p ⥱ v. proph_map_auth R ==∗ proph_map_auth (<[p := v]> R) ∗ p ⥱ v. Proof. Proof. iIntros (Hp) "HR". rewrite /proph_map_ctx p_mapsto_eq /p_mapsto_def. iIntros (Hp) "HR". rewrite /proph_map_ctx proph_mapsto_eq /proph_mapsto_def. iMod (own_update with "HR") as "[HR Hl]". iMod (own_update with "HR") as "[HR Hl]". { eapply auth_update_alloc, { eapply auth_update_alloc, (alloc_singleton_local_update _ _ (Excl \$ (v : option (leibnizC _))))=> //. (alloc_singleton_local_update _ _ (Excl \$ (v : option (leibnizC _))))=> //. ... @@ -165,14 +166,14 @@ Section proph_map. ... @@ -165,14 +166,14 @@ Section proph_map. Lemma proph_map_remove R p v : Lemma proph_map_remove R p v : proph_map_auth R -∗ p ⥱ v ==∗ proph_map_auth (delete p R). proph_map_auth R -∗ p ⥱ v ==∗ proph_map_auth (delete p R). Proof. Proof. iIntros "HR Hp". rewrite /proph_map_ctx p_mapsto_eq /p_mapsto_def. iIntros "HR Hp". rewrite /proph_map_ctx proph_mapsto_eq /proph_mapsto_def. rewrite /proph_map_auth to_proph_map_delete. iApply (own_update_2 with "HR Hp"). rewrite /proph_map_auth to_proph_map_delete. iApply (own_update_2 with "HR Hp"). apply auth_update_dealloc, (delete_singleton_local_update _ _ _). apply auth_update_dealloc, (delete_singleton_local_update _ _ _). Qed. Qed. Lemma proph_map_valid R p v : proph_map_auth R -∗ p ⥱ v -∗ ⌜R !! p = Some v⌝. Lemma proph_map_valid R p v : proph_map_auth R -∗ p ⥱ v -∗ ⌜R !! p = Some v⌝. Proof. Proof. iIntros "HR Hp". rewrite /proph_map_ctx p_mapsto_eq /p_mapsto_def. iIntros "HR Hp". rewrite /proph_map_ctx proph_mapsto_eq /proph_mapsto_def. iDestruct (own_valid_2 with "HR Hp") iDestruct (own_valid_2 with "HR Hp") as %[HH%proph_map_singleton_included _]%auth_valid_discrete_2; auto. as %[HH%proph_map_singleton_included _]%auth_valid_discrete_2; auto. Qed. Qed. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!