时间戳

首页 > 解决方案 > Coq：依赖列表上的类型不匹配，可以通过证明来解决

list - Coq：依赖列表上的类型不匹配，可以通过证明来解决

问题描述

在我最后一次在 coq 中使用列表时，我遇到了一个类型问题。但首先，定义；

休闲清单：

Inductive list (a : Set) : Set :=
| nil : list a
| cons : a -> list a -> list a
.

Fixpoint len {a : Set} (l : list a) : nat :=
  match l with
  | nil _ => 0
  | cons _ _ t => 1 + (len t)
  end.

依赖列表：

Inductive dlist (a : Set) : nat -> Set :=
| dnil : dlist a 0
| dcons : a -> forall n, dlist a n -> dlist a (S n)
.

转换：

Fixpoint from_d {a : Set} {n : nat} (l : dlist a n) : list a :=
  match l with
  | dnil _ => nil _
  | dcons _ h _ t => cons _ h (from_d t)
  end.

Fixpoint to_d {a : Set} (l : list a) : dlist a (len l) :=
  match l with
  | nil _ => dnil _
  | cons _ h t => dcons _ h _ (to_d t)
  end.

我想证明转换环岛，严格来说

Theorem d_round : forall (a : Set) (n : nat) (l : dlist a n),
    to_d (from_d l) = l.

但我收到以下错误：

The term "l" has type "dlist a n" while it is expected to have type
 "dlist a (len (from_d l))".

这很容易理解，但我完全不知道如何解决它。我可以很容易地证明

forall (a : Set) (n : nat) (l : dlist a n), n = len (from_d l).

但我认为没有办法使用这个定理让 Coq 相信列表的长度保持不变。怎么做？

标签： listcoqdependent-typetheorem-proving

解决方案

您要证明的是异质相等，l并且to_d (from_d l)具有不同的类型，因此无法与同质相等类型进行比较(=)。

如果理论是可扩展的，那将是另一回事（相同的类型可以转换），但是您必须手动处理这种差异。一种方法是定义一些transport与莱布尼茨原则相对应的方法： from x = yyou derived P x -> P yfor any P。

Definition transport {A} {x y : A} (e : x = y) {P : A -> Type} (t : P x) : P y :=
  match e with
  | eq_refl => t
  end.

在您的情况下，n = m -> dlist A n -> dlist A m您甚至可以使用专门的版本。

那么这个定理可以表述为：

Axiom e : forall (a : Set) (n : nat) (l : dlist a n), n = len (from_d l).

Theorem d_round : 
  forall (A : Set) (n : nat) (l : dlist A n),
    to_d (from_d l) = transport (e _ _ _) l.

现在你必须处理阻碍你的等式，但自然数上的等式是可判定的，因此是一个命题（任何两个 的证明n = m总是相等的，特别是任何 的证明n = n等于eq_refl；一个与 很好结合的事实transport eq_refl t = t） .

推荐阅读