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

Updated arc examples to use new hint notation, fixed remaining places without notation.

parent ce5ff095
Pipeline #64003 passed with stage
in 8 minutes and 41 seconds
......@@ -47,13 +47,14 @@ 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_part P xs v :
MergablePersist (is_list P xs v) (λ p Pin Pout,
......@@ -65,11 +66,12 @@ 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.
Obligation Tactic := verify_tac.
......
......@@ -145,11 +145,12 @@ Section instances.
ProtoNormalize false p [] (<?> m)
MsgTele2 m tv tP tp
(.. x, MaybeIntoLaterN false 1 (tele_app tP x) (tele_app tP' x))
BiAbd (TTl := [tele]) (TTr := [tele]) false (c p) (c <?.. x> MSG (tele_app tv) x {{ (tele_app tP' x) }}; tele_app (TT:= TT) tp x) id emp%I emp%I.
HINT c p [- ; emp] [id];
c <?.. x> MSG (tele_app tv) x {{ (tele_app tP' x) }}; tele_app (TT:= TT) tp x [emp].
Proof.
rewrite /ProtoNormalize /MsgTele2 /MaybeIntoLaterN /BiAbd /= !right_id
=> Hpm Hm HtP.
iIntros "Hc". iApply (iProto_mapsto_le with "Hc"). iIntros "!>".
rewrite /ProtoNormalize /MsgTele2 /MaybeIntoLaterN /= => Hpm Hm HtP.
iIntros "[Hc _]" => /=. rewrite right_id in Hpm. rewrite right_id.
iApply (iProto_mapsto_le with "Hc"). iIntros "!>".
iApply iProto_le_trans; [iApply Hpm|rewrite Hm].
iApply iProto_le_texist_elim_l; iIntros (x).
iApply iProto_le_trans; [|iApply (iProto_le_texist_intro_r _ x)]; simpl.
......
......@@ -157,11 +157,12 @@ Section specs.
Instance get_weak_tok γ γp l E n :
SolveSepSideCondition (n = 0) (* only relevant when n = 0; if > 0, we get it for free from CmraSubtract *)
BiAbd (TTl := [tele]) (TTr := [tele]) false (own γ ( (Some (Cinr $ Excl ()), n))) (weak_tok γ) (fupd E E)
(is_arc' γ γp l P2 ⌜↑N E)%I emp%I | 60. (* after assumption! *)
HINT own γ ( (Some (Cinr $ Excl ()), n)) [- ; is_arc' γ γp l P2 ⌜↑N E]
[fupd E E];
weak_tok γ [emp] | 60. (* after assumption! *)
Proof.
rewrite /SolveSepSideCondition /BiAbd /= => ->.
iStepsS. iInv N as "HN"; iRevert "HN"; iSmash.
move => ->. iStepsS.
iInv N as "HN"; iRevert "HN"; iSmash.
Qed.
Instance drop_arc_spec (γ γp : gname) (l : loc) :
......
......@@ -103,11 +103,8 @@ Section instances.
Section biabds.
Global Instance mapsto_biabd l (z1 z2 : Z) q p :
BiAbd (TTl := [tele]) (TTr := [tele]) p (l {q} #z1)%I (l {q} #z2)%I id z1 = z2%I z1 = z2%I | 51.
Proof.
rewrite /BiAbd /= bi.intuitionistically_if_elim.
iStepsS.
Qed.
HINT □⟨p l {q} #z1 [z1 = z2] [id]; l {q} #z2 [z1 = z2] | 51.
Proof. iStepsS. rewrite bi.intuitionistically_if_elim. iStepsS. Qed.
End biabds.
......
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