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?
To resolve this issue you might want to set Debug Typeclasses option:
Set Typeclasses Debug.
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.