Commit d500365d authored by Ralf Jung's avatar Ralf Jung
Browse files

fix build for real

parent dbb9afdc
Pipeline #75099 passed with stage
in 19 minutes and 42 seconds
......@@ -453,7 +453,7 @@ Section data_race.
apply: safe_reach_safe_implies => ?.
apply: safe_reach_refl. apply: post_in_ectx_intro. naive_solver.
}
iIntros (q v_t v_s) "Hl_t Hl_s #Hv Hc".
iIntros (q v_t v_s) "{Hv} Hl_t Hl_s #Hv Hc".
iDestruct (heap_mapsto_ne with "Hlr_s Hl_s") as %Hne2.
source_load. sim_pures. source_load. sim_pures.
source_bind (_ + _)%E. iApply source_red_safe_implies.
......
......@@ -183,7 +183,8 @@ Qed.
*)
Definition csim_expr_all π (P: list (expr Λ * expr Λ)) := ([ list] ip P, csim_expr (lift_post (ext_rel (π + i))) (π + i) (fst p) (snd p))%I.
Definition csim_expr_all π (P: list (expr Λ * expr Λ)) :=
([ list] i(p:_*_) P, csim_expr (lift_post (ext_rel (π + i))) (π + i) (fst p) (snd p))%I.
Notation must_step_all π := (must_step (csim_expr_all π)).
......@@ -251,7 +252,7 @@ Proof.
Qed.
Definition csim_expr_all_wo π P O :=
([ list] k p P, if (decide (k O)) then emp else csim_expr (lift_post (ext_rel (π + k))) (π + k) (fst p) (snd p))%I.
([ list] k (p:_*_) P, if (decide (k O)) then emp else csim_expr (lift_post (ext_rel (π + k))) (π + k) (fst p) (snd p))%I.
Lemma csim_expr_all_to_wo P π:
csim_expr_all π P csim_expr_all_wo π P .
......
......@@ -9,7 +9,6 @@ From iris.prelude Require Import options.
Lemma wf_init_state : state_wf init_state.
Proof.
constructor; simpl; try (intros ?; set_solver).
intros c Hc%elem_of_singleton_1. lia.
Qed.
(** Steps preserve wellformedness *)
......
......@@ -610,7 +610,7 @@ Section lemmas.
Proof. unseal. apply _. Qed.
Local Lemma tkmap_elems_unseal γ m :
([ map] k v' m, k [γ]{v'.1} v'.2) ==
([ map] k (v':_*_) m, k [γ]{v'.1} v'.2) ==
own γ ([^op map] kv' m, tkmap_view_frag (V:=leibnizO V) k v'.1 v'.2).
Proof.
unseal. destruct (decide (m = )) as [->|Hne].
......@@ -654,7 +654,7 @@ Section lemmas.
(** * Lemmas about [tkmap_auth] *)
Lemma tkmap_alloc_strong P m :
pred_infinite P
|==> γ, P γ⌝ tkmap_auth γ 1 m [ map] k v' m, k [γ]{v'.1} v'.2.
|==> γ, P γ⌝ tkmap_auth γ 1 m [ map] k (v':_*_) m, k [γ]{v'.1} v'.2.
Proof.
unseal. intros.
iMod (own_alloc_strong (tkmap_view_auth (V:=leibnizO V) 1 ) P)
......@@ -673,7 +673,7 @@ Section lemmas.
intros. iMod (tkmap_alloc_strong P ) as (γ) "(% & Hauth & _)"; eauto.
Qed.
Lemma tkmap_alloc m :
|==> γ, tkmap_auth γ 1 m [ map] k v' m, k [γ]{v'.1} v'.2.
|==> γ, tkmap_auth γ 1 m [ map] k (v':_*_) m, k [γ]{v'.1} v'.2.
Proof.
iMod (tkmap_alloc_strong (λ _, True) m) as (γ) "[_ Hmap]".
- by apply pred_infinite_True.
......@@ -764,7 +764,7 @@ Section lemmas.
(** Big-op versions of above lemmas *)
Lemma tkmap_lookup_big {γ q m} m0 :
tkmap_auth γ q m -
([ map] kv' m0, k [γ]{v'.1} v'.2) -
([ map] k(v':_*_) m0, k [γ]{v'.1} v'.2) -
m0 m.
Proof.
iIntros "Hauth Hfrag". rewrite map_subseteq_spec. iIntros (k [] Hm0).
......@@ -776,7 +776,7 @@ Section lemmas.
Lemma tkmap_insert_big {γ m} m' :
m' ## m
tkmap_auth γ 1 m ==
tkmap_auth γ 1 (m' m) ([ map] k v' m', k [γ]{v'.1} v'.2).
tkmap_auth γ 1 (m' m) ([ map] k (v':_*_) m', k [γ]{v'.1} v'.2).
Proof.
unseal. intros ?. rewrite -big_opM_own_1 -own_op.
apply own_update. apply: tkmap_view_alloc_big; done.
......
Supports Markdown
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