如何解决模式匹配两个列表,其类型取决于Coq
我定义了此功能。
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不知道剩下的唯一模式是“ 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.
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。