From eebc676ce4978b7e408c427889bae356d8b0efdc Mon Sep 17 00:00:00 2001 From: Vincent Semeria Date: Thu, 27 Jun 2019 23:35:03 +0200 Subject: Define constructive real numbers as Cauchy sequences of rational numbers. Redefine classical real numbers as a quotient of those constructive real numbers. --- .../10445-constructive-reals.rst | 30 ++++++++++++++++++++++ doc/stdlib/index-list.html.template | 3 +++ 2 files changed, 33 insertions(+) create mode 100644 doc/changelog/10-standard-library/10445-constructive-reals.rst (limited to 'doc') diff --git a/doc/changelog/10-standard-library/10445-constructive-reals.rst b/doc/changelog/10-standard-library/10445-constructive-reals.rst new file mode 100644 index 0000000000..dc5c97f895 --- /dev/null +++ b/doc/changelog/10-standard-library/10445-constructive-reals.rst @@ -0,0 +1,30 @@ +- New module `Reals.ConstructiveCauchyReals` defines constructive real numbers + by Cauchy sequences of rational numbers. Classical real numbers are now defined + as a quotient of these constructive real numbers, which significantly reduces + the number of axioms needed (see `Reals.Rdefinitions` and `Reals.Raxioms`), + while preserving backward compatibility. + + Futhermore, the new axioms for classical real numbers include the limited + principle of omniscience (`sig_forall_dec`), which is a logical principle + instead of an ad hoc property of the real numbers. In a future pull request + we propose to deduce the other axiom, `completeness`, from the logical + principle `sig_not_dec` (see `Reals.Rlogic`), which is the excluded middle + of negations in sort `Type`. + + If we want the axioms to be completely logical, we could also replace the + quotient axioms by functional extensionality, which gives the correct + equality to the equivalences classes represented as `bool`-valued functions + (also using Hedberg to get the unicity of proofs that those functions + are indeed equivalence classes). However that last part is not + completely backward compatible : it assumes funext, which is more + powerful than ad hoc quotient axioms. + + Future work includes the development of constructive analysis, by + moving the constructive lemmas in new modules (see `Reals.RIneq_constr`), + and by interfacing tighter with libraries C-CoRN and math-classes. + Since the constructive definitions are weaker, this will require + to adapt the definitions in some places. We also need to work on + efficient extractions of constructive real numbers, so that we can + compute them in practice. + + See `#10445 `_, by Vincent Semeria. diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index a561de1d0c..eb7c982d49 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -516,7 +516,9 @@ through the Require Import command.

theories/Reals/Rdefinitions.v + theories/Reals/ConstructiveCauchyReals.v theories/Reals/Raxioms.v + theories/Reals/RIneq_constr.v theories/Reals/RIneq.v theories/Reals/DiscrR.v theories/Reals/ROrderedType.v @@ -561,6 +563,7 @@ through the Require Import command.

theories/Reals/Ranalysis5.v theories/Reals/Ranalysis_reg.v theories/Reals/Rcomplete.v + theories/Reals/Rcomplete_constr.v theories/Reals/RiemannInt.v theories/Reals/RiemannInt_SF.v theories/Reals/Rpow_def.v -- cgit v1.2.3 From d92c1fd7e17237652fd84e353a68cf776dc09563 Mon Sep 17 00:00:00 2001 From: Vincent Semeria Date: Wed, 17 Jul 2019 08:32:20 +0200 Subject: Rename ConstructiveRIneq and ConstructiveRcomplete --- doc/stdlib/index-list.html.template | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'doc') diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index eb7c982d49..61d601be7d 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -518,7 +518,7 @@ through the Require Import command.

theories/Reals/Rdefinitions.v theories/Reals/ConstructiveCauchyReals.v theories/Reals/Raxioms.v - theories/Reals/RIneq_constr.v + theories/Reals/ConstructiveRIneq.v theories/Reals/RIneq.v theories/Reals/DiscrR.v theories/Reals/ROrderedType.v @@ -563,7 +563,7 @@ through the Require Import command.

theories/Reals/Ranalysis5.v theories/Reals/Ranalysis_reg.v theories/Reals/Rcomplete.v - theories/Reals/Rcomplete_constr.v + theories/Reals/ConstructiveRcomplete.v theories/Reals/RiemannInt.v theories/Reals/RiemannInt_SF.v theories/Reals/Rpow_def.v -- cgit v1.2.3 From a1359ffb3d95686f6176b1d4a893f16252fc745c Mon Sep 17 00:00:00 2001 From: Vincent Semeria Date: Thu, 18 Jul 2019 20:33:11 +0200 Subject: Shorten changelog --- .../10445-constructive-reals.rst | 24 +++------------------- 1 file changed, 3 insertions(+), 21 deletions(-) (limited to 'doc') diff --git a/doc/changelog/10-standard-library/10445-constructive-reals.rst b/doc/changelog/10-standard-library/10445-constructive-reals.rst index dc5c97f895..d69056fc2f 100644 --- a/doc/changelog/10-standard-library/10445-constructive-reals.rst +++ b/doc/changelog/10-standard-library/10445-constructive-reals.rst @@ -6,25 +6,7 @@ Futhermore, the new axioms for classical real numbers include the limited principle of omniscience (`sig_forall_dec`), which is a logical principle - instead of an ad hoc property of the real numbers. In a future pull request - we propose to deduce the other axiom, `completeness`, from the logical - principle `sig_not_dec` (see `Reals.Rlogic`), which is the excluded middle - of negations in sort `Type`. + instead of an ad hoc property of the real numbers. - If we want the axioms to be completely logical, we could also replace the - quotient axioms by functional extensionality, which gives the correct - equality to the equivalences classes represented as `bool`-valued functions - (also using Hedberg to get the unicity of proofs that those functions - are indeed equivalence classes). However that last part is not - completely backward compatible : it assumes funext, which is more - powerful than ad hoc quotient axioms. - - Future work includes the development of constructive analysis, by - moving the constructive lemmas in new modules (see `Reals.RIneq_constr`), - and by interfacing tighter with libraries C-CoRN and math-classes. - Since the constructive definitions are weaker, this will require - to adapt the definitions in some places. We also need to work on - efficient extractions of constructive real numbers, so that we can - compute them in practice. - - See `#10445 `_, by Vincent Semeria. + See `#10445 `_, by Vincent Semeria, + with the help and review of Guillaume Melquiond and Bas Spitters. -- cgit v1.2.3