add Countable instance for decidable Sigma types

This instance became useful when working with, e.g., a type for elements of a set { a : A | a ∈ X } and wanting to construct a gmap with this domain.

Thanks for the MR, this is a very sensible instance.

I think the code can be shortened using a.) inj_countable and b.) guard:

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.

(This also uses option_guard_True_pi, which is part of !256 (merged).)

!256 (merged) has been merged. Can you update this MR? Thanks :).

Sure; do you want to have the Decision, ProofIrrel, ... assumptions on the Instance signature rather than as Context implicits? E.g. inj_countable is defined in a Section with Context implicits. Is there a system to when one approach is taken over the other?

added 18 commits

• 21700125...f7c9c556 - 17 commits from branch iris:master
• 1fb8aa47 - add Countable instance for decidable Sigma types

Compare with previous version

Anyway, updated now.

resolved all threads

merged

mentioned in commit 02e61349