2018 11 08 Meeting

Initial Agenda

• état des lieux
• projets de chacun, et but à long terme (e.g. sommabilité, théorie de la mesure/intégration, EDO/EDP, refactorisation(s) de code, modèle des réels, epsilon -> iota)
• traitement de PR et issues en cours
• fréquence de réunion, et la prochaine date (proposition de Cyril : une fois tous les deux mois en virtuel, et profiter de réunions mathcomp dev IRL pour ceux qui le peuvent, pour se voir juste avant ou juste après)
• rédaction d'articles

Participants

• Reynald Affeldt
• Cyril Cohen
• Assia Mahboubi
• Laurence Rideau
• Damien Rouhling

Summary

Next meetings

• Cyril opened a poll for a meeting in December

• Another meeting will probably take place in February, together with the math-comp meeting

Communication

Mailing list

• Goals: synchronise, make it possible for others to contact the developers

• Administrators: currently only Cyril, add Reynald and Assia? [DONE: Reynald is now also an admin]

• Invite Marie Kerjean. [DONE]

Contacts with developers of other libraries

• Sylvie Boldo and Guillaume Melquiond (Coquelicot) are aware that the library exists. We discussed with them (more with Guillaume). Guillaume would contribute if we change the axioms we use (see Axioms).

• Some Lean users are aware of the library

How to communicate

• Assia: do not reproduce math-comp's mistakes, i.e. write papers but also make them understandable by non-specialists, communicate in a clear way.

  Examples of issues (also for us):

  • Reynald's way of learning math-comp is by playing with it and discussing with developers to get clarifications on the (few) papers
  • The near + Landau paper is not clear enough: too many things kept implicit, we rely on reflexes we obtained trough experience
  • The discussion with Lean users about the chain rule did not help them to understand the differences with their work

  A possible solution: send the papers to non-specialists to get feedback before submission

• Conference papers can be better to advertise, but advertisement can come from applications of the library and journal papers give us more space

• Short term goal: write a paper on the general principles to design a library.

  • Ideal impact of this paper: make Lean people understand how to reproduce our work, give ideas to Coq developers for the new standard library
  • Cyril will open a repository with a brainstorming file [Done]
  • We will discuss this article in February but we should think about it before

Development

Ultimate goal

• Formalize mathematics as if we were doing proofs on paper

Two conflicting aspects in the development

• Cyril: go far enough with strong axioms and then try to use weaker axioms while keeping the ease of use

  This is a bit early to change the axioms because integrals and series are missing

• Assia: understand how each axiom contributes to the library, understand what classical analysis really means

• Pierre-Yves and Assia did a lot of work to figure out the right foundations but this is missing from the current library: we made this hard to integrate

  Laurence's warning: do not consider a Coquelicot à la mathcomp sufficient, foundations should be well thought

Axioms

• Guillaume Melquiond would like axioms that are compatible with HOTT

  Consequences: iota replaces epsilon and P \/ ~ P replaces {P} + {~P}

• Cyril: this change is costly, and we might miss the comfort brought by epsilon and {P} + {~P}

• Assia: not the priority yet, we should first clean up and understand the role of the axioms we use

  Moreover there is no proof assistant for HOTT and we don't know what such a proof assistant would be. Should we add complications for something we can only speculate about?

• Other systems have strong axioms and do not bother with HoTT

Differences with other systems

• Our greatest advantage: math-comp, i.e. a well-furnished library for algebra with adapted structures

• Isabelle people are ahead because they have less concerns with foundations

• Lean people are fast, but they lack the algebra library of mathcomp

• Computation is also an advantage of Coq, although it might be different if Lean 4 keeps its promises

• The best topic to avoid collisions with other systems and to benefit from our advantages is the frontier between algebra and analysis

Current and future projects

Cyril

• Simplify the filter infrastructure: we have both type classes and canonical structures, we should switch to only canonical structures (type class inference is often broken and too hard to debug)

  Assia: keep a branch with type classes to feed a discussion on inference mechanisms (for our next paper for instance)

  Other issue: default filters break unification in a complex way

• In math-comp: separate the norm and the absolute value in the hierarchy

• Long-term goal: reimplement near in ml

Damien

• Replace balls with entourages in the definition of uniform spaces

• Get rid of the dependency of the standard library's R, this also means merging Rbar and ereal.

  Assia: having extended positive real numbers would be interesting (for summability) but it is hard

• Rework the max with bigop and merge parts of this in math-comp

Pierre-Yves Strub

• A model of real numbers: Eudoxus reals
• Port to filters and complete the theory about summability
• Complete & finish the theory about discrete distributios

Assia

• Clean up of foundations: axioms, reorganise boolp, have notations for asbool, clean up the proof of Zorn's Lemma

Marie Kerjean (according to Assia)

• New to Coq so we should be kind and give appropriate feedback

• Start with a PR about a construction of complex numbers

  Assia: what related works should we look at?

  Answer: real-closed, coq-robot, spectral

• Longer-term goal: theory of D-finite functions

Reynald

• Link the mathematical jacobian with the notion of jacobian used in robotics

• Explore the compatibility between coq-robot and analysis for elementary functions

  Assia: elementary functions will benefit from the theory of D-finite functions

• Work on infotheo: discrete distributions, conditional independence of random variables

  Todo: synchronise with Pierre-Yves Strub

  Issue: to be compatible with analysis, it needs elementary functions