aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-11-27Merge pull request #428 from maximedenes/build-docCyril Cohen
Add Makefile target to build the doc
2019-11-25Have to change directory before checking for the dependency fileYves Bertot
2019-11-25adds a comment so that dead code can be remove when it is no longer usedYves Bertot
2019-11-25dependency file will change name after coq-8.10Yves Bertot
2019-11-25things that are needed to make 'make doc' workYves Bertot
2019-11-25Add missing dependenciesMaxime Dénès
Spotted by Yves.
2019-11-25Add Makefile target to build the docMaxime Dénès
2019-11-25remove duplicated sentence in CHANGELOG_UNRELEASEDCyril Cohen
2019-11-24Merge pull request #438 from pi8027/hint-databaseCyril Cohen
Fix hint declarations to specify the database explicitly
2019-11-25Fix hint declarations to specify the database explicitlyKazuhiko Sakaguchi
2019-11-23Merge pull request #437 from pi8027/gitignore-vos-vokCyril Cohen
Add *.vos and *.vok to .gitignore
2019-11-22Add *.vos and *.vok to .gitignoreKazuhiko Sakaguchi
2019-11-22Injectivity lemmas in fintype (#426)Kazuhiko Sakaguchi
2019-11-22Added ssrfun theorem `inj_compr` (#432)Cyril Cohen
2019-11-22New generalised induction idiom (#434)Georges Gonthier
Replaced the legacy generalised induction idiom with a more robust one that does not rely on the `{-2}` numerical occurrence selector, using either new helper lemmas `ubnP` and `ltnSE` or a specific `nat` induction principle `ltn_ind`. Added (non-strict in)equality induction helper lemmas Added `ubnP[lg]?eq` helper lemmas that abstract an integer expression along with some (in)equality, in preparation for some generalised induction. Note that while `ubnPleq` is very similar to `ubnP` (indeed `ubnP M` is basically `ubnPleq M.+1`), `ubnPgeq` is used to remember that the inductive value remains below the initial one. Used the change log to give notice to users to update the generalised induction idioms in their proofs to one of the new forms before Mathcomp 1.11.
2019-11-20Merge pull request #399 from CohenCyril/ltn_subYves Bertot
More arithmetic theorems
2019-11-19Merge pull request #420 from pi8027/all-lemmasCyril Cohen
Add all_filter, all_pmap, and all_allpairsP in seq.v
2019-11-18fixing CHANGELOG and ltn_pred lemmasCyril Cohen
2019-11-18Documenting `L` and `R` in `CONTRIBUTING.md`Cyril Cohen
2019-11-18More arithmetic theoremsCyril Cohen
- Generalizing `ltn_subr` - Adding `ltn_subl` and `ltn_subr` - Changing conclusion of `ltn_predl` to `0 < n` instead of `n != 0`
2019-11-18Merge pull request #381 from hivert/seqYves Bertot
More lemmas on seqs
2019-11-15More lemmas on seqsFlorent Hivert
2019-11-15fix in ssralg (#421)Cyril Cohen
* missing exports of lemmas `commrB`, `commr_sum` and `commr_prod` * missing `regular_*` canonical exports
2019-11-15Add all_filter, all_pmap, and all_allpairsP in seq.vKazuhiko Sakaguchi
2019-11-14Merge pull request #423 from thery/docYves Bertot
typo
2019-11-14typothery
2019-11-14fingraph: remove fin_inj_bij lemma as duplicate of injF_bij from fintype (#403)Anton Trunov
2019-11-14Lemmas on commutation with big sum and prod (#413)Florent Hivert
* Lemmas on commutation with big sum and prod * Added commrB Lemma * @CohenCyril review * apply -> apply:
2019-11-14Update pull_request_template.mdCyril Cohen
2019-11-14Update zmodp.v (#411)Gabriel Taumaturgo
2019-11-14some information about naming conventions for definitions (wip) (#415)affeldt-aist
2019-11-14typo (#412)Laurent Théry
2019-11-06Merge pull request #410 from GTaumaturgo/patch-1Cyril Cohen
Update README.md
2019-11-06Merge pull request #408 from chdoc/existsPnCyril Cohen
add existsPn/forallPn lemmas
2019-11-06Merge pull request #406 from hivert/algebrasCyril Cohen
Commutative Algebras
2019-11-04Update README.mdGabriel Taumaturgo
2019-11-04Fixed the documentationFlorent Hivert
2019-11-04minor revisionChristian Doczkal
2019-11-04Fixed inheritance of fieldExt / fieldOver / splitting fieldFlorent Hivert
2019-11-04add existsPn/forallPn lemmasChristian Doczkal
2019-11-03Interface for commutative and commutative-unitary algebrasFlorent Hivert
Initial properties of polynomials in R-algebras
2019-10-31Merge pull request #378 from pi8027/fix-ltngtPCyril Cohen
Reorder the arguments in `compare_nat` and `ltngtP`
2019-10-30Change the order of arguments in `ltngtP`Kazuhiko Sakaguchi
from `ltngtP m n : compare_nat m n (m <= n) (n <= m) (m < n) (n < m) (n == m) (m == n)` to `ltngtP m n : compare_nat m n (n == m) (m == n) (n <= m) (m <= n) (n < m) (m < n)`, to make it tries to match subterms with `m < n` first, `m <= n`, then `m == n`.
2019-10-30Merge pull request #400 from pi8027/scale-typeCyril Cohen
Add an explicit type annotation to GRing.scale
2019-10-26Add an explicit type annotation to GRing.scaleKazuhiko Sakaguchi
`V` was wrongly eta-expanded before: GRing.scale : forall (R : ringType) (V : lmodType R), R -> GRing.Zmodule.Pack (GRing.Lmodule.class V) -> GRing.Zmodule.Pack (GRing.Lmodule.class V)
2019-10-26Merge pull request #397 from CohenCyril/remove_addnKCLaurent Théry
Removing duplicate lemma `addnKC` (= `addKn`)
2019-10-25Removing duplicate lemma `addnKC` (= `addKn`)Cyril Cohen
2019-10-25Merge pull request #396 from CohenCyril/edivnDLaurent Théry
More arithmetic theorems
2019-10-25Instances for empty type. (#393)Arthur Azevedo de Amorim
* Add notation and instances for empty type. * Update change log. * Mention void in fintype header. * Remove unnecessary explicit argument. * Documentation header for void.
2019-10-25Stability proofs of sort (#358)Kazuhiko Sakaguchi
* Modified the definition of sort to work on any type * Other Generalizations, fixes and CHANGELOG entry * Add stability lemmas for `path.sort` - Inverse the comparison in `merge` and swap arguments of it everywhere. - Add `sort_rec1` and `sortE` to simplify inductive proofs on `sort`. - Add `seq.mask_filter`, `mem2E`, `path_mask`, `path_filter`, and `sorted_mask`. - Generalize `sorted_filter`, `homo_path_in`, `mono_path_in`, `homo_sorted_in`, and `mono_sorted_in` to non-`eqType`s. - Add the following lemmas to state the stability of `path.merge` and `path.sort`. sorted_merge : forall (T : Type) (leT : rel T), transitive leT -> forall s t : seq T, sorted leT (s ++ t) -> merge leT s t = s ++ t merge_stable_path : forall (T : Type) (leT leT' : rel T), total leT -> forall (x : T) (s1 s2 : seq T), all (fun y : T => all (leT' y) s2) s1 -> path [rel x0 y | leT x0 y && (leT y x0 ==> leT' x0 y)] x s1 -> path [rel x0 y | leT x0 y && (leT y x0 ==> leT' x0 y)] x s2 -> path [rel x0 y | leT x0 y && (leT y x0 ==> leT' x0 y)] x (merge leT s1 s2) merge_stable_sorted : forall (T : Type) (leT leT' : rel T), total leT -> forall s1 s2 : seq T, all (fun x : T => all (leT' x) s2) s1 -> sorted [rel x y | leT x y && (leT y x ==> leT' x y)] s1 -> sorted [rel x y | leT x y && (leT y x ==> leT' x y)] s2 -> sorted [rel x y | leT x y && (leT y x ==> leT' x y)] (merge leT s1 s2) sorted_sort : forall (T : Type) (leT : rel T), transitive leT -> forall s : seq T, sorted leT s -> sort leT s = s sort_stable : forall (T : Type) (leT leT' : rel T), total leT -> transitive leT' -> forall s : seq T, sorted leT' s -> sorted [rel x y | leT x y && (leT y x ==> leT' x y)] (sort leT s) filter_sort : forall (T : Type) (leT : rel T), total leT -> transitive leT -> forall (p : pred T) (s : seq T), [seq x <- sort leT s | p x] = sort leT [seq x <- s | p x] mask_sort : forall (T : Type) (leT : rel T), total leT -> transitive leT -> forall (s : seq T) (m : bitseq), {m_s : bitseq | mask m_s (sort leT s) = sort leT (mask m s)} mask_sort' : forall (T : Type) (leT : rel T), total leT -> transitive leT -> forall (s : seq T) (m : bitseq), sorted leT (mask m s) -> {m_s : bitseq | mask m_s (sort leT s) = mask m s} subseq_sort : forall (T : eqType) (leT : rel T), total leT -> transitive leT -> {homo sort leT : t s / subseq t s} subseq_sort' : forall (T : eqType) (leT : rel T), total leT -> transitive leT -> forall t s : seq T, subseq t s -> sorted leT t -> subseq t (sort leT s) mem2_sort : forall (T : eqType) (leT : rel T), total leT -> transitive leT -> forall (s : seq T) (x y : T), leT x y -> mem2 s x y -> mem2 (sort leT s) x y * Avoid some eta-expansions * Get the proper fix of `order_path_min` and remove `sort_map_in` * Update documentation and CHANGELOG entries
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 17:38:01 +0000