模式匹配两个列表，其类型是Coq上的依赖类型

Question

我定义了这个函数。

Inductive Euc:nat -> Type:=
|RO : Euc 0
|Rn : forall {n:nat}, R -> Euc n -> Euc (S n).
Notation "[ ]" := RO.
Infix ":::" := Rn (at level 60, right associativity).
Fixpoint QE {A}(b c:Euc A) :=
match b,c with
|b':::bs, c'::: cs => (b'+c') ::: QE bs cs
|_, _ => []
end.

我遇到了错误"；术语"；[]"；具有类型"；Euc 0〃；而预期其具有类型"0"；Euc A"&"；。

如何教导CoqEuc 0就是Euc A？

Answer 1

Coq不知道剩下的唯一模式是"RO"；构造函数，因此不能返回空的Euc。要解决这个问题，只需删除_并专门化案例：

Fixpoint QE {A}(b c:Euc A) : Euc A.
refine (match b,c with
|RO, RO => _
|H => ????
end).

这迫使coq理解您正在处理一个特定的构造函数。此外，Coq总是会实例化新的消除变量(不是类型(，因此Coq可能会抱怨bs和cs有不同的索引。coq-vectordef库有几个如何管理它的例子。第一种更成熟的方法是使用消去方案，请注意，您可以使用head和last来破坏非零向量。例如：

Definition rect_euc {n : nat} (v : Euc (S n)) :
forall (P : Euc (S n) -> Type) (H : forall ys a, P (a ::: ys)), P v.
refine (match v  with
|@Rn _ _ _ => _
|R0 => _
end).
apply idProp.
intros; apply H.
Defined.

现在，您只需要使用该方案来销毁两个向量，同时保留两个向量的长度：

Fixpoint QE (n : nat) {struct n} : Euc n -> Euc n -> Euc n :=
match n as c return Euc c -> Euc c -> Euc c with
| S m => fun a => 
(@rect_euc _ a _ (fun xs x b =>
(@rect_euc _ b _ (fun ys y => (x + y) ::: @QE m xs ys))))
| 0 => fun xs ys => []
end.

或者，您可以使用coq策略来记住两个索引是相等的：

Fixpoint QE' (n : nat) (b : Euc n) : Euc n -> Euc n.
refine (match b in Euc n return Euc n -> Euc n with
|@Rn m x xs => _    
|@RO => fun H => []
end).
remember (S m).
intro H; destruct H as [| k y ys].
inversion Heqn0.
inversion Heqn0.
subst; exact ((x + y) ::: QE' _ xs ys).
Defined.