Library functional_algebra.commutative_ring
This module defines the commutative_ring record type which
represents algebraic commutative 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/>.
Require Import Description.
Require Import FunctionalExtensionality.
Require Import base.
Require Import function.
Require Import monoid.
Require Import group.
Require Import abelian_group.
Require Import ring.
Module Commutative_Ring.
Represents algebraic commutative 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 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 multiplication is left distributive
over addition.
Enable implicit arguments for commutative
ring properties.
Arguments E_0 {c}.
Arguments E_1 {c}.
Arguments sum {c} x y.
Arguments prod {c} x y.
Arguments distinct_0_1 {c} _.
Arguments sum_is_assoc {c} x y z.
Arguments sum_is_comm {c} x y.
Arguments sum_id_l {c} x.
Arguments sum_inv_l_ex {c} x.
Arguments prod_is_assoc {c} x y z.
Arguments prod_id_l {c} x.
Arguments prod_sum_distrib_l {c} x y z.
Arguments prod_is_comm {c} x y.
Define notations for ring properties.
Notation "0" := E_0 : commutative_ring_scope.
Notation "1" := E_1 : commutative_ring_scope.
Notation "x + y" := (sum x y) (at level 50, left associativity) : commutative_ring_scope.
Notation "{+}" := sum : commutative_ring_scope.
Notation "x # y" := (prod x y) (at level 50, left associativity) : commutative_ring_scope.
Notation "{#}" := prod : commutative_ring_scope.
Open Scope commutative_ring_scope.
Section Theorems.
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.
Proves that 1 is the right identity element.
Definition prod_id_r
: prod_is_id_r 1
:= fun x : E
=> eq_ind_r
(fun a => a = x)
(prod_id_l x)
(prod_is_comm x 1).
: prod_is_id_r 1
:= fun x : E
=> eq_ind_r
(fun a => a = x)
(prod_id_l x)
(prod_is_comm x 1).
Proves that multiplication is right distributive
over addition.
Definition prod_sum_distrib_r
: Ring.is_distrib_r E {#} {+}
:= fun x y z : E
=> prod_sum_distrib_l x y z
|| x # (y + z) = a + (x # z) @a by <- prod_is_comm x y
|| x # (y + z) = (y # x) + a @a by <- prod_is_comm x z
|| a = (y # x) + (z # x) @a by <- prod_is_comm x (y + z).
: Ring.is_distrib_r E {#} {+}
:= fun x y z : E
=> prod_sum_distrib_l x y z
|| x # (y + z) = a + (x # z) @a by <- prod_is_comm x y
|| x # (y + z) = (y # x) + a @a by <- prod_is_comm x z
|| a = (y # x) + (z # x) @a by <- prod_is_comm x (y + z).
Represents the non-commutative ring formed
by addition and multiplication over E.
Definition ring := Ring.ring E 0 1 {+} {#} distinct_0_1 sum_is_assoc sum_is_comm sum_id_l sum_inv_l_ex prod_is_assoc prod_id_l prod_id_r prod_sum_distrib_l prod_sum_distrib_r.
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.
Represents the monoid formed by
multiplication over E.
Proves that 1 <> 0.
Definition distinct_1_0
: E_1 (c := r) <> E_0 (c := r)
:= fun H : E_1 = E_0
=> distinct_0_1 (eq_sym H).
: E_1 (c := r) <> E_0 (c := r)
:= fun H : E_1 = E_0
=> distinct_0_1 (eq_sym H).
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.
Definition sum_id_l_uniq
: forall x : E, Monoid.is_id_l E {+} x -> x = 0
:= Ring.sum_id_l_uniq ring.
: forall x : E, Monoid.is_id_l E {+} x -> x = 0
:= Ring.sum_id_l_uniq ring.
Proves that the right identity element is unique.
Definition sum_id_r_uniq
: forall x : E, Monoid.is_id_r E {+} x -> x = 0
:= Ring.sum_id_r_uniq ring.
: forall x : E, Monoid.is_id_r E {+} x -> x = 0
:= Ring.sum_id_r_uniq ring.
Proves that the identity element is unique.
Proves that for every group element, x,
its left and right inverses are equal.
Definition sum_inv_l_r_eq
: forall x y : E, sum_is_inv_l x y -> forall z : E, sum_is_inv_r x z -> y = z
:= Ring.sum_inv_l_r_eq ring.
: forall x y : E, sum_is_inv_l x y -> forall z : E, sum_is_inv_r x z -> y = z
:= Ring.sum_inv_l_r_eq ring.
Proves that the inverse relation is
symmetrical.
Definition sum_inv_sym
: forall x y : E, sum_is_inv x y <-> sum_is_inv y x
:= Ring.sum_inv_sym ring.
: forall x y : E, sum_is_inv x y <-> sum_is_inv y x
:= Ring.sum_inv_sym ring.
Proves that an element's inverse is unique.
Definition sum_inv_uniq
: forall x y z : E, sum_is_inv x y -> sum_is_inv x z -> z = y
:= Ring.sum_inv_uniq ring.
: forall x y z : E, sum_is_inv x y -> sum_is_inv x z -> z = y
:= Ring.sum_inv_uniq ring.
Proves that every element has an inverse.
Proves explicitly that every element has a
unique inverse.
Definition sum_inv_uniq_ex
: forall x : E, exists! y : E, sum_is_inv x y
:= Ring.sum_inv_uniq_ex ring.
: forall x : E, exists! y : E, sum_is_inv x y
:= Ring.sum_inv_uniq_ex ring.
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.
Definition sum_inv_l_uniq
: forall x y z : E, sum_is_inv_l x y -> sum_is_inv_l x z -> z = y
:= Ring.sum_inv_l_uniq ring.
: forall x y z : E, sum_is_inv_l x y -> sum_is_inv_l x z -> z = y
:= Ring.sum_inv_l_uniq ring.
Proves that an element's right inverse
is unique.
Definition sum_inv_r_uniq
: forall x y z : E, sum_is_inv_r x y -> sum_is_inv_r x z -> z = y
:= Ring.sum_inv_r_uniq ring.
: forall x y z : E, sum_is_inv_r x y -> sum_is_inv_r x z -> z = y
:= Ring.sum_inv_r_uniq ring.
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.
Represents strongly-specified negation.
Represents negation.
Definition sum_neg
: E -> E
:= Ring.sum_neg ring.
Notation "{-}" := (sum_neg) : commutative_ring_scope.
Notation "- x" := (sum_neg x) : commutative_ring_scope.
: E -> E
:= Ring.sum_neg ring.
Notation "{-}" := (sum_neg) : commutative_ring_scope.
Notation "- x" := (sum_neg x) : commutative_ring_scope.
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 0's negation is 0.
Proves that if an element's, x, negation
equals 0, x must equal 0.
Definition sum_neg_0
: forall x : E, - x = 0 -> x = 0
:= fun x H
=> proj2 (sum_neg_def x)
|| x + a = 0 @a by <- H
|| a = 0 @a by <- sum_id_r x.
: forall x : E, - x = 0 -> x = 0
:= fun x H
=> proj2 (sum_neg_def x)
|| x + a = 0 @a by <- H
|| a = 0 @a by <- sum_id_r x.
Prove that 0 is the only element whose additive
inverse (negation) equals 0.
Definition sum_neg_0_uniq
: unique (fun x => - x = 0) 0
:= conj sum_0_neg
(fun x H => eq_sym (sum_neg_0 x H)).
: unique (fun x => - x = 0) 0
:= conj sum_0_neg
(fun x H => eq_sym (sum_neg_0 x H)).
Accepts one element, x, and asserts
that x is the identity element.
Proves that the left identity element is unique.
Definition prod_id_l_uniq
: forall x : E, (Monoid.is_id_l E {#} x) -> x = 1
:= Ring.prod_id_l_uniq ring.
: forall x : E, (Monoid.is_id_l E {#} x) -> x = 1
:= Ring.prod_id_l_uniq ring.
Proves that the right identity element is unique.
Definition prod_id_r_uniq
: forall x : E, (Monoid.is_id_r E {#} x) -> x = 1
:= Ring.prod_id_r_uniq ring.
: forall x : E, (Monoid.is_id_r E {#} x) -> x = 1
:= Ring.prod_id_r_uniq ring.
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 every left inverse must also
be a right inverse.
Definition prod_is_inv_lr
: forall x y : E, prod_is_inv_l x y -> prod_is_inv_r x y
:= fun x y H
=> H || a = 1 @a by prod_is_comm x y.
: forall x y : E, prod_is_inv_l x y -> prod_is_inv_r x y
:= fun x y H
=> H || a = 1 @a by prod_is_comm x y.
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
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
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 = sum_neg -1
- 1 * -1 = 1
Proves that -1 is its own multiplicative
inverse.
Definition E_n1_inv
: prod_is_inv {-1} {-1}
:= Ring.E_n1_inv ring.
End Theorems.
End Commutative_Ring.
: prod_is_inv {-1} {-1}
:= Ring.E_n1_inv ring.
End Theorems.
End Commutative_Ring.