Skip to content
Snippets Groups Projects
Commit 547bf068 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Tweak proofs.

parent 05e9c03e
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
opam.pins
+ 1
− 1
View file @ 547bf068
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq#f49a7f18c4afc34b9d2766f2b18e45e1a3cd38e7
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq#4417beb8bfa43f89c09a027e8dd55550bf8f7a63
theories/typing/perm_incl.v
+ 4
− 7
View file @ 547bf068
......@@ -37,8 +37,8 @@ Section props.
Proof.
split.
- iIntros (? tid) "H". eauto.
- iIntros (??? H12 H23 tid) "#LFT H".
iMod (H12 with "LFT H") as "H". by iApply (H23 with "LFT").
- iIntros (??? H12 H23 tid) "#LFT H". iApply (H23 with "LFT >").
by iApply (H12 with "LFT").
Qed.
Global Instance perm_equiv_equiv : Equivalence (⇔).
......@@ -277,10 +277,7 @@ Section props.
iApply (fupd_mask_mono (↑lftN)). done.
iMod (bor_create with "LFT Hown") as "[Hbor Hext]". done.
iSplitL "Hbor". by simpl; eauto.
iMod (bor_create with "LFT Hf") as "[_ Hf]". done.
iIntros "!>#H†".
iMod ("Hext" with "H†") as "Hext". iMod ("Hf" with "H†") as "Hf". iIntros "!>/=".
iExists _. iFrame. auto.
iIntros "!>#H†". iExists _. iMod ("Hext" with "H†") as "$". by iFrame.
Qed.
Lemma rebor_uniq_borrowing κ κ' ν ty :
......@@ -293,7 +290,7 @@ Section props.
iApply (fupd_mask_mono (↑lftN)). done.
iMod (rebor with "LFT Hord H") as "[H Hextr]". done.
iModIntro. iSplitL "H". iExists _. by eauto.
iIntros "H†". iMod ("Hextr" with "H†"). simpl. auto.
iIntros "H†". iExists _. by iMod ("Hextr" with "H†") as "$".
Qed.
Lemma lftincl_borrowing κ κ' q : borrowing κ ⊤ q.[κ'] (κ ⊑ κ').
......
theories/typing/type.v
+ 30
− 28
View file @ 547bf068
......@@ -157,7 +157,8 @@ Section types.
(∃ l:loc, ⌜vl = [ #l ]⌝ ∗ ▷ l ↦∗: ty.(ty_own) tid ∗ ▷ †{q}l…ty.(ty_size))%I;
ty_shr κ tid E l :=
(∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ∗
∀ q', □ (q'.[κ] ={mgmtE ∪ E, mgmtE}▷=∗ ty.(ty_shr) κ tid E l' ∗ q'.[κ]))%I
□ (∀ q' F, ⌜E ∪ mgmtE ⊆ F⌝ →
q'.[κ] ={F,F∖E}▷=∗ ty.(ty_shr) κ tid E l' ∗ q'.[κ]))%I
|}.
Next Obligation. done. Qed.
Next Obligation.
......@@ -176,25 +177,26 @@ Section types.
rewrite bor_unfold_idx. iDestruct "Hb2" as (i) "(#Hpb&Hpbown)".
iMod (inv_alloc N _ (idx_bor_own 1 i ∨ ty_shr ty κ tid (↑N) l')%I
with "[Hpbown]") as "#Hinv"; first by eauto.
iExists l'. iIntros "!>{$Hbf}". iIntros (q'') "!#Htok".
iExists l'. iIntros "!>{$Hbf}!#". iIntros (q'' F) "% Htok".
iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
replace ((mgmtE ∪ ↑N) ∖ ↑N) with mgmtE by set_solver.
iDestruct "INV" as "[>Hbtok|#Hshr]".
- iMod (bor_later_tok with "LFT [Hbtok] Htok") as "[Hb Htok]". set_solver.
{ rewrite bor_unfold_idx. iExists i. eauto. }
iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]"; try done.
iApply "Hclose". eauto.
- iIntros "!>". iNext. iMod ("Hclose" with "[]") as "_"; by eauto.
- iMod (bor_later_tok with "LFT [Hbtok] Htok") as "H". set_solver.
{ rewrite bor_unfold_idx. eauto. }
iModIntro. iNext. iMod "H" as "[Hb Htok]".
iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]". done. set_solver.
iApply "Hclose". auto.
- iModIntro. iNext. iMod ("Hclose" with "[]") as "_"; by eauto.
Qed.
Next Obligation.
intros _ ty κ κ' tid E E' l ?. iIntros "#LFT #Hκ #H".
iDestruct "H" as (l') "[Hfb Hvs]".
iExists l'. iSplit. by iApply (frac_bor_shorten with "[]").
iIntros (q') "!#Htok".
iApply step_fupd_mask_mono. reflexivity. apply union_preserving_l. eassumption.
iDestruct "H" as (l') "[Hfb #Hvs]".
iExists l'. iSplit. by iApply (frac_bor_shorten with "[]"). iIntros "!#".
iIntros (q' F) "% Htok".
iApply (step_fupd_mask_mono F _ _ (F∖E)). set_solver. set_solver.
iMod (lft_incl_acc with "Hκ Htok") as (q'') "[Htok Hclose]". set_solver.
iMod ("Hvs" $! q'' with "Htok") as "[Hshr Htok]".
iMod ("Hclose" with "Htok") as "$". by iApply (ty.(ty_shr_mono) with "LFT Hκ").
iMod ("Hvs" with "* [%] Htok") as "Hvs'". set_solver. iModIntro. iNext.
iMod "Hvs'" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
by iApply (ty.(ty_shr_mono) with "LFT Hκ").
Qed.
Next Obligation. done. Qed.
......@@ -204,8 +206,8 @@ Section types.
(∃ l:loc, ⌜vl = [ #l ]⌝ ∗ &{κ} l ↦∗: ty.(ty_own) tid)%I;
ty_shr κ' tid E l :=
(∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗
∀ q', □ (q'.[κ∪κ']
={mgmtE ∪ E, ↑tlN}▷=∗ ty.(ty_shr) (κ∪κ') tid E l' ∗ q'.[κ∪κ']))%I
□ ∀ q' F, ⌜E ∪ mgmtE ⊆ F⌝ → q'.[κ∪κ']
={F, F∖E∖↑lftN}▷=∗ ty.(ty_shr) (κ∪κ') tid E l' ∗ q'.[κ∪κ'])%I
|}.
Next Obligation. done. Qed.
Next Obligation.
......@@ -223,16 +225,14 @@ Section types.
rewrite {1}bor_unfold_idx. iDestruct "Hb2" as (i) "[#Hpb Hpbown]".
iMod (inv_alloc N _ (idx_bor_own 1 i ∨ ty_shr ty (κ∪κ') tid (↑N) l')%I
with "[Hpbown]") as "#Hinv"; first by eauto.
iExists l'. iIntros "!>{$Hbf}". iIntros (q'') "!#Htok".
iApply (step_fupd_mask_mono (mgmtE ∪ ↑N) _ _ ((mgmtE ∪ ↑N) ∖ ↑N ∖ ↑lftN)).
{ assert (nclose lftN ⊥ ↑tlN) by solve_ndisj. set_solver. } set_solver.
iExists l'. iIntros "!>{$Hbf}!#". iIntros (q'' F) "% Htok".
iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
iDestruct "INV" as "[>Hbtok|#Hshr]".
- iAssert (&{κ'}&{κ} l' ↦∗: ty_own ty tid)%I with "[Hbtok]" as "Hb".
{ rewrite (bor_unfold_idx κ'). eauto. }
iMod (bor_unnest with "LFT Hb") as "Hb". set_solver.
iMod (ty.(ty_share) with "LFT Hb Htok") as "[#Hshr Htok]"; try done. set_solver.
iMod ("Hclose" with "[]") as "_". eauto. by iFrame.
- iMod (bor_unnest _ _ _ (l' ↦∗: ty_own ty tid)%I with "LFT [Hbtok]") as "Hb".
{ set_solver. } { iApply bor_unfold_idx. eauto. }
iModIntro. iNext. iMod "Hb".
iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]"; try done. set_solver.
iApply "Hclose". eauto.
- iMod ("Hclose" with "[]") as "_". by eauto.
iApply step_fupd_mask_mono; last by eauto. done. set_solver.
Qed.
......@@ -243,11 +243,13 @@ Section types.
- iApply lft_le_incl. apply gmultiset_union_subseteq_l.
- iApply (lft_incl_trans with "[] Hκ").
iApply lft_le_incl. apply gmultiset_union_subseteq_r. }
iExists l'. iSplit. by iApply (frac_bor_shorten with "[]"). iIntros (q) "!#Htok".
iApply step_fupd_mask_mono. reflexivity. apply union_preserving_l. eassumption.
iExists l'. iSplit. by iApply (frac_bor_shorten with "[]").
iIntros "!#". iIntros (q F) "% Htok".
iApply (step_fupd_mask_mono F _ _ (F∖E∖ ↑lftN)). set_solver. set_solver.
iMod (lft_incl_acc with "Hκ0 Htok") as (q') "[Htok Hclose]". set_solver.
iMod ("Hvs" $! q' with "Htok") as "[#Hshr Htok]".
iMod ("Hclose" with "Htok") as "$". by iApply (ty_shr_mono with "LFT Hκ0").
iMod ("Hvs" with "* [%] Htok") as "Hvs'". set_solver. iModIntro. iNext.
iMod "Hvs'" as "[#Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
by iApply (ty_shr_mono with "LFT Hκ0").
Qed.
Next Obligation. done. Qed.
......
theories/typing/type_incl.v
+ 14
− 14
View file @ 547bf068
......@@ -38,8 +38,7 @@ Section ty_incl.
Lemma ty_incl_weaken ρ θ ty1 ty2 :
ρ ⇒ θ → ty_incl θ ty1 ty2 → ty_incl ρ ty1 ty2.
Proof.
iIntros (Hρθ Hρ' tid) "#LFT H". iMod (Hρθ with "LFT H").
by iApply (Hρ' with "LFT").
iIntros (Hρθ Hρ' tid) "#LFT H". iApply (Hρ' with "LFT>"). iApply (Hρθ with "LFT H").
Qed.
Global Instance ty_incl_preorder ρ: Duplicable ρ → PreOrder (ty_incl ρ).
......@@ -63,8 +62,9 @@ Section ty_incl.
iDestruct (ty_size_eq with "Hown") as %<-. iFrame.
iExists _. by iFrame.
- iDestruct "H" as (l') "[Hfb #Hvs]". iSplit; last done. iExists l'. iFrame.
iIntros (q') "!#Hκ". iMod ("Hvs" $! _ with "Hκ") as "[Hshr $]".
by iDestruct ("Hshri" $! _ _ _ with "Hshr") as "[$ _]".
iIntros "!#". iIntros (q' F) "% Hκ".
iMod ("Hvs" with "* [%] Hκ") as "Hvs'". done. iModIntro. iNext.
iMod "Hvs'" as "[Hshr $]". by iDestruct ("Hshri" with "* Hshr") as "[$ _]".
Qed.
Lemma lft_incl_ty_incl_uniq_bor ty κ1 κ2 :
......@@ -79,9 +79,10 @@ Section ty_incl.
apply gmultiset_union_subseteq_l.
- iApply lft_le_incl. apply gmultiset_union_subseteq_r. }
iSplitL; last done. iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'.
iFrame. iIntros (q') "!#Htok".
iFrame. iIntros "!#". iIntros (q' F) "% Htok".
iMod (lft_incl_acc with "Hincl' Htok") as (q'') "[Htok Hclose]". set_solver.
iMod ("Hupd" with "*Htok") as "[H Htok]". iMod ("Hclose" with "Htok") as "$".
iMod ("Hupd" with "* [%] Htok") as "Hupd'"; try done. iModIntro. iNext.
iMod "Hupd'" as "[H Htok]". iMod ("Hclose" with "Htok") as "$".
by iApply (ty_shr_mono with "LFT Hincl' H").
Qed.
......@@ -194,7 +195,7 @@ Section ty_incl.
→ (nth i tyl2 ∅%T).(ty_own) tid vl)).
{ clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH].
- iIntros "_ _!>*!#". eauto.
- iIntros "#LFT #Hρ". iMod (IH with "LFT Hρ") as "#IH".
- iIntros "#LFT #Hρ". iMod (IH with "LFT Hρ") as "#IH".
iMod (Hincl with "LFT Hρ") as "[#Hh _]".
iIntros "!>*!#*Hown". destruct i as [|i]. by iApply "Hh". by iApply "IH". }
iMod (Hincl with "LFT Hρ") as "#Hincl". iIntros "!>!#*H".
......@@ -219,8 +220,8 @@ Section ty_incl.
Proof.
iIntros (? Hρ1ρ2 tid) "#LFT #Hρ!>". iSplit; iIntros "!#*H"; last by auto.
iDestruct "H" as (f) "[% Hwp]". subst. iExists _. iSplit. done.
iIntros (vl) "Hρ2 Htl". iMod (Hρ1ρ2 with "LFT [$Hρ2 $Hρ]").
by iApply ("Hwp" with "[-Htl] Htl").
iIntros (vl) "Hρ2 Htl". iApply ("Hwp" with ">[-Htl] Htl").
iApply (Hρ1ρ2 with "LFT"). by iFrame.
Qed.
Lemma ty_incl_fn {A n} ρ ρ1 ρ2 :
......@@ -229,13 +230,12 @@ Section ty_incl.
Proof.
iIntros (? Hρ1ρ2 tid) "#LFT #Hρ!>". iSplit; iIntros "!#*#H".
- iDestruct "H" as (f) "[% Hwp]". subst. iExists _. iSplit. done.
iIntros (x vl) "!#[Hρ2 Htl]". iMod (Hρ1ρ2 with "LFT [$Hρ2 $Hρ]").
iApply "Hwp". by iFrame.
iIntros (x vl) "!#[Hρ2 Htl]". iApply ("Hwp" with ">").
  • Ralf Jung @jung ·
    Owner

    What does iApply ... with ">" do? > doesn't seem to match the grammar given for spec patterns in the documentation.

    Cc @robbertkrebbers

  • Jacques-Henri Jourdan @jjourdan ·
    Maintainer

    That's a very cool feature I just learnt: it lets you apply something that has a modality, while keeping the modality here for the generated subgoal.

  • Ralf Jung @jung ·
    Owner

    But which assumptions do you get in the subgoal? Is it equivalent to >[] or >[-]?

  • Jacques-Henri Jourdan @jjourdan ·
    Maintainer

    You get all the remaining assumptions. I.e., as usually with iApply, there is an implicit "[-]".

  • Ralf Jung @jung ·
    Owner

    How is this "as usual"? I was not aware that [-] is a default in other ways, too. Certainly the documentation for iApply doesn't mention this.

  • Jacques-Henri Jourdan @jjourdan ·
    Maintainer

    Well, If your goal is A and you have "H" : B -* A, you can iApply "H", and your goal becomes B with all the other hypotheses. That's pretty usual.

  • Robbert Krebbers @robbertkrebbers ·
    Owner

    What JH said :).

  • Ralf Jung @jung ·
    Owner

    Do I have to write an issue for the documentation to be updated, or is this informal request sufficient? ;)

  • Jacques-Henri Jourdan @jjourdan ·
    Maintainer

    I don't know. It feels rather intuitive, no? If you feel it necessary, we could add an example in the doc.

  • Ralf Jung @jung ·
    Owner

    I feel the doc is plain wrong -- the grammar for "proof terms" does not allow the term "H" with ">".

  • Robbert Krebbers @robbertkrebbers ·
    Owner

    I have improved the docs.

  • Ralf Jung @jung ·
    Owner

    Great, thanks :)

  • Please register or sign in to reply
iFrame. iApply (Hρ1ρ2 with "LFT"). by iFrame.
- iSplit; last done. simpl. iDestruct "H" as (vl0) "[? Hvl]".
iExists vl0. iFrame "#". iNext. iDestruct "Hvl" as (f) "[% Hwp]".
iExists f. iSplit. done.
iIntros (x vl) "!#[Hρ2 Htl]". iMod (Hρ1ρ2 with "LFT [$Hρ2 $Hρ]").
iApply "Hwp". by iFrame.
iExists f. iSplit. done. iIntros (x vl) "!#[Hρ2 Htl]".
iApply ("Hwp" with ">"). iFrame. iApply (Hρ1ρ2 with "LFT >"). by iFrame.
Qed.
Lemma ty_incl_fn_cont {A n} ρ ρf (x : A) :
......
theories/typing/typing.v
+ 11
− 19
View file @ 547bf068
......@@ -292,17 +292,13 @@ Section typing.
iApply (has_type_wp with "H◁"). iIntros (v) "Hνv H◁!>". iDestruct "Hνv" as %Hνv.
rewrite has_type_value. iDestruct "H◁" as (l) "[Heq #H↦]". iDestruct "Heq" as %[=->].
iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[[Htok1 Htok2] Hclose]". done.
iDestruct "H↦" as (vl) "[H↦b Hown]".
iDestruct "H↦" as (vl) "[H↦b #Hown]".
iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
iApply (wp_fupd_step _ (↑heapN) with "[Hown Htok2]"); try done.
- rewrite -(left_id (R:=eq) ∅ (∪) (↑heapN)). assert (⊤ = ⊤∖↑heapN ∪ ↑heapN) as ->.
{ by rewrite (comm (R:=eq)) -union_difference_L. }
iApply step_fupd_mask_frame_r; try set_solver.
iApply step_fupd_mask_mono; last by iApply ("Hown" with "* Htok2").
set_solver. repeat apply union_least; solve_ndisj.
iApply (wp_fupd_step _ (⊤∖↑lrustN) with "[Hown Htok2]"); try done.
- iApply ("Hown" with "* [%] Htok2"). set_solver.
- wp_read. iIntros "!>[Hshr ?]". iFrame "H⊑".
iSplitL "Hshr"; first by iExists _; auto.
iMod ("Hclose'" with "[$H↦]") as "?". iApply "Hclose". iFrame.
iSplitL "Hshr"; first by iExists _; auto. iApply ("Hclose" with ">").
iFrame. iApply "Hclose'". auto.
Qed.
Lemma typed_deref_uniq_bor_bor ty ν κ κ' κ'' q:
......@@ -326,7 +322,7 @@ Section typing.
wp_read. iIntros "!> Hbor". iFrame "#". iSplitL "Hbor".
- iExists _. iSplitR; first by auto. iApply (bor_shorten with "[] Hbor").
iApply (lft_incl_glb with "H⊑2"). iApply lft_incl_refl.
- iMod ("Hclose'" with "[$H↦]") as "[_ ?]". by iApply "Hclose".
- iApply ("Hclose" with ">"). by iMod ("Hclose'" with "[$H↦]") as "[_ $]".
Qed.
Lemma typed_deref_shr_bor_bor ty ν κ κ' κ'' q:
......@@ -343,16 +339,12 @@ Section typing.
iAssert (κ' ⊑ κ'' ∪ κ')%I as "#H⊑3".
{ iApply (lft_incl_glb with "H⊑2 []"). iApply lft_incl_refl. }
iMod (lft_incl_acc with "H⊑3 Htok2") as (q''') "[Htok Hclose'']". done.
iApply (wp_fupd_step _ (↑heapN) with "[Hown Htok]"); try done.
- rewrite -(left_id (R:=eq) ∅ (∪) (↑heapN)). assert (⊤ = ⊤∖↑heapN ∪ ↑heapN) as ->.
{ by rewrite (comm (R:=eq)) -union_difference_L. }
iApply step_fupd_mask_frame_r; try set_solver.
iApply step_fupd_mask_mono; last by iApply ("Hown" with "* Htok").
set_solver. repeat apply union_least; solve_ndisj.
iApply (wp_fupd_step _ (_∖_) with "[Hown Htok]"); try done.
- iApply ("Hown" with "* [%] Htok"). set_solver.
- wp_read. iIntros "!>[Hshr Htok]". iFrame "H⊑1". iSplitL "Hshr".
+ iExists _. iSplitR. done. by iApply (ty_shr_mono with "LFT H⊑3 Hshr").
+ iMod ("Hclose''" with "Htok"). iMod ("Hclose'" with "[$H↦]").
iApply "Hclose". iFrame.
+ iApply ("Hclose" with ">"). iMod ("Hclose'" with "[$H↦]") as "$".
by iMod ("Hclose''" with "Htok") as "$".
Qed.
Definition update (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=
......@@ -421,7 +413,7 @@ Section typing.
typed_program ρ2 e → (ρ1 ⇒ ρ2) → typed_program ρ1 e.
Proof.
iIntros (Hρ2 Hρ12 tid) "!#(#HEAP & #LFT & Hρ1 & Htl)".
iMod (Hρ12 with "LFT Hρ1"). iApply Hρ2. iFrame "∗#".
iApply (Hρ2 with ">"). iFrame "∗#". iApply (Hρ12 with "LFT Hρ1").
Qed.
Lemma typed_program_exists {A} ρ θ e:
......
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