2020 12 17 Meeting - math-comp/analysis GitHub Wiki

Participants: Marie, Kazuhiko, Pierre-Yves, Cyril, Reynald

• PR 283
  • still need to split lemmas in two
  • add lemmas "interior of ball is open" and "interior of closed ball is ball"?
  • for the time being, do not add any open_ball definition to normedtype.v
    • maybe later if needed
  • should be done by next month
• TODO: put in the documentation
  • NB: balls from pseudometric types are not necessarily open
• PR 305
  • close but don't remove: keep as documentation
• PR 275
  • TODO: add changelog entries
    • drop support for versions before MathComp 1.12
  • TODO: release mathcomp-analysis 0.3.5 once merged
• NB: hierarchy-builder requires Coq 8.11
• TODO: issue to add test with Coq 8.13
• summary of the new interval library
  • bounds are now +oo and -oo, "left of x" and "right of x" (meaning open or closed depending on which extremity we are)
• NB: another order of intervals: by their middle point (x+1/x-1 for half-open intervals)
• PR 294
  • no major issue, should be done by next month
• PR 309
  • predeqP should be should be like predeqE but with <=> instead of =
  • what is predeqP right now should be called seteqP
• PR 205
  • could be merged by next month
  • ^o only used on intermediate structures (as in https://github.com/math-comp/analysis/blob/b3a67378443dc35cd788b02dc384a5f3a4949935/theories/normedtype.v#L1258)
    • topological structure defined on any numField as a clone of the regular structure on algebra
  • NB: remaining ^o in sequences.v
  • NB: derive.v still slow to compile, this is because of type classes
    • part of the solution could be to lock the definition mentioned in issue 118 with a module
• PR 302 New nix
  • refactoring of nix files for analysis to work with the future version of Coq packages that is under refactoring (see this PR)
  • using MathComp-Analysis as a benchmark
• PR 306 Generated nix CI test
  • generated using PR 302
  • to be put in draft mode but should be merged as some point
• meta discussion about simplification of filters
  • this ultimately calls for an extension of hierarchy-builder
  • alternative approach (besides the existing PRs): duplicate the hiearchy of algebraic predicates https://github.com/math-comp/math-comp/blob/master/mathcomp/algebra/ssralg.v#L3526-L3752
  • TODO: try...