Agenda of November 27th 2019 meeting 10:00 to 11:30 - math-comp/math-comp GitHub Wiki

  • Discussion: PR #441, that is required to help future inclusion of finmap. It would be great that it is included in the release.

    • PR #441 has too many merges. It would be nice to forbid the use of "merging-by-default" that is forced by the github interface and advertise a better practice.

    • There are four lemmas in the family of big_image that have been moved to the section on abelian structures. The change is lightweight for math-comp, because big_image is actually not used there. Apart from this, porting most idioms to a new big_enumP lemma is described in the PR. Porting is kept easy, because index_enum_key is kept transparent.

  • Work on finmap will include changes to fintype.

    • finmap will need to be broken into three pieces.

      1. finmap proper for finite maps,
      2. finite sets should merge with the existing with the existing finset of math-comp
      3. the rest should probably go into fintype. The update of fintype will need that fintype contains the description of representation types for finset. And finset will just be a wrapper for it.

      still need some work to understand when a predicate has a finite range.

      The other issue is about pretty-printing. bigop is an example where canonical structures get exposed when rewriting and simplification to recover polished display. There is another way (also present in math-comp). When working with algebraic predicates, there is a key that is used to master display. Georges has been working on new approaches with phantom arguments to make display more visibility. using coercions to make canonical structures constructors invisible.

      Cyril is afraid about the interaction with parametricity translations.

    • filtered types are related to the ways to get enumerations for given predicate. As a result, cardinals will be equal, but it will be difficult to have convertibility (it will not hold). Some obviously finite predicates will not be understood as finite. For instance, "sum of cardinals is equal to sum cardinal of union and cardinal of intersection" will not transport easily to finite predicates over non-finite types. No canonical structures for lambdas, so when handling lambdas, there will be some trial and backtrack required.

      As a result of these experiments, some object that are visibly equal will not be recognized as convertible by Coq. Georges mention that part of the problem comes from the poor error messaging of Coq, and therefore the way to progress is to see how that can be solved ath the Coq level.

  • discussion about how to manage the developments that depend on mathcomp

    • assia would like time to catch up before the release of a version with the new finmap
    • multinomial
      • does not compile with the latest release
    • CoqEAL breaks
      • template polymorphism seems to be the culprit
      • the parametricity plugin (?) is broken with Coq 8.10.1
        • it is compiled with --no-template-check for the CI to go through
    • put CoqEAL in the CI?
    • ref: https://github.com/CoqEAL/CoqEAL/issues/23