## Stream: Coq users

### Topic: Decidable equality and countability on Σ types?

#### Ignat Insarov (Jun 19 2021 at 15:54):

I have some sigma types `{ℕ | ℕ → ℙ}` and I want to put them in a `gset`. How can I explain to Coq that numbers decorated with proofs are still countable and have decidable equality? _(I assume that this holds due to proof irrelevance.)_

Here is my code so far.

``````From stdpp Require Import
base
fin_sets
gmap
.

Notation ℕ := nat.
Notation ℙ := Prop.

Definition completeSet
(item: Type)
(hasHallmark: item → ℙ)
`{ EqDecision item
, Countable item
} := { s: gset item
| ∀anItem, hasHallmark anItem → anItem = anItem }.

Example exampleOfCompleteSet: completeSet ℕ even.
Proof.
unfold completeSet.
exists {[2]}.
intros. reflexivity. Qed.

Definition completeSet₂
(item: Type)
(hasHallmark: item → ℙ)
`{ EqDecision {anItem: item | hasHallmark anItem}
, Countable {anItem: item | hasHallmark anItem}
} := { s: gset {anItem: item | hasHallmark anItem}
| ∀anItem, hasHallmark anItem → anItem = anItem }.

Example anotherExampleOfCompleteSet: completeSet₂ ℕ even.
(*
Error:
Unable to satisfy the following constraints:

?EqDecision1 : "EqDecision {anItem : ℕ | (λ n : ℕ, Nat.even n) anItem}"

?H : "Countable {anItem : ℕ | (λ n : ℕ, Nat.even n) anItem}"
*)
``````

#### Gaëtan Gilbert (Jun 19 2021 at 16:07):

you define the appropriate `Instance`s

#### Ignat Insarov (Jun 19 2021 at 16:10):

``````Class RelDecision {A B} (R : A → B → Prop) :=
decide_rel x y :> Decision (R x y).
…
Notation EqDecision A := (RelDecision (=@{A})).
``````

So I must define `Coq.Init.Logic.eq` for my Σ type? Is it even legal?

#### Ignat Insarov (Jun 19 2021 at 16:12):

I do not understand what `decide_rel x y :> Decision (R x y)` means…

#### Ignat Insarov (Jun 19 2021 at 16:22):

This works:

``````Instance countableOnEvenℕ: Countable ({n: ℕ | even n}). Admitted.
``````

`EqDecision` arises automagically.

#### Ignat Insarov (Jun 19 2021 at 16:22):

Can I somehow make it work for any property, not only `even`?

#### Gaëtan Gilbert (Jun 19 2021 at 16:28):

``````Class RelDecision {A B} (R : A → B → Prop) :=
decide_rel x y :> Decision (R x y).
``````

is equivalent to

``````Definition RelDecision {A B} (R : A → B → Prop) := forall x y, Decision (R x y).
Instance decide_rel {A B} (R : A → B → Prop) (H:RelDecision R)  : forall x y, Decision (R x y) := H.
``````

#### Gaëtan Gilbert (Jun 19 2021 at 16:34):

Ignat Insarov said:

Can I somehow make it work for any property, not only `even`?

You could try proving it, I think you need the property to be decidable in order to get a countable sigma type though

#### Ignat Insarov (Jun 19 2021 at 16:39):

Maybe I can make a class for decidable properties and instantiate the properties I want to wield into that class…

#### Gaëtan Gilbert (Jun 19 2021 at 16:43):

https://gitlab.mpi-sws.org/iris/stdpp/-/blob/0a38be458cbfd571889b888fb27c8e4432fcaae9/theories/base.v#L315

#### Ignat Insarov (Jun 20 2021 at 08:29):

Wow, they really thought of everything!

Last updated: Jun 16 2024 at 01:42 UTC