Library functional_algebra.field

This module defines the Field record type which can be used to represent algebraic fields and provides a collection of axioms and theorems describing them. Algebraic fields are rings in which every *non-zero* element has a multiplicative inverse. The subset of elements that have inverses form a group w.r.t multiplication. 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/>.

Represents algebraic fields.

Represents the set of 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 0 is the left identity element.

Asserts that every element has an additive inverse.

Asserts that multiplication is associative.

Asserts that multiplication is commutative.

Asserts that 1 is the left identity element.

Asserts that every *non-zero* element has a multiplicative inverse. Note: this is the property that distinguishes fields from commutative rings.

Asserts that multiplication is left distributive over addition.

Enable implicit arguments for field properties.

Define notations for field properties.

Represents an arbitrary commutative 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.

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.

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 commutative ring that addition and multiplication form over E.

Represents the non-commutative ring formed by addition and multiplication over E.

Represents the abelian group formed by addition over E.

Represents the abelian group formed by addition over E.

Represents the monoid formed by addition over E.

Represents the monoid formed by multiplication over E.

Proves that 1 <> 0.

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

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 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.

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 1 is the right identity element.

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

Proves that the left identity element is unique.

Proves that the right identity element is unique.

Proves that the right 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 every left inverse must also be a right inverse.

Proves that every non-zero element has a right multiplicative inverse.

Proves that every non-zero element has a multiplicative 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 every nonzero element has a unique inverse.

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

Proves that multiplication is right distributive over addition.

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.

Proves that the product of two non-zero values is non-zero. x * y <> 0 x * y = 0 -> False assume x * y = 0 1/x * x * y = 1/x * 0 y = 0 which is a contradiction.

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.

Proves that -1 is nonzero.

Represents the reciprical operation.

Represents the reciprical operation.

Proves that the reciprical operation correctly returns the inverse of the given element.

Proves that (1/-1) = -1.

Proves that recipricals are nonzero.

Proves that 1/(1/x) = x

Represents division.

Proves that x y/x = y.

Proves that x/y y = x.

The following section proves that the set of nonzero elements forms an algebraic group over multiplication with 1 as the identity. To show this, we map every nonzero field element, x, onto a dependent product, (x, H), where H represents a proof that x is nonzero. We then define equality over these products such that two pair, (x, H) and (y, H0), are equal whenever x and y are. Continuing, we define multiplication reasonably so that (x, H) (y, H0) = (x * y, H1) where denotes multiplication over pairs. With these definitions in hand, we show that the resulting elements form a group and that this group is isomorphic with the set of nonzero field elements. Represents those field elements that are nonzero. Note: each value can be seen intuitively as a pair, (x, H), where x is a monoid element and H is a proof that x is invertable.

Accepts a field element and a proof that it is nonzero and returns its projection in D.

Asserts that any two equal non-zero elements, x and y, are equivalent (using dependent equality). Note: to compare sig elements that differ only in their proof terms, such as (x, H) and (x, H0), we must introduce a new notion of equality called "dependent equality". This relationship is defined in the Eqdep module.

Given that two invertable monoid elements x and y are equal (using dependent equality), this lemma proves that their projections into D are equal. Note: this proof is equivalent to: eq_dep_eq_sig E (Monoid.has_inv m) y x H0 H (D_eq_dep x H y H0 H1). The definition for eq_dep_eq_sig has been expanded however for compatability with Coq v8.4.

Represents the group identity element.

Represents the group operation. Note: intuitively this function accepts two invertable monoid elements, (x, H) and (y, H0), and returns (x + y, H1), where H, H0, and H1 are generalized invertability proofs.

TODO Proves that D and D_prod are isomorphic with the set of nonzero field elements. Definition D_iso Accepts a group element, x, and asserts that x is a left identity element.

Accepts a group element, x, and asserts that x is a right identity element.

Accepts a group element, x, and asserts that x is an/the identity element.

Proves that D_1 is a left identity element.

Proves that D_1 is a right identity element.

Proves that D_1 is the identity element.

Proves that the group operation is associative.

Accepts two values, x and y, and asserts that y is a left inverse of x.

Accepts two values, x and y, and asserts that y is a right inverse of x.

Accepts two values, x and y, and asserts that y is an inverse of x.

Accepts two nonzero elements, x and y, where y is a left inverse of x and proves that y's projection into D is the left inverse of x's.

Accepts two invertable monoid elements, x and y, where y is a right inverse of x and proves that y's projection into D is the right inverse of x's.

Accepts two invertable monoid elements, x and y, where y is the inverse of x and proves that y's projection into D is the inverse of x's.

Accepts a nonzero element and returns its inverse, y, along with a proof that y is x's inverse.

Proves that every group element has an inverse.

Proves that every group element has a left inverse.

Proves that every group element has a right inverse.

Proves that the set of nonzero elements form a group over multiplication.