aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
* Stop using auto with * in two proofs.Gravatar Théo Zimmermann2017-05-16
| | | | | | auto with * is an overkill for people who do not care to understand what they really need. In these two cases, one lemma which was available in the typeclass_instances hint db.
* Merge PR#201: Transparent abstractGravatar Maxime Dénès2017-05-11
|\
* \ Merge PR#605: Report a useful error for dependent inductionGravatar Maxime Dénès2017-05-05
|\ \
* \ \ Merge PR#593: Functional choice <-> [inhabited] and [forall] commuteGravatar Maxime Dénès2017-05-05
|\ \ \
* \ \ \ Merge PR#588: Allow interactive editing of {C,}Morphisms in PGGravatar Maxime Dénès2017-05-03
|\ \ \ \
* \ \ \ \ Merge PR#386: Better editing of the standard library in coqtop/PGGravatar Maxime Dénès2017-05-03
|\ \ \ \ \
| | | | * | Report a useful error for dependent inductionGravatar Tej Chajed2017-05-03
| |_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The dependent induction tactic notation is in the standard library but not loaded by default, leading to a parser error message that is confusing and unhelpful. This commit adds a notation for dependent induction to Init that fails and reports [Require Import Coq.Program.Equality.] is required to use [dependent induction].
| | | * | Reorganize comment documentation of ChoiceFacts.vGravatar Gaetan Gilbert2017-05-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Shortnames and natural language descriptions of principles are moved next to each principle. The table of contents is moved to after the principle definitions. Extra definitions are moved to the definition section (eg DependentFunctionalChoice) Compatibility notations have been moved to the end of the file. Details: The following used to be announced but were neither defined or used, and have been removed: - OAC! - Ext_pred = extensionality of predicates - Ext_fun_prop_repr = choice of a representative among extensional functions to Prop GuardedFunctionalRelReification was announced with shortname GAC! but shortname GFR_fun was used next to it. Only the former has been retained. Shortnames and descriptions have been invented for InhabitedForallCommute DependentFunctionalRelReification ExtensionalPropositionRepresentative ExtensionalFunctionRepresentative Some modification of headlines
| | | * | Functional choice <-> [inhabited] and [forall] commuteGravatar Gaetan Gilbert2017-04-30
| |_|/ / |/| | |
* | | | Suppress warning message in stdlib.Gravatar Guillaume Melquiond2017-04-29
| | | |
| | * | Allow interactive editing of {C,}Morphisms in PGGravatar Jason Gross2017-04-28
| |/ / |/| |
| * | Add .dir-locals.el and _CoqProject files for emacs stdlib editingGravatar Jason Gross2017-04-28
|/ / | | | | | | | | | | | | | | | | | | | | | | These set up PG to use the local coqtop, and the local coqlib, when editing files in the stdlib. As per https://github.com/coq/coq/pull/386#issuecomment-279012238, we can use `_CoqProject` for `theories/Init`, and this allows CoqIDE to edit those files. However, we cannot use it for `theories/`, because a `_CoqProject` file will override a `.dir-locals.el` in the same directory, and there is no way to get PG to pick up a valid `-coqlib` from `_CoqProject` (because it'll take the path relative to the current directory, not relative to the directory of `_CoqProject`).
* | Merge PR#414: Some more theory on powerRZ.Gravatar Maxime Dénès2017-04-27
|\ \
* \ \ Merge PR#584: Give andb_prop a simpler proofGravatar Maxime Dénès2017-04-27
|\ \ \
* | | | Small typo in commentGravatar Vadim Zaliva2017-04-26
| | | |
| | | * Add transparent_abstract tacticGravatar Jason Gross2017-04-25
| |_|/ |/| |
| * | Give andb_prop a simpler proofGravatar Jason Gross2017-04-25
|/ / | | | | No need to use `discriminate`. This is the hopefully uncontroversial part of https://github.com/coq/coq/pull/401.
* | Merge PR#545: Add some hints to the "real" database to automatically ↵Gravatar Maxime Dénès2017-04-19
|\ \ | | | | | | | | | discharge literal comparisons.
* \ \ Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-15
|\ \ \
| | * | Add some hints to the "real" database to automatically discharge literal ↵Gravatar Guillaume Melquiond2017-04-07
| |/ / |/| | | | | | | | comparisons.
* | | Merge PR#455: Farewell decl_modeGravatar Maxime Dénès2017-04-06
|\ \ \
| | * \ Merge branch 'origin/v8.5' into v8.6.Gravatar Hugo Herbelin2017-04-06
| | |\ \ | | | | | | | | | | | | | | | Was needed to be done for a while.
* | | | | Fix documentation typo (bug #5433).Gravatar Guillaume Melquiond2017-04-02
| | | | |
* | | | | Simplify some proofs.Gravatar Guillaume Melquiond2017-04-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit does not modify the signature of the involved modules, only the opaque proof terms. One has to wonder how proofs can bitrot so much that several occurrences of "replace 4 with 4" start appearing.
* | | | | Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R.Gravatar Guillaume Melquiond2017-03-30
| | | | |
* | | | | Merge PR#469: Added take to VectorDefGravatar Maxime Dénès2017-03-30
|\ \ \ \ \
| * | | | | Added take to VectorDef.Gravatar George Stelle2017-03-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Added a function that takes the first [p] elements of a vector, and a few lemmas proving some of its properties.
* | | | | | Fixing missing PropFacts.v in Logic/vo.itarget.Gravatar Hugo Herbelin2017-03-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is while waiting for a possible different solution, if ever such a different solution is adopted, since the coq.inria.fr/library has currently a broken link and someone rightly complained about it.
* | | | | | Merge PR#392: strengthened the statement of JMeq_eq_depGravatar Maxime Dénès2017-03-24
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
|\ \ \ \ \ \ \ | | |_|_|/ / / | |/| | | | |
* | | | | | | Make IZR a morphism for field.Gravatar Guillaume Melquiond2017-03-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There are now two field structures for R: one in RealField and one in RIneq. The first one is used to prove that IZR is a morphism which is needed to define the second one.
* | | | | | | Change the parser and printer so that they use IZR for real constants.Gravatar Guillaume Melquiond2017-03-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There are two main issues. First, (-cst)%R is no longer syntactically equal to (-(cst))%R (though they are still convertible). This breaks some rewriting rules. Second, the ring/field_simplify tactics did not know how to refold real constants. This defect is no longer hidden by the pretty-printer, which makes these tactics almost unusable on goals containing large constants. This commit also modifies the ring/field tactics so that real constant reification is now constant time rather than linear. Note that there is now a bit of code duplication between z_syntax and r_syntax. This should be fixed once plugin interdependencies are supported. Ideally the r_syntax plugin should just disappear by declaring IZR as a coercion. Unfortunately the coercion mechanism is not powerful enough yet, be it for parsing (need the ability for a scope to delegate constant parsing to another scope) or printing (too many visible coercions left).
* | | | | | | Make IZR use a compact representation of integers.Gravatar Guillaume Melquiond2017-03-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | That way, (IZR 5) is no longer reduced to 2 + 1 + 1 + 1 (which is not convertible to 5) but instead to 1 + 2 * 2 (which is). Moreover, it means that, after reduction, real constants no longer exponentially blow up. Note that I was not able to fix the test-suite for the declarative mode, so the missing proof terms have been admitted.
* | | | | | | Simplify some proofs using ring and field.Gravatar Guillaume Melquiond2017-03-22
| | | | | | |
* | | | | | | Add a forgotten (?) line to "theories/Logic/vo.itarget".Gravatar Matej Kosik2017-03-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The "theories/Logic/PropExtensionalityFacts.v" file was: - compiled - used in several places but not actually installed. This commit fixes that.
* | | | | | | Merge PR#442: Allow interactive editing of Coq.Init.LogicGravatar Maxime Dénès2017-03-17
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR#451: Add η principles for sigma typesGravatar Maxime Dénès2017-03-17
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR#444: Simplifying a statement in Hurkens.v + a case study for eautoGravatar Maxime Dénès2017-03-14
|\ \ \ \ \ \ \ \ \ | |_|_|_|_|/ / / / |/| | | | | | | |
| | | | * | | | | Fix 3 unused-intro-pattern warnings in stdlib.Gravatar Théo Zimmermann2017-03-14
| | | | | | | | |
* | | | | | | | | Merge PR#318: Providing a file in the Logic library to work with extensional ↵Gravatar Maxime Dénès2017-03-09
|\ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | choice
| | | | | | | * | | Farewell decl_modeGravatar Enrico Tassi2017-03-07
| |_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit removes from the source tree plugins/decl_mode, its chapter in the reference manual and related tests.
* | | | | | | | | Merge PR#279: A few lemmas about iff and about orders on positive and ZGravatar Maxime Dénès2017-03-06
|\ \ \ \ \ \ \ \ \
| | * | | | | | | | Strengthening some of the results in ChoiceFacts.v.Gravatar Hugo Herbelin2017-03-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Further highlighting when the correspondence between variants of choice is independent of the domain and codomain of the function, as was done already done in the beginning of the file (suggestion from Jason). Adding some corollaries.
| | * | | | | | | | Adding explicitly a file to work in the context of propositional extensionality.Gravatar Hugo Herbelin2017-03-03
| | | | | | | | | |
| | * | | | | | | | Adding a file providing extensional choice (i.e. choice over setoids).Gravatar Hugo Herbelin2017-03-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Also integrating suggestions from Théo.
| | * | | | | | | | Adding various properties and characterization of the extensionalGravatar Hugo Herbelin2017-03-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | axiom of choice (i.e. choice on setoids) and of the axiom selecting representatives in classes of equivalence. Also integrating suggestions from Théo.
| | * | | | | | | | Slightly unifying renaming in ChoiceFacts.v.Gravatar Hugo Herbelin2017-03-03
| | | | | | | | | |
| | * | | | | | | | Logic library: Adding a characterization of excluded-middle in term ofGravatar Hugo Herbelin2017-03-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | choice of a representative in a partition of bool. Also move a result about propositional extensionality from ClassicalFacts.v to PropExtensionalityFacts.v, generalizing it by symmetry. Also spotting typos (thanks to Théo).
* | | | | | | | | | Merge PR#273: Tidy stdlibGravatar Maxime Dénès2017-03-03
|\ \ \ \ \ \ \ \ \ \
| | * | | | | | | | | Completing basic lemmas about <= and < in BinInt.Z.Pos2Z.Gravatar Hugo Herbelin2017-03-03
| | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 16:56:20 +0000