coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Mutually recursive functions with a decreasing measure

From: Washington Ribeiro <wtonribeiro AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Mutually recursive functions with a decreasing measure
Date: Thu, 17 Sep 2015 09:47:36 -0300
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=wtonribeiro AT gmail.com; spf=Pass smtp.mailfrom=wtonribeiro AT gmail.com; spf=None smtp.helo=postmaster AT mail-yk0-f171.google.com
Ironport-phdr: 9a23:fJ0k6hBaaO9c+bHuji9DUyQJP3N1i/DPJgcQr6AfoPdwSP7/pMbcNUDSrc9gkEXOFd2CrakU16yN6uu9ByQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTrkbvrsMCNKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46FppIZ8VvDxeL19RrhFBhwnNXo07Yvlr0rtVwyKs0QVSWUXlBVUBA6N1hDwU5brtWOuqfZ63jObN8D3V7ccVjGr7qMtQxjt3nRUfwUl+X3a35QjxJlQpwis8kRy

Dear,

It's possible to define in Coq a mutually recursive function with a decreasing measure and with a automatically generated rewriting equation?

I've used three different kind of definitions as follow:

	Muttually recursive	Decreasing measure	Rewriting equation
Fixpoint	Yes	No	Yes
Function	No	Yes	Yes
Program Fixpoint	Yes	Yes	No

So my problem is that I never have a definition with a automatically generated rewriting equation that allows to explicit a decreasing parameter and that is muttually recursive.

Best,

Washington

[Coq-Club] Mutually recursive functions with a decreasing measure, Washington Ribeiro, 09/17/2015
- <Possible follow-up(s)>
- [Coq-Club] Mutually recursive functions with a decreasing measure, Washington Ribeiro, 09/20/2015
  - Re: [Coq-Club] Mutually recursive functions with a decreasing measure, Pierre Courtieu, 09/22/2015
    - Re: [Coq-Club] Mutually recursive functions with a decreasing measure, Washington Ribeiro, 09/22/2015
      - Re: [Coq-Club] Mutually recursive functions with a decreasing measure, Pierre Courtieu, 09/23/2015
        
        Re: [Coq-Club] Mutually recursive functions with a decreasing measure, Washington Ribeiro, 09/23/2015