使用destruct代替反转

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归纳数据类型的值时,我们用多个子目标替换当前目标,每个可能值为1 X.当我们破坏时False,我们最终会得到零子目标来证明(因为它没有值),因此证明已经完成.

基本上,destruct并inversion在这里做或多或少同样的事情.