The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

I think the point of Emilio's message was that with countability you can 
get the proof for free, and no proof effort is needed. I don't think his 
point was that the countability stuff is truly needed.

Emilio can probably correct me if I'm getting this wrong.

On 26/08/2020 23.30, Arthur Azevedo de Amorim wrote:
> 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