aboutsummaryrefslogtreecommitdiff
path: root/theories/Logic
AgeCommit message (Collapse)Author
2017-03-19Add a forgotten (?) line to "theories/Logic/vo.itarget".Matej Kosik
The "theories/Logic/PropExtensionalityFacts.v" file was: - compiled - used in several places but not actually installed. This commit fixes that.
2017-03-14Merge PR#444: Simplifying a statement in Hurkens.v + a case study for eautoMaxime Dénès
2017-03-03Strengthening some of the results in ChoiceFacts.v.Hugo Herbelin
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.
2017-03-03Adding explicitly a file to work in the context of propositional extensionality.Hugo Herbelin
2017-03-03Adding a file providing extensional choice (i.e. choice over setoids).Hugo Herbelin
Also integrating suggestions from Théo.
2017-03-03Adding various properties and characterization of the extensionalHugo Herbelin
axiom of choice (i.e. choice on setoids) and of the axiom selecting representatives in classes of equivalence. Also integrating suggestions from Théo.
2017-03-03Slightly unifying renaming in ChoiceFacts.v.Hugo Herbelin
2017-03-03Logic library: Adding a characterization of excluded-middle in term ofHugo Herbelin
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).
2017-03-03Formatting references with surrounding brackets in Diaconescu.v.Hugo Herbelin
2017-02-24Simplifying the proof of NoRetractToModalProposition.paradox inHugo Herbelin
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.]
2016-12-19Fix a typo in Hurkens.v commentJason Gross
2016-12-11strengthened the statement of JMeq_eq_depAbhishek Anand
because P:U->Prop implies P:U->Type, the new statement is strictly more useful. No change was needed to the proof.
2016-11-18Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-24Remove v62 from stdlib.Théo Zimmermann
This old compatibility hint database can be safely removed now that coq-contribs do not depend on it anymore.
2016-10-08Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-06Fixing unexpected "noise" introduced in commit 24d5448c.Hugo Herbelin
A file was introduced by mistake in theories/Logic.
2016-10-05Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-02More tests for tactic "subst".Hugo Herbelin
2016-09-19extensionality: Handle dependently-used hypothesesJason Gross
2016-09-19Adding an "extensionality in H" tactic which applies functionalHugo Herbelin
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.
2016-07-08Typo in a comment of stdlib.Hugo Herbelin
2016-02-22Moving the Tauto tactic to proper Ltac.Pierre-Marie Pédrot
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.
2016-01-29Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-23Fix bug #4503: mixing universe polymorphic and monomorphicMatthieu Sozeau
variables and definitions in sections is unsupported.
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-12-17Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-15Refine tactic now shelves unifiable holes.Pierre-Marie Pédrot
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.
2015-12-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-10Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Hugo Herbelin
Marking it as experimental.
2015-12-05Fix to previous commit (ClassicalFacts.v).Hugo Herbelin
2015-12-05Adding proofs on the relation between excluded-middle and minimization.Hugo Herbelin
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.
2015-11-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-27Univs: entirely disallow instantiation of polymorphic constants withMatthieu Sozeau
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.
2015-11-07Adding an amazing property of Prop.Hugo Herbelin
2015-09-08Minor modifications to WeakFanTheorem.Hugo Herbelin
2015-07-31Remove some outdated files and fix permissions.Guillaume Melquiond
2015-01-12Update headers.Maxime Dénès
2014-12-01Added an arithmetical characterization of the hypothesis of WKL.Hugo Herbelin
2014-11-02Improving elimination with indices, getting rid of intrusive residualHugo Herbelin
local definitions...
2014-10-27Make sure that Logic/ExtensionalityFacts gets compiled.Guillaume Melquiond
2014-10-27Fix some typos.Guillaume Melquiond
2014-10-27Fix some typos in comments.Guillaume Melquiond
2014-10-22EqdepFacts: generalize statements which were wrongly restricted to Prop.Arnaud Spiwack
2014-10-16ConstructiveEpsilon: simplify the before_witness type using non-uniform ↵Arnaud Spiwack
parameters.
2014-09-26Hurkens.v: Fix a syntax error.Arnaud Spiwack
Introduced in c74a70a73b3bf39394c551f1cdb224450bf77176.
2014-09-26ClassicalFacts: adds a proof that weak excluded middle implies weak proof ↵Arnaud Spiwack
irrelevance. Application of previous commit in Hurkens.v.
2014-09-26Hurkens.v: new paradox: type of modal propositions is not a retract.Arnaud Spiwack
In particular there is no retract of the type of negative propositions in a negative proposition.
2014-09-26Hurkens.v: fix coqdoc formatting in a comment.Arnaud Spiwack
2014-09-25Hurkens.v: update comments.Arnaud Spiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-13 19:19:34 +0000