The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 12/8/18 9:22 AM, Klaus Ostermann wrote:
> I'm making a few experiments with using subset types for "certified
> programming".
>
> I'm stuck with a certified variants of the "insert" function as used in
> insertion sort, that is,
> it's type should say that the input list and output list are sorted and
> that the output list
> contains both the input list and the element to be inserted.
>
> Could somebody tell me how to do this idiomatically in Coq, preferably
> without using
> "dependent destruction" and other tactics that require additional
> axioms?
What follows is probably not the sort of answer you are looking for, but 
I think it might nonetheless be the most useful one you receive.

It actually isn't idiomatic to program with subset types in Coq! I 
recommend avoiding explicit dependently typed programming whenever 
possible.  There should be a high standard of justification for any 
explicit dependent types (which are sometimes the right tool for a 
job).  It tends to be painful to define and reason about such programs.  
Experts generally avoid it.