用 Coq 中的列表证明

Question

我试图在 CoqIDE（学校）中证明一些东西。我挡住了一步，这是

`Print length. (* la longueur de listes *)


Lemma mystere A:  forall l : list A, length l = 0 <-> l = nil.
intros.
destruct l.
* split.
- intros.
reflexivity.
- intros. 
simpl.
reflexivity.
* split.
- intros.
???? <- I have tried many things, but without success..
Admitted.
`

谢谢各位的考虑！

Answer 1

你的上下文有一个假设

H : length (a :: l) = 0

这是荒谬的，因为length (a :: l)是继任者。您可以通过运行simpl in *或看到这一点simpl in H，这会导致

H : S (length l) = 0

如果你现在跑

Search (S _) 0.

第二个条目（之后H）是

O_S: forall n : nat, 0 <> S n

所以我们可以运行symmetry in H得到一个与 更好匹配的假设O_S。

H : 0 = S (length l)

既然a <> b是 just a = b -> False，我们现在可以运行apply O_S in H得到

H : False

现在我们已经有效地完成了。我们可以完成与证明exfalso; assumption，或与exfalso; exact H，或easy，或与now trivial（或now idtac），或与case H，或destruct H，或elim H，或refine match H with end，或induction H，或refine (False_rect _ H)，或tauto。所有这些基本上等同于同一件事（尽管其中一些，例如easy和tauto，也可以解决其他目标）。