From eee738a6848e926dd9852067c1192920b36909a0 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 7 May 2020 07:30:32 +0900 Subject: [PATCH 1/7] start a contributing file (wip) --- CONTRIBUTING.md | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 CONTRIBUTING.md diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md new file mode 100644 index 000000000..f43548e76 --- /dev/null +++ b/CONTRIBUTING.md @@ -0,0 +1,28 @@ +# Contribution Guide for the mathcomp-analysis library (WIP) + +## `=>` vs. `-->` vs. cvg vs. lim + +TODO: explain in particular the lemmas `cvgP`, `cvg_ex` + +## `near` tactics vs. `filterS`, `filterS2`, `filterS3` lemmas + +TODO + +## idioms + +### How to introduce a positive real number? + +When introducing a positive real number, it is best to turn it into a +`posnum` whose type is equipped with better automation. There is an +idiomatic way to perform such an introduction. Given a goal of the +form +``` +========================== +forall e : R, 0 < e -> G +``` +the tactic `move=> _/posnumP[e]` performs the following introduction +``` +e : {posnum R} +========================== +G +``` From 3678ba235f8351c4cd44f8eb17779d398734dea1 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 7 May 2020 19:02:36 +0900 Subject: [PATCH 2/7] add link to mathcomp's contribution guide --- CONTRIBUTING.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index f43548e76..20cffc5ff 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -1,5 +1,10 @@ # Contribution Guide for the mathcomp-analysis library (WIP) +The purpose of this file is to document scripting techniques to be +used when contributing to mathcomp-analysis. It comes as an addition +to mathcomp's [contribution +guide](https://github.com/math-comp/math-comp/blob/master/CONTRIBUTING.md). + ## `=>` vs. `-->` vs. cvg vs. lim TODO: explain in particular the lemmas `cvgP`, `cvg_ex` From a4a7d008b959cc7ef031e956a7296b30cf778e8d Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 8 May 2020 03:48:29 +0900 Subject: [PATCH 3/7] add a comment about near tactics vs. filter lemmas --- CONTRIBUTING.md | 22 +++++++++++++++++++--- 1 file changed, 19 insertions(+), 3 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 20cffc5ff..d1f2d0d16 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -1,17 +1,31 @@ -# Contribution Guide for the mathcomp-analysis library (WIP) +# Contribution Guide for the mathcomp-analysis library (WIP) The purpose of this file is to document scripting techniques to be used when contributing to mathcomp-analysis. It comes as an addition to mathcomp's [contribution guide](https://github.com/math-comp/math-comp/blob/master/CONTRIBUTING.md). -## `=>` vs. `-->` vs. cvg vs. lim +## `=>` vs. `-->` vs. `cvg` vs. `lim` TODO: explain in particular the lemmas `cvgP`, `cvg_ex` ## `near` tactics vs. `filterS`, `filterS2`, `filterS3` lemmas -TODO +When dealing with limits, mathcomp-analysis favors filters +that are behind goals such as +``` +{near \oo, G}. +``` +In the presence of such goals, the `near` tactics can be used to +recover epsilon-delta reasoning +(see [this paper](https://doi.org/10.6092/issn.1972-5787/8124)). + +However, when the proof does not require changing the epsilon it +is often worth using filters and lemmas such as +``` +filterS : forall T (F : set (set T)), Filter F -> forall P Q : set T, P `<=` Q -> F P -> F Q +``` +and its variants (`filterS2`, `filterS3`, etc.). ## idioms @@ -31,3 +45,5 @@ e : {posnum R} ========================== G ``` + +## TODO: Landau notations \ No newline at end of file From df6a1406e0cf199a9f0930cab5e4dc85e198f39b Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 12 Jun 2020 00:40:37 +0900 Subject: [PATCH 4/7] move comment about PR from readme.md to contributing.md --- CONTRIBUTING.md | 13 ++++++++++--- README.md | 3 +-- 2 files changed, 11 insertions(+), 5 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index d1f2d0d16..42754b295 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -5,6 +5,11 @@ used when contributing to mathcomp-analysis. It comes as an addition to mathcomp's [contribution guide](https://github.com/math-comp/math-comp/blob/master/CONTRIBUTING.md). +## Policy for Pull Requests + +Always submit a pull request for code and wait for the CI to pass before merging. +Text markup files may be edited directly though, should you have commit rights. + ## `=>` vs. `-->` vs. `cvg` vs. `lim` TODO: explain in particular the lemmas `cvgP`, `cvg_ex` @@ -27,7 +32,11 @@ filterS : forall T (F : set (set T)), Filter F -> forall P Q : set T, P `<=` Q - ``` and its variants (`filterS2`, `filterS3`, etc.). -## idioms +## Landau notations + +TODO + +## Idioms ### How to introduce a positive real number? @@ -45,5 +54,3 @@ e : {posnum R} ========================== G ``` - -## TODO: Landau notations \ No newline at end of file diff --git a/README.md b/README.md index 445f935f9..b2402da62 100644 --- a/README.md +++ b/README.md @@ -28,8 +28,7 @@ authors). ## Contributing -Always submit a pull request for code and wait for the CI to pass before merging. -Text markup files may be edited directly though, should you have commit rights. +see [CONTRIBUTING.md](CONTRIBUTING.md) ## License From 01e58b895e66015ffa5f53b547fb045f241fffd2 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 18 Jun 2020 04:00:04 +0900 Subject: [PATCH 5/7] naming convention about homo/mono lemmas --- CONTRIBUTING.md | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 42754b295..531b94d58 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -36,6 +36,20 @@ and its variants (`filterS2`, `filterS3`, etc.). TODO +## Naming convention + +### homo and mono notations + +Statements of `{homo ...}` or `{mono ...}` shouldn't be named after `homo`, or `mono` +(just as for `{morph ...}` lemmas). Instead use the head of the unfolded statement +(for `homo`) or the head of the LHS of the equality (for `mono`). + +When a `{mono ...}` lemma subsumes `{homo ...}`, it gets priority +for the short name, and, if really needed, the corresponding `{homo ...}` +lemma can be suffixed with `W`. If the `{mono ...}` lemma is +only valid on a subdomain, then the `{homo ...}` lemma takes the +short name, and the `{mono ...}` lemma gets the suffix `in`. + ## Idioms ### How to introduce a positive real number? From 3ea8a270d7380ae4c4c252c07a68fc2c04769a44 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Sat, 8 Aug 2020 00:09:06 +0200 Subject: [PATCH 6/7] Minor fixes --- CONTRIBUTING.md | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 531b94d58..92298d176 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -1,6 +1,6 @@ # Contribution Guide for the mathcomp-analysis library (WIP) -The purpose of this file is to document scripting techniques to be +The purpose of this file is to document coding styles to be used when contributing to mathcomp-analysis. It comes as an addition to mathcomp's [contribution guide](https://github.com/math-comp/math-comp/blob/master/CONTRIBUTING.md). @@ -17,16 +17,16 @@ TODO: explain in particular the lemmas `cvgP`, `cvg_ex` ## `near` tactics vs. `filterS`, `filterS2`, `filterS3` lemmas When dealing with limits, mathcomp-analysis favors filters -that are behind goals such as +phrasing, as in ``` -{near \oo, G}. +\forall x \near \oo, P x. ``` In the presence of such goals, the `near` tactics can be used to recover epsilon-delta reasoning (see [this paper](https://doi.org/10.6092/issn.1972-5787/8124)). However, when the proof does not require changing the epsilon it -is often worth using filters and lemmas such as +is might be worth using filter combinators, i.e. lemmas such as ``` filterS : forall T (F : set (set T)), Filter F -> forall P Q : set T, P `<=` Q -> F P -> F Q ``` @@ -42,7 +42,10 @@ TODO Statements of `{homo ...}` or `{mono ...}` shouldn't be named after `homo`, or `mono` (just as for `{morph ...}` lemmas). Instead use the head of the unfolded statement -(for `homo`) or the head of the LHS of the equality (for `mono`). +(for `homo`) or the head of the LHS of the equality (for `mono`), as in +```coq +Lemma le_contract : {mono contract : x y / (x <= y)%O}. +``` When a `{mono ...}` lemma subsumes `{homo ...}`, it gets priority for the short name, and, if really needed, the corresponding `{homo ...}` From b74dce4e008958cecd772ec165fa7821fed03b5d Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Sat, 8 Aug 2020 00:23:49 +0200 Subject: [PATCH 7/7] a short description for cvg and landau --- CONTRIBUTING.md | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 92298d176..dbcc1fd25 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -10,9 +10,11 @@ guide](https://github.com/math-comp/math-comp/blob/master/CONTRIBUTING.md). Always submit a pull request for code and wait for the CI to pass before merging. Text markup files may be edited directly though, should you have commit rights. -## `=>` vs. `-->` vs. `cvg` vs. `lim` +## `-->` vs. `cvg` vs. `lim` -TODO: explain in particular the lemmas `cvgP`, `cvg_ex` +- `F --> x` means `F` tends to `x`. _This is the preferred way of stating a convergence._ **Lemmas about it use the string `cvg`.** +- `lim F` is the limit of `F`, it makes sense only when `F` converges and defaults to a distinguished point otherwise. _It should only be used when there is no other expression for the limit._ **Lemmas about it use the string `lim`.** +- `cvg F` is defined as `F --> lim F`, and is equivalent through `cvgP` and `cvg_ex` to the existence of some `x` such that `F --> x`. _When the limit is known, `F --> x` should be preferred._ **Lemmas about it use the string `is_cvg`.**``` ## `near` tactics vs. `filterS`, `filterS2`, `filterS3` lemmas @@ -34,7 +36,13 @@ and its variants (`filterS2`, `filterS3`, etc.). ## Landau notations -TODO +Landau notations can be written in four shapes: +- `f =o_F e` (i.e. functional with a simple right member, thus a binary notation) +- `f = g +o_F e` (i.e. functional with an additive right member, thus ternary) +- `f x =o_(x \near F) (e x)` (i.e. pointwise with a simple right member, thus binary) +- `f x = g x +o_(x \near F) (e x)` (i.e. pointwise with an additive right member, thus ternary) + +The outcome is an expression with the normal Leibniz equality `=` and term `'o_F` which is not parsable. See [this paper](https://doi.org/10.6092/issn.1972-5787/8124) for more explanation and the header of the file [landau.v](https://github.com/math-comp/analysis/blob/master/theories/landau.v). ## Naming convention