coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Mutual induction over a single inductive type

From: Adam Chlipala <adamc AT hcoop.net>
To: Nikhil Swamy <nswamy AT microsoft.com>
Cc: "coq-club AT pauillac.inria.fr" <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] Mutual induction over a single inductive type
Date: Sun, 22 Feb 2009 18:42:19 -0500
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Nikhil Swamy wrote:

I have a single inductively defined proposition T and
I need to prove a lemma P over T using mutual induction with
another lemma Q over T. What's the easiest way of doing this?

This isn't really mutual induction. You can prove a lemma that, for each value of the inductive type, asserts the conjunction of the two facts that interest you.

[Coq-Club] Mutual induction over a single inductive type, Nikhil Swamy
- Re: [Coq-Club] Mutual induction over a single inductive type, Adam Chlipala
- Re: [Coq-Club] Mutual induction over a single inductive type, Matthieu Sozeau
  - RE: [Coq-Club] Mutual induction over a single inductive type, Nikhil Swamy
    - Re: [Coq-Club] Mutual induction over a single inductive type, Hugo Herbelin