coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Mutually recursive lemmas and decreasing arguments

From: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>
To: Adam Chlipala <adam AT chlipala.net>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Mutually recursive lemmas and decreasing arguments
Date: Fri, 11 Mar 2011 02:29:08 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type :content-transfer-encoding; b=f726vfRDaUeD/U9blk8YO+LIh6CSQOoeHGwJncj2HSQ5s5NmFABVAZ1yRu5tpp851D gi30evCUzGqyYaCRxM3CjXpbLl2K72yUxYGXLsWlMqxHkCS6c3QfP1W2SchiOarJKjvb mPlscqgWjT6NC0EEMqCoWTSCurywYDTrUVXG0=

2011/3/11 Adam Chlipala
<adam AT chlipala.net>:
> Are you using an induction principle generated by [Scheme]? �There shouldn't
> be any need for explicit [fix]es if so.

You're right ! Using combined Scheme after producing the induction
principles with Scheme allows me to prove my lemma (as a triple
conjonction).

I'll look how to prove the three lemmas directly tomorrow.

Thanks Adam

- Alexandre

[Coq-Club] Mutually recursive lemmas and decreasing arguments, Alexandre Pilkiewicz
- Re: [Coq-Club] Mutually recursive lemmas and decreasing arguments, Adam Chlipala
  - Re: [Coq-Club] Mutually recursive lemmas and decreasing arguments, Alexandre Pilkiewicz
- Re: [Coq-Club] Mutually recursive lemmas and decreasing arguments, Matthieu Sozeau