The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

You may be able to do that, but that sounds rather adhoc/specialized.

Again, I think the point is that *if* you are in the fortunate situation 
that you are dealing with lists of countable types, you can get this for 
free from very generic infrastructure from extracting witnesses from 
existentials in libraries like ssreflect or std++. The point is not that 
such libraries give the most general theorem for free.

If you are not in that fortunate situation, or you want to obtain the 
most general theorem, then well, you have to construct the witness in 
some other way, for example using your proof.

On 27/08/2020 00.22, jonikelee AT gmail.com wrote:
> On Thu, 27 Aug 2020 00:03:18 +0200
> Robbert Krebbers <mailinglists AT robbertkrebbers.nl> wrote:
>
> > 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.
>
> If so, can't one set up some typeclasses (or canonical structures) so
> that left inverses, when registered, get found and used automatically?
> That still would not add requirements to A or require decidable
> equality.
>
> > 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
> > > > > > > > >   
> > > > > > >   
> > > > >   
> > > >   
> > >
> > >