[Coq-Club] Coq Standard Library Requests

[Larry Darryl Lee]

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

[Larry Darryl Lee]

Hi Coq Moderators,

I previously sent the following message from
***@nolijconsulting.com. Please disregard that message and post
the message I sent from ***@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

Post by Larry Darryl Lee
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
    (**
      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
    (**
      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

[Théo Zimmermann]

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

Post by Larry Darryl Lee
Hi Coq Moderators,
I previously sent the following message from
address and the one I'd like to use with the Coq Club mailing list.
I apologize for the confusion,
Thanks,
- Larry Lee

Post by Larry Darryl Lee
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
(**
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
(**
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

[Larry Darryl Lee]

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

[Beta Ziliani]

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 <

Post by Larry Darryl Lee
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
(**
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
(**
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