The Coq mailing list

[Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>]

Hi Xavier,

thank you for answering.

this wouldn't work, however, because Q genuinely relies on *smaller T* in one case, where bigger P might appear; while R always relies the *same T* but smaller P (and it goes back to Q with the same T but even smaller P).

Thanks,

Jason Hu

https://hustmphrrr.github.io/

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Xavier Leroy <xavier.leroy AT college-de-france.fr>
Sent: March 22, 2019 4:41 AM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] How to organize this tricky proof?

 

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