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.4.tar.gz
sha512=1776f6fd142df8018546087f01d412e82fb629f7c653794dc2669b2016cd026e2e9c660a54211e1875d411092750dc6da8c2168ec3b1e1a5a810ee04676429bb

Description

This library provides ring, field, lra, nra, and psatz tactics for the Mathematical Components library. These tactics use the algebraic structures defined in the MathComp library and their canonical instances for the instance resolution, and do not require any special instance declaration, like the Add Ring and Add Field commands. Therefore, each of these tactics works with any instance of the respective structure, including concrete instances declared through Hierarchy Builder, abstract instances, and mixed concrete and abstract instances, e.g., int * R where R is an abstract commutative ring. 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: 25 Jan 2025

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.4~"
  5. coq >= "8.16" & < "9.1~"

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