update sum type definition

theories/typing/sum.v

@@ -6,101 +6,117 @@ From lrust.typing Require Import type_incl.
 Section sum.
   Context `{typeG Σ}.
 
+  Local Obligation Tactic := idtac.
+
   Program Definition emp : type := {| st_own tid vl := False%I |}.
   Next Obligation. iIntros (tid vl) "[]". Qed.
   Global Instance emp_empty : Empty type := emp.
 
+  Definition list_max (l : list nat) := foldr max 0%nat l.
+
   Lemma split_sum_mt l tid q tyl :
     (l ↦∗{q}: λ vl,
-         ∃ (i : nat) vl', ⌜vl = #i :: vl'⌝ ∗ ty_own (nth i tyl ∅) tid vl')%I
-    ⊣⊢ ∃ (i : nat), l ↦{q} #i ∗ shift_loc l 1 ↦∗{q}: ty_own (nth i tyl ∅) tid.
+         ∃ (i : nat) vl' vl'', ⌜vl = #i :: vl' ++ vl''⌝ ∗
+                               ⌜length vl = S (list_max $ map ty_size $ tyl)⌝ ∗
+                               ty_own (nth i tyl ∅) tid vl')%I
+    ⊣⊢ ∃ (i : nat), l ↦{q} #i ∗ shift_loc l 1 ↦∗{q}: (nth i tyl ∅).(ty_own) tid ∗
+                     shift_loc l (S $ (nth i tyl ∅).(ty_size)) ↦∗{q}: λ vl,
+                       ⌜((nth i tyl ∅).(ty_size) + length vl)%nat = (list_max $ map ty_size $ tyl)⌝.
   Proof.
     iSplit; iIntros "H".
-    - iDestruct "H" as (vl) "[Hmt Hown]". iDestruct "Hown" as (i vl') "[% Hown]".
+    - iDestruct "H" as (vl) "[Hmt Hown]". iDestruct "Hown" as (i vl' vl'') "(% & % & Hown)".
       subst. iExists i. iDestruct (heap_mapsto_vec_cons with "Hmt") as "[$ Hmt]".
-      iExists vl'. by iFrame.
-    - iDestruct "H" as (i) "[Hmt1 Hown]". iDestruct "Hown" as (vl) "[Hmt2 Hown]".
-      iExists (#i::vl). rewrite heap_mapsto_vec_cons. iFrame. eauto.
+      (* TODO: I should not have to say '[#]' here, similar to iDestruct ... as %.... *)
+      iAssert (⌜length vl' = (nth i tyl ∅).(ty_size)⌝%I) with "[#]" as %Hvl'.
+      { iApply ty_size_eq. done. }
+      iDestruct (heap_mapsto_vec_app with "Hmt") as "[Hmt Htail]". iSplitR "Htail".
+      + iExists vl'. by iFrame.
+      + iExists vl''. rewrite (shift_loc_assoc_nat _ 1) Hvl'. iFrame. iPureIntro.
+        rewrite -Hvl'. simpl in *. rewrite -app_length. congruence.
+    - iDestruct "H" as (i) "(Hmt1 & Hown & Htail)".
+      iDestruct "Hown" as (vl') "[Hmt2 Hown]". iDestruct "Htail" as (vl'') "[Hmt3 %]".
+      (* TODO: I should not have to say '[#]' here, similar to iDestruct ... as %.... *)
+      iAssert (⌜length vl' = (nth i tyl ∅).(ty_size)⌝%I) with "[#]" as %Hvl'.
+      { iApply ty_size_eq. done. } iExists (#i::vl'++vl'').
+      rewrite heap_mapsto_vec_cons heap_mapsto_vec_app (shift_loc_assoc_nat _ 1) Hvl'.
+      iFrame. iExists i, vl', vl''. iSplit; first done. iFrame. iPureIntro.
+      simpl. f_equal. by rewrite app_length Hvl'.
   Qed.
 
-  Class LstTySize (n : nat) (tyl : list type) :=
-    size_eq : Forall ((= n) ∘ ty_size) tyl.
-  Instance LstTySize_nil n : LstTySize n nil := List.Forall_nil _.
-  Lemma LstTySize_cons n ty tyl :
-    ty.(ty_size) = n → LstTySize n tyl → LstTySize n (ty :: tyl).
-  Proof. intros. constructor; done. Qed.
-
-  Lemma sum_size_eq n tid i tyl vl {Hn : LstTySize n tyl} :
-    ty_own (nth i tyl ∅) tid vl -∗ ⌜length vl = n⌝.
-  Proof.
-    iIntros "Hown". iDestruct (ty_size_eq with "Hown") as %->.
-    revert Hn. rewrite /LstTySize List.Forall_forall /= =>Hn.
-    edestruct nth_in_or_default as [| ->]. by eauto.
-    iDestruct "Hown" as "[]".
-  Qed.
-
-  Program Definition sum {n} (tyl : list type) {_:LstTySize n tyl} :=
-    {| ty_size := S n;
+  Program Definition sum (tyl : list type) :=
+    {| ty_size := S (list_max $ map ty_size $ tyl);
        ty_own tid vl :=
-         (∃ (i : nat) vl', ⌜vl = #i :: vl'⌝ ∗ (nth i tyl ∅).(ty_own) tid vl')%I;
+         (∃ (i : nat) vl' vl'', ⌜vl = #i :: vl' ++ vl''⌝ ∗
+                                ⌜length vl = S (list_max $ map ty_size $ tyl)⌝ ∗
+                                (nth i tyl ∅).(ty_own) tid vl')%I;
        ty_shr κ tid N l :=
          (∃ (i : nat), (&frac{κ} λ q, l ↦{q} #i) ∗
-               (nth i tyl ∅).(ty_shr) κ tid N (shift_loc l 1))%I
+               (nth i tyl ∅).(ty_shr) κ tid N (shift_loc l 1) ∗
+               (&frac{κ} λ q, shift_loc l (S $ (nth i tyl ∅).(ty_size)) ↦∗{q}: λ vl,
+                       ⌜((nth i tyl ∅).(ty_size) + length vl)%nat = (list_max $ map ty_size $ tyl)⌝))%I
     |}.
   Next Obligation.
-    iIntros (n tyl Hn tid vl) "Hown". iDestruct "Hown" as (i vl') "(%&Hown)".
-    subst. simpl. by iDestruct (sum_size_eq with "Hown") as %->.
+    iIntros (tyl tid vl) "Hown". iDestruct "Hown" as (i vl' vl'') "(%&%&_)".
+    subst. done.
   Qed.
   Next Obligation.
-    intros n tyl Hn E N κ l tid ??. iIntros "#LFT Hown". rewrite split_sum_mt.
+    intros tyl E N κ l tid ??. iIntros "#LFT Hown". rewrite split_sum_mt.
     iMod (bor_exists with "LFT Hown") as (i) "Hown". set_solver.
-    iMod (bor_sep with "LFT Hown") as "[Hmt Hown]". set_solver.
+    iMod (bor_sep with "LFT Hown") as "[Hmt Hown]". solve_ndisj.
+    iMod (bor_sep with "LFT Hown") as "[Hown Htail]". solve_ndisj.
     iMod ((nth i tyl ∅).(ty_share) with "LFT Hown") as "#Hshr"; try done.
-    iMod (bor_fracture with "LFT [-]") as "H"; last by eauto. set_solver. iFrame.
+    iMod (bor_fracture with "LFT [Htail]") as "H";[set_solver| |]; last first.
+    - iMod (bor_fracture with "LFT [Hmt]") as "H'";[set_solver| |]; last eauto.
+      by iFrame.
+    - by iFrame.
   Qed.
   Next Obligation.
-    intros n tyl Hn κ κ' tid E E' l ?. iIntros "#LFT #Hord H".
-    iDestruct "H" as (i) "[Hown0 Hown]". iExists i. iSplitL "Hown0".
-    by iApply (frac_bor_shorten with "Hord").
-    iApply ((nth i tyl ∅).(ty_shr_mono) with "LFT Hord"); last done. done.
+    intros tyl κ κ' tid E E' l ?. iIntros "#LFT #Hord H".
+    iDestruct "H" as (i) "[Hown0 [Hown Htail]]". iExists i.
+    iSplitL "Hown0"; last iSplitL "Hown".
+    - by iApply (frac_bor_shorten with "Hord").
+    - iApply ((nth i tyl ∅).(ty_shr_mono) with "LFT Hord"); last done. done.
+    - by iApply (frac_bor_shorten with "Hord").
   Qed.
 
   (* TODO : Make the Forall parameter a typeclass *)
-  Global Program Instance sum_copy `(LstTySize n tyl) :
+  (* TODO : This next step is suspuciously slow. *)
+  Global Program Instance sum_copy tyl :
     Forall Copy tyl → Copy (sum tyl).
   Next Obligation.
