From d224fef76c5c4e76ee3107666e708c55d5142b04 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 14 Dec 2016 23:59:40 +0100
Subject: [PATCH] Simplify prood of sum_proper. Define LstCopy.

---
 theories/typing/product.v |  4 +---
 theories/typing/sum.v     | 15 ++++-----------
 theories/typing/type.v    | 15 ++++++++++-----
 3 files changed, 15 insertions(+), 19 deletions(-)

diff --git a/theories/typing/product.v b/theories/typing/product.v
index d8296966..cf23254f 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -127,9 +127,7 @@ Section product.
   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).
+  Global Instance product_copy tys : LstCopy tys → Copy (product tys).
   Proof. induction 1; apply _. Qed.
 End product.
 
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 02c67710..00b11cb0 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -110,18 +110,11 @@ Section sum.
   Global Instance sum_proper E L:
     Proper (Forall2 (eqtype E L) ==> eqtype E L) sum.
   Proof.
-    (* TODO: Isn't there sth. showing that Forall2 is monotnous wrt. the predicate? *)
-    intros tyl1 tyl2 Heq.
-    assert (Forall2 (subtype E L) tyl1 tyl2 ∧ Forall2 (subtype E L) tyl2 tyl1).
-    { induction Heq as [|???? Heq]; first done. destruct_and!.
-      destruct Heq. split; constructor; done. }
-    destruct_and!. split; apply sum_mono; done.
+    intros tyl1 tyl2 Heq; split; eapply sum_mono; [|rewrite -Forall2_flip];
+      (eapply Forall2_impl; [done|by intros ?? []]).
   Qed.
 
-  (* TODO : Make the Forall parameter a typeclass *)
-  (* TODO : This next step is suspuciously slow. *)
-  Global Instance sum_copy tyl :
-    Forall Copy tyl → Copy (sum tyl).
+  Global Instance sum_copy tyl: LstCopy tyl → Copy (sum tyl).
   Proof.
     intros HFA. split.
     - intros tid vl.
@@ -142,7 +135,7 @@ Section sum.
       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.
+            (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]".
diff --git a/theories/typing/type.v b/theories/typing/type.v
index ac870439..4e6f5c37 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -42,16 +42,21 @@ Section type.
     }.
   Global Existing Instances ty_shr_persistent.
 
-  Class Copy (t : type) := {
-    copy_persistent tid vl : PersistentP (t.(ty_own) tid vl);
+  Class Copy (ty : type) := {
+    copy_persistent tid vl : PersistentP (ty.(ty_own) tid vl);
     copy_shr_acc κ tid E F l q :
       mgmtE ∪ F ⊆ E →
-      lft_ctx -∗ t.(ty_shr) κ tid F l -∗
-        q.[κ] ∗ na_own tid F ={E}=∗ ∃ q', ▷l ↦∗{q'}: t.(ty_own) tid ∗
-          (▷l ↦∗{q'}: t.(ty_own) tid ={E}=∗ q.[κ] ∗ na_own tid F)
+      lft_ctx -∗ ty.(ty_shr) κ tid F l -∗
+        q.[κ] ∗ na_own tid F ={E}=∗ ∃ q', ▷l ↦∗{q'}: ty.(ty_own) tid ∗
+          (▷l ↦∗{q'}: ty.(ty_own) tid ={E}=∗ q.[κ] ∗ na_own tid F)
   }.
   Global Existing Instances copy_persistent.
 
+  Class LstCopy (tys : list type) := lst_copy : Forall Copy tys.
+  Global Instance lst_copy_nil : LstCopy [] := List.Forall_nil _.
+  Global Instance lst_copy_cons ty tys :
+    Copy ty → LstCopy tys → LstCopy (ty::tys) := List.Forall_cons _ _ _.
+
   (* We are repeating the typeclass parameter here jsut to make sure
      that simple_type does depend on it. Otherwise, the coercion defined
      bellow will not be acceptable by Coq. *)
-- 
GitLab