关于我在 Coq 上的归纳类型的琐碎定理

Question

如下所示，我定义了依赖类型和微不足道的引理。

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。

请告诉我如何证明。

Answer 1

你应该会发现证明更简单类型的定理很容易

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. UIP_dec 来自Coq.Logic.Eqdep_dec 的事实证明0 = 0 的所有证明都等于eq_refl，假设nat 的相等性是可判定的
3. nat 的相等性是可判定的这一事实，您可以从Coq.Arith.Arith 中的某个引理中获取这一事实（在Require Import Coq.Arith.Arith 之后使用Search 以找到具有正确类型的引理的名称）或证明使用decide equality 策略从头开始
4. subst + simpl 看到你的依赖相等现在将简化为你想要证明的定理

---

或者，您可以使用Require Import Coq.Program.Tactics 和dependent destruction t，但要注意这通常会引入对公理的不必要依赖（通过Print Assumptions 可见）

Answer 2

在这种情况下，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 的模式匹配不足以帮助您，那么理解它可能会有所帮助。