The Coq mailing list

[Xavier Leroy <xavier.leroy AT college-de-france.fr>]

On Thu, Mar 21, 2019 at 9:51 PM Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com> wrote:

Hi,

consider a type `T` and an inductively defined proposition `P : T -> Prop`. theorem `foo : forall (t : T), P t -> Q t` is proved by doing an induction on `t` and then `P t`.

however, inside of `foo`, in each case of `t`, I will need another theorem `bar : forall (t : T), P t -> R t`, which is proved by induction on `P t` and some cases require `foo`.

What about proving

Lemma foobar: forall (t: T), P t -> Q t /\ R t.

with a single induction on "P t" ?  Then, "foo" and "bar" are trivial corollaries.

- Xavier Leroy

since `bar` always operate on smaller `P t` instances, so these two theorems are true, but just mutually dependent.

my problem is, I am not sure how to organize this proof to make it shorter. clearly, I can prove `bar` for each particular `t` but it pointlessly adds so much more identical proofs. On the other hand, `foo` and `bar` are not structurally mutually recursive either, because `foo` decreases on `T` while `bar` decreases on `P t`, which stops me from using Fixpoint.

Is there any way to organize the proof, so that I only need to prove `foo` and `bar` once?

Sincerely Yours,

Jason Hu