The Coq mailing list

[Favonia <favonia AT umn.edu>]

You may break the mutuality by defining a proposition `PQ t` intuitively meaning `forall (smaller t' that would be used in the proof), P t' -> Q t'` and proving `bar' : forall (t : T), PQ t -> (P t -> R t)` instead. Things may be further simplified through minor adjustments depending on what `P` and `Q` actually are.

Best,

Favonia

they/them/theirs

On Thu, Mar 21, 2019 at 3: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`.

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