Library functional_algebra.monoid

This module defines the Monoid record type which represents algebraic structures called Monoids and provides a collection of theorems and axioms 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 base.
Require Import function.
Require Import ProofIrrelevance.
Require Import Bool.

Require Import Arith.
Require Import Wf.
Require Import Wellfounded.
Require Import Wf_nat.

Module Monoid.

Accepts a function, f, and asserts that f is associative.
Definition is_assoc (T : Type) (f : T -> T -> T) : Prop := forall x y z : T, f x (f y z) = f (f x y) z.

Accepts two arguments, f and x, and asserts that x is a left identity element w.r.t. f.
Definition is_id_l (T : Type) (f : T -> T -> T) (E : T) : Prop := forall x : T, f E x = x.

Accepts two arguments, f and x, and asserts that x is a right identity element w.r.t. f.
Definition is_id_r (T : Type) (f : T -> T -> T) (E : T) : Prop := forall x : T, f x E = x.

Accepts two arguments, f and x, and asserts that x is an identity element w.r.t. f.
Definition is_id (T : Type) (f : T -> T -> T) (E : T) : Prop := is_id_l T f E /\ is_id_r T f E.

Accepts three arguments, f, e, and H, where H proves that e is the identity element w.r.t. f, and returns a function that accepts two arguments, x and y, and asserts that y is x's left inverse.
Definition is_inv_l (T : Type) (f : T -> T -> T) (E : T) (_ : is_id T f E) (x y : T) : Prop := f y x = E.

Accepts three arguments, f, e, and H, where H proves that e is the identity element w.r.t. f, and returns a function that accepts two arguments, x and y, and asserts that y is x's right inverse.
Definition is_inv_r (T : Type) (f : T -> T -> T) (E : T) (_ : is_id T f E) (x y : T) : Prop := f x y = E.

Accepts three arguments, f, e, and H, where H proves that e is the identity element w.r.t. f, and returns a function that accepts two arguments, x and y, and asserts that y is x's inverse.
Definition is_inv (T : Type) (f : T -> T -> T) (E : T) (H : is_id T f E) (x y : T) : Prop := is_inv_l T f E H x y /\ is_inv_r T f E H x y.

Represents algebraic monoids.
Structure Monoid : Type := monoid {

  
Represents the set of monoid elements.
  E: Set;

  
Represents the identity element.
  E_0: E;

  
Represents the monoid operation.
  op: E -> E -> E;

  
Asserts that the monoid operator is associative.
  op_is_assoc : is_assoc E op;

  
Asserts that E_0 is the left identity element.
  op_id_l : is_id_l E op E_0;

  
Asserts that E_0 is the right identity element.
  op_id_r : is_id_r E op E_0
}.

Enable implicit arguments for monoid properties.

Arguments E_0 {m}.

Arguments op {m} x y.

Arguments op_is_assoc {m} x y z.

Arguments op_id_l {m} x.

Arguments op_id_r {m} x.

Define notations for monoid properties.

Notation "0" := E_0 : monoid_scope.

Notation "x + y" := (op x y) (at level 50, left associativity) : monoid_scope.

Notation "{+}" := op : monoid_scope.

Open Scope monoid_scope.

Section Theorems.

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

Represents the set of monoid elements.
Definition M := E m.

Accepts one monoid element, x, and asserts that x is the left identity element.
Definition op_is_id_l := is_id_l M {+}.

Accepts one monoid element, x, and asserts that x is the right identity element.
Definition op_is_id_r := is_id_r M {+}.

Accepts one monoid element, x, and asserts that x is the identity element.
Definition op_is_id := is_id M {+}.

Proves that 0 is the identity element.
Definition op_id
  : is_id M {+} 0
  := conj op_id_l op_id_r.

Proves that the left identity element is unique.
Definition op_id_l_uniq
  : forall x : M, (op_is_id_l x) -> x = 0
  := fun x H
       => H 0 || a = 0 @a by <- op_id_r x.

Proves that the right identity element is unique.
Definition op_id_r_uniq
  : forall x : M, (op_is_id_r x) -> x = 0
  := fun x H
       => H 0 || a = 0 @a by <- op_id_l x.

