diff --git a/exercises/link_value_invs.v b/exercises/link_value_invs.v new file mode 100644 index 0000000000000000000000000000000000000000..d462cb3e222b0812ac1e6ce2429c83841856f164 --- /dev/null +++ b/exercises/link_value_invs.v @@ -0,0 +1,86 @@ +From iris.algebra Require Import auth frac_auth excl list. +From iris.base_logic.lib Require Import invariants. +From iris.heap_lang Require Import lib.par proofmode notation lang. + +Section LV_Invs. + Context `{!heapG Σ, !spawnG Σ, !inG Σ my_auth_cmra, !inG Σ my_camera}. + + Context (P : Z → iProp Σ). + + Fixpoint link_inv' (L: list (loc * Z)) (next_link: base_lit): iProp Σ := + (match L with + | [] => True + | [(h, _)] => h ↦ #next_link + | (h, _) :: ((l, _) :: _) as L' => h ↦ #l ∗ link_inv' L' next_link + end)%I. + + Definition link_inv (L: list (loc * Z)): iProp Σ := + link_inv' L 0. + + Fixpoint value_inv (Lin: list (loc * Z)): iProp Σ := + (match Lin with + | [] => True + | (l, v) :: L' => (l +ₗ 1) ↦ #v ∗ P(v) ∗ value_inv L' + end)%I. + + Lemma tail_recursive_expansion (L: list (loc * Z)): + L = [] ∨ (∃L' t v, L = L' ++ [(t, v)]). + Proof. + induction L as [|(t', v')]; auto. right. + destruct IHL. + - rewrite H. by exists nil, t', v'. + - destruct H as [L' [t [v]]]. rewrite H. by exists ((t', v') :: L'), t, v. + Qed. + + Lemma link_inv_expand (L L': list (loc * Z)) (l: loc) (v: Z) (nl: base_lit): + (link_inv' L nl → ⌜L = L' ++ [(l, v)]⌝ → link_inv' L' l ∗ l ↦ #nl)%I. + Proof. + assert (H: forall a1 b1 a2 b2 A a, (link_inv' ((a1, b1) :: ((a2, b2) :: A))) a = (a1 ↦ #a2 ∗ link_inv' ((a2, b2) :: A) a)%I). + { intros. unfold link_inv'. by fold (link_inv' ((a2, b2) :: A) a). } + iInduction L' as [|[l' v'] L'] "IH" forall (L); iIntros "H %". + - iSplitR. done. rewrite app_nil_l in a. by rewrite a. + - rewrite a. + replace (((l', v') :: L') ++ [(l, v)]) with ((l', v') :: (L' ++ [(l, v)])) by done. + destruct L' as [|[l'' v''] L']. + + rewrite app_nil_l. iDestruct "H" as "(Hl & Hr)". iFrame. + + replace (((l', v') :: ((l'', v'') :: L') ++ [(l, v)])) with (((l', v') :: ((l'', v'') :: (L' ++ [(l, v)])))) by done. + rewrite H. iDestruct "H" as "(H & H2)". + iDestruct ("IH" with "[H2]") as "IH'". iFrame. + iFrame. by iApply "IH'". + Qed. + + Lemma link_inv_expand_rev (L L': list (loc * Z)) (l: loc) (v: Z) (nl: base_lit) : + (link_inv' L' l ∗ l ↦ #nl → ⌜L = L' ++ [(l, v)]⌝ → link_inv' L nl)%I. + Proof. + iInduction L' as [|[l' v'] L'] "IH" forall (L); iIntros "H %"; rewrite a. + - rewrite app_nil_l. by iDestruct "H" as "(_ & H)". + - replace (((l', v') :: L') ++ [(l, v)]) with ((l', v') :: (L' ++ [(l, v)])) by done. + destruct L' as [|[l'' v''] L']. + + by rewrite app_nil_l. + + iDestruct "H" as "((H & H2) & H3)". + iDestruct ("IH" with "[H2 H3]") as "IH'". iFrame. iFrame. by iApply "IH'". + Qed. + + Lemma value_inv_expand (L L': list (loc * Z)) (l: loc) (v: Z) : + (value_inv L → ⌜L = L' ++ [(l, v)]⌝ → value_inv L' ∗ (l +ₗ 1) ↦ #v ∗ P(v))%I. + Proof. + iInduction L' as [|[l' v'] L''] "IH" forall (L). + - iIntros "H %". iSplitR. done. rewrite app_nil_l in a. rewrite a. + iDestruct "H" as "(H1 & H2 & _)". iFrame. + - iIntros "H %". rewrite a. + replace (((l', v') :: L'') ++ [(l, v)]) with ((l', v') :: (L'' ++ [(l, v)])) by done. + iDestruct "H" as "(Hl & HPv & Hr)". iFrame. + iDestruct ("IH" with "Hr") as "IH'". by iApply "IH'". + Qed. + + Lemma value_inv_expand_rev (L L': list (loc * Z)) (l: loc) (v: Z) : + (value_inv L' ∗ (l +ₗ 1) ↦ #v ∗ P(v) → ⌜L = L' ++ [(l, v)]⌝ → value_inv L)%I. + Proof. + iInduction L' as [|[l' v'] L''] "IH" forall (L); iIntros "H %"; rewrite a. + - rewrite app_nil_l. iDestruct "H" as "(_ & H1 & H2)". iFrame. + - replace (((l', v') :: L'') ++ [(l, v)]) with ((l', v') :: (L'' ++ [(l, v)])) by done. + iDestruct "H" as "((H & H2 & H3) & H4 & H5)". + iDestruct ("IH" with "[H3 H4 H5]") as "IH'". iFrame. iFrame. by iApply "IH'". + Qed. + +End LV_Invs. \ No newline at end of file diff --git a/exercises/list_pre.v b/exercises/list_pre.v index 444c4f2af1cb62fb661c7a678fb5205152533963..45758fd4ed71660712ee1bdc5e765f34277a22e2 100644 --- a/exercises/list_pre.v +++ b/exercises/list_pre.v @@ -105,8 +105,7 @@ Section ListMaster. destruct x, y; try done; try inversion H1; try inversion H0. - unfold Assoc. intros. destruct x, y, z; try done. assert (ListSome l0 ⋅ ListBot = ListBot). done. - destruct (ListSome l ⋅ ListSome l0); rewrite H0; try done. - unfold "⋅", lp_op. admit. + destruct (ListSome l ⋅ ListSome l0); rewrite H0; try done. admit. - unfold Comm. intros. destruct x, y; try done. unfold "⋅", lp_op. destruct (decide (l `prefix_of` l0)); destruct (decide (l0 `prefix_of` l)); try done. diff --git a/exercises/queue-spec.v b/exercises/queue-spec.v index 9aded92576c7b6da48072533ff5856c57d38fa37..f6045e51285708fc48a3c309fffb7cf5c08aee31 100644 --- a/exercises/queue-spec.v +++ b/exercises/queue-spec.v @@ -86,15 +86,19 @@ Section MSQueue. Lemma link_inv_expand (L L': list (loc * Z)) (l: loc) (v: Z) (nl: base_lit): (link_inv' L nl → ⌜L = L' ++ [(l, v)]⌝ → link_inv' L' l ∗ l ↦ #nl)%I. Proof. + assert (H: forall a1 b1 a2 b2 A a, (link_inv' ((a1, b1) :: ((a2, b2) :: A))) a = (a1 ↦ #a2 ∗ link_inv' ((a2, b2) :: A) a)%I). + { intros. unfold link_inv'. by fold (link_inv' ((a2, b2) :: A) a). } iInduction L' as [|[l' v'] L'] "IH" forall (L); iIntros "H %". - iSplitR. done. rewrite app_nil_l in a. by rewrite a. - rewrite a. replace (((l', v') :: L') ++ [(l, v)]) with ((l', v') :: (L' ++ [(l, v)])) by done. destruct L' as [|[l'' v''] L']. + rewrite app_nil_l. iDestruct "H" as "(Hl & Hr)". iFrame. - + iDestruct "H" as "(H & H2)". iDestruct ("IH" with "[H2]") as "IH'". (*iApply "H2".*) admit. + + replace (((l', v') :: ((l'', v'') :: L') ++ [(l, v)])) with (((l', v') :: ((l'', v'') :: (L' ++ [(l, v)])))) by done. + rewrite H. iDestruct "H" as "(H & H2)". + iDestruct ("IH" with "[H2]") as "IH'". iFrame. iFrame. by iApply "IH'". - Admitted. + Qed. Lemma link_inv_expand_rev (L L': list (loc * Z)) (l: loc) (v: Z) (nl: base_lit) : (link_inv' L' l ∗ l ↦ #nl → ⌜L = L' ++ [(l, v)]⌝ → link_inv' L nl)%I. @@ -114,7 +118,7 @@ Section MSQueue. | (l, v) :: L' => (l +ₗ 1) ↦ #v ∗ P(v) ∗ value_inv L' end)%I. - Lemma value_inv_rev_expand (L L': list (loc * Z)) (l: loc) (v: Z) : + Lemma value_inv_expand (L L': list (loc * Z)) (l: loc) (v: Z) : (value_inv L → ⌜L = L' ++ [(l, v)]⌝ → value_inv L' ∗ (l +ₗ 1) ↦ #v ∗ P(v))%I. Proof. iInduction L' as [|[l' v'] L''] "IH" forall (L). @@ -126,7 +130,7 @@ Section MSQueue. iDestruct ("IH" with "Hr") as "IH'". by iApply "IH'". Qed. - Lemma value_inv_rev_expand_rev (L L': list (loc * Z)) (l: loc) (v: Z) : + Lemma value_inv_expand_rev (L L': list (loc * Z)) (l: loc) (v: Z) : (value_inv L' ∗ (l +ₗ 1) ↦ #v ∗ P(v) → ⌜L = L' ++ [(l, v)]⌝ → value_inv L)%I. Proof. iInduction L' as [|[l' v'] L''] "IH" forall (L); iIntros "H %"; rewrite a. @@ -242,11 +246,13 @@ Section MSQueue. - iDestruct (link_inv_expand with "Hl") as "Hl". by iApply "Hl". } iDestruct "Ht" as "[Hl Ht]". rewrite loc_add_0. wp_store. - iMod (@own_lat_auth_update (leibnizO (loc * Z)) _ _ _ _ _ _ (Lout_rest ++ [(h, d)] ++ Lin ++ [(n, x)]) _ with "Hγp●") as "[[Hγp●1 Hγp●2] _]". + assert (Ex: (Lout_rest ++ L_rest ++ [(t, tv)]) `prefix_of` (Lout_rest ++ [(h, d)] ++ Lin ++ [(n, x)])). + { rewrite <- H. do 2 (apply prefix_app). by exists [(n, x)]. } + iMod (@own_lat_auth_update (leibnizO (loc * Z)) _ _ _ _ _ _ (Lout_rest ++ [(h, d)] ++ Lin ++ [(n, x)]) Ex with "Hγp●") as "[[Hγp●1 Hγp●2] _]". iMod ("Hclose" with "[Hhq Htq Ht Hl Hv Hnl Hnd Hγc● Hγp●1 Px]") as "_". { iNext. iExists _, _, _. iFrame. iExists (Lin ++ [(n, x)]), Lout_rest, d. rewrite app_assoc. iFrame. rewrite app_assoc. rewrite H. rewrite loc_add_0. - iDestruct (value_inv_rev_expand_rev (Lin ++ [(n, x)]) Lin n x) as "Hvalue". + iDestruct (value_inv_expand_rev (Lin ++ [(n, x)]) Lin n x) as "Hvalue". iDestruct ("Hvalue" with "[Hv Hnd Px]") as "Hv". by iFrame. iDestruct (link_inv_expand_rev ((L_rest ++ [(t, tv)]) ++ [(n, x)]) (L_rest ++ [(t, tv)]) n x 0) as "Hlink". iDestruct (link_inv_expand_rev (L_rest ++ [(t, tv)]) L_rest t tv n) as "Hlink'". @@ -262,8 +268,8 @@ Section MSQueue. { iNext. iExists _, _, _. iFrame. } iModIntro. wp_seq. iApply "Post". iSplitL. rewrite app_assoc. iExists _, x, (Lout_rest ++ [(h, d)] ++ Lin). - rewrite app_assoc. rewrite app_assoc. iFrame. by iLeft. - Admitted. + do 2 (rewrite app_assoc). iFrame. by iLeft. + Qed. Lemma tryDeq_spec q γc γp: {{{ Queue q γc γp ∗ Consumer q γc }}}