From 27e2cf0a58d41138b6e294538fda42dc1980552b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 10 Jan 2017 13:59:26 +0100
Subject: [PATCH] try and fail to make using ty_size_eq on \later own more
 convenient

---
 theories/typing/product_split.v | 1 +
 theories/typing/type.v          | 6 +++++-
 theories/typing/uniq_bor.v      | 1 -
 3 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 154dca9f..dce282b4 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -95,6 +95,7 @@ Section product_split.
     iDestruct "H" as (vl1 vl2) "(>% & H1 & H2)". subst.
     rewrite heap_mapsto_vec_app -freeable_sz_split.
     iDestruct "H†" as "[H†1 H†2]". iDestruct "H↦" as "[H↦1 H↦2]".
+    (* FIXME: I found no way to use ty_size_eq_later here to avoid the assert. *)
     iAssert (▷ ⌜length vl1 = ty_size ty1⌝)%I with "[#]" as ">EQ".
     { iNext. by iApply ty_size_eq. }
     iDestruct "EQ" as %->. iSplitL "H↦1 H†1 H1".
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 89ffb4c6..31c53a2b 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -50,6 +50,11 @@ Section type.
     }.
   Global Existing Instances ty_shr_persistent.
 
+  Lemma ty_size_eq_later (ty : type) tid vl :
+    ▷ ty.(ty_own) tid vl -∗ ▷ ⌜length vl = ty.(ty_size)⌝.
+  Proof. iIntros "Hown". iApply ty_size_eq. done. Qed.
+
+  (** Copy types *)
   Fixpoint shr_locsE (l : loc) (n : nat) : coPset :=
     match n with
     | 0%nat => ∅
@@ -99,7 +104,6 @@ Section type.
     rewrite shr_locsE_shift na_own_union //. apply shr_locsE_disj.
   Qed.
 
-  (** Copy types *)
   Class Copy (t : type) := {
     copy_persistent tid vl : PersistentP (t.(ty_own) tid vl);
     copy_shr_acc κ tid E F l q :
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index e20a4f68..cf019f8a 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -7,7 +7,6 @@ Set Default Proof Using "Type".
 
 Section uniq_bor.
   Context `{typeG Σ}.
-
   Local Hint Extern 1000 (_ ⊆ _) => set_solver : ndisj.
 
   Program Definition uniq_bor (κ:lft) (ty:type) :=
-- 
GitLab