在上次使用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列表的长度保持不变。怎么做?
[您要证明的是异类相等,l
和to_d (from_d l)
具有不同的类型,因此无法与同质相等类型(=)
进行比较。
如果理论上是可扩展的,那将是另一回事(相等类型是可转换的,但是您必须手动处理此差异。一种实现方法是定义一些与Leibniz原理相对应的transport
:从x = y
中得出任何P x -> P y
的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
充分结合的事实)。