逻辑：所有定义和 All_In 定理答案

【问题标题】：Logic: All definition and All_In theorem逻辑：所有定义和 All_In 定理
【发布时间】：2019-04-26 19:30:39
【问题描述】：

这是任务：

从[In]中汲取灵感，写一个递归函数[All] 声明某个属性 [P] 包含列表 [l] 的所有元素。到确保您的定义是正确的，证明下面的 [All_In] 引理。（当然，您的定义应该不只是重述左手 [All_In] 的一侧。）

In 是这样定义的：

Fixpoint In {A : Type} (x : A) (l : list A) : Prop :=
  match l with
  | [] => False
  | x' :: l' => x' = x \/ In x l'
  end.

起初我以类似的方式定义All：

Fixpoint All {T : Type} (P : T -> Prop) (l : list T) : Prop :=
  match l with
  | [] => False
  | x' :: l' => P x' /\ All P l'
  end.

但后来我认为这是不正确的，因为连词末尾的 False 总是会给出 False。

如果列表的最后一个 nil 元素不为空，我们需要忽略它（这行不通，只是一个想法）：

Fixpoint All {T : Type} (P : T -> Prop) (l : list T) : Prop :=
  match l with
  | [] => False
  | x' :: l' => P x' /\ if l' = [] then True else All P l'
  end.

错误，我不知道如何解决：

错误：术语“l' = [ ]”的类型为“Prop”，它不是（共）感应型。

然后我回到第一种情况：

  | x' :: l' => P x' /\ All P l'

并尝试证明 All_In 定理：

Lemma All_In :
  forall T (P : T -> Prop) (l : list T),
    (forall x, In x l -> P x) <->
    All P l.
Proof.
  intros T P l. split.
  - (* Left to right *)
    intros H. induction l as [| h t IHl].
    + simpl. simpl in H.

现在我们被困住了：

T : Type
P : T -> Prop
H : forall x : T, False -> P x
============================
False

因为我们在结论中有 False，但前提中没有 False 假设，整个陈述都是谎言。

如何正确定义All？
我的证明有什么问题？

【问题讨论】：

标签： coq logical-foundations

【解决方案1】：

All 应将[] 转换为True。这基本上是因为vacuous truth，但您可以看到不这样做会导致问题。

没有All P [] 为真也使你的引理为假。对于所有x，In x [] 都是假的。但是 false 意味着任何东西，包括P x，所以我们有forall x, In x [] -> P x。但是如果All P []为假，那么这两个语句就不能等价了。

【讨论】：