aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Logic
Commit message (Collapse)AuthorAge
* 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
|
* 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
|\
* | 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#444: Simplifying a statement in Hurkens.v + a case study for eautoGravatar Maxime Dénès2017-03-14
|\ \
* | | 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).
* | | Formatting references with surrounding brackets in Diaconescu.v.Gravatar Hugo Herbelin2017-03-03
| | |
| * | Simplifying the proof of NoRetractToModalProposition.paradox inGravatar Hugo Herbelin2017-02-24
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Hurkens.v by dropping the artificial need for monad laws. Tactic eauto decided to be dependent on the laws but there is a shorter proof without them. [Interestingly, eauto is not able to find the short proof. This is a situation of the form subgoal 1: H : ?A |- P x subgoal 2: H : M ?A |- M (forall x, P x) where addressing the second subgoal would find the right instance of ?A, but this instance is too hard to find by addressing first the first subgoal.]
* | Fix a typo in Hurkens.v commentGravatar Jason Gross2016-12-19
| |
| * strengthened the statement of JMeq_eq_depGravatar Abhishek Anand2016-12-11
|/ | | | because P:U->Prop implies P:U->Type, the new statement is strictly more useful. No change was needed to the proof.
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\
| * Remove v62 from stdlib.Gravatar Théo Zimmermann2016-10-24
| | | | | | | | | | This old compatibility hint database can be safely removed now that coq-contribs do not depend on it anymore.
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-08
|\|
| * Fixing unexpected "noise" introduced in commit 24d5448c.Gravatar Hugo Herbelin2016-10-06
| | | | | | | | A file was introduced by mistake in theories/Logic.
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\|
| * More tests for tactic "subst".Gravatar Hugo Herbelin2016-10-02
| |
* | extensionality: Handle dependently-used hypothesesGravatar Jason Gross2016-09-19
| |
* | Adding an "extensionality in H" tactic which applies functionalGravatar Hugo Herbelin2016-09-19
|/ | | | | | | | extensionality in H supposed to be a quantified equality until giving a bare equality. Thanks to Jason Gross and Jonathan Leivent for suggestions and examples.
* Typo in a comment of stdlib.Gravatar Hugo Herbelin2016-07-08
|
* Moving the Tauto tactic to proper Ltac.Gravatar Pierre-Marie Pédrot2016-02-22
| | | | | | This gets rid of brittle code written in ML files through Ltac quotations, and reduces the dependance of Coq to such a feature. This also fixes the particular instance of bug #2800, although the underlying issue is still there.
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\
| * Fix bug #4503: mixing universe polymorphic and monomorphicGravatar Matthieu Sozeau2016-01-23
| | | | | | | | variables and definitions in sections is unsupported.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-17
|\|
| * Refine tactic now shelves unifiable holes.Gravatar Pierre-Marie Pédrot2015-12-15
| | | | | | | | | | | | The unshelve tactical can be used to get the shelved holes. This changes the proper ordering of holes though, so expect some broken scripts. Also, the test-suite is not fixed yet.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-11
|\|
| * Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Gravatar Hugo Herbelin2015-12-10
| | | | | | | | Marking it as experimental.
* | Fix to previous commit (ClassicalFacts.v).Gravatar Hugo Herbelin2015-12-05
| |
* | Adding proofs on the relation between excluded-middle and minimization.Gravatar Hugo Herbelin2015-12-05
| | | | | | | | | | | | | | In particular, a proof of the equivalence of excluded-middle and an unrestricted principle of minimization. Credits to Arnaud Spiwack for the ideas and formalizations of the proofs.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-29
|\|
| * Univs: entirely disallow instantiation of polymorphic constants withGravatar Matthieu Sozeau2015-11-27
| | | | | | | | | | | | | | | | | | Prop levels. As they are typed assuming all variables are >= Set now, and this was breaking an invariant in typing. Only one instance in the standard library was used in Hurkens, which can be avoided easily. This also avoids displaying unnecessary >= Set constraints everywhere.
* | Adding an amazing property of Prop.Gravatar Hugo Herbelin2015-11-07
|/
* Minor modifications to WeakFanTheorem.Gravatar Hugo Herbelin2015-09-08
|
* Remove some outdated files and fix permissions.Gravatar Guillaume Melquiond2015-07-31
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Added an arithmetical characterization of the hypothesis of WKL.Gravatar Hugo Herbelin2014-12-01
|
* Improving elimination with indices, getting rid of intrusive residualGravatar Hugo Herbelin2014-11-02
| | | | local definitions...
* Make sure that Logic/ExtensionalityFacts gets compiled.Gravatar Guillaume Melquiond2014-10-27
|
* Fix some typos.Gravatar Guillaume Melquiond2014-10-27
|
* Fix some typos in comments.Gravatar Guillaume Melquiond2014-10-27
|
* EqdepFacts: generalize statements which were wrongly restricted to Prop.Gravatar Arnaud Spiwack2014-10-22
|
* ConstructiveEpsilon: simplify the before_witness type using non-uniform ↵Gravatar Arnaud Spiwack2014-10-16
| | | | parameters.
* Hurkens.v: Fix a syntax error.Gravatar Arnaud Spiwack2014-09-26
| | | Introduced in c74a70a73b3bf39394c551f1cdb224450bf77176.
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 09:48:53 +0000