调试专门研究和/或应用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 _)。