Commit f7991ef5 authored by Ralf Jung's avatar Ralf Jung

fix nits

parent e9f37915
...@@ -76,7 +76,7 @@ Section coinflip. ...@@ -76,7 +76,7 @@ Section coinflip.
Proof using N. Proof using N.
iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam. iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.
wp_apply wp_new_proph; first done. wp_apply wp_new_proph; first done.
iIntros (p) "Hp". iDestruct "Hp" as (v) "Hp". iIntros (v p) "Hp".
wp_let. wp_let.
wp_bind (_ <- _)%E. wp_bind (_ <- _)%E.
iMod "AU" as "[Hl [_ Hclose]]". iMod "AU" as "[Hl [_ Hclose]]".
......
...@@ -289,7 +289,7 @@ Qed. ...@@ -289,7 +289,7 @@ Qed.
(** Lifting lemmas for creating and resolving prophecy variables *) (** Lifting lemmas for creating and resolving prophecy variables *)
Lemma wp_new_proph : Lemma wp_new_proph :
{{{ True }}} NewProph {{{ (p : proph), RET (LitV (LitProphecy p)); p - }}}. {{{ True }}} NewProph {{{ v (p : proph), RET (LitV (LitProphecy p)); p v }}}.
Proof. Proof.
iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR". iSplit. iIntros (σ1 κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR". iSplit.
...@@ -304,7 +304,7 @@ Proof. ...@@ -304,7 +304,7 @@ Proof.
iPureIntro. split. iPureIntro. split.
+ apply first_resolve_insert; auto. + apply first_resolve_insert; auto.
+ rewrite dom_insert_L. by apply union_mono_l. + rewrite dom_insert_L. by apply union_mono_l.
- iApply "HΦ". by iExists _. - iApply "HΦ". done.
Qed. Qed.
Lemma wp_resolve_proph e1 e2 p v w: Lemma wp_resolve_proph e1 e2 p v w:
...@@ -320,7 +320,7 @@ Proof. ...@@ -320,7 +320,7 @@ Proof.
unfold cons_obs. simpl. unfold cons_obs. simpl.
iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step. iApply fupd_frame_l. iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step. iApply fupd_frame_l.
iSplit=> //. iFrame. iSplit=> //. iFrame.
iMod ((@proph_map_remove _ _ _ _ _ _ _ p0) with "HR Hp") as "Hp". iModIntro. iMod (@proph_map_remove with "HR Hp") as "Hp". iModIntro.
iSplitR "HΦ". iSplitR "HΦ".
- iExists _. iFrame. iPureIntro. split; first by eapply first_resolve_delete. - iExists _. iFrame. iPureIntro. split; first by eapply first_resolve_delete.
rewrite dom_delete. rewrite <- difference_empty_L. by eapply difference_mono. rewrite dom_delete. rewrite <- difference_empty_L. by eapply difference_mono.
......
...@@ -20,7 +20,7 @@ Section first_resolve. ...@@ -20,7 +20,7 @@ Section first_resolve.
(map_of_list pvs : gmap P V) !! p. (map_of_list pvs : gmap P V) !! p.
Definition first_resolve_in_list R pvs := Definition first_resolve_in_list R pvs :=
forall p v, p dom (gset _) R p v, p dom (gset _) R
first_resolve pvs p = Some v first_resolve pvs p = Some v
R !! p = Some (Some v). R !! p = Some (Some v).
...@@ -156,13 +156,11 @@ Section proph_map. ...@@ -156,13 +156,11 @@ Section proph_map.
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 (?) "HR". rewrite /proph_map_ctx p_mapsto_eq /p_mapsto_def. iIntros (Hp) "HR". rewrite /proph_map_ctx p_mapsto_eq /p_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 _))))=> //.
apply lookup_to_proph_map_None. apply (iffLR (not_elem_of_dom _ _) H1). apply lookup_to_proph_map_None. apply (iffLR (not_elem_of_dom _ _) Hp). }
}
iModIntro. rewrite /proph_map_auth to_proph_map_insert. iFrame. iModIntro. rewrite /proph_map_auth to_proph_map_insert. iFrame.
Qed. Qed.
......
...@@ -103,6 +103,7 @@ Section language. ...@@ -103,6 +103,7 @@ Section language.
ρ2 = (t1 ++ e2 :: t2 ++ efs, σ2) ρ2 = (t1 ++ e2 :: t2 ++ efs, σ2)
prim_step e1 σ1 κ e2 σ2 efs prim_step e1 σ1 κ e2 σ2 efs
step ρ1 κ ρ2. step ρ1 κ ρ2.
Hint Constructors step.
(* TODO (MR) introduce notation ::? for cons_obs and suggest for inclusion to stdpp? *) (* TODO (MR) introduce notation ::? for cons_obs and suggest for inclusion to stdpp? *)
Definition cons_obs {A} (x : option A) (xs : list A) := Definition cons_obs {A} (x : option A) (xs : list A) :=
...@@ -115,10 +116,9 @@ Section language. ...@@ -115,10 +116,9 @@ Section language.
step ρ1 κ ρ2 step ρ1 κ ρ2
nsteps n ρ2 κs ρ3 nsteps n ρ2 κs ρ3
nsteps (S n) ρ1 (cons_obs κ κs) ρ3. nsteps (S n) ρ1 (cons_obs κ κs) ρ3.
Hint Constructors nsteps.
Definition erased_step (ρ1 ρ2 : cfg Λ) := exists κ, step ρ1 κ ρ2. Definition erased_step (ρ1 ρ2 : cfg Λ) := κ, step ρ1 κ ρ2.
Hint Constructors step nsteps.
Lemma erased_steps_nsteps ρ1 ρ2 : Lemma erased_steps_nsteps ρ1 ρ2 :
rtc erased_step ρ1 ρ2 rtc erased_step ρ1 ρ2
......
...@@ -134,8 +134,8 @@ Section lifting. ...@@ -134,8 +134,8 @@ Section lifting.
iDestruct "Hσκs" as "[Hσ Hκs]". iDestruct "Hσκs" as "[Hσ Hκs]".
rewrite /ownP_state /ownP_obs. rewrite /ownP_state /ownP_obs.
iMod (own_update_2 with "Hσ Hσf") as "[Hσ Hσf]". iMod (own_update_2 with "Hσ Hσf") as "[Hσ Hσf]".
{ apply auth_update. apply: option_local_update. { apply auth_update. apply: option_local_update.
by apply: (exclusive_local_update _ (Excl σ2)). } by apply: (exclusive_local_update _ (Excl σ2)). }
iMod (own_update_2 with "Hκs Hκsf") as "[Hκs Hκsf]". iMod (own_update_2 with "Hκs Hκsf") as "[Hκs Hκsf]".
{ apply auth_update. apply: option_local_update. { apply auth_update. apply: option_local_update.
by apply: (exclusive_local_update _ (Excl (κs'':leibnizC _))). } by apply: (exclusive_local_update _ (Excl (κs'':leibnizC _))). }
......
...@@ -58,7 +58,7 @@ Proof. ...@@ -58,7 +58,7 @@ Proof.
(* FIXME: reflexivity, as being called many times by f_equiv and f_contractive (* FIXME: reflexivity, as being called many times by f_equiv and f_contractive
is very slow here *) is very slow here *)
do 24 (f_contractive || f_equiv). apply IH; first lia. do 24 (f_contractive || f_equiv). apply IH; first lia.
intros v. eapply dist_le; eauto with omega. intros v. eapply dist_le; eauto with lia.
Qed. Qed.
Global Instance wp_proper s E e : Global Instance wp_proper s E e :
Proper (pointwise_relation _ () ==> ()) (wp (PROP:=iProp Σ) s E e). Proper (pointwise_relation _ () ==> ()) (wp (PROP:=iProp Σ) s E e).
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment