aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Program/Equality.v
Commit message (Collapse)AuthorAge
* Used multiple lists of implicit arguments to transfer the choices ofGravatar herbelin2010-10-23
| | | | | | | | | | Program in terms of implicit arguments to the rest of the library. This commit only covers the case of list of implicit arguments that have a different length in Program (e.g. inl, Vcons) but not the case of implicit arguments which differs only in their maximality status (e.g. pair). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13575 85f007b7-540e-0410-9357-904b9bb8a0f7
* Using multiple lists of implicit arguments in Program for preservingGravatar herbelin2010-10-03
| | | | | | | | | | | | | | the compatibility with the rest of the theories. Used multiple lists of implicit arguments in Init only when the maximality status is not modified in Program (and thus the compatibility is strictly preserved). This improves the compatibility for the implicit arguments of eq_refl and JMeq_refl between 8.2 and 8.3 when using Program (up to the residual differences in the maximality status). For the constants Acc_inv, inl, inr, left, right, Vnil, Vcons, the compatibility with 8.2 is not improved but the consistency between Program and the rest of the library is. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13485 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed commit r13359 which was incomplete for its "trunk" part. ThanksGravatar herbelin2010-07-31
| | | | | | to Julien for noticing it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13366 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reorder resolution of type class and unification constraints.Gravatar msozeau2010-03-07
| | | | | | | | Fix a bug in dependent elimination when treating defined variables in the context. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12851 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update CHANGES, add documentation for new commands/tactics and do a bitGravatar msozeau2010-01-30
| | | | | | | of cleanup in tactics/ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12705 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes in typeclasses, avoiding repeated evar normalizations.Gravatar msozeau2009-11-24
| | | | | | | | | | | Improve generalization by equalities tactic, now allowing to generalize an arbitrary application, e.g. in preparation for applying an elimination principle for a function. This adds a flag to generalize_dep so that it doesn't abstract the variable if it is defined, just introducing a let-in. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12541 85f007b7-540e-0410-9357-904b9bb8a0f7
* Integrate a few improvements on typeclasses and Program from the equations ↵Gravatar msozeau2009-10-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | branch and remove equations stuff which moves to a separate plugin. Classes: - Ability to define classes post-hoc from constants or inductive types. - Correctly rebuild the hint database associated to local hypotheses when they are changed by a [Hint Extern] in typeclass resolution. Tactics and proofs: - Change [revert] so that it keeps let-ins (but not [generalize]). - Various improvements to the [generalize_eqs] tactic to make it more robust and produce the smallest proof terms possible. Move [specialize_hypothesis] in tactics.ml as it goes hand in hand with [generalize_eqs]. - A few new general purpose tactics in Program.Tactics like [revert_until] - Make transitive closure well-foundedness proofs transparent. - More uniform testing for metas/evars in pretyping/unification.ml (might introduce a few changes in the contribs). Program: - Better sorting of dependencies in obligations. - Ability to start a Program definition from just a type and no obligations, automatically adding an obligation for this type. - In compilation of Program's well-founded definitions, make the functional a separate definition for easier reasoning. - Add a hint database for every Program populated by [Hint Unfold]s for every defined obligation constant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12440 85f007b7-540e-0410-9357-904b9bb8a0f7
* Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'Gravatar letouzey2009-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12380 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix the stdlib doc compilation + switch all .v file to utf8Gravatar letouzey2009-09-28
| | | | | | | | | | | | | | | | | | | 1) compilation of Library.tex was failing on a "Ext_" in Diaconescu.v In fact coqdoc was trying to recognize the end of a _emphasis_ and hence inserted a bogus }. For the moment I've enclosed the phrase with [ ], but this emphasis "feature" of coqdoc seems _really_ easy to broke. Matthieu ? 2) By the way, this Library document was made from latin1 and utf8 source file, hence bogus characters. All .v containing special characters are converted to utf8, and their first line is now mentionning this. (+ killed some old french comments and some other avoidable special characters). PLEASE: let's stick to this convention and avoid latin1, at least in .v files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12363 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use unfold directly in unfold_equations. Fixes test-suite.Gravatar msozeau2009-07-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12246 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix premature optimisation in dependent induction: even variable args needGravatar msozeau2009-04-10
| | | | | | | | | | | to be generalized as they may appear in other arguments or their types. Try to keep the original names around as well, using the ones found in the goal. This only requires that interning a pattern [forall x, _] properly declares [x] as a metavariable, binding instances are already part of the substitutions computed by [extended_matches]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12079 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report r11631 from 8.2 and handle non-dependent goals better inGravatar msozeau2009-02-04
| | | | | | | [dependent induction]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11881 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generalized binding syntax overhaul: only two new binders: `() and `{},Gravatar msozeau2008-12-14
| | | | | | | | | | | | | | | | | guessing the binding name by default and making all generalized variables implicit. At the same time, continue refactoring of Record/Class/Inductive etc.., getting rid of [VernacRecord] definitively. The AST is not completely satisfying, but leaning towards Record/Class as restrictions of inductive (Arnaud, anyone ?). Now, [Class] declaration bodies are either of the form [meth : type] or [{ meth : type ; ... }], distinguishing singleton "definitional" classes and inductive classes based on records. The constructor syntax is accepted ([meth1 : type1 | meth1 : type2]) but raises an error immediately, as support for defining a class by a general inductive type is not there yet (this is a bugfix!). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11679 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix a bug in the specialization by unification tactic related to the problemsGravatar msozeau2008-11-07
| | | | | | | | given by injection. Add the example to the test-suite for [dependent destruction]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11551 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite 11472 et 11473Gravatar herbelin2008-10-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11474 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various little improvements:Gravatar msozeau2008-09-25
| | | | | | | | | | | | | | - A new [dependent pattern] tactic to do a pattern on an object in an inductive family and generalize by both the indexes and the object itself. Useful to prepare a goal for elimination with a dependent principle. - Better dependent elimination simplification tactic that doesn't throw away non-dependent equalities if they can't be injected. - Add [fold_sub] and [unfold_sub] tactics for folding/unfolding well-founded definitions using measures built by Program. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11420 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report improvements in Equations to the dependent elimination tactic:Gravatar msozeau2008-09-15
| | | | | | | | | | | - Do not touch at the user equalities and so on by using a blocking constant. This avoids the wild autoinjections and subst tactics that were used before. Thanks to Brian Aydemir for an example were this hurt a lot. - Debug the tactic used to simplify induction hypotheses. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11415 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finish debugging the unification machinery in [Equations]. Do the _compGravatar msozeau2008-09-13
| | | | | | | | | | dance when defining a new program by default, which forces use of JMeq but makes for much more robust tactics. Everything in success/Equations works except for limitations due to JMeq or the guardness checker (one example seems to actually diverge...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11402 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a type argument to letin_tac instead of using casts and recomputingGravatar msozeau2008-09-12
| | | | | | | | | when one wants a particular type. Rewrite of the unification behind [Equations], much more robust but still buggy w.r.t. inaccessible patterns. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11399 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add enough information to correctly globalize recursive calls in inductive andGravatar msozeau2008-09-11
| | | | | | | | | recursive definitions and references to previous fields in record and classes definitions. Fixes the corresponding typesetting issue in coqdoc output. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11397 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix a bug reintroduced in [setoid_reflexivity] etc...Gravatar msozeau2008-09-09
| | | | | | | | Go back to refine_hyp instead of specialize, because only the former handles open terms. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11391 85f007b7-540e-0410-9357-904b9bb8a0f7
* More debugging of [Equations], now able to discharge even the heavilyGravatar msozeau2008-09-07
| | | | | | | | dependent [noConfusion] definitions in "A Few Constructions on Constructors". Now the guardness check is blocking. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11374 85f007b7-540e-0410-9357-904b9bb8a0f7
* Better handling of recursive Equations definitions... still not perfect.Gravatar msozeau2008-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11356 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correct handling of implicit arguments in [Equations] definitions,Gravatar msozeau2008-09-03
| | | | | | | | support for "where" notation declarations as well. Better checking of recursivity or not, after type-checking. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11354 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add support for recursive definitions to [Equations], deciding if aGravatar msozeau2008-09-02
| | | | | | | | definition is recursive or not based on occurence of a rec call in the body. Examples updated, enjoy! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11353 85f007b7-540e-0410-9357-904b9bb8a0f7
* Initial implementation of a new command to define (dependent) functions byGravatar msozeau2008-09-02
| | | | | | | | | | | | | | | | | | | | | | equations. It is essentially an implementation of the "Eliminating Dependent Pattern-Matching" paper by Goguen, McBride and McKinna, relying on the new dependent eliminations tactics. The bulk is in contrib/subtac/equations.ml4. It implements a tree splitting on a set of clauses and the generation of a corresponding proof term along with some obligations at each splitting node. The obligations are solved by driving the dependent elimination tactic and you get a complete proof term at the end with the code given by the equations at the right spots, the rest of the cases being pruned automatically. Does not support recursion yet, a file with examples is in the test-suite. With recursion, it would be similar to Agda 2's pattern matching, except it won't reduce in Coq due to JMeq's/K. Incidentally, the simplification tactics after dependent elimination have been improved, resulting in a clearer and more space efficient implementation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11352 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes in dependent induction tactic to keep names, allow givingGravatar msozeau2008-08-21
| | | | | | | | intro-patterns and avoid useless generalizations on inductive parameters. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11331 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes in generalize_eqs/dependent induction to allow the user to specifyGravatar msozeau2008-07-28
| | | | | | | generalized variables himself. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11280 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add test-suite file for bug# 1905 and minor fix in Program/Equality.Gravatar msozeau2008-07-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11245 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improve the dependent induction tactic to automatically find theGravatar msozeau2008-05-30
| | | | | | | | generalized hypotheses. Also move part of the tactic to ML and improve the generated proof term in case of non-dependent induction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11023 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various fixes:Gravatar msozeau2008-05-15
| | | | | | | | | | | | - Fix a typo in lowercase_utf8 - Fix generation of signatures in subtac_cases not working for dependent inductive types with dependent indices. - Fix coercion of inductive types generating ill-typed terms. - Fix test script using new syntax for Instances. - Move simpl_existTs to Program.Equality and use it in simpl_depind. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10932 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
| | | | | | | | pas correctes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10739 85f007b7-540e-0410-9357-904b9bb8a0f7
* Debug implementation of dependent induction/dependent destruction and ↵Gravatar msozeau2008-01-31
| | | | | | document it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10490 85f007b7-540e-0410-9357-904b9bb8a0f7
* Work on dependent induction tactic and friends, finish the test-suite exampleGravatar msozeau2008-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10487 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merged revisions ↵Gravatar msozeau2007-12-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,10398,10403-10408 via svnmerge from svn+ssh://msozeau@scm.gforge.inria.fr/svn/coq/branches/TypeClasses ........ r10358 | msozeau | 2007-12-10 15:42:53 +0100 (Mon, 10 Dec 2007) | 1 line Comment grammar error ........ r10359 | msozeau | 2007-12-10 16:04:09 +0100 (Mon, 10 Dec 2007) | 7 lines The initial Type Classes patch. This patch introduces type classes and instance definitions a la Haskell. Technically, it uses the implicit arguments mechanism which was extended a bit. The patch also introduces a notation for explicitely marking implicit, maximally inserted parameters. It includes the tactic redefinition code too (Ltac tac ::= foo redefines tac). ........ r10360 | msozeau | 2007-12-10 16:14:30 +0100 (Mon, 10 Dec 2007) | 1 line Fix interface ........ r10361 | msozeau | 2007-12-10 16:28:19 +0100 (Mon, 10 Dec 2007) | 1 line Fix more xlate code ........ r10362 | msozeau | 2007-12-11 02:00:53 +0100 (Tue, 11 Dec 2007) | 3 lines Update coqdoc for type classes, fix proof state not being displayed on Next Obligation. ........ r10365 | msozeau | 2007-12-11 14:22:35 +0100 (Tue, 11 Dec 2007) | 3 lines Bug fixes in Instance decls. ........ r10371 | msozeau | 2007-12-12 21:17:30 +0100 (Wed, 12 Dec 2007) | 3 lines Streamline typeclass context implementation, prepare for class binders in proof statements. ........ r10372 | msozeau | 2007-12-12 22:03:38 +0100 (Wed, 12 Dec 2007) | 1 line Minor cosmetic fixes: allow sorts as typeclass param instances without parens and infer more types in class definitions ........ r10373 | msozeau | 2007-12-13 00:35:09 +0100 (Thu, 13 Dec 2007) | 2 lines Better names in g_vernac, binders in Lemmas and Context [] to introduce a typeclass context. ........ r10377 | msozeau | 2007-12-13 18:34:33 +0100 (Thu, 13 Dec 2007) | 1 line Stupid bug ........ r10383 | msozeau | 2007-12-16 00:04:48 +0100 (Sun, 16 Dec 2007) | 1 line Bug fixes in name handling and implicits, new syntax for using implicit mode in typeclass constraints ........ r10384 | msozeau | 2007-12-16 15:53:24 +0100 (Sun, 16 Dec 2007) | 1 line Streamlined implementation of instances again, the produced typeclass is a typeclass constraint. Added corresponding implicit/explicit behaviors ........ r10394 | msozeau | 2007-12-18 23:42:56 +0100 (Tue, 18 Dec 2007) | 4 lines Various fixes for implicit arguments, new "Enriching" kw to just enrich existing sets of impl args. New syntax !a to force an argument, even if not dependent. New tactic clrewrite using a setoid typeclass implementation to do setoid_rewrite under compatible morphisms... very experimental. Other bugs related to naming in typeclasses fixed. ........ r10395 | msozeau | 2007-12-19 17:11:55 +0100 (Wed, 19 Dec 2007) | 3 lines Progress on setoids using type classes, recognize setoid equalities in hyps better. Streamline implementation to return more information when resolving setoids (return the results setoid). ........ r10398 | msozeau | 2007-12-20 10:18:19 +0100 (Thu, 20 Dec 2007) | 1 line Syntax change, more like Coq ........ r10403 | msozeau | 2007-12-21 22:30:35 +0100 (Fri, 21 Dec 2007) | 1 line Add right-to-left rewriting in class_setoid, fix some discharge/substitution bug, adapt test-suite to latest syntax ........ r10404 | msozeau | 2007-12-24 21:47:58 +0100 (Mon, 24 Dec 2007) | 2 lines Work on type classes based rewrite tactic. ........ r10405 | msozeau | 2007-12-27 18:51:32 +0100 (Thu, 27 Dec 2007) | 2 lines Better evar handling in pretyping, reorder theories/Program and add some tactics for dealing with subsets. ........ r10406 | msozeau | 2007-12-27 18:52:05 +0100 (Thu, 27 Dec 2007) | 1 line Forgot to add a file ........ r10407 | msozeau | 2007-12-29 17:19:54 +0100 (Sat, 29 Dec 2007) | 4 lines Generalize usage of implicit arguments in terms, up to rawconstr. Binders are decorated with binding info, either Implicit or Explicit for rawconstr. Factorizes code for typeclasses, topconstrs decorations are Default (impl|expl) or TypeClass (impl|expl) and implicit quantification is resolve at internalization time, getting rid of the arbitrary prenex restriction on contexts. ........ r10408 | msozeau | 2007-12-31 00:58:50 +0100 (Mon, 31 Dec 2007) | 4 lines Fix parsing of subset binders, bugs in subtac_cases and handling of mutual defs obligations. Add useful tactics to Program.Subsets. ........ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10410 85f007b7-540e-0410-9357-904b9bb8a0f7
* Addition of more general tactics for equality. Functional extensionality and ↵Gravatar msozeau2007-10-24
| | | | | | | | | eta expansion axioms for dependent functions. Cleanup in Utils. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10260 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add more equality tactics. Upgrade program_simpl for discrimination of ↵Gravatar msozeau2007-08-26
| | | | | | conjuncts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10093 85f007b7-540e-0410-9357-904b9bb8a0f7
* A better Program documentation. Include it in the generated stdlib doc.Gravatar msozeau2007-08-08
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10061 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 22:04:30 +0000