我有一个带有对象和箭头的图表，并由此定义了箭头路径的概念。我想定义这些路径的串联。下面的代码是我天真的尝试。但是，当 match 子句中的 p' 为 emptyPath 时，我收到错误:“术语“p”的类型为“path A B”，而它预计有类型 “路径 A C”。从概念上讲应该没有问题，因为在这种情况下 B 等于 C。我怎样才能让它发挥作用？
Parameter Object : Set.
Parameter Arrow : Object -> Object -> Set.
Inductive path : Object -> Object -> Set :=
emptyPath : forall X, path X X
| cons : forall {A B C} (p : path A B) (f : Arrow B C), path A C.
Fixpoint concat {A B C : Object} (p : path A B) (p' : path B C) : path A C :=
match p' return path A C with
| emptyPath _ => p
| cons _ _ _ p0 f => cons (concat p p0) f
end.
请您参考如下方法:
只要您的定义中存在“变化的索引”，您就需要应用所谓的“护航模式”来使您的定义发挥作用。基本思想是重新抽象一些参数，以便依赖模式匹配可以“更改”它们的类型。
Parameter Object : Set.
Parameter Arrow : Object -> Object -> Set.
Inductive path : Object -> Object -> Set :=
emptyPath : forall X, path X X
| cons : forall {A B C} (p : path A B) (f : Arrow B C), path A C.
Fixpoint concat {A B C : Object} (p : path A B) (p' : path B C) : path A C :=
match p' in path B C return path A B -> path A C with
| emptyPath _ => fun p => p
| cons _ _ _ p0 f => fun p => cons (concat p p0) f
end p.
您可以在 Adam Chlipala 的 CPDT 中了解有关车队模式的更多信息。书。