| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
silencing warnings in individual packages
|
|
|
|
|
|
|
|
|
|
- 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
|
|
- mostly gathered the changes from previous commits
- add `minrC`
- minor doc addition to `order.v`
|
|
- min and max can now be used in a partial order (sometimes under preconditions)
- min and max can now be used in a numDomainType (sometimes under preconditions)
|
|
- `Order.max` and `Order.min` are now convertible to `maxn` and `minn`
- Inserting `(fun _ _ => erefl)` in `LeOrderMixin` and `LtOrderMixin`
gives `meet`/`join` which are convertible to `min`/`max`
- `Order.max` and `Order.min` are not convertible to former `Num.max` and `Num.min`
|
|
- max and min are not defined in terms or meet and join anymore
- extremum_inP is a generalization of extremum suitable for a partial order
- arg_min and arg_max are usable in a porderType
- equivalences between min and meet, and max and join are proven for orderType
- leP, ltP, ltgtP, and `[l]?comparable_.*P` lemmas have been generalized to take this into account
- total_display was completely removed
|
|
Lemma addition to ssrnum
|
|
|
|
* Missing mono lemmas
|
|
|
|
|
|
|
|
|
|
mathcomp-analysis project
|
|
|
|
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`.
|
|
Remove the tuple extensions in order.v that is available in tuple.v
|
|
|
|
This fixes two issues:
- dual_finLatticeType was missing, and
- dual_finDistrLatticeType was just an identity function.
|
|
In particular: rephrased permS0 and permS1 with all_equal_to
|
|
|
|
|
|
adding deprecations in ssrnat
|
|
|
|
|
|
fixes #469
|
|
switching long suffixes to short suffixes
|
|
Remove hint declarations using non-global definitions.
|
|
+ `odd_add` -> `oddD`
+ `odd_sub` -> `oddB`
+ `take_addn` -> `takeD`
+ `rot_addn` -> `rotD`
+ `nseq_addn` -> `nseqD`
fixes #359
|
|
Documentation typos
|
|
|
|
|
|
the->this
Co-Authored-By: Yves Bertot <yves.bertot@inria.fr>
|
|
|
|
|
|
Rewriting with AC (not modulo AC), using a small scale command.
|
|
|
|
%AC annotation are for backward compatilibity with coq <= 8.9
|
|
This replaces opA, opC, opAC, opCA, ... and any combinations of them
- Right now the rewrite relies on an rather efficient computation
of perm_eq using a "spaghetti sort" in O(n log n)
- Wrongly formed AC statements send error messages showing the
discrepancy between LHS and RHS patterns.
Usage :
rewrite [pattern](AC operator pattern-shape re-ordering)
rewrite [pattern](ACl operator re-ordering)
- pattern is optional, as usual,
- operator must have a canonical Monoid.com_law structure
(additions, multiplications, conjunction and disjunction do)
- pattern-shape is expressed using the syntax
p := n | p * p'
where "*" is purely formal
and n > 0 is number of left associated symbols
examples of pattern shapes:
+ 4 represents (n * m * p * q)
+ (1*2) represents (n * (m * p))
- re-ordering is expressed using the syntax
s := n | s * s'
where "*" is purely formal and n is the position in the LHS
If the ACl variant is used, the pattern-shape defaults to the
pattern fully associated to the left i.e. n i.e (x * y * ...)
Examples of re-orderings:
- ACl op ((0*1)*2) is the identity (and should fail to rewrite)
- opAC == ACl op ((0*2)*1) == AC op 3 ((0*2)*1)
- opCA == AC op (2*1) (0*1*2)
- rewrite opCA -opA == rewrite (ACl op (0*(2*1))
- opACA == AC (2*2) ((0*2)*(1*3))
|
|
|
|
remove deprecated commands whose deprecation was introduced in 1.9.0
|
