0

这是任务：

从 [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 假设，整个陈述都是谎言。

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

1 回答 1

2

All应该[]采取True。这本质上是因为空洞的事实，但是您可以看到不这样做是如何引起问题的。

不All P []为真也会使你的引理为假。总而言之x，In x []是假的。但是 false 意味着任何东西，包括P x，所以我们有forall x, In x [] -> P x。但如果All P []是假的，那么这两个陈述就不能等价。

于 2019-04-26T21:02:11.557 回答