algebra-tactics
algebra-tactics copied to clipboard
math-comp
Ring, field, lra, nra, and psatz tactics for Mathematical Components
Since the issue has been fixed on the Coq side (coq/coq#18166), we should be able to revert #90 (after the release of Coq 8.18.1 or 8.19).
Files in `examples/` have two roles: - examples showing the features of Algebra Tactics, and - test-suite. I see the following three issues: - Currently, these two things are kind...
Short term: - [x] Avoid [hypotheses search triggered by `exact`](https://github.com/math-comp/algebra-tactics/pull/54#discussion_r1029139823). This can be a source of [a significant slowdown](https://github.com/math-comp/algebra-tactics/pull/72#issuecomment-1326671256). - Done in #74, but does not fix the slowdown. -...
It would be nice to support commutative and non-commutative algebras in general. The interesting part would be that scalars are still commutative in non-commutative algebras and thus requires a new...
Thanks to coq/coq#15921, it should be possible to reimplement mczify in the preprocessing approach of Algebra Tactics. I'm curious how much we could improve the performance (of Apery for example)...
I should investigate this at some point, but I'm not sure if 100 is large enough: https://github.com/math-comp/algebra-tactics/blob/0b8356c0168fc91b8355d2507343f3d5fdacff05/theories/ring.v#L654 Coq uses 1000 instead: https://github.com/coq/coq/blob/110921a449fcb830ec2a1cd07e3acc32319feae6/theories/setoid_ring/Ring_tac.v#L340 I think we should at least give a...
Currently, Algebra Tactics do not provide `ring_simplify`. I would like to implement it at some point.
opam package
Hi @pi8027 , I have an opam switch with coq 8.13.1, and I get the following error message when trying to install your library with opam, following the instructions in...
Although it may lead to some performance issues.