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 ++++++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100644 doc/changelog/10-standard-library/10445-constructive-reals.rst (limited to 'doc/changelog') 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. -- 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/changelog') 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