Coq Proof 中使用了错误的类型类实例

Question

我正在尝试基于 CoqExtLib 中定义的有限映射来执行以下证明。但是，我遇到一个问题，证明中显示的

RelDec

实例与我认为声明的实例不同。

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'*)

如您所见，我正在尝试利用这样一个事实：如果

rel_dec

的两个输入不相等，则它必须评估为 false。这似乎与 ExtLib.Data.Nat 中给出的定义匹配：

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

但是，在我上面展示的代码中，它使用

>=

而不是

=

作为有限映射参数化的关系，所以我无法应用定理

rel_dec_correct

。

为什么会发生这种情况？如何选择 RelDec 的实例？在证明有关由类型类限定的类型的定理时，我需要做一些特别的事情吗？如何获得适用于相等而不是大于的

rel_dec_correct

版本？

Answer 1

要解决此问题，您可能需要设置

Debug Typeclasses

选项：

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

或者，使用

Set Printing Implicit

显示 Coq 已拾取的实例。

后者向我们表明它是

RelDec_ge

，因为目标现在具有以下形式：

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

显然 Coq 选择了不适合您目的的实例，但是您可以像这样锁定您想要的关系：

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

现在

apply (RelDec.rel_dec_correct l l').

解决了目标，但是

pose

不起作用，因为没有任何信息可以将目标与有用的实例联系起来。

pose

策略只会找到

RelDec nat <rel>

的一个实例（您可以用这种白话列出所有它们：

Print Instances RelDec.RelDec.

）。

BC 有一个非常好的 关于类型类的教程皮尔斯你可能想看看。