Comment faire correspondre un motif sur Prop lorsque la preuve en Coq sans élimination sur le type

Question

Je suis en train de prouver que la queue d'une liste triée est triée en Coq, en utilisant la correspondance de modèles au lieu de la tactique:

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. 

Cela échoue cependant avec:

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. 

Je pense qu'il est possible dans le calcul sous-jacent, comme les contrôles de type-code Lean suivants, et Lean est également construit sur le 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 

Answer 1

Cela semble être un bug. Le problème, je pense, est dans la partie suivante:

in Sorted _ (h::t) 

En pur CIC, ce genre d'annotation sur match expressions n'est pas autorisé. , Vous devez écrire à la place quelque chose comme ceci:

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. 

La différence est que l'indice dans la clause in est maintenant une nouvelle variable qui est lié à la clause return. Pour vous éviter d'avoir à écrire de tels programmes horribles, Coq vous permet de mettre des expressions légèrement plus compliquées dans les clauses in que les variables génériques, comme celle que vous aviez. Pour éviter de compromettre la solidité, cette extension est en fait compilée jusqu'aux termes de base de CIC. J'imagine qu'il ya un bug quelque part cette traduction qui est produit à la place le terme suivant:

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. 

Notez l'annotation return Type. En effet, si vous essayez d'entrer cet extrait dans Coq, vous obtenez exactement le même message d'erreur que celui que vous avez vu.