调试专门化和/或应用Coq中的错误

Question

我正试图用apply (list2map_not_in_default [(k, v)] i) in H2.命令找出以下错误的来源。

这里是list2map_not_in_default类型：

list2map_not_in_default
: forall (al : list (key * V)) (i : key),
~ (exists v : V, In (i, v) al) -> list2map al i = default

错误：

Error:
Unable to apply lemma of type
"~ (exists v0 : V, In (i, v0) [(k, v)]) -> list2map [(k, v)] i = default"
on hypothesis of type "~ (exists v : V, In (i, v) [(k, v)])".

或者apply (list2map_not_in_default [(k, v)] i) in H2.，可以被视为以下错误，从而您可以完全看到我的上下文。

Error:
In environment
V : Type
default : V
lo : key
l : tree
k : key
v : V
r : tree
hi : key
H0_ : SearchTree' lo l k
H0_0 : SearchTree' (S k) r hi
i : nat
Hleft : ~ (exists v : V, In (i, v) (slow_elements l))
H : i < k
H0 : k <> i
H1 : list2map (slow_elements l) i = default
H2 : ~ (exists v : V, In (i, v) [(k, v)])
The term "H2" has type "~ (exists v : V, In (i, v) [(k, v)])"
while it is expected to have type "~ (exists v0 : V, In (?i, v0) ?al)".

在前面的证明中，我使用了完全相同的引理specialize (list2map_not_in_default _ _ Hleft).，没有任何问题。

这适用于以下情况

V : Type
default : V
lo : key
l : tree
k : key
v : V
r : tree
hi : key
H0_ : SearchTree' lo l k
H0_0 : SearchTree' (S k) r hi
i : nat
Hleft : ~ (exists v : V, In (i, v) (slow_elements l))
H : i < k
H0 : k <> i
============================
list2map (slow_elements l ++ [(k, v)] ++ slow_elements r) i =
list2map (slow_elements l) i

通过所需的应用程序生成目标。

list2map (slow_elements l) i = default ->
list2map (slow_elements l ++ [(k, v)] ++ slow_elements r) i =
list2map (slow_elements l) i

这里发生了什么？关于如何修复它，有什么建议吗？

Answer 1

apply in使用的统一算法非常弱。对此你无能为力(除了打开错误报告并希望有人修复它(。只是用一些其他的策略。正如您已经注意到的，specialize工作得更好，因为您正在显式地编写lambda项。另一个类似的策略是assert (H3 := list2map_not_in_default _ _ Hleft)。或者你可以使用最具表现力的策略：(simple) refine (let H3 := list2map_not_in_default _ _ Hleft in _)。