Skip to content

2023 04 20 Meeting

Jump to bottom
Pierre Roux edited this page Apr 21, 2023 · 5 revisions

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

  • Check TODOs from the last meeting (https://github.com/math-comp/analysis/wiki/2023-02-06-Meeting)
  • follow-up of the conversation about probability.v PR 516:
    • should we put counter-examples in a Module, in a special file, have a naming scheme for them?
    • "If A is a non-measurable subset of T, then f = X_B - X_(~B) (the characteristics functions) is non measurable. But it only takes values of 1 or -1. So f^2 is constant, therefore measurable."
    • use the Example of the vernacular
      • could pollute the Search outputs but so will Modules
        • not sure about this one
      • see CEP 42
    • name them "counter_example_blah"
      • (so that we can use blacklisting if necessary)
    • some counter-examples might be result of HB.instance
    • or put everything in a separate file that is not required
    • NB: the Lebesgue measure could by in a separated file but not required
    • TODO: document in CONTRIBUTING.md
    • what about the Modules "Test" in itv.v?
      • put them in a test suite?
      • put them in a example file?
      • e.g., example/example_itv.v
  • discussion about the scope discipline and order displays, particularly with extended reals (c.f., the discussion in math-comp/980)
    • ring_scope and ereal_scope used in combination in ereal.v
    • solution to avoid the %E and %R?
    • open the order_scope is a bad idea
    • cyril:
      • %E and %R serve as a documentation
      • there is a coercion from nat_to_int, there is disambiguation for comparison but not for ==
      • in wait of a feature of Coq with which we can use the annotation only to disambiguate
      • we would also need in Coq a way to enable/disable printing of the coercions in the middle of a proof (Pierre afterwards: seems like Add / Remove Printing Coercion qualid already allows that)
    • Pierre: we have an explicit coercion %:E
      • since we switch from Reals to realType
      • if we get the implicit coercion in the future, we'll need the disambiguation
    • conclusion: don't do anything to remain ready for future coercions
  • public announcement: regarding compatibility, from now on we should
    • target PRs on master when possible and, once merged, cherry-pick on hierarchy-builder
    • target other PRs on hierarchy-builder
  • release of algebra tactics
    • should we use lra agressively?
    • for the time being, use it only where it reduces substantially the size of the proof
    • TODO: test with {i01 R}, rewrite signed.v and itv.v
      • infer canonically the membership by deferring the witness to lra (to handle more complicated inequations)
  • Modules vs Factories. I can't tell whether we generally want to encode properties into HB mixins or Modules. Things like "Hausdorff", "continuous", "convex", that refine structures rather than add new ones, in particular. For an example of a module, see the countable uniformity stuff. Could this be a factory? I would love to have some guidance on this. See PR 885 for an example.
    • e.g., countable uniformity in the HB branch it is built as a Module, but can it be a factory?
    • "as a Module" -> Zachary is actually referring to aliases / feather factories
    • a factory is supposed to be alternative interfaces
      • the fields of a factory should be axioms of the theory
      • like an alternative definition
    • about countable uniformity?
      • use an existential to clarify that the witness is not determined
    • Pierre: factories could have been mixins if the hierarchy is organized in another way
    • waiting for a feature of HB that checks that all the axioms of a theory can be deduced
    • each factory should correspond to a single structure
    • TODO(Cyril): to document the difference between alias and factories during the forthcoming MathComp documentation sprint
      maybe there: https://github.com/math-comp/hierarchy-builder/wiki/FeatherFactory
  • close the following PRs?:
  • merge 833 after all?
    • we should prove them
    • it should be ok to "undeprecate" them
    • __deprecated -> __admitted
    • "lacks proof" -> "use __admitted... if you really want to use them"
    • TODO(rei)
  • question about type classes and canonical structures the apply of type classes if not powerful enough use Hint Extern to solve the problem with apply: TODO(rei ?): Hint Extern with the pattern (grep the code), put the Hint in the typeclass_instances database
  • check the milestone so that we can release 0.6.2
  • Takafumi: do we have differentiability in thethe multivariable case?
    • we handle matrices but that wouldn't be textbook for the case of two variables
    • use row vectors for inputs but induction will be tedious
    • TODO: try, state Stokes' theorem
  • about Hahn decomposition theorem
    • generalization with FinNum
    • fine acts like homeomorphisms and it might be better that the theorem lift from \bar R to R
  • the PR on convexity has been merged
    • conversation partly recorded as issue 904
    • TODO: in the future, define differentiability to the left/right and/or "within derivable"
  • usage report about itv.v:
    • see this commit for an error message
    • TODO: Pierre to have a look
  • About Urysohn's Lemma PR 900
    • the PR is missing the final statement because it lacks something that will come easily with HB
    • that's an original proof (no textbook)
    • crucial use of
      • finite intersection for filters
      • countable uniformity implies pseudometric (T is uniform and there is a countable basis for its entourage then T is a pseudo-metric space)
    • TODO: Reynald to lint
Clone this wiki locally