| Age | Commit message (Collapse) | Author |
|---|
|
|
|
fixes #469
|
|
switching long suffixes to short suffixes
|
|
+ `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>
|
|
|
|
|
|
%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
|
|
Extend comparison predicates for nat with minn and maxn and reorder arguments of those in order.v
|
|
fixes #418
|
|
Find
|
|
Co-Authored-By: Kazuhiko Sakaguchi <pi8027@gmail.com>
|
|
|
|
|
|
|
|
Non-distributive lattice structures
|
|
|
|
|
|
|
|
Adapt to coq/coq#11368 (Turn trailing implicit warning into an error)
|
|
|
|
|
|
|
|
Indeed, the name converse and notation ^c were already taken in
https://github.com/math-comp/math-comp/blob/master/mathcomp/algebra/ssralg.v#L989-L990
We are renaming to dual.
|
|
|
|
- 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`.
|
|
|
|
|
|
- adding a doc paragraph on displays
- Changelog
- better proofs for new logn, gcdn, lcmn, partn facts
- Putting comments in the example of nat
|
|
|
|
|
|
|
|
scopes
|
|
- Rename `totalLatticeMixin` to `totalPOrderMixin`.
- Refactor num mixins.
- Use `Num.min` and `Num.max` rather than lattice notations if applicable.
|
|
New lemmas:
- meet_l, meet_r, join_l, join_r.
Renamings:
- Order.BLatticeTheory.lexUl -> disjoint_lexUl,
- Order.BLatticeTheory.lexUr -> disjoint_lexUr,
- Order.TBLatticeTheory.lexIl -> cover_leIxl,
- Order.TBLatticeTheory.lexIr -> cover_leIxr.
Use `Order.TTheory` instead of `Order.Theory` if applicable
|
|
The comparison predicates (for nat, ordered types, ordered integral domains)
must have the following order of arguments:
- leP x y : le_xor_gt x y ... (x <= y) (y < x) ... .
- ltP x y : lt_xor_ge x y ... (y <= x) (x < y) ... .
- ltgtP x y : compare x y ... (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y) ... .
|
|
- comparer -> compare (in order.v)
- eq constructor of compare goes last
- "x < y" is matched before "x > y"
- "x <= y" is matched before "x >= y"
- adding prod and lexi ordering on tuple
- adding missing CS
- edit CHANGELOG
|
|
|
|
#283, #285, #286, #288, #296, #330, #334, and #341)
ssrnum related changes:
- Redefine the intermediate structure between `idomainType` and `numDomainType`,
which is `normedDomainType` (normed integral domain without an order).
- Generalize (by using `normedDomainType` or the order structures), relocate
(to order.v), and rename ssrnum related definitions and lemmas.
- Add a compatibility module `Num.mc_1_9` and export it to check compilation.
- Remove the use of the deprecated definitions and lemmas from entire theories.
- Implement factories mechanism to construct several ordered and num structures
from fewer axioms.
order related changes:
- Reorganize the hierarchy of finite lattice structures. Finite lattices have
top and bottom elements except for empty set. Therefore we removed finite
lattice structures without top and bottom.
- Reorganize the theory modules in order.v:
+ `LTheory` (lattice and partial order, without complement and totality)
+ `CTheory` (`LTheory` + complement)
+ `Theory` (all)
- Give a unique head symbol for `Total.mixin_of`.
- Replace reverse and `^r` with converse and `^c` respectively.
- Fix packing and cloning functions and notations.
- Provide more ordered type instances:
Products and lists can be ordered in two different ways: the lexicographical
ordering and the pointwise ordering. Now their canonical instances are not
exported to make the users choose them.
- Export `Order.*.Exports` modules by default.
- Specify the core hint database explicitly in order.v. (see #252)
- Apply 80 chars per line restriction.
General changes:
- Give consistency to shape of formulae and namings of `lt_def` and `lt_neqAle`
like lemmas:
lt_def x y : (x < y) = (y != x) && (x <= y),
lt_neqAle x y : (x < y) = (x != y) && (x <= y).
- Enable notation overloading by using scopes and displays:
+ Define `min` and `max` notations (`minr` and `maxr` for `ring_display`) as
aliases of `meet` and `join` specialized for `total_display`.
+ Provide the `ring_display` version of `le`, `lt`, `ge`, `gt`, `leif`, and
`comparable` notations and their explicit variants in `Num.Def`.
+ Define 3 variants of `[arg min_(i < n | P) F]` and `[arg max_(i < n | P) F]`
notations in `nat_scope` (specialized for nat), `order_scope` (general
version), and `ring_scope` (specialized for `ring_display`).
- Update documents and put CHANGELOG entries.
|
|
|
|
needed lemmas (#261)
* adds relevant theorems when fcycle f (orbit f x) and the needed lemmas
* Generalize f_step lemmas
* Generalizations, shorter proofs, bugfixes, CHANGELOG
- changelog, renamings and comments
- renaming `homo_cycle` to `mem_fcycle` and other small renamings
- name swap `mem_orbit` and `in_orbit`
- simplifications
- generalization following @pi8027's comment
- Getting rid of many uniquness condition in `fingraph.v`
- added cases to the equivalence `orbitPcycle`
- added `cycle_catC`
|
|
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.
|
|
|
|
|
|
|
