关于Coq上的归纳类型的平凡定理

问题描述

我定义了从属类型和琐碎的引理，如下所示。

Require Import Coq.Reals.Reals.

Inductive Euc :nat -> Type:=
|RO : Euc 0
|Rn : forall {n:nat},R -> Euc n -> Euc (S n).

Lemma ROEuc : forall t:(Euc 0),t = RO.
Proof.
intros. Admitted.

我不知道如何证明。 Euc 0不是归纳类型，因此我不能使用destruct t或induction t。

请告诉我如何证明。

解决方法

您应该容易证明更简单类型的定理

Lemma ROEuc' : forall n (t : Euc n),n = 0 -> existT Euc n t = existT Euc 0 RO.

您可以简单地destruct t，给您一个琐碎的案例，再给一个congruence可以解决的荒谬案例。

要从这一引理推导出引理，您将需要四个工具：

1. 将inversion_sigma的等式转化为依赖等式的existT策略
2. 来自Coq.Logic.Eqdep_dec的事实UIP_dec证明0 = 0的所有证明在假设eq_refl相等的假设下等于nat 1 li>
3. nat的相等性是可以确定的，您可以从Coq.Arith.Arith中的某个引理中提取事实（在Search之后使用Require Import Coq.Arith.Arith查找引理的名称正确的类型）或使用decide equality策略从头开始证明
4. subst + simpl来看您的从属等式现在将简化为您要证明的定理

---

或者，您可以Require Import Coq.Program.Tactics并使用dependent destruction t，但是请注意，这通常会导致对公理的不必要依赖（在Print Assumptions可见）

,

在这种情况下，Coq实际上足够聪明，可以为您进行依赖模式匹配。 这里使用的魔术策略是refine (match t in Euc 0 with RO => _)，这使您只有一个琐碎的目标（可能会有各种各样的destruct做到这一点，但我不知道会是什么样子）。在这里，in Euc 0子句告诉Coq您只对0长度向量感兴趣，并且由于0是根据构造函数构建的nat，因此Coq可以得出RS的情况是构造函数的不相交是不可能的。

完整证明：

Lemma ROEuc : forall t:(Euc 0),t = RO.
Proof.
intros.
refine (match t in Euc 0 with RO => _ end).
reflexivity.
Qed.

此匹配生成的证明术语实际上相当复杂，但是如果您需要编写有关Coq的模式匹配功能不足以帮助您的依赖类型的其他证明，那么理解它可能会有所帮助。