Programming "quote" using canonical structures directives
Talk by Cyril Cohen my_stdcoq_quote.tgz
Pros:
- mix well with the general use of canonical structures in math.comp. libraries
- fine-tunable
Cons:
- introduce quite a lot of ad hoc CIC infrastructure (however, this infrastructure can probably be moved out of the actual proof if a bit of ltac is used so as to restrict the use of the CIC infrastructure to the unification algorithm)
More precise comparison with type-classes-based quote and with ML-written quote to be done.
About the work of Pierre-Yves Strub on the Calculus of Presburger Inductive Constructions
So as to provide extensional reasoning in Coq, the discussion concluded on the existence of the following possible approaches:
- Approach based on Nicolas Oury's work: CIC + Nicolas' axioms + use of eq_rect coercions + ad hoc support for hiding these coercions from the user (if ever possible).
- Minimal support for extensionality: allow any equation of the context whose proof is closed (up to free variables in inhabited types) to be used in the conversion.
- More realistic minimal extensionality: allow any instance of a universally quantified equation of the context whose proof is closed (up to free variables in inhabited types) to be used in the conversion (this requires pattern-matching). Note: following Pierre-Yves' result, equations with non-closed proofs can still be used in contexts with non-strong elimination. Questions: how to recognize usable equations; decidability issues.
- A variant of Pierre-Yves' approach: dynamic reflection of certified decision procedure in the kernel (restriction to contexts not using strong elimination if using equations with non closed proofs). An immediate question is: what criterion to use to combine different decision procedures?
- Pierre-Yves' current approach: static linking of extracted certified decision procedure for Presburger in the kernel (needs retroknowledge for the properties of the arithmetical symbols). An immediate question is: why to restrict to Presburger on nat and not to support other decision procedures? To which extent is the approach scalable?
Preparation of Coq 8.3
End of September: 8.3 branch created and new developments for 8.3 stop December: release of 8.3
Remark: switching to ocamlbuild is not realistic. Tested by Pierre and Stéphane, ocamlbuild is not mature enough yet (parallelization do not work, checking that nothing has to be done is exaggeratedly long).
Foreseeable contents of 8.3
Arnaud:
almost fully operational new tactic engine for which "tactic" is basically "subgoal list -> subgoal list" and dependent and non dependent evars live in the same space
- info and Show Script are at the time being discontinued, a few contribs are not compiling yet
Arnaud's archive is at http://git.spiwack.net/coq/.git; brave souls are invited to work with this archive; if ever they make non-proof-engine related modifications to it, they can cherry-pick the modifs to the trunk as if they had first worked in the trunk
- the decision of integrating the new proof engine to 8.3 is postponed
Hugo:
- grammar subentries
- intro-pattern extensions and cleaning, patterns in change
- minor improvements in the library (with Pierre)
Tom:
- "Cereal"/"external" under consideration
Julien Forest:
- nothing planned but can help on debugging or so
Bruno:
- finalization of Groebner with Loïc (and finding a name for it)
- a few bits with Ltac [exceptions, isolating components for easy reuse by ML tactics, ... ]
- a few bits with the checker
Matthieu: ?
Vincent Gross:
- Coqtop and Coqide living separately (?)
Other informations
Benjamin Grégoire:
- has a library of persistent arrays
Yann Régis-Gianas:
- lying unicode support on the standard table of unicode attributes (lowercase/uppercase distinction, symbol/ident distinction, etc)
Assia
- simplex method with Pierre-Yves
- [If I understood well] (modular) elimination of quantifiers (internship at the joint lab)
- application to Presburger (Cooper's algorithm)
- ongoing library of polynomials