Coq：证明没有非递归构造函数的归纳类型是无人居住的答案

【问题标题】：Coq: prove that an inductive type w/o a non-recursive constructor is uninhabitatedCoq：证明没有非递归构造函数的归纳类型是无人居住的
【发布时间】：2019-05-11 19:37:34
【问题描述】：

我对 Coq 及其基本理论不熟悉。假设有一个没有非递归构造函数的归纳类型。不可能产生它的一个实例。但能证明吗？

Inductive impossible : Type :=
  | mk (x : impossible).

Theorem indeed_impossible : forall (x : impossible), False.

如果不是 - 这是 Coq 的一个缺点还是 CoC 的一个特性？

【问题讨论】：

标签： coq dependent-type theorem-proving

【解决方案1】：

这很容易通过对x 的归纳来证明。你只会得到一个带有荒谬归纳假设的归纳步骤，而没有需要你实际产生荒谬的基本情况。

Theorem indeed_impossible : forall (x : impossible), False.
Proof.
  induction 1.
  (* just need to show [False |- False] *)
  trivial.
Qed.

编辑：@simpadjo：对我个人来说更清楚的替代证明：

Theorem indeed_impossible : forall (x : impossible), False.
Proof.
 intros. induction x. assumption. Qed.

【讨论】：

谢谢。我试图应用倒置，但它当然无济于事。
@HTNW 感谢您提供证明脚本。我证明它有点不同（见我的编辑）。你能解释一下induction 1是什么意思吗？
嗯，我的编辑尚不可见，因为它需要同行评审。这是证明：介绍。感应 x。假设。 Qed。
@simpadjo induction 1 与 intros x. induction x 相同，但名称为 x。 trivial 是auto 的变体，除了它尝试更少地解决目标。 auto 总是首先检查假设。 Here's the documentation.
其实我现在想想，你可以说now induction 1。