The Coq mailing list

[Clément Pit-Claudel <cpitclaudel AT gmail.com>]

In other words:

Definition extract' : forall {A} {y x : list A} (P : isPrefixOf x y), {z | x 
++ z = y}.
  intros A y x P.
  exists (List.skipn (List.length x) y).
  destruct P as (z & H).
  revert y z H. induction x; cbn; intros y z H.
  - reflexivity.
  - erewrite <- H, IHx; reflexivity.
Qed.


On 8/26/20 5:30 PM, 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
>>>>>>>
>>>>>
>>>
>>
> 
>