どのようにプロップのパターンマッチをするタイプ

Question

に排除することなく、コックに証明するとき、私はソートされたリストの末尾ではなく戦術のパターンマッチングを使用して、コックにソートされていることを証明しようとしている：

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. 

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 

：私もCICに基づいて構築され、次のリーンコードタイプ・チェックとして、それは根本的な微積分で可能だ疑い、リーン

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. 

：これはと、しかし、失敗しました

Answer 1

これはバグのようです。問題は、私が思うに、以下の部分にされています。純粋なCICで

in Sorted _ (h::t) 

、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でこのスニペットを入力しようとすると、まったく同じエラーメッセージが表示されます。