Require Import Utils.
Require Import Strings.

Finite Semigroups

This file contains basics of finite semigroups, most importantly that for every element a of a finite semigroup, there is an n such that a * n is idempotent.

Definition associative (Gamma: finType) (add: Gamma -> Gamma -> Gamma) := forall a b c, add a (add b c) = add (add a b) c.

A finite semigroup is a finite type with an associatide addition operation.
Class FiniteSemigroup := mkSG {
   elements : finType;
   add : elements -> elements -> elements;
   Assoc: associative add
}.

Coercion elements : FiniteSemigroup >-> finType.

Definition of homomorphisms specialized to morphisms from the semigroup of nonempty strings (with concatenation) to some finite semigroup. We do not need a general notion with arvitrary semigroups on both sides.
Definition is_homomorphism (Gamma: FiniteSemigroup) (Y:Type) (f: NStr Y -> Gamma) := forall x y , f(nstr_concat' x y) = add (f x) (f y).

Section FiniteSemigroup.

  Context {Gamma : FiniteSemigroup}.
  Implicit Types (a b c : Gamma).

Sum of a string (called color in the paper. Sum of a string is more aligned with add, mul, etc in the following

  Fixpoint SUM (x : NStr Gamma) := match x with
    | sing a => a
    | ncons a x => add a (SUM x)
  end.

  Lemma SUM_concat x y : SUM (nstr_concat' x y) = add (SUM x) (SUM y).
  Proof.
    induction x.
    - reflexivity.
    - simpl. now rewrite IHx, Assoc.
  Qed.

  Lemma SUM_is_homomorphism : is_homomorphism SUM.
  Proof.
     intros x y. apply SUM_concat.
  Qed.

We define multiplication a * n. a * 0 does not make sense as semigroups do not have a neutral element. In this case we just return a.

  Fixpoint mul (a:Gamma) n {struct n} := match n with
     | 0 => a
     | 1 => a
     | S n => add a (mul a n)
  end.

  Lemma mul_step a n : n > 0 -> mul a (S n) = add a (mul a n).
  Proof.
    intros L. cbn. destruct n; auto.
  Qed.

  Lemma mul_comm a n : n > 0 -> add (mul a n) a = add a (mul a n).
  Proof.
    intros L. induction n; auto.
    destruct n; auto. remember (S n) as N.
    rewrite mul_step by omega. rewrite <-IHn at 2 by omega. now rewrite Assoc.
  Qed.

  Lemma mul_distr a n m : n > 0 -> m > 0 -> (mul a (n + m)) = add (mul a n) (mul a m).
  Proof.
    intros Ln Lm.
    induction m.
    - exfalso. omega.
    - destruct m.
      + cbn. rewrite_eq (n+1 = S n). rewrite mul_step by omega.
        now rewrite mul_comm.
      + rewrite_eq (n + S(S m) = S (n + S m)). rewrite !mul_step by omega.
        rewrite IHm by omega. rewrite !Assoc. f_equal.
        now rewrite mul_comm.
  Qed.

  Lemma mul_mult a n m : n > 0 -> m > 0 -> (mul a (n * m)) = (mul (mul a n) m).
  Proof.
    intros Ln Lm.
    induction m.
    - exfalso. omega.
    - destruct m.
      + cbn. now rewrite Nat.mul_1_r.
      + remember (S m) as M. rewrite mul_step by omega.
        rewrite <-IHm by omega.
        rewrite Nat.mul_succ_r.
        rewrite_eq (n*M + n = n + n* M). rewrite mul_distr; auto.
        apply mul_ge_0; omega.
  Qed.

Idempotent Elements


  Definition idempotent a := add a a = a.


  Fixpoint prefix_of_function (f: nat -> Gamma) n := match n with
    | 0 => []
    | S n => (f 0) :: (prefix_of_function (fun n => f (S n)) n)
  end.

  Lemma prefix_of_function_correct f n k D: k < n -> @str_nth Gamma D (prefix_of_function f n) k = f k.
  Proof.
    revert f k D. induction n; intros f k D L.
    - now exfalso.
    - simpl. destruct k; auto.
      rewrite IHn; auto.
  Qed.

  Lemma prefix_of_function_length f n : length (prefix_of_function f n) = n.
  Proof.
    revert f; induction n; intros f; simpl; auto.
  Qed.

For every element a, there is strictly positive number n such that a * n is idempotent.

  Lemma mul_yields_idempotent a : exists n, n > 0 /\ idempotent (mul a n).
  Proof.
    unfold idempotent.
    destruct (duplicates (x :=prefix_of_function (fun n => (mul a (Nat.pow 2 n))) (S (Cardinality Gamma)))) as [i [j [L D]]].
    - rewrite prefix_of_function_length. omega.
    - rewrite !prefix_of_function_length in L.
      rewrite !prefix_of_function_correct in D by omega.
      remember (j - i) as k. assert (j = i + k) by omega. subst j. assert (k > 0) by omega.
      decide (k = 1).
      + subst k. exists (Nat.pow 2 i). split. apply pow_ge_zero.
        rewrite Nat.pow_add_r in D. rewrite mul_mult in D; auto; apply pow_ge_zero.
      + exists ( (Nat.pow 2 i) * ((Nat.pow 2 k)-1)). rewrite Nat.pow_add_r in D.
        remember (Nat.pow 2 i) as I. remember (Nat.pow 2 k) as K.
        assert (K > 2). { subst K. destruct k.
           - exfalso. omega.
           - cbn. enough (Nat.pow 2 k >1 ) by omega.
             destruct k.
             + exfalso. omega.
             + cbn. enough(Nat.pow 2 k > 0) by omega. apply pow_ge_zero. }
        assert (I > 0). { subst I. apply pow_ge_zero. } clear HeqI HeqK.
        split. { apply mul_ge_0; omega. }
        rewrite <-mul_distr; auto.
        * rewrite <-Nat.mul_add_distr_l. rewrite_eq ((K-1) +(K-1) = K + (K -2) ).
          rewrite Nat.mul_add_distr_l. rewrite mul_distr; auto.
          -- rewrite <-D. rewrite <-mul_distr; auto.
             ++ f_equal. enough ( I = I * 1) as H'.
                ** rewrite H' at 1. rewrite <-Nat.mul_add_distr_l. f_equal. omega.
                ** symmetry. apply Nat.mul_1_r.
             ++ apply mul_ge_0; omega.
          -- apply mul_ge_0; omega.
          -- apply mul_ge_0; omega.
        * apply mul_ge_0; omega.
        * apply mul_ge_0; omega.
  Qed.

  Lemma SUM_flatten u : SUM (nstr_flatten u) = SUM (nstr_map SUM u).
  Proof.
    induction u as [v|v u]; simpl; auto.
    rewrite <-IHu. induction v; simpl; auto.
    now rewrite IHv, Assoc.
  Qed.


End FiniteSemigroup.