Proof donegit add *.v!

exercises/link_value_invs.v

+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

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.

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 }}}