Proves that the identity element is unique.
Definition op_id_uniq
  : forall x : M, (op_is_id x) -> x = 0
  := fun x
       => and_ind (fun H _ => op_id_l_uniq x H).

Proves the left introduction rule.
Definition op_intro_l
  : forall x y z : M, x = y -> z + x = z + y
  := fun x y z H
       => f_equal ({+} z) H.

Proves the right introduction rule.
Definition op_intro_r
  : forall x y z : M, x = y -> x + z = y + z
  := fun x y z H
       => eq_refl (x + z)
       || x + z = a + z @a by <- H.

Accepts two monoid elements, x and y, and asserts that y is x's left inverse.
Definition op_is_inv_l := is_inv_l M {+} 0 op_id.

Accepts two monoid elements, x and y, and asserts that y is x's right inverse.
Definition op_is_inv_r := is_inv_r M {+} 0 op_id.

Accepts two monoid elements, x and y, and asserts that y is x's inverse.
Definition op_is_inv := is_inv M {+} 0 op_id.

Accepts one argument, x, and asserts that x has a left inverse.
Definition has_inv_l
  := fun x => exists y : M, op_is_inv_l x y.

Accepts one argument, x, and asserts that x has a right inverse.
Definition has_inv_r
  := fun x => exists y : M, op_is_inv_r x y.

Accepts one argument, x, and asserts that x has an inverse.
Definition has_inv
  := fun x => exists y : M, op_is_inv x y.

Proves that the left and right inverses of an element must be equal.
Definition op_inv_l_r_eq
  : forall x y : M, op_is_inv_l x y -> forall z : M, op_is_inv_r x z -> y = z
  := fun x y H1 z H2
       => op_is_assoc y x z
          || y + a = (y + x) + z @a by <- H2
          || a = (y + x) + z @a by <- op_id_r y
          || y = a + z @a by <- H1
          || y = a @a by <- op_id_l z.

Proves that the inverse relationship is symmetric.
Definition op_inv_sym
  : forall x y : M, op_is_inv x y <-> op_is_inv y x
  := fun x y
       => conj
            (fun H : op_is_inv x y
              => conj (proj2 H) (proj1 H))
            (fun H : op_is_inv y x
              => conj (proj2 H) (proj1 H)).

The next few lemmas define special cases where cancellation holds and culminate in the Unique Inverse theorem which asserts that, in a Monoid, every value has at most one inverse.
Proves the left cancellation law for elements possessing a left inverse.
Definition op_cancel_l
  : forall x y z : M, has_inv_l z -> z + x = z + y -> x = y
  := fun x y z H H0
       => ex_ind
            (fun u H1
              => op_intro_l (z + x) (z + y) u H0
              || a = u + (z + y) @a by <- op_is_assoc u z x
              || (u + z) + x = a @a by <- op_is_assoc u z y
              || a + x = a + y @a by <- H1
              || a = 0 + y @a by <- op_id_l x
              || x = a @a by <- op_id_l y)
            H.

Proves the right cancellation law for elements possessing a right inverse.
Definition op_cancel_r
  : forall x y z : M, has_inv_r z -> x + z = y + z -> x = y
  := fun x y z H H0
       => ex_ind
            (fun u H1
              => op_intro_r (x + z) (y + z) u H0
              || a = (y + z) + u @a by op_is_assoc x z u
              || x + (z + u) = a @a by op_is_assoc y z u
              || x + a = y + a @a by <- H1
              || a = y + 0 @a by <- op_id_r x
              || x = a @a by <- op_id_r y)
            H.

Proves that an element's left inverse is unique.
Definition op_inv_l_uniq
  : forall x : M, has_inv_r x -> forall y z : M, op_is_inv_l x y -> op_is_inv_l x z -> z = y
  := fun x H y z H0 H1
       => let H2
            : z + x = y + x
            := H1 || z + x = a @a by H0 in
          let H3
            : z = y
            := op_cancel_r z y x H H2 in
          H3.

Proves that an element's right inverse is unique.
Definition op_inv_r_uniq
  : forall x : M, has_inv_l x -> forall y z : M, op_is_inv_r x y -> op_is_inv_r x z -> z = y
  := fun x H y z H0 H1
       => let H2
            : x + z = x + y
            := H1 || x + z = a @a by H0 in
          let H3
            : z = y
            := op_cancel_l z y x H H2 in
          H3.

