coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Factorial function

From: Vincent Aravantinos <vincent.aravantinos AT yahoo.fr>
To: "Jimmy Miller" <captainthunder AT gmail.com>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Factorial function
Date: Tue, 11 Sep 2007 15:14:42 +0200
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.fr; h=Received:X-YMail-OSG:In-Reply-To:References:Mime-Version:Content-Type:Message-Id:Cc:Content-Transfer-Encoding:From:Subject:Date:To:X-Mailer; b=ypsFI7dPvYoH0iSfJ+Nv6wmYL/2LG6kdeu025r2z138iw0Kw/IoKCHlluABWJUvSIo0Iv9AAcmJxkZCXwgeCfuLw4SmzF8H/7RybP4qtmf6npzKZWjIOCwe5EW92Fs5bvLROXwyNA4NOTUWQCghrBp5Cq5T5rcM2AAbhpIOuilA= ;
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Le 3 sept. 07 � 17:39, Jimmy Miller a �crit :

In Coq.Arith.Factorial, the fact function is defined as follows:

Fixpoint fact (n:nat) : nat :=
  match n with
  | O => 1
  | S n => S n * fact n
  end.

I think this is equivalent to this :

Fixpoint fact (p:nat) : nat :=
  match p with
  | O => 1
  | S n => S n * fact n
  end.

ie. the parameter n is not the same as the n bounded in the second branch of the match. Thus 'fact' is indeed seeing its parameter decreasing.

But I'm having trouble understanding how this function works. Usually
in a recursive factorial, fact is given n-1 each time it recurses, but
here I only see n getting passed to it. Wouldn't this cause infinite
recursion, because fact gets the same argument every time, and thus n
will never reach 0?

Vincent

[Coq-Club] Factorial function, Jimmy Miller
- Re: [Coq-Club] Factorial function, Vincent Aravantinos
- Re: [Coq-Club] Factorial function, Adam James Chlipala