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: Tue, 2 Jun 2009 20:57:35 +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=BPSFvggPqMmpYyMm8+35Q0Zj+idCJS1lZauyGM2szooY4CYUWCvk2QAXpMWhTZt329 nn5Mig9put58LKKvRH1+3i3z+NRA5IH1rw0HM2gMa9WMM/3HcUF79h2BciDgJJvmOZy9 HcSP8dsMffDg8b9xoRcA7m0tB+oSQ6QFFX8uE=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hello Yves, Vincent and the rest of the list,

Yes, Scheme works, so thanks for that.

The Theorem ... with ... construction seems nice too and is a reason
to upgrade to 8.2, but does not work quite as well for me. If I do

Theorem mutual_ind_A:
   forall P: A -> Prop,
   forall Q: B -> Prop,
   P mk_a ->
   Q mk_b ->
   (forall b: B, Q b -> P (S b)) ->
   (forall a: A, P a -> Q (T a)) ->
   forall a: A, P a
with mutual_ind_B:
   forall P: A -> Prop,
   forall Q: B -> Prop,
   P mk_a ->
   Q mk_b ->
   (forall b: B, Q b -> P (S b)) ->
   (forall a: A, P a -> Q (T a)) ->
   forall b: B, Q b.

Coq answers with "Anomaly: uncaught exception Not_found. Please report."

All the best,
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