From fa1cf9280b312aadb228536671bcaa538e345646 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 14 Dec 2016 09:37:09 +0100
Subject: [PATCH] Product flattening.

---
 theories/typing/bool.v     |  2 +-
 theories/typing/function.v |  3 +-
 theories/typing/int.v      |  2 +-
 theories/typing/own.v      |  2 +-
 theories/typing/product.v  | 85 ++++++++++++++++----------------------
 theories/typing/shr_bor.v  |  5 +--
 theories/typing/sum.v      |  8 +---
 theories/typing/type.v     | 10 ++---
 8 files changed, 47 insertions(+), 70 deletions(-)

diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index b53199cf..f2db2e46 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -6,7 +6,7 @@ Section bool.
   Context `{typeG Σ}.
 
   Program Definition bool : type :=
-    {| st_size := 1; st_own tid vl := (∃ z:bool, ⌜vl = [ #z ]⌝)%I |}.
+    {| st_own tid vl := (∃ z:bool, ⌜vl = [ #z ]⌝)%I |}.
   Next Obligation. iIntros (tid vl) "H". iDestruct "H" as (z) "%". by subst. Qed.
 
   Lemma typed_bool ρ (b:Datatypes.bool): typed_step_ty ρ #b bool.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index ed55d80b..c7c171d4 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -10,8 +10,7 @@ Section fn.
 
   Program Definition fn {A n} (E : A → elctx)
           (tys : A → vec type n) (ty : A → type) : type :=
-    {| st_size := 1;
-       st_own tid vl := (∃ f, ⌜vl = [f]⌝ ∗ □ ∀ (x : A) (args : vec val n) (k : val),
+    {| st_own tid vl := (∃ f, ⌜vl = [f]⌝ ∗ □ ∀ (x : A) (args : vec val n) (k : val),
          typed_body (E x) []
                     [CctxElt k [] 1 (λ v, [TCtx_holds (v!!!0) (ty x)])]
                     (zip_with (TCtx_holds ∘ of_val) args (tys x))
diff --git a/theories/typing/int.v b/theories/typing/int.v
index ce2340bd..31d8a7b8 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -6,7 +6,7 @@ Section int.
   Context `{typeG Σ}.
 
   Program Definition int : type :=
