The Coq mailing list

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

Oh - sorry, it wasn't intended to be off-list.  Thanks for the detailed
explanation.

On Tue, 25 Aug 2020 20:58:12 +0200
Robbert Krebbers <mailinglists AT robbertkrebbers.nl> wrote:

> Not sure if this was intended to be off-list.
> 
> It's like that, but more complicated for the general case. Since bool
> is finite, termination is trivial. For types are are countable, not 
> non-finite, (take p : nat → bool) you need to find a suitable 
> termination measure.
> 
> On 8/25/20 8:54 PM, jonikelee AT gmail.com wrote:
> > On Tue, 25 Aug 2020 20:37:47 +0200
> > Robbert Krebbers <mailinglists AT robbertkrebbers.nl> wrote:
> >   
> >> The mentioned proof makes use of the following theorem:
> >>
> >>     (∃ x : A, P x) → { x : A | P x }
> >>
> >> under the assumption that 1.) A is countable, and 2.) the predicate
> >> is decidable.  
> > 
> > I see. I missed that there was a double "==" in isPrefixOf.  Ok, so
> > this is just something like:
> > 
> > Definition extract{P : bool -> bool}(e : exists b, P b = true) : {b
> > | P b = true}. Proof.
> >    assert bool as b by constructor.
> >    destruct (P b) eqn:E.
> >    - exists b. exact E.
> >    - destruct (P (negb b)) eqn:E2.
> >      + exists (negb b). exact E2.
> >      + exfalso. destruct e as (b' & F), b, b'.
> >        all:cbn in *. all:congruence.
> > Defined.
> > 
> > OK - not as magical as I thought.  Thanks.
> >   
> >>
> >> This theorem holds intuitively because you can write an algorithm
> >> that searches for the witness. Because A is countable, it can
> >> simply enumerate all elements. Then, because P is decidable, it
> >> can test for each element if P holds or not. Now, since (∃ x : A,
> >> P x) holds, this algorithm will terminate, i.e. finally find a
> >> witness.
> >>
> >> The Coq standard library also includes a version of this theorem,
> >> see
> >> https://coq.inria.fr/distrib/current/stdlib/Coq.Logic.ConstructiveEpsilon.html
> >>
> >> Also std++ includes a version of this theorem, see
> >> https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/countable.v#L84
> >>
> >> choiceType in ssreflect (or the Countable type class in std++)
> >> expresses that a type is countable, and is used to automatically
> >> infer assumption (1) in the above theorem.
> >>
> >> Hope this helps!
> >>
> >> On 8/25/20 8:27 PM, jonikelee AT gmail.com wrote:  
> >>> 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  
> >>>      
> >