From 15b9474e6b255f893d38033d2d4a2dfed62f0405 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 1 Mar 2017 19:24:53 +0100
Subject: [PATCH] show all type-non-expansive functions to also be properly
 non-expansive

---
 theories/typing/fixpoint.v                    |  5 +++++
 theories/typing/product.v                     |  9 +++++++++
 theories/typing/sum.v                         | 20 ++++++++++++++++++-
 theories/typing/unsafe/cell.v                 |  5 +++++
 theories/typing/unsafe/refcell/refcell.v      | 16 +++++++++++++--
 theories/typing/unsafe/rwlock/rwlock.v        | 15 ++++++++++++--
 .../typing/unsafe/rwlock/rwlockreadguard.v    |  2 +-
 .../typing/unsafe/rwlock/rwlockwriteguard.v   |  2 +-
 8 files changed, 67 insertions(+), 7 deletions(-)

diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index bfe13041..308fb517 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -18,6 +18,11 @@ Section fixpoint_def.
   Definition type_fixpoint : type := fixpointK 2 T.
 End fixpoint_def.
 
+Lemma type_fixpoint_ne `{typeG Σ} (T1 T2 : type → type)
+  `{!TypeContractive T1, !TypeContractive T2} n :
+  (∀ t, T1 t ≡{n}≡ T2 t) → type_fixpoint T1 ≡{n}≡ type_fixpoint T2.
+Proof. eapply fixpointK_ne; apply type_contractive_ne, _. Qed.
+
 Section fixpoint.
   Context `{typeG Σ}.
   Context (T : type → type) {HT: TypeContractive T}.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 86916b7e..5a27d299 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -71,6 +71,13 @@ Section product.
     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.
   Proof.
@@ -141,6 +148,8 @@ Section product.
 
   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.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 0d598a27..ef3d107d 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -95,7 +95,7 @@ Section sum.
     - iApply ((nth i tyl ∅).(ty_shr_mono) with "Hord"); done.
   Qed.
 
-  Global Instance sum_type_ne n: Proper (Forall2 (type_dist2 n) ==> type_dist2 n) sum.
+  Global Instance sum_type_ne n : Proper (Forall2 (type_dist2 n) ==> type_dist2 n) sum.
   Proof.
     intros x y EQ.
     assert (EQmax : list_max (map ty_size x) = list_max (map ty_size y)).
@@ -113,6 +113,24 @@ Section sum.
       solve_proper_core ltac:(fun _ => exact:EQnth || f_type_equiv || f_equiv).
   Qed.
 
+  Global Instance sum_ne : NonExpansive sum.
+  Proof.
+    intros n x y EQ.
+    assert (EQmax : list_max (map ty_size x) = list_max (map ty_size y)).
+    { induction EQ as [|???? EQ _ IH]=>//=.
+      rewrite IH. f_equiv. apply EQ. }
+    (* TODO: If we had the right lemma relating nth, (Forall2 R) and R, we should
+       be able to make this more automatic. *)
+    assert (EQnth :∀ i, type_dist n (nth i x ∅) (nth i y ∅)).
+    { clear EQmax. induction EQ as [|???? EQ _ IH]=>-[|i] //=. }
+    constructor; simpl.
+    - by rewrite EQmax.
+    - intros tid vl. rewrite EQmax.
+      solve_proper_core ltac:(fun _ => exact:EQnth || f_equiv).
+    - intros κ tid l. unfold is_pad. rewrite EQmax.
+      solve_proper_core ltac:(fun _ => exact:EQnth || (eapply ty_size_ne; try reflexivity) || f_equiv).
+  Qed.
+
   Global Instance sum_mono E L :
     Proper (Forall2 (subtype E L) ==> subtype E L) sum.
   Proof.
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index b273af62..76dcf323 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -24,6 +24,11 @@ Section cell.
   Global Instance cell_type_ne : TypeNonExpansive cell.
   Proof. solve_type_proper. Qed.
 
+  Global Instance cell_ne : NonExpansive cell.
+  Proof.
+    constructor; solve_proper_core ltac:(fun _ => (eapply ty_size_ne; try reflexivity) || f_equiv).
+  Qed.
+
   Global Instance cell_mono E L : Proper (eqtype E L ==> subtype E L) cell.
   Proof.
     iIntros (?? EQ%eqtype_unfold) "#HE #HL".
diff --git a/theories/typing/unsafe/refcell/refcell.v b/theories/typing/unsafe/refcell/refcell.v
index 063fd5b1..aa8ee23e 100644
--- a/theories/typing/unsafe/refcell/refcell.v
+++ b/theories/typing/unsafe/refcell/refcell.v
@@ -49,12 +49,18 @@ Section refcell_inv.
              end
       end)%I.
 
-  Global Instance refcell_inv_ne n tid l γ α :
+  Global Instance refcell_inv_type_ne n tid l γ α :
     Proper (type_dist2 n ==> dist n) (refcell_inv tid l γ α).
   Proof. 
     solve_proper_core ltac:(fun _ => exact: type_dist2_S || f_type_equiv || f_contractive || f_equiv).
   Qed.
 
+  Global Instance refcell_inv_ne tid l γ α : NonExpansive (refcell_inv tid l γ α).
+  Proof.
+    intros n ???. (* TODO: f_equiv takes forever here, what is going on? *)
+    eapply refcell_inv_type_ne, type_dist_dist2. done.
+  Qed.
+
   Lemma refcell_inv_proper E L tid l γ α ty1 ty2 :
     eqtype E L ty1 ty2 →
     elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗
@@ -151,7 +157,13 @@ Section refcell.
   Global Instance refcell_type_ne : TypeNonExpansive refcell.
   Proof.
     constructor;
-      solve_proper_core ltac:(fun _ => exact: type_dist2_S || f_type_equiv || f_contractive || f_equiv).
+      solve_proper_core ltac:(fun _ => exact: type_dist2_S || (eapply refcell_inv_type_ne; try reflexivity) ||
+                                              f_type_equiv || f_contractive || f_equiv).
+  Qed.
+
+  Global Instance refcell_ne : NonExpansive refcell.
+  Proof.
+    constructor; solve_proper_core ltac:(fun _ => (eapply ty_size_ne; try reflexivity) || f_equiv).
   Qed.
 
   Global Instance refcell_mono E L : Proper (eqtype E L ==> subtype E L) refcell.
diff --git a/theories/typing/unsafe/rwlock/rwlock.v b/theories/typing/unsafe/rwlock/rwlock.v
index fcdfbe40..17772145 100644
--- a/theories/typing/unsafe/rwlock/rwlock.v
+++ b/theories/typing/unsafe/rwlock/rwlock.v
@@ -46,12 +46,17 @@ Section rwlock_inv.
       | _ => (* Locked for write. *) True
       end)%I.
 
-  Global Instance rwlock_inv_ne n tid l γ α :
+  Global Instance rwlock_inv_type_ne n tid l γ α :
     Proper (type_dist2 n ==> dist n) (rwlock_inv tid l γ α).
   Proof. 
     solve_proper_core ltac:(fun _ => exact: type_dist2_S || f_type_equiv || f_contractive || f_equiv).
   Qed.
 
+  Global Instance rwlock_inv_ne tid l γ α : NonExpansive (rwlock_inv tid l γ α).
+  Proof.
+    intros n ???. eapply rwlock_inv_type_ne, type_dist_dist2. done.
+  Qed.
+
   Lemma rwlock_inv_proper E L tid l γ α ty1 ty2 :
     eqtype E L ty1 ty2 →
     elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗
@@ -145,7 +150,13 @@ Section rwlock.
   Global Instance rwlock_type_ne : TypeNonExpansive rwlock.
   Proof.
     constructor;
-      solve_proper_core ltac:(fun _ => exact: type_dist2_S || f_type_equiv || f_contractive || f_equiv).
+      solve_proper_core ltac:(fun _ => exact: type_dist2_S || (eapply rwlock_inv_type_ne; try reflexivity) ||
+                                              f_type_equiv || f_contractive || f_equiv).
+  Qed.
+
+  Global Instance rwlock_ne : NonExpansive rwlock.
+  Proof.
+    constructor; solve_proper_core ltac:(fun _ => (eapply ty_size_ne; try reflexivity) || f_equiv).
   Qed.
 
   Global Instance rwlock_mono E L : Proper (eqtype E L ==> subtype E L) rwlock.
diff --git a/theories/typing/unsafe/rwlock/rwlockreadguard.v b/theories/typing/unsafe/rwlock/rwlockreadguard.v
index 9b773a27..01076b7a 100644
--- a/theories/typing/unsafe/rwlock/rwlockreadguard.v
+++ b/theories/typing/unsafe/rwlock/rwlockreadguard.v
@@ -64,7 +64,7 @@ Section rwlockreadguard.
   Global Instance rwlockreadguard_type_contractive α : TypeContractive (rwlockreadguard α).
   Proof.
     constructor;
-      solve_proper_core ltac:(fun _ => exact: type_dist2_S || (eapply rwlock_inv_ne; try reflexivity) ||
+      solve_proper_core ltac:(fun _ => exact: type_dist2_S || (eapply rwlock_inv_type_ne; try reflexivity) ||
                                               f_type_equiv || f_contractive || f_equiv).
   Qed.
   Global Instance rwlockreadguard_ne α : NonExpansive (rwlockreadguard α).
diff --git a/theories/typing/unsafe/rwlock/rwlockwriteguard.v b/theories/typing/unsafe/rwlock/rwlockwriteguard.v
index 9386c022..660d3fd9 100644
--- a/theories/typing/unsafe/rwlock/rwlockwriteguard.v
+++ b/theories/typing/unsafe/rwlock/rwlockwriteguard.v
@@ -76,7 +76,7 @@ Section rwlockwriteguard.
   Global Instance rwlockwriteguard_type_contractive α : TypeContractive (rwlockwriteguard α).
   Proof.
     constructor;
-      solve_proper_core ltac:(fun _ => exact: type_dist2_S || (eapply rwlock_inv_ne; try reflexivity) ||
+      solve_proper_core ltac:(fun _ => exact: type_dist2_S || (eapply rwlock_inv_type_ne; try reflexivity) ||
                                               f_type_equiv || f_contractive || f_equiv).
   Qed.
   Global Instance rwlockwriteguard_ne α : NonExpansive (rwlockwriteguard α).
-- 
GitLab