package coq-mathcomp-algebra-tactics
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=ce05b0b58232ea85bcfab1f33dc9bbeecb5dfc9b775d22b04fd82e1536559bec
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