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

【问题标题】：Pattern match with two list whose type is dependent type on Coq与两个列表的模式匹配，其类型是 Coq 上的依赖类型
【发布时间】：2020-09-10 15:02:07
【问题描述】：

我定义了这个函数。

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”，而预期的类型为“Euc A”。

我如何告诉 Coq Euc 0 是 Euc A？

【问题讨论】：

标签： coq dependent-type

【解决方案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 库有几个例子来说明如何管理它。第一种方法和更成熟的方法是使用消除方案，注意您可以使用头和尾来破坏非零向量。例如：

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.

【讨论】：