-
Notifications
You must be signed in to change notification settings - Fork 111
Agenda of the October 25th 2018 meeting, 14h to 18h
affeldt-aist edited this page Oct 26, 2018
·
6 revisions
- frequency of the meetings, and next date (tentative proposal: 1 meeting per month)
- news from the libraries, current live projects, longer term ones : status, goals, merge plans,… E.g.: multivariate polynomials, ordered structures, real and complex analysis, ssreflect plugin, automation…
- API change policy (e.g. what exactly do we guarantee by increasing x, y or z, in a x.y.z version of mathcomp)
- current pull requests / bug reports
- Primitive projections
- if times allows: documentation/website/wiki/book/gallery
- Pierre-Yves Strub
- Assia Mahboubi
- Enrico Tassi
- Reynald Affeldt
- Georges Gonthier
- Cyril Cohen
- Emilio J. Gallego Arias
- Damien Rouhling
- Laurence Rideau
- Laurent Théry
- Maxime Dénès
- one meeting every two months
- virtual meeting during December https://framadate.org/oWQ9vLF1xbl74VcU
- face-to-face meeting in February https://framadate.org/k3esao1uTosdxIMO
- Cyril to framadate (see linkks above)
- first draft on bilinear/Hermitian forms, to be merged
- PR marked as a RFC
- port to Feit-Thompson in progress, replaces the ad-hoc part of characters
- main instance: dot product
- Georges: see extremal groups in
extremal.v
, conversation to be continued off-line
- want to have Gröbner bases in MathComp
- waiting for the work by Pierre-Yves on multinomials
- Pierre-Yves plans to merge by the end of the year
- Cyril observed that multinomials depens on finmap
- Debate (Cyril, Laurent, Assia):
- have subdirectories and let OPAM manage the dependencies?
- OPAM is too complicated
- users may want the multinomials with a simple
Require Import all_algebra
- tentative conclusion:
- put as much as possible in the main repository even though it may cause non-trivial updates of the code base
- distinguish “corrections” (improvement to be done right away)
and “generalizations/additions” (which can wait)
- difference may not be obvious
- as for finmap: by December in MathComp?
- TODO (Cyril): PR by the next meeting to discuss
- Plugin improvements:
- intro pattern that pop and generalize afterwards
- intro pattern of records (with naming determined by a user-given prefix/suffix and field names)
- notation to introduce the first hypothesis in the stack
- documentation within the PR
- TODO (Enrico): Demo for the next meeting, release should happen in June 2019
- Elpi not yet to be used in MathComp
- Cleaning of the code of the plugin planned
- next step: filtering (but should be transparent for the user)
- wip: library about triangulations
- uses finite functions to represent pointers, circular lists represented as an orbit of a function on a finite domain
- Georges soon to add a library with hypermaps and a similar feature
but relying on type changes
- both approached to be compared
- Georges: reappearance of a bug in Coq 8.8.1 that turns
.+1
intosuccn
by the pretty-printer (problem of priorities of notations)- not noticed by others
- Maxime observes that Coq 8.8.2 is only available with OPAM2
- Proof of the four color theorem to be released
- to clean “collective” (?) predicates
- currently relies on a workaround to help unification that is not necessary anymore, implemented in two different ways
- to be changed to better behave w.r.t. coercions
- origin of the problem: being into a list could not be defined as a coercion (uniform inheritance condition) and could not be patched, eta-conversion was done appropriately
- something has changed in the unification since 2008/2009
- Feature request (for Coq):
coq_makefile
to understand more flags, why-arg
is necessary in-arg -w
? (causes problems when loading with some versions of Proof General)
- working an infrastructure for a new standard library
- technically easy part done: new prelude so that the internals of
SSReflect tactics do not depend on the standard library
- Emilio observes that dependencies can be removed with a few hundred lines with almost no proof (but using standard tactics) (tested before SSReflect was merged into Coq)
- next is what to do with eqType? what will happen if we change
eqType with a type-class?
- Georges: do as Lean or stay as MathComp does
- MathComp exposes
==
in the structure - Lean uses a separate class for the decision procedure but boolean manipulations become difficult (boolean predicate found only in some cases)
- MathComp exposes
- Assia observes that Lean does not exploit much conversion except
at the leaves of proofs, to blur the difference between
Prop
andbool
- Maxime asking about using type-classes in MathComp?
- Georges: was tried with the hierarchy of algebraic predicates but was too unstable at the time (problem of uncontrolled divergences, but there was no mode at the time)
- Cyril mentions that Prolog-like cut are to be added but too experimental
- Georges:
- type-classes require to have types that expose all the components, causes complexity problems when we have complex hierarchies, could be mitigated by primitive projections
- only exposing keys and add inferred contents causes unification problems with non-tree hierarchies unless the user adds type constraints
- the simplest and the more robust is to use canonical structures
- however, selection of by-default values could be revised to use (inhabited) type classes; the problem is orthogonal to algebraic structures (in particular, not preserved by subtypes)
- Georges: do as Lean or stay as MathComp does
- presentation of mathcomp-analysis
- includes topological/uniform/normed spaces, Landau symbols, derivative/differential
- original intent was to make Coquelicot compatible with MathComp
- Georges observes that there are reals in the four color theorem
- experimentations with
near
tactics:-
near
tactics improve onbigenough
for epsilon-delta reasoning, could make their way to MathComp - Assia: nice to have tactics for that but seems not ready because difficult to use; some problems come from Coq (management of existentials) but there also might be interface problems, looks like hacks
- Cyril:
near
tactics are for backward chaining, efficient when there are several existentials- TODO: blackboard discussion
- TODO (Cyril): demo of
near
tactics for the next meeting
- Georges mentions a similar mechanism in SSReflect using
have
, observes that commands related to existentials in Coq are difficult to use (Maxime agrees) and that there is a need for a scope mechanism to avoid some leaks
-
- cleaning w.r.t. norm and absolute value in MathComp
- more theorems should be shared, need for a notion of order,
ssrnum
too rigid, to be generalized - PR in MathComp planned
- more theorems should be shared, need for a notion of order,
- quick overview of libraries under development
- information theory and error-correcting codes using MathComp
- using reals from the Coq standard library
- required a generalization of
arg_max
- TODO: discuss with Cyril about an existing, related PR
- provides discrete probabilities with finite domain
- relation with Pierre-Yves’ formalization of probabilities?
- mentions difficulties using finite fields and questioning
documentation, sent to
PrimeCharType
and usage in Feit-Thompson
- formalization of robot arm manipulators
- mostly 3D geometry
- uses
complex.v
fromreal_closed
to define angles- complex not in MathComp because there is no reals yet
- uses mathcomp-analysis for velocity
- monadic equational reasoning
- need to “rewrite under lambdas”
- relation with https://github.com/erikmd/ssr-under-tac?
- coloring issues for minted when used with SSReflect
- issue already mentioned by Florent Hivert
- information theory and error-correcting codes using MathComp
- cleaning the proof of irrationality of zeta(3)
- compiles with Coq 8.4, uses CoqEAL
- which parts are to go to MathComp? what depends on computing aspects?
- the approach of “equivalences for free” (a recently accepted paper) seems to lead to less code
- added the definition of multinomial coefficients that generalize binomial coefficients
- compiles with Coq 8.4, uses CoqEAL
- working on reals with Pierre-Yves
- one issue is how to go smoothly between
bool
andProp
in a classical setting
- one issue is how to go smoothly between
- formalization of Tate’s algorithm from elliptic curves
- one issue is the definition of the conductor
- how to define differentiable manifolds in Coq
- has a beginning of an answer in Lean
- proof of Abel–Ruffini theorem with Sophie and Pierre-Yves
- availability of CIFRE scholarship with Denis Cousineau
- smarter
Search
command? - Laurent observes that Coq’s hammer does not work with SSReflect
- smarter
- Marie to instantiate complex numbers with reals
- multinomials to be generalized
- to port reals
- cleaning the formalization of probabilities
- plan to work on integration for mathcomp-analysis with Cyril
-
PR 230
- Use
eq_irrelevance
instead ofbool_irrelevance
- Georges rather to keep
bool_irrelevance
but change the definition to match the name
- Use
-
PR 163
- linter in awk to format the code in a standard manner, not developed anymore
- to put on stand-by
- recommendations are written in CONTRIBUTING.md
-
PR 211
- rewriting with AC, following discussions with Kazuhiko
- consist in a lemma parameterized by an encoding of permutations
- input: a wanted ordering with parentheses
- reorganizes terms but does not solve equalities
- recognizes the
.[AC
symbol, usingMonoid.com_law
as an abstraction - Enrico thinks that it is a lot of Ltac (hacks?) and should maybe use OCaml
- TODO: try to use ML
- discussion on why using
cbv
, bug when when usingltac:
in aNotation
- TODO: in case of merge, see if it is useful in the library
- Georges mentions
bool_congr
andnat_congr
as candidates for improvements
- Georges mentions
- relation with issue 212?
-
PR 221
- discussion requires more preparation, Assia volunteered
-
PR 209
- contains a proof of QE monadic style and moves
countalg
toalgebra
- Georges:
-
finalg
does not inherit fromcountalg
because disjoint theories - historically
countalg
made to have the construction of algebraic numbers so it appears infield
- were in separate files because worked on by Cyril and Georges separately
- not against putting them together
-
- to be merged
- contains a proof of QE monadic style and moves
- TODO: PR 219
- TODO: merge PR 218
- work by Gaëtan Gilbert (sProp) on proof irrelevance
- impact on users: 2/3% when not used, 5% for fields
- Georges not suprised that it happens in such files
- MathComp does not use primitive projections
- Maxime mentions a recent (small-scale) experiment with Vincent that shows that it does not work