From facab8cdf5ea1b08e467f8ad3541f01e9cc960e2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <gaeher@mpi-sws.org>
Date: Wed, 26 Mar 2025 14:41:30 +0000
Subject: [PATCH] lft is EqDecision and Countable

---
 lifetime/lifetime_sig.v      | 11 +++++++++--
 lifetime/model/definitions.v |  1 +
 lifetime/model/primitive.v   |  4 ++++
 3 files changed, 14 insertions(+), 2 deletions(-)

diff --git a/lifetime/lifetime_sig.v b/lifetime/lifetime_sig.v
index 06af32be..451a0727 100644
--- a/lifetime/lifetime_sig.v
+++ b/lifetime/lifetime_sig.v
@@ -65,7 +65,16 @@ Module Type lifetime_sig.
 
   (** * Instances *)
   Global Declare Instance lft_inhabited : Inhabited lft.
+  Global Declare Instance lft_eq_dec : EqDecision lft.
+  Global Declare Instance lft_countable : Countable lft.
+
+  Global Declare Instance atomic_lft_inhabited : Inhabited atomic_lft.
+  Global Declare Instance atomic_lft_eq_dec : EqDecision atomic_lft.
+  Global Declare Instance atomic_lft_countable : Countable atomic_lft.
+
   Global Declare Instance bor_idx_inhabited : Inhabited bor_idx.
+  Global Declare Instance bor_idx_eq_dec : EqDecision bor_idx.
+  Global Declare Instance bor_idx_countable : Countable bor_idx.
 
   Global Declare Instance lft_intersect_comm : Comm (A:=lft) eq (⊓).
   Global Declare Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓).
@@ -110,8 +119,6 @@ Module Type lifetime_sig.
   Global Declare Instance atomic_lft_to_lft_inj : Inj eq eq atomic_lft_to_lft.
   Global Declare Instance positive_to_atomic_lft_inj : Inj eq eq positive_to_atomic_lft.
 
-  Global Declare Instance atomic_lft_eq_dec : EqDecision atomic_lft.
-  Global Declare Instance atomic_lft_countable : Countable atomic_lft.
 
   (** * Laws *)
   Parameter lft_tok_sep : ∀ q κ1 κ2, q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ⊓ κ2].
diff --git a/lifetime/model/definitions.v b/lifetime/model/definitions.v
index 89a416db..6f00d3d2 100644
--- a/lifetime/model/definitions.v
+++ b/lifetime/model/definitions.v
@@ -353,6 +353,7 @@ Qed.
 Global Instance positive_to_atomic_lft_inj : Inj eq eq positive_to_atomic_lft.
 Proof. apply _. Qed.
 
+Global Definition atomic_lft_inhabited : Inhabited atomic_lft := _.
 Global Definition atomic_lft_eq_dec : EqDecision atomic_lft := _.
 Global Definition atomic_lft_countable : Countable atomic_lft := _.
 
diff --git a/lifetime/model/primitive.v b/lifetime/model/primitive.v
index 3fd9472c..a9104e8f 100644
--- a/lifetime/model/primitive.v
+++ b/lifetime/model/primitive.v
@@ -303,7 +303,11 @@ Qed.
 
 (** Basic rules about lifetimes  *)
 Local Instance lft_inhabited : Inhabited lft := _.
+Local Instance lft_eq_dec : EqDecision lft := _.
+Local Instance lft_countable : Countable lft := _.
 Local Instance bor_idx_inhabited : Inhabited bor_idx := _.
+Local Instance bor_idx_eq_dec : EqDecision bor_idx := _.
+Local Instance bor_idx_countable : Countable bor_idx := _.
 Local Instance lft_intersect_comm : Comm (A:=lft) eq (⊓) := _.
 Local Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓) := _.
 Local Instance lft_intersect_inj_1 κ : Inj eq eq (κ ⊓.) := _.
-- 
GitLab