-    {| st_size := 1; st_own tid vl := (∃ z:Z, ⌜vl = [ #z ]⌝)%I |}.
+    {| st_own tid vl := (∃ z:Z, ⌜vl = [ #z ]⌝)%I |}.
   Next Obligation. iIntros (tid vl) "H". iDestruct "H" as (z) "%". by subst. Qed.
 
   Lemma typed_int ρ (z:Datatypes.nat) :
diff --git a/theories/typing/own.v b/theories/typing/own.v
index aaf7b21d..273b45f5 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -12,7 +12,7 @@ Section own.
   (* Even though it does not seem too natural to put this here, it is
      the only place where it is used. *)
   Program Definition uninit : type :=
-    {| st_size := 1; st_own tid vl := ⌜length vl = 1%nat⌝%I |}.
+    {| st_own tid vl := ⌜length vl = 1%nat⌝%I |}.
   Next Obligation. done. Qed.
 
   Program Definition freeable_sz (n : nat) (sz : nat) (l : loc) : iProp Σ :=
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 0933c519..10724e77 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -7,8 +7,17 @@ Section product.
   Context `{typeG Σ}.
 
   Program Definition unit : type :=
-    {| st_size := 0; st_own tid vl := ⌜vl = []⌝%I |}.
-  Next Obligation. iIntros (tid vl) "%". simpl. by subst. Qed.
+    {| ty_size := 0; ty_own tid vl := ⌜vl = []⌝%I; ty_shr κ tid E l := True%I |}.
+  Next Obligation. iIntros (tid vl) "%". by subst. Qed.
+  Next Obligation. by iIntros (???????) "_ _". Qed.
+  Next Obligation. by iIntros (???????) "_ _ $". Qed.
+
+  Global Instance unit_copy : Copy unit.
+  Proof.
+    split. by apply _.
+    iIntros (???????) "_ _ $". iExists 1%Qp. iSplitL; last by auto.
+    iExists []. iSplitL; last by auto. rewrite heap_mapsto_vec_nil. auto.
+  Qed.
 
   Lemma split_prod_mt tid ty1 ty2 q l :
     (l ↦∗{q}: λ vl,
@@ -121,71 +130,49 @@ Notation Π := product.
 Section typing.
   Context `{typeG Σ}.
 
-  (* FIXME : do we still need this (flattening and unflattening)? *)
-
-  Lemma ty_incl_prod2_assoc1 ρ ty1 ty2 ty3 :
-    ty_incl ρ (product2 ty1 (product2 ty2 ty3)) (product2 (product2 ty1 ty2) ty3).
+  Global Instance prod2_assoc E L : Assoc (eqtype E L) product2.
   Proof.
-    iIntros (tid) "_ _!>". iSplit; iIntros "!#/=*H".
+    split; (split; simpl; [by rewrite assoc| |]; intros; iIntros "_ _ _ H").
     - iDestruct "H" as (vl1 vl') "(% & Ho1 & H)".
       iDestruct "H" as (vl2 vl3) "(% & Ho2 & Ho3)". subst.
       iExists _, _. iSplit. by rewrite assoc. iFrame. iExists _, _. by iFrame.
     - iDestruct "H" as (E1 E2') "(% & Hs1 & H)".
       iDestruct "H" as (E2 E3) "(% & Hs2 & Hs3)". rewrite shift_loc_assoc_nat.
-      iSplit; last by rewrite assoc.
       iExists (E1 ∪ E2), E3. iSplit. by iPureIntro; set_solver. iFrame.
       iExists E1, E2. iSplit. by iPureIntro; set_solver. by iFrame.
-  Qed.
-
-  Lemma ty_incl_prod2_assoc2 ρ ty1 ty2 ty3 :
-    ty_incl ρ (product2 (product2 ty1 ty2) ty3) (product2 ty1 (product2 ty2 ty3)).
-  Proof.
-    iIntros (tid) "_ _!>". iSplit; iIntros "!#/=*H".
     - iDestruct "H" as (vl1 vl') "(% & H & Ho3)".
       iDestruct "H" as (vl2 vl3) "(% & Ho1 & Ho2)". subst.
       iExists _, _. iSplit. by rewrite -assoc. iFrame. iExists _, _. by iFrame.
     - iDestruct "H" as (E1' E3) "(% & H & Hs3)".
       iDestruct "H" as (E1 E2) "(% & Hs1 & Hs2)". rewrite shift_loc_assoc_nat.
-      iSplit; last by rewrite assoc.
       iExists E1, (E2 ∪ E3). iSplit. by iPureIntro; set_solver. iFrame.
       iExists E2, E3. iSplit. by iPureIntro; set_solver. by iFrame.
   Qed.
 
-  Lemma ty_incl_prod_flatten ρ tyl1 tyl2 tyl3 :
-    ty_incl ρ (Π(tyl1 ++ Π tyl2 :: tyl3))
-              (Π(tyl1 ++ tyl2 ++ tyl3)).
+  Global Instance prod2_unit_leftid E L : LeftId (eqtype E L) unit product2.
+  Proof.
+    intros ty. split; (split; [done| |]); intros; iIntros "#LFT _ _ H".
+    - iDestruct "H" as (? ?) "(% & % & ?)". by subst.
+    - iDestruct "H" as (? ?) "(% & ? & ?)". rewrite shift_loc_0.
+      iApply (ty_shr_mono with "LFT []"); last done. set_solver. iApply lft_incl_refl.
+    - iExists [], _. eauto.
+    - iExists ∅, F. rewrite shift_loc_0. iFrame. by iPureIntro; set_solver.
+  Qed.
+
+  Global Instance prod2_unit_rightid E L : RightId (eqtype E L) unit product2.
   Proof.
-  Admitted.
-  (*   apply (ty_incl_weaken _ ⊤). apply perm_incl_top. *)
-  (*   induction tyl1; last by apply (ty_incl_prod2 _ _ _ _ _ _). *)
-  (*   induction tyl2 as [|ty tyl2 IH]; simpl. *)
-  (*   - iIntros (tid) "#LFT _". iSplitL; iIntros "/=!>!#*H". *)
-  (*     + iDestruct "H" as (vl1 vl2) "(% & % & Ho)". subst. done. *)
-  (*     + iDestruct "H" as (E1 E2) "(% & H1 & Ho)". iSplit; last done. *)
-  (*       rewrite shift_loc_0. iApply (ty_shr_mono with "LFT [] Ho"). set_solver. *)
-  (*       iApply lft_incl_refl. *)
-  (*   - etransitivity. apply ty_incl_prod2_assoc2. *)
-  (*     eapply (ty_incl_prod2 _ _ _ _ _ _). done. apply IH. *)
-  (* Qed. *)
+    intros ty. split; (split; [by rewrite /= -plus_n_O| |]); intros; iIntros "#LFT _ _ H".
+    - iDestruct "H" as (? ?) "(% & ? & %)". subst. by rewrite app_nil_r.
+    - iDestruct "H" as (? ?) "(% & ? & _)".
+      iApply (ty_shr_mono with "LFT []"); last done. set_solver. iApply lft_incl_refl.
+    - iExists _, []. rewrite app_nil_r. eauto.
+    - iExists F, ∅. iFrame. by iPureIntro; set_solver.
+  Qed.
 
-  Lemma ty_incl_prod_unflatten ρ tyl1 tyl2 tyl3 :
-    ty_incl ρ (Π(tyl1 ++ tyl2 ++ tyl3))
-              (Π(tyl1 ++ Π tyl2 :: tyl3)).
+  Lemma ty_incl_prod_flatten E L tyl1 tyl2 tyl3 :
+    eqtype E L (Π(tyl1 ++ Π tyl2 :: tyl3)) (Π(tyl1 ++ tyl2 ++ tyl3)).
   Proof.
-  Admitted.
-  (*   apply (ty_incl_weaken _ ⊤). apply perm_incl_top. *)
-  (*   induction tyl1; last by apply (ty_incl_prod2 _ _ _ _ _ _). *)
-  (*   induction tyl2 as [|ty tyl2 IH]; simpl. *)
-  (*   - iIntros (tid) "#LFT _". iMod (bor_create with "LFT []") as "[Hbor _]". *)
-  (*     done. instantiate (1:=True%I). by auto. instantiate (1:=static). *)
-  (*     iMod (bor_fracture (λ _, True%I) with "LFT Hbor") as "#Hbor". done. *)
-  (*     iSplitL; iIntros "/=!>!#*H". *)
-  (*     + iExists [], vl. iFrame. auto. *)
-  (*     + iSplit; last done. iExists ∅, E. iSplit. iPureIntro; set_solver. *)
-  (*       rewrite shift_loc_0. iFrame. iExists []. iSplit; last auto. *)
-  (*       setoid_rewrite heap_mapsto_vec_nil. *)
-  (*       iApply (frac_bor_shorten with "[] Hbor"). iApply lft_incl_static. *)
-  (*   - etransitivity; last apply ty_incl_prod2_assoc1. *)
-  (*     eapply (ty_incl_prod2 _ _ _ _ _ _). done. apply IH. *)
-  (* Qed. *)
+    unfold product. induction tyl1; simpl; last by f_equiv.
+    induction tyl2. by rewrite left_id. by rewrite /= -assoc; f_equiv.
+  Qed.
 End typing.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 310440f0..7061d7bf 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -8,8 +8,7 @@ Section shr_bor.
   Context `{typeG Σ}.
 
   Program Definition shr_bor (κ : lft) (ty : type) : type :=
-    {| st_size := 1;
-       st_own tid vl :=
+    {| st_own tid vl :=
          (∃ (l:loc), ⌜vl = [ #l ]⌝ ∗ ty.(ty_shr) κ tid (↑lrustN) l)%I |}.
   Next Obligation.
     iIntros (κ ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
@@ -18,7 +17,7 @@ Section shr_bor.
   Global Instance subtype_shr_bor_mono E L :
     Proper (lctx_lft_incl E L --> subtype E L ==> subtype E L) shr_bor.
   Proof.
-    intros κ1 κ2 Hκ ty1 ty2 Hty. apply subtype_simple_type. done.
+    intros κ1 κ2 Hκ ty1 ty2 Hty. apply subtype_simple_type.
     iIntros (??) "#LFT #HE #HL H". iDestruct (Hκ with "HE HL") as "#Hκ".
     iDestruct "H" as (l) "(% & H)". subst. iExists _. iSplit. done.
     iApply (ty2.(ty_shr_mono) with "LFT Hκ"). reflexivity.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index c707306a..d9aa9782 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -6,7 +6,7 @@ From lrust.typing Require Import type_incl.
 Section sum.
   Context `{typeG Σ}.
 
-  Program Definition emp : type := {| st_size := 0; st_own tid vl := False%I |}.
+  Program Definition emp : type := {| st_own tid vl := False%I |}.
   Next Obligation. iIntros (tid vl) "[]". Qed.
   Global Instance emp_empty : Empty type := emp.
 
@@ -101,7 +101,6 @@ 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 ]" :=
@@ -110,11 +109,6 @@ Notation "Σ[ ty1 ; .. ; tyn ]" :=
 Section incl.
   Context `{typeG Σ}.
 
-   (* FIXME : do we need that anywhere?. *)
-  Lemma ty_incl_emp ρ ty : ty_incl ρ ∅ ty.
-  Proof.
-  Admitted.
-
   (* TODO *)
   (* Lemma ty_incl_sum ρ n tyl1 tyl2 (_ : LstTySize n tyl1) (_ : LstTySize n tyl2) : *)
   (*   Duplicable ρ → Forall2 (ty_incl ρ) tyl1 tyl2 → *)
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 6ad88ebc..7f79f464 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -56,16 +56,15 @@ Section type.
      that simple_type does depend on it. Otherwise, the coercion defined
      bellow will not be acceptable by Coq. *)
   Record simple_type `{typeG Σ} :=
-    { st_size : nat;
-      st_own : thread_id → list val → iProp Σ;
+    { st_own : thread_id → list val → iProp Σ;
 
-      st_size_eq tid vl : st_own tid vl -∗ ⌜length vl = st_size⌝;
+      st_size_eq tid vl : st_own tid vl -∗ ⌜length vl = 1%nat⌝;
       st_own_persistent tid vl : PersistentP (st_own tid vl) }.
 
   Global Existing Instance st_own_persistent.
 
   Program Definition ty_of_st (st : simple_type) : type :=
-    {| ty_size := st.(st_size); ty_own := st.(st_own);
+    {| ty_size := 1; ty_own := st.(st_own);
 
        (* [st.(st_own) tid vl] needs to be outside of the fractured
           borrow, otherwise I do not know how to prove the shr part of
@@ -154,12 +153,11 @@ Section subtyping.
   Qed.
 
   Lemma subtype_simple_type (st1 st2 : simple_type) :
-    st1.(st_size) = st2.(st_size) →
     (∀ tid vl, lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗
                  st1.(st_own) tid vl -∗ st2.(st_own) tid vl) →
     subtype st1 st2.
   Proof.
-    intros Hsz Hst. split; [done|by apply Hst|].
+    intros Hst. split; [done|by apply Hst|].
     iIntros (????) "#LFT #HE #HL H /=".
     iDestruct "H" as (vl) "[Hf [Hown|H†]]"; iExists vl; iFrame "Hf"; last by auto.
     iLeft. by iApply (Hst with "LFT HE HL *").
-- 
GitLab