PROSAGA码农传奇-精益-如何在Coq中进行证明而不在类型上消除时对Prop进行模式匹配

<div class =“post-text”itemprop =“text”>
  <P>
    这似乎是一个错误。我认为，问题在于以下部分：
  </p>
   <pre>
    <code>
      in Sorted _ (h::t)

</code>
  </pre>
  <P>
    在纯CIC中，这种注释就有了
     <code>
      match
    </code>
     表达式是不允许的。相反，你需要写这样的东西：
  </p>
   <pre>
    <code>
      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.

</code>
  </pre>
  <P>
    区别在于指数中的
     <code>
      in
    </code>
     子句现在是一个绑定在的新变量
     <code>
      return
    </code>
     条款。为了减轻您编写这些可怕程序的麻烦，Coq允许您将更复杂的表达式放入其中
     <code>
      in
    </code>
     子句比泛型变量，就像你拥有的那样。为避免损害稳健性，此扩展实际上已编译为核心CIC术语。我想在某个地方有一个错误就是这个翻译产生了以下术语：
  </p>
   <pre>
    <code>
      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.

</code>
  </pre>
  <P>
    请注意
     <code>
      return Type
    </code>
     注解。实际上，如果您尝试在Coq中输入此片段，则会得到与您看到的完全相同的错误消息。
  </p>
</DIV>