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}"
*)
```

you define the appropriate `Instance`

s

```
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?

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

means…

This works:

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

`EqDecision`

arises automagically.

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

?

```
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.
```

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

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

Wow, they really thought of everything!

Last updated: Jun 16 2024 at 01:42 UTC