The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Hi Larry,

It seems that the list moderators didn't see this message, because both of your previous messages passed through.

Anyways, as Beta said in reply to the other thread, you should open a pull request at https://github.com/coq/coq if you want to propose a change to the standard library. There are no clear rules of what is acceptable content for the standard library at the moment, but this small addition would have good chances of getting in.

Best,

Théo

Le jeu. 23 août 2018 à 16:52, Larry Darryl Lee <llee454 AT gmail.com> a écrit :

Hi Coq Moderators,

I previously sent the following message from
larry.lee AT nolijconsulting.com. Please disregard that message and post
the message I sent from llee454 AT gmail.com, as this is my personal email
address and the one I'd like to use with the Coq Club mailing list.

I apologize for the confusion,
Thanks,

- Larry Lee

On Thu, 2018-08-23 at 10:50 -0400, Larry Darryl Lee wrote:
> Hi,
>
> I recently worked on a small project and noticed that the List
> library
> within the Coq Standard library is missing two obvious proofs.
>
> First, the List library defines a proof `Forall_impl` that has an
> obvious analog for the `Exists` predicate.
>
> Second, the List library defines a proof `Forall_inv` that applies to
> the head of a list, but lacks the obvious analogue for the tail of a
> list.
>
> I'd like to propose adding two proofs to the Standard List library.
> The
> first, is a proof `Exists_impl` which fills the gap left by
> `Forall_impl`:
>
>     (**
>       Accepts two predicates, [P] and [Q], and a
>       list, [xs], and proves that, if [P -> Q],
>       and there exists an element in [xs] for which
>       [P] is true, then there exists an element in
>       [xs] for which [Q] is true.
>     *)
>     Definition Exists_impl
>       :  forall (A : Type) (P Q : A -> Prop),
>          (forall x : A, P x -> Q x) ->
>          forall xs : list A,
>            Exists P xs ->
>            Exists Q xs
>       := fun _ P Q H xs H0
>            => let H1
>                 :  exists x, In x xs /\ P x
>                 := proj1 (Exists_exists P xs) H0 in
>               let H2
>                 :  exists x, In x xs /\ Q x
>                 := ex_ind
>                      (fun x H2
>                        => ex_intro
>                             (fun x => In x xs /\ Q x)
>                             x
>                             (conj
>                               (proj1 H2)
>                               (H x (proj2 H2))))
>                      H1 in
>               (proj2 (Exists_exists Q xs)) H2.
>
>     Arguments Exists_impl {A} {P} {Q} H xs H0.
>
> The second is a proof `Forall_inv_tail` that fills the gap left by
> `Forall_inv`. It's proof is similarly easy:
>
>     (**
>       Accepts a predicate, [P], and a list, [x0 ::
>       xs], and proves that if [P] is true for every
>       element in [x0 :: xs], then [P] is true for
>       every element in [xs].
>     *)
>     Definition Forall_inv_tail
>       :  forall (A : Type) (P : A -> Prop) (x0 : A) (xs : list A),
>     Forall P (x0 :: xs) -> Forall P xs
>       := fun _ P x0 xs H
>            => let H0
>                 :  forall x, In x (x0 :: xs) -> P x
>                 := proj1 (Forall_forall P (x0 :: xs)) H in
>               let H1
>                 :  forall x, In x xs -> P x
>                 := fun x H2
>                      => H0 x (or_intror (x0 = x) H2) in
>               proj2 (Forall_forall P xs) H1.
>
>     Arguments Forall_tail {A} {P} x0 xs.
>
> At the moment, I've defined these proofs in a small personal library
> that I include in most of my projects, but I'd like to see these
> obvious extensions included in the Standard Library one day.
>
> Who should a I propose these additions to? What are the rules for
> adding theorems to the Coq Standard Library?
>
> - Larry Lee