时间戳

首页 > 解决方案 > 使用破坏而不是反转

coq - 使用破坏而不是反转

问题描述

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归纳法是如何被破坏的？它对目标和完成证明有何影响？

标签： coqprooftheorem-provingcoq-tactic

解决方案

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

当我们使用归纳数据类型destruct的值X时，我们将当前目标替换为多个子目标，每个可能的值一个X。当我们 destruct 时False，我们最终得到零个要证明的子目标（因为它的值为零），因此证明完成。

基本上，在这里或多或少地做同样的事情destruct。inversion

推荐阅读