The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le 10/08/2020 à 05:55, Agnishom Chattopadhyay a écrit :
> 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.

Indeed, H is a proof of proposition, so you cannot use it to produce an
actual value. It can only be used for things like proving the
termination of a recursive function.

Note that the witness function does not have to return z such that "x ++
z = y" in the general case (it is impossible anyway). It only has to do
so, if there actually exists such a z. So, we can use any dirty trick we
want to define the witness function.

For example, the function below will almost always return nonsensical
results, but we can prove that, if "isPrefixOf x y" holds, then "x ++
witness (x y) = y" holds too.

Definition witness (x y : list A) := skipn (length x) y.

Note that we do not even need to use H in the definition, since
termination is already proved by definition.

Best regards,

Guillaume