coq - 归纳定义的稠密向量引理

Question

受 StackOverflow 上另一个问题的启发，我定义了一个 dense vector 为具有 option A 类型元素的向量，仅包含 Some _元素，并且没有 None 元素。

Require Import Vector.
Section Dense.
  Variable A:Type.

  Inductive Is_dense : forall n, t (option A) n -> Prop :=
  | snil : Is_dense 0 (nil _)
  | scons: forall n s, Is_dense n s -> forall a, Is_dense (S n) (cons _ (Some a) _ s).

如何证明以下两个引理？

  Lemma Is_dense_tl: forall n (s: t (option A) (S n)),
                     Is_dense (S n) s -> Is_dense n (tl s).

和

  Lemma dense_hd: forall n (s: t (option A) (S n)), Is_dense (S n) s -> A.

而且，在第一个引理中，当我执行 inversion s. 时，我得到了被 s 使用的元素 h n' X的构造函数，但我怎样才能得到一个等式声明 s = cons (option A) h n' X?

Answer 1

因为类型依赖，inversion 不能直接生成你期望的，因为一般情况下不是这样。但是，对于一大类其相等性可判定的类型来说，这是正确的。在你的情况下，你可以应用 Eqdep_dec.inj_pair2_eq_dec 来获得你想要的平等，如果你提供这样一个事实:nat 上的平等是可判定的(而且它是)。

这是第一个引理的证明:

Lemma Is_dense_tl: forall n (s: t (option A) (S n)),
                     Is_dense (S n) s -> Is_dense n (tl s).
Proof.
intros n s hs.
inversion hs; subst; clear hs.
apply Eqdep_dec.inj_pair2_eq_dec in H0.
- now rewrite <- H0; simpl.
- (* insert proof of decidablity *) admit.
Qed.

编辑:关于您对第二个引理的评论。

你的两个引理之间的主要区别在于第一个引理试图证明存在于 Prop 中的属性 Is_dense n (tl s)，而第二个引理尝试证明显示类型为 A 的术语。简而言之，前者创建了一个Prop类的术语，后者创建了一个Type类的术语。

为了避免 Coq 逻辑中的不一致，有一个层次结构来组织排序，它是(不完全是，但给你一个粗略的想法)Prop: Set Set:Type_0 和 Type_n: Type_n+1。在这个层次结构之上构建了一个类型系统，其中依赖对(例如类型 {n: nat | even n } 是偶数自然数的类型)受到限制。您可以从其他 Prop 构建一个 Prop(例如 forall p:Prop, p -> p lives in Prop ).但是，当涉及到 Type 时，您需要小心。例如，(同样，请参阅 Coq 的文档以了解确切的语句)forall n:Type_i, Type_j 的类型为 Type_max(i,j)。

此限制是为了避免 Coq 类型系统中的不一致(如罗素悖论)。

在您的情况下，您正在尝试检查(使用 inversion)排序项 Prop (Is_dense (S n) s)构建 A 类型的术语，属于 Type 类型。这是类型系统所禁止的。要构建 Type 类别的术语，您需要至少检查 Set 类别的术语。在您的示例中，您所要做的就是将 Is_dense 的定义更改为 Type 而不是 Prop，您就可以去吧。