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只是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，也可以解决其他目标(。

Answer 2

试试这个：我想这样改变你的引理，

Definition length_nil_list (l: nat): bool :=
match l with
| O => true
| S _ => false
end.
Compute length_nil_list (S O).
Compute length_nil_list (O).
Compute length_nil_list (S (S O)).
Definition list_nil {X : Type} (l: list X): bool:=
match l with
| nil => true
| cons h t => false
end.
Compute list_nil [].
Compute list_nil [0].
Compute list_nil nil.
Lemma mystere A:  forall l : list A, 
length_nil_list (length l) = true <-> list_nil l = true.
Proof.
intros.
destruct l.
* split.
- intros.
reflexivity.
- intros. 
simpl.
reflexivity.
* split. 
- simpl. auto.
- simpl in *. auto.
Qed.