Coq anomaly

theories/typing/product.v

@@ -83,10 +83,11 @@ Section product.
     Proper (eqtype E L ==> eqtype E L ==> eqtype E L) product2.
   Proof. by intros ??[]??[]; split; apply product2_mono. Qed.
 
-  Global Program Instance product2_copy `(!Copy ty1) `(!Copy ty2) :
+  Global Instance product2_copy `(!Copy ty1) `(!Copy ty2) :
     Copy (product2 ty1 ty2).
-  Next Obligation.
-    intros ty1 ? ty2 ? κ tid E F l q ?. iIntros "#LFT H [[Htok1 Htok2] Htl]".
+  Proof.
+    split; first (intros; apply _).
+    intros κ tid E F l q ?. iIntros "#LFT H [[Htok1 Htok2] Htl]".
     iDestruct "H" as (E1 E2) "(% & H1 & H2)".
     assert (F = E1 ∪ E2 ∪ F∖(E1 ∪ E2)) as ->.
     { rewrite -union_difference_L; set_solver. }

theories/typing/sum.v

@@ -79,41 +79,53 @@ Section sum.
     - by iApply (frac_bor_shorten with "Hord").
   Qed.
 
+  Global Instance sum_mono E L:
+    Proper (Forall2 (subtype E L) ==> subtype E L) sum.
+  Proof.
+    intros tyl1 tyl2 Htyl. iIntros "#LFT #? %". iSplit; last (iSplit; iAlways).
+    - simpl. iInduction Htyl as l "IH". induction Htyl; first done. iPureIntro. do 2 f_equal. 
+      simpl. f_equal; last done.
+
+  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.
+
+
+  *)
   (* TODO : Make the Forall parameter a typeclass *)
   (* TODO : This next step is suspuciously slow. *)
-  Global Program Instance sum_copy tyl :
+  Global Instance sum_copy tyl :
     Forall Copy tyl → Copy (sum tyl).
-  Next Obligation.
-    intros tyl HFA tid vl.
-    cut (∀ i vl', PersistentP (ty_own (nth i tyl ∅) tid vl')). by apply _.
-    intros. apply @copy_persistent. edestruct nth_in_or_default as [| ->];
-      [by eapply List.Forall_forall| apply _].
-  Qed.
-  Next Obligation.
-    intros tyl HFA κ tid E F l q ?.
-    iIntros "#LFT #H[[Htok1 [Htok2 Htok3]] Htl]".
-    setoid_rewrite split_sum_mt. iDestruct "H" as (i) "[Hshr0 [Hshr Hshrtail]]".
-    iMod (frac_bor_acc with "LFT Hshr0 Htok1") as (q'1) "[Hown Hclose]". set_solver.
-    iMod (frac_bor_acc with "LFT Hshrtail Htok2") as (q'2) "[Htail Hclose']". set_solver.
-    iMod (@copy_shr_acc _ _ (nth i tyl ∅) with "LFT Hshr [Htok3 $Htl]")
-      as (q'3) "[Hownq Hclose'']"; try done.
-    { edestruct nth_in_or_default as [| ->]; last by apply _.
-        by eapply List.Forall_forall. }
-    destruct (Qp_lower_bound q'1 q'2) as (q'0 & q'01 & q'02 & -> & ->).
-    destruct (Qp_lower_bound q'0 q'3) as (q' & q'11 & q'12 & -> & ->).
-    rewrite -(heap_mapsto_vec_prop_op _ q' q'12); last (by intros; apply ty_size_eq).
-    rewrite -!Qp_plus_assoc.
-    rewrite -(heap_mapsto_vec_prop_op _ q' (q'11 + q'02)
-        (list_max (map ty_size tyl) - (ty_size (nth i tyl ∅)))%nat); last first.
-    { intros. iIntros (<-). iPureIntro. by rewrite minus_plus. }
-    iDestruct "Hownq" as "[Hownq1 Hownq2]". iDestruct "Hown" as "[Hown1 >Hown2]".
-    iDestruct "Htail" as "[Htail1 Htail2]".
-    iExists q'. iModIntro. iSplitL "Hown1 Hownq1 Htail1".
-    - iNext. iExists i. by iFrame.
-    - iIntros "H". iDestruct "H" as (i') "[>Hown1 [Hownq1 Htail1]]".
-      iDestruct (heap_mapsto_agree with "[$Hown1 $Hown2]") as %[= ->%Z_of_nat_inj].
-      iMod ("Hclose''" with "[$Hownq1 $Hownq2]"). iMod ("Hclose'" with "[$Htail1 $Htail2]").
-      iMod ("Hclose" with "[$Hown1 $Hown2]") as "$". by iFrame.
+  Proof.
+    intros HFA. split.
+    - intros tid vl.
+      cut (∀ i vl', PersistentP (ty_own (nth i tyl ∅) tid vl')). by apply _.
+      intros. apply @copy_persistent. edestruct nth_in_or_default as [| ->];
+                                        [by eapply List.Forall_forall| apply _].
+    - intros κ tid E F l q ?.
+      iIntros "#LFT #H[[Htok1 [Htok2 Htok3]] Htl]".
+      setoid_rewrite split_sum_mt. iDestruct "H" as (i) "[Hshr0 [Hshr Hshrtail]]".
+      iMod (frac_bor_acc with "LFT Hshr0 Htok1") as (q'1) "[Hown Hclose]". set_solver.
+      iMod (frac_bor_acc with "LFT Hshrtail Htok2") as (q'2) "[Htail Hclose']". set_solver.
+      iMod (@copy_shr_acc _ _ (nth i tyl ∅) with "LFT Hshr [Htok3 $Htl]")
+        as (q'3) "[Hownq Hclose'']"; try done.
+      { edestruct nth_in_or_default as [| ->]; last by apply _.
+          by eapply List.Forall_forall. }
+      destruct (Qp_lower_bound q'1 q'2) as (q'0 & q'01 & q'02 & -> & ->).
+      destruct (Qp_lower_bound q'0 q'3) as (q' & q'11 & q'12 & -> & ->).
+      rewrite -(heap_mapsto_vec_prop_op _ q' q'12); last (by intros; apply ty_size_eq).
+      rewrite -!Qp_plus_assoc.
+      rewrite -(heap_mapsto_vec_prop_op _ q' (q'11 + q'02)
+                                        (list_max (map ty_size tyl) - (ty_size (nth i tyl ∅)))%nat); last first.
+      { intros. iIntros (<-). iPureIntro. by rewrite minus_plus. }
+      iDestruct "Hownq" as "[Hownq1 Hownq2]". iDestruct "Hown" as "[Hown1 >Hown2]".
+      iDestruct "Htail" as "[Htail1 Htail2]".
+      iExists q'. iModIntro. iSplitL "Hown1 Hownq1 Htail1".
+      + iNext. iExists i. by iFrame.
+      + iIntros "H". iDestruct "H" as (i') "[>Hown1 [Hownq1 Htail1]]".
+        iDestruct (heap_mapsto_agree with "[$Hown1 $Hown2]") as %[= ->%Z_of_nat_inj].
+        iMod ("Hclose''" with "[$Hownq1 $Hownq2]"). iMod ("Hclose'" with "[$Htail1 $Htail2]").
+        iMod ("Hclose" with "[$Hown1 $Hown2]") as "$". by iFrame.
   Qed.
 End sum.