-    intros n tyl Hn HFA tid vl.
+    intros tyl HFA tid vl.
     cut (∀ i vl', PersistentP (ty_own (nth i tyl ∅) tid vl')). by apply _.
     intros. apply @copy_persistent. edestruct nth_in_or_default as [| ->];
       [by eapply List.Forall_forall| apply _].
   Qed.
   Next Obligation.
-    intros n tyl Hn HFA κ tid E F l q ?.
-    iIntros "#LFT #H[[Htok1 Htok2] Htl]".
-    setoid_rewrite split_sum_mt. iDestruct "H" as (i) "[Hshr0 Hshr]".
+    intros tyl HFA κ tid E F l q ?.
+    iIntros "#LFT #H[[Htok1 [Htok2 Htok3]] Htl]".
+    setoid_rewrite split_sum_mt. iDestruct "H" as (i) "[Hshr0 [Hshr Hshrtail]]".
     iMod (frac_bor_acc with "LFT Hshr0 Htok1") as (q'1) "[Hown Hclose]". set_solver.
-    iMod (@copy_shr_acc _ _ (nth i tyl ∅) with "LFT Hshr [Htok2 $Htl]")
-      as (q'2) "[Hownq Hclose']"; try done.
+    iMod (frac_bor_acc with "LFT Hshrtail Htok2") as (q'2) "[Htail Hclose']". set_solver.
+    iMod (@copy_shr_acc _ _ (nth i tyl ∅) with "LFT Hshr [Htok3 $Htl]")
+      as (q'3) "[Hownq Hclose'']"; try done.
     { edestruct nth_in_or_default as [| ->]; last by apply _.
         by eapply List.Forall_forall. }
-    destruct (Qp_lower_bound q'1 q'2) as (q' & q'01 & q'02 & -> & ->).
-    rewrite -{1}heap_mapsto_vec_prop_op; last (by intros; apply sum_size_eq, Hn).
+    destruct (Qp_lower_bound q'1 q'2) as (q'0 & q'01 & q'02 & -> & ->).
+    destruct (Qp_lower_bound q'0 q'3) as (q' & q'11 & q'12 & -> & ->).
+    rewrite -(heap_mapsto_vec_prop_op _ q' q'12); last (by intros; apply ty_size_eq).
+    rewrite -!Qp_plus_assoc.
+    rewrite -(heap_mapsto_vec_prop_op _ q' (q'11 + q'02)
+        (list_max (map ty_size tyl) - (ty_size (nth i tyl ∅)))%nat); last first.
+    { intros. iIntros (<-). iPureIntro. by rewrite minus_plus. }
     iDestruct "Hownq" as "[Hownq1 Hownq2]". iDestruct "Hown" as "[Hown1 >Hown2]".
-    iExists q'. iModIntro. iSplitL "Hown1 Hownq1".
+    iDestruct "Htail" as "[Htail1 Htail2]".
+    iExists q'. iModIntro. iSplitL "Hown1 Hownq1 Htail1".
     - iNext. iExists i. by iFrame.
-    - iIntros "H". iDestruct "H" as (i') "[>Hown1 Hownq1]".
+    - iIntros "H". iDestruct "H" as (i') "[>Hown1 [Hownq1 Htail1]]".
       iDestruct (heap_mapsto_agree with "[$Hown1 $Hown2]") as %[= ->%Z_of_nat_inj].
-      iCombine "Hown1" "Hown2" as "Hown". iMod ("Hclose" with "[Hown]") as "$"; first by eauto.
-      iCombine "Hownq1" "Hownq2" as "Hownq".
-      rewrite heap_mapsto_vec_prop_op; last (by intros; apply sum_size_eq, Hn).
-      by iApply "Hclose'".
+      iMod ("Hclose''" with "[$Hownq1 $Hownq2]"). iMod ("Hclose'" with "[$Htail1 $Htail2]").
+      iMod ("Hclose" with "[$Hown1 $Hown2]") as "$". by iFrame.
   Qed.
 End sum.
 
-Existing Instance LstTySize_nil.
-Hint Extern 1 (LstTySize _ (_ :: _)) =>
-  apply LstTySize_cons; [compute; reflexivity|] : typeclass_instances.
-
 (* Σ is commonly used for the current functor. So it cannot be defined
    as Π for products. We stick to the following form. *)
 Notation "Σ[ ty1 ; .. ; tyn ]" :=

theories/typing/type.v

@@ -153,8 +153,9 @@ Section subtyping.
       iApply (type_incl_trans with "[] []").
       + iApply (H12 with "[] []"); done.
       + iApply (H23 with "[] []"); done.
-Qed.
+  Qed.
 
+  (* TODO: The prelude should have a symmetric closure. *)
   Definition eqtype (ty1 ty2 : type) : Prop :=
     subtype ty1 ty2 ∧ subtype ty2 ty1.