start work towards equalizing: equality of lifetimes

theories/typing/lft_contexts.v

@@ -148,12 +148,12 @@ Section lft_contexts.
 
   (* Lifetime inclusion *)
 
-  (* There does not seem to be a need in the type system for
-     "equivalence" of lifetimes. If so, TODO : add it, and the
-     corresponding [Proper] instances for the relevent types. *)
   Definition lctx_lft_incl κ κ' : Prop :=
     elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗ κ ⊑ κ'.
 
+  Definition lctx_lft_eq κ κ' : Prop :=
+    lctx_lft_incl κ κ' ∧ lctx_lft_incl κ' κ.
+
   Lemma lctx_lft_incl_relf κ : lctx_lft_incl κ κ.
   Proof. iIntros "_ _". iApply lft_incl_refl. Qed.
 
@@ -164,6 +164,18 @@ Section lft_contexts.
     iApply (H1 with "HE HL"). iApply (H2 with "HE HL").
   Qed.
 
+  Global Instance lctx_lft_incl_proper :
+    Proper (lctx_lft_eq ==> lctx_lft_eq ==> iff) lctx_lft_incl.
+  Proof. intros ??[] ??[]. split; intros; by etrans; [|etrans]. Qed.
+
+  Global Instance lctx_lft_eq_equivalence : Equivalence lctx_lft_eq.
+  Proof.
+    split.
+    - by split.
+    - intros ?? Heq; split; apply Heq.
+    - intros ??? H1 H2. split; etrans; (apply H1 || apply H2).
+  Qed.
+
   Lemma lctx_lft_incl_static κ : lctx_lft_incl κ static.
   Proof. iIntros "_ _". iApply lft_incl_static. Qed.
 

theories/typing/shr_bor.v

@@ -26,9 +26,9 @@ Section shr_bor.
   Global Instance shr_mono_flip E L :
     Proper (lctx_lft_incl E L ==> flip (subtype E L) ==> flip (subtype E L)) shr_bor.
   Proof. intros ??????. by apply shr_mono. Qed.
-  Global Instance shr_proper E L κ :
-    Proper (eqtype E L ==> eqtype E L) (shr_bor κ).
-  Proof. intros ??[]. by split; apply shr_mono. Qed.
+  Global Instance shr_proper E L :
+    Proper (lctx_lft_eq E L ==> eqtype E L ==> eqtype E L) shr_bor.
+  Proof. intros ??[] ??[]. by split; apply shr_mono. Qed.
 
   Global Instance shr_contractive κ : Contractive (shr_bor κ).
   Proof.

theories/typing/uniq_bor.v

@@ -100,9 +100,9 @@ Section uniq_bor.
   Global Instance uniq_mono_flip E L :
     Proper (lctx_lft_incl E L ==> eqtype E L ==> flip (subtype E L)) uniq_bor.
   Proof. intros ??????. apply uniq_mono. done. by symmetry. Qed.
-  Global Instance uniq_proper E L κ :
-    Proper (eqtype E L ==> eqtype E L) (uniq_bor κ).
-  Proof. split; by apply uniq_mono. Qed.
+  Global Instance uniq_proper E L :
+    Proper (lctx_lft_eq E L ==> eqtype E L ==> eqtype E L) uniq_bor.
+  Proof. intros ??[]; split; by apply uniq_mono. Qed.
 
   Global Instance uniq_contractive κ : Contractive (uniq_bor κ).
   Proof.