Proof of [perm_split_own_prod].

perm.v

@@ -7,8 +7,8 @@ Bind Scope perm_scope with perm.
 
 (* TODO : find a better place for this. *)
 Definition valuable := option val.
-Definition proj_valuable (n : Z) :=
-  (≫= λ v, match v with LitV (LitLoc l) => Some (shift_loc l n) | _ => None end).
+Definition proj_valuable (n : Z) : valuable → valuable :=
+  (≫= λ v, match v with LitV (LitLoc l) => Some (#(shift_loc l n)) | _ => None end).
 
 Module Perm.
 

perm_incl.v

+From Coq Require Import Qcanon.
 From iris.algebra Require Import upred_big_op.
 From iris.program_logic Require Import thread_local.
 From lrust Require Export type perm.
 
-Import Perm.
+Import Perm Types.
 
 Section defs.
 
@@ -48,6 +49,14 @@ Section props.
     Proper ((⇔) ==> (⇔) ==> iff) (⇒).
   Proof. intros ??[??]??[??]; split; intros ?; by simplify_order. Qed.
 
+  Global Instance perm_sep_proper :
+    Proper ((⇔) ==> (⇔) ==> (⇔)) (sep).
+  Proof.
+    intros ??[A B]??[C D]; split; iIntros (tid) "[A B]".
+    iVs (A with "A") as "$". iApply (C with "B").
+    iVs (B with "A") as "$". iApply (D with "B").
+  Qed.
+
   Lemma perm_incl_top ρ : ρ ⇒ ⊤.
   Proof. iIntros (tid) "H". eauto. Qed.
 
@@ -101,4 +110,67 @@ Section props.
     admit. set_solver. iVsIntro. iExists _. iSplit. done. done.
   Admitted.
 
+  Lemma perm_split_own_prod tyl (q : Qp) (ql : list Qp) v :
+    length tyl = length ql →
+    foldr (λ (q : Qp) acc, q + acc)%Qc 0%Qc ql = q →
+    v ◁ own q (product tyl) ⇔
+      foldr (λ qtysz acc,
+             proj_valuable (Z.of_nat (qtysz.2.2)) v ◁
+                           own (qtysz.1) (qtysz.2.1) ★ acc)
+            ⊤ (combine ql (combine_offs tyl 0)).
+  Proof.
+    destruct tyl as [|ty0 tyl], ql as [|q0 ql]; try done.
+    { simpl. intros _?. destruct q as [q ?]. simpl in *. by subst. }
+    destruct v as [[[|l|]|]|];
+      try by split; iIntros (tid) "H";
+        [iDestruct "H" as (l) "[% _]" || iDestruct "H" as "[]" |
+         iDestruct "H" as "[[]_]"].
+    intros [= EQ]. revert EQ.
+    rewrite -{1}(shift_loc_0 l). change 0 with (Z.of_nat 0). generalize O at 2 3.
+    revert q ty0 q0 ql. induction tyl as [|ty1 tyl IH]=>q ty0 q0 ql offs Hlen Hq;
+      destruct ql as [|q1 ql]; try done.
+    - simpl in Hq. rewrite ->Qcplus_0_r, <-Qp_eq in Hq. subst q.
+      rewrite /= right_id. split; iIntros (tid) "H!==>/="; rewrite Nat.add_0_r.
+      + iDestruct "H" as (l') "(%&?&H)". iExists l'. iSplit. done. iFrame. iNext.
+        iDestruct "H" as (vl) "[Hvl H]".
+        iDestruct "H" as ([|?[|??]]) "(%&%&?)"; try done.
+        iExists _. subst. rewrite /= app_nil_r big_sepL_singleton. by iFrame.
+      + iDestruct "H" as (l') "(%&?&Hown)". iExists l'. iSplit. done. iFrame. iNext.
+        iDestruct "Hown" as (vl) "[Hmt Hown]". iExists vl. iFrame.
+        iExists [vl]. rewrite /= app_nil_r big_sepL_singleton. iFrame. by iSplit.
+    - assert (Hq' : (0 < q1 + foldr (λ (q : Qp) acc, q + acc) 0 ql)%Qc).
+      { apply Qcplus_pos_nonneg. done. clear. induction ql. done.
+        apply Qcplus_nonneg_nonneg; last done. by apply Qclt_le_weak. }
+      pose (q' := mk_Qp _ Hq').
+      assert (q = q0 + q')%Qp as -> by rewrite Qp_eq -Hq //. clear Hq.
+      injection Hlen. clear Hlen. intro Hlen.
+      simpl in IH|-*. rewrite -(IH q') //. split; iIntros (tid) "H".
+      + iDestruct "H" as (l') "(Hl'&Hf&H)". iDestruct "Hl'" as %[= Hl']. subst.
+        iDestruct "H" as (vl) "[Hvl H]".
+        iDestruct "H" as ([|vl0[|vl1 vll]]) "(>%&>%&Hown)"; try done. subst.
+        rewrite big_sepL_cons heap_mapsto_vec_app -heap_freeable_op_eq.
+        iDestruct "Hf" as "[Hf0 Hfq]". iDestruct "Hvl" as "[Hvl0 Hvll]".
+        iDestruct "Hown" as "[Hown0 Hown]".
+        iAssert (▷ (length vl0 = ty_size ty0))%I with "[#]" as "#>Hlenvl0".
+        { iNext. iApply (ty_size_eq with "Hown0"). }
+        iDestruct "Hlenvl0" as %Hlenvl0. iVsIntro. iSplitL "Hf0 Hvl0 Hown0".
+        * iExists _. iSplit. done. iFrame. iNext. iExists vl0. by iFrame.
+        * iExists _. iSplit. done. rewrite !shift_loc_assoc -!Nat2Z.inj_add Hlenvl0.
+          iFrame. iNext. iExists (concat (vl1 :: vll)). iFrame. iExists (_ :: _).
+          iSplit. done. iFrame. iPureIntro. simpl in *. congruence.
+      + iDestruct "H" as "[H0 H]".
+        iDestruct "H0" as (vl0) "(Heq&Hf0&Hmt0)". iDestruct "Heq" as %[= ?]. subst vl0.
+        iDestruct "H" as (vl) "(Heq&Hf&Hmt)". iDestruct "Heq" as %[= ?]. subst vl.
+        iVsIntro. iExists (shift_loc l offs). iSplit. done. iNext.
+        iSplitL "Hf Hf0".
+        * rewrite -heap_freeable_op_eq shift_loc_assoc Nat2Z.inj_add. by iFrame.
+        * iDestruct "Hmt0" as (vl0) "[Hmt0 Hown0]". iDestruct "Hmt" as (vl) "[Hmt Hown]".
+          iDestruct (ty_size_eq with "Hown0") as %<-.
+          iExists (vl0 ++ vl). iSplitL "Hmt Hmt0".
+          { rewrite heap_mapsto_vec_app shift_loc_assoc Nat2Z.inj_add. by iFrame. }
+          iDestruct "Hown" as (vll) "(%&%&Hown)". subst.
+          iExists (_ :: _). iSplit. done. iSplit. iPureIntro; simpl in *; congruence.
+          rewrite big_sepL_cons. by iFrame.
+  Qed.
+
 End props.

type.v

@@ -255,10 +255,10 @@ Section types.
     iIntros (κ ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
   Qed.
 
-  Fixpoint combine_accu_size (tyl : list type) (accu : nat) :=
+  Fixpoint combine_offs (tyl : list type) (accu : nat) :=
     match tyl with
     | [] => []
-    | ty :: q => (ty, accu) :: combine_accu_size q (accu + ty.(ty_size))
+    | ty :: q => (ty, accu) :: combine_offs q (accu + ty.(ty_size))
     end.
 
   Lemma list_ty_type_eq tid (tyl : list type) (vll : list (list val)) :
@@ -277,7 +277,7 @@ Section types.
     (l ↦★{q}: λ vl,
        ∃ vll, vl = concat vll ★ length tyl = length vll
          ★ [★ list] tyvl ∈ combine tyl vll, ty_own (tyvl.1) tid (tyvl.2))%I
-    ⊣⊢ [★ list] tyoffs ∈ combine_accu_size tyl 0,
+    ⊣⊢ [★ list] tyoffs ∈ combine_offs tyl 0,
          shift_loc l (tyoffs.2) ↦★{q}: ty_own (tyoffs.1) tid.
   Proof.
     rewrite -{1}(shift_loc_0 l). change 0%Z with (Z.of_nat 0).
@@ -331,7 +331,7 @@ Section types.
          (∃ vll, vl = concat vll ★ length tyl = length vll ★
                  [★ list] tyvl ∈ combine tyl vll, tyvl.1.(ty_own) tid (tyvl.2))%I;
        ty_shr κ tid N l :=
-         ([★ list] i ↦ tyoffs ∈ combine_accu_size tyl 0,
+         ([★ list] i ↦ tyoffs ∈ combine_offs tyl 0,
            tyoffs.1.(ty_shr) κ tid (N .@ i) (shift_loc l (tyoffs.2)))%I
     |}.
   Next Obligation.
@@ -350,7 +350,7 @@ Section types.
   Next Obligation.
     intros tyl E N κ l tid q ??. rewrite split_prod_mt.
     change (ndot (A:=nat)) with (λ N i, N .@ (0+i)%nat). generalize O at 3.
-    induction (combine_accu_size tyl 0) as [|[ty offs] ll IH].
+    induction (combine_offs tyl 0) as [|[ty offs] ll IH].
     - iIntros (?) "_$!==>". by rewrite big_sepL_nil.
     - iIntros (i) "Hown Htoks". rewrite big_sepL_cons.
       iVs (lft_borrow_split with "Hown") as "[Hownh Hownq]". set_solver.