Proves that an element's inverse is unique.
Definition op_inv_uniq
  : forall x y z : M, op_is_inv x y -> op_is_inv x z -> z = y
  := fun x y z H H0
       => op_inv_l_uniq x
            (ex_intro (fun y => op_is_inv_r x y) y (proj2 H))
            y z (proj1 H) (proj1 H0).

Proves that the identity element is its own left inverse.
Definition op_inv_0_l
  : op_is_inv_l 0 0
  := op_id_l 0 : 0 + 0 = 0.

Proves that the identity element is its own right inverse.
Definition op_inv_0_r
  : op_is_inv_r 0 0
  := op_id_r 0 : 0 + 0 = 0.

Proves that the identity element is its own inverse.
Definition op_inv_0
  : op_is_inv 0 0
  := conj op_inv_0_l op_inv_0_r.

Proves that the identity element has a left inverse.
Definition op_has_inv_l_0
  : has_inv_l 0
  := ex_intro (op_is_inv_l 0) 0 op_inv_0_l.

Proves that the identity element has a right inverse.
Definition op_has_inv_r_0
  : has_inv_r 0
  := ex_intro (op_is_inv_r 0) 0 op_inv_0_r.

Proves that the identity element has an inverse.
Definition op_has_inv_0
  : has_inv 0
  := ex_intro (op_is_inv 0) 0 op_inv_0.

Every monoid has a subset of elements that possess inverses. This can be seen by noting that, by definition, every monoid has an identity element (this is what distinguishes a monoid from a semigroup) and the identity element is its own inverse. The following theorems explore the behavior of those elements that possess inverses. They will prove especially ueseful when we consider groups where every element possess an inverse.
Accepts two arguments: x; and H, a proof that x has an inverse; and returns x's inverse, y, along with a proof that y is x's inverse.
Definition op_neg_strong
  : forall x : M, has_inv x -> { y | op_is_inv x y }
  := fun x H
       => constructive_definite_description (op_is_inv x)
            (ex_ind
              (fun y (H0 : op_is_inv x y)
                => ex_intro
                     (fun y => op_is_inv x y /\ forall z, op_is_inv x z -> y = z)
                     y
                     (conj H0 (fun z H1 => eq_sym (op_inv_uniq x y z H0 H1))))
              H).

Accepts two arguments: x; and H, a proof that x has an inverse. and returns x's inverse.
Definition op_neg
  : forall x : M, has_inv x -> M
  := fun x H => proj1_sig (op_neg_strong x H).

Notation "{-}" := (op_neg) : monoid_scope.

Proves that, forall x and H, where H is a proof that x has an inverse, `op_neg x H` is x's inverse.
Definition op_neg_def
  : forall (x : M) (H : has_inv x), op_is_inv x ({-} x H)
  := fun x H => proj2_sig (op_neg_strong x H).

Proves that, forall x and H, where H is a proof that x has an inverse, x is the inverse of `- x H`.
Note: this lemma is an immediate consequence of the symmetry of the inverse predicate.
Definition op_neg_inv
  : forall (x : M) (H : has_inv x), op_is_inv ({-} x H) x
  := fun x H
       => (proj1 (op_inv_sym x ({-} x H))) (op_neg_def x H).

Proves that, forall x and H, where H is a proof that x has an inverse, `- x H` has an inverse.
Note: this lemma is a weakening of `op_neg_inv` and is used to apply the lemmas and theorems in this section to expressions involving `op_neg`.
Definition op_neg_inv_ex
  : forall (x : M) (H : has_inv x), has_inv ({-} x H)
  := fun x H
       => ex_intro
            (op_is_inv ({-} x H))
            x
            (op_neg_inv x H).

