The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi Jason,

Could you be more specific,

> 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`.

Most of the time, if you proceed by induction on "t", then you cannot proceed by induction on "P t" afterwards because "t" is not

a freely evolving variable anymore in "P t". Maybe you use inversion ?

Best,

Dominique

---

De: "Jason -Zhong Sheng- Hu" <fdhzs2010 AT hotmail.com>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Jeudi 21 Mars 2019 21:50:55
Objet: [Coq-Club] How to organize this tricky proof?

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`.

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