2021 07 22 Meeting

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

• Yves working on generalizing lemmas on https://github.com/math-comp/analysis/pull/385 from closed intervals to arbitrary intervals
  • would prefer to have the definition of is_interval to be with large inequalities
    • TODO: produce a PR with the large inequalities
    • NB: besides master, also used in https://github.com/math-comp/analysis/pull/371
  • TODO: insert in mathcomp the bound_in_itv multi-rule from PR https://github.com/math-comp/analysis/pull/385
    • because existing rules force people to see the datatype of interval bounds
  • TODO: merge https://github.com/math-comp/analysis/pull/385 asap and makes issues
    • after naming and dispatching lemmas in existing files?
    • some contents to end in a new real_fun.v file anticipating on trigonometry?
  • how to write the image of an interval?
    • using set_of_itv and @` as in measure_wip.v in https://github.com/math-comp/analysis/pull/371?
  • Yves to issue about a problem using interior of intervals
• About Cstruct:
  • Goal: Reasoning about numerical computations on matrices, eigenvalues and Jordan normal forms
  • Rstruct is here for historical reasons and because it provides a model
  • wouldn't encourage Cstruct because there is already an implementation of complex numbers in MathComp
  • material about the geometric series already in mathcomp-analysis but for real numbers
  • yet no easy bridge right now between real and complex numbers and their norm
• About https://github.com/math-comp/analysis/pull/403:
  • Pierre to take a look
• About https://github.com/math-comp/analysis/pull/180:
  • TODO: merge asap
• About issue https://github.com/math-comp/analysis/issues/408:
  • using closed intervals as in {in [a, b], continuous f} is too strong
  • solution using within
  • Cyril to PR a solution about this issue
• PR https://github.com/math-comp/analysis/pull/311: Cyril is refactoring
• About PR https://github.com/math-comp/analysis/pull/375
  • could be merged but Cyril has a better solution
  • to cover extended real numbers and real types
  • let's merge it for the time being
• about PR https://github.com/math-comp/analysis/pull/374/:
  • maybe extract the lemmas about extended real numbers
  • rebase after https://github.com/math-comp/analysis/pull/403 is merged
• About https://github.com/math-comp/analysis/pull/398:
  • nsatz uses type classes, we do not have that for lra
  • PR something to Coq about lra such as what Kazuhiko is doing with lia?
    • pbm: real numbers are hard-wired in lra
  • Kazuhiko: general interface for realFieldType to prove Farkas' lemma in a general form looks like a lot of work