-
Notifications
You must be signed in to change notification settings - Fork 43
2021 07 22 Meeting
affeldt-aist edited this page Jul 22, 2021
·
1 revision
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 inmeasure_wip.v
in https://github.com/math-comp/analysis/pull/371?
- using
- Yves to issue about a problem using interior of intervals
- would prefer to have the definition of
- 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
- using closed intervals as in
- 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