package coq-mathcomp-algebra-tactics

  1. Overview
  2. Homepage
Ring, field, lra, nra, and psatz tactics for Mathematical Components

Install

Dune Dependency

Authors

Maintainers

Sources

1.2.0.tar.gz
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.

Tags

logpath:mathcomp.algebra_tactics

Published: 28 Sep 2023

Dependencies (5)

  1. coq-elpi >= "1.15.0" & != "1.17.0"
  2. coq-mathcomp-zify >= "1.5.0"
  3. coq-mathcomp-algebra
  4. coq-mathcomp-ssreflect >= "2.0" & < "2.1~"
  5. coq >= "8.16" & < "8.19~"

Dev Dependencies

None

Used by (2)

  1. coq-infotheo >= "0.7.0"
  2. coq-mathcomp-apery >= "1.0.2"

Conflicts

None

Rocq

Interactive Theorem Prover