The Coq mailing list

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

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