Apply changes requested by @jung

parent 56f311a9
...@@ -67,6 +67,7 @@ theories/base_logic/lib/na_invariants.v ...@@ -67,6 +67,7 @@ theories/base_logic/lib/na_invariants.v
theories/base_logic/lib/cancelable_invariants.v theories/base_logic/lib/cancelable_invariants.v
theories/base_logic/lib/gen_heap.v theories/base_logic/lib/gen_heap.v
theories/base_logic/lib/fancy_updates_from_vs.v theories/base_logic/lib/fancy_updates_from_vs.v
theories/base_logic/lib/proph_map.v
theories/program_logic/adequacy.v theories/program_logic/adequacy.v
theories/program_logic/lifting.v theories/program_logic/lifting.v
theories/program_logic/weakestpre.v theories/program_logic/weakestpre.v
...@@ -89,7 +90,6 @@ theories/heap_lang/notation.v ...@@ -89,7 +90,6 @@ theories/heap_lang/notation.v
theories/heap_lang/proofmode.v theories/heap_lang/proofmode.v
theories/heap_lang/adequacy.v theories/heap_lang/adequacy.v
theories/heap_lang/total_adequacy.v theories/heap_lang/total_adequacy.v
theories/heap_lang/proph_map.v
theories/heap_lang/lib/spawn.v theories/heap_lang/lib/spawn.v
theories/heap_lang/lib/par.v theories/heap_lang/lib/par.v
theories/heap_lang/lib/assert.v theories/heap_lang/lib/assert.v
......
...@@ -37,18 +37,18 @@ Section definitions. ...@@ -37,18 +37,18 @@ Section definitions.
Implicit Types p : P. Implicit Types p : P.
(** The list of resolves for [p] in [pvs]. *) (** The list of resolves for [p] in [pvs]. *)
Fixpoint list_resolves pvs p : list V := Fixpoint proph_list_resolves pvs p : list V :=
match pvs with match pvs with
| [] => [] | [] => []
| (q,v)::pvs => if decide (p = q) then v :: list_resolves pvs p | (q,v)::pvs => if decide (p = q) then v :: proph_list_resolves pvs p
else list_resolves pvs p else proph_list_resolves pvs p
end. end.
Definition resolves_in_list R pvs := Definition proph_resolves_in_list R pvs :=
map_Forall (λ p vs, vs = list_resolves pvs p) R. map_Forall (λ p vs, vs = proph_list_resolves pvs p) R.
Definition proph_map_ctx pvs (ps : gset P) : iProp Σ := Definition proph_map_ctx pvs (ps : gset P) : iProp Σ :=
( R, resolves_in_list R pvs ( R, proph_resolves_in_list R pvs
dom (gset _) R ps dom (gset _) R ps
own (proph_map_name pG) ( (to_proph_map R)))%I. own (proph_map_name pG) ( (to_proph_map R)))%I.
...@@ -67,9 +67,9 @@ Section list_resolves. ...@@ -67,9 +67,9 @@ Section list_resolves.
Implicit Type R : proph_map P V. Implicit Type R : proph_map P V.
Lemma resolves_insert pvs p R : Lemma resolves_insert pvs p R :
resolves_in_list R pvs proph_resolves_in_list R pvs
p dom (gset _) R p dom (gset _) R
resolves_in_list (<[p := list_resolves pvs p]> R) pvs. proph_resolves_in_list (<[p := proph_list_resolves pvs p]> R) pvs.
Proof. Proof.
intros Hinlist Hp q vs HEq. intros Hinlist Hp q vs HEq.
destruct (decide (p = q)) as [->|NEq]. destruct (decide (p = q)) as [->|NEq].
...@@ -107,7 +107,7 @@ Section to_proph_map. ...@@ -107,7 +107,7 @@ Section to_proph_map.
Qed. Qed.
End to_proph_map. End to_proph_map.
Lemma proph_map_init `{proph_mapPreG P V PVS} pvs ps : Lemma proph_map_init `{Countable P, !proph_mapPreG P V PVS} pvs ps :
(|==> _ : proph_mapG P V PVS, proph_map_ctx pvs ps)%I. (|==> _ : proph_mapG P V PVS, proph_map_ctx pvs ps)%I.
Proof. Proof.
iMod (own_alloc ( to_proph_map )) as (γ) "Hh". iMod (own_alloc ( to_proph_map )) as (γ) "Hh".
...@@ -131,7 +131,7 @@ Section proph_map. ...@@ -131,7 +131,7 @@ Section proph_map.
Lemma proph_map_new_proph p ps pvs : Lemma proph_map_new_proph p ps pvs :
p ps p ps
proph_map_ctx pvs ps == proph_map_ctx pvs ps ==
proph_map_ctx pvs ({[p]} ps) proph p (list_resolves pvs p). proph_map_ctx pvs ({[p]} ps) proph p (proph_list_resolves pvs p).
Proof. Proof.
iIntros (Hp) "HR". iDestruct "HR" as (R) "[[% %] H●]". iIntros (Hp) "HR". iDestruct "HR" as (R) "[[% %] H●]".
rewrite proph_eq /proph_def. rewrite proph_eq /proph_def.
...@@ -141,7 +141,7 @@ Section proph_map. ...@@ -141,7 +141,7 @@ Section proph_map.
apply (not_elem_of_dom (D:=gset P)). set_solver. apply (not_elem_of_dom (D:=gset P)). set_solver.
} }
iModIntro. iFrame. iModIntro. iFrame.
iExists (<[p := list_resolves pvs p]> R). iSplitR "H●". iExists (<[p := proph_list_resolves pvs p]> R). iSplitR "H●".
- iPureIntro. split. - iPureIntro. split.
+ apply resolves_insert; first done. set_solver. + apply resolves_insert; first done. set_solver.
+ rewrite dom_insert. set_solver. + rewrite dom_insert. set_solver.
...@@ -155,16 +155,16 @@ Section proph_map. ...@@ -155,16 +155,16 @@ Section proph_map.
iIntros "[HR Hp]". iDestruct "HR" as (R) "[HP H●]". iDestruct "HP" as %[Hres Hdom]. iIntros "[HR Hp]". iDestruct "HR" as (R) "[HP H●]". iDestruct "HP" as %[Hres Hdom].
rewrite /proph_map_ctx proph_eq /proph_def. rewrite /proph_map_ctx proph_eq /proph_def.
iDestruct (own_valid_2 with "H● Hp") as %[HR%proph_map_singleton_included _]%auth_valid_discrete_2. iDestruct (own_valid_2 with "H● Hp") as %[HR%proph_map_singleton_included _]%auth_valid_discrete_2.
assert (vs = v :: list_resolves pvs p) as ->. { assert (vs = v :: proph_list_resolves pvs p) as ->. {
rewrite (Hres p vs HR). simpl. rewrite decide_True; done. rewrite (Hres p vs HR). simpl. rewrite decide_True; done.
} }
iMod (own_update_2 with "H● Hp") as "[H● H◯]". { iMod (own_update_2 with "H● Hp") as "[H● H◯]". {
eapply auth_update. apply: singleton_local_update. eapply auth_update. apply: singleton_local_update.
- unfold to_proph_map. rewrite lookup_fmap. rewrite HR. done. - unfold to_proph_map. rewrite lookup_fmap. rewrite HR. done.
- apply (exclusive_local_update _ (Excl (list_resolves pvs p : list (leibnizC V)))). done. - apply (exclusive_local_update _ (Excl (proph_list_resolves pvs p : list (leibnizC V)))). done.
} }
unfold to_proph_map. rewrite -fmap_insert. unfold to_proph_map. rewrite -fmap_insert.
iModIntro. iExists (list_resolves pvs p). iFrame. iSplitR. iModIntro. iExists (proph_list_resolves pvs p). iFrame. iSplitR.
- iPureIntro. done. - iPureIntro. done.
- iExists _. iFrame. iPureIntro. split. - iExists _. iFrame. iPureIntro. split.
+ intros q ws HEq. destruct (decide (p = q)) as [<-|NEq]. + intros q ws HEq. destruct (decide (p = q)) as [<-|NEq].
......
From iris.program_logic Require Export weakestpre adequacy. From iris.program_logic Require Export weakestpre adequacy.
From iris.algebra Require Import auth. From iris.algebra Require Import auth.
From iris.heap_lang Require Import proofmode notation proph_map. From iris.heap_lang Require Import proofmode notation.
From iris.base_logic.lib Require Import proph_map.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
Set Default Proof Using "Type". Set Default Proof Using "Type".
......
From iris.algebra Require Import auth gmap. From iris.algebra Require Import auth gmap.
From iris.base_logic Require Export gen_heap. From iris.base_logic Require Export gen_heap.
From iris.base_logic.lib Require Export proph_map.
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting total_ectx_lifting. From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
From iris.heap_lang Require Export lang proph_map. From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import tactics. From iris.heap_lang Require Import tactics.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From stdpp Require Import fin_maps. From stdpp Require Import fin_maps.
......
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