证明Coq增加iota

我被卡在一个目标上。证明Coq增加iota

假设我们有如下定义：

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 n (iota n)假设In (S n) (iota n)。

来源

2017-07-23 Majha

正如你所观察到的事实是，在In n的n和一个在iota n是在你的语句步调一致，使归纳假设很难调用（如果不是完全没用）。

这里的诀窍是证明一个比你实际感兴趣的更一般的陈述，它打破了两个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

来源

2017-07-23 18:54:00 gallais

有趣 - 如何做一个当直觉看到什么时候某些事情不可能用当前的表述来证明时 - 是不是某些假设或归纳假设会直接（或间接）与结论相矛盾？或者是否存在“不够充分/强大”的归纳假设的概念？怎么能说出来？（这一点很明显，一旦你给我看，但自己搞清楚......） – Majha

大部分经验。但是，无论什么时候两件事情都在锁步中，或者一个值被固定为一个常数，并且阻止您使用归纳假设，这是一种强烈的气味，您可能想要寻找更一般的说法。 [这篇博客文章]（https://homes.cs.washington.edu/~jrw12/InductionExercises.html）设置了许多练习，你必须对归纳假设进行概括以使其发挥作用。你可能想看看它。 – gallais

非常感谢！基本上我需要“git gud”:)。 – Majha

证明Coq增加iota

回答

相关问题