逻辑：所有定义和All_In定理

Question

这是任务：

Drawing inspiration from [In], write a recursive function [All] stating that some property [P] holds of all elements of a list [l]. To make sure your definition is correct, prove the [All_In] lemma below. (Of course, your definition should not just restate the left-hand side of [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.

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

Error: The term "l' = [ ]" has type "Prop" which is not a (co-)inductive type.

那我回到第一种情况：

  | 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

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

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

Answer 1

All 应该 [] 到 True。这主要是因为 vacuous truth，但您可以看到不这样做会导致问题。

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

逻辑：所有定义和All_In定理

Logic: All definition and All_In theorem

coq

logical-foundations