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