coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Hugo Herbelin <herbelin AT pauillac.inria.fr>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club]Final release of Coq V8.1
- Date: Wed, 14 Feb 2007 20:33:57 +0100 (MET)
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Coq version 8.1 is finally out. It fixes many bugs of Coq version
8.1gamma and can be considered "stable". Compared to 8.1gamma, the
ring and field tactics have also been extended to deal with the power
function and to rewrite monomials on the fly (see documentation).
Compared to Coq 8.0, the main changes are the following:
- efficient evaluation
- new auxiliary algorithm for checking the convertibility of types,
specially dedicated to fast type-checking of reflexion-based proofs,
and more generally to intensive computation (by B. Grégoire)
- inductive types
- support for recursively non uniform parameters (by C. Paulin)
- support for some form of sort-polymorphism that leads to merge
prod and prodT, list and listT, etc. (by H. Herbelin)
- improved/extended tactics
- new implementation of setoid rewrite (by C. Sacerdoti Coen)
- improved implementation of simplification in rings (by B. Grégoire,
A. Mahboubi and B. Barras)
- improved implementation of simplification in fields (by L. Théry
and B. Barras)
- many other new tactic features (see attached file CHANGES)
- libraries
- finite sets and finite maps (by J.-C. Filliâtre and P. Letouzey)
- strings (by L. Théry)
- extensions of the library on lists (by P. Letouzey and J.-M. Notin)
- rational numbers (by P. Letouzey) [rational are defined as a quotient
over Z/Z+* -- an alternative library based on the canonical Stern-Brocot
representation is available in the user contributions]
- a few other evolutions (see attached file CHANGES)
- experimental features
- new command Function to generate fixpoints with arbitrary well-
foundedness termination evidence and associated "functional"
induction scheme, fixpoint equation, and support for inversion
(by P. Courtieu and J. Forest and by Y. Bertot)
- new command to generate proof obligations from definitions of
programs required to meet their specification (see chapter 19 in
the reference manual) (by M. Sozeau)
- mechanism to communicate with external tool, such as computer
algebra systems or theorem provers able to generate proofs (see the
end of chapter 9 in the reference manual)
- new declarative mathematical proof language (by P. Corbineau)
See the attached CHANGES file for the full list of new features.
The main sources of incompatibilities of Coq version 8.1 come from the
new implementations of the tactics setoid_rewrite, ring and field.
See http://coq.inria.fr/COMPATIBILITY for details and smooth migration
recommendations.
The documentation is available from http://coq.inria.fr.
Coq version 8.1 is based on the new Coq version 8.0 syntax. Users
migrating from Coq version 7.x and older must first translate their
developments from the old syntax using the translator provided with
Coq version 8.0.
For the list of known bugs or to submit a new one, see page Contacts
at http://coq.inria.fr. General questions or remarks can be sent to
Coq-Club AT pauillac.inria.fr.
See also http://coq.inria.fr.
The main changes in the Objective Caml interfaces of Coq are
documented in the file dev/doc/changes.txt of Coq source archive.
Here follows a list of user contributions submitted in the past two
years (see the Coq web site for download):
- CoLoR: a library on rewriting and termination (F. Blanqui, S. Hinderer,
S. Coupet-Grimal, W. Delobel, A. Koprowski)
- Library for persistent union-find (J.-C. Filliâtre)
- Micromega: reflexive tactics for Presburger arithmetic and more (F. Besson)
- Up-to techniques for weak bisimulation (D. Pous)
- Higher-order syntax from modules over monads (A. Hirschowitz, M. Maggesi)
- Bisimulation for the spi-calculus (S. Briais)
- Modelization of random programs (C. Paulin)
- An approach of proof by reflexion for first-order logic (P. Corbineau)
- Another approach of proof by reflexion for first-order logic (D. Hendriks)
- Intuitionistic propositional checker (K. Weich)
- Chou-Gao-Zhang area method for deciding affine geometry (J. Narboux)
- Proof of the Fairisle 4x4 Switch Element (S. Coupet-Grimal, L. Jakubiec)
- Kildall's data-flow analysis (S. Coupet-Grimal, W. Delobel)
- Diophantus' 20th Problem and Fermat's last theorem for n=4 (D. Delahaye,
M. Mayero)
- Karatsuba multiplication on binary numbers (R. O'Connor)
- Case study on square matrices (J.-C. Filliâtre)
- Divide-and-conquer for binary tree diameter computation (J.-C. Filliâtre)
- Certified Sudoku solver (L. Théry)
- Ordinals (Cantor, Veblen), hydra battle, Goodstein sequences (P. Castéran,
E. Contejean)
- The Godel-Rosser 1st incompleteness theorem (R. O'Connor)
- Embedding intuitionistic ZF set theory in Coq + intuit. choice (A. Miquel)
- Category theory in set theory (C. Simpson)
- Tait-style normalizability for simply-typed lambda-calculus (P. Letouzey,
H. Schwichtenberg)
The Coq development team
Changes from V8.1gamma to V8.1
==============================
Bug fixes
- Many bugs have been fixed (cf coq-bugs web page)
Tactics
- New tactic ring, ring_simplify and new tactic field now able to manage
power to a positive integer constant. Tactic ring on Z and R, and
field on R manage power (may lead to incompatibilities with V8.1gamma).
- Tactic field_simplify now applicable in hypotheses.
- New field_simplify_eq for simplifying field equations into ring equations.
- Tactics ring, ring_simplify, field, field_simplify and field_simplify_eq
all able to apply user-given equations to rewrite monoms on the fly
(see documentation).
Libraries
- New file ConstructiveEpsilon.v defining an epsilon operator and
proving the axiom of choice constructively for a countable domain
and a decidable predicate.
Changes from V8.1beta to V8.1gamma
==================================
Syntax
- changed parsing precedence of let/in and fun constructions of Ltac:
let x := t in e1; e2 is now parsed as let x := t in (e1;e2).
Language and commands
- Added sort-polymorphism for definitions in Type.
- Support for implicit arguments in the types of parameters in
(co-)fixpoints and (co-)inductive declarations.
- Improved type inference: use as much of possible general information.
before applying irreversible unification heuristics (allow e.g. to
infer the predicate in "(exist _ 0 (refl_equal 0) : {n:nat | n=0 })").
- Support for Miller-Pfenning's patterns unification in type synthesis
(e.g. can infer P such that P x y = phi(x,y)).
- Support for "where" clause in cofixpoint definitions.
- New option "Set Printing Universes" for making Type levels explicit.
Tactics
- Improved implementation of the ring and field tactics. For compatibility
reasons, the previous tactics are renamed as legacy ring and legacy field,
but should be considered as deprecated.
- New declarative mathematical proof language.
- Support for argument lists of arbitrary length in Tactic Notation.
- [rewrite ... in H] now fails if [H] is used either in an hypothesis
or in the goal.
- The semantics of [rewrite ... in *] has been slightly modified (see doc).
- Support for "as" clause in tactic injection.
- New forward-reasoning tactic "apply in".
- Ltac fresh operator now builds names from a concatenation of its arguments.
- New ltac tactic "remember" to abstract over a subterm and keep an equality
- Support for Miller-Pfenning's patterns unification in apply/rewrite/...
(may lead to few incompatibilities - generally now useless tactic calls).
Bug fixes
- Fix for notations involving basic "match" expressions.
- Numerous other bugs solved (a few fixes may lead to incompatibilities).
Changes from V8.0 to V8.1beta
=============================
Logic
- Added sort-polymorphism on inductive families
- Allowance for recursively non uniform parameters in inductive types
Syntax
- No more support for version 7 syntax and for translation to version 8
syntax.
- In fixpoints, the { struct ... } annotation is not mandatory any more when
only one of the arguments has an inductive type
- Added disjunctive patterns in match-with patterns
- Support for primitive interpretation of string literals
- Extended support for Unicode ranges
Vernacular commands
- Added "Print Ltac qualid" to print a user defined tactic.
- Added "Print Rewrite HintDb" to print the content of a DB used by
autorewrite.
- Added "Print Canonical Projections".
- Added "Example" as synonym of "Definition".
- Added "Proposition" and "Corollary" as extra synonyms of "Lemma".
- New command "Whelp" to send requests to the Helm database of proofs
formalized in the Calculus of Inductive Constructions.
- Command "functional induction" has been re-implemented from the new
"Function" command.
Ltac and tactic syntactic extensions
- New primitive "external" for communication with tool external to Coq.
- New semantics for "match t with": if a clause returns a
tactic, it is now applied to the current goal. If it fails, the next
clause or next matching subterm is tried (i.e. it behaves as "match
goal with" does). The keyword "lazymatch" can be used to delay the
evaluation of tactics occurring in matching clauses.
- Hint base names can be parametric in auto and trivial.
- Occurrence values can be parametric in unfold, pattern, etc.
- Added entry constr_may_eval for tactic extensions.
- Low-priority term printer made available in ML-written tactic extensions.
- "Tactic Notation" extended to allow notations of tacticals.
Tactics
- New implementation and generalization of [setoid_]* (setoid_rewrite,
setoid_symmetry, setoid_transitivity, setoid_reflexivity and autorewite).
New syntax for declaring relations and morphisms (old syntax still working
with minor modifications, but deprecated).
- New implementation (still experimental) of the ring tactic with a built-in
notion of coefficients and a better usage of setoids.
- New conversion tactic "vm_compute": evaluates the goal (or an hypothesis)
with a call-by-value strategy, using the compiled version of terms.
- When rewriting H where H is not directly a Coq equality, search first H for
a registered setoid equality before starting to reduce in H. This is
unlikely
to break any script. Should this happen nonetheless, one can insert
manually
some "unfold ... in H" before rewriting.
- Fixed various bugs about (setoid) rewrite ... in ... (in particular #1101)
- "rewrite ... in" now accepts a clause as place where to rewrite instead of
juste a simple hypothesis name. For instance:
rewrite H in H1,H2 |- * means rewrite H in H1; rewrite H in H2; rewrite H
rewrite H in * |- will do try rewrite H in Hi for all hypothesis Hi <> H.
- Added "dependent rewrite term" and "dependent rewrite term in hyp" (doc
TODO)
- Added "autorewrite with ... in hyp [using ...]".
- Tactic "replace" now accepts a "by" tactic clause.
- Added "clear - id" to clear all hypotheses except the ones depending in id.
- The argument of Declare Left Step and Declare Right Step is now a term
(it used to be a reference).
- Omega now handles arbitrary precision integers.
- Several bug fixes in Reflexive Omega (romega).
- Idtac can now be left implicit in a [...|...] construct: for instance,
[ foo | | bar ] stands for [ foo | idtac | bar ].
- Fixed a "fold" bug (non critical but possible source of incompatibilities).
- Added classical_left and classical_right which transforms |- A \/ B into
~B |- A and ~A |- B respectively.
- Added command "Declare Implicit Tactic" to set up a default tactic to be
used to solve unresolved subterms of term arguments of tactics.
- Better support for coercions to Sortclass in tactics expecting type
arguments.
- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses.
- New tactic "pose proof" that generalizes "assert (id:=p)" with intro
patterns.
- New introduction pattern "?" for letting Coq choose a name.
- Added "eassumption".
- Added option 'using lemmas' to auto, trivial and eauto.
- Tactic "congruence" is now complete for its intended scope (ground
equalities and inequalities with constructors). Furthermore, it
tries to equates goal and hypotheses.
- New tactic "rtauto" solves pure propositional logic and gives a
reflective version of the available proof.
- Numbering of "pattern", "unfold", "simpl", ... occurrences in "match
with" made consistent with the printing of the return clause after
the term to match in the "match-with" construct (use "Set Printing All"
to see hidden occurrences).
- Generalization of induction "induction x1...xn using scheme" where
scheme is an induction principle with complex predicates (like the
ones generated by function induction).
- Some small Ltac tactics has been added to the standard library
(file Tactics.v):
* f_equal : instead of using the different f_equalX lemmas
* case_eq : a "case" without loss of information. An equality
stating the current situation is generated in every sub-cases.
* swap : for a negated goal ~B and a negated hypothesis H:~A,
swap H asks you to prove A from hypothesis B
* revert : revert H is generalize H; clear H.
Extraction
- All type parts should now disappear instead of sometimes producing _
(for instance in Map.empty).
- Haskell extraction: types of functions are now printed, better
unsafeCoerce mechanism, both for hugs and ghc.
- Scheme extraction improved, see http://www.pps.jussieu.fr/~letouzey/scheme.
- Many bug fixes.
Modules
- Added "Locate Module qualid" to get the full path of a module.
- Module/Declare Module syntax made more uniform.
- Added syntactic sugar "Declare Module Export/Import" and
"Module Export/Import".
- Added syntactic sugar "Module M(Export/Import X Y: T)" and
"Module Type M(Export/Import X Y: T)"
(only for interactive definitions)
- Construct "with" generalized to module paths:
T with (Definition|Module) M1.M2....Mn.l := l' (doc TODO).
Notations
- Option "format" aware of recursive notations.
- Added insertion of spaces by default in recursive notations w/o separators.
- No more automatic printing box in case of user-provided printing "format".
- New notation "exists! x:A, P" for unique existence.
- Notations for specific numerals now compatible with generic notations of
numerals (e.g. "1" can be used to denote the unit of a group without
hiding 1%nat)
Libraries
- New library on String and Ascii characters (contributed by L. Thery).
- New library FSets+FMaps of finite sets and maps.
- New library QArith on rational numbers.
- Small extension of Zmin.V, new Zmax.v, new Zminmax.v.
- Reworking and extension of the files on classical logic and
description principles (possible incompatibilities)
- Few other improvements in ZArith potentially exceptionally breaking the
compatibility (useless hypothesys of Zgt_square_simpl and
Zlt_square_simpl removed; fixed names mentioning letter O instead of
digit 0; weaken premises in Z_lt_induction).
- Restructuration of Eqdep_dec.v and Eqdep.v: more lemmas in Type.
- Znumtheory now contains a gcd function that can compute within Coq.
- More lemmas stated on Type in Wf.v, removal of redundant Fix_F.
- Change of the internal names of lemmas in OmegaLemmas.
- Acc in Wf.v and clos_refl_trans in Relation_Operators.v now rely on
the allowance for recursively non uniform parameters (possible
source of incompatibilities: explicit pattern-matching on these
types may require to remove the occurrence associated to their
recursively non uniform parameter).
- Coq.List.In_dec has been set transparent (this may exceptionally break
proof scripts, set it locally opaque for compatibility).
- More on permutations of lists in List.v and Permutation.v.
- List.v has been much expanded.
- New file SetoidList.v now contains results about lists seen with
respect to a setoid equality.
- Library NArith has been expanded, mostly with results coming from
Intmap (for instance a bitwise xor), plus also a bridge between N and
Bitvector.
- Intmap has been reorganized. In particular its address type "addr" is
now N. User contributions known to use Intmap have been adapted
accordingly. If you're using this library please contact us.
A wrapper FMapIntMap now presents Intmap as a particular implementation
of FMaps. New developments are strongly encouraged to use either this
wrapper or any other implementations of FMap instead of using directly
this obsolete Intmap.
Tools
- New semantics for coqtop options ("-batch" expects option "-top dir"
for loading vernac file that contains definitions).
- Tool coq_makefile now removes custom targets that are file names in
"make clean"
- New environment variable COQREMOTEBROWSER to set the command invoked
to start the remote browser both in Coq and coqide. Standard syntax:
"%s" is the placeholder for the URL.
- [Coq-Club]Final release of Coq V8.1, Hugo Herbelin
Archive powered by MhonArc 2.6.16.