coq 中空列表和非空列表的析取

Question

我是 Coq 的新手。如何证明空表和非空表的析取是真的？

l = [] \/ l <> []

这是我正在研究的引理：

Lemma in_list: forall (X : Type) (a : X) l (P : X -> Prop),
        (a :: l <> [] /\ exists b : X, In b (a :: l) -> P b) ->

  (P a /\ l = [] \/
P a /\ l <> [] \/ ~ P a /\ l <> [] /\ (exists b : X, In b l -> P b))

所以证明引理的一种方法似乎是考虑两种情况：

if l = [] or l <> []

然后

if l = [], P a holds

和

if l <> [], ~ P a /\ l <> [] /\ (exists b : X, In b l -> P b) holds

我可以通过这种方式证明引理，但我不知道如何进行这种方式。我已经为 Prop 类型（不是列表）做了类似的事情，比如对于 Prop 类型的变量 R，它考虑了 True 或 False 的两种情况。我不确定我是否可以为列表做类似的事情。

destruct (classic R) as [r | rn].

谢谢，

Answer 1

这是一个非常基础的问题，看起来像是家庭作业的第 1 题，所以我建议您：

在纸上思考一下：你如何用笔和纸证明这一点？
您知道哪些策略，哪些可以应用在这里？
正如@anton 所说，至少向我们解释一下你尝试了什么，什么失败了

Answer 2

您已经知道：

destruct (classic R) as [r | rn].

它可以与任何 R : Prop 一起使用，并且它在内部依赖于排中公理。

存在一个更简单的版本，其中不需要公理，因为您已经知道对象只能有几种形式：

destruct l.

其中 l 是您的列表，但它也可以是自然数或析取证明...

coq 中空列表和非空列表的析取

disjunction of empty and non-empty list in coq

coq