EqDec and Typeclasses (example for option types) · Coq users

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

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 :)

Gaëtan Gilbert (Apr 06 2021 at 09:01):

Do you already know what Coq's Program does? if not you are actually trying to learn 3 things at the same time

Gaëtan Gilbert (Apr 06 2021 at 09:03):

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

Andrés Goens (Apr 06 2021 at 09:09):

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

Stream: Coq users

Topic: EqDec and Typeclasses (example for option types)

Andrés Goens (Apr 06 2021 at 08:03):

Gaëtan Gilbert (Apr 06 2021 at 09:01):

Gaëtan Gilbert (Apr 06 2021 at 09:03):

Andrés Goens (Apr 06 2021 at 09:09):