Skip to content
Snippets Groups Projects
Commit 91496e50 authored by Ralf Jung's avatar Ralf Jung
Browse files

update dependencies; fix for wp_finish changes

parent 4e300200
No related branches found
No related tags found
No related merge requests found
Pipeline #39207 passed
Stage: build
    Hide whitespace changes
    Inline Side-by-side
    Showing
    with 30 additions and 30 deletions
    opam
    + 1
    − 1
    View file @ 91496e50
    ...@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"] ...@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
    install: [make "install"] install: [make "install"]
    remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
    depends: [ depends: [
    "coq-iris-heap-lang" { (= "dev.2020-11-26.2.03b317f4") | (= "dev") } "coq-iris-heap-lang" { (= "dev.2020-12-04.7.68955c65") | (= "dev") }
    ] ]
    theories/channel/channel.v
    + 5
    − 5
    View file @ 91496e50
    ...@@ -284,27 +284,27 @@ Section channel. ...@@ -284,27 +284,27 @@ Section channel.
    - wp_apply (lisnil_spec with "Hr"); iIntros "Hr". - wp_apply (lisnil_spec with "Hr"); iIntros "Hr".
    destruct vsr as [|vr vsr]; wp_pures. destruct vsr as [|vr vsr]; wp_pures.
    { wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|]. { wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
    iIntros "_". wp_pures. iApply "HΦ". iLeft. iSplit; [done|]. iIntros "_". wp_pures. iModIntro. iApply "HΦ". iLeft. iSplit; [done|].
    iExists γ, Left, l, r, lk. eauto 10 with iFrame. } iExists γ, Left, l, r, lk. eauto 10 with iFrame. }
    wp_apply (lpop_spec with "Hr"); iIntros (v') "[% Hr]"; simplify_eq/=. wp_apply (lpop_spec with "Hr"); iIntros (v') "[% Hr]"; simplify_eq/=.
    iMod (iProto_recv_l with "Hctx H") as (q) "(Hctx & H & Hm)". wp_pures. iMod (iProto_recv_l with "Hctx H") as (q) "(Hctx & H & Hm)". wp_pures.
    rewrite iMsg_base_eq. rewrite iMsg_base_eq.
    iDestruct (iMsg_texist_exist with "Hm") as (x <-) "[Hp HP]". iDestruct (iMsg_texist_exist with "Hm") as (x <-) "[Hp HP]".
    wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|]. wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
    iIntros "_". wp_pures. iApply "HΦ". iRight. iExists x. iSplit; [done|]. iIntros "_". wp_pures. iModIntro. iApply "HΦ". iRight. iExists x. iSplit; [done|].
    iFrame "HP". iExists γ, Left, l, r, lk. iSplit; [done|]. iFrame "Hlk". iFrame "HP". iExists γ, Left, l, r, lk. iSplit; [done|]. iFrame "Hlk".
    by iRewrite "Hp". by iRewrite "Hp".
    - wp_apply (lisnil_spec with "Hl"); iIntros "Hl". - wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
    destruct vsl as [|vl vsl]; wp_pures. destruct vsl as [|vl vsl]; wp_pures.
    { wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|]. { wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
    iIntros "_". wp_pures. iApply "HΦ". iLeft. iSplit; [done|]. iIntros "_". wp_pures. iModIntro. iApply "HΦ". iLeft. iSplit; [done|].
    iExists γ, Right, l, r, lk. eauto 10 with iFrame. } iExists γ, Right, l, r, lk. eauto 10 with iFrame. }
    wp_apply (lpop_spec with "Hl"); iIntros (v') "[% Hl]"; simplify_eq/=. wp_apply (lpop_spec with "Hl"); iIntros (v') "[% Hl]"; simplify_eq/=.
    iMod (iProto_recv_r with "Hctx H") as (q) "(Hctx & H & Hm)". wp_pures. iMod (iProto_recv_r with "Hctx H") as (q) "(Hctx & H & Hm)". wp_pures.
    rewrite iMsg_base_eq. rewrite iMsg_base_eq.
    iDestruct (iMsg_texist_exist with "Hm") as (x <-) "[Hp HP]". iDestruct (iMsg_texist_exist with "Hm") as (x <-) "[Hp HP]".
    wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|]. wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
    iIntros "_". wp_pures. iApply "HΦ". iRight. iExists x. iSplit; [done|]. iIntros "_". wp_pures. iModIntro. iApply "HΦ". iRight. iExists x. iSplit; [done|].
    iFrame "HP". iExists γ, Right, l, r, lk. iSplit; [done|]. iFrame "Hlk". iFrame "HP". iExists γ, Right, l, r, lk. iSplit; [done|]. iFrame "Hlk".
    by iRewrite "Hp". by iRewrite "Hp".
    Qed. Qed.
    ...@@ -317,7 +317,7 @@ Section channel. ...@@ -317,7 +317,7 @@ Section channel.
    iIntros (Φ) "Hc HΦ". iLöb as "IH". wp_lam. iIntros (Φ) "Hc HΦ". iLöb as "IH". wp_lam.
    wp_apply (try_recv_spec with "Hc"); iIntros (w) "[[-> H]|H]". wp_apply (try_recv_spec with "Hc"); iIntros (w) "[[-> H]|H]".
    { wp_pures. by iApply ("IH" with "[$]"). } { wp_pures. by iApply ("IH" with "[$]"). }
    iDestruct "H" as (x ->) "[Hc HP]". wp_pures. iApply "HΦ". iFrame. iDestruct "H" as (x ->) "[Hc HP]". wp_pures. iApply "HΦ". by iFrame.
    Qed. Qed.
    (** ** Specifications for choice *) (** ** Specifications for choice *)
    ......
    theories/examples/sort.v
    + 2
    − 2
    View file @ 91496e50
    ...@@ -70,7 +70,7 @@ Section sort. ...@@ -70,7 +70,7 @@ Section sort.
    iApply "HΨ". iFrame. by rewrite list_merge_nil_l. } iApply "HΨ". iFrame. by rewrite list_merge_nil_l. }
    wp_apply (lisnil_spec with "Hl2"); iIntros "Hl2". wp_apply (lisnil_spec with "Hl2"); iIntros "Hl2".
    destruct xs2 as [|x2 xs2]; wp_pures. destruct xs2 as [|x2 xs2]; wp_pures.
    { iApply "HΨ". iFrame. } { iApply "HΨ". by iFrame. }
    wp_apply (lhead_spec_aux with "Hl1"); iIntros (v1 l1') "[HIx1 Hl1]". wp_apply (lhead_spec_aux with "Hl1"); iIntros (v1 l1') "[HIx1 Hl1]".
    wp_apply (lhead_spec_aux with "Hl2"); iIntros (v2 l2') "[HIx2 Hl2]". wp_apply (lhead_spec_aux with "Hl2"); iIntros (v2 l2') "[HIx2 Hl2]".
    wp_apply ("Hcmp" with "[$HIx1 $HIx2]"); iIntros "[HIx1 HIx2] /=". wp_apply ("Hcmp" with "[$HIx1 $HIx2]"); iIntros "[HIx1 HIx2] /=".
    ...@@ -147,6 +147,6 @@ Section sort. ...@@ -147,6 +147,6 @@ Section sort.
    wp_send with "[$Hcmp]". wp_send with "[$Hcmp]".
    wp_send with "[$Hl]". wp_send with "[$Hl]".
    wp_recv (ys) as "(Hsorted & Hperm & Hl)". wp_recv (ys) as "(Hsorted & Hperm & Hl)".
    iApply "HΦ"; iFrame. iApply "HΦ"; by iFrame.
    Qed. Qed.
    End sort. End sort.
    theories/examples/sort_fg.v
    + 2
    − 2
    View file @ 91496e50
    ...@@ -159,7 +159,7 @@ Section sort_fg. ...@@ -159,7 +159,7 @@ Section sort_fg.
    inversion 1; discriminate_list || simplify_list_eq. by constructor. inversion 1; discriminate_list || simplify_list_eq. by constructor.
    - wp_select with "[]". - wp_select with "[]".
    { by rewrite /= Hys Hxs Hys'. } { by rewrite /= Hys Hxs Hys'. }
    iApply "HΨ". iFrame. iApply "HΨ". by iFrame.
    Qed. Qed.
    Lemma sort_service_fg_merge_spec cmp c p c1 c2 xs ys xs1 xs2 y1 w1 ys1 ys2 : Lemma sort_service_fg_merge_spec cmp c p c1 c2 xs ys xs1 xs2 y1 w1 ys1 ys2 :
    ...@@ -249,7 +249,7 @@ Section sort_fg. ...@@ -249,7 +249,7 @@ Section sort_fg.
    iIntros (Φ) "[Hl Hc] HΦ". iIntros (Φ) "[Hl Hc] HΦ".
    iInduction xs as [|x xs] "IH" forall (xs'). iInduction xs as [|x xs] "IH" forall (xs').
    { wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl"; wp_pures. { wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl"; wp_pures.
    iApply "HΦ". rewrite right_id_L. iFrame. } iApply "HΦ". rewrite right_id_L. by iFrame. }
    wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl". wp_select. wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl". wp_select.
    wp_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]". wp_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
    wp_send with "[$HIx]". wp_apply ("IH" with "Hl Hc"). by rewrite -assoc_L. wp_send with "[$HIx]". wp_apply ("IH" with "Hl Hc"). by rewrite -assoc_L.
    ......
    theories/examples/swap_mapper.v
    + 1
    − 1
    View file @ 91496e50
    ...@@ -221,7 +221,7 @@ Section with_Σ. ...@@ -221,7 +221,7 @@ Section with_Σ.
    iIntros (Φ) "[Hl Hc] HΦ". iIntros (Φ) "[Hl Hc] HΦ".
    iInduction xs as [|x xs] "IH" forall (xs'). iInduction xs as [|x xs] "IH" forall (xs').
    { wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl"; wp_pures. { wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl"; wp_pures.
    iApply "HΦ". iFrame. } iApply "HΦ". by iFrame. }
    wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl". wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
    wp_send with "[//]". wp_send with "[//]".
    wp_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]". wp_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
    ......
    theories/logrel/examples/compute_client_list.v
    + 1
    − 1
    View file @ 91496e50
    ...@@ -187,7 +187,7 @@ Section compute_example. ...@@ -187,7 +187,7 @@ Section compute_example.
    iExists n, false. iExists n, false.
    rewrite lookup_total_insert -lsty_car_app lty_app_end_l lty_app_end_r. rewrite lookup_total_insert -lsty_car_app lty_app_end_l lty_app_end_r.
    iFrame "Hf Hcounter Hc". } iFrame "Hf Hcounter Hc". }
    iIntros "_". wp_pures. iApply "HΦ". iFrame "Hl Hlk Hsf". } iIntros "_". wp_pures. iApply "HΦ". by iFrame "Hl Hlk". }
    wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl". wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
    wp_apply (acquire_spec with "Hlk"). wp_apply (acquire_spec with "Hlk").
    iIntros "[Hlocked HI]". iIntros "[Hlocked HI]".
    ......
    theories/logrel/examples/mapper_list.v
    + 2
    − 2
    View file @ 91496e50
    ...@@ -245,7 +245,7 @@ Section mapper_example. ...@@ -245,7 +245,7 @@ Section mapper_example.
    iIntros (Φ) "[Hl Hc] HΦ". iIntros (Φ) "[Hl Hc] HΦ".
    iInduction xs as [|x xs] "IH". iInduction xs as [|x xs] "IH".
    { wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl"; wp_pures. { wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl"; wp_pures.
    iApply "HΦ". iFrame. } iApply "HΦ". by iFrame. }
    wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl". wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
    rewrite /select. rewrite /select.
    wp_send with "[]"; first by eauto. wp_send with "[]"; first by eauto.
    ...@@ -268,7 +268,7 @@ Section mapper_example. ...@@ -268,7 +268,7 @@ Section mapper_example.
    iIntros (Φ) "[Hl Hc] HΦ". iIntros (Φ) "[Hl Hc] HΦ".
    iInduction xs as [|x xs] "IH" forall (n). iInduction xs as [|x xs] "IH" forall (n).
    { wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl"; wp_pures. { wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl"; wp_pures.
    iApply "HΦ". iFrame. } iApply "HΦ". by iFrame. }
    wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl". wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
    simpl. simpl.
    iDestruct (iProto_mapsto_le c with "Hc []") as "Hc". iDestruct (iProto_mapsto_le c with "Hc []") as "Hc".
    ......
    theories/logrel/examples/par_recv.v
    + 4
    − 4
    View file @ 91496e50
    ...@@ -163,7 +163,7 @@ Section double_fc. ...@@ -163,7 +163,7 @@ Section double_fc.
    as "[Hγ1a Hγ1b]"; [by apply cmra_update_exclusive|]. as "[Hγ1a Hγ1b]"; [by apply cmra_update_exclusive|].
    wp_apply (release_spec with "[$Hlock $Hlocked Hγ1a Hc]"). wp_apply (release_spec with "[$Hlock $Hlocked Hγ1a Hc]").
    { iRight. iLeft. iExists true, v. iFrame. } { iRight. iLeft. iExists true, v. iFrame. }
    iIntros "_". wp_pures. iLeft. iFrame. iIntros "_". wp_pures. iLeft. by iFrame.
    + iDestruct "Hc" as ([] v) "[Hγ2 Hc]". + iDestruct "Hc" as ([] v) "[Hγ2 Hc]".
    { by iDestruct (own_valid_2 with "Hγ1 Hγ2") as %[]. } { by iDestruct (own_valid_2 with "Hγ1 Hγ2") as %[]. }
    wp_recv (v') as "HP". wp_pures. wp_recv (v') as "HP". wp_pures.
    ...@@ -173,7 +173,7 @@ Section double_fc. ...@@ -173,7 +173,7 @@ Section double_fc.
    iDestruct "Hγ2" as "[Hγ2a Hγ2b]". iDestruct "Hγ2" as "[Hγ2a Hγ2b]".
    wp_apply (release_spec with "[$Hlock $Hlocked Hγ1a Hγ2a Hc]"). wp_apply (release_spec with "[$Hlock $Hlocked Hγ1a Hγ2a Hc]").
    { do 2 iRight. iExists v', v. iFrame. } { do 2 iRight. iExists v', v. iFrame. }
    iIntros "_". wp_pures. iRight. iExists v. iFrame. iIntros "_". wp_pures. iRight. iExists v. by iFrame.
    + iDestruct "Hc" as (v v') "[Hγ1' _]". + iDestruct "Hc" as (v v') "[Hγ1' _]".
    by iDestruct (own_valid_2 with "Hγ1 Hγ1'") as %[]. by iDestruct (own_valid_2 with "Hγ1 Hγ1'") as %[].
    - (* Acquire lock *) - (* Acquire lock *)
    ...@@ -185,7 +185,7 @@ Section double_fc. ...@@ -185,7 +185,7 @@ Section double_fc.
    as "[Hγ2a Hγ2b]"; [by apply cmra_update_exclusive|]. as "[Hγ2a Hγ2b]"; [by apply cmra_update_exclusive|].
    wp_apply (release_spec with "[$Hlock $Hlocked Hγ2a Hc]"). wp_apply (release_spec with "[$Hlock $Hlocked Hγ2a Hc]").
    { iRight. iLeft. iExists false, v. iFrame. } { iRight. iLeft. iExists false, v. iFrame. }
    iIntros "_". wp_pures. iLeft. iFrame. iIntros "_". wp_pures. iLeft. by iFrame.
    + iDestruct "Hc" as ([] v) "[Hγ1 Hc]"; last first. + iDestruct "Hc" as ([] v) "[Hγ1 Hc]"; last first.
    { by iDestruct (own_valid_2 with "Hγ1 Hγ2") as %[]. } { by iDestruct (own_valid_2 with "Hγ1 Hγ2") as %[]. }
    wp_recv (v') as "HP". wp_pures. wp_recv (v') as "HP". wp_pures.
    ...@@ -195,7 +195,7 @@ Section double_fc. ...@@ -195,7 +195,7 @@ Section double_fc.
    iDestruct "Hγ1" as "[Hγ1a Hγ1b]". iDestruct "Hγ1" as "[Hγ1a Hγ1b]".
    wp_apply (release_spec with "[$Hlock $Hlocked Hγ1a Hγ2a Hc]"). wp_apply (release_spec with "[$Hlock $Hlocked Hγ1a Hγ2a Hc]").
    { do 2 iRight. iExists v, v'. iFrame. } { do 2 iRight. iExists v, v'. iFrame. }
    iIntros "_". wp_pures. iRight. iExists v. iFrame. iIntros "_". wp_pures. iRight. iExists v. by iFrame.
    + iDestruct "Hc" as (v v') "(_ & Hγ2' & _)". + iDestruct "Hc" as (v v') "(_ & Hγ2' & _)".
    by iDestruct (own_valid_2 with "Hγ2 Hγ2'") as %[]. by iDestruct (own_valid_2 with "Hγ2 Hγ2'") as %[].
    - iIntros (v1 v2) "[[[H1 Hγ]|H1] [[H2 Hγ']|H2]] !>". - iIntros (v1 v2) "[[[H1 Hγ]|H1] [[H2 Hγ']|H2]] !>".
    ......
    theories/logrel/lib/mutex.v
    + 1
    − 1
    View file @ 91496e50
    ...@@ -125,7 +125,7 @@ Section rules. ...@@ -125,7 +125,7 @@ Section rules.
    wp_apply (acquire_spec with "Hlock"); iIntros "[Hlocked Hinner]". wp_apply (acquire_spec with "Hlock"); iIntros "[Hlocked Hinner]".
    iDestruct "Hinner" as (v) "[Hl HA]". iDestruct "Hinner" as (v) "[Hl HA]".
    wp_load. iFrame "HA". iApply ctx_ltyped_cons. wp_load. iFrame "HA". iApply ctx_ltyped_cons.
    iFrame "HΓ". iExists _; iSplit; [done|]. iExists γ, l, lk, v. auto with iFrame. iFrame "HΓ". iModIntro. iExists _; iSplit; [done|]. iExists γ, l, lk, v. auto with iFrame.
    Qed. Qed.
    Lemma ltyped_mutex_release Γ Γ' (x : string) e A : Lemma ltyped_mutex_release Γ Γ' (x : string) e A :
    ......
    theories/logrel/session_typing_rules.v
    + 2
    − 2
    View file @ 91496e50
    ...@@ -98,7 +98,7 @@ Section session_typing_rules. ...@@ -98,7 +98,7 @@ Section session_typing_rules.
    iIntros (HΓx%ctx_lookup_perm Hin); iIntros "!>" (vs) "HΓ /=". iIntros (HΓx%ctx_lookup_perm Hin); iIntros "!>" (vs) "HΓ /=".
    rewrite {1}HΓx /=. rewrite {1}HΓx /=.
    iDestruct (ctx_ltyped_cons with "HΓ") as (c Hvs) "[Hc HΓ]". rewrite Hvs. iDestruct (ctx_ltyped_cons with "HΓ") as (c Hvs) "[Hc HΓ]". rewrite Hvs.
    rewrite /select. wp_send with "[]"; [by eauto|]. iSplit; [done|]. rewrite /select. wp_send with "[]"; [by eauto|]. iModIntro. iSplit; [done|].
    iDestruct (ctx_ltyped_insert _ _ x (chan _) with "[Hc //] HΓ") as "HΓ' /=". iDestruct (ctx_ltyped_insert _ _ x (chan _) with "[Hc //] HΓ") as "HΓ' /=".
    by rewrite insert_id // lookup_total_alt Hin. by rewrite insert_id // lookup_total_alt Hin.
    Qed. Qed.
    ...@@ -116,7 +116,7 @@ Section session_typing_rules. ...@@ -116,7 +116,7 @@ Section session_typing_rules.
    WP subst_map ws (switch_lams y i (S (length As)) e) WP subst_map ws (switch_lams y i (S (length As)) e)
    {{ ltty_car (lty_arr_list (A :: As) B) }}. {{ ltty_car (lty_arr_list (A :: As) B) }}.
    Proof. Proof.
    iIntros "H". wp_pures. iIntros (v) "HA". iIntros "H". wp_pures. iIntros "!>" (v) "HA".
    iDestruct ("H" with "HA") as "H". iDestruct ("H" with "HA") as "H".
    rewrite subst_map_insert. rewrite subst_map_insert.
    wp_apply "H". wp_apply "H".
    ......
    theories/logrel/term_typing_rules.v
    + 7
    − 7
    View file @ 91496e50
    ...@@ -136,7 +136,7 @@ Section term_typing_rules. ...@@ -136,7 +136,7 @@ Section term_typing_rules.
    Proof. Proof.
    iIntros "#He" (vs) "!> HΓ /=". wp_pures. iIntros "#He" (vs) "!> HΓ /=". wp_pures.
    iDestruct (ctx_ltyped_app with "HΓ") as "[HΓ1 $]". iDestruct (ctx_ltyped_app with "HΓ") as "[HΓ1 $]".
    iIntros (v) "HA1". wp_pures. iIntros "!>" (v) "HA1". wp_pures.
    iDestruct ("He" $! (binder_insert x v vs) with "[HA1 HΓ1]") as "He'". iDestruct ("He" $! (binder_insert x v vs) with "[HA1 HΓ1]") as "He'".
    { by iApply (ctx_ltyped_insert' with "HA1"). } { by iApply (ctx_ltyped_insert' with "HA1"). }
    rewrite subst_map_binder_insert. rewrite subst_map_binder_insert.
    ...@@ -172,7 +172,7 @@ Section term_typing_rules. ...@@ -172,7 +172,7 @@ Section term_typing_rules.
    iApply (big_sepL_impl with "HΓ1"). iIntros "!>" (k [y B] _) "/=". iApply (big_sepL_impl with "HΓ1"). iIntros "!>" (k [y B] _) "/=".
    iDestruct 1 as (v ?) "HB". iExists v. iSplit; [by auto|]. iDestruct 1 as (v ?) "HB". iExists v. iSplit; [by auto|].
    by iDestruct (coreP_intro with "HB") as "{HB} #HB". } by iDestruct (coreP_intro with "HB") as "{HB} #HB". }
    iLöb as "IH". iModIntro. iLöb as "IH".
    iIntros (v) "!> HA1". wp_pures. set (r := RecV f x _). iIntros (v) "!> HA1". wp_pures. set (r := RecV f x _).
    iDestruct ("He" $! (binder_insert f r (binder_insert x v vs)) iDestruct ("He" $! (binder_insert f r (binder_insert x v vs))
    with "[HΓ1 HA1]") as "He'". with "[HΓ1 HA1]") as "He'".
    ...@@ -245,7 +245,7 @@ Section term_typing_rules. ...@@ -245,7 +245,7 @@ Section term_typing_rules.
    iDestruct (ctx_ltyped_cons with "HΓ") as (v Hvs) "[HA HΓ]"; rewrite Hvs. iDestruct (ctx_ltyped_cons with "HΓ") as (v Hvs) "[HA HΓ]"; rewrite Hvs.
    iDestruct "HA" as (v1 v2 ->) "[HA1 HA2]". wp_pures. iDestruct "HA" as (v1 v2 ->) "[HA1 HA2]". wp_pures.
    iAssert (ltty_car (copy- A1) v1)%lty as "#HA1m"; [by iApply coreP_intro|]. iAssert (ltty_car (copy- A1) v1)%lty as "#HA1m"; [by iApply coreP_intro|].
    iFrame "HA1". iApply ctx_ltyped_cons. iExists _; iSplit; [done|]; iFrame "HΓ". iFrame "HA1". iApply ctx_ltyped_cons. iModIntro. iExists _; iSplit; [done|]; iFrame "HΓ".
    iExists v1, v2. eauto with iFrame. iExists v1, v2. eauto with iFrame.
    Qed. Qed.
    ...@@ -257,7 +257,7 @@ Section term_typing_rules. ...@@ -257,7 +257,7 @@ Section term_typing_rules.
    iDestruct (ctx_ltyped_cons with "HΓ") as (v Hvs) "[HA HΓ]"; rewrite Hvs. iDestruct (ctx_ltyped_cons with "HΓ") as (v Hvs) "[HA HΓ]"; rewrite Hvs.
    iDestruct "HA" as (v1 v2 ->) "[HA1 HA2]". wp_pures. iDestruct "HA" as (v1 v2 ->) "[HA1 HA2]". wp_pures.
    iAssert (ltty_car (copy- A2) v2)%lty as "#HA2m"; [by iApply coreP_intro|]. iAssert (ltty_car (copy- A2) v2)%lty as "#HA2m"; [by iApply coreP_intro|].
    iFrame "HA2". iApply ctx_ltyped_cons. iExists _; iSplit; [done|]; iFrame "HΓ". iFrame "HA2". iApply ctx_ltyped_cons. iModIntro. iExists _; iSplit; [done|]; iFrame "HΓ".
    iExists v1, v2. eauto with iFrame. iExists v1, v2. eauto with iFrame.
    Qed. Qed.
    ...@@ -304,7 +304,7 @@ Section term_typing_rules. ...@@ -304,7 +304,7 @@ Section term_typing_rules.
    Proof. Proof.
    iIntros "#He" (vs) "!> HΓ /=". wp_pures. iIntros "#He" (vs) "!> HΓ /=". wp_pures.
    iDestruct (ctx_ltyped_app with "HΓ") as "[HΓ1 $]". iDestruct (ctx_ltyped_app with "HΓ") as "[HΓ1 $]".
    iIntros (M) "/=". wp_pures. iIntros "!>" (M) "/=". wp_pures.
    iApply (wp_wand with "(He HΓ1)"). iIntros (v) "[$ _]". iApply (wp_wand with "(He HΓ1)"). iIntros (v) "[$ _]".
    Qed. Qed.
    ...@@ -369,7 +369,7 @@ Section term_typing_rules. ...@@ -369,7 +369,7 @@ Section term_typing_rules.
    iDestruct (ctx_ltyped_cons with "HΓ") as (v Hvs) "[HA HΓ]"; rewrite Hvs. iDestruct (ctx_ltyped_cons with "HΓ") as (v Hvs) "[HA HΓ]"; rewrite Hvs.
    iDestruct "HA" as (l w ->) "[? HA]". wp_load. iDestruct "HA" as (l w ->) "[? HA]". wp_load.
    iAssert (ltty_car (copy- A) w)%lty as "#HAm"; [by iApply coreP_intro|]. iAssert (ltty_car (copy- A) w)%lty as "#HAm"; [by iApply coreP_intro|].
    iFrame "HA". iApply ctx_ltyped_cons. iExists _; iSplit; [done|]; iFrame "HΓ". iFrame "HA". iApply ctx_ltyped_cons. iModIntro. iExists _; iSplit; [done|]; iFrame "HΓ".
    iExists l, w. eauto with iFrame. iExists l, w. eauto with iFrame.
    Qed. Qed.
    ...@@ -382,7 +382,7 @@ Section term_typing_rules. ...@@ -382,7 +382,7 @@ Section term_typing_rules.
    wp_apply (wp_wand with "(He HΓ)"). iIntros (v) "[HB HΓ']". wp_apply (wp_wand with "(He HΓ)"). iIntros (v) "[HB HΓ']".
    rewrite {2}HΓx /=. rewrite {2}HΓx /=.
    iDestruct (ctx_ltyped_cons with "HΓ'") as (vl Hvs) "[HA HΓ']"; rewrite Hvs. iDestruct (ctx_ltyped_cons with "HΓ'") as (vl Hvs) "[HA HΓ']"; rewrite Hvs.
    iDestruct "HA" as (l w ->) "[? HA]". wp_store. iSplit; [done|]. iDestruct "HA" as (l w ->) "[? HA]". wp_store. iModIntro. iSplit; [done|].
    iApply ctx_ltyped_cons. iExists _; iSplit; [done|]; iFrame "HΓ'". iApply ctx_ltyped_cons. iExists _; iSplit; [done|]; iFrame "HΓ'".
    iExists l, v. eauto with iFrame. iExists l, v. eauto with iFrame.
    Qed. Qed.
    ......
    theories/utils/llist.v
    + 2
    − 2
    View file @ 91496e50
    ...@@ -237,8 +237,8 @@ Proof. ...@@ -237,8 +237,8 @@ Proof.
    iIntros (Φ) "Hll HΦ". iIntros (Φ) "Hll HΦ".
    iInduction xs as [|x xs] "IH" forall (l n Φ); simpl; wp_rec; wp_pures. iInduction xs as [|x xs] "IH" forall (l n Φ); simpl; wp_rec; wp_pures.
    - destruct n as [|n]; simpl; wp_pures. - destruct n as [|n]; simpl; wp_pures.
    + wp_load. wp_alloc k. wp_store. iApply "HΦ"; iFrame. + wp_load. wp_alloc k. wp_store. iApply "HΦ"; by iFrame.
    + wp_load. wp_alloc k. iApply "HΦ"; iFrame. + wp_load. wp_alloc k. iApply "HΦ"; by iFrame.
    - iDestruct "Hll" as (v l') "(HIx & Hl & Hll)". destruct n as [|n]; simpl; wp_pures. - iDestruct "Hll" as (v l') "(HIx & Hl & Hll)". destruct n as [|n]; simpl; wp_pures.
    + wp_load. wp_alloc k. wp_store. iApply "HΦ"; eauto with iFrame. + wp_load. wp_alloc k. wp_store. iApply "HΦ"; eauto with iFrame.
    + wp_load; wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ. + wp_load; wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
    ......
    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