"False" 目标：这是否表明我做错了什么？

Question

我正在尝试证明以下 (https://softwarefoundations.cis.upenn.edu/lf-current/Logic.html):

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

Theorem 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.
destruct l.
- split.
  simpl. intros.

这给出：

2 goals
T : Type
P : T -> Prop
H : forall x : T, False -> P x
______________________________________(1/2)
False
______________________________________(2/2)
All P [ ] -> forall x : T, In x [ ] -> P x

几个问题：

目标中有“False”是否表示我的证明出错了（或者我的 All 定义不正确）？
我应该用 H 做什么？我不能破坏它，不能应用它，也不能用它来重写；它还有 x 不在上下文中...

编辑： 好的看起来命题自动为真，当没有可以应用它的元素时，我没有想到：https://en.wikipedia.org/wiki/Vacuous_truth

EDIT2：哇哦，我的 All 完全错了。练习说：Drawing inspiration from [In], write a recursive function [All]，我受那个 In 的启发有点太多了。已解决。

Answer 1

在某些情况下，将 False 作为目标是正常的，例如当您想证明 ~ P 时。这是因为那只是 P -> False 的缩写，显而易见的事情是引入 P，获得，例如，p : P 作为假设，False 作为你的目标。一旦你将 False 作为你的目标，你必须寻找你的上下文中出现的矛盾。
在这种特殊情况下，您的上下文似乎没有任何矛盾，这表明可能确实出了问题。一般来说，这可能是由于错误的定义、错误的引理或错误的证明步骤造成的。由于您的证明很短并且您处于基本情况下，因此先验证明不太可能是罪魁祸首。您似乎对 All 的定义已经不是很有信心，所以我建议您重新考虑一下。提示：您正在努力证明基本步骤，因此请在基本情况的定义中查找问题。空列表的每个元素是否都有属性 P?

"False" 目标：这是否表明我做错了什么？

"False" in goal: is that a an indication I am doing something wrong?

coq