用破坏代替反演

Question

我理解使用inversion战术的防爆原理：

Theorem ex_falso_quodlibet : forall (P:Prop),
  False -> P.
Proof.
  intros P contra.
  inversion contra.  Qed.

但是，我不明白Coq为了做同样的证明而使用destruct而不是inversion所采取的步骤

Theorem ex_falso_quodlibet' : forall (P:Prop),
  False -> P.
Proof.
  intros P contra.
  destruct contra.  Qed.

False如何被破坏？它对目标和完成证明有什么影响？

Answer 1

False是一种空的归纳数据类型，即它没有可能的值，参见这里。True是具有单个值I的归纳数据类型。

当我们destruct一个归纳数据类型的值X时，我们用多个子目标替换当前的目标，每个可能的X值每个子目标一个。当我们破坏False时，我们最终得到零子目标来证明(因为它的值为零)，因此证明就完成了。

基本上，destruct和inversion在这里做的事情差不多是一样的。