Commit 7b400617 authored by Ike Mulder's avatar Ike Mulder
Browse files

Using new hint notation in actris example.

parent 4ea80cea
Subproject commit 19cd2645fad66ec5f36c5d26844653a1dd588897
Subproject commit 03a7eae7923deac0a824eb524ce7692f20f1833b
......@@ -15,22 +15,19 @@ Section contribution_biabd.
Context `{contributionG Σ A}.
Global Instance deallocate_client γ i (x : A) :
BiAbd (TTl := [tele]) (TTr := [tele]) false (server γ (S i) x) (server γ i x) (bupd) (client γ (ε : A)) emp%I.
Proof.
rewrite /BiAbd /= right_id.
iIntros "[Hs Hc]".
by iMod (@dealloc_client with "Hs Hc") as "$".
HINT server γ (S i) x [- ; client γ (ε : A)] [bupd]; server γ i x [emp].
Proof.
iStepS.
by iMod (@dealloc_client with "H1 H2") as "$".
Qed.
Global Instance update_client_biabd γ i (x x' y y' : A) φ :
FindLocalUpdate x x' y y' φ
BiAbd (TTl := [tele]) (TTr := [tele]) false (server γ i x) (server γ i x') (bupd) (client γ y ⌜φ⌝)%I (client γ y') | 60.
HINT server γ i x [- ; client γ y ⌜φ⌝] [bupd]; server γ i x' [client γ y'] | 60.
(* should have precedence lower than assumption *)
Proof.
rewrite /FindLocalUpdate /BiAbd /= => Hφx.
iIntros "(Hs & Hc & %)".
specialize (Hφx H0).
by iMod (@update_client with "Hs Hc") as "[$ $]".
rewrite /FindLocalUpdate => Hφ. iStepS.
iMod (@update_client with "H1 H2") as "[$ $]"; eauto.
Qed.
Global Instance server_agree γ n (x y : A) P:
......@@ -57,11 +54,10 @@ Section contribution_biabd.
Qed.
Global Instance biabd_client_equiv γ (x y : A) p :
BiAbd (TTl := [tele]) (TTr := [tele]) p (client γ x) (client γ y) id (x y)%I emp%I.
HINT □⟨p client γ x [ - ; x y] [id]; client γ y [emp]. (* this is probably a bad instance *)
Proof.
rewrite /UcmraSubtract /CmraSubtract /BiAbd /= right_id bi.intuitionistically_if_elim.
iIntros "[Hγ Hxy]".
by iRewrite -"Hxy".
iStepS. rewrite bi.intuitionistically_if_elim.
rewrite H0. iStepsS.
Qed.
End contribution_biabd.
......@@ -203,11 +199,9 @@ Section actris_test.
Opaque start_chan par_map_service.
Global Instance llist_empty_biabd `(IC : C val iProp Σ) l xs : BiAbd (TTl := [tele]) (TTr := [tele]) false (l NONEV) (llist IC l xs) id xs = []%I xs = []%I.
Proof.
rewrite /BiAbd /=.
iStepsS.
Qed.
Global Instance llist_empty_biabd `(IC : C val iProp Σ) l xs :
HINT l NONEV [xs = []] [id]; llist IC l xs [xs = []].
Proof. iStepsS. Qed.
Global Instance par_map_client_spec2 n (vmap : val) (l : loc) xs :
SPEC {{ map_spec IA IB map vmap llist IA l xs 0 < n }}
......
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