这似乎是一个错误。我认为,问题在于以下部分:
in Sorted _ (h::t)
在纯CIC中,这种注释就有了 match 表达式是不允许的。相反,你需要写这样的东西:
match
Definition tail_also_sorted {A : Prop} {R : relation A} {h : A} {t : list A} (H: Sorted R (h::t)) : Sorted R t := match H in Sorted _ t' return match t' return Prop with | [] => True | h :: t => Sorted R t end with | Sorted_nil _ => I | Sorted_cons rest_sorted _ => rest_sorted end.
区别在于指数中的 in 子句现在是一个绑定在的新变量 return 条款。为了减轻您编写这些可怕程序的麻烦,Coq允许您将更复杂的表达式放入其中 in 子句比泛型变量,就像你拥有的那样。为避免损害稳健性,此扩展实际上已编译为核心CIC术语。我想在某个地方有一个错误就是这个翻译产生了以下术语:
in
return
Definition tail_also_sorted {A : Prop} {R : relation A} {h : A} {t : list A} (H: Sorted R (h::t)) : Sorted R t := match H in Sorted _ t' return match t' return Type with | [] => True | h :: t => Sorted R t end with | Sorted_nil _ => I | Sorted_cons rest_sorted _ => rest_sorted end.
请注意 return Type 注解。实际上,如果您尝试在Coq中输入此片段,则会得到与您看到的完全相同的错误消息。
return Type