Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Factorial function

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Factorial function


chronological Thread 
  • 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





Archive powered by MhonArc 2.6.16.

Top of Page