The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

I'm not a coq-dev, but I guess the most reasonably thing to do is to add a PR in github.

On Thu, Aug 23, 2018 at 11:48 AM, Larry Darryl Lee <Larry.Lee AT nolijconsulting.com> 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