Commit c5045145 authored by Robbert Krebbers's avatar Robbert Krebbers

Make `iDestruct ... as (cpat) "..."` work on '⌜φ⌝ ∧ P` and `⌜φ⌝ ∗ P`.

The advantage is that we can directly use a Coq introduction pattern
`cpat` to perform actions to the pure assertion. Before, this had
to be done in several steps:

  iDestruct ... as "[Htmp ...]"; iDestruct "Htmp" as %cpat.

That is, one had to introduce a temporary name.

I expect this to be quite useful in various developments as many of
e.g. our invariants are written as:

  ∃ x1 .. x2, ⌜ pure stuff ⌝ ∗ spacial stuff.
parent bd692a8b
...@@ -185,7 +185,7 @@ Lemma slice_insert_full E q f P Q : ...@@ -185,7 +185,7 @@ Lemma slice_insert_full E q f P Q :
slice N γ Q ?q box N (<[γ:=true]> f) (Q P). slice N γ Q ?q box N (<[γ:=true]> f) (Q P).
Proof. Proof.
iIntros (?) "HQ Hbox". iIntros (?) "HQ Hbox".
iMod (slice_insert_empty with "Hbox") as (γ) "(% & #Hslice & Hbox)". iMod (slice_insert_empty with "Hbox") as (γ ?) "[#Hslice Hbox]".
iExists γ. iFrame "%#". iMod (slice_fill with "Hslice HQ Hbox"); first done. iExists γ. iFrame "%#". iMod (slice_fill with "Hslice HQ Hbox"); first done.
by apply lookup_insert. by rewrite insert_insert. by apply lookup_insert. by rewrite insert_insert.
Qed. Qed.
...@@ -251,11 +251,11 @@ Proof. ...@@ -251,11 +251,11 @@ Proof.
iIntros (??) "#HQQ' #Hs Hb". destruct b. iIntros (??) "#HQQ' #Hs Hb". destruct b.
- iMod (slice_delete_full with "Hs Hb") as (P') "(HQ & Heq & Hb)"; try done. - iMod (slice_delete_full with "Hs Hb") as (P') "(HQ & Heq & Hb)"; try done.
iDestruct ("HQQ'" with "HQ") as "HQ'". iDestruct ("HQQ'" with "HQ") as "HQ'".
iMod (slice_insert_full with "HQ' Hb") as (γ') "(% & #Hs' & Hb)"; try done. iMod (slice_insert_full with "HQ' Hb") as (γ' ?) "[#Hs' Hb]"; try done.
iExists γ', _. iIntros "{$∗ $# $%} !>". do 2 iNext. iRewrite "Heq". iExists γ', _. iIntros "{$∗ $# $%} !>". do 2 iNext. iRewrite "Heq".
iAlways. by iSplit; iIntros "[? $]"; iApply "HQQ'". iAlways. by iSplit; iIntros "[? $]"; iApply "HQQ'".
- iMod (slice_delete_empty with "Hs Hb") as (P') "(Heq & Hb)"; try done. - iMod (slice_delete_empty with "Hs Hb") as (P') "(Heq & Hb)"; try done.
iMod (slice_insert_empty with "Hb") as (γ') "(% & #Hs' & Hb)"; try done. iMod (slice_insert_empty with "Hb") as (γ' ?) "[#Hs' Hb]"; try done.
iExists γ', _. iIntros "{$∗ $# $%} !>". do 2 iNext. iRewrite "Heq". iExists γ', _. iIntros "{$∗ $# $%} !>". do 2 iNext. iRewrite "Heq".
iAlways. by iSplit; iIntros "[? $]"; iApply "HQQ'". iAlways. by iSplit; iIntros "[? $]"; iApply "HQQ'".
Qed. Qed.
...@@ -268,16 +268,16 @@ Lemma slice_split E q f P Q1 Q2 γ b : ...@@ -268,16 +268,16 @@ Lemma slice_split E q f P Q1 Q2 γ b :
Proof. Proof.
iIntros (??) "#Hslice Hbox". destruct b. iIntros (??) "#Hslice Hbox". destruct b.
- iMod (slice_delete_full with "Hslice Hbox") as (P') "([HQ1 HQ2] & Heq & Hbox)"; try done. - iMod (slice_delete_full with "Hslice Hbox") as (P') "([HQ1 HQ2] & Heq & Hbox)"; try done.
iMod (slice_insert_full with "HQ1 Hbox") as (γ1) "(% & #Hslice1 & Hbox)"; first done. iMod (slice_insert_full with "HQ1 Hbox") as (γ1 ?) "[#Hslice1 Hbox]"; first done.
iMod (slice_insert_full with "HQ2 Hbox") as (γ2) "(% & #Hslice2 & Hbox)"; first done. iMod (slice_insert_full with "HQ2 Hbox") as (γ2 ?) "[#Hslice2 Hbox]"; first done.
iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro. iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
{ by eapply lookup_insert_None. } { by eapply lookup_insert_None. }
{ by apply (lookup_insert_None (delete γ f) γ1 γ2 true). } { by apply (lookup_insert_None (delete γ f) γ1 γ2 true). }
iNext. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto]. iNext. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2). iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
- iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; try done. - iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; try done.
iMod (slice_insert_empty with "Hbox") as (γ1) "(% & #Hslice1 & Hbox)". iMod (slice_insert_empty with "Hbox") as (γ1 ?) "[#Hslice1 Hbox]".
iMod (slice_insert_empty with "Hbox") as (γ2) "(% & #Hslice2 & Hbox)". iMod (slice_insert_empty with "Hbox") as (γ2 ?) "[#Hslice2 Hbox]".
iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro. iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
{ by eapply lookup_insert_None. } { by eapply lookup_insert_None. }
{ by apply (lookup_insert_None (delete γ f) γ1 γ2 false). } { by apply (lookup_insert_None (delete γ f) γ1 γ2 false). }
...@@ -296,14 +296,14 @@ Proof. ...@@ -296,14 +296,14 @@ Proof.
iMod (slice_delete_full with "Hslice2 Hbox") as (P2) "(HQ2 & Heq2 & Hbox)"; first done. iMod (slice_delete_full with "Hslice2 Hbox") as (P2) "(HQ2 & Heq2 & Hbox)"; first done.
{ by simplify_map_eq. } { by simplify_map_eq. }
iMod (slice_insert_full _ _ _ _ (Q1 Q2)%I with "[$HQ1 $HQ2] Hbox") iMod (slice_insert_full _ _ _ _ (Q1 Q2)%I with "[$HQ1 $HQ2] Hbox")
as (γ) "(% & #Hslice & Hbox)"; first done. as (γ ?) "[#Hslice Hbox]"; first done.
iExists γ. iIntros "{$% $#} !>". iNext. iExists γ. iIntros "{$% $#} !>". iNext.
eapply internal_eq_rewrite_contractive; [by apply _| |by eauto]. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc. iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
- iMod (slice_delete_empty with "Hslice1 Hbox") as (P1) "(Heq1 & Hbox)"; try done. - iMod (slice_delete_empty with "Hslice1 Hbox") as (P1) "(Heq1 & Hbox)"; try done.
iMod (slice_delete_empty with "Hslice2 Hbox") as (P2) "(Heq2 & Hbox)"; first done. iMod (slice_delete_empty with "Hslice2 Hbox") as (P2) "(Heq2 & Hbox)"; first done.
{ by simplify_map_eq. } { by simplify_map_eq. }
iMod (slice_insert_empty with "Hbox") as (γ) "(% & #Hslice & Hbox)". iMod (slice_insert_empty with "Hbox") as (γ ?) "[#Hslice Hbox]".
iExists γ. iIntros "{$% $#} !>". iNext. iExists γ. iIntros "{$% $#} !>". iNext.
eapply internal_eq_rewrite_contractive; [by apply _| |by eauto]. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc. iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
......
...@@ -47,7 +47,7 @@ Lemma inv_alloc N E P : ▷ P ={E}=∗ inv N P. ...@@ -47,7 +47,7 @@ Lemma inv_alloc N E P : ▷ P ={E}=∗ inv N P.
Proof. Proof.
rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros "HP [Hw $]". rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros "HP [Hw $]".
iMod (ownI_alloc ( (N : coPset)) P with "[$HP $Hw]") iMod (ownI_alloc ( (N : coPset)) P with "[$HP $Hw]")
as (i) "(% & $ & ?)"; auto using fresh_inv_name. as (i ?) "[$ ?]"; auto using fresh_inv_name.
Qed. Qed.
Lemma inv_alloc_open N E P : Lemma inv_alloc_open N E P :
...@@ -55,7 +55,7 @@ Lemma inv_alloc_open N E P : ...@@ -55,7 +55,7 @@ Lemma inv_alloc_open N E P :
Proof. Proof.
rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros (Sub) "[Hw HE]". rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros (Sub) "[Hw HE]".
iMod (ownI_alloc_open ( (N : coPset)) P with "Hw") iMod (ownI_alloc_open ( (N : coPset)) P with "Hw")
as (i) "(% & Hw & #Hi & HD)"; auto using fresh_inv_name. as (i ?) "(Hw & #Hi & HD)"; auto using fresh_inv_name.
iAssert (ownE {[i]} ownE ( N {[i]}) ownE (E N))%I iAssert (ownE {[i]} ownE ( N {[i]}) ownE (E N))%I
with "[HE]" as "(HEi & HEN\i & HE\N)". with "[HE]" as "(HEi & HEN\i & HE\N)".
{ rewrite -?ownE_op; [|set_solver..]. { rewrite -?ownE_op; [|set_solver..].
......
...@@ -105,7 +105,7 @@ Lemma ownI_open i P : wsat ∗ ownI i P ∗ ownE {[i]} ⊢ wsat ∗ ▷ P ∗ ow ...@@ -105,7 +105,7 @@ Lemma ownI_open i P : wsat ∗ ownI i P ∗ ownE {[i]} ⊢ wsat ∗ ▷ P ∗ ow
Proof. Proof.
rewrite /ownI /wsat -!lock. rewrite /ownI /wsat -!lock.
iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[? HI]". iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[? HI]".
iDestruct (invariant_lookup I i P with "[$]") as (Q) "[% #HPQ]". iDestruct (invariant_lookup I i P with "[$]") as (Q ?) "#HPQ".
iDestruct (big_opM_delete _ _ i with "HI") as "[[[HQ $]|HiE'] HI]"; eauto. iDestruct (big_opM_delete _ _ i with "HI") as "[[[HQ $]|HiE'] HI]"; eauto.
- iSplitR "HQ"; last by iNext; iRewrite -"HPQ". - iSplitR "HQ"; last by iNext; iRewrite -"HPQ".
iExists I. iFrame "Hw". iApply (big_opM_delete _ _ i); eauto. iExists I. iFrame "Hw". iApply (big_opM_delete _ _ i); eauto.
...@@ -116,7 +116,7 @@ Lemma ownI_close i P : wsat ∗ ownI i P ∗ ▷ P ∗ ownD {[i]} ⊢ wsat ∗ o ...@@ -116,7 +116,7 @@ Lemma ownI_close i P : wsat ∗ ownI i P ∗ ▷ P ∗ ownD {[i]} ⊢ wsat ∗ o
Proof. Proof.
rewrite /ownI /wsat -!lock. rewrite /ownI /wsat -!lock.
iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[? HI]". iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[? HI]".
iDestruct (invariant_lookup with "[$]") as (Q) "[% #HPQ]". iDestruct (invariant_lookup with "[$]") as (Q ?) "#HPQ".
iDestruct (big_opM_delete _ _ i with "HI") as "[[[HQ ?]|$] HI]"; eauto. iDestruct (big_opM_delete _ _ i with "HI") as "[[[HQ ?]|$] HI]"; eauto.
- iDestruct (ownD_singleton_twice with "[$]") as %[]. - iDestruct (ownD_singleton_twice with "[$]") as %[].
- iExists I. iFrame "Hw". iApply (big_opM_delete _ _ i); eauto. - iExists I. iFrame "Hw". iApply (big_opM_delete _ _ i); eauto.
......
...@@ -67,7 +67,7 @@ Proof. ...@@ -67,7 +67,7 @@ Proof.
wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst. wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
- iMod ("Hclose" with "[Hl]"); [iNext; iExists _; iFrame; eauto|]. - iMod ("Hclose" with "[Hl]"); [iNext; iExists _; iFrame; eauto|].
iModIntro. wp_match. iApply ("IH" with "Hγ [HΦ]"). auto. iModIntro. wp_match. iApply ("IH" with "Hγ [HΦ]"). auto.
- iDestruct "Hinv" as (v') "[% [HΨ|Hγ']]"; simplify_eq/=. - iDestruct "Hinv" as (v' ->) "[HΨ|Hγ']".
+ iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists _; iFrame; eauto|]. + iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists _; iFrame; eauto|].
iModIntro. wp_match. by iApply "HΦ". iModIntro. wp_match. by iApply "HΦ".
+ iDestruct (own_valid_2 with "Hγ Hγ'") as %[]. + iDestruct (own_valid_2 with "Hγ Hγ'") as %[].
......
...@@ -60,7 +60,7 @@ Section proof. ...@@ -60,7 +60,7 @@ Section proof.
{{{ is_lock γ lk R }}} try_acquire lk {{{ is_lock γ lk R }}} try_acquire lk
{{{ b, RET #b; if b is true then locked γ R else True }}}. {{{ b, RET #b; if b is true then locked γ R else True }}}.
Proof. Proof.
iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l) "[% #?]"; subst. iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l ->) "#Hinv".
wp_rec. iInv N as ([]) "[Hl HR]" "Hclose". wp_rec. iInv N as ([]) "[Hl HR]" "Hclose".
- wp_cas_fail. iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto). - wp_cas_fail. iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
iModIntro. iApply ("HΦ" $! false). done. iModIntro. iApply ("HΦ" $! false). done.
...@@ -82,7 +82,7 @@ Section proof. ...@@ -82,7 +82,7 @@ Section proof.
{{{ is_lock γ lk R locked γ R }}} release lk {{{ RET #(); True }}}. {{{ is_lock γ lk R locked γ R }}} release lk {{{ RET #(); True }}}.
Proof. Proof.
iIntros (Φ) "(Hlock & Hlocked & HR) HΦ". iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
iDestruct "Hlock" as (l) "[% #?]"; subst. iDestruct "Hlock" as (l ->) "#Hinv".
rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose". rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
wp_store. iApply "HΦ". iApply "Hclose". iNext. iExists false. by iFrame. wp_store. iApply "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
Qed. Qed.
......
...@@ -86,7 +86,7 @@ Section proof. ...@@ -86,7 +86,7 @@ Section proof.
Lemma wait_loop_spec γ lk x R : Lemma wait_loop_spec γ lk x R :
{{{ is_lock γ lk R issued γ x }}} wait_loop #x lk {{{ RET #(); locked γ R }}}. {{{ is_lock γ lk R issued γ x }}} wait_loop #x lk {{{ RET #(); locked γ R }}}.
Proof. Proof.
iIntros (Φ) "[Hl Ht] HΦ". iDestruct "Hl" as (lo ln) "(% & #?)". iIntros (Φ) "[Hl Ht] HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
iLöb as "IH". wp_rec. subst. wp_let. wp_proj. wp_bind (! _)%E. iLöb as "IH". wp_rec. subst. wp_let. wp_proj. wp_bind (! _)%E.
iInv N as (o n) "(Hlo & Hln & Ha)" "Hclose". iInv N as (o n) "(Hlo & Hln & Ha)" "Hclose".
wp_load. destruct (decide (x = o)) as [->|Hneq]. wp_load. destruct (decide (x = o)) as [->|Hneq].
...@@ -108,7 +108,7 @@ Section proof. ...@@ -108,7 +108,7 @@ Section proof.
Lemma acquire_spec γ lk R : Lemma acquire_spec γ lk R :
{{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ R }}}. {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ R }}}.
Proof. Proof.
iIntros (ϕ) "Hl HΦ". iDestruct "Hl" as (lo ln) "[% #?]". iIntros (ϕ) "Hl HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
iLöb as "IH". wp_rec. wp_bind (! _)%E. simplify_eq/=. wp_proj. iLöb as "IH". wp_rec. wp_bind (! _)%E. simplify_eq/=. wp_proj.
iInv N as (o n) "[Hlo [Hln Ha]]" "Hclose". iInv N as (o n) "[Hlo [Hln Ha]]" "Hclose".
wp_load. iMod ("Hclose" with "[Hlo Hln Ha]") as "_". wp_load. iMod ("Hclose" with "[Hlo Hln Ha]") as "_".
...@@ -139,7 +139,7 @@ Section proof. ...@@ -139,7 +139,7 @@ Section proof.
Lemma release_spec γ lk R : Lemma release_spec γ lk R :
{{{ is_lock γ lk R locked γ R }}} release lk {{{ RET #(); True }}}. {{{ is_lock γ lk R locked γ R }}} release lk {{{ RET #(); True }}}.
Proof. Proof.
iIntros (Φ) "(Hl & Hγ & HR) HΦ". iDestruct "Hl" as (lo ln) "[% #?]"; subst. iIntros (Φ) "(Hl & Hγ & HR) HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
iDestruct "Hγ" as (o) "Hγo". iDestruct "Hγ" as (o) "Hγo".
wp_let. wp_proj. wp_proj. wp_bind (! _)%E. wp_let. wp_proj. wp_proj. wp_bind (! _)%E.
iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)" "Hclose". iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)" "Hclose".
......
...@@ -123,7 +123,7 @@ Lemma wptp_result n e1 t1 v2 t2 σ1 σ2 φ : ...@@ -123,7 +123,7 @@ Lemma wptp_result n e1 t1 v2 t2 σ1 σ2 φ :
Proof. Proof.
intros. rewrite wptp_steps //. intros. rewrite wptp_steps //.
rewrite (Nat_iter_S_r (S n)). apply bupd_iter_mono. rewrite (Nat_iter_S_r (S n)). apply bupd_iter_mono.
iDestruct 1 as (e2 t2') "(% & (Hw & HE & _) & H & _)"; simplify_eq. iDestruct 1 as (e2 t2' ?) "((Hw & HE & _) & H & _)"; simplify_eq.
iDestruct (wp_value_inv with "H") as "H". rewrite fupd_eq /fupd_def. iDestruct (wp_value_inv with "H") as "H". rewrite fupd_eq /fupd_def.
iMod ("H" with "[Hw HE]") as ">(_ & _ & $)"; iFrame; auto. iMod ("H" with "[Hw HE]") as ">(_ & _ & $)"; iFrame; auto.
Qed. Qed.
...@@ -143,7 +143,7 @@ Lemma wptp_safe n e1 e2 t1 t2 σ1 σ2 Φ : ...@@ -143,7 +143,7 @@ Lemma wptp_safe n e1 e2 t1 t2 σ1 σ2 Φ :
Nat.iter (S (S n)) (λ P, |==> P) is_Some (to_val e2) reducible e2 σ2. Nat.iter (S (S n)) (λ P, |==> P) is_Some (to_val e2) reducible e2 σ2.
Proof. Proof.
intros ? He2. rewrite wptp_steps //; rewrite (Nat_iter_S_r (S n)). apply bupd_iter_mono. intros ? He2. rewrite wptp_steps //; rewrite (Nat_iter_S_r (S n)). apply bupd_iter_mono.
iDestruct 1 as (e2' t2') "(% & Hw & H & Htp)"; simplify_eq. iDestruct 1 as (e2' t2' ?) "(Hw & H & Htp)"; simplify_eq.
apply elem_of_cons in He2 as [<-|?]; first (iApply wp_safe; by iFrame "Hw H"). apply elem_of_cons in He2 as [<-|?]; first (iApply wp_safe; by iFrame "Hw H").
iApply wp_safe. iFrame "Hw". by iApply (big_sepL_elem_of with "Htp"). iApply wp_safe. iFrame "Hw". by iApply (big_sepL_elem_of with "Htp").
Qed. Qed.
...@@ -155,8 +155,7 @@ Lemma wptp_invariance n e1 e2 t1 t2 σ1 σ2 φ Φ : ...@@ -155,8 +155,7 @@ Lemma wptp_invariance n e1 e2 t1 t2 σ1 σ2 φ Φ :
Proof. Proof.
intros ?. rewrite wptp_steps //. intros ?. rewrite wptp_steps //.
rewrite (Nat_iter_S_r (S n)) !bupd_iter_frame_l. apply bupd_iter_mono. rewrite (Nat_iter_S_r (S n)) !bupd_iter_frame_l. apply bupd_iter_mono.
iIntros "[Hback H]". iIntros "[Hback H]". iDestruct "H" as (e2' t2' ->) "[(Hw&HE&Hσ) _]".
iDestruct "H" as (e2' t2') "(% & (Hw&HE&Hσ) & _)"; subst.
rewrite fupd_eq. rewrite fupd_eq.
iMod ("Hback" with "Hσ [$Hw $HE]") as "> (_ & _ & $)"; auto. iMod ("Hback" with "Hσ [$Hw $HE]") as "> (_ & _ & $)"; auto.
Qed. Qed.
......
...@@ -89,7 +89,7 @@ Section lifting. ...@@ -89,7 +89,7 @@ Section lifting.
iMod "H" as (σ1) "[Hred _]"; iDestruct "Hred" as %Hred%reducible_not_val. iMod "H" as (σ1) "[Hred _]"; iDestruct "Hred" as %Hred%reducible_not_val.
move: Hred; by rewrite to_of_val. move: Hred; by rewrite to_of_val.
- iApply wp_lift_step; [done|]; iIntros (σ1) "Hσ". - iApply wp_lift_step; [done|]; iIntros (σ1) "Hσ".
iMod "H" as (σ1') "(% & >Hσf & H)". rewrite /ownP. iMod "H" as (σ1' ?) "[>Hσf H]". rewrite /ownP.
iDestruct (own_valid_2 with "Hσ Hσf") iDestruct (own_valid_2 with "Hσ Hσf")
as %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2. as %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
iModIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 efs Hstep). iModIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 efs Hstep).
...@@ -169,7 +169,7 @@ Section ectx_lifting. ...@@ -169,7 +169,7 @@ Section ectx_lifting.
WP e1 @ E {{ Φ }}. WP e1 @ E {{ Φ }}.
Proof. Proof.
iIntros "H". iApply (ownP_lift_step E); try done. iIntros "H". iApply (ownP_lift_step E); try done.
iMod "H" as (σ1) "(%&Hσ1&Hwp)". iModIntro. iExists σ1. iMod "H" as (σ1 ?) "[Hσ1 Hwp]". iModIntro. iExists σ1.
iSplit; first by eauto. iFrame. iNext. iIntros (e2 σ2 efs) "% ?". iSplit; first by eauto. iFrame. iNext. iIntros (e2 σ2 efs) "% ?".
iApply ("Hwp" with "[]"); eauto. iApply ("Hwp" with "[]"); eauto.
Qed. Qed.
......
...@@ -688,6 +688,19 @@ Proof. done. Qed. ...@@ -688,6 +688,19 @@ Proof. done. Qed.
Global Instance into_exist_pure {A} (φ : A Prop) : Global Instance into_exist_pure {A} (φ : A Prop) :
@IntoExist M A x, φ x (λ a, ⌜φ a)%I. @IntoExist M A x, φ x (λ a, ⌜φ a)%I.
Proof. by rewrite /IntoExist pure_exist. Qed. Proof. by rewrite /IntoExist pure_exist. Qed.
Global Instance into_exist_and_pure P Q φ :
IntoPureT P φ IntoExist (P Q) (λ _ : φ, Q).
Proof.
intros (φ'&->&?). rewrite /IntoExist (into_pure P).
apply pure_elim_l=> Hφ. by rewrite -(exist_intro Hφ).
Qed.
Global Instance into_exist_sep_pure P Q φ :
IntoPureT P φ IntoExist (P Q) (λ _ : φ, Q).
Proof.
intros (φ'&->&?). rewrite /IntoExist (into_pure P).
apply pure_elim_sep_l=> Hφ. by rewrite -(exist_intro Hφ).
Qed.
Global Instance into_exist_always {A} P (Φ : A uPred M) : Global Instance into_exist_always {A} P (Φ : A uPred M) :
IntoExist P Φ IntoExist ( P) (λ a, (Φ a))%I. IntoExist P Φ IntoExist ( P) (λ a, (Φ a))%I.
Proof. rewrite /IntoExist=> HP. by rewrite HP always_exist. Qed. Proof. rewrite /IntoExist=> HP. by rewrite HP always_exist. Qed.
......
...@@ -23,6 +23,33 @@ Class IntoPure {M} (P : uPred M) (φ : Prop) := into_pure : P ⊢ ⌜φ⌝. ...@@ -23,6 +23,33 @@ Class IntoPure {M} (P : uPred M) (φ : Prop) := into_pure : P ⊢ ⌜φ⌝.
Arguments into_pure {_} _ _ {_}. Arguments into_pure {_} _ _ {_}.
Hint Mode IntoPure + ! - : typeclass_instances. Hint Mode IntoPure + ! - : typeclass_instances.
(* [IntoPureT] is a variant of [IntoPure] with the argument in [Type] to avoid
some shortcoming of unification in Coq's type class search. An example where we
use this workaround is to repair the following instance:
Global Instance into_exist_and_pure P Q (φ : Prop) :
IntoPure P φ → IntoExist (P ∧ Q) (λ _ : φ, Q).
Coq is unable to use this instance: [class_apply] -- which is used by type class
search -- fails with the error that it cannot unify [Prop] and [Type]. This is
probably caused because [class_apply] uses an ancient unification algorith. The
[refine] tactic -- which uses a better unification algorithm -- succeeds to
apply the above instance.
Since we do not want to define [Hint Extern] declarations using [refine] for
any instance like [into_exist_and_pure], we factor this out in the class
[IntoPureT]. This way, we only have to declare a [Hint Extern] using [refine]
once, and use [IntoPureT] in any instance like [into_exist_and_pure].
TODO: Report this as a Coq bug, or wait for https://github.com/coq/coq/pull/991
to be finished and merged someday. *)
Class IntoPureT {M} (P : uPred M) (φ : Type) :=
into_pureT : ψ : Prop, φ = ψ IntoPure P ψ.
Lemma into_pureT_hint {M} (P : uPred M) (φ : Prop) : IntoPure P φ IntoPureT P φ.
Proof. by exists φ. Qed.
Hint Extern 0 (IntoPureT _ _) =>
notypeclasses refine (into_pureT_hint _ _ _) : typeclass_instances.
Class FromPure {M} (P : uPred M) (φ : Prop) := from_pure : ⌜φ⌝ P. Class FromPure {M} (P : uPred M) (φ : Prop) := from_pure : ⌜φ⌝ P.
Arguments from_pure {_} _ _ {_}. Arguments from_pure {_} _ _ {_}.
Hint Mode FromPure + ! - : typeclass_instances. Hint Mode FromPure + ! - : typeclass_instances.
......
...@@ -35,7 +35,7 @@ Proof. ...@@ -35,7 +35,7 @@ Proof.
iLöb as "IH" forall (hd acc xs ys Φ). wp_rec. wp_let. iLöb as "IH" forall (hd acc xs ys Φ). wp_rec. wp_let.
destruct xs as [|x xs]; iSimplifyEq. destruct xs as [|x xs]; iSimplifyEq.
- wp_match. by iApply "HΦ". - wp_match. by iApply "HΦ".
- iDestruct "Hxs" as (l hd') "(% & Hx & Hxs)"; iSimplifyEq. - iDestruct "Hxs" as (l hd' ->) "[Hx Hxs]".
wp_match. wp_load. wp_proj. wp_let. wp_load. wp_proj. wp_let. wp_store. wp_match. wp_load. wp_proj. wp_let. wp_load. wp_proj. wp_let. wp_store.
iApply ("IH" $! hd' (SOMEV #l) xs (x :: ys) with "Hxs [Hx Hys]"); simpl. iApply ("IH" $! hd' (SOMEV #l) xs (x :: ys) with "Hxs [Hx Hys]"); simpl.
{ iExists l, acc; by iFrame. } { iExists l, acc; by iFrame. }
......
...@@ -45,7 +45,7 @@ Proof. ...@@ -45,7 +45,7 @@ Proof.
- iDestruct "Ht" as "%"; subst. - iDestruct "Ht" as "%"; subst.
wp_match. wp_load. wp_op. wp_store. wp_match. wp_load. wp_op. wp_store.
by iApply ("HΦ" with "[$Hl]"). by iApply ("HΦ" with "[$Hl]").
- iDestruct "Ht" as (ll lr vl vr) "(% & Hll & Htl & Hlr & Htr)"; subst. - iDestruct "Ht" as (ll lr vl vr ->) "(Hll & Htl & Hlr & Htr)".
wp_match. wp_proj. wp_load. wp_match. wp_proj. wp_load.
wp_apply ("IH" with "Hl Htl"). iIntros "[Hl Htl]". wp_apply ("IH" with "Hl Htl"). iIntros "[Hl Htl]".
wp_seq. wp_proj. wp_load. wp_seq. wp_proj. wp_load.
......
Markdown is supported
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