diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-10 13:22:29 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-10 13:22:29 +0000 |
| commit | 05085e80668a4d1dedc522c6af343168870cc648 (patch) | |
| tree | 084048fdff9f8d460e75ece78d5297b583d952f4 | |
| parent | d52641d2cda2af132c13dcb481f753d51e7af216 (diff) | |
First release of Vector library.
To avoid names¬ations clashs with list, Vector shouldn't be
"Import"ed but one can "Import Vector.VectorNotations." to have
notations.
SetoidVector at least remains to do.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13702 85f007b7-540e-0410-9357-904b9bb8a0f7
50 files changed, 968 insertions, 483 deletions
@@ -33,6 +33,11 @@ Libraries may introduce incompatibilities. In particular, the order of the arguments for BigN.shiftl and BigN.shiftr is now reversed: the number to shift now comes first. By default, the power function now takes two BigN. +- Creation of Vector, an idenpedant library for list indiced by their length. + Vectors' names overwrite lists' one so you shouldn't "Import" the library. + All old names change: functions' name become the CaML one and for example + Vcons become Vector.cons. You can use notations by importing + Vector.VectorNotations. Internal infrastructure @@ -83,7 +88,7 @@ Automation tactics hints (wish #2104). - An inductive type as argument of the "using" option of "auto/eauto/firstorder" is interpreted as using the collection of its constructors. -- New decision tactic "nsatz" to prove polynomial equations +- New decision tactic "nsatz" to prove polynomial equations by computation of Groebner bases. Other tactics @@ -95,9 +100,9 @@ Other tactics - Tactic "quote" now supports quotation of arbitrary terms (not just the goal). - Tactic "idtac" now displays its "list" arguments. -- New introduction patterns "*" for introducing the next block of dependent +- New introduction patterns "*" for introducing the next block of dependent variables and "**" for introducing all quantified variables and hypotheses. -- Pattern Unification for existential variables activated in tactics and +- Pattern Unification for existential variables activated in tactics and new option "Unset Tactic Evars Pattern Unification" to deactivate it. - Resolution of canonical structure is now part of the tactic's unification algorithm. @@ -214,11 +219,11 @@ Program that they can work on any subset of the arguments directly (uses currying). - Try to automatically clear structural fixpoint prototypes in obligations to avoid issues with opacity. -- Use return type clause inference in pattern-matching as in the standard +- Use return type clause inference in pattern-matching as in the standard typing algorithm. - Support [Local Obligation Tactic] and [Next Obligation with tactic]. - Use [Show Obligation Tactic] to print the current default tactic. -- [fst] and [snd] have maximal implicit arguments in Program now (possible +- [fst] and [snd] have maximal implicit arguments in Program now (possible source of incompatibility). Type classes @@ -229,7 +234,7 @@ Type classes - Use [Existing Class foo] to declare foo as a class a posteriori. [foo] can be an inductive type or a constant definition. No projections or instances are defined. -- Various bug fixes and improvements: support for defined fields, +- Various bug fixes and improvements: support for defined fields, anonymous instances, declarations giving terms, better handling of sections and [Context]. @@ -281,7 +286,7 @@ Library of incompatibilities solvable by qualifying names accordingly). - In ListSet, set_map has been fixed (source of incompatibilities if used). - Sorting library: - - new mergesort of worst-case complexity O(n*ln(n)) made available in + - new mergesort of worst-case complexity O(n*ln(n)) made available in Mergesort.v; - former notion of permutation up to setoid from Permutation.v is deprecated and moved to PermutSetoid.v; @@ -376,22 +381,22 @@ Changes from V8.1 to V8.2 Language -- If a fixpoint is not written with an explicit { struct ... }, then - all arguments are tried successively (from left to right) until one is +- If a fixpoint is not written with an explicit { struct ... }, then + all arguments are tried successively (from left to right) until one is found that satisfies the structural decreasing condition. -- New experimental typeclass system giving ad-hoc polymorphism and +- New experimental typeclass system giving ad-hoc polymorphism and overloading based on dependent records and implicit arguments. - New syntax "let 'pat := b in c" for let-binding using irrefutable patterns. -- New syntax "forall {A}, T" for specifying maximally inserted implicit +- New syntax "forall {A}, T" for specifying maximally inserted implicit arguments in terms. - Sort of Record/Structure, Inductive and CoInductive defaults to Type if omitted. -- (Co)Inductive types can be defined as records +- (Co)Inductive types can be defined as records (e.g. "CoInductive stream := { hd : nat; tl : stream }.") - New syntax "Theorem id1:t1 ... with idn:tn" for proving mutually dependent statements. - Support for sort-polymorphism on constants denoting inductive types. -- Several evolutions of the module system (handling of module aliases, +- Several evolutions of the module system (handling of module aliases, functorial module types, an Include feature, etc). - Prop now a subtype of Set (predicative and impredicative forms). - Recursive inductive types in Prop with a single constructor of which @@ -409,18 +414,18 @@ Vernacular commands - Modification of the Scheme command so you can ask for the name to be automatically computed (e.g. Scheme Induction for nat Sort Set). - New command "Combined Scheme" to build combined mutual induction - principles from existing mutual induction principles. -- New command "Scheme Equality" to build a decidable (boolean) equality + principles from existing mutual induction principles. +- New command "Scheme Equality" to build a decidable (boolean) equality for simple inductive datatypes and a decision property over this equality (e.g. Scheme Equality for nat). -- Added option "Set Equality Scheme" to make automatic the declaration +- Added option "Set Equality Scheme" to make automatic the declaration of the boolean equality when possible. -- Source of universe inconsistencies now printed when option +- Source of universe inconsistencies now printed when option "Set Printing Universes" is activated. - New option "Set Printing Existential Instances" for making the display of existential variable instances explicit. -- Support for option "[id1 ... idn]", and "-[id1 ... idn]", for the - "compute"/"cbv" reduction strategy, respectively meaning reduce only, or +- Support for option "[id1 ... idn]", and "-[id1 ... idn]", for the + "compute"/"cbv" reduction strategy, respectively meaning reduce only, or everything but, the constants id1 ... idn. "lazy" alone or followed by "[id1 ... idn]", and "-[id1 ... idn]" also supported, meaning apply all of beta-iota-zeta-delta, possibly restricting delta. @@ -447,46 +452,46 @@ Libraries SetoidList, ListSet, Sorting, Zmisc. This may induce a few incompatibilities. In case of trouble while fixing existing development, it may help to simply declare Set as an alias for Type (see file - SetIsType). -- New arithmetical library in theories/Numbers. It contains: - * an abstract modular development of natural and integer arithmetics + SetIsType). +- New arithmetical library in theories/Numbers. It contains: + * an abstract modular development of natural and integer arithmetics in Numbers/Natural/Abstract and Numbers/Integer/Abstract - * an implementation of efficient computational bounded and unbounded + * an implementation of efficient computational bounded and unbounded integers that can be mapped to processor native arithmetics. - See Numbers/Cyclic/Int31 for 31-bit integers and Numbers/Natural/BigN + See Numbers/Cyclic/Int31 for 31-bit integers and Numbers/Natural/BigN for unbounded natural numbers and Numbers/Integer/BigZ for unbounded - integers. + integers. * some proofs that both older libraries Arith, ZArith and NArith and newer BigN and BigZ implement the abstract modular development. - This allows in particular BigN and BigZ to already come with a + This allows in particular BigN and BigZ to already come with a large database of basic lemmas and some generic tactics (ring), This library has still an experimental status, as well as the processor-acceleration mechanism, but both its abstract and its concrete parts are already quite usable and could challenge the use - of nat, N and Z in actual developments. Moreover, an extension of + of nat, N and Z in actual developments. Moreover, an extension of this framework to rational numbers is ongoing, and an efficient - Q structure is already provided (see Numbers/Rational/BigQ), but - this part is currently incomplete (no abstract layer and generic + Q structure is already provided (see Numbers/Rational/BigQ), but + this part is currently incomplete (no abstract layer and generic lemmas). - Many changes in FSets/FMaps. In practice, compatibility with earlier version should be fairly good, but some adaptations may be required. * Interfaces of unordered ("weak") and ordered sets have been factorized thanks to new features of Coq modules (in particular Include), see FSetInterface. Same for maps. Hints in these interfaces have been - reworked (they are now placed in a "set" database). + reworked (they are now placed in a "set" database). * To allow full subtyping between weak and ordered sets, a field "eq_dec" has been added to OrderedType. The old version of OrderedType - is now called MiniOrderedType and functor MOT_to_OT allow to + is now called MiniOrderedType and functor MOT_to_OT allow to convert to the new version. The interfaces and implementations of sets now contain also such a "eq_dec" field. * FSetDecide, contributed by Aaron Bohannon, contains a decision - procedure allowing to solve basic set-related goals (for instance, + procedure allowing to solve basic set-related goals (for instance, is a point in a particular set ?). See FSetProperties for examples. * Functors of properties have been improved, especially the ones about - maps, that now propose some induction principles. Some properties - of fold need less hypothesis. + maps, that now propose some induction principles. Some properties + of fold need less hypothesis. * More uniformity in implementations of sets and maps: they all use - implicit arguments, and no longer export unnecessary scopes (see + implicit arguments, and no longer export unnecessary scopes (see bug #1347) * Internal parts of the implementations based on AVL have evolved a lot. The main files FSetAVL and FMapAVL are now much more @@ -500,31 +505,31 @@ Libraries structural yet efficient. The appendix files also contains alternative versions of these few functions, much closer to the initial Ocaml code and written via the Function framework. -- Library IntMap, subsumed by FSets/FMaps, has been removed from +- Library IntMap, subsumed by FSets/FMaps, has been removed from Coq Standard Library and moved into a user contribution Cachan/IntMap -- Better computational behavior of some constants (eq_nat_dec and - le_lt_dec more efficient, Z_lt_le_dec and Positive_as_OT.compare +- Better computational behavior of some constants (eq_nat_dec and + le_lt_dec more efficient, Z_lt_le_dec and Positive_as_OT.compare transparent, ...) (exceptional source of incompatibilities). - Boolean operators moved from module Bool to module Datatypes (may need to rename qualified references in script and force notations || and && to be at levels 50 and 40 respectively). -- The constructors xI and xO of type positive now have postfix notations - "~1" and "~0", allowing to write numbers in binary form easily, for instance +- The constructors xI and xO of type positive now have postfix notations + "~1" and "~0", allowing to write numbers in binary form easily, for instance 6 is 1~1~0 and 4*p is p~0~0 (see BinPos.v). -- Improvements to NArith (Nminus, Nmin, Nmax), and to QArith (in particular +- Improvements to NArith (Nminus, Nmin, Nmax), and to QArith (in particular a better power function). -- Changes in ZArith: several additional lemmas (used in theories/Numbers), +- Changes in ZArith: several additional lemmas (used in theories/Numbers), especially in Zdiv, Znumtheory, Zpower. Moreover, many results in Zdiv have been generalized: the divisor may simply be non-null instead of strictly positive (see lemmas with name ending by "_full"). An alternative file ZOdiv proposes a different behavior (the one of Ocaml) when dividing by negative numbers. -- Changes in Arith: EqNat and Wf_nat now exported from Arith, some +- Changes in Arith: EqNat and Wf_nat now exported from Arith, some constructions on nat that were outside Arith are now in (e.g. iter_nat). -- In SetoidList, eqlistA now expresses that two lists have similar elements - at the same position, while the predicate previously called eqlistA - is now equivlistA (this one only states that the lists contain the same - elements, nothing more). +- In SetoidList, eqlistA now expresses that two lists have similar elements + at the same position, while the predicate previously called eqlistA + is now equivlistA (this one only states that the lists contain the same + elements, nothing more). - Changes in Reals: * Most statement in "sigT" (including the completeness axiom) are now in "sig" (in case of incompatibility, @@ -541,7 +546,7 @@ Libraries - Definition of pred and minus made compatible with the structural decreasing criterion for use in fixpoints. - Files Relations/Rstar.v and Relations/Newman.v moved out to the user - contribution repository (contribution CoC_History). New lemmas about + contribution repository (contribution CoC_History). New lemmas about transitive closure added and some bound variables renamed (exceptional risk of incompatibilities). - Syntax for binders in terms (e.g. for "exists") supports anonymous names. @@ -609,7 +614,7 @@ Tactics - New tactics "ediscriminate", "einjection", "esimplify_eq". - Tactics "discriminate", "injection", "simplify_eq" now support any term as argument. Clause "with" is also supported. -- Unfoldable references can be given by notation's string rather than by name +- Unfoldable references can be given by notation's string rather than by name in unfold. - The "with" arguments are now typed using informations from the current goal: allows support for coercions and more inference of implicit arguments. @@ -622,8 +627,8 @@ Tactics (possible source of parsing incompatibilities when destruct or induction is part of a let-in expression in Ltac; extra parentheses are then required). - New support for "as" clause in tactics "apply in" and "eapply in". -- Some new intro patterns: - * intro pattern "?A" genererates a fresh name based on A. +- Some new intro patterns: + * intro pattern "?A" genererates a fresh name based on A. Caveat about a slight loss of compatibility: Some intro patterns don't need space between them. In particular intros ?a?b used to be legal and equivalent to intros ? a ? b. Now it @@ -632,31 +637,31 @@ Tactics for right-associative constructs like /\ or exists. - Several syntax extensions concerning "rewrite": * "rewrite A,B,C" can be used to rewrite A, then B, then C. These rewrites - occur only on the first subgoal: in particular, side-conditions of the + occur only on the first subgoal: in particular, side-conditions of the "rewrite A" are not concerned by the "rewrite B,C". - * "rewrite A by tac" allows to apply tac on all side-conditions generated by + * "rewrite A by tac" allows to apply tac on all side-conditions generated by the "rewrite A". - * "rewrite A at n" allows to select occurrences to rewrite: rewrite only + * "rewrite A at n" allows to select occurrences to rewrite: rewrite only happen at the n-th exact occurrence of the first successful matching of - A in the goal. + A in the goal. * "rewrite 3 A" or "rewrite 3!A" is equivalent to "rewrite A,A,A". * "rewrite !A" means rewriting A as long as possible (and at least once). * "rewrite 3?A" means rewriting A at most three times. * "rewrite ?A" means rewriting A as long as possible (possibly never). - * many of the above extensions can be combined with each other. + * many of the above extensions can be combined with each other. - Introduction patterns better respect the structure of context in presence of - missing or extra names in nested disjunction-conjunction patterns [possible + missing or extra names in nested disjunction-conjunction patterns [possible source of rare incompatibilities]. - New syntax "rename a into b, c into d" for "rename a into b; rename c into d" - New tactics "dependent induction/destruction H [ generalizing id_1 .. id_n ]" to do induction-inversion on instantiated inductive families à la BasicElim. -- Tactics "apply" and "apply in" now able to reason modulo unfolding of - constants (possible source of incompatibility in situations where apply +- Tactics "apply" and "apply in" now able to reason modulo unfolding of + constants (possible source of incompatibility in situations where apply may fail, e.g. as argument of a try or a repeat and in a ltac function); - versions that do not unfold are renamed into "simple apply" and + versions that do not unfold are renamed into "simple apply" and "simple apply in" (usable for compatibility or for automation). -- Tactics "apply" and "apply in" now able to traverse conjunctions and to - select the first matching lemma among the components of the conjunction; +- Tactics "apply" and "apply in" now able to traverse conjunctions and to + select the first matching lemma among the components of the conjunction; tactic "apply" also able to apply lemmas of conclusion an empty type. - Tactic "apply" now supports application of several lemmas in a row. - Tactics "set" and "pose" can set functions using notation "(f x1..xn := c)". @@ -666,69 +671,69 @@ Tactics - Tactic "generalize" now supports "at" options to specify occurrences and "as" options to name the quantified hypotheses. - New tactic "specialize H with a" or "specialize (H a)" allows to transform - in-place a universally-quantified hypothesis (H : forall x, T x) into its + in-place a universally-quantified hypothesis (H : forall x, T x) into its instantiated form (H : T a). Nota: "specialize" was in fact there in earlier versions of Coq, but was undocumented, and had a slightly different behavior. - New tactic "contradict H" can be used to solve any kind of goal as long as the user can provide afterwards a proof of the negation of the hypothesis H. If H is already a negation, say ~T, then a proof of T is asked. If the current goal is a negation, say ~U, then U is saved in H afterwards, - hence this new tactic "contradict" extends earlier tactic "swap", which is + hence this new tactic "contradict" extends earlier tactic "swap", which is now obsolete. -- Tactics f_equal is now done in ML instead of Ltac: it now works on any +- Tactics f_equal is now done in ML instead of Ltac: it now works on any equality of functions, regardless of the arity of the function. - New options "before id", "at top", "at bottom" for tactics "move"/"intro". -- Some more debug of reflexive omega (romega), and internal clarifications. +- Some more debug of reflexive omega (romega), and internal clarifications. Moreover, romega now has a variant "romega with *" that can be also used on non-Z goals (nat, N, positive) via a call to a translation tactic named zify (its purpose is to Z-ify your goal...). This zify may also be used - independantly of romega. -- Tactic "remember" now supports an "in" clause to remember only selected + independantly of romega. +- Tactic "remember" now supports an "in" clause to remember only selected occurrences of a term. - Tactic "pose proof" supports name overwriting in case of specialization of an hypothesis. -- Semi-decision tactic "jp" for first-order intuitionistic logic moved to user +- Semi-decision tactic "jp" for first-order intuitionistic logic moved to user contributions (subsumed by "firstorder"). Program - Moved useful tactics in theories/Program and documented them. -- Add Program.Basics which contains standard definitions for functional +- Add Program.Basics which contains standard definitions for functional programming (id, apply, flip...) - More robust obligation handling, dependent pattern-matching and well-founded definitions. - New syntax " dest term as pat in term " for destructing objects using - an irrefutable pattern while keeping equalities (use this instead of + an irrefutable pattern while keeping equalities (use this instead of "let" in Programs). -- Program CoFixpoint is accepted, Program Fixpoint uses the new way to infer +- Program CoFixpoint is accepted, Program Fixpoint uses the new way to infer which argument decreases structurally. -- Program Lemma, Axiom etc... now permit to have obligations in the statement +- Program Lemma, Axiom etc... now permit to have obligations in the statement iff they can be automatically solved by the default tactic. - Renamed "Obligations Tactic" command to "Obligation Tactic". - New command "Preterm [ of id ]" to see the actual term fed to Coq for debugging purposes. -- New option "Transparent Obligations" to control the declaration of - obligations as transparent or opaque. All obligations are now transparent +- New option "Transparent Obligations" to control the declaration of + obligations as transparent or opaque. All obligations are now transparent by default, otherwise the system declares them opaque if possible. -- Changed the notations "left" and "right" to "in_left" and "in_right" to hide - the proofs in standard disjunctions, to avoid breaking existing scripts when +- Changed the notations "left" and "right" to "in_left" and "in_right" to hide + the proofs in standard disjunctions, to avoid breaking existing scripts when importing Program. Also, put them in program_scope. Type Classes - New "Class", "Instance" and "Program Instance" commands to define - classes and instances documented in the reference manual. -- New binding construct " [ Class_1 param_1 .. param_n, Class_2 ... ] " - for binding type classes, usable everywhere. + classes and instances documented in the reference manual. +- New binding construct " [ Class_1 param_1 .. param_n, Class_2 ... ] " + for binding type classes, usable everywhere. - New command " Print Classes " and " Print Instances some_class " to - print tables for typeclasses. + print tables for typeclasses. - New default eauto hint database "typeclass_instances" used by the default - typeclass instance search tactic. -- New theories directory "theories/Classes" for standard typeclasses - declarations. Module Classes.RelationClasses is a typeclass port of - Relation_Definitions plus a generic development of algebra on + typeclass instance search tactic. +- New theories directory "theories/Classes" for standard typeclasses + declarations. Module Classes.RelationClasses is a typeclass port of + Relation_Definitions plus a generic development of algebra on n-ary heterogeneous predicates. - + Setoid rewriting - Complete (and still experimental) rewrite of the tactic @@ -740,19 +745,19 @@ Setoid rewriting - "-->", "++>" and "==>" are now right associative notations declared at level 55 in scope signature_scope. - Their introduction may break existing scripts that defined + Their introduction may break existing scripts that defined them as notations with different levels. - + - One needs to use [Typeclasses unfold [cst]] if [cst] is used as an abbreviation hiding products in types of morphisms, - e.g. if ones redefines [relation] and declares morphisms + e.g. if ones redefines [relation] and declares morphisms whose type mentions [relation]. - The [setoid_rewrite]'s semantics change when rewriting with a lemma: it can rewrite two different instantiations of the lemma at once. Use [setoid_rewrite H at 1] for (almost) the usual semantics. [setoid_rewrite] will also try to rewrite under binders now, and can - succeed on different terms than before. In particular, it will unify under + succeed on different terms than before. In particular, it will unify under let-bound variables. When called through [rewrite], the semantics are unchanged though. @@ -767,7 +772,7 @@ Setoid rewriting - Setoid_Theory is now an alias to Equivalence, scripts building objects of type Setoid_Theory need to unfold (or "red") the definitions - of Reflexive, Symmetric and Transitive in order to get the same goals + of Reflexive, Symmetric and Transitive in order to get the same goals as before. Scripts which introduced variables explicitely will not break. - The order of subgoals when doing [setoid_rewrite] with side-conditions @@ -775,7 +780,7 @@ Setoid rewriting - New standard library modules Classes.Morphisms declares standard morphisms on refl/sym/trans relations. - Classes.Morphisms_Prop declares morphisms on propositional + Classes.Morphisms_Prop declares morphisms on propositional connectives and Classes.Morphisms_Relations on generalized predicate connectives. Classes.Equivalence declares notations and tactics related to equivalences and Classes.SetoidTactics defines the @@ -787,30 +792,30 @@ Setoid rewriting and rewriting under binders. The tactic is also extensible entirely in Ltac. The documentation has been updated to cover these features. -- [setoid_rewrite] and [rewrite] now support the [at] modifier to select +- [setoid_rewrite] and [rewrite] now support the [at] modifier to select occurrences to rewrite, and both use the [setoid_rewrite] code, even when rewriting with leibniz equality if occurrences are specified. Extraction -- Improved behavior of the Caml extraction of modules: name clashes should - not happen anymore. +- Improved behavior of the Caml extraction of modules: name clashes should + not happen anymore. - The command Extract Inductive has now a syntax for infix notations. This - allows in particular to map Coq lists and pairs onto Caml ones: + allows in particular to map Coq lists and pairs onto Caml ones: Extract Inductive list => list [ "[]" "(::)" ]. Extract Inductive prod => "(*)" [ "(,)" ]. -- In pattern matchings, a default pattern "| _ -> ..." is now used whenever +- In pattern matchings, a default pattern "| _ -> ..." is now used whenever possible if several branches are identical. For instance, functions - corresponding to decidability of equalities are now linear instead of + corresponding to decidability of equalities are now linear instead of quadratic. - A new instruction Extraction Blacklist id1 .. idn allows to prevent filename conflits with existing code, for instance when extracting module List - to Ocaml. + to Ocaml. CoqIDE - CoqIDE font defaults to monospace so as indentation to be meaningful. -- CoqIDE supports nested goals and any other kind of declaration in the middle +- CoqIDE supports nested goals and any other kind of declaration in the middle of a proof. - Undoing non-tactic commands in CoqIDE works faster. - New CoqIDE menu for activating display of various implicit informations. @@ -824,8 +829,8 @@ Tools - Extended -I coqtop/coqc option to specify a logical dir: "-I dir -as coqdir". - New coqtop/coqc option -exclude-dir to exclude subdirs for option -R. - The binary "parser" has been renamed to "coq-parser". -- Improved coqdoc and dump of globalization information to give more - meta-information on identifiers. All categories of Coq definitions are +- Improved coqdoc and dump of globalization information to give more + meta-information on identifiers. All categories of Coq definitions are supported, which makes typesetting trivial in the generated documentation. Support for hyperlinking and indexing developments in the tex output has been implemented as well. @@ -861,8 +866,8 @@ Tactics 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 +- 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 @@ -901,7 +906,7 @@ Tactics - 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). +- 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. @@ -926,7 +931,7 @@ Logic 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 +- 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 @@ -951,7 +956,7 @@ Ltac and tactic syntactic extensions - 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 + 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. @@ -968,14 +973,14 @@ Tactics - 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 + 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 + 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 ... 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". @@ -986,19 +991,19 @@ Tactics (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, +- 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 +- 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 +- 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. -- Introduction patterns now support side hypotheses (e.g. intros [|] on +- Introduction patterns now support side hypotheses (e.g. intros [|] on "(nat -> nat) -> nat" works). - New introduction patterns "->" and "<-" for immediate rewriting of introduced hypotheses. @@ -1019,20 +1024,20 @@ Tactics - 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 +- 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 + * 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 + * 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 _ + +- All type parts should now disappear instead of sometimes producing _ (for instance in Map.empty). -- Haskell extraction: types of functions are now printed, better +- 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. @@ -1073,7 +1078,7 @@ Libraries 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 Acc_iter and +- More lemmas stated on Type in Wf.v, removal of redundant Acc_iter and Acc_iter2. - Change of the internal names of lemmas in OmegaLemmas. - Acc in Wf.v and clos_refl_trans in Relation_Operators.v now rely on @@ -1085,17 +1090,17 @@ Libraries 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 +- 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 +- 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 +- 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 @@ -1126,7 +1131,7 @@ Vernacular commands New syntax -- Semantics change of the if-then-else construction in 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; @@ -1148,7 +1153,7 @@ 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 +- XML exportation tool now exports the structure of vernacular files (cf chapter 13 in the reference manual) User contributions @@ -1165,7 +1170,7 @@ 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 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 @@ -1185,7 +1190,7 @@ Syntax extensions Revision of the standard library -- Many lemmas and definitions names have been made more uniform mostly +- 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") @@ -1233,7 +1238,7 @@ Known problems of the automatic translation 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 ======================================== @@ -1301,7 +1306,7 @@ Grammar extensions Library - New file about the factorial function in Arith -- An additional elimination Acc_iter for Acc, simplier than Acc_rect. +- 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 @@ -1313,7 +1318,7 @@ Library - 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 + - 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, @@ -1368,10 +1373,10 @@ Tactics Extraction (See details in plugins/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. + 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 @@ -1397,7 +1402,7 @@ Incompatibilities 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 +- 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 @@ -1412,14 +1417,14 @@ Symbolic notations - 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 +- "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 + longer supported; some incompatibilities in Grammar: when a syntax is a initial segment of an other one, Grammar does not work, use Notation Library @@ -1497,7 +1502,7 @@ Tactics 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 +- "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) @@ -1508,7 +1513,7 @@ Tactics Extraction (See details in plugins/extraction/CHANGES and README): - An experimental Scheme extraction is provided. -- Concerning Ocaml, extracted code is now ensured to always type-check, +- 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. @@ -1538,7 +1543,7 @@ Incompatibilities 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 + 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 @@ -1577,7 +1582,7 @@ Bug fixes Misc - Ocaml version >= 3.06 is needed to compile Coq from sources - - Simplification of fresh names creation strategy for Assert, Pose and + - Simplification of fresh names creation strategy for Assert, Pose and LetTac (PR#192) Changes from V7.2 to V7.3 @@ -1607,7 +1612,7 @@ Tactics - 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 +- "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 @@ -1623,7 +1628,7 @@ Bugs Extraction (details in plugins/extraction/CHANGES or documentation) - Signatures of extracted terms are now mostly expunged from dummy arguments. -- Haskell extraction is now operational (tested & debugged). +- Haskell extraction is now operational (tested & debugged). Standard library @@ -1635,8 +1640,8 @@ Standard library 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) +- 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 @@ -1645,7 +1650,7 @@ User Contributions - 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 +- 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 @@ -1681,7 +1686,7 @@ Language 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 + 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 @@ -1693,14 +1698,14 @@ Tactics Extraction (details in plugins/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. +- 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 [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 @@ -1905,7 +1910,7 @@ Changes in existing tactics an elimination schema, use "Elim <hyp> using <name of the new schema>" (*)(+) -- Simpl no longer unfolds the recursive calls of a mutually defined +- Simpl no longer unfolds the recursive calls of a mutually defined fixpoint (*)(+) - Intro now fails if the hypothesis name already exists (*)(+) @@ -1955,7 +1960,7 @@ Concrete syntax of constructions Parsing and grammar extension ----------------------------- -- More constraints when writing ast +- More constraints when writing ast - "{...}" and the macros $LIST, $VAR, etc. now expect a metavariable (an identifier starting with $) (*) @@ -2011,7 +2016,7 @@ Changes in existing commands ---------------------------- - Generalization of the usage of qualified identifiers in tactics - and commands about globals, e.g. Decompose, Eval Delta; + and commands about globals, e.g. Decompose, Eval Delta; Hints Unfold, Transparent, Require - Require synchronous with Reset; Require's scope stops at Section ending (*) @@ -2110,8 +2115,8 @@ New user contributions - 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) +- 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 diff --git a/Makefile.common b/Makefile.common index 26484fcdd..95063aa2f 100644 --- a/Makefile.common +++ b/Makefile.common @@ -1,4 +1,3 @@ - ####################################################################### # v # The Coq Proof Assistant / The Coq Development Team # # <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay # @@ -265,6 +264,7 @@ NARITHVO:=$(call cat_vo_itarget, theories/NArith) ZARITHVO:=$(call cat_vo_itarget, theories/ZArith) QARITHVO:=$(call cat_vo_itarget, theories/QArith) LISTSVO:=$(call cat_vo_itarget, theories/Lists) +VECTORSVO:=$(call cat_vo_itarget, theories/Vectors) STRINGSVO:=$(call cat_vo_itarget, theories/Strings) SETSVO:=$(call cat_vo_itarget, theories/Sets) FSETSVO:=$(call cat_vo_itarget, theories/FSets) @@ -282,7 +282,8 @@ THEORIESVO:=\ $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(PARITHVO) $(NARITHVO) $(ZARITHVO) \ $(SETOIDSVO) $(LISTSVO) $(STRINGSVO) $(SETSVO) $(FSETSVO) $(MSETSVO) \ $(RELATIONSVO) $(WELLFOUNDEDVO) $(REALSVO) $(SORTINGVO) $(QARITHVO) \ - $(NUMBERSVO) $(UNICODEVO) $(CLASSESVO) $(PROGRAMVO) $(STRUCTURESVO) + $(NUMBERSVO) $(UNICODEVO) $(CLASSESVO) $(PROGRAMVO) $(STRUCTURESVO) \ + $(VECTORSVO) THEORIESLIGHTVO:= $(INITVO) $(LOGICVO) $(ARITHVO) diff --git a/theories/Arith/Bool_nat.v b/theories/Arith/Bool_nat.v index 08a090325..f384e1488 100644 --- a/theories/Arith/Bool_nat.v +++ b/theories/Arith/Bool_nat.v @@ -34,4 +34,4 @@ Definition nat_noteq_bool x y := bool_of_sumbool (sumbool_not _ _ (eq_nat_dec x y)). Definition zerop_bool x := bool_of_sumbool (zerop x). -Definition notzerop_bool x := bool_of_sumbool (notzerop x).
\ No newline at end of file +Definition notzerop_bool x := bool_of_sumbool (notzerop x). diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v index c6bf35bb0..c9e6d3cf3 100644 --- a/theories/Arith/Compare.v +++ b/theories/Arith/Compare.v @@ -50,4 +50,4 @@ Qed. Require Export Wf_nat. -Require Export Min Max.
\ No newline at end of file +Require Export Min Max. diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v index 2b2cf860d..bcfbe0efe 100644 --- a/theories/Arith/Min.v +++ b/theories/Arith/Min.v @@ -39,4 +39,4 @@ Definition min_glb := Nat.min_glb. (* Compatibility *) Notation min_case2 := min_case (only parsing). Notation min_SS := Nat.succ_min_distr (only parsing). -(* end hide *)
\ No newline at end of file +(* end hide *) diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index 9e3823d7a..6eb667c11 100644 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -7,7 +7,8 @@ (************************************************************************) Require Import Decidable. - +Require Eqdep_dec. +Require Import Le Lt. Open Local Scope nat_scope. Implicit Types m n x y : nat. @@ -30,3 +31,22 @@ Hint Resolve O_or_S eq_nat_dec: arith. Theorem dec_eq_nat : forall n m, decidable (n = m). intros x y; unfold decidable in |- *; elim (eq_nat_dec x y); auto with arith. Defined. + +Definition UIP_nat:= Eqdep_dec.UIP_dec eq_nat_dec. + +Lemma le_unique: forall m n (h1 h2: m <= n), h1 = h2. +Proof. +fix 3. +refine (fun m _ h1 => match h1 as h' in _ <= k return forall hh: m <= k, h' = hh + with le_n => _ |le_S i H => _ end). +refine (fun hh => match hh as h' in _ <= k return forall eq: m = k, + le_n m = match eq in _ = p return m <= p -> m <= m with |eq_refl => fun bli => bli end h' with + |le_n => fun eq => _ |le_S j H' => fun eq => _ end eq_refl). +rewrite (UIP_nat _ _ eq eq_refl). reflexivity. +subst m. destruct (Lt.lt_irrefl j H'). +refine (fun hh => match hh as h' in _ <= k return match k as k' return m <= k' -> Prop + with |0 => fun _ => True |S i' => fun h'' => forall H':m <= i', le_S m i' H' = h'' end h' + with |le_n => _ |le_S j H2 => fun H' => _ end H). +destruct m. exact I. intros; destruct (Lt.lt_irrefl m H'). +f_equal. apply le_unique. +Qed. diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v index 48d730319..eb2d4df4c 100644 --- a/theories/Arith/Plus.v +++ b/theories/Arith/Plus.v @@ -24,17 +24,10 @@ Open Local Scope nat_scope. Implicit Types m n p q : nat. -(** * Zero is neutral *) - -Lemma plus_0_l : forall n, 0 + n = n. -Proof. - reflexivity. -Qed. - -Lemma plus_0_r : forall n, n + 0 = n. -Proof. - intro; symmetry in |- *; apply plus_n_O. -Qed. +(** * Zero is neutral +Deprecated : Already in Init/Peano.v *) +Definition plus_0_l n := eq_sym (plus_O_n n). +Definition plus_0_r n := eq_sym (plus_n_O n). (** * Commutativity *) @@ -47,14 +40,8 @@ Hint Immediate plus_comm: arith v62. (** * Associativity *) -Lemma plus_Snm_nSm : forall n m, S n + m = n + S m. -Proof. - intros. - simpl in |- *. - rewrite (plus_comm n m). - rewrite (plus_comm n (S m)). - trivial with arith. -Qed. +Definition plus_Snm_nSm : forall n m, S n + m = n + S m:= + plus_n_Sm. Lemma plus_assoc : forall n m p, n + (m + p) = n + m + p. Proof. diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index 694ed15b4..0c2181638 100644 --- a/theories/Bool/Bvector.v +++ b/theories/Bool/Bvector.v @@ -9,6 +9,8 @@ (** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *) Require Export Bool Sumbool. +Require Vector. +Export Vector.VectorNotations. Require Import Minus. Open Local Scope nat_scope. @@ -27,161 +29,6 @@ as definition, since the type inference mechanism for pattern-matching is sometimes weaker that the one implemented for elimination tactiques. *) -Section VECTORS. - -(** -A vector is a list of size n whose elements belongs to a set A. -If the size is non-zero, we can extract the first component and the -rest of the vector, as well as the last component, or adding or -removing a component (carry) or repeating the last component at the -end of the vector. -We can also truncate the vector and remove its p last components or -reciprocally extend the vector by concatenation. -A unary function over A generates a function on vectors of size n by -applying f pointwise. -A binary function over A generates a function on pairs of vectors of -size n by applying f pointwise. -*) - -Variable A : Type. - -Inductive vector : nat -> Type := - | Vnil : vector 0 - | Vcons : forall (a:A) (n:nat), vector n -> vector (S n). - -Definition Vhead (n:nat) (v:vector (S n)) := - match v with - | Vcons a _ _ => a - end. - -Definition Vtail (n:nat) (v:vector (S n)) := - match v with - | Vcons _ _ v => v - end. - -Definition Vlast : forall n:nat, vector (S n) -> A. -Proof. - induction n as [| n f]; intro v. - inversion v. - exact a. - - inversion v as [| n0 a H0 H1]. - exact (f H0). -Defined. - -Fixpoint Vconst (a:A) (n:nat) := - match n return vector n with - | O => Vnil - | S n => Vcons a _ (Vconst a n) - end. - -(** Shifting and truncating *) - -Lemma Vshiftout : forall n:nat, vector (S n) -> vector n. -Proof. - induction n as [| n f]; intro v. - exact Vnil. - - inversion v as [| a n0 H0 H1]. - exact (Vcons a n (f H0)). -Defined. - -Lemma Vshiftin : forall n:nat, A -> vector n -> vector (S n). -Proof. - induction n as [| n f]; intros a v. - exact (Vcons a 0 v). - - inversion v as [| a0 n0 H0 H1 ]. - exact (Vcons a0 (S n) (f a H0)). -Defined. - -Lemma Vshiftrepeat : forall n:nat, vector (S n) -> vector (S (S n)). -Proof. - induction n as [| n f]; intro v. - inversion v. - exact (Vcons a 1 v). - - inversion v as [| a n0 H0 H1 ]. - exact (Vcons a (S (S n)) (f H0)). -Defined. - -Lemma Vtrunc : forall n p:nat, n > p -> vector n -> vector (n - p). -Proof. - induction p as [| p f]; intros H v. - rewrite <- minus_n_O. - exact v. - - apply (Vshiftout (n - S p)). - - rewrite minus_Sn_m. - apply f. - auto with *. - exact v. - auto with *. -Defined. - -(** Concatenation of two vectors *) - -Fixpoint Vextend n p (v:vector n) (w:vector p) : vector (n+p) := - match v with - | Vnil => w - | Vcons a n' v' => Vcons a (n'+p) (Vextend n' p v' w) - end. - -(** Uniform application on the arguments of the vector *) - -Variable f : A -> A. - -Fixpoint Vunary n (v:vector n) : vector n := - match v with - | Vnil => Vnil - | Vcons a n' v' => Vcons (f a) n' (Vunary n' v') - end. - -Variable g : A -> A -> A. - -Lemma Vbinary : forall n:nat, vector n -> vector n -> vector n. -Proof. - induction n as [| n h]; intros v v0. - exact Vnil. - - inversion v as [| a n0 H0 H1]; inversion v0 as [| a0 n1 H2 H3]. - exact (Vcons (g a a0) n (h H0 H2)). -Defined. - -(** Eta-expansion of a vector *) - -Definition Vid n : vector n -> vector n := - match n with - | O => fun _ => Vnil - | _ => fun v => Vcons (Vhead _ v) _ (Vtail _ v) - end. - -Lemma Vid_eq : forall (n:nat) (v:vector n), v = Vid n v. -Proof. - destruct v; auto. -Qed. - -Lemma VSn_eq : - forall (n : nat) (v : vector (S n)), v = Vcons (Vhead _ v) _ (Vtail _ v). -Proof. - intros. - exact (Vid_eq _ v). -Qed. - -Lemma V0_eq : forall (v : vector 0), v = Vnil. -Proof. - intros. - exact (Vid_eq _ v). -Qed. - -End VECTORS. - -(* suppressed: incompatible with Coq-Art book -Implicit Arguments Vnil [A]. -Implicit Arguments Vcons [A n]. -*) - Section BOOLEAN_VECTORS. (** @@ -197,38 +44,38 @@ NOTA BENE: all shift operations expect predecessor of size as parameter (they only work on non-empty vectors). *) -Definition Bvector := vector bool. +Definition Bvector := Vector.t bool. -Definition Bnil := @Vnil bool. +Definition Bnil := @Vector.nil bool. -Definition Bcons := @Vcons bool. +Definition Bcons := @Vector.cons bool. -Definition Bvect_true := Vconst bool true. +Definition Bvect_true := Vector.const true. -Definition Bvect_false := Vconst bool false. +Definition Bvect_false := Vector.const false. -Definition Blow := Vhead bool. +Definition Blow := @Vector.hd bool. -Definition Bhigh := Vtail bool. +Definition Bhigh := @Vector.tl bool. -Definition Bsign := Vlast bool. +Definition Bsign := @Vector.last bool. -Definition Bneg := Vunary bool negb. +Definition Bneg n (v : Bvector n) := Vector.map negb v. -Definition BVand := Vbinary bool andb. +Definition BVand n (v : Bvector n) := Vector.map2 andb v. -Definition BVor := Vbinary bool orb. +Definition BVor n (v : Bvector n) := Vector.map2 orb v. -Definition BVxor := Vbinary bool xorb. +Definition BVxor n (v : Bvector n) := Vector.map2 xorb v. Definition BshiftL (n:nat) (bv:Bvector (S n)) (carry:bool) := - Bcons carry n (Vshiftout bool n bv). + Bcons carry n (Vector.shiftout bv). Definition BshiftRl (n:nat) (bv:Bvector (S n)) (carry:bool) := - Bhigh (S n) (Vshiftin bool (S n) carry bv). + Bhigh (S n) (Vector.shiftin carry bv). Definition BshiftRa (n:nat) (bv:Bvector (S n)) := - Bhigh (S n) (Vshiftrepeat bool n bv). + Bhigh (S n) (Vector.shiftrepeat bv). Fixpoint BshiftL_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) := match p with @@ -250,5 +97,3 @@ Fixpoint BshiftRa_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) := End BOOLEAN_VECTORS. -Implicit Arguments Vcons [[A] [n]] []. -Implicit Arguments Vnil [[A]] []. diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v index 6550a4955..6872eaea3 100644 --- a/theories/Bool/IfProp.v +++ b/theories/Bool/IfProp.v @@ -45,4 +45,4 @@ Lemma IfProp_sum : forall (A B:Prop) (b:bool), IfProp A B b -> {A} + {B}. destruct b; intro H. left; inversion H; auto with bool. right; inversion H; auto with bool. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v index 942607faf..73a092143 100644 --- a/theories/Bool/Sumbool.v +++ b/theories/Bool/Sumbool.v @@ -66,4 +66,4 @@ Definition bool_of_sumbool : intros A B H. elim H; intro; [exists true | exists false]; assumption. Defined. -Implicit Arguments bool_of_sumbool.
\ No newline at end of file +Implicit Arguments bool_of_sumbool. diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v index a7c739625..bac4c0d69 100644 --- a/theories/Bool/Zerob.v +++ b/theories/Bool/Zerob.v @@ -37,4 +37,4 @@ Hint Resolve zerob_false_intro: bool. Lemma zerob_false_elim : forall n:nat, zerob n = false -> n <> 0. Proof. destruct n; [ inversion 1 | auto with bool ]. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v index 2b7fe88bf..a001f2e92 100644 --- a/theories/Classes/Init.v +++ b/theories/Classes/Init.v @@ -34,4 +34,4 @@ Ltac unconvertible := | |- _ => exact tt end. -Hint Extern 0 (@Unconvertible _ _ _) => unconvertible : typeclass_instances.
\ No newline at end of file +Hint Extern 0 (@Unconvertible _ _ _) => unconvertible : typeclass_instances. diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index f449d8383..216ca35af 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -50,13 +50,7 @@ Qed. (** Injectivity of successor *) -Theorem eq_add_S : forall n m:nat, S n = S m -> n = m. -Proof. - intros n m Sn_eq_Sm. - replace (n=m) with (pred (S n) = pred (S m)) by auto using pred_Sn. - rewrite Sn_eq_Sm; trivial. -Qed. - +Definition eq_add_S n m (H: S n = S m): n = m := f_equal pred H. Hint Immediate eq_add_S: core. Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m. diff --git a/theories/Logic/SetIsType.v b/theories/Logic/SetIsType.v index ff9ec7f69..f0876fbcd 100644 --- a/theories/Logic/SetIsType.v +++ b/theories/Logic/SetIsType.v @@ -14,4 +14,4 @@ Set: simply insert some Require Export of this file at starting points of the development and try to recompile... *) -Notation "'Set'" := Type (only parsing).
\ No newline at end of file +Notation "'Set'" := Type (only parsing). diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index 0dd2fceaa..5b3157143 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -710,7 +710,8 @@ Lemma Nneg_bit0 : Nbit0 (Nxor a a') = true -> Nbit0 a = negb (Nbit0 a'). Proof. intros. - rewrite <- true_xorb, <- H, Nxor_bit0, xorb_assoc, xorb_nilpotent, xorb_false. + rewrite <- true_xorb, <- H, Nxor_bit0, xorb_assoc, + xorb_nilpotent, xorb_false. reflexivity. Qed. @@ -733,7 +734,8 @@ Lemma Nsame_bit0 : Proof. intros. rewrite <- (xorb_false (Nbit0 a)). assert (H0: Nbit0 (Npos (xO p)) = false) by reflexivity. - rewrite <- H0, <- H, Nxor_bit0, <- xorb_assoc, xorb_nilpotent, false_xorb. reflexivity. + rewrite <- H0, <- H, Nxor_bit0, <- xorb_assoc, xorb_nilpotent, false_xorb. + reflexivity. Qed. (** a lexicographic order on bits, starting from the lowest bit *) @@ -840,8 +842,8 @@ Lemma Nless_trans : Nless a a' = true -> Nless a' a'' = true -> Nless a a'' = true. Proof. induction a as [|a IHa|a IHa] using N_ind_double; intros a' a'' H H0. - destruct (Nless N0 a'') as []_eqn:Heqb. trivial. - rewrite (N0_less_2 a'' Heqb), (Nless_z a') in H0. discriminate H0. + case_eq (Nless N0 a'') ; intros Heqn. trivial. + rewrite (N0_less_2 a'' Heqn), (Nless_z a') in H0. discriminate H0. induction a' as [|a' _|a' _] using N_ind_double. rewrite (Nless_z (Ndouble a)) in H. discriminate H. rewrite (Nless_def_1 a a') in H. @@ -868,10 +870,10 @@ Lemma Nless_total : forall a a', {Nless a a' = true} + {Nless a' a = true} + {a = a'}. Proof. induction a using N_rec_double; intro a'. - destruct (Nless N0 a') as []_eqn:Heqb. left. left. auto. + case_eq (Nless N0 a') ; intros Heqb. left. left. auto. right. rewrite (N0_less_2 a' Heqb). reflexivity. induction a' as [|a' _|a' _] using N_rec_double. - destruct (Nless N0 (Ndouble a)) as []_eqn:Heqb. left. right. auto. + case_eq (Nless N0 (Ndouble a)) ; intros Heqb. left. right. auto. right. exact (N0_less_2 _ Heqb). rewrite 2!Nless_def_1. destruct (IHa a') as [ | ->]. left. assumption. @@ -910,9 +912,9 @@ Definition N2Bv (n:N) : Bvector (Nsize n) := Fixpoint Bv2N (n:nat)(bv:Bvector n) : N := match bv with - | Vnil => N0 - | Vcons false n bv => Ndouble (Bv2N n bv) - | Vcons true n bv => Ndouble_plus_one (Bv2N n bv) + | Vector.nil => N0 + | Vector.cons false n bv => Ndouble (Bv2N n bv) + | Vector.cons true n bv => Ndouble_plus_one (Bv2N n bv) end. Lemma Bv2N_N2Bv : forall n, Bv2N _ (N2Bv n) = n. @@ -928,13 +930,12 @@ Qed. Lemma Bv2N_Nsize : forall n (bv:Bvector n), Nsize (Bv2N n bv) <= n. Proof. -induction n; intros. -rewrite (V0_eq _ bv); simpl; auto. -rewrite (VSn_eq _ _ bv); simpl. -specialize IHn with (Vtail _ _ bv). -destruct (Vhead _ _ bv); - destruct (Bv2N n (Vtail bool n bv)); - simpl; auto with arith. +induction bv; intros. +auto. +simpl. +destruct h; + destruct (Bv2N n bv); + simpl ; auto with arith. Qed. (** In the previous lemma, we can only replace the inequality by @@ -944,15 +945,10 @@ Lemma Bv2N_Nsize_1 : forall n (bv:Bvector (S n)), Bsign _ bv = true <-> Nsize (Bv2N _ bv) = (S n). Proof. -induction n; intro. -rewrite (VSn_eq _ _ bv); simpl. -rewrite (V0_eq _ (Vtail _ _ bv)); simpl. -destruct (Vhead _ _ bv); simpl; intuition; try discriminate. -rewrite (VSn_eq _ _ bv); simpl. -generalize (IHn (Vtail _ _ bv)); clear IHn. -destruct (Vhead _ _ bv); - destruct (Bv2N (S n) (Vtail bool (S n) bv)); - simpl; intuition; try discriminate. +apply Vector.rectS ; intros ; simpl. +destruct a ; compute ; split ; intros x ; now inversion x. + destruct a, (Bv2N (S n) v) ; + simpl ;intuition ; try discriminate. Qed. (** To state nonetheless a second result about composition of @@ -982,7 +978,7 @@ Qed. [a] plus some zeros. *) Lemma N2Bv_N2Bv_gen_above : forall (a:N)(k:nat), - N2Bv_gen (Nsize a + k) a = Vextend _ _ _ (N2Bv a) (Bvect_false k). + N2Bv_gen (Nsize a + k) a = Vector.append (N2Bv a) (Bvect_false k). Proof. destruct a; simpl. destruct k; simpl; auto. @@ -994,13 +990,13 @@ Qed. Lemma N2Bv_Bv2N : forall n (bv:Bvector n), N2Bv_gen n (Bv2N n bv) = bv. Proof. -induction n; intros. -rewrite (V0_eq _ bv); simpl; auto. -rewrite (VSn_eq _ _ bv); simpl. -generalize (IHn (Vtail _ _ bv)); clear IHn. +induction bv; intros. +auto. +simpl. +generalize IHbv; clear IHbv. unfold Bcons. -destruct (Bv2N _ (Vtail _ _ bv)); - destruct (Vhead _ _ bv); intro H; rewrite <- H; simpl; trivial; +destruct (Bv2N _ bv); + destruct h; intro H; rewrite <- H; simpl; trivial; induction n; simpl; auto. Qed. @@ -1009,31 +1005,25 @@ Qed. Lemma Nbit0_Blow : forall n, forall (bv:Bvector (S n)), Nbit0 (Bv2N _ bv) = Blow _ bv. Proof. +apply Vector.caseS. intros. unfold Blow. -rewrite (VSn_eq _ _ bv) at 1. simpl. -destruct (Bv2N n (Vtail bool n bv)); simpl; - destruct (Vhead bool n bv); auto. +destruct (Bv2N n t); simpl; + destruct h; auto. Qed. -Definition Bnth (n:nat)(bv:Bvector n)(p:nat) : p<n -> bool. -Proof. - induction bv in p |- *. - intros. - exfalso; inversion H. - intros. - destruct p. - exact a. - apply (IHbv p); auto with arith. -Defined. +Notation Bnth := (@Vector.nth_order bool). Lemma Bnth_Nbit : forall n (bv:Bvector n) p (H:p<n), - Bnth _ bv p H = Nbit (Bv2N _ bv) p. + Bnth bv H = Nbit (Bv2N _ bv) p. Proof. induction bv; intros. inversion H. -destruct p; simpl; destruct (Bv2N n bv); destruct a; simpl in *; auto. +destruct p ; simpl. + destruct (Bv2N n bv); destruct h; simpl in *; auto. + specialize IHbv with p (lt_S_n _ _ H). + simpl in * ; destruct (Bv2N n bv); destruct h; simpl in *; auto. Qed. Lemma Nbit_Nsize : forall n p, Nsize n <= p -> Nbit n p = false. @@ -1045,12 +1035,12 @@ inversion H. inversion H. Qed. -Lemma Nbit_Bth: forall n p (H:p < Nsize n), Nbit n p = Bnth _ (N2Bv n) p H. +Lemma Nbit_Bth: forall n p (H:p < Nsize n), Nbit n p = Bnth (N2Bv n) H. Proof. destruct n as [|n]. inversion H. -induction n; simpl in *; intros; destruct p; auto with arith. -inversion H; inversion H1. +induction n ; destruct p ; unfold Vector.nth_order in *; simpl in * ; auto. +intros H ; destruct (lt_n_O _ (lt_S_n _ _ H)). Qed. (** Binary bitwise operations are the same in the two worlds. *) @@ -1058,35 +1048,17 @@ Qed. Lemma Nxor_BVxor : forall n (bv bv' : Bvector n), Bv2N _ (BVxor _ bv bv') = Nxor (Bv2N _ bv) (Bv2N _ bv'). Proof. -induction n; intros bv bv'. -rewrite (V0_eq _ bv), (V0_eq _ bv'); simpl; auto. -rewrite (VSn_eq _ _ bv), (VSn_eq _ _ bv'); simpl; auto. -rewrite IHn. -destruct (Vhead bool n bv), (Vhead bool n bv'), - (Bv2N n (Vtail bool n bv)), (Bv2N n (Vtail bool n bv')); - simpl; auto. -Qed. - -Lemma Nor_BVor : forall n (bv bv' : Bvector n), - Bv2N _ (BVor _ bv bv') = Nor (Bv2N _ bv) (Bv2N _ bv'). -Proof. -induction n; intros bv bv'. -rewrite (V0_eq _ bv), (V0_eq _ bv'); simpl; auto. -rewrite (VSn_eq _ _ bv), (VSn_eq _ _ bv'); simpl; auto. -rewrite IHn. -destruct (Vhead bool n bv), (Vhead bool n bv'), - (Bv2N n (Vtail bool n bv)), (Bv2N n (Vtail bool n bv')); - simpl; auto. +apply Vector.rect2 ; intros. +now simpl. +simpl. +destruct a, b, (Bv2N n v1), (Bv2N n v2); simpl in *; rewrite H ; now simpl. Qed. Lemma Nand_BVand : forall n (bv bv' : Bvector n), Bv2N _ (BVand _ bv bv') = Nand (Bv2N _ bv) (Bv2N _ bv'). Proof. -induction n; intros bv bv'. -rewrite (V0_eq _ bv), (V0_eq _ bv'); simpl; auto. -rewrite (VSn_eq _ _ bv), (VSn_eq _ _ bv'); simpl; auto. -rewrite IHn. -destruct (Vhead bool n bv), (Vhead bool n bv'), - (Bv2N n (Vtail bool n bv)), (Bv2N n (Vtail bool n bv')); +refine (Vector.rect2 _ _ _); simpl; intros; auto. +rewrite H. +destruct a, b, (Bv2N n v1), (Bv2N n v2); simpl; auto. Qed. diff --git a/theories/NArith/Ndist.v b/theories/NArith/Ndist.v index 9d399f5cd..22adc5050 100644 --- a/theories/NArith/Ndist.v +++ b/theories/NArith/Ndist.v @@ -333,4 +333,4 @@ Proof. intro. rewrite <- H. apply Nplength_ultra. rewrite Nxor_assoc. rewrite <- (Nxor_assoc a'' a'' a'). rewrite Nxor_nilpotent. rewrite Nxor_neutral_left. reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v index 43aafe24b..20016281a 100644 --- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v +++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -413,4 +413,4 @@ Qed. Lemma eqb_correct : forall x y, eqb x y = true -> x==y. Proof. now apply eqb_eq. Qed. -End CyclicRing.
\ No newline at end of file +End CyclicRing. diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index a5b537caa..1acdd17e5 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -1692,7 +1692,7 @@ Section Int31_Specs. unfold head031, recl. change On with (phi_inv (Z_of_nat (31-size))). replace (head031_alt size x) with - (head031_alt size x + (31 - size))%nat by (apply plus_0_r; auto). + (head031_alt size x + (31 - size))%nat by auto. assert (size <= 31)%nat by auto with arith. revert x H; induction size; intros. @@ -1800,7 +1800,7 @@ Section Int31_Specs. unfold tail031, recr. change On with (phi_inv (Z_of_nat (31-size))). replace (tail031_alt size x) with - (tail031_alt size x + (31 - size))%nat by (apply plus_0_r; auto). + (tail031_alt size x + (31 - size))%nat by auto. assert (size <= 31)%nat by auto with arith. revert x H; induction size; intros. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v index 788ca8e56..9981fab71 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSig.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v @@ -128,4 +128,4 @@ Module Type ZType_Notation (Import Z:ZType). Infix "<" := lt. End ZType_Notation. -Module Type ZType' := ZType <+ ZType_Notation.
\ No newline at end of file +Module Type ZType' := ZType <+ ZType_Notation. diff --git a/theories/Numbers/Rational/SpecViaQ/QSig.v b/theories/Numbers/Rational/SpecViaQ/QSig.v index de40f0704..2bdc1bba2 100644 --- a/theories/Numbers/Rational/SpecViaQ/QSig.v +++ b/theories/Numbers/Rational/SpecViaQ/QSig.v @@ -220,4 +220,4 @@ End QProperties. Module QTypeExt (Q : QType) <: QType <: TotalOrder <: HasCompare Q <: HasMinMax Q <: HasEqBool Q - := Q <+ QProperties.
\ No newline at end of file + := Q <+ QProperties. diff --git a/theories/PArith/Pminmax.v b/theories/PArith/Pminmax.v index 6fe6435a0..10eaa1608 100644 --- a/theories/PArith/Pminmax.v +++ b/theories/PArith/Pminmax.v @@ -123,4 +123,4 @@ Proof. apply plus_min_distr_l. Qed. -End P.
\ No newline at end of file +End P. diff --git a/theories/Program/Program.v b/theories/Program/Program.v index 8d7185828..14a7ffca7 100644 --- a/theories/Program/Program.v +++ b/theories/Program/Program.v @@ -11,4 +11,4 @@ Require Export Coq.Program.Equality. Require Export Coq.Program.Subset. Require Export Coq.Program.Basics. Require Export Coq.Program.Combinators. -Require Export Coq.Program.Syntax.
\ No newline at end of file +Require Export Coq.Program.Syntax. diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v index 1e1fcf935..d8176dc25 100644 --- a/theories/Program/Utils.v +++ b/theories/Program/Utils.v @@ -53,4 +53,4 @@ Extract Inductive bool => "bool" [ "true" "false" ]. Extract Inductive sumbool => "bool" [ "true" "false" ]. (* Extract Inductive prod "'a" "'b" => " 'a * 'b " [ "(,)" ]. *) (* Extract Inductive sigT => "prod" [ "" ]. *) -*)
\ No newline at end of file +*) diff --git a/theories/QArith/Qminmax.v b/theories/QArith/Qminmax.v index 01c6ab678..2da24ee6b 100644 --- a/theories/QArith/Qminmax.v +++ b/theories/QArith/Qminmax.v @@ -64,4 +64,4 @@ Proof. apply plus_min_distr_l. Qed. -End Q.
\ No newline at end of file +End Q. diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index 601c2549e..24f6d7204 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -208,4 +208,4 @@ intro; apply H; apply eqR_Qeq. rewrite H0; unfold Q2R in |- *; simpl in |- *; field; auto with real. Qed. -End LegacyQField.
\ No newline at end of file +End LegacyQField. diff --git a/theories/Reals/Integration.v b/theories/Reals/Integration.v index 2c69350d3..da1742ca6 100644 --- a/theories/Reals/Integration.v +++ b/theories/Reals/Integration.v @@ -8,4 +8,4 @@ Require Export NewtonInt. Require Export RiemannInt_SF. -Require Export RiemannInt.
\ No newline at end of file +Require Export RiemannInt. diff --git a/theories/Reals/Reals.v b/theories/Reals/Reals.v index 28d4a37cb..a15e9949d 100644 --- a/theories/Reals/Reals.v +++ b/theories/Reals/Reals.v @@ -27,4 +27,4 @@ Require Export Rfunctions. Require Export SeqSeries. Require Export Rtrigo. Require Export Ranalysis. -Require Export Integration.
\ No newline at end of file +Require Export Integration. diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index 65bf76c5f..5f8b5d9da 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -133,7 +133,7 @@ Section sequence. clear -Hi2pn. intros m. induction n. - rewrite plus_0_r. + rewrite<- plus_n_O. ring_simplify (sum m + (/ 2) ^ m - (/ 2) ^ m). split ; apply Rle_refl. rewrite <- plus_n_Sm. diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v index dfd029d96..d612e71ec 100644 --- a/theories/Sets/Cpo.v +++ b/theories/Sets/Cpo.v @@ -105,4 +105,4 @@ Section Specific_orders. {PO_of_chain : PO U; Chain_cond : Totally_ordered U PO_of_chain (Carrier_of U PO_of_chain)}. -End Specific_orders.
\ No newline at end of file +End Specific_orders. diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v index 0907d689b..24facb6f6 100644 --- a/theories/Sets/Image.v +++ b/theories/Sets/Image.v @@ -200,4 +200,4 @@ Section Image. End Image. -Hint Resolve Im_def image_empty finite_image: sets v62.
\ No newline at end of file +Hint Resolve Im_def image_empty finite_image: sets v62. diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v index f13ffd51a..a319b9832 100644 --- a/theories/Sets/Partial_Order.v +++ b/theories/Sets/Partial_Order.v @@ -97,4 +97,4 @@ Section Partial_order_facts. apply Strict_Rel_Transitive_with_Rel with (y := y); [ intuition | unfold Strict_Rel_of in H', H'0; intuition ]. Qed. -End Partial_order_facts.
\ No newline at end of file +End Partial_order_facts. diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v index 49c97251f..e28a12644 100644 --- a/theories/Sets/Permut.v +++ b/theories/Sets/Permut.v @@ -84,4 +84,4 @@ Section Axiomatisation. apply cong_left; apply perm_left. Qed. -End Axiomatisation.
\ No newline at end of file +End Axiomatisation. diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v index 8742d4c37..f8b24e747 100644 --- a/theories/Sets/Powerset.v +++ b/theories/Sets/Powerset.v @@ -185,4 +185,4 @@ Hint Resolve Union_increases_r: sets v62. Hint Resolve Intersection_decreases_l: sets v62. Hint Resolve Intersection_decreases_r: sets v62. Hint Resolve Empty_set_is_Bottom: sets v62. -Hint Resolve Strict_inclusion_is_transitive: sets v62.
\ No newline at end of file +Hint Resolve Strict_inclusion_is_transitive: sets v62. diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v index 9cfe37e59..a7fbb53da 100644 --- a/theories/Sets/Relations_1.v +++ b/theories/Sets/Relations_1.v @@ -62,4 +62,4 @@ End Relations_1. Hint Unfold Reflexive Transitive Antisymmetric Symmetric contains same_relation: sets v62. Hint Resolve Definition_of_preorder Definition_of_order - Definition_of_equivalence Definition_of_PER: sets v62.
\ No newline at end of file + Definition_of_equivalence Definition_of_PER: sets v62. diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v index 05e2fb80d..0c8329dd0 100644 --- a/theories/Sets/Relations_1_facts.v +++ b/theories/Sets/Relations_1_facts.v @@ -107,4 +107,4 @@ intros U R R' H' H'0; red in |- *. elim H'. intros H'1 H'2 x y z H'3 H'4; apply H'2. apply H'0 with y; auto with sets. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v index 8b4a20ff9..e7a69c99e 100644 --- a/theories/Sets/Relations_2.v +++ b/theories/Sets/Relations_2.v @@ -51,4 +51,4 @@ End Relations_2. Hint Resolve Rstar_0: sets v62. Hint Resolve Rstar1_0: sets v62. Hint Resolve Rstar1_1: sets v62. -Hint Resolve Rplus_0: sets v62.
\ No newline at end of file +Hint Resolve Rplus_0: sets v62. diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v index 13ec1e6c4..89b98c1f5 100644 --- a/theories/Sets/Relations_2_facts.v +++ b/theories/Sets/Relations_2_facts.v @@ -148,4 +148,4 @@ elim (H'3 t); auto with sets. intros z1 H'5; elim H'5; intros H'8 H'10; try exact H'8; clear H'5. exists z1; split; [ idtac | assumption ]. apply Rstar_n with t; auto with sets. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v index f48b9761e..8ac6e7fb4 100644 --- a/theories/Sets/Relations_3_facts.v +++ b/theories/Sets/Relations_3_facts.v @@ -166,4 +166,4 @@ generalize (H'2 v); intro h; lapply h; red in |- *; (exists z1; split); auto with sets. apply T with y1; auto with sets. apply T with t; auto with sets. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v index 119fcf803..bf1aaf8db 100644 --- a/theories/Sets/Uniset.v +++ b/theories/Sets/Uniset.v @@ -210,4 +210,4 @@ i*) End defs. -Unset Implicit Arguments.
\ No newline at end of file +Unset Implicit Arguments. diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v new file mode 100644 index 000000000..b90937a40 --- /dev/null +++ b/theories/Vectors/Fin.v @@ -0,0 +1,190 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Arith_base. + +(** [fin n] is a convinient way to represent \[1 .. n\] + +[fin n] can be seen as a n-uplet of unit where [F1] is the first element of +the n-uplet and [FS] set (n-1)-uplet of all the element but the first. + + Author: Pierre Boutillier + Institution: PPS, INRIA 12/2010 +*) + +Inductive t : nat -> Set := +|F1 : forall {n}, t (S n) +|FS : forall {n}, t n -> t (S n). + +Section SCHEMES. +Definition case0 {P} (p: t 0): P p := + match p as p' in t n return + match n as n' return t n' -> Type + with |0 => fun f0 => P f0 |S _ => fun _ => @ID end p' + with |F1 _ => @id |FS _ _ => @id end. + +Definition caseS (P: forall n, t (S n) -> Type) + (P1: forall n, P n F1) (PS : forall n (p: t n), P n (FS p)) + n (p: t (S n)): P n p := + match p as p0 in t n0 + return match n0 as nn return t nn -> Type with + |0 => fun _ => @ID |S n' => fun p' => P n' p' + end p0 with + |F1 k => P1 k + |FS k pp => PS k pp + end. + +Definition rectS (P: forall n, t (S n) -> Type) + (P1: forall n, P n F1) (PS : forall n (p: t (S n)), P n p -> P (S n) (FS p)): + forall n (p: t (S n)), P n p := +fix rectS_fix n (p: t (S n)): P n p:= + match p as p0 in t n0 + return match n0 as nn return t nn -> Type with + |0 => fun _ => @ID |S n' => fun p' => P n' p' + end p0 with + |F1 k => P1 k + |FS 0 pp => @case0 (fun f => P 0 (FS f)) pp + |FS (S k) pp => PS k pp (rectS_fix k pp) + end. + +Definition rect2 (P: forall {n} (a b: t n), Type) + (H0: forall n, P (S n) F1 F1) + (H1: forall n (f: t n), P (S n) F1 (FS f)) + (H2: forall n (f: t n), P (S n) (FS f) F1) + (HS: forall n (f g : t n), P n f g -> P (S n) (FS f) (FS g)): + forall n (a b: t n), P n a b := +fix rect2_fix n (a: t n): forall (b: t n), P n a b := +match a with + |F1 m => fun (b: t (S m)) => match b as b' in t n' + return match n' as n0 + return t n0 -> Type with + |0 => fun _ => @ID + |S n0 => fun b0 => P (S n0) F1 b0 + end b' with + |F1 m' => H0 m' + |FS m' b' => H1 m' b' + end + |FS m a' => fun (b: t (S m)) => match b as b' in t n' + return match n' as n0 + return t n0 -> Type with + |0 => fun _ => @ID + |S n0 => fun b0 => + forall (a0: t n0), P (S n0) (FS a0) b0 + end b' with + |F1 m' => fun aa => H2 m' aa + |FS m' b' => fun aa => HS m' aa b' (rect2_fix m' aa b') + end a' +end. +End SCHEMES. + +(** [to_nat f] = p iff [f] is the p{^ th} element of [fin m]. *) +Fixpoint to_nat {m} (n : t m) : {i | i < m} := + match n in t k return {i | i< k} with + |F1 j => exist (fun i => i< S j) 0 (Lt.lt_0_Sn j) + |FS _ p => match to_nat p with |exist i P => exist _ (S i) (Lt.lt_n_S _ _ P) end + end. + +(** [of_nat p n] answers the p{^ th} element of [fin n] if p < n or a proof of +p >= n else *) +Fixpoint of_nat (p n : nat) : (t n) + { exists m, p = n + m } := + match n with + |0 => inright _ (ex_intro (fun x => p = 0 + x) p (@eq_refl _ p)) + |S n' => match p with + |0 => inleft _ (F1) + |S p' => match of_nat p' n' with + |inleft f => inleft _ (FS f) + |inright arg => inright _ (match arg with |ex_intro m e => + ex_intro (fun x => S p' = S n' + x) m (f_equal S e) end) + end + end + end. + +(** [of_nat_lt p n H] answers the p{^ th} element of [fin n] +it behaves much better than [of_nat p n] on open term *) +Fixpoint of_nat_lt {p n : nat} : p < n -> t n := + match n with + |0 => fun H : p < 0 => False_rect _ (Lt.lt_n_O p H) + |S n' => match p with + |0 => fun _ => @F1 n' + |S p' => fun H => FS (of_nat_lt (Lt.lt_S_n _ _ H)) + end + end. + +Lemma of_nat_to_nat_inv {m} (p : t m) : of_nat_lt (proj2_sig (to_nat p)) = p. +Proof. +induction p. + reflexivity. + simpl; destruct (to_nat p). simpl. subst p; repeat f_equal. apply Peano_dec.le_unique. +Qed. + +(** [weak p f] answers a function witch is the identity for the p{^ th} first +element of [fin (p + m)] and [FS (FS .. (FS (f k)))] for [FS (FS .. (FS k))] +with p FSs *) +Fixpoint weak {m}{n} p (f : t m -> t n) : + t (p + m) -> t (p + n) := +match p as p' return t (p' + m) -> t (p' + n) with + |0 => f + |S p' => fun x => match x in t n0 return + match n0 with |0 => @ID |S n0' => n0' = p' + m -> t (S p' + n) end with + |F1 n' => fun eq : n' = p' + m => F1 + |FS n' y => fun eq : n' = p' + m => FS (weak p' f (eq_rect _ t y _ eq)) + end (eq_refl _) +end. + +(** The p{^ th} element of [fin m] viewed as the p{^ th} element of +[fin (m + n)] *) +Fixpoint L {m} n (p : t m) : t (m + n) := + match p with |F1 _ => F1 |FS _ p' => FS (L n p') end. + +Lemma L_sanity {m} n (p : t m) : proj1_sig (to_nat (L n p)) = proj1_sig (to_nat p). +Proof. +induction p. + reflexivity. + simpl; destruct (to_nat (L n p)); simpl in *; rewrite IHp. now destruct (to_nat p). +Qed. + +(** The p{^ th} element of [fin m] viewed as the p{^ th} element of +[fin (n + m)] +Really really ineficient !!! *) +Definition L_R {m} n (p : t m) : t (n + m). +induction n. + exact p. + exact ((fix LS k (p: t k) := + match p in t n0 return t (S n0) with + |F1 _ => F1 + |FS _ p' => FS (LS _ p') + end) _ IHn). +Defined. + +(** The p{^ th} element of [fin m] viewed as the (n + p){^ th} element of +[fin (n + m)] *) +Fixpoint R {m} n (p : t m) : t (n + m) := + match n with |0 => p |S n' => FS (R n' p) end. + +Lemma R_sanity {m} n (p : t m) : proj1_sig (to_nat (R n p)) = n + proj1_sig (to_nat p). +Proof. +induction n. + reflexivity. + simpl; destruct (to_nat (R n p)); simpl in *; rewrite IHn. now destruct (to_nat p). +Qed. + +Fixpoint depair {m n} (o : t m) (p : t n) : t (m * n) := +match o with + |F1 m' => L (m' * n) p + |FS m' o' => R n (depair o' p) +end. + +Lemma depair_sanity {m n} (o : t m) (p : t n) : + proj1_sig (to_nat (depair o p)) = n * (proj1_sig (to_nat o)) + (proj1_sig (to_nat p)). +induction o ; simpl. + rewrite L_sanity. now rewrite Mult.mult_0_r. + + rewrite R_sanity. rewrite IHo. + rewrite Plus.plus_assoc. destruct (to_nat o); simpl; rewrite Mult.mult_succ_r. + now rewrite (Plus.plus_comm n). +Qed.
\ No newline at end of file diff --git a/theories/Vectors/Vector.v b/theories/Vectors/Vector.v new file mode 100644 index 000000000..f3e5e338f --- /dev/null +++ b/theories/Vectors/Vector.v @@ -0,0 +1,22 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Vectors. + + Author: Pierre Boutillier + Institution: PPS, INRIA 12/2010 + +Originally from the contribution bit vector by Jean Duprat (ENS Lyon). + +Based on contents from Util/VecUtil of the CoLoR contribution *) + +Require Fin. +Require VectorDef. +Require VectorSpec. +Include VectorDef. +Include VectorSpec. diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v new file mode 100644 index 000000000..e5bb66a20 --- /dev/null +++ b/theories/Vectors/VectorDef.v @@ -0,0 +1,330 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Definitions of Vectors and functions to use them + + Author: Pierre Boutillier + Institution: PPS, INRIA 12/2010 +*) + +(** +Names should be "caml name in list.ml" if exists and order of arguments +have to be the same. complain if you see mistakes ... *) + +Require Import Arith_base. +Require Fin. +Open Local Scope nat_scope. + +(** +A vector is a list of size n whose elements belong to a set A. *) + +Inductive t A : nat -> Type := + |nil : t A 0 + |cons : forall (h:A) (n:nat), t A n -> t A (S n). + +Local Notation "[]" := (nil _). +Local Notation "h :: t" := (cons _ h _ t) (at level 60, right associativity). + +Section SCHEMES. + +(** An induction scheme for non-empty vectors *) +Definition rectS {A} (P:forall {n}, t A (S n) -> Type) + (bas: forall a: A, P 0 (a :: [])) + (rect: forall a {n} (v: t A (S n)), P n v -> P (S n) (a :: v)) := + fix rectS_fix {n} (v: t A (S n)) : P n v := + match v with + |nil => @id + |cons a 0 v => + match v as vnn in t _ nn + return + match nn as nnn return t A nnn -> Type with + |0 => fun vm => P 0 (a :: vm) + |S _ => fun _ => ID + end vnn + with + |nil => bas a + |_ :: _ => @id + end + |cons a (S nn') v => rect a nn' v (rectS_fix _ v) + end. + +(** An induction scheme for 2 vectors of same length *) +Definition rect2 {A B} (P:forall n, t A n -> t B n -> Type) + (bas : P 0 [] []) (rect : forall n v1 v2, P n v1 v2 -> + forall a b, P (S n) (a :: v1) (b :: v2)) := +fix rect2_fix {n} (v1:t A n): + forall v2 : t B n, P n v1 v2 := +match v1 as v1' in t _ n1 + return forall v2 : t B n1, P n1 v1' v2 with + |[] => fun v2 => + match v2 as v2' in t _ n2 + return match n2 as n2' return t B n2' -> Type with + |0 => fun v2 => P 0 [] v2 |S _ => fun _ => @ID end v2' with + |[] => bas + |_ :: _ => @id + end + |h1 :: t1 => fun v2 => + match v2 as v2' in t _ n2 + return match n2 as n2' + return t B n2' -> Type with + |0 => fun _ => @ID + |S n' => fun v2 => forall t1' : t A n', + P (S n') (h1 :: t1') v2 + end v2' with + |[] => @id + |h2 :: t2 => fun t1' => + rect _ t1' t2 (rect2_fix _ t1' t2) h1 h2 + end t1 +end. + +(** A vector of length [0] is [nil] *) +Definition case0 {A} (P:t A 0 -> Type) (H:P (nil A)) v:P v := +match v with + |[] => H +end. + +(** A vector of length [S _] is [cons] *) +Definition caseS {A} (P : forall n, t A (S n) -> Type) + (H : forall h n t, P _ (h :: t)) n v : P n v := +match v with + |[] => @id (* Why needed ? *) + |h :: t => H h _ t +end. +End SCHEMES. + +Section BASES. +(** The first element of a non empty vector *) +Definition hd {A} {n} (v:t A (S n)) := Eval cbv delta beta in +(caseS (fun n v => A) (fun h n t => h) n v). + +(** The last element of an non empty vector *) +Definition last {A} {n} (v : t A (S n)) := Eval cbv delta in +(rectS (fun _ _ => A) (fun a => a) (fun _ _ _ H => H) _ v). + +(** Build a vector of n{^ th} [a] *) +Fixpoint const {A} (a:A) (n:nat) := + match n return t A n with + | O => nil A + | S n => a :: (const a n) + end. + +(** The [p]{^ th} element of a vector of length [m]. + +Computational behavior of this function should be the same as +ocaml function. *) +Fixpoint nth {A} {m} (v' : t A m) (p : Fin.t m) {struct p} : A := +match p in Fin.t m' return t A m' -> A with + |Fin.F1 q => fun v => caseS (fun n v' => A) (fun h n t => h) q v + |Fin.FS q p' => fun v => (caseS (fun n v' => Fin.t n -> A) + (fun h n t p0 => nth t p0) q v) p' +end v'. + +(** An equivalent definition of [nth]. *) +Definition nth_order {A} {n} (v: t A n) {p} (H: p < n) := +(nth v (Fin.of_nat_lt H)). + +(** Put [a] at the p{^ th} place of [v] *) +Fixpoint replace {A n} (v : t A n) (p: Fin.t n) (a : A) {struct p}: t A n := + match p in Fin.t j return t A j -> t A j with + |Fin.F1 k => fun v': t A (S k) => caseS (fun n _ => t A (S n)) (fun h _ t => a :: t) _ v' + |Fin.FS k p' => fun v': t A (S k) => + (caseS (fun n _ => Fin.t n -> t A (S n)) (fun h _ t p2 => h :: (replace t p2 a)) _ v') p' + end v. + +(** Version of replace with [lt] *) +Definition replace_order {A n} (v: t A n) {p} (H: p < n) := +replace v (Fin.of_nat_lt H). + +(** Remove the first element of a non empty vector *) +Definition tl {A} {n} (v:t A (S n)) := Eval cbv delta beta in +(caseS (fun n v => t A n) (fun h n t => t) n v). + +(** Remove last element of a non-empty vector *) +Definition shiftout {A} {n:nat} (v:t A (S n)) : t A n := +Eval cbv delta beta in (rectS (fun n _ => t A n) (fun a => []) + (fun h _ _ H => h :: H) _ v). + +(** Add an element at the end of a vector *) +Fixpoint shiftin {A} {n:nat} (a : A) (v:t A n) : t A (S n) := +match v with + |[] => a :: [] + |h :: t => h :: (shiftin a t) +end. + +(** Copy last element of a vector *) +Definition shiftrepeat {A} {n} (v:t A (S n)) : t A (S (S n)) := +Eval cbv delta beta in (rectS (fun n _ => t A (S (S n))) + (fun h => h :: h :: []) (fun h _ _ H => h :: H) _ v). + +(** Remove [p] last elements of a vector *) +Lemma trunc : forall {A} {n} (p:nat), n > p -> t A n + -> t A (n - p). +Proof. + induction p as [| p f]; intros H v. + rewrite <- minus_n_O. + exact v. + + apply shiftout. + + rewrite minus_Sn_m. + apply f. + auto with *. + exact v. + auto with *. +Defined. + +(** Concatenation of two vectors *) +Fixpoint append {A}{n}{p} (v:t A n) (w:t A p):t A (n+p) := + match v with + | [] => w + | a :: v' => a :: (append v' w) + end. + +Infix "++" := append. + +(** Two definitions of the tail recursive function that appends two lists but +reverses the first one *) + +(** This one has the exact expected computational behavior *) +Fixpoint rev_append_tail {A n p} (v : t A n) (w: t A p) + : t A (tail_plus n p) := + match v with + | [] => w + | a :: v' => rev_append_tail v' (a :: w) + end. + +(** This one has a better type *) +Definition rev_append {A n p} (v: t A n) (w: t A p) + :t A (n + p) := +eq_rect _ (fun n => t A n) (rev_append_tail v w) _ + (eq_sym _ _ _ (plus_tail_plus n p)). + +(** rev [a₁ ; a₂ ; .. ; an] is [an ; a{n-1} ; .. ; a₁] + +Caution : There is a lot of rewrite garbage in this definition *) +Definition rev {A n} (v : t A n) : t A n := + eq_rect _ (fun n => t A n) (rev_append v []) + _ (eq_sym _ _ _ (plus_n_O _)). + +End BASES. +Local Notation "v [@ p ]" := (nth v p) (at level 1). + +Section ITERATORS. +(** * Here are special non dependent useful instantiation of induction +schemes *) + +(** Uniform application on the arguments of the vector *) +Definition map {A} {B} (f : A -> B) : forall {n} (v:t A n), t B n := + fix map_fix {n} (v : t A n) : t B n := match v with + | [] => [] + | a :: v' => (f a) :: (map_fix _ v') + end. + +(** map2 g [x1 .. xn] [y1 .. yn] = [(g x1 y1) .. (g xn yn)] *) +Definition map2 {A B C}{n} (g:A -> B -> C) (v1:t A n) (v2:t B n) + : t C n := +Eval cbv delta beta in rect2 (fun n _ _ => t C n) (nil C) + (fun _ _ _ H a b => (g a b) :: H) _ v1 v2. + +(** fold_left f b [x1 .. xn] = f .. (f (f b x1) x2) .. xn *) +Definition fold_left {A B:Type} (f:B->A->B): forall (b:B) {n} (v:t A n), B := + fix fold_left_fix (b:B) n (v : t A n) : B := match v with + | [] => b + | a :: w => (fold_left_fix (f b a) _ w) + end. + +(** fold_right f [x1 .. xn] b = f x1 (f x2 .. (f xn b) .. ) *) +Definition fold_right {A B : Type} (f : A->B->B) := + fix fold_right_fix {n} (v : t A n) (b:B) + {struct v} : B := + match v with + | [] => b + | a :: w => f a (fold_right_fix _ w b) + end. + +(** fold_right2 g [x1 .. xn] [y1 .. yn] c = g x1 y1 (g x2 y2 .. (g xn yn c) .. ) *) +Definition fold_right2 {A B C} (g:A -> B -> C -> C) {n} (v:t A n) + (w : t B n) (c:C) : C := +Eval cbv delta beta in rect2 (fun _ _ _ => C) c + (fun _ _ _ H a b => g a b H) _ v w. + +(** fold_left2 f b [x1 .. xn] [y1 .. yn] = g .. (g (g a x1 y1) x2 y2) .. xn yn *) +Definition fold_left2 {A B C: Type} (f : A -> B -> C -> A) := +fix fold_left2_fix (a : A) {n} (v : t B n) : t C n -> A := +match v in t _ n0 return t C n0 -> A with + |[] => fun w => match w in t _ n1 + return match n1 with |0 => A |S _ => @ID end with + |[] => a + |_ :: _ => @id end + |cons vh vn vt => fun w => match w in t _ n1 + return match n1 with |0 => @ID |S n => t B n -> A end with + |[] => @id + |wh :: wt => fun vt' => fold_left2_fix (f a vh wh) _ vt' wt end vt +end. + +End ITERATORS. + +Implicit Arguments rectS. +Implicit Arguments rect2. +Implicit Arguments fold_left. +Implicit Arguments fold_right. +Implicit Arguments map. +Implicit Arguments fold_left2. + + +Section SCANNING. +Inductive Forall {A} (P: A -> Prop): forall {n} (v: t A n), Prop := + |Forall_nil: Forall P [] + |Forall_cons {n} x (v: t A n): P x -> Forall P v -> Forall P (x::v). +Hint Constructors Forall. + +Inductive Exists {A} (P:A->Prop): forall {n}, t A n -> Prop := + |Exists_cons_hd {m} x (v: t A m): P x -> Exists P (x::v) + |Exists_cons_tl {m} x (v: t A m): Exists P v -> Exists P (x::v). +Hint Constructors Exists. + +Inductive In {A} (a:A): forall {n}, t A n -> Prop := + |In_cons_hd {m} (v: t A m): In a (a::v) + |In_cons_tl {m} x (v: t A m): In a v -> In a (x::v). +Hint Constructors In. + +Inductive Forall2 {A B} (P:A->B->Prop): forall {n}, t A n -> t B n -> Prop := + |Forall2_nil: Forall2 P [] [] + |Forall2_cons {m} x1 x2 (v1:t A m) v2: P x1 x2 -> Forall2 P v1 v2 -> + Forall2 P (x1::v1) (x2::v2). +Hint Constructors Forall2. + +Inductive Exists2 {A B} (P:A->B->Prop): forall {n}, t A n -> t B n -> Prop := + |Exists2_cons_hd {m} x1 x2 (v1: t A m) (v2: t B m): P x1 x2 -> Exists2 P (x1::v1) (x2::v2) + |Exists2_cons_tl {m} x1 x2 (v1:t A m) v2: Exists2 P v1 v2 -> Exists2 P (x1::v1) (x2::v2). +Hint Constructors Exists2. + +End SCANNING. + +Section VECTORLIST. +(** * vector <=> list functions *) + +Fixpoint of_list {A} (l : list A) : t A (length l) := +match l as l' return t A (length l') with + |Datatypes.nil => [] + |(h :: tail)%list => (h :: (of_list tail)) +end. + +Definition to_list {A}{n} (v : t A n) : list A := +Eval cbv delta beta in fold_right (fun h H => Datatypes.cons h H) v Datatypes.nil. +End VECTORLIST. + +Module VectorNotations. +Notation "[]" := [] : vector_scope. +Notation "h :: t" := (h :: t) (at level 60, right associativity) + : vector_scope. + +Notation "v [@ p ]" := (nth v p) (at level 1, format "v [@ p ]") : vector_scope. + +Open Scope vector_scope. +End VectorNotations. diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v new file mode 100644 index 000000000..1fa70a60c --- /dev/null +++ b/theories/Vectors/VectorSpec.v @@ -0,0 +1,113 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Proofs of specification for functions defined over Vector + + Author: Pierre Boutillier + Institution: PPS, INRIA 12/2010 +*) + +Require Fin. +Require Import VectorDef. +Import VectorNotations. + +(** Lemmas are done for functions that use [Fin.t] but thanks to [Peano_dec.le_unique], all +is true for the one that use [lt] *) + +Lemma eq_nth_iff A n (v1 v2: t A n): + (forall p1 p2, p1 = p2 -> v1 [@ p1 ] = v2 [@ p2 ]) <-> v1 = v2. +Proof. +split. + revert n v1 v2; refine (rect2 _ _ _); simpl; intros. + reflexivity. + f_equal. apply (H0 Fin.F1 Fin.F1 eq_refl). + apply H. intros p1 p2 H1; + apply (H0 (Fin.FS p1) (Fin.FS p2) (f_equal (@Fin.FS n) H1)). + intros; now f_equal. +Qed. + +Lemma nth_order_last A: forall n (v: t A (S n)) (H: n < S n), + nth_order v H = last v. +Proof. +unfold nth_order; refine (rectS _ _ _); now simpl. +Qed. + +Lemma shiftin_nth A a n (v: t A n) k1 k2 (eq: k1 = k2): + nth (shiftin a v) (Fin.L_R 1 k1) = nth v k2. +Proof. +subst k2; induction k1. + generalize dependent n. apply caseS ; intros. now simpl. + generalize dependent n. refine (caseS _ _) ; intros. now simpl. +Qed. + +Lemma shiftin_last A a n (v: t A n): last (shiftin a v) = a. +Proof. +induction v ;now simpl. +Qed. + +Lemma shiftrepeat_nth A: forall n k (v: t A (S n)), + nth (shiftrepeat v) (Fin.L_R 1 k) = nth v k. +Proof. +refine (Fin.rectS _ _ _); intros. + revert n v; refine (caseS _ _); simpl; intros. now destruct t. + revert p H. + refine (match v as v' in t _ m return match m as m' return t A m' -> Type with + |S (S n) => fun v => forall p : Fin.t (S n), + (forall v0 : t A (S n), (shiftrepeat v0) [@ Fin.L_R 1 p ] = v0 [@p]) -> + (shiftrepeat v) [@Fin.L_R 1 (Fin.FS p)] = v [@Fin.FS p] + |_ => fun _ => @ID end v' with + |[] => @id |h :: t => _ end). destruct n0. exact @id. now simpl. +Qed. + +Lemma shiftrepeat_last A: forall n (v: t A (S n)), last (shiftrepeat v) = last v. +Proof. +refine (rectS _ _ _); now simpl. +Qed. + +Lemma const_nth A (a: A) n (p: Fin.t n): (const a n)[@ p] = a. +Proof. +now induction p. +Qed. + +Lemma nth_map {A B} (f: A -> B) {n} v (p1 p2: Fin.t n) (eq: p1 = p2): + (map f v) [@ p1] = f (v [@ p2]). +Proof. +subst p2; induction p1. + revert n v; refine (caseS _ _); now simpl. + revert n v p1 IHp1; refine (caseS _ _); now simpl. +Qed. + +Lemma nth_map2 {A B C} (f: A -> B -> C) {n} v w (p1 p2 p3: Fin.t n): + p1 = p2 -> p2 = p3 -> (map2 f v w) [@p1] = f (v[@p2]) (w[@p3]). +Proof. +intros; subst p2; subst p3; revert n v w p1. +refine (rect2 _ _ _); simpl. + exact (Fin.case0). + intros n v1 v2 H a b p; revert n p v1 v2 H; refine (Fin.caseS _ _ _); + now simpl. +Qed. + +Lemma fold_left_right_assoc_eq {A B} {f: A -> B -> A} + (assoc: forall a b c, f (f a b) c = f (f a c) b) + {n} (v: t B n): forall a, fold_left f a v = fold_right (fun x y => f y x) v a. +Proof. +assert (forall n h (v: t B n) a, fold_left f (f a h) v = f (fold_left f a v) h). + induction v0. + now simpl. + intros; simpl. rewrite<- IHv0. now f_equal. + induction v. + reflexivity. + simpl. intros; now rewrite<- (IHv). +Qed. + +Lemma to_list_of_list_opp {A} (l: list A): to_list (of_list l) = l. +Proof. +induction l. + reflexivity. + unfold to_list; simpl. now f_equal. +Qed. diff --git a/theories/Vectors/vo.itarget b/theories/Vectors/vo.itarget new file mode 100644 index 000000000..7f00d0162 --- /dev/null +++ b/theories/Vectors/vo.itarget @@ -0,0 +1,4 @@ +Fin.vo +VectorDef.vo +VectorSpec.vo +Vector.vo diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v index 4e9c85278..4f4a6078c 100644 --- a/theories/ZArith/Zbool.v +++ b/theories/ZArith/Zbool.v @@ -230,4 +230,4 @@ Lemma Zeq_bool_if : forall x y, if Zeq_bool x y then x=y else x<>y. Proof. intros. generalize (Zeq_bool_eq x y)(Zeq_bool_neq x y). destruct Zeq_bool; auto. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/ZArith/Zdigits.v b/theories/ZArith/Zdigits.v index 6d8a237e5..ff1d96df4 100644 --- a/theories/ZArith/Zdigits.v +++ b/theories/ZArith/Zdigits.v @@ -45,17 +45,17 @@ Section VALUE_OF_BOOLEAN_VECTORS. exact 0%Z. inversion H0. - exact (bit_value a + 2 * H H2)%Z. + exact (bit_value h + 2 * H H2)%Z. Defined. Lemma two_compl_value : forall n:nat, Bvector (S n) -> Z. Proof. simple induction n; intros. inversion H. - exact (- bit_value a)%Z. + exact (- bit_value h)%Z. inversion H0. - exact (bit_value a + 2 * H H2)%Z. + exact (bit_value h + 2 * H H2)%Z. Defined. End VALUE_OF_BOOLEAN_VECTORS. @@ -134,7 +134,7 @@ Section Z_BRIC_A_BRAC. Lemma binary_value_Sn : forall (n:nat) (b:bool) (bv:Bvector n), - binary_value (S n) (Vcons bool b n bv) = + binary_value (S n) ( b :: bv) = (bit_value b + 2 * binary_value n bv)%Z. Proof. intros; auto. diff --git a/theories/ZArith/Zminmax.v b/theories/ZArith/Zminmax.v index 61c31f109..63317d9cb 100644 --- a/theories/ZArith/Zminmax.v +++ b/theories/ZArith/Zminmax.v @@ -19,4 +19,4 @@ Notation Zmin_max_distr_r := Z.min_max_distr (only parsing). Notation Zmax_min_modular_r := Z.max_min_modular (only parsing). Notation Zmin_max_modular_r := Z.min_max_modular (only parsing). Notation max_min_disassoc := Z.max_min_disassoc (only parsing). -(*end hide*)
\ No newline at end of file +(*end hide*) diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v index 8f4a69b1e..454f62aa9 100644 --- a/theories/ZArith/Znat.v +++ b/theories/ZArith/Znat.v @@ -194,7 +194,7 @@ Proof. Qed. (** For compatibility *) -Definition Zpos_eq_Z_of_nat_o_nat_of_P p := eq_sym (Z_of_nat_of_P p). +Definition Zpos_eq_Z_of_nat_o_nat_of_P p := eq_sym _ _ _ (Z_of_nat_of_P p). (******************************************************************) (** Properties of the injection from N into Z *) diff --git a/theories/theories.itarget b/theories/theories.itarget index 7cc4e09a9..3a87d8cf1 100644 --- a/theories/theories.itarget +++ b/theories/theories.itarget @@ -6,6 +6,7 @@ MSets/vo.otarget Structures/vo.otarget Init/vo.otarget Lists/vo.otarget +Vectors/vo.otarget Logic/vo.otarget PArith/vo.otarget NArith/vo.otarget diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index a62510b68..7ffb5a5f3 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -73,6 +73,7 @@ let theories_dirs_map = [ "theories/Sets", "Sets" ; "theories/Structures", "Structures" ; "theories/Lists", "Lists" ; + "theories/Vectors", "Vectors" ; "theories/Wellfounded", "Wellfounded" ; "theories/Relations", "Relations" ; "theories/Numbers", "Numbers" ; |