coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to make mutual recursive theorems?

From: Chris Dams <chris.dams.nl AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] How to make mutual recursive theorems?
Date: Wed, 3 Jun 2009 07:33:37 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :content-type:content-transfer-encoding; b=iDNhwSX7fZ7q0VRnpf9nXvd8ESDPgULGxOfQKjZK2FueXwZGtjYeD78HIb5XFaDMCF EwbFCbS5lKfeEFvCXoQdXcB4ASwC+rMP8pVl5srNgGnWVhMmjq6DcSs4caVQ2f+znbaB Kbl6TQTgBvEeqbfG3F52Q1S1oJJI7FgJADwsY=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Dear all,

I did some more experimentation and found a way to make the Theorem
... with ... construction work. I now have

Inductive A: Set
:= | mk_a: A
| S: B -> A
with B: Set
:= | mk_b: B
| T: A -> B.

Section test.

Variable P: A -> Prop.
Variable Q: B -> Prop.
Variable p0: P mk_a.
Variable q0: Q mk_b.
Variable IH1: (forall b: B, Q b -> P (S b)).
Variable IH2: (forall a: A, P a -> Q (T a)).

Theorem mutual_ind_A: forall a: A, P a
with mutual_ind_B: forall b: B, Q b.
(* first branch *)
intro a.
destruct a as [|b].
exact p0.
apply IH1.
apply mutual_ind_B.
(* second branch *)
intro b.
destruct b as [|a].
exact q0.
apply IH2.
apply mutual_ind_A.
Qed.

End test.

Check mutual_ind_A.

And that works perfectly.

Thanks again,
Chris

Re: [Coq-Club] How to make mutual recursive theorems?, Chris Dams
- Re: [Coq-Club] How to make mutual recursive theorems?, Hugo Herbelin
  - Re: [Coq-Club] How to make mutual recursive theorems?, Chris Dams