Merge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coq

_CoqProject

@@ -30,6 +30,7 @@ theories/typing/typing.v
 theories/typing/lft_contexts.v
 theories/typing/type_context.v
 theories/typing/cont_context.v
+theories/typing/uninit.v
 theories/typing/own.v
 theories/typing/uniq_bor.v
 theories/typing/shr_bor.v

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.

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

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) :

theories/typing/own.v

@@ -4,17 +4,11 @@ From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.lang Require Export new_delete.
 From lrust.lang Require Import heap.
 From lrust.typing Require Export type.
-From lrust.typing Require Import typing product perm.
+From lrust.typing Require Import typing product perm uninit.
 
 Section own.
   Context `{typeG Σ}.
 
-  (* 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 |}.
-  Next Obligation. done. Qed.
-
   Program Definition freeable_sz (n : nat) (sz : nat) (l : loc) : iProp Σ :=
     match sz, n return _ with
     | 0%nat, _ => True
@@ -123,7 +117,7 @@ Section own.
   Proof. intros ?? Heq. split; f_equiv; apply Heq. Qed.
 
   Lemma typed_new ρ (n : nat):
-    0 ≤ n → typed_step_ty ρ (new [ #n]%E) (own n (Π(replicate n uninit))).
+    0 ≤ n → typed_step_ty ρ (new [ #n]%E) (own n (uninit n)).
   Proof.
     iIntros (Hn tid) "!#(#HEAP&_&_&$)". iApply (wp_new with "HEAP"); try done.
     iIntros "!>*(% & H† & H↦)". iExists _. iSplit. done. iNext.
@@ -133,9 +127,7 @@ Section own.
       clear Hn. apply (inj Z.of_nat) in Hlen. subst.
       iInduction vl as [|v vl] "IH". done.
       iExists [v], vl. iSplit. done. by iSplit.
-    - assert (ty_size (Π (replicate n uninit)) = n) as ->.
-      { clear. induction n; rewrite //= IHn //. }
-      by rewrite freeable_sz_full.
+    - by rewrite uninit_sz freeable_sz_full.
   Qed.
 
   Lemma typed_delete ty (ν : expr):
@@ -178,8 +170,7 @@ Section own.
   Qed.
 
   Lemma consumes_move ty n:
-    consumes ty (λ ν, ν ◁ own n ty)%P
-             (λ ν, ν ◁ own n (Π(replicate ty.(ty_size) uninit)))%P.
+    consumes ty (λ ν, ν ◁ own n ty)%P (λ ν, ν ◁ own n (uninit ty.(ty_size)))%P.
   Proof.
     iIntros (ν tid Φ E ?) "_ H◁ Htl HΦ". iApply (has_type_wp with "H◁").
     iIntros (v) "Hνv H◁". iDestruct "Hνv" as %Hνv.
@@ -192,7 +183,6 @@ Section own.
     - rewrite -Hlen. iExists vl. iIntros "{$H↦}!>". clear.
       iInduction vl as [|v vl] "IH". done.
       iExists [v], vl. iSplit. done. by iSplit.
-    - assert (ty_size (Π (replicate (ty_size ty) uninit)) = ty_size ty) as ->; last by auto.
-      clear. induction ty.(ty_size). done. by apply (f_equal S).
+    - rewrite uninit_sz; auto.
   Qed.
 End own.

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,
@@ -109,11 +118,18 @@ Section product.
       iMod ("Hclose2" with "[H2 H↦2]") as "[$$]". by iExists _; iFrame. done.
   Qed.
 
-  Definition product := fold_right product2 unit.
+  Definition product := foldr product2 unit.
 
-  (* Given that in practice, product will be used with concrete lists,
-     there should be no need to declare [Copy] and [Proper] instances
-     for [product]. *)
+  Global Instance product_mono E L:
+    Proper (Forall2 (subtype E L) ==> subtype E L) product.
+  Proof. intros ??. induction 1. done. by simpl; f_equiv. Qed.
+  Global Instance product_proper E L:
+    Proper (Forall2 (eqtype E L) ==> eqtype E L) product.
+  Proof. intros ??. induction 1. done. by simpl; f_equiv. Qed.
+  (* FIXME : this instance is never going to be used, because Forall is
+     not a typeclass. *)
+  Global Instance product_copy tys : Forall Copy tys → Copy (product tys).
+  Proof. induction 1; apply _. Qed.
 End product.
 
 Arguments product : simpl never.
@@ -122,71 +138,59 @@ 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.
-  (*   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. *)
-
-  Lemma ty_incl_prod_unflatten ρ tyl1 tyl2 tyl3 :
-    ty_incl ρ (Π(tyl1 ++ tyl2 ++ tyl3))
-              (Π(tyl1 ++ Π tyl2 :: tyl3)).
+    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.
-  (*   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. *)
-*)
+    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 eqtype_prod_flatten E L tyl1 tyl2 tyl3 :
+    eqtype E L (Π(tyl1 ++ Π tyl2 :: tyl3)) (Π(tyl1 ++ tyl2 ++ tyl3)).
+  Proof.
+    unfold product. induction tyl1; simpl; last by f_equiv.
+    induction tyl2. by rewrite left_id. by rewrite /= -assoc; f_equiv.
+  Qed.
+
+  Lemma eqtype_prod_nil_flatten E L tyl1 tyl2 :
+    eqtype E L (Π(Π tyl1 :: tyl2)) (Π(tyl1 ++ tyl2)).
+  Proof. apply (eqtype_prod_flatten _ _ []). Qed.
+  Lemma eqtype_prod_flatten_nil E L tyl1 tyl2 :
+    eqtype E L (Π(tyl1 ++ [Π tyl2])) (Π(tyl1 ++ tyl2)).
+  Proof. by rewrite (eqtype_prod_flatten E L tyl1 tyl2 []) app_nil_r. Qed.
+  Lemma eqtype_prod_app E L tyl1 tyl2 :
+    eqtype E L (Π[Π tyl1; Π tyl2]) (Π(tyl1 ++ tyl2)).
+  Proof. by rewrite -eqtype_prod_flatten_nil -eqtype_prod_nil_flatten. Qed.
 End typing.

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.

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 ]" :=

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
@@ -168,12 +167,11 @@ Qed.
   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. iIntros. iSplit; first done. iSplit; iAlways.
+    intros Hst. iIntros. iSplit; first done. iSplit; iAlways.
     - iIntros. iApply (Hst with "* [] [] []"); done.
     - iIntros (????) "H".
       iDestruct "H" as (vl) "[Hf [Hown|H†]]"; iExists vl; iFrame "Hf"; last by auto.

theories/typing/uninit.v

+From lrust.typing Require Export type.
+From lrust.typing Require Import product.
+
+Section uninit.
+  Context `{typeG Σ}.
+
+  Program Definition uninit_1 : type :=
+    {| st_own tid vl := ⌜length vl = 1%nat⌝%I |}.
+  Next Obligation. done. Qed.
+
+  Definition uninit (n : nat) : type :=
+    Π (replicate n uninit_1).
+
+  Global Instance uninit_copy n : Copy (uninit n).
+  Proof. apply product_copy, Forall_replicate, _. Qed.
+
+  Lemma uninit_sz n : ty_size (uninit n) = n.
+  Proof. induction n. done. simpl. by f_equal. Qed.
+
+  Lemma eqtype_uninit_product E L ns :
+    eqtype E L (uninit (foldr plus 0%nat ns)) (Π(uninit <$> ns)).
+  Proof.
+    induction ns as [|n ns IH]. done. revert IH.
+    by rewrite /= /uninit replicate_plus eqtype_prod_nil_flatten -!eqtype_prod_app=>->.
+  Qed.
+End uninit.
\ No newline at end of file