Coq：证明一个归纳类型w/o一个非递归构造函数是无人居住的

Question

我是 Coq 及其基础理论的新手。假设有一个没有非递归构造函数的归纳类型。不可能生成它的实例。但它能被证明吗？

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

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

如果不是 - 它是 Coq 的缺点还是 CoC 的特性？

Answer 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.

Coq: prove that an inductive type w/o a non-recursive constructor is uninhabitated