Algebra Tactics 1.2.3

This release is compatible with Coq 8.16 to 8.19, MathComp 2.0 to 2.2, Mczify 1.15, and Coq-Elpi 1.15 to 2.0 (except 1.17.0).

Algebra Tactics 1.2.2

This release fixes the issue (#87) that the ring and field tactics emit false deprecation warnings.

Algebra Tactics 1.2.1

This release fixes the issue that ring tactic actually does not work for commutative semirings.

Algebra Tactics 1.2.0

This release is compatible with Coq 8.16 to 8.18, MathComp 2.0, Mczify 1.15, and Coq-Elpi 1.15 to 1.19 (except 1.17.0).

• The ring tactic now supports commutative semirings as in the ring tactic of Coq, thanks to the semiRingType and comSemiRingType structures introduced in MathComp 2.0. All the provided tactics support semiring homomorphisms applied to semiring subexpressions as well.
• The lra, nra, and psatz tactics now support additive functions applied to Z-module or N-module subexpressions.
• The preprocessors now automatically compress homomorphisms from "initial objects" (nat, N, int, and Z) to the canonical ones (e.g., intr) and thus equate more variables.

EDIT: the ring tactic actually does not work for commutative semirings. This issue will be fixed in Algebra Tactics 1.2.1.

Algebra Tactics 1.1.1

This release fixes a minor issue regarding type casts in the goal.

Algebra Tactics 1.1.0

This release is compatible with Coq 8.16 to 8.17, MathComp 1.15 to 1.16, Mczify 1.1 to 1.3, and Coq-Elpi 1.15 to 1.17.1 (except 1.17.0).

• It provides the lra, nra, and psatz tactics for MathComp (contributed by Pierre Roux). For now, these tactics are considered experimental features and subject to change.
• All the provided tactics now support Nat.of_num_uint of type Number.uint -> nat without triggering computation in nat.

Algebra Tactics 1.0.0

This is the first stable release of Algebra Tactics, compatible with Coq 8.13 to 8.15, MathComp 1.12 to 1.14, Mczify 1.1 to 1.2, and Coq-Elpi 1.10.1 to 1.14.

• The provided tactics now report time spent for reification and reflection only when the #[verbose] attribute is supplied.
• The ring and field tactics do not accept implications as goals anymore. To reason modulo monomial equalities, the equalities have to be explicitly provided as arguments, e.g., ring: Ha Hb.

Algebra Tactics 0.3.0

This release is compatible with Coq 8.13 to 8.15, MathComp 1.12 to 1.14, Mczify 1.1 to 1.2, and Coq-Elpi 1.10.1 to 1.13. It fixes some performance issues, and provides experimental options to skip checking of some definitional equations that must hold regardless of whether the goal equation is valid or not, using the exact_no_check tactic:

Ltac ring_reflection ::= ring_reflection_no_check.
Ltac field_reflection ::= field_reflection_no_check.

Algebra Tactics 0.2.0

This release is compatible with Coq 8.13 to 8.15, MathComp 1.12 to 1.14, Mczify 1.1 to 1.2, and Coq-Elpi 1.10.1 to 1.12. It fixes some performance issues and an issue with the non-nullity conditions of the field tactic.

Algebra Tactics 0.1.0

This is the first release of Algebra Tactics, which provides ring and field tactics for Mathematical Components. It is compatible with Coq 8.13 to 8.14+rc1, MathComp 1.12, Mczify 1.1.0, and Coq-Elpi 1.10.1 to 1.11.2.