[Merged by Bors] - feat: monotonicity lemmas for OrdinalApprox#15522
[Merged by Bors] - feat: monotonicity lemmas for OrdinalApprox#15522PhoenixIra wants to merge 13 commits intomasterfrom
Conversation
PR summary b46332a675Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
vihdzp
left a comment
There was a problem hiding this comment.
Sorry this took so long. I would've reviewed earlier, but I had never heard about "ordinal approximants" to fixed points. For a good while I thought the ordinals themselves were the ones being approximated!
| intro f g h x a | ||
| induction a using Ordinal.induction with | ||
| | h i ih => | ||
| unfold lfpApprox |
There was a problem hiding this comment.
Having to unfold a definition over and over is somewhat of an antipattern. The issue here is that since your definition of lfpApprox is recursive, it's not unfolded by default, causing it not to be definitionally equal. A simple fix is to introduce a lemma like
theorem lfpApprox_def (a : Ordinal) :
lfpApprox f x a = sSup ({ f (lfpApprox f x b) | (b : Ordinal) (_ : b < a) } ∪ {x}) := by
rw [lfpApprox]and to rewrite using that lemma (which notably, is now searchable) instead of using unfold.
There was a problem hiding this comment.
I added that theorem and refactored it in the previous existing theorems. Is this fine, or should the second part be a separate PR?
|
Thank you very much for the review! |
|
As a separate thing, I've skimmed through the two references provided, and neither calls these values "ordinal approximants". I find the name to be quite misleading, as really, the approximations are simply ordinal-indexed. Moreover, the file never mentions the actual result being built towards, that the fixed points of a monotone function on a complete lattice form a complete lattice themselves. Do you think you could add this documentation to the file in a separate PR? |
|
I can create a separate PR to fix the name confusion. Do you expect this separate PR to only change the wording of "ordinal approximants" to "ordinal-indexed approximants", or would you also like to see some more details (which?) regarding the chosen name? |
|
Just that change, and a better docstring for By the way, I just noticed that |
|
FYI I just opened #16361 which simplifies a lot of the proofs that were already in the file. |
|
I have created the doc PR here: #16406 I do not plan to further make any connections between this theorem and fixedPoints.completeLattice. I believe both proofs are used for different applications. It is sometimes nice to argue about pre fixed points (as Tarski's Theorem is enabling), but it is sometimes nice to be able to apply transfinite induction on fixed points (as Cousot-Cousot's Theorem is enabling). I considered to maybe generalize the ordinal-indexed approximations to domains with a complete partial order instead of complete lattices - but I have no plan to do it yet. |
|
Moreover, I think it is redundant to give another construction of a complete lattice of fixed points in this file, as the supremum of fixed points is constructed analogous to Tarski's theorem, as far as I remember. The connection to the least fixed point and the greatest fixed point however are created in |
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
As mentioned in #15522, the documentation uses heavily the wording "ordinal approximation", which suggests that ordinals are approximated. This PR changes it to "ordinal-indexed approximation" and highlights the indexed nature of ordinals in various places. It also fixes some apparent then vs than errors. I appreciate any suggestions to further improve the documentation and hints for spelling mistakes. [](https://gitpod.io/from-referrer/) Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com> Co-authored-by: Ira Fesefeldt <public@feuervogel.me>
fpvandoorn
left a comment
There was a problem hiding this comment.
One comment, otherwise LGTM.
bors d+
|
✌️ PhoenixIra can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
As mentioned in #15522, the documentation uses heavily the wording "ordinal approximation", which suggests that ordinals are approximated. This PR changes it to "ordinal-indexed approximation" and highlights the indexed nature of ordinals in various places. It also fixes some apparent then vs than errors. I appreciate any suggestions to further improve the documentation and hints for spelling mistakes. [](https://gitpod.io/from-referrer/) Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com> Co-authored-by: Ira Fesefeldt <public@feuervogel.me>
|
bors r+ |
This PR adds two lemmas about monotonicity for `lfpApprox` and `gfpApprox` each. I found them helpful when working with the API. Co-authored-by: Ira Fesefeldt <public@feuervogel.me> Co-authored-by: Ira Fesefeldt <9974411+PhoenixIra@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
This PR adds two lemmas about monotonicity for `lfpApprox` and `gfpApprox` each. I found them helpful when working with the API. Co-authored-by: Ira Fesefeldt <public@feuervogel.me> Co-authored-by: Ira Fesefeldt <9974411+PhoenixIra@users.noreply.github.com>
This PR adds two lemmas about monotonicity for
lfpApproxandgfpApproxeach. I found them helpful when working with the API.I am a bit unsure about the names and would welcome any suggestions. Especially to make them fit with the already present monotonicity lemma.
Moreover, I could now express the monotonicity for the functions inlfpApprox_mono₁in terms ofMonotone. I welcome any suggestions to express it withMonotone.