The Coq mailing list

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

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