From 4240d3b53a604bbad63221ef017a7f65decfa483 Mon Sep 17 00:00:00 2001 From: Pierre Rousselin Date: Fri, 15 Sep 2023 15:52:03 +0200 Subject: [PATCH 1/3] Adding a CEP about Reals --- text/000-clean-up-Reals.md | 113 +++++++++++++++++++++++++++++++++++++ 1 file changed, 113 insertions(+) create mode 100644 text/000-clean-up-Reals.md diff --git a/text/000-clean-up-Reals.md b/text/000-clean-up-Reals.md new file mode 100644 index 00000000..41be75a7 --- /dev/null +++ b/text/000-clean-up-Reals.md @@ -0,0 +1,113 @@ +- Title: A cleaner Reals library + +- Drivers: Pierre Rousselin/Villetaneuse + +---- + +# Summary + +Our goal is to clean up the Reals library. In particular: +- Since the main source of documentation are the `.v` files themselves (with + eventually some `coqdoc` formatting), having 82 files is very inconvenient for + the user. Moreover the titles themselves can be misleading. We wish to regroup + the content in a very reduced amount of files (e.g. `Rfunctions.v` could be + one file). +- The proofs in Reals are very outdated, do not respect what is now considered + good practice (strict focusing, not using automatically generated names), and + use auto pervasively with a not very thought off hint database. They tend to + use a lot of unneeded automation because there are many missing lemmas. This + in turn make Reals quite slow to compile. We believe the proofs could be + reworked to be both prettier, shorter, quicker to compile and closer to usual + mathematical practice. +- Some definitions are ill-chosen. We could offer alternatives with translation + lemmas for compatibility. The unfortunate `sum_f_R0` (which lacks a notion of + empty sum) is a good example. +- Some identifiers are ill-chosen in an international setting, for instance, + using `pos` for "positif" (in french) when the intended meaning is + "non-negative" or even worse, using `neg` (for "negative") instead of `opp` + (for "opposite"). Others are not informative at all (for instance `tech_23`). + This should, at least partially, be addressed. Although some concessions will + have to be made in order to preserve, to a large extend, backward + compatibility. +- The logic of Reals (as they were first formalized) is now better understood + (see `Reals/Rlogic.v`). One can derive consequences of the weak excluded + middle and the limited principal of omniscience and use them to simplify + proofs and statements. This was done in the Coquelicot library, to define, for + instance, a total "limit" function on real sequences. It can be used here as + well. + +# Motivation + +We encountered Reals when writing a small course for undergraduate students. +While we were seduced by its simplicity, some aspects were very frustrating. +This lead to a first PR (#17036) with a better `RIneq.v`. +After that, we tried to clean up other files but got carried away. And indeed, +we believe that a substantial change is off the scale of small pull requests. + +We think that a better Reals library could be very useful for teaching +mathematics, for instance in first year of university (or even in high school). +The fact that it does not use a lot of abstraction can be an asset in this +regard. Our course went all the way to convergence of sequences. It would +however be difficult to cover more content without a better designed library. + +While we are aware that the standard library may lose its "standard" status in +the future, this may take some time. And even after demotion, if it does indeed +happen, having a cleaner library would make it easier to find maintainers. + +# Detailed design + +The detailed design is to be discussed with Reals maintainers (namely Hugo +Herbelin, Laurent Théry and Guillaume Melquiond) and/or other Coq developers. + +Here is a first rough and incomplete plan: +1. Yet another PR about `RIneq` completing results about division and + subtraction and adding common one-step reasoning lemmas, for instance + "changing the side of a term" in a equation or an inequality. + These are needed to obtain smaller proofs afterwards and correspond to usual + mathematical practice for, e.g. high school students. +2. Incorporate all parts of `Rfunctions` inside `Rfunctions` itself in, say, the + same order as they are required. This could be split in separate PR (for + instance one for `Rsqr`, one for `Rmin` and `Rmax`, etc). The continuous + integration would tell if the small files need to be kept with a deprecation + period or can be thrown away directly. +3. The same method can then be applied to the other main parts of the library, + namely `SeqSeries` `Rtrigo` `Ranalysis` and `RiemannInt`. + +The following [branch](https://github.com/Villetaneuse/coq/tree/Reals_prototype) +contains an incomplete prototype with `Rfunctions` and `SeqSeries` as single +files. While it still needs more polishing and requires advice, it shows that it +is possible to considerably reduce the size of proofs, without any automation +except that of the `easy` tactic. + +We do not, at this stage, wish to change the underlying logic of the library. We +can work with this middle ground between intuitionistic and classical logic. +While we aim at making important changes, we also wish to preserve, to some +extend, backward compatibility. + +# Drawbacks + +- The major drawback is probably that it may be time consuming for the + maintainers. It could be deemed not worth it. +- Giving alternative (better) definitions could lead to increase unreasonably + the number of lemmas, this will have to be carefully balanced. +- Having less files *could* lead, in a heavily multithreaded environment to + increased compilation time (but we deem it unlikely). + +# Alternatives + +- It may be possible to be less ambitious regarding the changes, only cleaning + up some proofs and deprecating some lemmas, without touching the general + structure of the library. +- Another possible design was described by Vincent Semeria: have a first layer + of constructive mathematics and a second layer specialized using stronger + axioms. It would be beautiful but it does not solve our issues. + +# Unresolved questions + +- The status of functional extensionality in Reals has not, to our knowledge, + been discussed. It is used to define the real numbers but never after. + Maybe it is to keep Reals independent of this particular construction. +- The same question holds for Setoids. They are used in the definition of real + numbers. This allows to use `setoid_rewrite` during the development, which + can be very handy (we can rewrite under `forall` and `exists`). With + functional extensionality and Setoids, we could rewrite under `fun` too. From 2caa44cf5ce6d5f578a85a8c57c5061b7ef9de4c Mon Sep 17 00:00:00 2001 From: Pierre Rousselin Date: Mon, 18 Sep 2023 11:14:08 +0200 Subject: [PATCH 2/3] Mention mathcomp-analysis and C-Corn --- text/000-clean-up-Reals.md | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/text/000-clean-up-Reals.md b/text/000-clean-up-Reals.md index 41be75a7..cd4b4721 100644 --- a/text/000-clean-up-Reals.md +++ b/text/000-clean-up-Reals.md @@ -101,6 +101,26 @@ extend, backward compatibility. - Another possible design was described by Vincent Semeria: have a first layer of constructive mathematics and a second layer specialized using stronger axioms. It would be beautiful but it does not solve our issues. +- The library `mathcomp-analysis` is a very advanced analysis library built on + top of Mathcomp, ssreflect and Hierarchy Builder. + A definition of the real numbers is given (taken, if we're not mistaken from + the pre-existing library coq-alternate-reals) but is seldom, if ever, used. + Its lemmas are very general and do not rely on a specific construction of the + real numbers, but are parameterized by instances of type `realType`. + Its logic is stronger than that of Reals, assuming not only functional + extensionality but also propositional extentionality and constructive + indefinite description (which in turn imply the excluded middle in its + strongest form). Most basic lemmas are instead very general lemmas about, say, + abelian groups or ordered fields of which real numbers are just another + instance. While it certainly is a very carefully written library, it is very + involved and, in our opinion, demanding for the average Coq user. We would not + use it with first year undergraduate students for instance. Furthermore, + unless Flocq and Coquelicot are in a large part rewritten, they will still + depend on Reals. So I think mathcomp-analysis and Reals should coexist, as + they target very different users and have very different philosophies. +- The library C-Corn is another analysis library with constructions of real + numbers. It focuses mostly on constructive analysis so is probably less + practical for a classical introductory mathematics course. # Unresolved questions From 2cc502a57e77b12624f26e119927e4fcd7abc5e9 Mon Sep 17 00:00:00 2001 From: Pierre Rousselin Date: Fri, 29 Sep 2023 15:42:20 +0200 Subject: [PATCH 3/3] Correct statements about math-comp/analysis Also, mention Math-classes and coq/coq#17877 --- text/.000-clean-up-Reals.md.swp | Bin 0 -> 20480 bytes text/000-clean-up-Reals.md | 47 +++++++++++++++++--------------- 2 files changed, 25 insertions(+), 22 deletions(-) create mode 100644 text/.000-clean-up-Reals.md.swp diff --git a/text/.000-clean-up-Reals.md.swp b/text/.000-clean-up-Reals.md.swp new file mode 100644 index 0000000000000000000000000000000000000000..c6f04af3819669ca41bc39aa20635d6843b8c5d9 GIT binary patch literal 20480 zcmeI4NsJ`fS;qs0&7LvFfH)!hxkiX;t17E!2788k7?VgZqES5ntU1YvNEP3 z<7LNE*=eyIfD=dv8H9wz0dw(zu@5Yk4;Bb<;(`P>vj`z15STl{3%~#OBC@I*d+Zwm zMM+;R84+*!e`~z|r&?Tp`Q|P6xAu06@arakGxz3$}t_3OuZ6?}c%Z;nrcuiDwV_$Gr*mnQ@! z1ip0y`fhpr)LXJA9)HYS{n3MWx*z!dk9_OTPj^lTObAQ}ObAQ}ObAQ}ObAQ}ObGm+ zN1)q0l>Gv``1WBZ&ksMp?SY@)G5r0$;pYnvTz_czd;Iw;4_qJqoPJCQObAQ}ObAQ} zObAQ}ObAQ}ObAQ}ObAQ}ObGlhAmHKIA7$PT>4hKue|-P{hqq?g-y?s7{2}rg&QPol4ZYzynq}dfA?^f{Ti}H9P-6C^EdKd z?R%IP$&nvK9zh;PzWUu+_7&u_NRAvJfBjuq_RGjGA@4=L^qpDu zd&o~BZ${pPe4Yc0*N}H0Z$}^ZV_C&smjikwQIx1H@*w* z!>8_W8Jq0!nY&r%vDrlX*jJU~j;?ia>E@@)zRtTc*6o~!+p-7`eAcz0T5{=#1?`Ts zj*P{vJ-_g+%srzuo+0w!nC-}g+1bpk%CnVg^Hq$MYrDP(b=S`H;GI=ygKeY^p$LWR zqKk{pYvF5_#%?!FjLX*fWfz*QZwh{`3pPp*NxO;s$|HT-`%2>->Z4MllTwptu> zXDpMSc+NVxs|eOXn$ z$AE5y3VQ*yYr1g4n$rrOjdxuUE25g-(jlmS-S^*+tn_QMP&Cwp`hk z-O5>K4JJ_5(i@Mv!y03)cJ9UgED{IYbN7#wWh=kg1lGFp7s9|hYtsR#s$4XlRd3CX z*Zv#;ItSSF3~Bad$#$+xHOr*uW#6%9StDy)`n(RSFXd%J4p?PHY-k;2 z0!OaImOEF((1K}!31+XX*t6Rvqx2XYW2}6a>lx6Irm+?LBSN88#-9`)%uGJYQGP8t)MvJ%hDU0SDr2j>BnS=NLzCYZSo^$m~p z4O4IRsJvK6Y_)j}UNibxz!v4!EhettTU?)Mgso|KiKC|7jUZsKI1`&^Tb&;Di+1l1 zIqrh``R>uaMHeBSU3&imegFW2>F$EZ)RwNVOBUARZSD}`Go5hLmH2RNmc1g#%lbSm zZI4E>v(ZBKk&f|pTJy56%n7^TbDloSGL$HvV3Khpyjx1@O2U*y3iGeHTyg^jL-a~` zDfGBa&o{-_&?;IzZKfkzIFfmEO_{=#nXcQ-R_Z|rjxwAh&~wk6@A z%)yyJEkE$>Cgd2Y-E5F8n_j9_5HiRykl160B$L6Vw<|nm+msfkdCOcRj zS}q&`Roh{>F*D%Ya=5Uzv_jwm*)2)3AY97?rCS1Ak1gcrWUwH@MI;gsQHUH$jHI!$ zD6jy$*q*VqG2^Bo-j*9yg$2iTP53L#wREGrg$dRgEup^LG1OrjlseUPcye0Bvoc3% z*Kk~xq}_lVo*+lv?^L6k4+nql!o9pAPZrrR`w4g>Bj|?Y1cze@VCqcSfh}OR<;MfD z9RTXM9m9y}sqJDcSeOzAidmFn$|DA|0}JeHPre7RRA%tmhU^rY3x(FGnBa*iERASY z9Jz(h&y|oF)F5vOUKO7cEU|0ymC6b{t-=NsHj0AL&>((LDbT4TkZFPep-EW}wUMZV zp3LhYZZ?rn5e|eK$dFkSjuoTI+O~_4F>nfh_RMHuZr+7__3GnKfH~tG)UiIUiJf}j zK$+hn&o&Z3k5HkK(46b@Vdnjw2B}5J>0q|#pooR6eZ3>dVCz^x z(n+e@$KiO`QGi`g?@)_T2C2R>=$*yv5b>%mntO z_#vUbB-t+`m7AGR%Jf>uxMZ>)Q&Kbpy%-cuMO=Fgf2I^oQD^`G5EFFTldX%Yg_Q)H zzli3as?EtaI04={L?gvI44(YL@)VktD$PCRC0w;4NOqqFoHNna(ebkkmGBdxfd54i94p{|-C=UaLX?)Cc8FlRI5{s)uasJ-^hLV%JMccnF_(PNNiv_nXlU2RgCDlq@=NSbT{i1k*Pp^ z!z;t1?sm_+OS9uOnlHY)=aiJ1_J;eg_2|3Ps5+n5ij$Y|ZmRe?fUNGkBQ$Tgr}vfn zeUoK+|Njc_?eFAWUhn@84ez&l-}i_fnO5>TkF{gFEUhw8W(8xR!w|1bQ1FSh@ z59@k$7<=xDo)hszu@0o64lP)=9T>6|s4Z0NPUm!P-f8%`Mb>t6_ zpF!S=d;xxcgM1LVg?t%)|1(IAJc~Soya#zV@*i;hUqCj<3Gz?y{lANR6!~f71ISCr zf5H2I7WoA7Jo2CL{eOb2kRL<-6|Vo2$On)w!}Gt6d<=OT@)vOYTjUV=BE0^uBF`X) z$lr3P@f*lX$XDU?KZpD#@(JYUke@|n$UlR@ClO(BQ+Pb^mCn|T-#4yFXNRj;L3HaB z9Gm#2H^^wDxuGWjorxm0GoZ^uS{pk8acZ;Sba5a} zb%TaD3*@;XB}}&%%)owmwpG02w*tD>xd4zS9}Ch$xOs zo5-nR7vT)A(3bKxr~qwAr}aE+oY$Ty5}hX`nz--_jsZDH)L+);z#^q5aoEtJ>VROB z%dxqfAcLXCvlDj!8}*~O*KUK;>ZyU5%|jy!oe7vMoq}pb5Xq_SLMOd25j6_zR{U!V zds1ZDNQ#2pNZ6*0!0>X=sZ&Qc!f#r#b6~ElW7{zuLtd&@lnOy<*Otks+_T4YTh!wu zgSN&gpFMt77qwvY0ZFreczht8VqcCgzTnapi&6}M>}>;~8QaJY;9$K;(TP=Jc^19c ztR3Ns;)jdsQV6^p1Je_g!XdcPS_+VilmZvw7ITr4h-E@6`ku^P0N8Xhco}z7b`Sk5 zC5lcs9^ufy3@3GuMAOW@&^Ow)n0(Y*n`yjI#r&=<;|lNSInKp?M;cA+7=yvSH6B)t z8;4VCxRccWkdElhQH=;lJfBhNU!QtqIHe0VI$}?UgITU+in6{)KEXD)0GET~#7$Y_ z9-Q3Mz*AeZi}uHs7;W@eE&Vm_QF<#N%;^iwTArTAJ$VFMd3lxsJ zh`g8+a;0<`<=NjjwkgO!7mIa`iBZ&Y7)}jb>p)l%xoZsn&}U@8SQMEHm^;Lix!jw^ z0^^Hu$^i~36oA#ez<>iCxaVq81c2d(vw@AwuLJ`egWU*k%`h4Sgsv9LfAKNiDMfmt z0!Pmt?^Iw&v0hn$#U(lwWYl@WMK$P{TQXD^>7rO#bd%p<9WC}#iAa)5zX&Pen|!r% z&(P3>fsC1Bj79VR;j#0}ND2Xcq2?@lx`yaBItiO8Y08N;OYrx~xW3XSqcUp|pvX$~ zmslPc`h}!X%Q5Cgka{EGcs~(;P`|$ zv9W=}v{Y!<#$Go?BQ+{@vA0$mvyZ{QS@q41(76+G`*l+d@TbK_zh1~vXpc(GOk*XP z`f*5+<|amDaY@;nc7a5KL)s~eL%$6jGEY7Eq~aJJCauDJlGZg9wtBARTO~uY2Bfp~ zvRI9*-2xZ)D4Qm}I1z5LMRzDAQ%%ziwpR2cq?hNAu_~L1%t{){E$s8f)V*fAO7z^j ztZIK38}%u|dfHXE3kO@%_XTXss#btdUzEftmCY=e16$n4(N)gr^r^yZ{SgH);*>O(J( zQWAy*lG|Wi86E8c0LhyaaZ)z7FZ)u^wO*g)ElDl9Bu7*7qk*|mI>@JMxa(YF>dOO^`O*{)U+EDkYaiI#?9pG6;y`gFWAEjZG zew&XSuDWj1-Z(iqV^95J#w7QV)`}P>T@%8|DT%Co6$sMY*A!B$*#R$|Uzu@!O3%bu zoV)qym@$TBotCPV>YH^(AKnx8=9T)h$6a&kSE`=1lQq9=WYNxJNjcFa!L*syy zH^h%~*^&Y76(duKx8%ooYL8Seg4#1!!2Gnm+sqY{$G?fSBMNJOk4vG;35|D{Pg*YP Ip3t8CH=W%+fB*mh literal 0 HcmV?d00001 diff --git a/text/000-clean-up-Reals.md b/text/000-clean-up-Reals.md index cd4b4721..d34f6039 100644 --- a/text/000-clean-up-Reals.md +++ b/text/000-clean-up-Reals.md @@ -40,7 +40,7 @@ Our goal is to clean up the Reals library. In particular: We encountered Reals when writing a small course for undergraduate students. While we were seduced by its simplicity, some aspects were very frustrating. -This lead to a first PR (#17036) with a better `RIneq.v`. +This lead to a first PR (coq/coq#17036) with a better `RIneq.v`. After that, we tried to clean up other files but got carried away. And indeed, we believe that a substantial change is off the scale of small pull requests. @@ -91,7 +91,8 @@ extend, backward compatibility. - Giving alternative (better) definitions could lead to increase unreasonably the number of lemmas, this will have to be carefully balanced. - Having less files *could* lead, in a heavily multithreaded environment to - increased compilation time (but we deem it unlikely). + increased compilation time (but we deem it unlikely). We will have + coq/coq#17877 in mind and try to break dependencies when we can. # Alternatives @@ -103,24 +104,26 @@ extend, backward compatibility. axioms. It would be beautiful but it does not solve our issues. - The library `mathcomp-analysis` is a very advanced analysis library built on top of Mathcomp, ssreflect and Hierarchy Builder. - A definition of the real numbers is given (taken, if we're not mistaken from - the pre-existing library coq-alternate-reals) but is seldom, if ever, used. - Its lemmas are very general and do not rely on a specific construction of the - real numbers, but are parameterized by instances of type `realType`. - Its logic is stronger than that of Reals, assuming not only functional - extensionality but also propositional extentionality and constructive - indefinite description (which in turn imply the excluded middle in its - strongest form). Most basic lemmas are instead very general lemmas about, say, - abelian groups or ordered fields of which real numbers are just another - instance. While it certainly is a very carefully written library, it is very - involved and, in our opinion, demanding for the average Coq user. We would not - use it with first year undergraduate students for instance. Furthermore, - unless Flocq and Coquelicot are in a large part rewritten, they will still - depend on Reals. So I think mathcomp-analysis and Reals should coexist, as - they target very different users and have very different philosophies. + The definition of real numbers is never used. Instead, at this time, the + lemmas do not rely on a specific construction of the real numbers, but are + parameterized by instances of type `realType`. Its logic is stronger than that + of Reals, assuming not only functional extensionality but also propositional + extentionality and constructive indefinite description (which in turn imply + the excluded middle in its strongest form). Most basic lemmas are instead very + general lemmas about, say, abelian groups or ordered fields of which real + numbers are just another instance. While it certainly is a very carefully + written library, it is very involved and, in our opinion, demanding for the + average Coq user. We would not use it with first year undergraduate students + for instance. Furthermore, unless Flocq and Coquelicot are in a large part + rewritten, they will still depend on Reals. So I think mathcomp-analysis and + Reals should coexist, as they target very different users and have very + different philosophies. - The library C-Corn is another analysis library with constructions of real - numbers. It focuses mostly on constructive analysis so is probably less - practical for a classical introductory mathematics course. + numbers. It focuses mostly on constructive analysis. The C-corn library + is itself based on Math-classes, a library of abstract interfaces for + mathematical structures, using Coq's type classes. It certainly is a very + interesting library, but is probably less practical for a classical + introductory mathematics course. # Unresolved questions @@ -128,6 +131,6 @@ extend, backward compatibility. been discussed. It is used to define the real numbers but never after. Maybe it is to keep Reals independent of this particular construction. - The same question holds for Setoids. They are used in the definition of real - numbers. This allows to use `setoid_rewrite` during the development, which - can be very handy (we can rewrite under `forall` and `exists`). With - functional extensionality and Setoids, we could rewrite under `fun` too. + numbers. This allows to use `setoid_rewrite` during the development, which can + be very handy (we can rewrite under `forall` and `exists`). With functional + extensionality and Setoids, we could rewrite under `fun` too.