This package provides a Coq formalization of abstract algebra using a functional programming style. The modules contained within the package span monoids, groups, rings, and fields and provides both axiom definitions for these structures and proofs of foundational results. The current package contains over 800 definitions and proofs.
This initial release includes definitions and theorems for algebraic structures ranging from monoids to fields. It includes proofs of all of the basic theorems that apply to these structures and includes expression simplifiers for monoids and groups. The expression simplifier for groups does not yet simplify negations, but provides a basis for further development.
This release satisfies its initial goals by providing a substantial worked example illustrating a functional programming style in Coq and by showing how proof by reflection can be used to automate routine algebraic rewrite steps when developing proofs in this manner.
Note: this release is actually a minor edit to the 1.0.1 release. I've updated the _CoqProject file by renaming the build target. Previously, it had been "functional-algebra", now it is "functional_algebra." This resolves a Make error. I regenerated the Makefile, and the package compiles under Coq version 8.8.1. Coqc throws two warnings however because I shadow global variables within a section, but I believe that this practice is justified in the two instances where it occurs.
This initial release includes definitions and theorems for algebraic structures ranging from monoids to fields. It includes proofs of all of the basic theorems that apply to these structures and includes expression simplifiers for monoids and groups. The expression simplifier for groups does not yet simplify negations, but provides a basis for further development.
This release satisfies its initial goals by providing a substantial worked example illustrating a functional programming style in Coq and by showing how proof by reflection can be used to automate routine algebraic rewrite steps when developing proofs in this manner.
Note: this release is actually a minor edit to the 1.0.0 release. I've added the LGPLv3 license file and notification to all source files.
This initial release includes definitions and theorems for algebraic structures ranging from monoids to fields. It includes proofs of all of the basic theorems that apply to these structures and includes expression simplifiers for monoids and groups. The expression simplifier for groups does not yet simplify negations, but provides a basis for further development.
This release satisfies its initial goals by providing a substantial worked example illustrating a functional programming style in Coq and by showing how proof by reflection can be used to automate routine algebraic rewrite steps when developing proofs in this manner.