split the algebra library; use fsatz more

1 files changed, 60 insertions, 0 deletions

diff --git a/src/Algebra/Monoid.v b/src/Algebra/Monoid.v
new file mode 100644
index 000000000..f71efff3e
--- /dev/null
+++ b/src/Algebra/Monoid.v
@@ -0,0 +1,60 @@
+Require Import Coq.Classes.Morphisms.
+Require Import Crypto.Util.Tactics.
+Require Import Crypto.Algebra.
+
+Section Monoid.
+  Context {T eq op id} {monoid:@monoid T eq op id}.
+  Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
+  Local Infix "*" := op.
+  Local Infix "=" := eq : eq_scope.
+  Local Open Scope eq_scope.
+
+  Lemma cancel_right z iz (Hinv:op z iz = id) :
+    forall x y, x * z = y * z <-> x = y.
+  Proof.
+    split; intros.
+    { assert (op (op x z) iz = op (op y z) iz) as Hcut by (rewrite_hyp ->!*; reflexivity).
+      rewrite <-associative in Hcut.
+      rewrite <-!associative, !Hinv, !right_identity in Hcut; exact Hcut. }
+    { rewrite_hyp ->!*. reflexivity. }
+  Qed.
+
+  Lemma cancel_left z iz (Hinv:op iz z = id) :
+    forall x y, z * x = z * y <-> x = y.
+  Proof.
+    split; intros.
+    { assert (op iz (op z x) = op iz (op z y)) as Hcut by (rewrite_hyp ->!*; reflexivity).
+      rewrite !associative, !Hinv, !left_identity in Hcut; exact Hcut. }
+    { rewrite_hyp ->!*; reflexivity. }
+  Qed.
+
+  Lemma inv_inv x ix iix : ix*x = id -> iix*ix = id -> iix = x.
+  Proof.
+    intros Hi Hii.
+    assert (H:op iix id = op iix (op ix x)) by (rewrite Hi; reflexivity).
+    rewrite associative, Hii, left_identity, right_identity in H; exact H.
+  Qed.
+
+  Lemma inv_op x y ix iy : ix*x = id -> iy*y = id -> (iy*ix)*(x*y) =id.
+  Proof.
+    intros Hx Hy.
+    cut (iy * (ix*x) * y = id); try intro H.
+    { rewrite <-!associative; rewrite <-!associative in H; exact H. }
+    rewrite Hx, right_identity, Hy. reflexivity.
+  Qed.
+
+End Monoid.
+
+Section Homomorphism.
+  Context {T  EQ OP ID} {monoidT:  @monoid T  EQ OP ID }.
+  Context {T' eq op id} {monoidT': @monoid T' eq op id }.
+  Context {phi:T->T'}.
+  Local Infix "=" := eq. Local Infix "=" := eq : type_scope.
+  Class is_homomorphism :=
+    {
+      homomorphism : forall a b,  phi (OP a b) = op (phi a) (phi b);
+
+      is_homomorphism_phi_proper : Proper (respectful EQ eq) phi
+    }.
+  Global Existing Instance is_homomorphism_phi_proper.
+End Homomorphism.
\ No newline at end of file