代码之家 › 专栏 › 技术社区 › Waiting for Dev...

使用析构函数而不是反转

coq-tactic theorem-proving proof coq

1

Waiting for Dev... · 技术社区 · 8 年前

我了解使用 inversion 策略:

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

然而,我不理解coq为了做同样的证明而采取的步骤,但是使用 destruct 而不是 反转 :

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

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

1 回复 | 直到 8 年前

1

5

yeputons 8 年前

False 是一个空的归纳数据类型,即它没有可能的值,请参见 here . True 是具有单个值的归纳数据类型 I

当我们 destruct 价值观 X 对于归纳数据类型,我们将当前目标替换为多个子目标,每个子目标的可能值为 X . 当我们毁灭 假 ,我们最终要证明零个子目标(因为它有零个值),因此证明就完成了。

基本上, 毁灭 和 inversion 在这里做或多或少相同的事情。