package coq-mathcomp-algebra-tactics
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=c3b1275cb5662fe70b131a912979b19dbffde80ac28d97ca06a243737741dcb1
Description
This library provides ring
, field
, lra
, nra
, and psatz
tactics for
algebraic structures of the Mathematical Components library. The ring
tactic
works with any comRingType
(commutative ring) or comSemiRingType
(commutative semiring). The field
tactic works with any fieldType
(field).
The other (Micromega) tactics work with any realDomainType
(totally ordered
integral domain) or realFieldType
(totally ordered field). Algebra Tactics
do not provide a way to declare instances, like the Add Ring
and Add Field
commands, but use canonical structure inference instead. Therefore, each of
these tactics works with any canonical (or abstract) instance of the
respective structure declared through Hierarchy Builder. Another key feature
of Algebra Tactics is that they automatically push down ring morphisms and
additive functions to leaves of ring/field expressions before applying the
proof procedures.
Dependencies (5)
-
coq-elpi
>= "1.15.0" & != "1.17.0"
-
coq-mathcomp-zify
>= "1.5.0"
- coq-mathcomp-algebra
-
coq-mathcomp-ssreflect
>= "2.0" & < "2.1~"
-
coq
>= "8.16" & < "8.19~"
Dev Dependencies
None
Used by (2)
-
coq-infotheo
>= "0.7.0"
-
coq-mathcomp-apery
>= "1.0.2"
Conflicts
None