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

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 Debug Typeclasses.
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.）。

B.C 的 tutorial on typeclasses 非常好。皮尔斯你可能想看看。

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

Wrong Typeclass Instance used in Coq Proof

functional-programming

typeclass

theorem-proving

coq

dependent-type