From fb2e6501516184a03fbc475921c20499f87d3aac Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 5 Nov 2010 18:27:39 +0000
Subject: Numbers: axiomatization, properties and implementations of gcd
- For nat, we create a brand-new gcd function, structural in
the sense of Coq, even if it's Euclid algorithm. Cool...
- We re-organize the Zgcd that was in Znumtheory, create out of it
files Pgcd, Ngcd_def, Zgcd_def. Proofs of correctness are revised
in order to be much simpler (no omega, no advanced lemmas of
Znumtheory, etc).
- Abstract Properties NZGcd / ZGcd / NGcd could still be completed,
for the moment they contain up to Gauss thm. We could add stuff
about (relative) primality, relationship between gcd and div,mod,
or stuff about parity, etc etc.
- Znumtheory remains as it was, apart for Zgcd and correctness proofs
gone elsewhere. We could later take advantage of ZGcd in it.
Someday, we'll have to switch from the current Zdivide inductive,
to Zdivide' via exists. To be continued...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13623 85f007b7-540e-0410-9357-904b9bb8a0f7
---
doc/stdlib/index-list.html.template | 6 ++++++
1 file changed, 6 insertions(+)
(limited to 'doc/stdlib')
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index e0f445d03..43761b0ab 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -140,6 +140,7 @@ through the Require Import command.
theories/PArith/POrderedType.v
theories/PArith/Pminmax.v
theories/PArith/Psqrt.v
+ theories/PArith/Pgcd.v
(theories/PArith/PArith.v)
@@ -153,6 +154,7 @@ through the Require Import command.
theories/NArith/Ndist.v
theories/NArith/Ndec.v
theories/NArith/Ndiv_def.v
+ theories/NArith/Ngcd_def.v
theories/NArith/Nsqrt_def.v
(theories/NArith/NArith.v)
@@ -186,6 +188,7 @@ through the Require Import command.
theories/ZArith/Zlog_def.v
theories/ZArith/Zlogarithm.v
(theories/ZArith/ZArith.v)
+ theories/ZArith/Zgcd_def.v
theories/ZArith/Zgcd_alt.v
theories/ZArith/Zwf.v
theories/ZArith/Znumtheory.v
@@ -240,6 +243,7 @@ through the Require Import command.
theories/Numbers/NatInt/NZPow.v
theories/Numbers/NatInt/NZSqrt.v
theories/Numbers/NatInt/NZLog.v
+ theories/Numbers/NatInt/NZGcd.v
@@ -284,6 +288,7 @@ through the Require Import command.
theories/Numbers/Natural/Abstract/NPow.v
theories/Numbers/Natural/Abstract/NSqrt.v
theories/Numbers/Natural/Abstract/NLog.v
+ theories/Numbers/Natural/Abstract/NGcd.v
theories/Numbers/Natural/Abstract/NProperties.v
theories/Numbers/Natural/Binary/NBinary.v
theories/Numbers/Natural/Peano/NPeano.v
@@ -310,6 +315,7 @@ through the Require Import command.
theories/Numbers/Integer/Abstract/ZMaxMin.v
theories/Numbers/Integer/Abstract/ZParity.v
theories/Numbers/Integer/Abstract/ZPow.v
+ theories/Numbers/Integer/Abstract/ZGcd.v
theories/Numbers/Integer/Abstract/ZProperties.v
theories/Numbers/Integer/Abstract/ZDivEucl.v
theories/Numbers/Integer/Abstract/ZDivFloor.v
--
cgit v1.2.3