我试图证明排序列表的尾部在 Coq 中排序,使用模式匹配而不是策略:
Require Import Coq.Sorting.Sorted.
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 _ (h::t) return Sorted _ t with
| Sorted_nil _ => Sorted_nil R
| Sorted_cons rest_sorted _ => rest_sorted
end.
但是,此操作失败,并显示:
Error:
Incorrect elimination of "H" in the inductive type "Sorted":
the return type has sort "Type" while it should be "Prop".
Elimination of an inductive object of sort Prop
is not allowed on a predicate in sort Type
because proofs can be eliminated only to build proofs.
我怀疑在底层演算中这是可能的,因为以下精益代码类型检查,精益也是建立在 CIC 之上的:
inductive is_sorted {α: Type} [decidable_linear_order α] : list α -> Prop
| is_sorted_zero : is_sorted []
| is_sorted_one : ∀ (x: α), is_sorted [x]
| is_sorted_many : ∀ {x y: α} {ys: list α}, x < y -> is_sorted (y::ys) -> is_sorted (x::y::ys)
lemma tail_also_sorted {α: Type} [decidable_linear_order α] : ∀ {h: α} {t: list α},
is_sorted (h::t) -> is_sorted t
| _ [] _ := is_sorted.is_sorted_zero
| _ (y::ys) (is_sorted.is_sorted_many _ rest_sorted) := rest_sorted
这似乎是一个错误。我认为,问题出在以下部分:
in Sorted _ (h::t)
在纯 CIC 中,不允许对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 术语。我想某处有一个错误,就是这个翻译,它正在产生以下术语:
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 中输入此代码段,您会收到与您看到的完全相同的错误消息。