代码之家 › 专栏 › 技术社区 › jmite

在COQ证明中使用了错误的typeclass实例

theorem-proving dependent-type typeclass coq functional-programming

1

jmite · 技术社区 · 7 年前

我正在尝试根据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实例?当证明typeclasses限定的类型的定理时,我是否需要做一些特殊的事情?我怎样才能得到 rel_dec_正确 这适用于平等,不大于?

1 回复 | 直到 7 年前

1

Anton Trunov 7 年前

要解决此问题,您可能需要设置 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 不起作用,因为没有任何信息可以将目标与有用的实例联系起来。这个 姿势 战术只会找到一个例子 RelDec nat <rel> (你可以用这个白话文列出所有这些: Print Instances RelDec.RelDec. )

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