| Age | Commit message (Collapse) | Author |
|---|
|
Adding lemma sumnB
|
|
cf https://stackoverflow.com/questions/61556710
|
|
- The `deprecate` notation and `iota_add` have been deprecated. All the uses of
the `deprecate` notation have been replaced with the `deprecated` attribute.
- Deprecation aliases in `ssrnat` and `ssrnum` introduced in MathComp 1.11+beta1
have been removed.
- Remove `VDFILE` related hacks from `Makefile.common`.
|
|
|
|
Using Coq 8.10 ssreflect new features
|
|
|
|
|
|
|
|
- Rename `eq_sorted` lemmas to `sorted_eq` to address a naming inconsistency.
- Lemma `sort_le_id` has been generalized from `orderType` to `porderType`.
|
|
|
|
|
|
New `big_uncond` and `big_rmcond -> big_rmcond_in`
|
|
|
|
+ eq_liftF and lift_eqF
+ proof simplificaions
|
|
- Lemma `big_rmcond` has been renamed `big_rmcomd_in` and the variant which does not require an `eqType` has been added and named `big_uncond`.
- The name `big_rmcond` is deprecated and will be reused for `big_uncond` in the next version of math-comp
- Additionally `big_uncond_in` is made available for uniformity, but is already deprecated.
|
|
|
|
|
|
|
|
|
|
- deprecating `fintype.arg_(min|max)P`
- removing dangling comments connecting min max and meet join
- better compatibility module
- removing broken notations with `\min` and `\max` (no neutral available)
- fixing `incompare` and `incomparel` in order.v
- adding missing elimination lemmas (`(comparable_)?(max|min)E[lg][et]`)
- adding missing `(comparable|real)_arg(min|max)P`
- CHANGELOG update
|
|
|
|
This change reduces
- use of numerical occurrence selectors (#436) and
- use of non ssreflect tactics such as `auto`,
and improves use of comparison predicates such as `posnP`, `leqP`, `ltnP`,
`ltngtP`, and `eqVneq`.
|
|
Documentation typos
|
|
|
|
fixes #418
|
|
|
|
- Replace `altP eqP` and `altP (_ =P _)` with `eqVneq`:
The improved `eqVneq` lemma (#351) is redesigned as a comparison predicate and
introduces a hypothesis in the form of `x != y` in the second case. Thus,
`case: (altP eqP)`, `case: (altP (x =P _))` and `case: (altP (x =P y))` idioms
can be replaced with `case: eqVneq`, `case: (eqVneq x)` and
`case: (eqVneq x y)` respectively. This replacement slightly simplifies and
reduces proof scripts.
- use `have [] :=` rather than `case` if it is better.
- `by apply:` -> `exact:`.
- `apply/lem1; apply/lem2` or `apply: lem1; apply: lem2` -> `apply/lem1/lem2`.
- `move/lem1; move/lem2` -> `move/lem1/lem2`.
- Remove `GRing.` prefix if applicable.
- `negbTE` -> `negPf`, `eq_refl` -> `eqxx` and `sym_equal` -> `esym`.
|
|
Added lemmas `big_enum_cond`, `big_enum` and `big_enumP` to handle more
explicitly big ops iterating over explicit enumerations in a `finType`.
The previous practice was to rely on the convertibility between
`enum A` and `filter A (index_enum T)`, sometimes explicitly via the
`filter_index_enum` equality, more often than not implicitly.
Both are likely to fail after the integration of `finmap`, as the
`choiceType` theory can’t guarantee that the order in selected
enumerations is consistent.
For this reason `big_enum` and the related (but currently unused)
`big_image` lemmas are restricted to the abelian case. The `big_enumP`
lemma can be used to handle enumerations in the non-abelian case, as
explained in the `bigop.v` internal documentation.
The Changelog entry enjoins clients to stop relying on either
`filter_index_enum` and convertibility (though this PR still provides
both), and warns about the restriction of the `big_image` lemma set to
the abelian case, as it it a possible source of incompatibility.
|
|
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.
|
|
|
|
### Added
- Fintype theorems: `fintype0`, `card_le1P`, `mem_card1`,
`card1P`, `fintype_le1P`, `fintype1`, `fintype1P`.
- Bigop theorems: `big_rmcond`, `bigD1_seq`,
`reindex_enum_val_cond`, `reindex_enum_rank_cond`,
`reindex_enum_val`, `reindex_enum_rank`, `big_set`.
|
|
- Change the naming of permutation lemmas so they conform to a
consistent policy: `perm_eq` lemmas have a `perm_` (_not_ `perm_eq`)
prefix, or sometimes a `_perm` suffix for lemmas that _prove_ `perm_eq`
using a property when there is also a lemma _using_ `perm_eq` for the
same property. Lemmas that do not concern `perm_eq` do _not_ have
`perm` in their name.
- Change the definition of `permutations` for a time- and space-
back-to-front generation algorithm.
- Add frequency tally operations `tally`, `incr_tally`, `wf_tally` and
`tally_seq`, used by the improved `permutation` algorithm.
- add deprecated aliases for renamed lemmas
|
|
|
|
|
|
|
|
```
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
```
|
|
|
|
|
|
|
|
|
|
It was emitting a deprecation warning and will soon be removed from Coq.
|
|
|
|
|
