Skip to content

2022 01 20 Meeting

Jump to bottom
affeldt-aist edited this page Jan 21, 2022 · 1 revision

Participants: Cyril, Kazuhiko, Pierre, Reynald, Takafumi, Yves, Zachary

  • Announcements:
    • from now, use Unshelve instead of Grab
      • Grab existential to be removed from Coq
    • support for Coq 8.11 and 8.12 dropped, support for Coq 8.15 added
      • the master of mathcomp-analysis is in the CI of Coq
      • we should be contacted by Coq people in case of problem
  • about documentation
    • we tentatively generated html document with math-comp tools (https://math-comp.github.io/analysis/htmldoc_0_3_12/)
      • TODO: add the library graph
    • as a first step towards cleaning, address old comments:
      • issue 503
        • equivalence theorem between the limit and the sup
        • TODO: rm
      • issue 515
      • issue 521
        • don't know.
        • TODO: restore it?
      • issue 522
        • TODO: rm
      • issue 523
        • don't know, can be removed as cvg_distP does the job
        • TODO: rm
      • PR 524
      • PS: one way to make commented code disappear it to use begin hide/end hide
        • but that should be exceptional (for wip for example)
    • files to better document?
      • add pointers to the standard library (which contains pointers to the litterature)
        • put in the doc the definition asbool
        • notations for forall, exists?
        • many things to be deleted because unused, inherited from previous work by assia and pierre-yves
        • TODO: cyril
    • Wiki entry about documentation format
    • Later we can try out alectryon (see PR 458)
    • yves: add a word about documenting the notations in the wiki entry
  • PRs in progress:
    • PR 505 (fix boundary conditions) (issue 408)
      • zachary introduced an ad hoc notation that is a temporary solution
      • zachary now fixing IVT and MVT applications, crushing merge conflicts (realfun.v requires fixes)
    • improvements:
      • PR 511 (posnum)
        • generalize posnum and nonneg, not tied to ring
        • needs to be documented
        • pierre to extend for extended reals as a subsequent PR
        • help wanted for the documentation
        • TODO: pierre
      • PR 492 (functions and cardinality)
        • quick tour by cyril
        • takafumi: use of a cardinal type?
          • cyril: could be simpler than card_eq_sym, card_eq_trans, etc.
        • continuous, bijective functions should also be part of this hierarchy
        • TODO: reynald to review and document (put TODOs for cyril for unclear parts)
    • PR 487 (replacing strict inequalities)
      • everything should boil down to a hint as here
      • the user proofs should not be impacted by the change of definitions thanks to hints
      • TODO: cyril to review
  • PRs to merge:
    • merge PR 474? (Hausdorff product)
      • squash and merge
    • about ereal.v:
      • merge PR 514?
        • mule_def_neq0_infty: ordering justified if we look at the hypos like arguments (as in type classes)
      • merge 508?
        • mule_eq_pinfty: underscore because of long suffix
        • TODO: reynald fix
    • merge PR 517? (unicode symbols for company-coq)
      • merge
    • merge PR 489? (sup with supremums)
      • though the cleaning of the theory of sup/inf and ereal_sup/ereal_inf is not completed, can we merge and issue to reboot later, since it is already an improvement?
      • we want to test more the theory
      • maybe the supremum should be defined only when there is a top element
      • what is the closest thing we can have before HB is ready?
      • TODO: schedule a more in-depth discussion for the next days
  • news from Lebesgue integration (dominated convergence, Fubini's theorem, etc.)
    • saikawa: relation between Riemann and Lebesgue?
    • about functions with finite image
Clone this wiki locally