Commit b7c603f7 authored by Ike Mulder's avatar Ike Mulder
Browse files

Using new biabd/abduct notation in lib and comparison examples.

parent 7e31500e
......@@ -60,13 +60,13 @@ Section spec.
(l : loc), v = #l inv N (stack_inv P l)%I.
Global Instance biabd_islist_none xs P :
BiAbd (TTl := [tele]) (TTr := [tele]) false empty_hyp_first (is_list P xs NONEV) id xs = []%I xs = []%I.
Proof. rewrite /BiAbd /=. iStepsS. Qed.
HINT empty_hyp_first [xs = []] [id]; is_list P xs NONEV [xs = []].
Proof. iStepsS. Qed.
Global Instance biabd_islist_some P (l : loc) xs :
BiAbd (TTl := [tele_pair val; list val; val]) (TTr := [tele]) false empty_hyp_last (is_list P xs $ SOMEV #l)%I
id (λ x xs' t, l ↦□ x (l + 1) ↦□ t P x is_list P xs' t xs = x :: xs')%I (λ x xs' _, xs = x :: xs')%I.
Proof. rewrite /BiAbd /=. iStepsS. Qed.
HINT empty_hyp_last [x xs' t ; l ↦□ x (l + 1) ↦□ t P x is_list P xs' t xs = x :: xs']
[id]; is_list P xs (SOMEV #l) [xs = x :: xs'].
Proof. iStepsS. Qed.
Instance is_list_remember_skel P xs v :
MergablePersist (is_list P xs v) (λ p Pin Pout,
......@@ -78,11 +78,13 @@ Section spec.
Qed.
Global Instance biabd_islist_pop P l v E p :
BiAbd (TTl := [tele_pair val; list val]) (TTr := [tele_pair list val]) p ((l + 1) ↦□ v)%I (λ xs, is_list P xs v)%I
(fupd E E) (λ x xs', l ↦□ x is_list P xs' (SOMEV #l))%I (λ x xs' xs, val_is_unboxed v P x xs' = x :: xs)%I | 30.
HINT □⟨p
(l + 1) ↦□ v [x xs'; l ↦□ x is_list P xs' (SOMEV #l)]
[fupd E E] xs;
is_list P xs v [val_is_unboxed v P x xs' = x :: xs] | 30.
Proof.
rewrite /BiAbd /= => x xs'. rewrite bi.intuitionistically_if_elim.
iStepS. destruct xs'; iRevert "H3"; iStepsS.
iStepsS. rewrite bi.intuitionistically_if_elim.
destruct x0; iRevert "H3"; iStepsS.
Qed.
Global Instance match_list xs v e1 e2 :
......
......@@ -61,13 +61,12 @@ Section proof.
Definition is_list (v : val) : iProp Σ := (l : loc) (lk : val) γ, v = (#l, lk)%V is_lock γ lk ( z v, l v is_node z v).
Global Instance none_is_node z :
BiAbd (TTl := [tele]) (TTr := [tele]) false empty_hyp_first (is_node z NONEV) id emp%I emp%I.
Proof. rewrite /BiAbd /= is_node_unfold. iSmash. Qed.
HINT empty_hyp_first [emp] [id]; is_node z NONEV [emp].
Proof. iStepS. rewrite is_node_unfold. iSmash. Qed.
Global Instance some_is_node z (l : loc) lk :
BiAbd (TTl := [tele_pair gname]) (TTr := [tele]) false empty_hyp_last (is_node z $ SOMEV (#l, lk)%V) id
(λ γ, is_lock γ lk (lock_inv z l is_node)) (λ γ, emp%I).
Proof. rewrite /BiAbd /= => γ. rewrite is_node_unfold. iSmash. Qed.
HINT empty_hyp_last [γ; is_lock γ lk (lock_inv z l is_node)] [id]; is_node z (SOMEV (#l, lk)%V) [emp].
Proof. iStepsS. rewrite is_node_unfold. iSmash. Qed.
Global Instance match_node (nd : val) e1 e2 z :
SPEC [is_node z nd] {{ True }} Case nd e1 e2 {{ [^0] RET Case nd e1 e2; is_node_pre is_node z nd }} | 50.
......
......@@ -41,15 +41,15 @@ Section node.
Qed.
Global Instance is_node_from_unfold γm P l γ E :
BiAbd (TTl := [tele_pair val; dfrac]) (TTr := [tele]) false empty_hyp_last (is_node γm P l γ) (fupd E E)
(λ v q, (l + 1) {q} v (v = NONEV q = DfracOwn 1 own γ None (
(l2 : loc) v' γ', v = SOMEV #l2 (* we internalize the possible #q ~~> □ update *) l2 ↦□ v'
((P v' own γ' (Excl' l2)) own γ (Excl' l)) inv N (is_node γm P l2 γ') loc_map_elem γm l2 DfracDiscarded γ')))%I (λ v q, emp)%I.
(* we internalize the possible #q ~~> □ update *)
HINT empty_hyp_last [v q; (l + 1) {q} v (v = NONEV q = DfracOwn 1 own γ None (
(l2 : loc) v' γ', v = SOMEV #l2 l2 ↦□ v'
((P v' own γ' (Excl' l2)) own γ (Excl' l)) inv N (is_node γm P l2 γ') loc_map_elem γm l2 DfracDiscarded γ')) ]
[fupd E E]; is_node γm P l γ [emp].
Proof.
rewrite /BiAbd /= => v q.
iStepS; rewrite (is_node_unfold _ P l γ); try solve [iSmash].
* iAssert (|={E}=> (l + 1) ↦□ SOMEV #x)%I with "[H1]" as ">#Hl"; iSmash.
* iAssert (|={E}=> (l + 1) ↦□ SOMEV #x)%I with "[H1]" as ">#Hl"; iSmash.
iStepsS; rewrite (is_node_unfold _ P l γ); try solve [iSmash].
* iAssert (|={E}=> (l + 1) ↦□ SOMEV #x1)%I with "[H1]" as ">#Hl"; iSmash.
* iAssert (|={E}=> (l + 1) ↦□ SOMEV #x1)%I with "[H1]" as ">#Hl"; iSmash.
Qed.
Global Instance is_node_into_exist γm (P : val iProp Σ) (l : loc) γ :
......@@ -62,12 +62,13 @@ Section node.
Proof. rewrite /AtomIntoExist /IntoExistCareful /IntoExistCareful2 /= is_node_unfold //. Qed.
Global Instance queue_head_change (l l' : loc) p γ γ' γm E P :
BiAbd (TTl := [tele]) (TTr := [tele]) p ((l + 1) ↦□ SOMEV #l')%I ( own γ (Excl' l'))%I (fupd E E)
(own γ' (Excl' l) inv N (is_node γm P l γ') loc_map_elem γm l' DfracDiscarded γ ⌜↑N E)%I
( v, l' ↦□ v P v)%I.
HINT □⟨p
(l + 1) ↦□ SOMEV #l' [- ; own γ' (Excl' l) inv N (is_node γm P l γ') loc_map_elem γm l' DfracDiscarded γ ⌜↑N E]
[fupd E E];
( own γ (Excl' l')) [ v, l' ↦□ v P v].
Proof.
rewrite /BiAbd /= bi.intuitionistically_if_elim.
iStepS. iInv N as "HN".
iStepsS. rewrite bi.intuitionistically_if_elim.
iInv N as "HN".
iRevert "HN". rewrite {2 3}is_node_unfold.
iSmash.
Qed.
......@@ -79,8 +80,8 @@ Section node.
Global Instance allocate_any_loc l :
(* ideally the sidecondition would be a forall. but that is not sound: we must be able to know l now *)
BiAbd (TTl := [tele]) (TTr := [tele_pair gname]) false empty_hyp_last (λ γ, own γ None) bupd emp%I (λ γ, own γ (Excl' l))%I.
Proof. rewrite /BiAbd /=. iStepS. iAssert (|==> γ, own γ (Excl' l))%I as ">[%γ Hγ]"; iStepsS. Qed.
HINT empty_hyp_last [emp] [bupd] γ; own γ None [own γ $ Excl' l].
Proof. iStepS. iAssert (|==> γ, own γ (Excl' l))%I as ">[%γ Hγ]"; iStepsS. Qed.
End node.
......
......@@ -27,12 +27,12 @@ Section lock_increment.
Proof.
iStepsS.
iMod (own_alloc (F O F 0)) as (γ) "[Hγ Hγ']";
first by apply auth_both_valid.
first by apply auth_both_valid. iIntros "!>".
wp_apply (newlock_spec _ L ( m : nat, x0 #(m + s) own γ (F m)) with "[H2 Hγ]").
{ iStepsS.
by replace (Z.to_nat (s - s)) with 0 by lia. }
iStepsS.
iDestruct "Hγ'" as "[Hγ1 Hγ2]".
iDestruct "Hγ'" as "[Hγ1 Hγ2]". iIntros "!>".
wp_apply (wp_par (λ _, own γ (F{1/2} 1)) (λ _, own γ (F{1/2} 1)) with "[Hγ1] [Hγ2]");
iStepsS.
Qed.
......@@ -46,7 +46,7 @@ Section lock_increment.
Proposition parallel_add_fg_spec (s : nat) :
{{{ True }}} parallel_add_fg #s {{{ RET #(2%nat + s); True }}}.
Proof.
do 23 iStepS.
do 18 iStepS.
(* par will now say: i know the spec of FAA! we need to prevent that here *)
iMod (own_alloc (F O F 0)) as (γ) "[Hγ Hγ']";
first by apply auth_both_valid.
......@@ -55,7 +55,7 @@ Section lock_increment.
{ iStepsS.
replace (Z.to_nat (s - s)) with 0 by lia.
iStepsS. }
iDestruct "Hγ'" as "[Hγ1 Hγ2]".
iDestruct "Hγ'" as "[Hγ1 Hγ2]". iIntros "!>".
wp_apply (wp_par (λ _, own γ (F{1/2} 1)) (λ _, own γ (F{1/2} 1)) with "[Hγ1] [Hγ2]");
iStepsS.
Qed.
......@@ -67,9 +67,9 @@ Section lock_increment.
Proposition parallel_store_spec : {{{ True }}} parallel_store #() {{{ (n : Z), RET #n; True }}}.
Proof.
do 23 iStepS.
do 18 iStepS.
pose proof (nroot .@ "N") as N.
iMod (inv_alloc N _ ( n : Z, x0 #n) with "[H2]") as "#HN"; first iStepsS.
iMod (inv_alloc N _ ( n : Z, x0 #n) with "[H2]") as "#HN"; first iStepsS. iIntros "!>".
wp_apply (wp_par (λ _, True) (λ _, True))%I;
iStepsS.
Qed.
......@@ -79,8 +79,7 @@ Section lock_increment.
do 8 iStepS.
iMod (inv_alloc nroot _ (x0 #2 P) with "[H3 H1]") as "#HN". { iStepsS. }
iStepsS.
admit.
Admitted.
Abort.
End lock_increment.
......@@ -106,11 +105,11 @@ Section stateG_automation.
Context `{!stateG Σ, !invGS Σ}.
Global Instance biabd_start_finish p γ :
BiAbd (TTl := [tele]) (TTr := [tele]) p (own γ Start) (own γ Finish) (bupd) emp%I (own γ Finish).
Proof.
rewrite /BiAbd /= bi.intuitionistically_if_elim !right_id.
HINT □⟨p own γ Start [emp] [bupd]; own γ Finish [own γ Finish].
Proof.
iStepS. rewrite bi.intuitionistically_if_elim.
rewrite own_update; last by apply (cmra_update_exclusive Finish).
iStepS. (* TODO: iStepS does not solve this, due to the different sum_inr_subtract_n/s instances *)
(* TODO: iStepS does not solve this, due to the different sum_inr_subtract_n/s instances *)
iMod "H1" as "#H".
iStepsS.
Qed.
......@@ -177,7 +176,7 @@ Section exercises.
slow_incr_par #l
{{ (z : Z), RET #z; z = (n + 1)%Z z = (n + 2)%Z }}.
Proof.
do 9 iStepS.
do 8 iStepS.
(* allocation is manual since γ2 is not mentioned in the first case of invariant, and we have no CoAllocate instance *)
iMod (own_alloc Start) as (γ1) "Hγ1"; first done.
iMod (own_alloc 1%Qp) as (γ2) "Hγ2"; first done.
......
......@@ -76,8 +76,8 @@ Section problems.
*)
Section side_cond_problems.
Context `{!Inhabited A} {P Q R : A iProp Σ}.
Axiom example : (a : A), BiAbd (TTl := [tele]) (TTr := [tele]) false (P a) (Q a) id (R a) emp%I.
Local Existing Instance example.
Context (the_hint : (a : A), HINT P a [emp R a] [id]; Q a [emp]).
Local Existing Instance the_hint.
Lemma test :( ( a, P a) |==> a, R a)%I @{iPropI Σ} |==> a, Q a emp.
Proof. iStepsS. Qed.
......
......@@ -78,19 +78,17 @@ Section instances.
Global Instance mapsto_val_may_need_more (l : loc) (v1 v2 : val) (q1 q2 : Qp) mq q :
FracSub q2 q1 mq
TCEq mq (Some q)
BiAbd (TTl := [tele_pair val]) (TTr := [tele]) false (l {#q1} v1)%I (l {#q2} v2)%I id
(λ v', v1 = v2 l {#q} v')%I (λ v', v1 = v2 v' = v1)%I | 55.
HINT l {#q1} v1 [v'; v1 = v2 l {#q} v'] [id]; l {#q2} v2 [v1 = v2 v' = v1] | 55.
Proof.
rewrite /BiAbd /= /FracSub => <- -> v'.
rewrite /FracSub => <- -> v' /=.
iStepsS.
Qed.
Global Instance mapsto_val_have_enough (l : loc) (v1 v2 : val) (q1 q2 : Qp) mq :
FracSub q1 q2 mq
BiAbd (TTl := [tele]) (TTr := [tele]) false (l {#q1} v1)%I (l {#q2} v2)%I id v1 = v2%I
(v1 = v2 match mq with | Some q => l {#q} v1 | _ => True end)%I | 54.
HINT l {#q1} v1 [v1 = v2] [id]; l {#q2}v2 [v1 = v2 match mq with | Some q => l {#q} v1 | _ => True end] | 54.
Proof.
rewrite /BiAbd /= /FracSub => <-.
rewrite /= /FracSub => <-.
destruct mq; iStepsS.
iDestruct "H1" as "[H1 H1']".
iStepsS.
......@@ -111,10 +109,10 @@ Section instances.
Qed.
Global Instance as_persistent_mapsto p l q v :
BiAbd (TTl := [tele]) (TTr := [tele]) p (l {q} v)%I (l ↦□ v)%I (bupd) emp%I (l ↦□ v)%I | 100.
HINT □⟨p l {q} v [emp] [bupd]; l ↦□ v [l ↦□ v] | 100.
Proof.
rewrite /BiAbd /= right_id bi.intuitionistically_if_elim.
iIntros "Hl".
iIntros "Hl" => /=.
rewrite /= right_id bi.intuitionistically_if_elim.
iMod (mapsto_persist with "Hl") as "#Hl".
iStepsS.
Qed.
......@@ -123,10 +121,10 @@ Section instances.
Global Instance array_mapsto_head l v vs q l' :
OffsetLoc l 1 l' (* this makes us get (l +ₗ (1 + 1)) instead of ((l +ₗ 1) +ₗ 1) *)
BiAbd (TTl := [tele]) (TTr := [tele]) false (l ↦∗{q} vs)%I (l {q} v)%I id hd_error vs = Some v%I (l' ↦∗{q} tail vs hd_error vs = Some v%I)%I | 20.
HINT l ↦∗{q} vs [hd_error vs = Some v] [id]; l {q} v [l' ↦∗{q} tail vs hd_error vs = Some v] | 20.
Proof.
rewrite /BiAbd /= /OffsetLoc => ->.
iIntros "[H %]".
rewrite /= /OffsetLoc => ->.
iIntros "[H %] /=".
destruct vs => //.
iDestruct (array_cons with "H") as "[Hv Hl]"; iFrame.
case: H => ->. iStepsS.
......@@ -134,10 +132,10 @@ Section instances.
Global Instance head_mapsto_array l v vs q l' :
OffsetLoc l 1 l'
BiAbd (TTl := [tele]) (TTr := [tele]) false (l {q} v)%I (l {q} vs)%I id (hd_error vs = Some v (l' ↦∗{q} tail vs))%I emp%I | 20.
HINT l {q} v [hd_error vs = Some v l' ↦∗{q} tail vs] [id]; l ↦∗{q} vs [emp] | 20.
Proof.
rewrite /BiAbd /= => ->.
iIntros "(H & % & Htl)".
rewrite /= => ->.
iIntros "(H & % & Htl) /=".
destruct vs => //.
case: H => ->.
rewrite array_cons.
......@@ -147,10 +145,10 @@ Section instances.
Global Instance array_mapsto_head_offset l v vs q i l':
SolveSepSideCondition (0 i < length vs)%Z (* that this is_Some is given, but that it is equal to v is a proof obligation *)
OffsetLoc l (Z.succ i) l'
BiAbd (TTl := [tele]) (TTr := [tele]) false (l ↦∗{q} vs)%I ((l + i) {q} v)%I id vs !! Z.to_nat i = Some v%I
((l ↦∗{q} take (Z.to_nat i) vs) vs !! Z.to_nat i = Some v%I (l' ↦∗{q} drop (S $ Z.to_nat i) vs))%I | 20.
HINT l ↦∗{q} vs [vs !! Z.to_nat i = Some v] [id]; (l + i) {q} v [
(l ↦∗{q} take (Z.to_nat i) vs) vs !! Z.to_nat i = Some v (l' ↦∗{q} drop (S $ Z.to_nat i) vs)] | 20.
Proof.
rewrite /SolveSepSideCondition /BiAbd /= => Hi ->.
rewrite /SolveSepSideCondition /= => Hi ->.
iStepS.
rewrite -{1}(take_drop_middle _ _ _ H).
rewrite array_app array_cons; iRevert "H1"; iStepS.
......@@ -164,27 +162,27 @@ Section instances.
Global Instance array_from_shorter vs1 vs2 l l' q :
SolveSepSideCondition (length vs1 length vs2)
OffsetLoc l (length vs1) l'
BiAbd (TTl := [tele]) (TTr := [tele]) false (l ↦∗{q} vs1) (l ↦∗{q} vs2)%I id (take (length vs1) vs2 = vs1 (l' ↦∗{q} (list.drop (length vs1) vs2)))%I emp%I | 51.
HINT l ↦∗{q} vs1 [take (length vs1) vs2 = vs1 l' ↦∗{q} (list.drop (length vs1) vs2) ] [id];
l ↦∗{q} vs2 [emp] | 51.
Proof.
rewrite /SolveSepSideCondition /BiAbd => Hl -> /=.
rewrite /SolveSepSideCondition => Hl -> /=.
iStepS.
rewrite -{2}(take_drop (length vs1) vs2) H array_app.
iStepsS.
Qed.
Global Instance empty_array_solve l q :
BiAbd false empty_hyp_last (TTl := [tele]) (TTr := [tele]) (l ↦∗{q} [])%I id emp%I emp%I.
HINT empty_hyp_last [emp] [id]; l ↦∗{q} [] [emp].
Proof.
rewrite /BiAbd /=. rewrite array_nil. iStepsS.
iStepsS. rewrite array_nil. iStepsS.
Qed.
End biabds.
Section abds.
Global Instance fork_abduct e (Φ : val iPropI Σ) s E :
Abduct (TT := [tele]) false empty_hyp_last (wp s E (Fork e) Φ)%I id ( Φ #() WP e @ s; {{ _, True }})%I.
HINT1 empty_hyp_last [ Φ #() WP e @ s; {{ _, True }}] [id]; wp s E (Fork e) Φ.
Proof. (* eliding the type of Φ will give fork_abduct weird unsimplified (and ununifiable!) TeleO -t> T types *)
rewrite /Abduct /=. iStepsS.
iApply (wp_fork with "H2"). iStepsS.
iStepsS. iApply (wp_fork with "H2"). iStepsS.
Qed.
End abds.
......
......@@ -7,7 +7,6 @@ Import bi.
(* This file contains all base (bi)abduction hints, needed for minimal functionality of Diaframe.
*)
Set Universe Polymorphism.
Section biabd_instances.
......@@ -19,22 +18,21 @@ Section biabd_instances.
Global Instance bi_abd_from_assumption p P P' :
(* this requirement will remember newly proven persistent things *)
TCIf (TCAnd (TCEq p false) $ Persistent P) (TCEq P' P) (TCEq P' emp%I)
BiAbd (TTl := [tele]) (TTr := [tele]) p P P id emp%I P' | 50.
Proof.
HINT □⟨p P [emp] [id]; P [P'] | 50.
Proof.
rewrite /BiAbd /= !right_id //.
case => [[-> HP] -> | ->].
- rewrite intuitionistically_if_elim.
apply persistent_entails_r => //.
case => [[-> HP] -> /= | ->].
- apply persistent_entails_r => //.
- rewrite right_id.
apply intuitionistically_if_elim.
Qed.
Global Instance bi_abd_from_assumption_intuit P :
BiAbd (TTl := [tele]) (TTr := [tele]) true P ( P)%I id emp%I emp%I | 50.
HINT □⟨true P [emp] [id]; P [emp].
Proof. by rewrite /BiAbd /= !right_id. Qed.
Global Instance bi_abd_empty_goal_from_emp p :
BiAbd (TTl := [tele]) (TTr := [tele]) (PROP := PROP) p emp%I empty_goal id emp%I emp%I | 50.
HINT □⟨p emp [emp] [@id PROP]; empty_goal [emp] | 50.
Proof. by rewrite /BiAbd /= empty_goal_eq bi.intuitionistically_if_elim. Qed.
......@@ -69,8 +67,8 @@ Section biabd_instances.
Global Instance abd_if_bool_decide `{Decision φ} (L R : PROP) :
(* cannot be a biabd, since the forall would not be introducable! *)
Abduct (TT := [tele]) false empty_hyp_first (if bool_decide φ then L else R) id
( (b : bool), (b = true ⌜φ⌝ b = false ¬φ⌝ )- if b then L else R).
HINT1 empty_hyp_first [ (b : bool), (b = true ⌜φ⌝ b = false ¬φ⌝ )- if b then L else R]
[id]; if bool_decide φ then L else R.
Proof.
rewrite /Abduct /=.
case_bool_decide.
......@@ -81,6 +79,16 @@ Section biabd_instances.
iIntros "H".
iApply "H". by iRight.
Qed.
Global Instance biabd_emp_valid {TTl TTr} p P Q M R S :
AsEmpValid (BiAbd (TTl := TTl) (TTr := TTr) p P Q M R S) (.. (ttl : TTl), ?p P (tele_app R ttl) - M $ .. (ttr : TTr), tele_app Q ttr tele_app (tele_app S ttl) ttr).
Proof.
split.
- rewrite /BiAbd /= => /tforall_forall HPQ.
iIntros (ttl) "HPR". rewrite HPQ //.
- rewrite /BiAbd tforall_forall /= => HPQ ttl.
iApply HPQ.
Qed.
End biabd_instances.
Section abduction_instances.
......@@ -103,6 +111,14 @@ Section abduction_instances.
- by rewrite HS right_id.
- by apply sep_elim_l, _.
Qed.
Global Instance abduct_emp_valid {TT} p P Q M R :
AsEmpValid (Abduct (TT := TT) p P Q M R) (?p P R - M $ .. (tt : TT), tele_app Q tt)%I.
Proof.
split; rewrite /Abduct /=.
- move => -> //. iIntros "$".
- move => HPQ. iApply HPQ.
Qed.
End abduction_instances.
Unset Universe Polymorphism.
......
......@@ -95,59 +95,45 @@ Section automation.
Global Instance biabd_alloc_none q φ mq :
CmraSubtract 1%Qp q φ mq
BiAbd (TTl := [tele]) (TTr := [tele_pair gname]) false empty_hyp_last (λ γ, no_tokens P γ q) bupd ⌜φ⌝%I (λ γ, default emp (q' mq; Some $ no_tokens P γ q'))%I.
HINT empty_hyp_last [⌜φ⌝] [bupd] γ; no_tokens P γ q [default emp (q' mq; Some $ no_tokens P γ q')].
Proof. apply: tokenizable.biabd_alloc_none. Qed.
Global Instance biabd_alloc_some :
BiAbd (TTl := [tele]) (TTr := [tele_pair gname]) false empty_hyp_last (λ γ, token_counter P γ 1) bupd (P 1) (λ γ, token P γ)%I.
HINT empty_hyp_last [ - ; P 1] [bupd] γ; token_counter P γ 1 [token P γ].
Proof. apply: tokenizable.biabd_alloc_some. Qed.
Global Instance biabd_create_token γ p1 p2 :
SolveSepSideCondition (p2 = Pos.succ p1)
BiAbd (TTl := [tele]) (TTr := [tele]) false (token_counter P γ p1) (token_counter P γ p2) bupd emp%I (token P γ).
HINT token_counter P γ p1 [emp] [bupd]; token_counter P γ p2 [token P γ].
Proof. apply: tokenizable.biabd_create_token. Qed.
Global Instance biabd_create_first_token γ p :
SolveSepSideCondition (p = 1%positive)
BiAbd (TTl := [tele]) (TTr := [tele]) false (no_tokens P γ 1) (token_counter P γ p) bupd (P 1) (token P γ).
HINT no_tokens P γ 1 [- ; P 1] [bupd]; token_counter P γ p [token P γ].
Proof. apply: tokenizable.biabd_create_first_token. Qed.
Global Instance biabd_delete_token γ p1 p2 :
SolveSepSideCondition (1 < p1)%positive
SolveSepSideCondition (p2 = Pos.pred p1)
BiAbd (TTl := [tele]) (TTr := [tele]) false (token_counter P γ p1) (token_counter P γ p2) bupd (token P γ) emp%I.
HINT token_counter P γ p1 [- ; token P γ] [bupd]; token_counter P γ p2 [emp].
Proof. apply: tokenizable.biabd_delete_token. Qed.
Global Instance biabd_delete_last_token γ q mq φ p :
SolveSepSideCondition (p = 1)%positive
CmraSubtract 1%Qp q φ mq
BiAbd (TTl := [tele]) (TTr := [tele]) false (token_counter P γ p) (no_tokens P γ q) bupd (token P γ ⌜φ⌝)%I (P 1 default emp (q' mq; Some $ no_tokens P γ q'))%I.
HINT token_counter P γ p [- ; token P γ ⌜φ⌝] [bupd]; no_tokens P γ q [P 1 default emp (q' mq; Some $ no_tokens P γ q')].
Proof. apply: tokenizable.biabd_delete_last_token. Qed.
Global Instance biabd_delete_last_token_to_req γ p :
SolveSepSideCondition (p = 1%positive)
BiAbd (TTl := [tele]) (TTr := [tele]) false (token_counter P γ p) (P 1) bupd (token P γ) (no_tokens P γ 1).
HINT token_counter P γ p [- ; token P γ] [bupd]; P 1 [no_tokens P γ 1].
Proof. apply: tokenizable.biabd_delete_last_token_to_req. Qed.
Global Instance no_tokens_split γ q1 q2 mq :
FracSub q1 q2 mq
BiAbd (TTl := [tele]) (TTr := [tele]) false (no_tokens P γ q1) (no_tokens P γ q2) id True%I
(match mq with | Some q => no_tokens P γ q | None => True end)%I.
HINT no_tokens P γ q1 [True] [id]; no_tokens P γ q2 [match mq with | Some q => no_tokens P γ q | None => True end].
Proof. apply: tokenizable.no_tokens_split. Qed.
Global Instance token_access γ :
BiAbd (TTl := [tele]) (TTr := [tele_pair Qp]) false (token P γ) (λ q, P q) id True%I (λ q, (P q - token P γ))%I.
Proof.
rewrite /BiAbd /=.
iStepsS.
Qed.
Global Instance token_access2 γ :