The Coq mailing list

[Larry Darryl Lee <llee454 AT gmail.com>]

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