define ty_own via locations WIP

theories/typing/product.v

@@ -15,56 +15,48 @@ Section product.
      convertible, but products are opaque in some hint DBs, so this does make a
      difference. *)
   Program Definition unit0 : type :=
-    {| ty_size := 0; ty_own tid vl := ⌜vl = []⌝%I; ty_shr κ tid l := True%I |}.
-  Next Obligation. iIntros (tid vl) "%". by subst. Qed.
+    {| ty_size := 0; ty_copy := true; ty_own tid l := True%I; ty_shr κ tid l := True%I |}.
+  Next Obligation. iIntros (tid l) "Hmt". iExists [# ]. rewrite heap_mapsto_vec_nil. eauto. Qed.
   Next Obligation. by iIntros (??????) "_ _ $". Qed.
   Next Obligation. by iIntros (????) "_ $". Qed.
-
-  Global Instance unit0_copy : Copy unit0.
-  Proof.
-    split. by apply _. iIntros (????????) "_ _ Htok $".
+  Next Obligation.
+    iIntros (?????????) "_ _ Htok $".
     iDestruct (na_own_acc with "Htok") as "[$ Htok]"; first solve_ndisj.
-    iExists 1%Qp. iModIntro. iSplitR.
-    { iExists []. iSplitL; last by auto. rewrite heap_mapsto_vec_nil. auto. }
-    iIntros "Htok2 _". iApply "Htok". done.
+    iExists 1%Qp, [# ]. iModIntro. rewrite heap_mapsto_vec_nil.
+    do 2 (iSplitR; eauto).
+    iIntros "Htok2 _". by iApply "Htok".
   Qed.
 
+  Global Instance unit0_copy : Copy unit0.
+  Proof. done. Qed.
+
   Global Instance unit0_send : Send unit0.
-  Proof. iIntros (tid1 tid2 vl) "H". done. Qed.
+  Proof. done. Qed.
 
   Global Instance unit0_sync : Sync unit0.
-  Proof. iIntros (????) "_". done. Qed.
-
-  Lemma split_prod_mt tid ty1 ty2 q l :
-    (l ↦∗{q}: λ vl,
-       ∃ vl1 vl2, ⌜vl = vl1 ++ vl2⌝ ∗ ty1.(ty_own) tid vl1 ∗ ty2.(ty_own) tid vl2)%I
-       ⊣⊢ l ↦∗{q}: ty1.(ty_own) tid ∗ (l +ₗ ty1.(ty_size)) ↦∗{q}: ty2.(ty_own) tid.
-  Proof.
-    iSplit; iIntros "H".
-    - iDestruct "H" as (vl) "[H↦ H]". iDestruct "H" as (vl1 vl2) "(% & H1 & H2)".
-      subst. rewrite heap_mapsto_vec_app. iDestruct "H↦" as "[H↦1 H↦2]".
-      iDestruct (ty_size_eq with "H1") as %->.
-      iSplitL "H1 H↦1"; iExists _; iFrame.
-    - iDestruct "H" as "[H1 H2]". iDestruct "H1" as (vl1) "[H↦1 H1]".
-      iDestruct "H2" as (vl2) "[H↦2 H2]". iExists (vl1 ++ vl2).
-      rewrite heap_mapsto_vec_app. iDestruct (ty_size_eq with "H1") as %->.
-      iFrame. iExists _, _. by iFrame.
-  Qed.
+  Proof. done. Qed.
 
   Program Definition product2 (ty1 ty2 : type) :=
     {| ty_size := ty1.(ty_size) + ty2.(ty_size);
-       ty_own tid vl := (∃ vl1 vl2,
-         ⌜vl = vl1 ++ vl2⌝ ∗ ty1.(ty_own) tid vl1 ∗ ty2.(ty_own) tid vl2)%I;
+       ty_copy := ty1.(ty_copy) && ty2.(ty_copy);
+       ty_own tid l := (ty1.(ty_own) tid l ∗ ty2.(ty_own) tid (l +ₗ ty1.(ty_size)))%I;
        ty_shr κ tid l :=
          (ty1.(ty_shr) κ tid l ∗
           ty2.(ty_shr) κ tid (l +ₗ ty1.(ty_size)))%I |}.
   Next Obligation.
-    iIntros (ty1 ty2 tid vl) "H". iDestruct "H" as (vl1 vl2) "(% & H1 & H2)".
-    subst. rewrite app_length !ty_size_eq.
-    iDestruct "H1" as %->. iDestruct "H2" as %->. done.
+    iIntros (ty1 ty2 tid l) "[Hty1 Hty2]".
+    iDestruct (ty_move with "Hty1") as (vl1) "[Hvl1 Hty1]".
+    iDestruct (ty_move with "Hty2") as (vl2) "[Hvl2 Hty2]".
+    iExists (vl1 +++ vl2). rewrite vec_to_list_app heap_mapsto_vec_app vec_to_list_length.
+    iFrame.
+    (* TODO is there a nicer way to do this? *)
+    destruct (ty_copy ty1), (ty_copy ty2) => /=;
+      try (iRevert "Hty1"; iIntros "#Hty1"); try (iRevert "Hty2"; iIntros "#Hty2"); try iModIntro;
+    iIntros (l'); rewrite heap_mapsto_vec_app vec_to_list_length; iDestruct 1 as "[Hl1 Hl2]";
+    by iSplitL "Hl1 Hty1"; [ iApply "Hty1" | iApply "Hty2" ].
   Qed.
-  Next Obligation.
-    intros ty1 ty2 E κ l tid q ?. iIntros "#LFT /=H Htok". rewrite split_prod_mt.
+ Next Obligation.
+    intros ty1 ty2 E κ l tid q ?. iIntros "#LFT /=H Htok".
     iMod (bor_sep with "LFT H") as "[H1 H2]"; first solve_ndisj.
     iMod (ty1.(ty_share) with "LFT H1 Htok") as "[? Htok]"; first solve_ndisj.
     iMod (ty2.(ty_share) with "LFT H2 Htok") as "[? Htok]"; first solve_ndisj.
@@ -74,17 +66,41 @@ Section product.
     intros ty1 ty2 κ κ' tid l. iIntros "/= #H⊑ [H1 H2]".
     iSplitL "H1"; by iApply (ty_shr_mono with "H⊑").
   Qed.
-
-  Global Instance product2_type_ne n:
-    Proper (type_dist2 n ==> type_dist2 n ==> type_dist2 n) product2.
-  Proof. solve_type_proper. Qed.
-
-  Global Instance product2_ne :
-    NonExpansive2 product2.
-  Proof.
-    constructor;
-      solve_proper_core ltac:(fun _ => (eapply ty_size_ne; try reflexivity) || f_equiv).
+  Next Obligation.
+    intros ty1 ty2 κ tid E F l q ? ? HF. iIntros "#LFT [H1 H2] Htl [Htok1 Htok2]".
+    destruct_and?.
+    iMod (@ty_copy_shr_acc with "LFT H1 Htl Htok1") as (q1 vl1) "(Htl & Hmt1 & Hown1 & Hclose1)"; [done | solve_ndisj | |].
+    { rewrite <-HF. apply shr_locsE_subseteq. simpl. clear. lia. }
+    iMod (@ty_copy_shr_acc with "LFT H2 Htl Htok2") as (q2 vl2) "(Htl & Hmt2 & Hown2 & Hclose2)"; [done | solve_ndisj | |].
+    { move: HF. rewrite /= -plus_assoc shr_locsE_shift.
+      assert (shr_locsE l (ty_size ty1) ## shr_locsE (l +ₗ (ty_size ty1)) (ty_size ty2 + 1))
+             by exact: shr_locsE_disj.
+      set_solver. }
+    iDestruct (na_own_acc with "Htl") as "[$ Htlclose]".
+    { generalize (shr_locsE_shift l ty1.(ty_size) ty2.(ty_size)). simpl. set_solver+. }
+    destruct (Qp_lower_bound q1 q2) as (qq & q'1 & q'2 & -> & ->). iExists qq, (vl1 +++ vl2).
+    iModIntro. rewrite vec_to_list_app heap_mapsto_vec_app vec_to_list_length.
+    iDestruct "Hmt1" as "[H↦1 H↦1f]". iDestruct "Hmt2" as "[H↦2 H↦2f]".
+    iFrame.
+    iSplitL "Hown1 Hown2".
+    { iIntros "!#" (l'). rewrite heap_mapsto_vec_app vec_to_list_length.
+      iDestruct 1 as "[Hmt1 Hmt2]". iSplitL "Hown1 Hmt1"; by [ iApply "Hown1" | iApply "Hown2" ]. }
+    iIntros "Htl [H1 H2]".
+    iDestruct ("Htlclose" with "Htl") as "Htl".
+    iCombine "H1" "H↦1f" as "H↦1". iCombine "H2" "H↦2f" as "H↦2".
+    iMod ("Hclose2" with "Htl H↦2") as "[Htl $]".
+    by iMod ("Hclose1" with "Htl H↦1") as "[Htl $]".
   Qed.
+  (* Global Instance product2_type_ne n: *)
+    (* Proper (type_dist2 n ==> type_dist2 n ==> type_dist2 n) product2. *)
+  (* Proof. solve_type_proper. Qed. *)
+
+  (* Global Instance product2_ne : *)
+  (*   NonExpansive2 product2. *)
+  (* Proof. *)
+  (*   constructor; *)
+  (*     solve_proper_core ltac:(fun _ => (eapply ty_size_ne; try reflexivity) || f_equiv). *)
+  (* Qed. *)
 
   Global Instance product2_mono E L:
     Proper (subtype E L ==> subtype E L ==> subtype E L) product2.
@@ -92,16 +108,16 @@ Section product.
     iIntros (ty11 ty12 H1 ty21 ty22 H2). iIntros (qL) "HL".
     iDestruct (H1 with "HL") as "#H1". iDestruct (H2 with "HL") as "#H2".
     iClear "∗". iIntros "!# #HE".
-    iDestruct ("H1" with "HE") as "#(% & #Ho1 & #Hs1)". clear H1.
+    iDestruct ("H1" with "HE") as (Hs1) "#(#Ho1 & #Hs1)". clear H1.
     iDestruct ("H2" with "HE") as "#(% & #Ho2 & #Hs2)". clear H2.
     iSplit; first by (iPureIntro; simpl; f_equal). iSplit; iAlways.
-    - iIntros (??) "H". iDestruct "H" as (vl1 vl2) "(% & Hown1 & Hown2)".
-      iExists _, _. iSplit. done. iSplitL "Hown1".
+    - iIntros (??) "[Hown1 Hown2]".
+      iSplitL "Hown1".
       + by iApply "Ho1".
-      + by iApply "Ho2".
+      + rewrite Hs1. by iApply "Ho2".
     - iIntros (???) "#[Hshr1 Hshr2]". iSplit.
       + by iApply "Hs1".
-      + rewrite -(_ : ty_size ty11 = ty_size ty12) //. by iApply "Hs2".
+      + rewrite Hs1. by iApply "Hs2".
   Qed.
   Global Instance product2_proper E L:
     Proper (eqtype E L ==> eqtype E L ==> eqtype E L) product2.
@@ -109,42 +125,12 @@ Section product.
 
   Global Instance product2_copy `{!Copy ty1} `{!Copy ty2} :
     Copy (product2 ty1 ty2).
-  Proof.
-    split; first (intros; apply _).
-    intros κ tid E F l q ? HF. iIntros "#LFT [H1 H2] Htl [Htok1 Htok2]".
-    iMod (@copy_shr_acc with "LFT H1 Htl Htok1") as (q1) "(Htl & H1 & Hclose1)"; first solve_ndisj.
-    { rewrite <-HF. apply shr_locsE_subseteq. simpl. clear. lia. }
-    iMod (@copy_shr_acc with "LFT H2 Htl Htok2") as (q2) "(Htl & H2 & Hclose2)"; first solve_ndisj.
-    { move: HF. rewrite /= -plus_assoc shr_locsE_shift.
-      assert (shr_locsE l (ty_size ty1) ## shr_locsE (l +ₗ (ty_size ty1)) (ty_size ty2 + 1))
-             by exact: shr_locsE_disj.
-      set_solver. }
-    iDestruct (na_own_acc with "Htl") as "[$ Htlclose]".
-    { generalize (shr_locsE_shift l ty1.(ty_size) ty2.(ty_size)). simpl. set_solver+. }
-    destruct (Qp_lower_bound q1 q2) as (qq & q'1 & q'2 & -> & ->). iExists qq.
-    iDestruct "H1" as (vl1) "[H↦1 H1]". iDestruct "H2" as (vl2) "[H↦2 H2]".
-    rewrite !split_prod_mt.
-    iDestruct (ty_size_eq with "H1") as "#>%".
-    iDestruct (ty_size_eq with "H2") as "#>%".
-    iDestruct "H↦1" as "[H↦1 H↦1f]". iDestruct "H↦2" as "[H↦2 H↦2f]".
-    iIntros "!>". iSplitL "H↦1 H1 H↦2 H2".
-    - iNext. iSplitL "H↦1 H1". iExists vl1. by iFrame. iExists vl2. by iFrame.
-    - iIntros "Htl [H1 H2]". iDestruct ("Htlclose" with "Htl") as "Htl".
-      iDestruct "H1" as (vl1') "[H↦1 H1]". iDestruct "H2" as (vl2') "[H↦2 H2]".
-      iDestruct (ty_size_eq with "H1") as "#>%".
-      iDestruct (ty_size_eq with "H2") as "#>%".
-      iCombine "H↦1" "H↦1f" as "H↦1". iCombine "H↦2" "H↦2f" as "H↦2".
-      rewrite !heap_mapsto_vec_op; [|congruence..].
-      iDestruct "H↦1" as "[_ H↦1]". iDestruct "H↦2" as "[_ H↦2]".
-      iMod ("Hclose2" with "Htl [H2 H↦2]") as "[Htl $]". by iExists _; iFrame.
-      iMod ("Hclose1" with "Htl [H1 H↦1]") as "[$$]". by iExists _; iFrame. done.
-  Qed.
+  Proof. split => /=. by rewrite ! copy_ty_copy.  Qed.
 
   Global Instance product2_send `{!Send ty1} `{!Send ty2} :
     Send (product2 ty1 ty2).
   Proof.
-    iIntros (tid1 tid2 vl) "H". iDestruct "H" as (vl1 vl2) "(% & Hown1 & Hown2)".
-    iExists _, _. iSplit; first done. iSplitL "Hown1"; by iApply @send_change_tid.
+    iIntros (tid1 tid2 vl) "[Hown1 Hown2]". iSplitL "Hown1"; by iApply @send_change_tid.
   Qed.
 
   Global Instance product2_sync `{!Sync ty1} `{!Sync ty2} :
@@ -163,10 +149,10 @@ Section product.
     ty_outlives_E (product [ty1; ty2]) ϝ = ty_outlives_E ty1 ϝ ++ ty_outlives_E ty2 ϝ.
   Proof. rewrite /product /ty_outlives_E /= fmap_app //. Qed.
 
-  Global Instance product_type_ne n: Proper (Forall2 (type_dist2 n) ==> type_dist2 n) product.
-  Proof. intros ??. induction 1=>//=. by f_equiv. Qed.
-  Global Instance product_ne : NonExpansive product.
-  Proof. intros ??. induction 1=>//=. by f_equiv. Qed.
+  (* Global Instance product_type_ne n: Proper (Forall2 (type_dist2 n) ==> type_dist2 n) product. *)
+  (* Proof. intros ??. induction 1=>//=. by f_equiv. Qed. *)
+  (* Global Instance product_ne : NonExpansive product. *)
+  (* Proof. intros ??. induction 1=>//=. by f_equiv. Qed. *)
   Global Instance product_mono E L:
     Proper (Forall2 (subtype E L) ==> subtype E L) product.
   Proof. intros ??. induction 1=>//=. by f_equiv. Qed.
@@ -200,25 +186,18 @@ Section typing.
   Global Instance prod2_assoc E L : Assoc (eqtype E L) product2.
   Proof.
     intros ???. apply eqtype_unfold. iIntros (?) "_ !# _".
-    iSplit; first by rewrite /= assoc. iSplit; iIntros "!# *"; iSplit; 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 (vl1 vl') "(% & H & Ho3)".
-      iDestruct "H" as (vl2 vl3) "(% & Ho1 & Ho2)". subst.
-      iExists _, _. iSplit. by rewrite -assoc. iFrame. iExists _, _. by iFrame.
-    - iDestruct "H" as "(Hs1 & Hs2 & Hs3)". rewrite shift_loc_assoc_nat.
-      by iFrame.
-    - iDestruct "H" as "[[Hs1 Hs2] Hs3]". rewrite /= shift_loc_assoc_nat.
-      by iFrame.
+    iSplit; first by rewrite /= assoc.
+    iSplit; iIntros "!# *"; iSplit;
+      try iIntros "(Hs1 & Hs2 & Hs3)"; try iIntros "[[Hs1 Hs2] Hs3]";
+        rewrite /= shift_loc_assoc_nat;iFrame.
   Qed.
 
   Global Instance prod2_unit_leftid E L : LeftId (eqtype E L) unit product2.
   Proof.
     intros ty. apply eqtype_unfold. iIntros (?) "_ !# _". iSplit; first done.
     iSplit; iIntros "!# *"; iSplit; iIntros "H".
-    - iDestruct "H" as (? ?) "(% & % & ?)". by subst.
-    - iExists [], _. eauto.
+    - iDestruct "H" as "(% & ?)". by rewrite shift_loc_0.
+    - rewrite /= shift_loc_0. by iFrame.
     - iDestruct "H" as "(? & ?)". rewrite shift_loc_0.
       iApply ty_shr_mono; last done.
       iApply lft_incl_refl.
@@ -229,8 +208,8 @@ Section typing.
   Proof.
     intros ty. apply eqtype_unfold. iIntros (?) "_ !# _".
     iSplit; first by rewrite /= -plus_n_O. iSplit; iIntros "!# *"; iSplit; iIntros "H".
-    - iDestruct "H" as (? ?) "(% & ? & %)". subst. by rewrite app_nil_r.
-    - iExists _, []. rewrite app_nil_r. eauto.
+    - by iDestruct "H" as "(? & %)".
+    - iFrame.
     - iDestruct "H" as "(? & _)". done.
     - simpl. iFrame.
   Qed.

theories/typing/type_context.v

@@ -8,11 +8,13 @@ Bind Scope expr_scope with path.
 (* TODO: Consider making this a pair of a path and the rest. We could
    then e.g. formulate tctx_elt_hasty_path more generally. *)
 Inductive tctx_elt `{!typeG Σ} : Type :=
+| TCtx_val (v : val) (ty : simple_type)
 | TCtx_hasty (p : path) (ty : type)
 | TCtx_blocked (p : path) (κ : lft) (ty : type).
 
 Notation tctx := (list tctx_elt).
 
+Notation "v ◁ᵥ ty" := (TCtx_val v ty%list%T) (at level 70).
 Notation "p ◁ ty" := (TCtx_hasty p ty%list%T) (at level 70).
 Notation "p ◁{ κ } ty" := (TCtx_blocked p κ ty)
    (at level 70, format "p  ◁{ κ }  ty").
@@ -21,32 +23,30 @@ Section type_context.
   Context `{!typeG Σ}.
   Implicit Types T : tctx.
 
-  Fixpoint eval_path (p : path) : option val :=
+  Fixpoint eval_path (p : path) : option loc :=
     match p with
     | BinOp OffsetOp e (Lit (LitInt n)) =>
       match eval_path e with
-      | Some (#(LitLoc l)) => Some (#(l +ₗ n))
+      | Some l => Some (l +ₗ n)
       | _ => None
       end
-    | e => to_val e
+    | Lit (LitLoc l) => Some l
+    | _ => None
     end.
 
-  Lemma eval_path_of_val (v : val) :
-    eval_path v = Some v.
-  Proof. destruct v. done. simpl. rewrite (decide_left _). done. Qed.
+  Lemma eval_path_of_loc (l : loc) :
+    eval_path #l = Some l.
+  Proof. done. Qed.
 
-  Lemma wp_eval_path E p v :
-    eval_path p = Some v → (WP p @ E {{ v', ⌜v' = v⌝ }})%I.
+  Lemma wp_eval_path E p l :
+    eval_path p = Some l → (WP p @ E {{ v', ⌜v' = #l⌝ }})%I.
   Proof.
-    revert v; induction p; intros v; try done.
-    { intros [=]. by iApply wp_value. }
-    { move=> /of_to_val=> ?. by iApply wp_value. }
+    revert l; induction p; intros v; try done.
+    { destruct l; intros [=]. iApply wp_value. by subst. }
     simpl. destruct op; try discriminate; [].
     destruct p2; try (intros ?; by iApply wp_value); [].
     destruct l; try (intros ?; by iApply wp_value); [].
     destruct (eval_path p1); try done.
-    destruct v0; try discriminate; [].
-    destruct l; try discriminate; [].
     intros [=<-]. wp_bind p1. iApply (wp_wand with "[]").
     { iApply IHp1. done. }
     iIntros (v) "%". subst v. wp_op. done.
@@ -57,26 +57,26 @@ Section type_context.
   Proof.
     intros Hpv. revert v Hpv.
     induction p as [| | |[] p IH [|[]| | | | | | | | | |] _| | | | | | | |]=>//.
-    - unfold eval_path=>? /of_to_val <-. apply is_closed_of_val.
-    - simpl. destruct (eval_path p) as [[[]|]|]; intros ? [= <-].
+    - simpl. destruct (eval_path p) => //. intros ? [= <-].
       specialize (IH _ eq_refl). apply _.
   Qed.
 
   (** Type context element *)
   Definition tctx_elt_interp (tid : thread_id) (x : tctx_elt) : iProp Σ :=
     match x with
-    | p ◁ ty => ∃ v, ⌜eval_path p = Some v⌝ ∗ ty.(ty_own) tid [v]
-    | p ◁{κ} ty => ∃ v, ⌜eval_path p = Some v⌝ ∗
-                             ([†κ] ={⊤}=∗ ty.(ty_own) tid [v])
+    | v ◁ᵥ ty => ty.(st_own) tid v
+    | p ◁ ty => ∃ l, ⌜eval_path p = Some l⌝ ∗ ty.(ty_own) tid l
+    | p ◁{κ} ty => ∃ l, ⌜eval_path p = Some l⌝ ∗
+                             ([†κ] ={⊤}=∗ ty.(ty_own) tid l)
     end%I.
 
   (* Block tctx_elt_interp from reducing with simpl when x is a constructor. *)
   Global Arguments tctx_elt_interp : simpl never.
 
-  Lemma tctx_hasty_val tid (v : val) ty :
-    tctx_elt_interp tid (v ◁ ty) ⊣⊢ ty.(ty_own) tid [v].
+  Lemma tctx_hasty_val tid (l : loc) ty :
+    tctx_elt_interp tid (#l ◁ ty) ⊣⊢ ty.(ty_own) tid l.
   Proof.
-    rewrite /tctx_elt_interp eval_path_of_val. iSplit.
+    rewrite /tctx_elt_interp eval_path_of_loc. iSplit.
     - iIntros "H". iDestruct "H" as (?) "[EQ ?]".
       iDestruct "EQ" as %[=->]. done.
     - iIntros "?". iExists _. auto.
@@ -87,20 +87,20 @@ Section type_context.
     tctx_elt_interp tid (p1 ◁ ty) ≡ tctx_elt_interp tid (p2 ◁ ty).
   Proof. intros Hp. rewrite /tctx_elt_interp /=. setoid_rewrite Hp. done. Qed.
 
-  Lemma tctx_hasty_val' tid p (v : val) ty :
-    eval_path p = Some v →
-    tctx_elt_interp tid (p ◁ ty) ⊣⊢ ty.(ty_own) tid [v].
+  Lemma tctx_hasty_val' tid p (l : loc) ty :
+    eval_path p = Some l →
+    tctx_elt_interp tid (p ◁ ty) ⊣⊢ ty.(ty_own) tid l.
   Proof.
     intros ?. rewrite -tctx_hasty_val. apply tctx_elt_interp_hasty_path.
-    rewrite eval_path_of_val. done.
+    rewrite eval_path_of_loc. done.
   Qed.
 
   Lemma wp_hasty E tid p ty Φ :
     tctx_elt_interp tid (p ◁ ty) -∗
-    (∀ v, ⌜eval_path p = Some v⌝ -∗ ty.(ty_own) tid [v] -∗ Φ v) -∗
+    (∀ l, ⌜eval_path p = Some l⌝ -∗ ty.(ty_own) tid l -∗ Φ #l) -∗
     WP p @ E {{ Φ }}.
   Proof.
-    iIntros "Hty HΦ". iDestruct "Hty" as (v) "[% Hown]".
+    iIntros "Hty HΦ". iDestruct "Hty" as (l) "[% Hown]".
     iApply (wp_wand with "[]"). { iApply wp_eval_path. done. }
     iIntros (v') "%". subst v'. iApply ("HΦ" with "[] Hown"). by auto.
   Qed.
@@ -134,16 +134,22 @@ Section type_context.
   Proof. rewrite /tctx_interp /= right_id //. Qed.
 
   (** Copy typing contexts *)
+  Definition tctx_elt_copy (x : tctx_elt) :=
+     match x with
+     | TCtx_val v ty => true
+     | TCtx_hasty p ty => ty.(ty_copy)
+     | TCtx_blocked p κ ty => ty.(ty_copy)
+     end.
+
   Class CopyC (T : tctx) :=
-    copyc_persistent tid : Persistent (tctx_interp tid T).
-  Global Existing Instances copyc_persistent.
+    copyc_persistent : Forall tctx_elt_copy T.
 
   Global Instance tctx_nil_copy : CopyC [].
-  Proof. rewrite /CopyC. apply _. Qed.
+  Proof. constructor. Qed.
 
   Global Instance tctx_ty_copy T p ty :
     CopyC T → Copy ty → CopyC ((p ◁ ty) :: T).
-  Proof. intros ???. rewrite tctx_interp_cons. apply _. Qed.
+  Proof. intros ??. constructor => //. by rewrite /= copy_ty_copy.  Qed.
 
   (** Send typing contexts *)
   Class SendC (T : tctx) :=
@@ -201,24 +207,25 @@ Section type_context.
     tctx_incl E L T1 T2 → tctx_incl E L (T1++T) (T2++T).
   Proof. by intros; apply tctx_incl_app. Qed.
 
-  Lemma copy_tctx_incl E L p `{!Copy ty} :
-    tctx_incl E L [p ◁ ty] [p ◁ ty; p ◁ ty].
-  Proof. iIntros (??) "_ _ $ * [#$ $] //". Qed.
+  (* TODO: is it a problem that the following two do not hold anymore? *)
+  (* Lemma copy_tctx_incl E L p `{!Copy ty} : *)
+  (*   tctx_incl E L [p ◁ ty] [p ◁ ty; p ◁ ty]. *)
+  (* Proof. iIntros (??) "_ _ $ * [#$ $] //". Qed. *)
 
-  Lemma copy_elem_of_tctx_incl E L T p `{!Copy ty} :
-    p ◁ ty ∈ T → tctx_incl E L T ((p ◁ ty) :: T).
-  Proof.
-    remember (p ◁ ty). induction 1 as [|???? IH]; subst.
-    - apply (tctx_incl_frame_r _ [_] [_;_]), copy_tctx_incl, _.
-    - etrans. by apply (tctx_incl_frame_l [_]), IH, reflexivity.
-      apply contains_tctx_incl, submseteq_swap.
-  Qed.
+  (* Lemma copy_elem_of_tctx_incl E L T p `{!Copy ty} : *)
+  (*   p ◁ ty ∈ T → tctx_incl E L T ((p ◁ ty) :: T). *)
+  (* Proof. *)
+  (*   remember (p ◁ ty). induction 1 as [|???? IH]; subst. *)
+  (*   - apply (tctx_incl_frame_r _ [_] [_;_]), copy_tctx_incl, _. *)
+  (*   - etrans. by apply (tctx_incl_frame_l [_]), IH, reflexivity. *)
+  (*     apply contains_tctx_incl, submseteq_swap. *)
+  (* Qed. *)
 
   Lemma subtype_tctx_incl E L p ty1 ty2 :
     subtype E L ty1 ty2 → tctx_incl E L [p ◁ ty1] [p ◁ ty2].
   Proof.
     iIntros (Hst ??) "#LFT #HE HL [H _]".
-    iDestruct "H" as (v) "[% H]". iDestruct (Hst with "HL HE") as "#(_ & Ho & _)". 
+    iDestruct "H" as (v) "[% H]". iDestruct (Hst with "HL HE") as "#(_ & Ho & _)".
     iFrame "HL". iApply big_sepL_singleton. iExists _. iFrame "%". by iApply "Ho".
   Qed.
 
@@ -230,14 +237,14 @@ Section type_context.
     tctx_extract_hasty E L p ty T T' →
     tctx_extract_hasty E L p ty (x::T) (x::T').
   Proof. unfold tctx_extract_hasty=>->. apply contains_tctx_incl, submseteq_swap. Qed.
-  Lemma tctx_extract_hasty_here_copy E L p1 p2 ty ty' T :
-    p1 = p2 → Copy ty → subtype E L ty ty' →
-    tctx_extract_hasty E L p1 ty' ((p2 ◁ ty)::T) ((p2 ◁ ty)::T).
-  Proof.
-    intros -> ??. apply (tctx_incl_frame_r _ [_] [_;_]).
-    etrans; first by apply copy_tctx_incl, _.
-    by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl.
-  Qed.
+  (* Lemma tctx_extract_hasty_here_copy E L p1 p2 ty ty' T : *)
+  (*   p1 = p2 → Copy ty → subtype E L ty ty' → *)
+  (*   tctx_extract_hasty E L p1 ty' ((p2 ◁ ty)::T) ((p2 ◁ ty)::T). *)
+  (* Proof. *)
+  (*   intros -> ??. apply (tctx_incl_frame_r _ [_] [_;_]). *)
+  (*   etrans; first by apply copy_tctx_incl, _. *)
+  (*   by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl. *)
+  (* Qed. *)
   Lemma tctx_extract_hasty_here E L p1 p2 ty ty' T :
     p1 = p2 → subtype E L ty ty' → tctx_extract_hasty E L p1 ty' ((p2 ◁ ty)::T) T.
   Proof.
@@ -311,7 +318,7 @@ Section type_context.
   Qed.
 End type_context.
 
-Hint Resolve tctx_extract_hasty_here_copy | 1 : lrust_typing.
+(* Hint Resolve tctx_extract_hasty_here_copy | 1 : lrust_typing. *)
 Hint Resolve tctx_extract_hasty_here | 20 : lrust_typing.
 Hint Resolve tctx_extract_hasty_further | 50 : lrust_typing.
 Hint Resolve tctx_extract_blocked_here tctx_extract_blocked_cons

theories/typing/util.v

@@ -21,13 +21,13 @@ Section util.
   Lemma delay_borrow_step :
     lfeE ⊆ N → (∀ x, Persistent (Post x)) →
     lft_ctx -∗ &{κ} P -∗
-      □ (∀ x, &{κ} P -∗ Pre x -∗ Frame x ={F1 x,F2 x}▷=∗ Post x ∗ Frame x) ={N}=∗ 
+      □ (∀ x, &{κ} P -∗ Pre x -∗ Frame x ={F1 x,F2 x}▷=∗ Post x ∗ Frame x) ={N}=∗
       □ (∀ x, Pre x -∗ Frame x ={F1 x,F2 x}▷=∗ Post x ∗ Frame x).
    *)
 
   Lemma delay_sharing_later N κ l ty tid :
     lftE ⊆ N →
-    lft_ctx -∗ &{κ}(▷ l ↦∗: ty_own ty tid) ={N}=∗
+    lft_ctx -∗ &{κ}(▷ ty_own ty tid l) ={N}=∗
        □ ∀ (F : coPset) (q : Qp),
        ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ (q).[κ] ={F,F ∖ ↑shrN}▷=∗ ty.(ty_shr) κ tid l ∗ (q).[κ].
   Proof.
@@ -49,7 +49,7 @@ Section util.
 
   Lemma delay_sharing_nested N κ κ' κ'' l ty tid :
     lftE ⊆ N →
-    lft_ctx -∗ ▷ (κ'' ⊑ κ ⊓ κ') -∗ &{κ'}(&{κ}(l ↦∗: ty_own ty tid)) ={N}=∗
+    lft_ctx -∗ ▷ (κ'' ⊑ κ ⊓ κ') -∗ &{κ'}(&{κ}(ty_own ty tid l)) ={N}=∗
        □ ∀ (F : coPset) (q : Qp),
        ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ (q).[κ''] ={F,F ∖ ↑shrN}▷=∗ ty.(ty_shr) κ'' tid l ∗ (q).[κ''].
   Proof.