Hi! I'm pretty new to Coq and I'm trying to figure out decidable equality and typeclasses at the same time. Coming from 'informal' mathematics where equality is not as complex as in type theory, I'm still a bit confused. While the HoTT book makes a great job at explaining the different notions of equality in type theory, I was surprised I couldn't find anything discussing the EqDec typeclass in Coq specifically (not in the Coq resources at least). Did I miss anything? Could someone point out a good resource for this?

At any case, I'm trying to define an instance for the option type, which should be simple enough. This is my attempt so far (after importing `Program.Utils`

, `Classes.Equivalence`

and `Classes.EquivDec`

):

```
Program Instance option_eqdec {A : Type} `{EqDec A} : EqDec (option A) eq := {
equiv_dec s1 s2 :=
match s1,s2 with
| None, None => in_left (*s1 === s2 *)
| None, Some _ => in_right (*s1 =/= s2*)
| Some x, None => in_right (*s1 =/= s2*)
| Some x, Some y => if x == y then in_left else in_right
end
}.
```

While Coq seems to be happy with this, it does spit out some strange messages:

```
tion_eqdec has type-checked, generating 5 obligations
Solving obligations automatically...
option_eqdec_obligation_2 is defined
option_eqdec_obligation_3 is defined
3 obligations remaining
Obligation 1 of option_eqdec:
(forall (A : Type) (R0 : Relation_Definitions.relation A) (equiv0 : Equivalence R0),
EqDec A R0 -> forall s1 s2 : option A, None = s1 -> None = s2 -> s1 === s2).
Obligation 4 of option_eqdec:
(forall (A : Type) (R0 : Relation_Definitions.relation A) (equiv0 : Equivalence R0),
EqDec A R0 -> forall (s1 s2 : option A) (x y : A), Some x = s1 -> Some y = s2 -> x === y -> s1 === s2).
Obligation 5 of option_eqdec:
(forall (A : Type) (R0 : Relation_Definitions.relation A) (equiv0 : Equivalence R0),
EqDec A R0 -> forall (s1 s2 : option A) (x y : A), Some x = s1 -> Some y = s2 -> x =/= y -> s1 =/= s2).
```

I'm not sure if this definition is working there. I can't get Coq to actually decide equality for two terms, like:

```
Eval simpl in None == Some 0.
```

On the other hand, it has the same behavior if I leave out the option types, with something like:

```
Eval simpl in 1 == 0.
```

This also won't show me the decision of equality, both leave the `equiv_dec`

function applied to both terms and the sum type showing both. Maybe this is just because it won't show me which constructor it uses? At any case, should I worry about those obligations? Does this definition make any sense? Why is this instance for option not defined anywhere, or did I just miss it? It seems like a very 'standard' thing to do. I'm just trying to make sense of all of this :)

Hi! I'm pretty new to Coq and I'm trying to figure out decidable equality and typeclasses at the same time.

Do you already know what Coq's `Program`

does? if not you are actually trying to learn 3 things at the same time

if Program says `obligations remaining`

it means you have to do `Next Obligation`

and prove the goals it opens before your instance will be defined

I guess I'm actually trying to learn 3 things at the same time then :sweat_smile: thanks for the pointers!

Last updated: Oct 08 2024 at 16:02 UTC