How to pattern match on a Prop when proving in Coq without elimination on Type

Question

I'm trying to prove that the tail of a sorted list is sorted in Coq, using pattern matching instead of tactics:

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.

This fails however, with:

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.

I suspect it's possible in the underlying Calculus, as the following Lean code type-checks, and Lean is also built upon the 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

This seems like a bug. The problem, I think, is in the following part:

in Sorted _ (h::t)

In pure CIC, this kind of annotation on match expressions is not allowed. Instead, you are required to write something like this:

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.

The difference is that the index in the in clause is now a fresh variable that is bound in the return clause. To relieve you from having to write such horrible programs, Coq allows you to put slightly more complicated expressions in in clauses than generic variables, like the one you had. To avoid compromising soundness, this extension is actually compiled down to core CIC terms. I imagine that there is a bug somewhere is this translation that is producing the following term instead:

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.

Notice the return Type annotation. Indeed, if you try to enter this snippet in Coq, you get exactly the same error message as the one you saw.