From cffd3c7050aef19940805c0c805a65c355359961 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 23 Mar 2017 09:40:14 +0100
Subject: [PATCH] Rc is type contractive
---
theories/typing/lib/rc.v | 18 ++++++++++++++++++
1 file changed, 18 insertions(+)
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index 09f45a88..badc241e 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -36,6 +36,13 @@ Section rc.
| None => True
end)%I.
+ Global Instance rc_type_ne n :
+ Proper (type_dist2 n ==> dist n) (rc_inv tid ν γ l).
+ Proof.
+ solve_proper_core
+ ltac:(fun _ => exact: type_dist2_S || f_type_equiv || f_contractive || f_equiv).
+ Qed.
+
Program Definition rc (ty : type) :=
{| ty_size := 1;
ty_own tid vl :=
@@ -122,6 +129,17 @@ Section rc.
- by iApply lft_incl_trans.
- by iApply na_bor_shorten.
Qed.
+
+ Global Instance rc_type_contractive : TypeContractive rc.
+ Proof.
+ constructor;
+ 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 rc_ne : NonExpansive rc.
+ Proof. apply type_contractive_ne, _. Qed.
+
End rc.
Section code.
--
GitLab