From c0c4f210bb2de63fa0e062b0479a15eeabd907b7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de> Date: Mon, 24 Mar 2025 09:45:44 +0100 Subject: [PATCH 1/4] lft is EqDecision and Countable --- lifetime/lifetime_sig.v | 2 ++ lifetime/model/definitions.v | 3 +++ 2 files changed, 5 insertions(+) diff --git a/lifetime/lifetime_sig.v b/lifetime/lifetime_sig.v index 06af32be..095c9560 100644 --- a/lifetime/lifetime_sig.v +++ b/lifetime/lifetime_sig.v @@ -65,6 +65,8 @@ 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 bor_idx_inhabited : Inhabited bor_idx. Global Declare Instance lft_intersect_comm : Comm (A:=lft) eq (⊓). diff --git a/lifetime/model/definitions.v b/lifetime/model/definitions.v index 89a416db..900aad50 100644 --- a/lifetime/model/definitions.v +++ b/lifetime/model/definitions.v @@ -356,4 +356,7 @@ Proof. apply _. Qed. Global Definition atomic_lft_eq_dec : EqDecision atomic_lft := _. Global Definition atomic_lft_countable : Countable atomic_lft := _. +Global Definition lft_eq_dec : EqDecision lft := _. +Global Definition lft_countable : Countable lft := _. + End basic_properties. -- GitLab From 1b2301d2654450b99de60da9f41785580ed64df3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de> Date: Wed, 26 Mar 2025 15:34:38 +0100 Subject: [PATCH 2/4] move instances --- lifetime/model/definitions.v | 4 ---- lifetime/model/primitive.v | 2 ++ 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/lifetime/model/definitions.v b/lifetime/model/definitions.v index 900aad50..ee360cda 100644 --- a/lifetime/model/definitions.v +++ b/lifetime/model/definitions.v @@ -355,8 +355,4 @@ Proof. apply _. Qed. Global Definition atomic_lft_eq_dec : EqDecision atomic_lft := _. Global Definition atomic_lft_countable : Countable atomic_lft := _. - -Global Definition lft_eq_dec : EqDecision lft := _. -Global Definition lft_countable : Countable lft := _. - End basic_properties. diff --git a/lifetime/model/primitive.v b/lifetime/model/primitive.v index 3fd9472c..4f32bf11 100644 --- a/lifetime/model/primitive.v +++ b/lifetime/model/primitive.v @@ -303,6 +303,8 @@ 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 lft_intersect_comm : Comm (A:=lft) eq (⊓) := _. Local Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓) := _. -- GitLab From 5b4262a1a139f039bcc7408cf41b21394d77eab9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de> Date: Wed, 26 Mar 2025 15:39:02 +0100 Subject: [PATCH 3/4] add missing instances + group more sensibly --- lifetime/lifetime_sig.v | 9 +++++++-- lifetime/model/definitions.v | 1 + lifetime/model/primitive.v | 2 ++ 3 files changed, 10 insertions(+), 2 deletions(-) diff --git a/lifetime/lifetime_sig.v b/lifetime/lifetime_sig.v index 095c9560..451a0727 100644 --- a/lifetime/lifetime_sig.v +++ b/lifetime/lifetime_sig.v @@ -67,7 +67,14 @@ Module Type lifetime_sig. 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 (⊓). @@ -112,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 ee360cda..35fdc4a0 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 := _. End basic_properties. diff --git a/lifetime/model/primitive.v b/lifetime/model/primitive.v index 4f32bf11..a9104e8f 100644 --- a/lifetime/model/primitive.v +++ b/lifetime/model/primitive.v @@ -306,6 +306,8 @@ 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 From 1bffd3565302a8bd34293ca96caf29fa0edc3aa9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de> Date: Wed, 26 Mar 2025 15:40:55 +0100 Subject: [PATCH 4/4] restore blank --- lifetime/model/definitions.v | 1 + 1 file changed, 1 insertion(+) diff --git a/lifetime/model/definitions.v b/lifetime/model/definitions.v index 35fdc4a0..6f00d3d2 100644 --- a/lifetime/model/definitions.v +++ b/lifetime/model/definitions.v @@ -356,4 +356,5 @@ 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 := _. + End basic_properties. -- GitLab