What is the correct way to define a DecidableType module?

Question

I have this type in Coq:

Inductive s_symb : Type :=
| s_symb_expr : nat -> s_symb 
| s_symb_fld : nat -> list string -> s_symb.

I want to create a MSetWeakList of s_symb, so I need to prove the type decidable. My usual routine, learnt from some StackOverflow articles, is along these lines:

From Coq Require Import MSets.MSetWeakList.
From Coq Require Import Structures.DecidableType.
From Coq Require Import Structures.DecidableTypeEx.

Module SSymb_as_MDT <: MiniDecidableType.
  Definition t := s_symb.

  Theorem eq_dec : forall s1 s2 : s_symb, { s1 = s2 } + { s1 <> s2 }.
  Proof.
    intro s1. induction s1. intro s2. destruct s2.
    - assert ({n = n0} + {n <> n0}) by apply Nat.eq_dec. sauto.
    - sauto.
    - intro s2. destruct s2.
      * assert ({n = n0} + {n <> n0}) by apply Nat.eq_dec. sauto.
      * assert ({n = n0} + {n <> n0}) by apply Nat.eq_dec. assert ({l = l0} + {l <> l0}) by apply ListString_as_MDT.eq_dec. sauto.
  Defined.
End SSymb_as_MDT.

Module SSymb_as_UDT <: UsualDecidableType := Make_UDT(SSymb_as_MDT).
Module SSymb_as_DT <: DecidableType := UDT_to_DT(SSymb_as_UDT).

Module SetSymb := MSetWeakList.Make(SSymb_as_DT).

Unfortunately this does not work: the last row is rejected with the error "The field eq_equiv is missing in SSymb_as_DT". So I read more StackOverflow and I learnt that I shall also define eq_equiv, a proof of the fact that the equality is an equivalence. I tried to add it to SSymb_as_MDT this way:

Module SSymb_as_MDT <: MiniDecidableType.
  Definition t := s_symb.
  Definition eq := @eq s_symb.

  Theorem eq_dec : forall s1 s2 : s_symb, { s1 = s2 } + { s1 <> s2 }.
  Proof. (* as above *)
  Defined.

  Theorem eq_equiv : Equivalence eq.
  Proof.
    split. congruence. congruence. congruence.
  Defined.
End SSymb_as_MDT.

but while Coq is happy with the definitions and the new proof, still the module SSymb_as_DT cannot see it, and I have the same error message. What shall I do for eq_equiv to be visible to SSymb_as_DT? As a second question, why eq_equiv was missing in first place? Shouldn't Make_UDT or UDT_to_DT add it in a somehow standard way?

Answer 1

You got confused because there are two definitions of DecidableType in the Coq standard library, and you happened to use the deprecated one.

You imported Structures.DecidableType which is deprecated. From its documentation:

NB: This file is here only for compatibility with earlier version of FSets and FMap. Please use Structures/Equalities.v directly now.

So replace the imports of DecidableType and DecidableTypeEx with

From Coq Require Import Structures.Equalities.

The actual DecidableType you need is a supertype of UsualDecidableType, which you got from Make_UDT.

Module SSymb_as_UDT <: UsualDecidableType := Make_UDT(SSymb_as_MDT).
Module SetSymb := MSetWeakList.Make(SSymb_as_UDT).