证明基于固定点定义的引理

Question

试图证明以下引理：

我已经在目标中尝试了 unfold nth_error 和 nth，但我想不出一种方法来告诉 Coq 打破这两个函数的 Fixpoint 定义。我也尝试对 n 和列表进行归纳，但其中 none 能够解决问题，因为列表中的项目彼此无关。但这显然是一个正确的引理，现在我觉得无法证明，谁能帮我解决这个问题？非常感激！

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

Answer 1

您的问题确实应该进行编辑以包含 Minimal, Reproducible Example，这样我们就不需要猜测您使用的是什么定义。我假设您正在使用标准库的 List 模块并且 node 只是某种类型。在没有更多信息的情况下，我假设它类似于 Variable node: Type.

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

你可能会得到一些荒谬的假设，比如 n < 0。你可以使用 PeanoNat.Nat 中的一些引理从中得出矛盾。使用 Search 方言可能会有所帮助。例如，Search (?n < 0). 找到我提到的引理。还有一个步骤，您需要从 S m < S n 得出 m < 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].

证明基于固定点定义的引理

proof Lemma which based on Fixpoint definitions

coq

coq-tactic

proof-general