The Coq mailing list

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

That's an interesting suggestion, thanks.

On Tue, Aug 25, 2020, 12:15 Emilio Jesús Gallego Arias <e AT x80.org> wrote:

Hi Agnishom,

Agnishom Chattopadhyay <agnishom AT cmi.ac.in> writes:

> 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.

If you can afford to work with a type A which has a notion of choice
principle you can indeed write your witness function. Example:

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Variable (A : choiceType).

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

Definition extract x y (w : isPrefixOf x y) : list A := xchoose w.

Kind regards,
Emilio