Proves that negation is injective over the set of invertible elements - I.E. forall x and y if the negation of x equals the negation of y then x and y must be equal.
Definition op_neg_inj
  : forall (x : M) (H : has_inv x) (y : M) (H0 : has_inv y),
     {-} x H = {-} y H0 ->
     x = y
  := fun x H y H0 H1
       => let H2
            : x + ({-} x H) = y + ({-} x H)
            := (proj2 (op_neg_def x H) : x + ({-} x H) = 0)
               || x + ({-} x H) = a @a by proj2 (op_neg_def y H0)
               || x + ({-} x H) = y + a @a by H1 in
          let H3
            : x = y
            := op_cancel_r x y ({-} x H)
               (ex_intro
                 (op_is_inv_r ({-} x H))
                 x
                 (proj2 (proj1 (op_inv_sym x ({-} x H)) (op_neg_def x H))))
               H2 in
          H3.

Proves that double negation is equivalent to the identity function for all invertible values.
Note: the monoid negation operation requires a proof that the value passed to it is invertible. The form of this theorem explicitly asserts that double negation is equivalent to the identity operation for any proof that the negative has an inverse.
Definition op_cancel_neg_gen
  : forall (x : M) (H : has_inv x) (H0 : has_inv ({-} x H)), {-} ({-} x H) H0 = x
  := fun x H H0
       => let H1
            : op_is_inv ({-} x H) ({-} ({-} x H) H0)
            := op_neg_def ({-} x H) H0 in
          let H3
            : op_is_inv ({-} x H) x
            := op_neg_inv x H in
          op_inv_uniq ({-} x H) x ({-} ({-} x H) H0) H3 H1.

Proves that double negation is equivalent to the identity function for all invertible values.
Definition op_cancel_neg
  : forall (x : M) (H : has_inv x), {-} ({-} x H) (op_neg_inv_ex x H) = x
  := fun x H
       => op_cancel_neg_gen x H (op_neg_inv_ex x H).

Proves that negation is onto over the subset of invertable values.
Definition op_neg_onto
  : forall (y : M) (H : has_inv y), exists (x : M) (H0 : has_inv x), {-} x H0 = y
  := fun y H
       => ex_intro
            (fun x => exists H0 : has_inv x, {-} x H0 = y)
            ({-} y H)
            (ex_intro
              (fun H0 => {-} ({-} y H) H0 = y)
              (op_neg_inv_ex y H)
              (op_cancel_neg y H)).

Proves that invertability is closed over the monoid operation.
Note: given this theorem, we can conclude that the set of invertible elements within a monoid, which must be nonempty, forms a group.
Definition op_inv_closed
  : forall (x : M) (H : has_inv x) (y : M) (H0 : has_inv y), has_inv (x + y)
  := fun x H y H0
       => ex_ind
            (fun u (H1 : op_is_inv x u)
              => ex_ind
                   (fun v (H2 : op_is_inv y v)
                     => ex_intro
                          (op_is_inv (x + y))
                          (v + u)
                          (conj
                            (op_is_assoc (v + u) x y
                              || (v + u) + (x + y) = a + y @a by op_is_assoc v u x
                              || (v + u) + (x + y) = (v + a) + y @a by <- proj1 H1
                              || (v + u) + (x + y) = a + y @a by <- op_id_r v
                              || (v + u) + (x + y) = a @a by <- proj1 H2
                            )
                            (op_is_assoc (x + y) v u
                              || (x + y) + (v + u) = a + u @a by op_is_assoc x y v
                              || (x + y) + (v + u) = (x + a) + u @a by <- proj2 H2
                              || (x + y) + (v + u) = a + u @a by <- op_id_r x
                              || (x + y) + (v + u) = a @a by <- proj2 H1
                            )))
                   H0)
            H.

Proves that every boolean value is either true or false.
Definition bool_dec0
  : forall b : bool, {b = true}+{b = false}
  := bool_rect
       (fun b => {b = true}+{b = false})
       (left (true = false) (eq_refl true))
       (right (false = true) (eq_refl false)).

End Theorems.

End Monoid.

Coq does not export notations outside of sections. Consequently the notationsdefined above are not visible to other modules. To fix this, we gather all the notations here for export.

Notation "0" := (Monoid.E_0) : monoid_scope.

Notation "x + y" := (Monoid.op x y) (at level 50, left associativity) : monoid_scope.

Notation "{+}" := (Monoid.op) : monoid_scope.

Notation "{-}" := (Monoid.op_neg _) : monoid_scope.