The Coq mailing list

[Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>]

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? I'm stuck on
how to make the case distinction on whether the element to be inserted
is less than or eqal
to the first element. Presumably this requires a fancy "return" annotation?

Inductive Sorted : list nat -> Prop :=
    | Sorted_nil : Sorted []
    | Sorted_cons1 a : Sorted [a]
    | Sorted_consn a b l :
        Sorted (b :: l) -> a <= b -> Sorted (a :: b :: l).

Definition sortedOf(l: list nat)(q: list nat) := Sorted q /\ forall m,
In m l <-> In m q.

Fixpoint insert(n: nat)(l: { q: list nat | Sorted q}) : { q: list nat |
sortedOf (cons n (proj1_sig l)) q}.   
refine(  match l return { q: list nat | sortedOf (cons n (proj1_sig l))
q} with
  | exist [] st =>  _
  | exist (cons x xs) st => _
  end).
- refine (exist _ [n] _). split.  constructor. intros. split; intros. 
simpl in H ; destruct H ; subst; constructor; auto. inversion H.
  constructor. inversion H ; subst; auto. inversion H0.
-  (* stuck here; how to make the case distinction on whether n <= x ? )


Klaus