Changes from V8.0 ================= Environment variables - 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 (doc TODO) Vernacular commands - Added "Print Ltac qualid" to print a user defined tactic (doc TODO) - Added "Print Rewrite HintDb" to print the content of a DB used by autorewrite (doc TODO) - Added "Print Canonical Projections" (doc TODO) Gallina - Added disjunctive patterns in match-with patterns Ltac - New primitive "external" for communication with tool external to Coq - Semantics of "match t with" changed: 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"). - New modifier "lazy" (TODO) for "match t with" and "match goal with" telling to delay the evaluation of tactic expression. 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) (doc TODO) - Added "clear - id" to clear all hypotheses except the ones depending in id. - Added "dependent rewrite term" and "dependent rewrite term in hyp" (doc TODO) - The argument of Declare Left Step and Declare Right Step is now a term (it used to be a reference) (doc TODO) - Omega now handles arbitrary precision integers - Idtac can now be left implicit in a [...|...] construct: for instance, [ foo | | bar ] stands for [ foo | idtac | bar ]. (doc TODO). - "Tactic Notation" extended to allow notations of tacticals (doc TODO). - Added "autorewrite with ... in hyp [using ...]" (doc TODO). - Added entry constr_may_eval for tactic extensions (new syntax). - Fixed a "fold" bug (non critical and 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. Modules - Added "Locate Module qualid" to get the full path of a module. - Module/Declare Module syntax made more uniform (doc TODO) - Added syntactic sugar "Declare Module Export/Import" and "Module Export/Import" (doc TODO) - Added syntactic sugar "Module M(Export/Import X Y: T)" and "Module Type M(Export/Import X Y: T)" (only for interactive definitions) (doc TODO) - Construct "with" generalized to module paths: T with (Definition|Module) M1.M2....Mn.l := l'. (doc TODO) Notations - "format" option aware of recursive notations Library - Few 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) Changes from V8.0beta to V8.0 ============================= Vernacular commands - New option "Set Printing All" to deactivate all high-level forms of printing (implicit arguments, coercions, destructing let, if-then-else, notations, projections) - "Functional Scheme" and "Functional Induction" extended to polymorphic types and dependent types - Notation now allows recursive patterns, hence recovering parts of the fonctionalities of pre-V8 Grammar/Syntax commands - Command "Print." discontinued. - Redundant syntax "Implicit Arguments On/Off" discontinued New syntax - Semantics change of the if-then-else construction in new syntax: "if c then t1 else t2" now stands for "match c with c1 _ ... _ => t1 | c2 _ ... _ => t2 end" with no dependency of t1 and t2 in the arguments of the constructors; this may cause incompatibilities for files translated using coq 8.0beta Interpretation scopes - Delimiting key %bool for bool_scope added - Import no more needed to activate argument scopes from a module Tactics and the tactic Language - Semantics of "assert" is now consistent with the reference manual - New tactics stepl and stepr for chaining transitivity steps - Tactic "replace ... with ... in" added - Intro patterns now supported in Ltac (parsed with prefix "ipattern:") Executables and tools - Added option -top to change the name of the toplevel module "Top" - Coqdoc updated to new syntax and now part of Coq sources - XML exportation tool now exports the structure of vernacular files (cf chapter 13 in the reference manual) User contributions - User contributions have been updated to the new syntax Bug fixes - Many bugs have been fixed (cf coq-bugs web page) Changes from V8.0beta old syntax to V8.0beta ============================================ New concrete syntax - A completely new syntax for terms - A more uniform syntax for tactics and the tactic language - A few syntactic changes for vernacular commands - A smart automatic translator translating V8.0 files in old syntax to files valid for V8.0 Syntax extensions - "Grammar" for terms disappears - "Grammar" for tactics becomes "Tactic Notation" - "Syntax" disappears - Introduction of a notion of interpretation scope allowing to use the same notations in various contexts without using specific delimiters (e.g the same expression "4<=3+x" is interpreted either in "nat", "positive", "N" (previously "entier"), "Z", "R", depending on which interpretation scope is currently open) [see documentation for details] - Notation now mandatorily requires a precedence and associativity (default was to set precedence to 1 and associativity to none) Revision of the standard library - Many lemmas and definitions names have been made more uniform mostly in Arith, NArith, ZArith and Reals (e.g : "times" -> "Pmult", "times_sym" -> "Pmult_comm", "Zle_Zmult_pos_right" -> "Zmult_le_compat_r", "SUPERIEUR" -> "Gt", "ZERO" -> "Z0") - Order and names of arguments of basic lemmas on nat, Z, positive and R have been made uniform. - Notions of Coq initial state are declared with (strict) implicit arguments - eq merged with eqT: old eq disappear, new eq (written =) is old eqT and new eqT is syntactic sugar for new eq (notation == is an alias for = and is written as it, exceptional source of incompatibilities) - Similarly, ex, ex2, all, identity are merged with exT, exT2, allT, identityT - Arithmetical notations for nat, positive, N, Z, R, without needing any backquote or double-backquotes delimiters. - In Lists: new concrete notations; argument of nil is now implicit - All changes in the library are taken in charge by the translator Semantical changes during translation - Recursive keyword set by default (and no longer needed) in Tactic Definition - Set Implicit Arguments is strict by default in new syntax - reductions in hypotheses of the form "... in H" now apply to the type also if H is a local definition - etc Gallina - New syntax of the form "Inductive bool : Set := true, false : bool." for enumerated types - Experimental syntax of the form p.(fst) for record projections (activable with option "Set Printing Projections" which is recognized by the translator) Known problems of the automatic translation - iso-latin-1 characters are no longer supported: move your files to 7-bits ASCII or unicode before translation (swith to unicode is automatically done if a file is loaded and saved again by coqide) - Renaming in ZArith: incompatibilities in Coq user contribs due to merging names INZ, from Reals, and inject_nat. - Renaming and new lemmas in ZArith: may clash with names used by users - Restructuration of ZArith: replace requirement of specific modules in ZArith by "Require Import ZArith_base" or "Require Import ZArith" - Some implicit arguments must be made explicit before translation: typically for "length nil", the implicit argument of length must be made explicit - Grammar rules, Infix notations and V7.4 Notations must be updated wrt the new scheme for syntactic extensions (see translator documentation) - Unsafe for annotation Cases when constructors coercions are used or when annotations are eta-reduced predicates Changes from V7.4 to V8.0beta old syntax ======================================== Logic - Set now predicative by default - New option -impredicative-set to set Set impredicative - The standard library doesn't need impredicativity of Set and is compatible with the classical axioms which contradict Set impredicativity Syntax for arithmetic - Notation "=" and "<>" in Z and R are no longer implicitly in Z or R (with possible introduction of a coercion), use ...=... or ...<>... instead - Locate applied to a simple string (e.g. "+") searches for all notations containing this string Vernacular commands - "Declare ML Module" now allows to import .cma files. This avoids to use a bunch of "Declare ML Module" statements when using several ML files. - "Set Printing Width n" added, allows to change the size of width printing (TODO : doc). - "Implicit Variables Type x,y:t" (new syntax: "Implicit Types x y:t") assigns default types for binding variables. - Declarations of Hints and Notation now accept a "Local" flag not to be exported outside the current file even if not in section - "Print Scopes" prints all notations - New command "About name" for light printing of type, implicit arguments, etc. - New command "Admitted" to declare incompletely proven statement as axioms - New keyword "Conjecture" to declare an axiom intended to be provable - SearchAbout can now search for lemmas referring to more than one constant and on substrings of the name of the lemma - "Print Implicit" displays the implicit arguments of a constant - Locate now searches for all names having a given suffix - New command "Functional Scheme" for building an induction principle from a function defined by case analysis and fix. Commands - new coqtop/coqc option -dont-load-proofs not to load opaque proofs in memory Implicit arguments - Inductive in sections declared with implicits now "discharged" with implicits (like constants and variables) - Implicit Arguments flags are now synchronous with reset - New switch "Unset/Set Printing Implicits" (new syntax: "Unset/Set Printing Implicit") to globally control printing of implicits Grammar extensions - UTF-8 encoded unicode blocks 0380-03FF (greek letters) and 2100-214F (letter-like, including aleph and double N,Z,Q,R) are supported identifiers; UTF-8 unicode blocs 2200-22FF (mathematical operators), 2A00-2AFF (supplemental mathematical operators) 2300-23FF (miscellaneous technical, including sqrt symbol), 2600-26FF (miscellaneous symbols) 2190-21FF (arrows A) and 2900-297F (arrows B) are supported symbols Library - New file about the factorial function in Arith - An additional elimination Acc_iter for Acc, simplier than Acc_rect. This new elimination principle is used for definition well_founded_induction. - New library NArith on binary natural numbers - R is now of type Set - Restructuration in ZArith library - "true_sub" used in Zplus now a definition, not a local one (source of incompatibilities in proof referring to true_sub, may need extra Unfold) - Some lemmas about minus moved from fast_integer to Arith/Minus.v (le_minus, lt_mult_left) (theoretical source of incompatibilities) - Several lemmas moved from auxiliary.v and zarith_aux.v to fast_integer.v (theoretical source of incompatibilities) - Variables names of iff_trans changed (source of incompatibilities) - ZArith lemmas named OMEGA something or fast_ something, and lemma new_var are now out of ZArith (except OMEGA2) - Redundant ZArith lemmas have been renamed: for the following pairs, use the second name (Zle_Zmult_right2, Zle_mult_simpl), (OMEGA2, Zle_0_plus), (Zplus_assoc_l, Zplus_assoc), (Zmult_one, Zmult_1_n), (Zmult_assoc_l, Zmult_assoc), (Zmult_minus_distr, Zmult_Zminus_distr_l) (add_un_double_moins_un_xO, is_double_moins_un), (Rlt_monotony_rev,Rlt_monotony_contra) (source of incompatibilities) - Few minor changes (no more implicit arguments in Zmult_Zminus_distr_l and Zmult_Zminus_distr_r, lemmas moved from Zcomplements to other files) (rare source of incompatibilities) - New lemmas provided by users added Tactic language - Fail tactic now accepts a failure message - Idtac tactic now accepts a message - New primitive tactic "FreshId" (new syntax: "fresh") to generate new names - Debugger prints levels of calls Tactics - Replace can now replace proofs also - Fail levels are now decremented at "Match Context" blocks only and if the right-hand-side of "Match term With" are tactics, these tactics are never evaluated immediately and do not induce backtracking (in contrast with "Match Context") - Quantified names now avoid global names of the current module (like Intro names did) [source of rare incompatibilities: 2 changes in the set of user contribs] - NewDestruct/NewInduction accepts intro patterns as introduction names - NewDestruct/NewInduction now work for non-inductive type using option "using" - A NewInduction naming bug for inductive types with functional arguments (e.g. the accessibility predicate) has been fixed (source of incompatibilities) - Symmetry now applies to hypotheses too - Inversion now accept option "as [ ... ]" to name the hypotheses - Contradiction now looks also for contradictory hypotheses stating ~A and A (source of incompatibility) - "Contradiction c" try to find an hypothesis in context which contradicts the type of c - Ring applies to new library NArith (require file NArithRing) - Field now works on types in Set - Auto with reals now try to replace le by ge (Rge_le is no longer an immediate hint), resulting in shorter proofs - Instantiate now works in hyps (syntax : Instantiate in ...) - Some new tactics : EConstructor, ELeft, Eright, ESplit, EExists - New tactic "functional induction" to perform case analysis and induction following the definition of a function. - Clear now fails when trying to remove a local definition used by a constant appearing in the current goal Extraction (See details in contrib/extraction/CHANGES) - The old commands: (Recursive) Extraction Module M. are now: (Recursive) Extraction Library M. To use these commands, M should come from a library M.v - The other syntax Extraction & Recursive Extraction now accept module names as arguments. Bugs - see coq-bugs server for the complete list of fixed bugs Miscellaneous - Implicit parameters of inductive types definition now taken into account for infering other implicit arguments Incompatibilities - Persistence of true_sub (4 incompatibilities in Coq user contributions) - Variable names of some constants changed for a better uniformity (2 changes in Coq user contributions) - Naming of quantified names in goal now avoid global names (2 occurrences) - NewInduction naming for inductive types with functional arguments (no incompatibility in Coq user contributions) - Contradiction now solve more goals (source of 2 incompatibilities) - Merge of eq and eqT may exceptionally result in subgoals now solved automatically - Redundant pairs of ZArith lemmas may have different names: it may cause "Apply/Rewrite with" to fail if using the first name of a pair of redundant lemmas (this is solved by renaming the variables bound by "with"; 3 incompatibilities in Coq user contribs) - ML programs referring to constants from fast_integer.v must use "Coqlib.gen_constant_modules Coqlib.zarith_base_modules" instead Changes from V7.3.1 to V7.4 =========================== Symbolic notations - Introduction of a notion of scope gathering notations in a consistent set; a notation sets has been developped for nat, Z and R (undocumented) - New command "Notation" for declaring notations simultaneously for parsing and printing (see chap 10 of the reference manual) - Declarations with only implicit arguments now handled (e.g. the argument of nil can be set implicit; use !nil to refer to nil without arguments) - "Print Scope sc" and "Locate ntn" allows to know to what expression a notation is bound - New defensive strategy for printing or not implicit arguments to ensure re-type-checkability of the printed term - In Grammar command, the only predefined non-terminal entries are ident, global, constr and pattern (e.g. nvar, numarg disappears); the only allowed grammar types are constr and pattern; ast and ast list are no longer supported; some incompatibilities in Grammar: when a syntax is a initial segment of an other one, Grammar does not work, use Notation Library - Lemmas in Set from Compare_dec.v (le_lt_dec, ...) and Wf_nat.v (lt_wf_rec, ...) are now transparent. This may be source of incompatibilities. - Syntactic Definitions Fst, Snd, Ex, All, Ex2, AllT, ExT, ExT2, ProjS1, ProjS2, Error, Value and Except are turned to notations. They now must be applied (incompatibilities only in unrealistic cases). - More efficient versions of Zmult and times (30% faster) - Reals: the library is now divided in 6 parts (Rbase, Rfunctions, SeqSeries, Rtrigo, Ranalysis, Integration). New tactics: Sup and RCompute. See Reals.v for details. Modules - Beta version, see doc chap 2.5 for commands and chap 5 for theory Language - Inductive definitions now accept ">" in constructor types to declare the corresponding constructor as a coercion. - Idem for assumptions declarations and constants when the type is mentionned. - The "Coercion" and "Canonical Structure" keywords now accept the same syntax as "Definition", i.e. "hyps :=c (:t)?" or "hyps :t". - Theorem-like declaration now accepts the syntax "Theorem thm [x:t;...] : u". - Remark's and Fact's now definitively behave as Theorem and Lemma: when sections are closed, the full name of a Remark or a Fact has no longer a section part (source of incompatibilities) - Opaque Local's (i.e. built by tactics and ended by Qed), do not survive section closing any longer; as a side-effect, Opaque Local's now appear in the local context of proofs; their body is hidden though (source of incompatibilities); use one of Remark/Fact/Lemma/Theorem instead to simulate the old behaviour of Local (the section part of the name is not kept though) ML tactic and vernacular commands - "Grammar tactic" and "Grammar vernac" of type "ast" are no longer supported (only "Grammar tactic simple_tactic" of type "tactic" remains available). - Concrete syntax for ML written vernacular commands and tactics is now declared at ML level using camlp4 macros TACTIC EXTEND et VERNAC COMMAND EXTEND. - "Check n c" now "n:Check c", "Eval n ..." now "n:Eval ..." - "Proof with T" (* no documentation *) - SearchAbout id - prints all theorems which contain id in their type Tactic definitions - Static globalisation of identifiers and global references (source of incompatibilities, especially, Recursive keyword is required for mutually recursive definitions). - New evaluation semantics: no more partial evaluation at definition time; evaluation of all Tactic/Meta Definition, even producing terms, expect a proof context to be evaluated (especially "()" is no longer needed). - Debugger now shows the nesting level and the reasons of failure Tactics - Equality tactics (Rewrite, Reflexivity, Symmetry, Transitivity) now understand JM equality - Simpl and Change now apply to subterms also - "Simpl f" reduces subterms whose head constant is f - Double Induction now referring to hypotheses like "Intros until" - "Inversion" now applies also on quantified hypotheses (naming as for Intros until) - NewDestruct now accepts terms with missing hypotheses - NewDestruct and NewInduction now accept user-provided elimination scheme - NewDestruct and NewInduction now accept user-provided introduction names - Omega could solve goals such as ~`x=y` but failed when the hypothesis was unfolded to `x < y` -> False. This is fixed. In addition, it can also recognize 'False' in the hypothesis and use it to solve the goal. - Coercions now handled in "with" bindings - "Subst x" replaces all ocurrences of x by t in the goal and hypotheses when an hypothesis x=t or x:=t or t=x exists - Fresh names for Assert and Pose now based on collision-avoiding Intro naming strategy (exceptional source of incompatibilities) - LinearIntuition (* no documentation *) - Unfold expects a correct evaluable argument - Clear expects existing hypotheses Extraction (See details in contrib/extraction/CHANGES and README): - An experimental Scheme extraction is provided. - Concerning Ocaml, extracted code is now ensured to always type-check, thanks to automatic inserting of Obj.magic. - Experimental extraction of Coq new modules to Ocaml modules. Proof rendering in natural language - Export of theories to XML for publishing and rendering purposes now includes proof-trees (see http://www.cs.unibo.it/helm) Miscellaneous - Printing Coercion now used through the standard keywords Set/Add, Test, Print - "Print Term id" is an alias for "Print id" - New switch "Unset/Set Printing Symbols" to control printing of symbolic notations - Two new variants of implicit arguments are available - "Unset/Set Contextual Implicits" tells to consider implicit also the arguments inferable from the context (e.g. for nil or refl_eq) - "Unset/Set Strict Implicits" tells to consider implicit only the arguments that are inferable in any case (i.e. arguments that occurs as argument of rigid constants in the type of the remaining arguments; e.g. the witness of an existential is not strict since it can vanish when applied to a predicate which does not use its argument) Incompatibilities - "Grammar tactic ... : ast" and "Grammar vernac ... : ast" are no longer supported, use TACTIC EXTEND and VERNAC COMMAND EXTEND on the ML-side instead - Transparency of le_lt_dec and co (leads to some simplification in proofs; in some cases, incompatibilites is solved by declaring locally opaque the relevant constant) - Opaque Local do not now survive section closing (rename them into Remark/Lemma/... to get them still surviving the sections; this renaming allows also to solve incompatibilites related to now forbidden calls to the tactic Clear) - Remark and Fact have no longer (very) long names (use Local instead in case of name conflict) Bugs - Improved localisation of errors in Syntactic Definitions - Induction principle creation failure in presence of let-in fixed (#238) - Inversion bugs fixed (#212 and #220) - Omega bug related to Set fixed (#180) - Type-checking inefficiency of nested destructuring let-in fixed (#216) - Improved handling of let-in during holes resolution phase (#239) Efficiency - Implementation of a memory sharing strategy reducing memory requirements by an average ratio of 3. Changes from V7.3 to V7.3.1 =========================== Bug fixes - Corrupted Field tactic and Match Context tactic construction fixed - Checking of names already existing in Assert added (PR#182) - Invalid argument bug in Exact tactic solved (PR#183) - Colliding bound names bug fixed (PR#202) - Wrong non-recursivity test for Record fixed (PR#189) - Out of memory/seg fault bug related to parametric inductive fixed (PR#195) - Setoid_replace/Setoid_rewrite bug wrt "==" fixed Misc - Ocaml version >= 3.06 is needed to compile Coq from sources - Simplification of fresh names creation strategy for Assert, Pose and LetTac (PR#192) Changes from V7.2 to V7.3 ========================= Language - Slightly improved compilation of pattern-matching (slight source of incompatibilities) - Record's now accept anonymous fields "_" which does not build projections - Changes in the allowed elimination sorts for certain class of inductive definitions : an inductive definition without constructors of Sort Prop can be eliminated on sorts Set and Type A "singleton" inductive definition (one constructor with arguments in the sort Prop like conjunction of two propositions or equality) can be eliminated directly on sort Type (In V7.2, only the sorts Prop and Set were allowed) Tactics - New tactic "Rename x into y" for renaming hypotheses - New tactics "Pose x:=u" and "Pose u" to add definitions to local context - Pattern now working on partially applied subterms - Ring no longer applies irreversible congruence laws of mult but better applies congruence laws of plus (slight source of incompatibilities). - Field now accepts terms to be simplified as arguments (as for Ring). This extension has been also implemented using the toplevel tactic language. - Intuition does no longer unfold constants except "<->" and "~". It can be parameterized by a tactic. It also can introduce dependent product if needed (source of incompatibilities) - "Match Context" now matching more recent hypotheses first and failing only on user errors and Fail tactic (possible source of incompatibilities) - Tactic Definition's without arguments now allowed in Coq states - Better simplification and discrimination made by Inversion (source of incompatibilities) Bugs - "Intros H" now working like "Intro H" trying first to reduce if not a product - Forward dependencies in Cases now taken into account - Known bugs related to Inversion and let-in's fixed - Bug unexpected Delta with let-in now fixed Extraction (details in contrib/extraction/CHANGES or documentation) - Signatures of extracted terms are now mostly expunged from dummy arguments. - Haskell extraction is now operational (tested & debugged). Standard library - Some additions in [ZArith]: three files (Zcomplements.v, Zpower.v and Zlogarithms.v) moved from contrib/omega in order to be more visible, one Zsgn function, more induction principles (Wf_Z.v and tail of Zcomplements.v), one more general Euclid theorem - Peano_dec.v and Compare_dec.v now part of Arith.v Tools - new option -dump-glob to coqtop to dump globalizations (to be used by the new documentation tool coqdoc; see http://www.lri.fr/~filliatr/coqdoc) User Contributions - CongruenceClosure (congruence closure decision procedure) [Pierre Corbineau, ENS Cachan] - MapleMode (an interface to embed Maple simplification procedures over rational fractions in Coq) [David Delahaye, Micaela Mayero, Chalmers University] - Presburger: A formalization of Presburger's algorithm [Laurent Thery, INRIA Sophia Antipolis] - Chinese has been rewritten using Z from ZArith as datatype ZChinese is the new version, Chinese the obsolete one [Pierre Letouzey, LRI Orsay] Incompatibilities - Ring: exceptional incompatibilities (1 above 650 in submitted user contribs, leading to a simplification) - Intuition: does not unfold any definition except "<->" and "~" - Cases: removal of some extra Cases in configurations of the form "Cases ... of C _ => ... | _ D => ..." (effects on 2 definitions of submitted user contributions necessitating the removal of now superfluous proof steps in 3 different proofs) - Match Context, in case of incompatibilities because of a now non trapped error (e.g. Not_found or Failure), use instead tactic Fail to force Match Context trying the next clause - Inversion: better simplification and discrimination may occasionally lead to less subgoals and/or hypotheses and different naming of hypotheses - Unification done by Apply/Elim has been changed and may exceptionally lead to incompatible instantiations - Peano_dec.v and Compare_dec.v parts of Arith.v make Auto more powerful if these files were not already required (1 occurrence of this in submitted user contribs) Changes from V7.1 to V7.2 ========================= Language - Automatic insertion of patterns for local definitions in the type of the constructors of an inductive types (for compatibility with V6.3 let-in style) - Coercions allowed in Cases patterns - New declaration "Canonical Structure id = t : I" to help resolution of equations of the form (proj ?)=a; if proj(e)=a then a is canonically equipped with the remaining fields in e, i.e. ? is instantiated by e Tactics - New tactic "ClearBody H" to clear the body of definitions in local context - New tactic "Assert H := c" for forward reasoning - Slight improvement in naming strategy for NewInduction/NewDestruct - Intuition/Tauto do not perform useless unfolding and work up to conversion Extraction (details in contrib/extraction/CHANGES or documentation) - Syntax changes: there are no more options inside the extraction commands. New commands for customization and options have been introduced instead. - More optimizations on extracted code. - Extraction tests are now embedded in 14 user contributions. Standard library - In [Relations], Rstar.v and Newman.v now axiom-free. - In [Sets], Integers.v now based on nat - In [Arith], more lemmas in Min.v, new file Max.v, tail-recursive plus and mult added to Plus.v and Mult.v respectively - New directory [Sorting] with a proof of heapsort (dragged from 6.3.1 lib) - In [Reals], more lemmas in Rbase.v, new lemmas on square, square root and trigonometric functions (R_sqr.v - Rtrigo.v); a complementary approach and new theorems about continuity and derivability in Ranalysis.v; some properties in plane geometry such as translation, rotation or similarity in Rgeom.v; finite sums and Chasles property in Rsigma.v Bugs - Confusion between implicit args of locals and globals of same base name fixed - Various incompatibilities wrt inference of "?" in V6.3.1 fixed - Implicits in infix section variables bug fixed - Known coercions bugs fixed - Apply "universe anomaly" bug fixed - NatRing now working - "Discriminate 1", "Injection 1", "Simplify_eq 1" now working - NewInduction bugs with let-in and recursively dependent hypotheses fixed - Syntax [x:=t:T]u now allowed as mentioned in documentation - Bug with recursive inductive types involving let-in fixed - Known pattern-matching bugs fixed - Known Cases elimination predicate bugs fixed - Improved errors messages for pattern-matching and projections - Better error messages for ill-typed Cases expressions Incompatibilities - New naming strategy for NewInduction/NewDestruct may affect 7.1 compatibility - Extra parentheses may exceptionally be needed in tactic definitions. - Coq extensions written in Ocaml need to be updated (see dev/changements.txt for a description of the main changes in the interface files of V7.2) - New behaviour of Intuition/Tauto may exceptionally lead to incompatibilities ---------------------------------------------------------------------------- Changes from V6.3.1 and V7.0 to V7.1 ==================================== Notes: - items followed by (**) are important sources of incompatibilities - items followed by (*) may exceptionally be sources of incompatibilities - items followed by (+) have been introduced in version 7.0 Main novelties ============== References are to Coq V7.1 reference manual - New primitive let-in construct (see sections 1.2.8 and ) - Long names (see sections 2.6 and 2.7) - New high-level tactic language (see chapter 10) - Improved search facilities (see section 5.2) - New extraction algorithm managing the Type level (see chapter 17) - New rewriting tactic for arbitrary equalities (see chapter 19) - New tactic Field to decide equalities on commutative fields (see 7.11) - New tactic Fourier to solve linear inequalities on reals numbers (see 7.11) - New tactics for induction/case analysis in "natural" style (see 7.7) - Deep restructuration of the code (safer, simpler and more efficient) - Export of theories to XML for publishing and rendering purposes (see http://www.cs.unibo.it/helm) Details of changes ================== Language: new "let-in" construction ----------------------------------- - New construction for local definitions (let-in) with syntax [x:=u]t (*)(+) - Local definitions allowed in Record (a.k.a. record à la Randy Pollack) Language: long names -------------------- - Each construction has a unique absolute names built from a base name, the name of the module in which they are defined (Top if in coqtop), and possibly an arbitrary long sequence of directory (e.g. "Coq.Lists.PolyList.flat_map" where "Coq" means that "flat_map" is part of Coq standard library, "Lists" means it is defined in the Lists library and "PolyList" means it is in the file Polylist) (+) - Constructions can be referred by their base name, or, in case of conflict, by a "qualified" name, where the base name is prefixed by the module name (and possibly by a directory name, and so on). A fully qualified name is an absolute name which always refer to the construction it denotes (to preserve the visibility of all constructions, no conflict is allowed for an absolute name) (+) - Long names are available for modules with the possibility of using the directory name as a component of the module full name (with option -R to coqtop and coqc, or command Add LoadPath) (+) - Improved conflict resolution strategy (the Unix PATH model), allowing more constructions to be referred just by their base name Language: miscellaneous ----------------------- - The names of variables for Record projections _and_ for induction principles (e.g. sum_ind) is now based on the first letter of their type (main source of incompatibility) (**)(+) - Most typing errors have now a precise location in the source (+) - Slightly different mechanism to solve "?" (*)(+) - More arguments may be considered implicit at section closing (*)(+) - Bug with identifiers ended by a number greater than 2^30 fixed (+) - New visibility discipline for Remark, Fact and Local: Remark's and Fact's now survive at the end of section, but are only accessible using a qualified names as soon as their strength expires; Local's disappear and are moved into local definitions for each construction persistent at section closing Language: Cases --------------- - Cases no longer considers aliases inferable from dependencies in types (*)(+) - A redundant clause in Cases is now an error (*) Reduction --------- - New reduction flags "Zeta" and "Evar" in Eval Compute, for inlining of local definitions and instantiation of existential variables - Delta reduction flag does not perform Zeta and Evar reduction any more (*) - Constants declared as opaque (using Qed) can no longer become transparent (a constant intended to be alternatively opaque and transparent must be declared as transparent (using Defined)); a risk exists (until next Coq version) that Simpl and Hnf reduces opaque constants (*) New tactics ----------- - New set of tactics to deal with types equipped with specific equalities (a.k.a. Setoids, e.g. nat equipped with eq_nat) [by C. Renard] - New tactic Assert, similar to Cut but expected to be more user-friendly - New tactic NewDestruct and NewInduction intended to replace Elim and Induction, Case and Destruct in a more user-friendly way (see restrictions in the reference manual) - New tactic ROmega: an experimental alternative (based on reflexion) to Omega [by P. Crégut] - New tactic language Ltac (see reference manual) (+) - New versions of Tauto and Intuition, fully rewritten in the new Ltac language; they run faster and produce more compact proofs; Tauto is fully compatible but, in exchange of a better uniformity, Intuition is slightly weaker (then use Tauto instead) (**)(+) - New tactic Field to decide equalities on commutative fields (as a special case, it works on real numbers) (+) - New tactic Fourier to solve linear inequalities on reals numbers [by L. Pottier] (+) - New tactics dedicated to real numbers: DiscrR, SplitRmult, SplitAbsolu (+) Changes in existing tactics --------------------------- - Reduction tactics in local definitions apply only to the body - New syntax of the form "Compute in Type of H." to require a reduction on the types of local definitions - Inversion, Injection, Discriminate, ... apply also on the quantified premises of a goal (using the "Intros until" syntax) - Decompose has been fixed but hypotheses may get different names (*)(+) - Tauto now manages uniformly hypotheses and conclusions of the form "t=t" which all are considered equivalent to "True". Especially, Tauto now solves goals of the form "H : ~ t = t |- A". - The "Let" tactic has been renamed "LetTac" and is now based on the primitive "let-in" (+) - Elim can no longer be used with an elimination schema different from the one defined at definition time of the inductive type. To overload an elimination schema, use "Elim using " (*)(+) - Simpl no longer unfolds the recursive calls of a mutually defined fixpoint (*)(+) - Intro now fails if the hypothesis name already exists (*)(+) - "Require Prolog" is no longer needed (i.e. it is available by default) (*)(+) - Unfold now fails on a non unfoldable identifier (*)(+) - Unfold also applies on definitions of the local context - AutoRewrite now deals only with the main goal and it is the purpose of Hint Rewrite to deal with generated subgoals (+) - Redundant or incompatible instantiations in Apply ... with ... are now correctly managed (+) Efficiency ---------- - Excessive memory uses specific to V7.0 fixed - Sizes of .vo files vary a lot compared to V6.3 (from -30% to +300% depending on the developments) - An improved reduction strategy for lazy evaluation - A more economical mechanism to ensure logical consistency at the Type level; warning: this is experimental and may produce "universes" anomalies (please report) Concrete syntax of constructions -------------------------------- - Only identifiers starting with "_" or a letter, and followed by letters, digits, "_" or "'" are allowed (e.g. "$" and "@" are no longer allowed) (*) - A multiple binder like (a:A)(a,b:(P a))(Q a) is no longer parsed as (a:A)(a0:(P a))(b:(P a))(Q a0) but as (a:A)(a0:(P a))(b:(P a0))(Q a0) (*)(+) - A dedicated syntax has been introduced for Reals (e.g ``3+1/x``) (+) - Pretty-printing of Infix notations fixed. (+) Parsing and grammar extension ----------------------------- - More constraints when writing ast - "{...}" and the macros $LIST, $VAR, etc. now expect a metavariable (an identifier starting with $) (*) - identifiers should starts with a letter or "_" and be followed by letters, digits, "_" or "'" (other characters are still supported but it is not advised to use them) (*)(+) - Entry "command" in "Grammar" and quotations (<<...>> stuff) is renamed "constr" as in "Syntax" (+) - New syntax "[" sentence_1 ... sentence_n"]." to group sentences (useful for Time and to write grammar rules abbreviating several commands) (+) - The default parser for actions in the grammar rules (and for patterns in the pretty-printing rules) is now the one associated to the grammar (i.e. vernac, tactic or constr); no need then for quotations as in <:vernac:<...>>; to return an "ast", the grammar must be explicitly typed with tag ": ast" or ": ast list", or if a syntax rule, by using <<...>> in the patterns (expression inside these angle brackets are parsed as "ast"); for grammars other than vernac, tactic or constr, you may explicitly type the action with tags ": constr", ": tactic", or ":vernac" (**)(+) - Interpretation of names in Grammar rule is now based on long names, which allows to avoid problems (or sometimes tricks;) related to overloaded names (+) New commands ------------ - New commands "Print XML All", "Show XML Proof", ... to show or export theories to XML to be used with Helm's publishing and rendering tools (see http://www.cs.unibo.it/helm) (by Claudio Sacerdoti Coen) (+) - New commands to manually set implicit arguments (+) - "Implicits ident." to activate the implicit arguments mode just for ident - "Implicits ident [num1 num2 ...]." to explicitly give which arguments have to be considered as implicit - New SearchPattern/SearchRewrite (by Yves Bertot) (+) - New commands "Debug on"/"Debug off" to activate/deactivate the tactic language debugger (+) - New commands to map physical paths to logical paths (+) - Add LoadPath physical_dir as logical_dir - Add Rec LoadPath physical_dir as logical_dir Changes in existing commands ---------------------------- - Generalization of the usage of qualified identifiers in tactics and commands about globals, e.g. Decompose, Eval Delta; Hints Unfold, Transparent, Require - Require synchronous with Reset; Require's scope stops at Section ending (*) - For a module indirectly loaded by a "Require" but not exported, the command "Import module" turns the constructions defined in the module accessible by their short name, and activates the Grammar, Syntax, Hint, ... declared in the module (+) - The scope of the "Search" command can be restricted to some modules (+) - Final dot in command (full stop/period) must be followed by a blank (newline, tabulation or whitespace) (+) - Slight restriction of the syntax for Cbv Delta: if present, option [-myconst] must immediately follow the Delta keyword (*)(+) - SearchIsos currently not supported - Add ML Path is now implied by Add LoadPath (+) - New names for the following commands (+) AddPath -> Add LoadPath Print LoadPath -> Print LoadPath DelPath -> Remove LoadPath AddRecPath -> Add Rec LoadPath Print Path -> Print Coercion Paths Implicit Arguments On -> Set Implicit Arguments Implicit Arguments Off -> Unset Implicit Arguments Begin Silent -> Set Silent End Silent -> Unset Silent. Tools ----- - coqtop (+) - Two executables: coqtop.byte and coqtop.opt (if supported by the platform) - coqtop is a link to the more efficient executable (coqtop.opt if present) - option -full is obsolete (+) - do_Makefile renamed into coq_makefile (+) - New option -R to coqtop and coqc to map a physical directory to a logical one (+) - coqc no longer needs to create a temporary file - No more warning if no initialization file .coqrc exists Extraction ---------- - New algorithm for extraction able to deal with "Type" (+) (by J.-C. Filliâtre and P. Letouzey) Standard library ---------------- - New library on maps on integers (IntMap, contributed by Jean Goubault) - New lemmas about integer numbers [ZArith] - New lemmas and a "natural" syntax for reals [Reals] (+) - Exc/Error/Value renamed into Option/Some/None (*) New user contributions ---------------------- - Constructive complex analysis and the Fundamental Theorem of Algebra [FTA] (Herman Geuvers, Freek Wiedijk, Jan Zwanenburg, Randy Pollack, Henk Barendregt, Nijmegen) - A new axiomatization of ZFC set theory [Functions_in_ZFC] (C. Simpson, Sophia-Antipolis) - Basic notions of graph theory [GRAPHS-BASICS] (Jean Duprat, Lyon) - A library for floating-point numbers [Float] (Laurent Théry, Sylvie Boldo, Sophia-Antipolis) - Formalisation of CTL and TCTL temporal logic [CtlTctl] (Carlos Daniel Luna,Montevideo) - Specification and verification of the Railroad Crossing Problem in CTL and TCTL [RailroadCrossing] (Carlos Daniel Luna,Montevideo) - P-automaton and the ABR algorithm [PAutomata] (Christine Paulin, Emmanuel Freund, Orsay) - Semantics of a subset of the C language [MiniC] (Eduardo Giménez, Emmanuel Ledinot, Suresnes) - Correctness proofs of the following imperative algorithms: Bresenham line drawing algorithm [Bresenham], Marché's minimal edition distance algorithm [Diff] (Jean-Christophe Filliâtre, Orsay) - Correctness proofs of Buchberger's algorithm [Buchberger] and RSA cryptographic algorithm [Rsa] (Laurent Théry, Sophia-Antipolis) - Correctness proof of Stalmarck tautology checker algorithm [Stalmarck] (Laurent Théry, Pierre Letouzey, Sophia-Antipolis)