| 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.
|
|
|
|
|
|
|
|
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.
|
