0

试图证明以下引理：

我已经尝试在目标中展开 nth_error 和 nth，但我无法找到一种方法来告诉 Coq 打破这两个函数的 Fixpoint 定义。我也尝试对 n 和列表进行归纳，但由于列表中的项目彼此无关，因此它们都无法解决问题。但这显然是一个正确的引理，现在我觉得它是不可证明的，任何人都可以帮我解决这个问题吗？非常感激！

Lemma nth_error_nth :
  forall nodes1 (node : node) n,
    n < length nodes1 ->
    nth_error nodes1 n = Some (nth n nodes1 node).
4

1 回答 1

2

您的问题确实应该被编辑以包含一个最小的、可重现的示例，这样我们就不需要猜测您使用的是什么定义。我假设您正在使用标准库的List模块，这node只是某种类型。如果没有更多信息，我将假设它类似于Variable node: Type.

为了证明这个引理，列表本身的归纳应该起作用。您可能还需要对n(try destruct n) 进行案例分析，因为n_th还有其他一些事情取决于是否n存在0。如果某件事似乎无法证明，请尝试加强归纳假设。这涉及在您使用induction. 您可以使用revert或根本不intro使用所讨论的假设来完成此操作。

您可能会得到一些荒谬的假设，例如 n < 0。您可以使用其中的一些引理PeanoNat.Nat从中得出矛盾。Search使用白话可能会有所帮助。例如，Search (?n < 0).找到我提到的引理。m < n您还需要从中得出结论的一步S m < S n，这可以通过 来完成Lt.lt_S_n。

只是为了让你开始，这里是一个证明的开始。

Lemma nth_error_nth :
  forall nodes1 (node : node) n,
    n < (length nodes1) ->
    nth_error nodes1 n = Some (nth n nodes1 node).
Proof.
  (* we don't intro n since we'll need to apply
     the inductive hypothesis to two different values of n *)
  intros nodes1 node.
  induction nodes1 as [ | a nodes1 IH].
于 2019-08-18T03:20:25.827 回答