Wrong Typeclass Instance used in Coq Proof

Question

I'm trying to perform the following proof based on Finite Maps as defined in CoqExtLib. However, I'm having a problem where the instance of RelDec showing up in the proof is different than the instance that I think is declared.

Require Import ExtLib.Data.Map.FMapAList.
Require ExtLib.Structures.Sets.
Module DSet := ExtLib.Structures.Sets.          
Require ExtLib.Structures.Maps.
Module Map := ExtLib.Structures.Maps.
Require Import ExtLib.Data.Nat.
Require Import Coq.Lists.List.

Definition Map k v := alist k v.
Definition loc := nat.
Definition sigma : Type := (Map loc nat).


Lemma not_in_sigma : forall (l l' : loc) (e : nat) (s : sigma),
    l <> l' ->
    Map.lookup l ((l',e)::s) = Map.lookup l s.
  intros. simpl. assert ( RelDec.rel_dec l l' = true -> l = l').
  pose (ExtLib.Core.RelDec.rel_dec_correct l l') as i. destruct i.

(*i := RelDec.rel_dec_correct l l' : RelDec.rel_dec l l' = true <-> l >= l'*)

As you can see, I'm trying to use the fact that rel_dec must evaluate to false if its two inputs are not equal. This seems to match the definition given in ExtLib.Data.Nat:

Global Instance RelDec_eq : RelDec (@eq nat) := { rel_dec := EqNat.beq_nat }.

However, in the code I showed above, it's using >= instead of = as the relation that the finite map is parameterized on, so I can't apply the theorem rel_dec_correct.

Why is this happening? How is the instance for RelDec being chosen? Is there something special I need to do when proving theorems about types qualified by typeclasses? How can I get a version of rel_dec_correct that applies to equality, not greater-than?

Anton Trunov Anton Trunov · Accepted Answer · 2018-07-20T19:56:42

To resolve this issue you might want to set Debug Typeclasses option:

Set Debug Typeclasses.
assert ( RelDec.rel_dec l l' = true -> l = l').

or, alternatively, use Set Printing Implicit to reveal the instances Coq has picked up.

The latter shows us that it is RelDec_ge as the goal now has the following form:

@RelDec.rel_dec loc ge RelDec_ge l l' = true -> l = l'

Apparently Coq chose the instance which is wrong for your purposes, however you can lock the relation you want like so:

assert ( RelDec.eq_dec l l' = true -> l = l').

Now apply (RelDec.rel_dec_correct l l'). resolves the goal, but pose won't work, since there is no information that would tie the goal to a useful instance. The pose tactic would just find an instance of RelDec nat <rel> (you can list all of them with this vernacular: Print Instances RelDec.RelDec.).

There is a very nice tutorial on typeclasses by B.C. Pierce you might want to have a look at.

Wrong Typeclass Instance used in Coq Proof

1 Answers