Have subtyping between product of uninit and uninit automatically proved.

theories/typing/product.v

@@ -6,13 +6,13 @@ Set Default Proof Using "Type".
 Section product.
   Context `{typeG Σ}.
 
-  Program Definition unit : type :=
+  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.
   Next Obligation. by iIntros (??????) "_ _ $". Qed.
   Next Obligation. by iIntros (????) "_ _ $". Qed.
 
-  Global Instance unit_copy : Copy unit.
+  Global Instance unit0_copy : Copy unit0.
   Proof.
     split. by apply _. iIntros (????????) "_ _ Htok $".
     iDestruct (na_own_acc with "Htok") as "[$ Htok]"; first set_solver+.
@@ -21,10 +21,10 @@ Section product.
     iIntros "Htok2 _". iApply "Htok". done.
   Qed.
 
-  Global Instance unit_send : Send unit.
+  Global Instance unit0_send : Send unit0.
   Proof. iIntros (tid1 tid2 vl) "H". done. Qed.
 
-  Global Instance unit_sync : Sync unit.
+  Global Instance unit0_sync : Sync unit0.
   Proof. iIntros (????) "_". done. Qed.
 
   Lemma split_prod_mt tid ty1 ty2 q l :
@@ -141,7 +141,8 @@ Section product.
     iIntros (κ tid1 ti2 l) "[#Hshr1 #Hshr2]". iSplit; by iApply @sync_change_tid.
   Qed.
 
-  Definition product := foldr product2 unit.
+  Definition product := foldr product2 unit0.
+  Definition unit := product [].
 
   Global Instance product_ne n: Proper (dist n ==> dist n) product.
   Proof. intros ??. induction 1=>//=. by f_equiv. Qed.
@@ -167,10 +168,9 @@ Section product.
   Definition product_cons ty tyl :
     product (ty :: tyl) = product2 ty (product tyl) := eq_refl _.
   Definition product_nil :
-    product [] = unit := eq_refl _.
+    product [] = unit0 := eq_refl _.
 End product.
 
-Arguments product : simpl never.
 Notation Π := product.
 
 Section typing.
@@ -232,5 +232,6 @@ Section typing.
   Proof. by rewrite -prod_flatten_r -prod_flatten_l. Qed.
 End typing.
 
+Arguments product : simpl never.
+Hint Opaque product : lrust_typing lrust_typing_merge.
 Hint Resolve product_mono' product_proper' : lrust_typing.
-Hint Opaque product : lrust_typing typeclass_instances.

theories/typing/product_split.v

@@ -70,7 +70,7 @@ Section product_split.
     clear Hp. destruct tyl.
     { iDestruct (elctx_interp_persist with "HE") as "#HE'".
       iDestruct (llctx_interp_persist with "HL") as "#HL'". iFrame "HE HL". 
-      iClear "IH Htyl". simpl. iExists #l. rewrite product_nil. iSplitR; first done.
+      iClear "IH Htyl". iExists #l. rewrite product_nil. iSplitR; first done.
       assert (eqtype E L (ptr ty) (ptr (product2 ty unit))) as [Hincl _].
       { rewrite right_id. done. }
       iDestruct (Hincl with "LFT HE' HL'") as "#(_ & #Heq & _)". by iApply "Heq". }
@@ -330,7 +330,7 @@ End product_split.
 
 (* We do not want unification to try to unify the definition of these
    types with anything in order to try splitting or merging. *)
-Hint Opaque own uniq_bor shr_bor product tctx_extract_hasty : lrust_typing lrust_typing_merge.
+Hint Opaque own uniq_bor shr_bor tctx_extract_hasty : lrust_typing lrust_typing_merge.
 
 (* We make sure that splitting is tried before borrowing, so that not
    the entire product is borrowed when only a part is needed. *)

theories/typing/tests/init_prod.v

@@ -21,8 +21,7 @@ Section rebor.
     apply type_fn; try apply _. move=> /= [] ret p. inv_vec p=>x y. simpl_subst.
     eapply type_deref; [solve_typing..|apply read_own_move|done|]=>x'. simpl_subst.
     eapply type_deref; [solve_typing..|apply read_own_move|done|]=>y'. simpl_subst.
-    eapply (type_new_subtype (Π[uninit 1; uninit 1])); [apply _|done| |].
-      { apply (uninit_product_subtype [1;1]%nat). }
+    eapply (type_new_subtype (Π[uninit 1; uninit 1])); [solve_typing..|].
       intros r. simpl_subst. unfold Z.to_nat, Pos.to_nat; simpl.
     eapply (type_assign (own 2 (uninit 1))); [solve_typing..|by apply write_own|].
     eapply type_assign; [solve_typing..|by apply write_own|].

theories/typing/tests/lazy_lft.v

@@ -25,8 +25,7 @@ Section lazy_lft.
   Proof.
     apply type_fn; try apply _. move=> /= [] ret p. inv_vec p. simpl_subst.
     eapply (type_newlft []); [solve_typing|]=>α.
-    eapply (type_new_subtype (Π[uninit 1;uninit 1])%T); [solve_typing..| |].
-      { apply (uninit_product_subtype [1;1]%nat). }
+    eapply (type_new_subtype (Π[uninit 1;uninit 1])); [solve_typing..|].
       intros t. simpl_subst.
     eapply type_new; [solve_typing..|]=>f. simpl_subst.
     eapply type_new; [solve_typing..|]=>g. simpl_subst.

theories/typing/uninit.v

@@ -45,39 +45,51 @@ Section uninit.
     eqtype E L (uninit0 n) (uninit n).
   Proof. apply equiv_eqtype; (split; first split)=>//=. apply uninit0_sz. Qed.
 
-  (* TODO : these lemmas cannot be used by [solve_typing], because
-     unification cannot infer the [ns] parameter. *)
-  Lemma uninit_product_eqtype {E L} ns :
-    eqtype E L (uninit (foldr plus 0%nat ns)) (Π(uninit <$> ns)).
+  Lemma uninit_product_subtype_cons {E L} (ntot n : nat) tyl :
+    n ≤ ntot →
+    subtype E L (uninit (ntot-n)) (Π tyl) →
+    subtype E L (uninit ntot) (Π(uninit n :: tyl)).
   Proof.
-    rewrite -uninit_uninit0_eqtype. etrans; last first.
-    { apply product_proper. eapply Forall2_fmap, Forall_Forall2, Forall_forall.
-      intros. by rewrite -uninit_uninit0_eqtype. }
-    induction ns as [|n ns IH]=>//=. revert IH.
-    by rewrite /= /uninit0 replicate_plus prod_flatten_l -!prod_app=>->.
+    intros ?%Nat2Z.inj_le Htyl. rewrite (le_plus_minus n ntot) // -!uninit_uninit0_eqtype
+      /uninit0 replicate_plus prod_flatten_l -!prod_app. do 3 f_equiv.
+    by rewrite <-Htyl, <-uninit_uninit0_eqtype.
   Qed.
-  Lemma uninit_product_eqtype' {E L} ns :
-    eqtype E L (Π(uninit <$> ns)) (uninit (foldr plus 0%nat ns)).
-  Proof. symmetry; apply uninit_product_eqtype. Qed.
-  Lemma uninit_product_subtype {E L} ns :
-    subtype E L (uninit (foldr plus 0%nat ns)) (Π(uninit <$> ns)).
-  Proof. apply uninit_product_eqtype'. Qed.
-  Lemma uninit_product_subtype' {E L} ns :
-    subtype E L (Π(uninit <$> ns)) (uninit (foldr plus 0%nat ns)).
-  Proof. apply uninit_product_eqtype. Qed.
+  Lemma uninit_product_subtype_cons' {E L} (ntot n : nat) tyl :
+    n ≤ ntot →
+    subtype E L (Π tyl) (uninit (ntot-n)) →
+    subtype E L (Π(uninit n :: tyl)) (uninit ntot).
+  Proof.
+    intros ?%Nat2Z.inj_le Htyl. rewrite (le_plus_minus n ntot) // -!uninit_uninit0_eqtype
+      /uninit0 replicate_plus prod_flatten_l -!prod_app. do 3 f_equiv.
+    by rewrite ->Htyl, <-uninit_uninit0_eqtype.
+  Qed.
+  Lemma uninit_product_eqtype_cons {E L} (ntot n : nat) tyl :
+    n ≤ ntot →
+    eqtype E L (uninit (ntot-n)) (Π tyl) →
+    eqtype E L (uninit ntot) (Π(uninit n :: tyl)).
+  Proof.
+    intros ? []. split.
+    - by apply uninit_product_subtype_cons.
+    - by apply uninit_product_subtype_cons'.
+  Qed.
+  Lemma uninit_product_eqtype_cons' {E L} (ntot n : nat) tyl :
+    n ≤ ntot →
+    eqtype E L (Π tyl) (uninit (ntot-n)) →
+    eqtype E L (Π(uninit n :: tyl)) (uninit ntot).
+  Proof. symmetry. by apply uninit_product_eqtype_cons. Qed.
 
   Lemma uninit_unit_eqtype E L :
     eqtype E L (uninit 0) unit.
-  Proof. apply (uninit_product_eqtype []). Qed.
+  Proof. by rewrite -uninit_uninit0_eqtype. Qed.
   Lemma uninit_unit_eqtype' E L :
-    subtype E L unit (uninit 0).
-  Proof. apply (uninit_product_eqtype' []). Qed.
+    eqtype E L unit (uninit 0).
+  Proof. by rewrite -uninit_uninit0_eqtype. Qed.
   Lemma uninit_unit_subtype E L :
     subtype E L (uninit 0) unit.
-  Proof. apply (uninit_product_subtype []). Qed.
+  Proof. by rewrite -uninit_uninit0_eqtype. Qed.
   Lemma uninit_unit_subtype' E L :
     subtype E L unit (uninit 0).
-  Proof. apply (uninit_product_subtype []). Qed.
+  Proof. by rewrite -uninit_uninit0_eqtype. Qed.
 
   Lemma uninit_own n tid vl :
     (uninit n).(ty_own) tid vl ⊣⊢ ⌜length vl = n⌝.
@@ -92,7 +104,7 @@ Section uninit.
   Qed.
 End uninit.
 
-Hint Resolve uninit_product_eqtype uninit_product_eqtype'
-     uninit_product_subtype uninit_product_subtype'
-     uninit_unit_eqtype uninit_unit_eqtype'
-     uninit_unit_subtype uninit_unit_subtype' : lrust_typing.
+Hint Resolve uninit_product_eqtype_cons uninit_product_eqtype_cons'
+             uninit_product_subtype_cons uninit_product_subtype_cons'
+             uninit_unit_eqtype uninit_unit_eqtype'
+             uninit_unit_subtype uninit_unit_subtype' : lrust_typing.