2023 12 21 Meeting

Participants: Alessandro, Georges, Pierre, Quentin, Reynald, Takafumi

• which keywords to add to opam files?
  • see PR 1125
• about the release of MathComp-Analysis 1.0.0
  • the documentation of the HB branch needs to be updated
  • main problem is topology.v
  • shall we release 1.0.0 without the doc updated?
    • no
  • what to do for topology.v?
    • put the list of structures first
    • then put the notations
  • TODO:
    • Reynald will do a first pass (before the end of next week)
    • Takafumi will do a second pass (interested in documented filtered types)
  • hard deadline for the release: mid-January 2024
• release of MathComp-Analysis 0.6.7 before Christmas
• TODO: issue about the funny title (* The algebraic part of the algebraic hierarchy *)
  • see PR https://github.com/math-comp/math-comp/pull/1144
• PR by Takafumi https://github.com/math-comp/analysis/pull/1117
  • Zorn's variant:
    • localized version where the maximal element is taken over a given point
    • stated for relations in Prop
    • stronger than the original Zorn's lemma
    • no link with the Zorn lemma by Georges
      • the latter is a bit stronger because it is localized to subsets
      • only require a preorder and not a partial order
        • similar to the already present ZL_preorder in fact
    • Quentin has ported Georges' Zorn's lemma
    • there is also Zorn_bigcup
      • NB(rei): used in ex_maximal_disjoint_subcollection which is used in Vitali's lemma
  • maybe derive the Prop version from the bool version
    • but this require PR #1119 first...
  • Conclusion: issue postponed
• PR #1119 (adding a contraposition tactic)
  • quick demo by Quentin
  • Georges had a work about the implementation
  • Quentin has a couple of TOTHINK
    • do not use exfalso for consistency
    • 8.12 issue still need to be addressed
  • MCA is adequate because it is a tactic for a Prop irrelevant setting
    • it would require more work for a MathComp version
  • TODO: Quentin to complete the PR with the doc so that it can be reviewed lightly in January
• making classical a standalone library
  • idea by Yves for use in liberabaci among others
  • coq-mathcomp-classical is already a package
  • TODO: Takafumi to come up with ideas to improve the presentation of the webpage
  • recorded as issue https://github.com/math-comp/analysis/issues/1126
• documentation using coq2html:
  • here is a PR that does minimal changes https://github.com/math-comp/analysis/pull/1108
    • TODO: pierre to double-check
  • the result can be seen: https://yoshihiro503.github.io/coq2html/
  • still a few bugs but it does not use sed and allows for markdown
  • drop coqdoc for the next release?
    • yes
  • other issue related to documentation: https://github.com/math-comp/analysis/issues/1071
  • rename to rocq2html?
  • TODO(rei): contact Xavier
• PR triaging:
  • https://github.com/math-comp/analysis/pull/1029 (adapting) -> Pierre?
    • closed (problem forgotten, not needed anymore apparently since CI is happy)
  • https://github.com/math-comp/analysis/pull/1121 (lim sup)
    • TODO: review asked to Zachary
  • https://github.com/math-comp/analysis/pull/1083 (radon nikodym chain rule)
    • TODO: Quentin will take a quick look (keeping in mind that we have extra notations for HB on Coq 8.14 and 8.15 and that we might need a notation for ae_eq)
    • TODO: will also ask Zachary afterwards
  • https://github.com/math-comp/analysis/pull/1122 (easy fix but that raises the question of the status of forms.v)
    • try to remove mulr_rev in favor of R^C (put R^C in the canonical, cast one of the arguments to the converse ring)
    • Takafumi: is there a morphism defined from R to R^C?
      • Shouldn't be too hard
• Poll for the next meeting: https://framadate.org/XMI2ZG5hAIoNdhjD