证明Coq中的iota不断增加

Question

我被一个目标卡住了。

假设我们有以下定义：

Fixpoint iota (n : nat) : list nat :=
  match n with
    | 0   => []
    | S k => iota k ++ [k]
  end.

我们想要证明：

Theorem t1 : forall n, In n (iota n) -> False.

到目前为止，我已经做到了以下几点：

Theorem t1 : forall n, In n (iota n) -> False.
Proof.
  intros.
  induction n.
    - cbn in H. contradiction.
    - cbn in H. apply app_split in H.
      Focus 2. unfold not. intros.
      unfold In in H0. destruct H0. assert (~(n = S n)) by now apply s_inj.
      contradiction.
      apply H0.
      apply IHn.

我使用了这两个引理，省略了证明：

Axiom app_split : forall A x (l l2 : list A), In x (l ++ l2) -> not (In x l2) -> In x l.
Axiom s_inj     : forall n, ~(n = S n).

然而，我完全被卡住了，我需要以某种方式证明这一点:假设In (S n) (iota n)为In n (iota n)。

Answer 1

正如您已经观察到的，In n中的n和iota n中的are在您的语句中步调一致，这使得归纳假设很难被引用(如果不是完全无用的话)。

这里的技巧是证明一个比您实际感兴趣的语句更一般的语句，它打破了两个n之间的依赖关系。我建议：

Theorem t : forall n k, n <= k -> In k (iota n) -> False.

您可以从其中推导出t1作为推论：

Corollary t1 : forall n, In n (iota n) -> False.
intro n; apply (t n n); reflexivity.
Qed.

如果你想偷看t的证明，你可以have a look at this self-contained gist