From 1fb8aa4751240634a87cc4703d0f55c23167b90f Mon Sep 17 00:00:00 2001
From: Simon Gregersen <gregersen@cs.au.dk>
Date: Sat, 24 Apr 2021 12:45:56 +0200
Subject: [PATCH] add Countable instance for decidable Sigma types

---
 theories/countable.v | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/theories/countable.v b/theories/countable.v
index 689ff40a..b1cbe454 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -340,3 +340,12 @@ Next Obligation.
   intros T ?? t.
   by rewrite <-(right_id_L [] _ (gen_tree_to_list _)), gen_tree_of_to_list.
 Qed.
+
+(** ** Sigma *)
+Program Instance countable_sig `{Countable A} (P : A → Prop)
+        `{!∀ x, Decision (P x), !∀ x, ProofIrrel (P x)} :
+  Countable { x : A | P x } :=
+  inj_countable proj1_sig (λ x, guard (P x) as Hx; Some (x ↾ Hx)) _.
+Next Obligation.
+  intros A ?? P ?? [x Hx]. by erewrite (option_guard_True_pi (P x)).
+Qed.
-- 
GitLab