Agenda of the October 25th 2018 meeting, 14h to 18h - math-comp/math-comp GitHub Wiki
Proposed topics
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
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
Enrico
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)
Yves
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 into
succn 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
Georges
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)
Maxime
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)
Assia observes that Lean does not exploit much conversion except
at the leaves of proofs, to blur the difference between Prop
and bool
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)
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
Cyril
experimentations with near tactics:
near tactics improve on bigenough 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
Reynald
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 from real_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
Assia
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
working on reals with Pierre-Yves
one issue is how to go smoothly between bool and Prop in a
classical setting
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
Marie to instantiate complex numbers with reals
Pierre-Yves
multinomials to be generalized
to port reals
cleaning the formalization of probabilities
plan to work on integration for mathcomp-analysis with Cyril