Library functional_algebra.ring

This module defines the Ring record type which can be used to represent algebraic rings and provides a collection of axioms and theorems describing them. Copyright (C) 2018 Larry D. Lee Jr. <llee454@gmail.com> This program is free software: you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. You should have received a copy of the GNU Lesser General Public License along with this program. If not, see <https://www.gnu.org/licenses/>.

Accepts two binary functions, f and g, and asserts that f is left distributive over g.

Accepts two binary functions, f and g, and asserts that f is right distributive over g.

Accepts two binary functions, f and g, and asserts that f is distributive over g.

Represents algebraic rings

Represents the set of ring elements.

Represents 0 - the additive identity.

Represents 1 - the multiplicative identity.

Represents addition.

Represents multiplication.

Asserts that 0 /= 1.

Asserts that addition is associative.

Asserts that addition is commutative.

Asserts that E_0 is the left identity element.

Asserts that every element has an additive inverse.

Asserts that multiplication is associative.

Asserts that 1 is the left identity element.

Asserts that 1 is the right identity element.

Asserts that multiplication is left distributive over addition.

Asserts that multiplication is right distributive over addition.

Enable implicit arguments for ring properties.

Define notations for ring properties.

Represents an arbitrary ring. Note: we use Variable rather than Parameter to ensure that the following theorems are generalized w.r.t r.

Represents the set of group elements. Note: We use Let to define E as a local abbreviation.

A predicate that accepts one element, x, and asserts that x is nonzero.

Accepts one ring element, x, and asserts that x is the left identity element.

Accepts one ring element, x, and asserts that x is the right identity element.

Accepts one ring element, x, and asserts that x is the identity element.

Represents the abelian group formed by addition over E.

Represents the group formed by addition over E.

Represents the monoid formed by addition over E.

Proves that 0 is the right identity element.

Proves that 0 is the identity element.

Accepts two elements, x and y, and asserts that y is x's left inverse.

Accepts two elements, x and y, and asserts that y is x's right inverse.

Accepts two elements, x and y, and asserts that y is x's inverse.

Asserts that every element has a right inverse.

Proves that the left identity element is unique.

Proves that the right identity element is unique.

Proves that the identity element is unique.

Proves that for every group element, x, its left and right inverses are equal.

Proves that the inverse relation is symmetrical.

Proves that an element's inverse is unique.

Proves that every group element has an inverse.

Proves explicitly that every element has a unique inverse.

Proves the left introduction rule.

Proves the right introduction rule.

Proves the left cancellation rule.

Proves the right cancellation rule.

Proves that an element's left inverse is unique.

Proves that an element's right inverse is unique.

TODO: move the following theorems about 0 to monoid. Proves that 0 is its own left additive inverse.

Proves that 0 is its own right additive inverse.

Proves that 0 is it's own additive inverse.

Proves that if an element's, x, additive inverse equals 0, x equals 0.

Proves that 0 is the only element whose additive inverse is 0.

Represents strongly-specified negation.

Represents negation.

Asserts that the negation returns the inverse of its argument.

Proves that negation is one-to-one

Proves the cancellation property for negation.

Proves that negation is onto

Proves that negation is surjective

Proves that neg x = y -> neg y = x

Accepts one element, x, and asserts that x is the left identity element.

Accepts one element, x, and asserts that x is the right identity element.

Accepts one element, x, and asserts that x is the identity element.

Represents the monoid formed by op over E.

Proves that 1 is the identity element.

Proves that the left identity element is unique.

Proves that the right identity element is unique.

Proves that the identity element is unique.

Proves the left introduction rule.

Proves the right introduction rule.

Accepts two elements, x and y, and asserts that y is x's left inverse.

Accepts two elements, x and y, and asserts that y is x's right inverse.

Accepts two elements, x and y, and asserts that y is x's inverse.

Accepts one argument, x, and asserts that x has a left inverse.

Accepts one argument, x, and asserts that x has a right inverse.

Accepts one argument, x, and asserts that x has an inverse.

Proves that the left and right inverses of an element must be equal.

Proves that the inverse relationship is symmetric.

Proves the left cancellation law for elements possessing a left inverse.

Proves the right cancellation law for elements possessing a right inverse.

Proves that an element's left inverse is unique.

Proves that an element's right inverse is unique.

Proves that an element's inverse is unique.

Proves that 1 is its own left multiplicative inverse.

Proves that 1 is its own right multiplicative inverse.

Proves that 1 is its own recriprical.

Proves that 1 has a left multiplicative inverse.

Proves that 1 has a right multiplicative inverse.

Proves that 1 has a reciprical

TODO Reciprical functions (op_neg) from Monoid. Asserts that multiplication is distributive over addition.

Proves that 0 times every number equals 0. 0 x = 0 x (0 + 0) x = 0 x 0 x + 0 x = 0 x 0 x = 0

Proves that 0 times every number equals 0.

Proves that 0 does not have a left multiplicative inverse.

Proves that 0 does not have a right multiplicative inverse.

Proves that 0 does not have a multiplicative inverse - I.E. 0 does not have a reciprocal.

Proves that multiplicative inverses, when they exist are always nonzero.

Represents -1 and proves that it exists.

Represents -1.

Defines a symbolic representation for -1 Note: here we represent the inverse of 1 rather than the negation of 1. Letter we prove that the negation equals the inverse. Note: brackets are needed to ensure Coq parses the symbol as a single token instead of a prefixed function call.

Asserts that -1 is the additive inverse of 1.

Asserts that -1 is the left inverse of 1.

Asserts that -1 is the right inverse of 1.

Asserts that every additive inverse of 1 must be equal to -1.

Proves that -1 * x equals the multiplicative inverse of x.

• 1 x + x = 0
• 1 x + 1 x = 0

(-1 + 1) x = 0 0 x = 0 0 = 0

Proves that x * -1 equals the multiplicative inverse of x. x -1 + x = 0

Proves that x + -1 x = 0.

Proves that x + x -1 = 0.

Proves that -1 x is the additive inverse of x.

Proves that x -1 is the additive inverse of x.

Proves that multiplying by -1 is equivalent to negation.

Accepts one element, x, and proves that x -1 equals the additive negation of x.

Accepts one element, x, and proves that

• 1 x equals the additive negation of x.

Proves that -1 x = x -1.

Proves that the additive negation of 1 equals -1.

Proves that the additive negation of -1 equals 1.

Proves that -1 * -1 = 1.

• 1 * -1 = -1 * -1
• 1 * -1 = prod -1 -1
• 1 * -1 = - -1
• 1 * -1 = 1

Proves that -1 is its own multiplicative inverse.