Как сопоставить с образцом на опоре при испытании в Coq без исключения на Type

Я пытаюсь доказать, что хвост отсортированного списка сортируется в 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

dependent-type theorem-proving coq type-theory lean
person LogicChains    schedule 11.07.2017    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Это похоже на ошибку. Проблема, я думаю, в следующем:

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, вы получите точно такое же сообщение об ошибке, что и то, которое вы видели.

person Arthur Azevedo De Amorim    schedule 11.07.2017
comment
Где лучше всего сообщить о проблеме? - person LogicChains; 12.07.2017