The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

Can someone explain to a non-ssreflect/non-mathcomp user how choiceType
works?  It looks like it must rely on an axiom.  Are there any types
that fulfill it?  For example, is there a non-axiomatic way in which
bool is a choiceType?

Because, the ability to pull the necessary x out of "exists x, P x"
seems magical.  How would a program using this extract?

On Tue, 25 Aug 2020 19:15:14 +0200
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