2022 09 22 Meeting

Participants: Affeldt, Cohen, Roux, Stone

• port to HB #698

  • in topology.v:
    • find a way to port Definition product_topologicalType
      • does not seem to require any special technique, should be a standard approach, i.e., define a symbol product_... which is a Type that is endowed with a canonical structure, etc.
      • TODO: Reynald to investigate in October
    • non forgetful inheritance warning at line 3840
      • is it related to the fact that the uniform topology does not depend on the topology of the domain?
        • maybe no
      • actually, this should be an error
      • isSource was never intended to be a structure, it was a technical artifact
        • rule of thumb: ignore the warning and leave an issue?
      • TODO: Cyril to investigate
    • Section RestrictedUniformTopology.: might be connect to the non forgetful inheritance warning
    • uniform_limit_continuous and another one: ...
  • in normedtype.v: depends on product topology

• split packages classical #600 (this seems mostly ready, just waiting to happen)

  • should be top priority
  • we have added the split in nix and this should indeed be done first, the opam sync is easier
  • PR not yet reviewed
  • What do you do when the version is too low for the classical package to exist?
    • it becomes a dummy package that does nothing (trick borrowed from MathComp)
    • Cyril: would have wanted an error to be thrown. do not see where this is done in MathComp
      • https://github.com/NixOS/nixpkgs/blob/master/pkgs/development/coq-modules/mathcomp/default.nix#L112
      • it's a dummy package at the top not the bottom, it does introduce an extra dependency, it does not change the preexisting hierarchy
  • this PR is orthogonal to the one HB but it might have a big impact
  • TODO: merge what we have ASAP and try to improve later

• PRs:

  • https://github.com/math-comp/analysis/pull/747
    • easy one
    • NB: no unfold before an intro
  • https://github.com/math-comp/analysis/pull/748
    • more interesting
    • problem with R and \bar R: we want both theories for integral in R and in \bar R
    • go to Bochner integral and integral on R would be Bochner1?
    • using a different notation would also make sense
    • Rintegral is transitory and only exist because we do not have Bochner
      • notation in ring_scope following the pattern for `| ... |
    • Bochner needs a notion of dual space
      • definition via a canonical embedding into a dual space
      • we were waiting for HB to do that
  • https://github.com/math-comp/analysis/pull/737
    • report a curiousness about a need to a structure whereas the mixin only is needed
      • see isse #750
    • Cyril:
      • generalize [0,1] in IsPath
      • definition of path is not the right one
      • composition of paths is not associative
      • define path as a quotient up to remapping
    • use generic_quotient with same_path_component to define the equivalence relation
      • 1. reparametrization is an equivalence relation
      • 2. use that to build the canonical surjection
      • 3. define paths as point in the range of that space
    • TODO: redefine paths
      • Cyril: some proofs might shrink
  • https://github.com/math-comp/analysis/pull/674
    • uniform space respected uniform and weak topology
    • Cyril to review?
  • https://github.com/math-comp/analysis/pull/627
    • not worth merging now