The Coq mailing list

[Agnishom Chattopadhyay <agnishom AT cmi.ac.in>]

I have a function that is something like this:

 Definition isPrefixOf (x : list A) (y : list A) :=
     exists z, x ++ z = y.

Now, I want to define a witness function. Informally, it can be described as follows: Given x and y such that (isPrefixOf x y), return z which satisfies the criteria exists z, x ++ z = y.

I would try to define it this way, but that would not work (possibly because exists z, x ++ z = y is a Prop and we are asking for something in Type) :

Definition witness (x y : list A) {H : isPrefixOf x y} : list A.
    destruct H.

Abort.

Another option seems to be to define

Definition isPrefixOf (x y : list A) :=
    sig (fun z => x ++ z = y).

But I do not like this because this does not let me define things like Instance isPrefixOf_PreOrder : PreOrder isPrefixOf.

So, how can I have my cake and eat it too?