coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Fixpoint decreasing parameter:help

From: Groleo Marius <groleo AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Fixpoint decreasing parameter:help
Date: Wed, 13 Jan 2010 19:06:26 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=WR2udMKE/ssUJC0pZm9r2LOq4z7OQY3LpUJOTJ26UFaJX/xCw4xt4ImyjWC6xcrKND kS2i+8gPOxgXdot14MOs5vNpwcAt8xRZi8GNeeZ8Fq0gX+A2JquwJnpueHSxwHOrt22L 5Z78Ju2e3JmNDY5srijoia/c50gdKIDS53d5k=

Hi list

I'm trying to write a recursive function, that would only loop until a
given parameter, n, get equal to 1.
Require Import Arith.Min.
Require Import ZArith.BinInt.
Require Import ZArith.
Require Import ZArith_dec.
Require Import Zwf.

Open Scope Z_scope.

Fixpoint loop ( woff roff :Z )(n:Z) :=
  match n with
  | 0 => 0
  | n' => loop 1 1 (Zminus n' 1)
  end.

Error: Cannot guess decreasing argument of fix.

Can you point me please to some documents regarding this construct ?

--
Regards, Groleo!

[Coq-Club] Fixpoint decreasing parameter:help, Groleo Marius
- Re: [Coq-Club] Fixpoint decreasing parameter:help, Adam Chlipala
  - Re: [Coq-Club] Fixpoint decreasing parameter:help, Groleo Marius
- Re: [Coq-Club] Fixpoint decreasing parameter:help, Adam Koprowski
  - Re: [Coq-Club] Fixpoint decreasing parameter:help, Groleo Marius