| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
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))
|
|
|
|
Reimplement the hierarchy related tools in OCaml
|
|
- 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
|
|
|
|
|
|
|
|
Namely:
-projection-no-head-constant
-redundant-canonical-projection
-notation-overridden
|
|
- countalg goes to the algebra package
- finalg now get the expected inheritance from countalg
- closed_field now contains the construction of algebraic closure for countable fields (previously in countalg)
- proof of quantifier elimination for closed field rewritten in a monadic style
|
|
|
|
|
|
|
|
|
|
|
|
The content of this file is similar to that of ssrfun.v and aims to
increase compatibility with Coq 8.6+ for third-party libraries that
depend on both math-comp and ssrmatching.v
Close #63
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
