The Coq mailing list

[Arthur Azevedo de Amorim <arthur.aa AT gmail.com>]

That is a good point. It actually follows because (x ++) has a left
inverse: drop (length x). We don't even need the existence proof to
extract the witness!

On Wed, Aug 26, 2020 at 5:16 PM jonikelee AT gmail.com <jonikelee AT gmail.com> 
wrote:
>
> It turns out that no assumptions about the countability of list
> element's type is necessary, nor does one have to use a decidable
> equality:
>
> Require Export Coq.Lists.List.
> Import ListNotations.
>
> Definition isPrefixOf{A} (x y : list A) :=
>   exists z, x ++ z = y. (*note: plain Leibniz = here*)
>
> Definition extract : forall {A}{y x : list A}(P : isPrefixOf x y), {z | x 
> ++ z = y}.
> Proof.
>   intro A. induction y. all:intros x P.
>   - exists []. destruct P as (z & E). rewrite app_nil_r. apply app_eq_nil 
> in E. tauto.
>   - destruct x as [|b x].
>     { exists (a::y). reflexivity. }
>     enough (a=b /\ isPrefixOf x y) as (e & Q).
>     { specialize (IHy x Q) as (z & f). exists z. cbn. congruence. }
>     destruct P as (z & E). cbn in E. injection E. intros H1 H2.
>     split.
>     + congruence.
>     + exists z. exact H1.
> Defined.
>
>
>
> On Tue, 25 Aug 2020 16:31:10 -0400
> "jonikelee AT gmail.com" <jonikelee AT gmail.com> wrote:
>
> > 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
> > > >>>
> > > >
> >
>


-- 
Arthur Azevedo de Amorim