| Age | Commit message (Collapse) | Author |
|---|
|
automatically instead
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
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].
|
|
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
|
|
|
|
|
|
|
|
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`).
|
|
|
|
|
|
|
|
|
|
No need to use `discriminate`. This is the hopefully uncontroversial part of https://github.com/coq/coq/pull/401.
|
|
discharge literal comparisons.
|
|
|
|
comparisons.
|
|
|
|
Was needed to be done for a while.
|
|
|
|
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.
|
|
|
|
|
|
Added a function that takes the first [p] elements of a vector, and
a few lemmas proving some of its properties.
|
|
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.
|
|
|
|
|
|
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.
|
|
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).
|
|
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.
|
|
|
|
The "theories/Logic/PropExtensionalityFacts.v" file was:
- compiled
- used in several places
but not actually installed.
This commit fixes that.
|
|
|
|
|
|
|
|
|
|
choice
|
|
This commit removes from the source tree plugins/decl_mode,
its chapter in the reference manual and related tests.
|
|
|
|
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.
|
|
|
|
Also integrating suggestions from Théo.
|
|
axiom of choice (i.e. choice on setoids) and of the axiom selecting
representatives in classes of equivalence.
Also integrating suggestions from Théo.
|
|
|
|
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).
|
|
|
