| Age | Commit message (Collapse) | Author |
|---|
|
Construct `finfun_of` directly from a bespoke indexed inductive type,
which both makes it structurally positive (and therefore usable as a
container in an `Inductive` definition), and accommodates naturally
dependent functions.
This is still WIP, because this PR exposed a serious shortcoming of
the Coq unification algorithm’s implantation of Miller patterns. This
bug defeats the inference of `Canonical` structures for `{ffun S -> T}`
when the instances are defined in the dependent case!
This causes unmanageable regressions starting in `matrix.v`, so I
have not been able to check for any impact past that. I’m pushing this
commit so that the Coq issue may be addressed.
Made `fun_of_fin` structurally decreasing: Changed the primitive
accessor of `finfun_of` from `tfgraph` to the `Funclass` coercion
`fun_of_fin`. This will make it possible to define recursive functions
on inductive types built using finite functions. While`tfgraph` is
still useful to transport the tuple canonical structures to
`finfun_of`, it is no longer central to the theory so its role has
been reduced.
|
|
As per @ejgallego ’s suggestion.
|
|
Add extra eta lemmas for the under tactic
|
|
Refactoring allpairs to handle the dependent version as well
|
|
|
|
compat sumn with bigop
|
|
missing lemma in seq.v
|
|
|
|
|
|
adding ffun0
|
|
|
|
Related: coq/coq#9651
|
|
[doc] Mention that "connect" computes the reflexive transitive closure
|
|
while some refs (see e.g. [1]) don't assume that the "transitive closure" is
reflexive; so one won't need to look at lemma "connect0" to figure this out.
[1] https://en.wikipedia.org/wiki/Transitive_closure
[ci skip]
|
|
A tool to draw the hierarchy diagram
|
|
remove dependency on hidden case branch types
|
|
Anticipating coq/coq#9170, remove numeric occurrence selector affected
by the (invisible) presence of explicit types for variables bound in
`match` branch patterns. The proof could be further simplified if this
change is implemented.
|
|
Export addrKA and subrKA from GRing.Theory
|
|
|
|
|
|
|
|
|
|
|
|
pmap_cat, pmap_perm and perm_map_inj added
|
|
* Update README.md
|
|
itv_intersection, redefine prev_of_itv and itv_decompose using lersif, extend itv_rewrite, simplify proofs (#271)
|
|
Namely:
-projection-no-head-constant
-redundant-canonical-projection
-notation-overridden
|
|
|
|
* Add some theorems on lersif and intervals
* Add more theorems on lersif
* Remove needless parens
* ChangeLog
* Move lersifN
* Add lersif_anti
|
|
* Update INSTALL.md for installing mathcomp as local opam packages
This patch documents the change 1046da99d22462d6aeb23dd12043c2537f47abf1
that was required by the GitLab CI setup to be able to rely on opam 2.0.
Close #251
* Propose to bump the required version of coq in coq-mathcomp-ssreflect.opam
so the CI could use the Docker image coqorg/coq:8.9 (which is already available
albeit it currently is a synonymous of coqorg/coq:8.9-beta1 with the opam repos
coq-released + coq-core-dev + coq-extra-dev)
* [ci] Add math-comp/odd-order and coq-community/lemma-overloading jobs
Related: math-comp/math-comp#245 and math-comp/math-comp#256
|
|
|
|
Setup Docker-based configuration for GitLab CI
|
|
|
|
* This job is only instantiated with coqorg/coq:latest
* Add the associated Dockerfile.make
|
|
|
|
* Install coq-mathcomp-character in only 1 switch (cf. the build-arg $compiler)
* Remove the other switch
* Base the final image on coqorg/base:bare (which has no OCaml compiler layers)
|
|
* Design:
- build stage (e.g. docker build -t mathcomp-dev:$IID_$SLUG_coq-8.6 .)
- choice of the OCaml compiler: var OPAM_SWITCH in {base, edge}
(Dockerfile containing: "opam switch set $compiler && eval $(opam env)")
- master (protected branch) => push on GitLab registry and Docker Hub
- other branches (not tags) => push on GitLab registry
- Todo: GitHub PRs => push on GitLab
- test stage (image: mathcomp-dev:$IID_$SLUG_coq-8.6)
- script template foreach project (custom CONTRIB_URL, script)
- jobs foreach project and Coq version (custom COQ_VERSION, CONTRIB_VERSION)
* Config for protected branches:
- set vars HUB_REGISTRY, HUB_REGISTRY_USER, HUB_REGISTRY_IMAGE, HUB_TOKEN
* Remark:
- The name chosen for branches should ideally yield different values
of CI_COMMIT_REF_SLUG.
- But this is not mandatory as image tags start with "${CI_PIPELINE_IID}_".
cf. doc:
- CI_COMMIT_REF_NAME: The branch or tag name for which project is built.
- CI_COMMIT_REF_SLUG: $CI_COMMIT_REF_NAME lowercased, shortened to 63 bytes,
and with everything except 0-9 and a-z replaced with -.
No leading / trailing -. Use in URLs, host names and domain names.
- CI_PIPELINE_IID: The unique id of the current pipeline scoped to project.
|
|
|
|
|
|
"""
Failed checks on coq-mathcomp-ssreflect package definition from source
at file:///home/coq/mathcomp/ssreflect:
error 57: Synopsis and description must not be both empty
"""
|
|
* (Update make's path accordingly)
* This patch is required for opam 2.0 pinning
* As a result, these *.opam files are now similar to the opam files in
https://github.com/coq/opam-coq-archive/blob/master/extra-dev/packages/coq-mathcomp-*/coq-mathcomp-*.dev/
|
|
swap mingroup / maxgroup arguments
|
|
|
|
Moved set argument before predicate argument for mingroup and maxgroup
because Coq only displays notation with identifier parameters that are
both bound and free if there is at least one free occurrence to the
left of the binder.
|
|
Correct and improve implicits and documentation of MatrixGenField; also corrects changes in #262 to allow for a compatible fix in `odd-order`.
|
|
Refactored and completed implicit and scope signatures of constants of
MatrixGenField, the module that contains the construction of an
extension field for an irreducible representation, and for decidability
definitions.
Completed and corrected some errors in the corresponding header
documentation.
|
|
Cancel lemmas implicit
|
|
Like injectivity lemmas, instances of cancellation lemmas (whose
conclusion is `cancel ? ?`, `{in ?, cancel ? ?}`, `pcancel`, or
`ocancel`) are passed to
generic lemmas such as `canRL` or `canLR_in`. Thus such lemmas should
not have trailing on-demand implicits _just before_ the `cancel`
conclusion, as these would be inconvenient to insert (requiring
essentially an explicit eta-expansion).
We therefore use `Arguments` or `Prenex Implicits` directives to make
all such arguments maximally inserted implicits. We don’t, however make
other arguments implicit, so as not to spoil direct instantiation of
the lemmas (in, e.g., `rewrite -[y](invmK injf)`).
We have also tried to do this with lemmas whose statement matches a
`cancel`, i.e., ending in `forall x, g (E[x]) = x` (where pattern
unification will pick up `f = fun x => E[x]`).
We also adjusted implicits of a few stray injectivity
lemmas, and defined constants.
We provide a shorthand for reindexing a bigop with a permutation.
Finally we used the new implicit signatures to simplify proofs that
use injectivity or cancellation lemmas.
|
|
|
|
fix TFAE
|
