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

Made irisexamples working again (only on 8.15), and now using new hint notation there.

Also prevented losing □  modality in some cases.
parent f1564b05
......@@ -24,38 +24,33 @@ Proof. solve_inG. Qed.
Section barrier_biabds.
Context `{!invGS Σ, !barrierG Σ}.
Global Instance gset_dealloc_biabd2 p (X : gset gname) γ E :
BiAbd (PROP := iPropI Σ) p (TTl := [tele_pair bool; gset gname]) (TTr := [tele_pair (gset gname)])
(own γ $ GSet X) (λ gs, own γ $ GSet gs)
(fupd E E) (λ b Y, b = true own γ $ GSet Y b = false Y = ∅⌝)%I
(λ b Y gs, b = true gs = X Y b = false gs = X)%I. (* | 0.*)
Global Instance gset_dealloc_biabd2 p (X : gset gname) γ :
HINT □⟨p own γ ( GSet X) [b Y; b = true own γ ( GSet Y) b = false Y = ∅⌝]
[bupd] gs;
own γ ( GSet gs) [if b then gs = X Y else gs = X].
Proof.
rewrite /BiAbd /= => [[]] Y /=;
rewrite bi.intuitionistically_if_elim.
- rewrite -(bi.exist_intro (X Y)).
do 3 iStepS; rewrite bi.intuitionistically_if_elim.
- rewrite -(bi.exist_intro (X x0)).
iStepsS.
- iStepS. iExists X. iStepsS.
- iExists X. iStepsS.
Qed.
Global Instance saved_prop_alloc P E :
BiAbd (TTl := [tele]) (TTr:= [tele_pair gname]) false empty_hyp_last (λ γ, saved_prop_own γ P) (fupd E E) emp%I (λ γ, saved_prop_own γ P)%I.
Global Instance saved_prop_alloc P :
HINT empty_hyp_last [- ; emp] [bupd] γ; saved_prop_own γ P [saved_prop_own γ P].
Proof.
rewrite /BiAbd /= empty_hyp_last_eq left_id.
iIntros "_".
iStepS.
iMod (saved_prop_alloc P%I) as (γsp) "#Hsp".
iStepsS.
Qed.
(* not done by local_updates since this does not satisfy coallocation premises *)
Global Instance own_auth_alloc X E :
BiAbd (TTl := [tele]) (TTr:= [tele_pair gname]) false empty_hyp_last (λ γ, own γ ( GSet X)) (fupd E E)
⌜✓ X%I (λ γ, own γ ( GSet X))%I.
Global Instance own_auth_alloc X :
HINT empty_hyp_last [- ; emp] [bupd] γ; own γ ( GSet X) [own γ ( GSet X)].
Proof.
rewrite /BiAbd /= empty_hyp_last_eq left_id.
iIntros "%".
iStepS.
iMod (own_alloc ( (GSet X) (GSet X))) as (γ) "[H1 H2]".
{ by apply auth_both_valid_discrete. }
by iExists γ; iFrame.
iStepsS.
Qed.
Global Instance merged_hyp_saved_prop γ P Q :
......@@ -76,26 +71,23 @@ Section big_opS_biabds.
Global Instance big_sepS_delete_biabd `{EqDecision A, Countable A} (Φ : A PROP) (X : gset A) (x : A) p :
SolveSepSideCondition (x X)
BiAbd p (TTl := [tele]) (TTr := [tele])
([ set] y X, Φ y)%I ([ set] y X {[x]}, Φ y)%I
id emp%I (Φ x).
HINT □⟨p [ set] y X, Φ y [- ; emp] [id]; [ set] y X {[x]}, Φ y [Φ x].
Proof.
rewrite /SolveSepSideCondition /BiAbd
/= right_id bi.intuitionistically_if_elim => Hx.
by rewrite big_sepS_delete // bi.sep_comm.
move => Hx. iStepS.
rewrite bi.intuitionistically_if_elim.
rewrite big_sepS_delete //. iStepsS.
Qed.
Global Instance internal_eq_biabd `{BiInternalEq PROP} p (P Q : PROP) :
TCOr (TCEq p true) (TCOr (Affine (PROP := PROP) (P Q)%I) (Absorbing P))
BiAbd p (TTl := [tele]) (TTr := [tele]) (P Q)%I Q id P emp%I.
HINT □⟨p P Q [- ; P] [id]; Q [emp].
Proof.
rewrite /BiAbd /= right_id => HpQ.
case: HpQ => [-> /= | ]; last rewrite bi.intuitionistically_if_elim.
- iIntros "[#HPQ P]".
by iRewrite -"HPQ".
- case => HQ;
iIntros "[HPQ P]";
by iRewrite -"HPQ".
case => [-> | HPQ].
- iStepS. iRewrite -"H1". iStepsS.
- case: HPQ => HPQ; iStartProof => /=;
rewrite bi.intuitionistically_if_elim; iStepS.
* iRewrite -"H1"; iStepsS.
* iRewrite -"H1"; iStepsS.
Qed.
End big_opS_biabds.
......@@ -166,5 +158,5 @@ Section proof.
- once opened, the required updates are really quite subtle (and i think set in general is not really nice for automation)
- closing of the invariant requires introducing ▷ to get the required saved_prop agreement, which means
we forego being able to update. *)
Admitted.
Abort.
End proof.
......@@ -40,15 +40,15 @@ Section stacks.
l, v = #l inv N (stack_inv P l)%I.
Global Instance biabd_islist_none P :
BiAbd (TTl := [tele]) (TTr := [tele]) false empty_hyp_first (is_list P NONEV) id emp%I emp%I.
Proof. rewrite /BiAbd /= is_list_unfold /=. iSmash. Qed.
HINT empty_hyp_first [- ; emp] [id]; is_list P NONEV [emp].
Proof. iStepS. rewrite is_list_unfold /=. iSmash. Qed.
Global Instance biabd_islist_some P (l : loc) :
BiAbd (TTl := [tele (_ : val) (_ : val)]) (TTr := [tele]) false empty_hyp_last (is_list P $ SOMEV #l)
id (λ h t, l ↦□ (h, t)%V P h is_list P t)%I (λ _ _, emp)%I.
HINT empty_hyp_last [h t; l ↦□ (h, t)%V P h is_list P t] [id];
is_list P (SOMEV #l) [emp].
Proof.
rewrite /BiAbd /= empty_hyp_last_eq => h t.
rewrite (is_list_unfold _ (InjRV _)) left_id right_id /=. iStepS.
do 3 iStepS.
rewrite (is_list_unfold _ (InjRV _)) right_id /=.
iRight. iStepsS.
Qed.
......@@ -63,13 +63,13 @@ Section stacks.
iStepsS; iIntros "!>"; iStepsS.
Qed.
Global Instance biabd_islist_pop P l h v E p :
BiAbd (TTl := [tele]) (TTr := [tele]) p (l ↦□ (h, v)%V)%I ( is_list P v)%I
(fupd E E) (is_list P (SOMEV #l))%I (val_is_unboxed v P h)%I | 30.
Global Instance biabd_islist_pop P l h v p E :
HINT □⟨p l ↦□ (h, v)%V [- ; is_list P (SOMEV #l)] [fupd E E];
is_list P v [val_is_unboxed v P h] | 30.
Proof.
rewrite /BiAbd /= bi.intuitionistically_if_elim.
rewrite (is_list_unfold _ (InjRV _)) /=. iStepS.
rewrite is_list_unfold; iRevert "H3". iSmash.
iStepS. rewrite bi.intuitionistically_if_elim.
rewrite (is_list_unfold _ (InjRV _)) /=. iReIntro "H2".
rewrite is_list_unfold. iReIntro "H3"; iSmash.
Qed.
Theorem new_stack_spec P :
......
......@@ -118,16 +118,15 @@ Section stack_works.
( mailbox l, v = (mailbox, #l)%V is_mailbox Nmailbox P mailbox inv N (stack_inv P l))%I.
Global Instance biabd_islist_none P :
BiAbd (TTl := [tele]) (TTr := [tele]) false empty_hyp_first (is_list P NONEV) id emp%I emp%I.
Proof. rewrite /BiAbd /= is_list_unfold /=. iSmash. Qed.
HINT empty_hyp_first [- ; emp] [id]; is_list P NONEV [emp].
Proof. iStepS. rewrite is_list_unfold. iSmash. Qed.
Global Instance biabd_islist_some P l :
BiAbd (TTl := [tele (_ : val) (_ : val)]) (TTr := [tele]) false empty_hyp_last (is_list P $ SOMEV #l)
id (λ h t, l ↦□ (h, t)%V P h is_list P t)%I (λ _ _, emp)%I.
HINT empty_hyp_last [h t; l ↦□ (h, t)%V P h is_list P t] [id];
is_list P (SOMEV #l) [emp].
Proof.
rewrite /BiAbd /= empty_hyp_last_eq => h t.
rewrite (is_list_unfold _ (SOMEV _)) /=.
iStepsS. iRight. iStepsS.
iStepsS. rewrite (is_list_unfold _ (SOMEV _)) /=.
iRight. iStepsS.
Qed.
Instance is_list_remember_part P v :
......@@ -141,11 +140,11 @@ Section stack_works.
Qed.
Global Instance biabd_islist_pop P l h v E p :
BiAbd (TTl := [tele]) (TTr := [tele]) p (l ↦□ (h, v)%V)%I ( is_list P v)%I
(fupd E E) (is_list P (SOMEV #l))%I (val_is_unboxed v P h)%I | 30.
HINT □⟨p l ↦□ (h, v)%V [- ; is_list P (SOMEV #l)] [fupd E E];
is_list P v [val_is_unboxed v P h] | 30.
Proof.
rewrite /BiAbd /= bi.intuitionistically_if_elim.
rewrite (is_list_unfold _ (InjRV _)) /=. iStepS.
iStepS. rewrite bi.intuitionistically_if_elim. iReIntro "H1".
rewrite (is_list_unfold _ (InjRV _)) /=. iReIntro "H2".
rewrite is_list_unfold; iRevert "H3". iSmash.
Qed.
......
......@@ -91,24 +91,24 @@ Section stack.
Qed.
Global Instance biabd_islist_none xs :
BiAbd (TTl := [tele]) (TTr := [tele]) false empty_hyp_first (list_inv xs NONEV) id xs = []%I xs = []%I.
Proof. rewrite /BiAbd /=. iStepsS. Qed.
HINT empty_hyp_first [xs = []] [id]; list_inv xs NONEV [xs = []].
Proof. iStepsS. Qed.
Lemma list_inv_unboxed xs v : list_inv xs v val_is_unboxed v%I.
Proof. induction xs; iStepsS. Qed.
Global Instance biabd_islist_keep_unboxed p xs v :
BiAbd (TTl := [tele]) (TTr := [tele]) p (list_inv xs v) (list_inv xs v) id emp%I val_is_unboxed v%I | 40.
HINT □⟨p list_inv xs v [- ; emp] [id]; list_inv xs v [val_is_unboxed v] | 40.
Proof.
rewrite /BiAbd /= bi.intuitionistically_if_elim; iStepS.
iStepS. rewrite bi.intuitionistically_if_elim.
iAssert val_is_unboxed v%I as "%". { by iApply list_inv_unboxed. }
iStepsS.
Qed.
Global Instance biabd_islist_some (l : loc) xs :
BiAbd (TTl := [tele_pair val; list val; val]) (TTr := [tele]) false empty_hyp_last (list_inv xs $ SOMEV #l)%I
id (λ x xs' t, l ↦□ (x, t) list_inv 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, t) list_inv xs' t xs = x :: xs'] [id];
list_inv xs (SOMEV #l) [xs = x :: xs'].
Proof. iStepsS. Qed.
(** Proofs. *)
Lemma new_stack_spec :
......@@ -119,10 +119,10 @@ Section stack.
TCIf (SolveSepSideCondition (l1 = l2)) False TCTrue
(* makes sure we find a better instance if they are unifiable
-> what is new here, is the quantification over l3! *)
BiAbd (TTl := [tele_pair list val]) (TTr := [tele]) p (own γs ( Excl' l1)) (own γs ( Excl' l2)) bupd
(λ l3, own γs ( Excl' l3)) (λ l3, own γs ( Excl' l2) l3 = l1 )%I | 30.
HINT □⟨p own γs ( Excl' l1) [l3; own γs ( Excl' l3)] [bupd];
own γs ( Excl' l2) [own γs ( Excl' l2) l3 = l1] | 30.
Proof.
rewrite /SolveSepSideCondition /BiAbd /= => Hneq l3.
move => _. iStepS.
rewrite bi.intuitionistically_if_elim.
iStepsS.
Qed.
......@@ -207,13 +207,16 @@ Ltac iWPStep :=
iInv "H1" as "HN"; iReIntro "HN".
iMod ("H10" with "H12") as "HAU".
iMod "HAU" as "[%l [Hl1 [_ Hl2]]]"; iReIntro "Hl1".
iAssert (|==> own γs ( Excl' (x12 :: x10)) stack_content γs (x12 :: x10))%I with "[H14 H12]" as ">[H14 H12]".
iAssert (|==> own γs ( Excl' (x13 :: x10)) stack_content γs (x13 :: x10))%I with "[H14 H12]" as ">[H14 H12]".
{ iStepsS. }
iMod ("Hl2" with "H12") as "Hx14".
iMod "H3" as "[%l [Hl1 [_ Hl2]]]"; iReIntro "Hl1".
iAssert (|==> own γs ( Excl' x10) stack_content γs x10)%I with "[H14 H12]" as ">[H14 H12]".
{ iStepsS. }
iMod ("Hl2" $! (InjRV x12) with "[H12]") as "Hl2"; first iStepsS.
iMod ("Hl2" $! (InjRV x13) with "[H12]") as "Hl2"; first iStepsS.
solveStep.
solveStep.
solveStep.
solveStep.
solveStep.
solveStep.
......
......@@ -106,18 +106,18 @@ Section proof.
Qed.
Global Instance abduct_saved_pred_alloc Q :
BiAbd (TTl := [tele]) (TTr := [tele_pair gname]) false empty_hyp_last (λ γ, saved_pred_own γ Q) (bupd) emp%I (λ γ, saved_pred_own γ Q)%I.
HINT empty_hyp_last [- ; emp] [bupd] γ; saved_pred_own γ Q [saved_pred_own γ Q].
Proof.
rewrite /BiAbd /= empty_hyp_last_eq left_id.
iStepS.
iMod (saved_pred_alloc Q) as (γsp) "#HQ".
iStepsS.
Qed.
Global Instance pers_to_intuit (P : iProp Σ) p :
BiAbd (TTl := [tele]) (TTr := [tele]) p (<pers> P)%I ( P)%I id emp%I ( P)%I.
HINT □⟨p (<pers> P) [- ; emp] [id]; P [ P].
Proof.
rewrite /BiAbd /= right_id bi.intuitionistically_if_elim.
rewrite -bi.intuitionistically_into_persistently.
iStepS.
rewrite bi.intuitionistically_if_elim -bi.intuitionistically_into_persistently.
iStepsS.
Qed.
......
......@@ -202,7 +202,7 @@ Section drop_modal_instances.
(* this causes better inspection on things like □ ⋄ ⌜φ⌝ *)
Global Instance drop_modal_persistently R:
DropModal (PROP := PROP) (bi_intuitionistically)%I R Persistent.
DropModal (PROP := PROP) (bi_intuitionistically)%I R (λ P, TCAnd (Persistent P) (Affine P)).
Proof.
rewrite /DropModal => P HP.
iIntros "HPR #HP".
......
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