Skip to Content.
Sympa Menu

coq-club - [Coq-Club] The greatest common divisor in the standard library

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] The greatest common divisor in the standard library


chronological Thread 
  • From: "Andrés Sicard-Ramírez" <andres.sicard AT gmail.com>
  • To: Coq-Club <coq-club AT pauillac.inria.fr>
  • Cc: "Ana Bove" <bove AT chalmers.se>, "Peter Dybjer" <peterd AT cs.chalmers.se>
  • Subject: [Coq-Club] The greatest common divisor in the standard library
  • Date: Thu, 10 Jul 2008 14:42:30 +0200
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:cc:mime-version:content-type :content-transfer-encoding:content-disposition; b=TS8+wLBen2cA8wffVo1SZCiAsOU3sTEoalO2iYSUcUKj/QsXaORpSNboGbbvWwZjU5 7sM9NBLVSmYU8OGRscTzUm5ggYGuGPjyffw7+Rq1jPOyKbkn6FqxUD2483/qxCIUGcm7 Isy7morrOEGmMF1f4c0xGHGHI6O2zkf/ZY1fo=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hello,

It seems that the specification 'Zis_gcd' is not the correct one for
the greatest common divisor. The function 'Zgcd' satisfies this
specification (Lemma Zgcd_is_gcd : forall a b, Zis_gcd a b (Zgcd a
b)), however, Zgcd 0 0 = 0 and 0 is not the greatest common divisor of
0 and 0 (I guess it should be undefined because any number divides 0).
Is the specification 'Zis_gcd' incorrect or am I missing something?

Thanks,

-- 
Andrés



Archive powered by MhonArc 2.6.16.

Top of Page