HyPre.pred.MonoidHomomorphism

From Coq Require Import
  Program.Equality.

From HyPre Require Export
  ListExtra
  NatExtra
  VectorExtra.

Import ListNotations.
Set Implicit Arguments.
Set Maximal Implicit Insertion.
Set Universe Polymorphism.

Section Monoid.
  Universe u.
  Variable S : Type@{u}.

  Class Monoid@{} : Type :=
    {
      monoid_plus : S -> S -> S;
      monoid_unit : S;
    }.

  Class MonoidLaws@{} (M : Monoid) : Type :=
    {
      monoid_assoc : forall m1 m2 m3, monoid_plus (monoid_plus m1 m2) m3 = monoid_plus m1 (monoid_plus m2 m3);
      monoid_lunit : forall m, monoid_plus monoid_unit m = m;
      monoid_runit : forall m, monoid_plus m monoid_unit = m;
    }.

End Monoid.

Require Vector.

Generalizable All Variables.
(*Existing Class Monoid.*)

Global Instance Monoid_nat : Monoid nat
  := {| monoid_plus := Nat.add; monoid_unit := 0 |}.

Global Program Instance MonoidLaws_nat : MonoidLaws (Monoid_nat).
Next Obligation.
  lia.
Qed.

(*Existing Instance Monoid_nat_plus.*)

Class MonoidHomomorphism {M N : Type} {MMon : Monoid M} {NMon : Monoid N} (hom : M -> N)
  := {
      homomorph : forall m1 m2, hom (monoid_plus m1 m2) = monoid_plus (hom m1) (hom m2);
      homomorph_unit : hom monoid_unit = monoid_unit;
    }.

Class MonoidIsomorphism {M N : Type} {MMon : Monoid M} {NMon : Monoid N} (hom : M -> N)
  := {
      MonoidIsomorphism_homomorph :> MonoidHomomorphism hom;
      injective : forall m1 m2, hom m1 = hom m2 -> m1 = m2;
      surjective : forall m, {m' | hom m' = m};
    }.

(*Definition len_vec `{MM : MonoidHomomorphism} {k : nat} : Vector.t M k -> Vector.t N k
  := Vector.map hom.*)

Definition vm_plus `{MMon : Monoid M} {k : nat} : Vector.t M k -> Vector.t M k -> Vector.t M k
  := Vector.map2 (monoid_plus).

Module MonoidHomomorphismNotations.

  Infix "+m+" := (monoid_plus) (at level 69).

  Infix "+vm+" := vm_plus (at level 69).

End MonoidHomomorphismNotations.

Import MonoidHomomorphismNotations.

Lemma Monoid_unit_lunique `{M : Monoid} {ML : @MonoidLaws _ M}
  : forall m, (forall m', m +m+ m' = m') -> m = monoid_unit.
Proof.
  intros.
  specialize (H monoid_unit).
  setoid_rewrite monoid_runit in H.
  assumption.
Qed.

Lemma Monoid_unit_runique `{M : Monoid} `{ML : MonoidLaws}
  : forall m, (forall m', m' +m+ m = m') -> m = monoid_unit.
Proof.
  intros.
  specialize (H monoid_unit).
  setoid_rewrite monoid_lunit in H.
  assumption.
Qed.

Generalizable No Variables.

Global Instance MonList X : Monoid (list X)
  := {|
      monoid_plus := (@app X);
      monoid_unit := [];
    |}.
Global Program Instance MonLawsList X : MonoidLaws (MonList X).
Next Obligation.
  rewrite app_assoc.
  reflexivity.
Qed.
Next Obligation.
  rewrite app_nil_r.
  reflexivity.
Qed.

Global Instance MonPair M M' {MM : Monoid M} {MM' : Monoid M'}
  : Monoid (M*M')
  := {|
      monoid_plus := fun (x y : M*M') => let (x1,x2) := x in
                                      let (y1,y2) := y in
                                      (x1 +m+ y1, x2 +m+ y2);
      monoid_unit := (monoid_unit,monoid_unit)
    |}.
Global Program Instance MonLawsPair M M' {MM : Monoid M} {MM' : Monoid M'} {MLM : MonoidLaws MM} {MLM' : MonoidLaws MM'}
  : MonoidLaws (@MonPair M M' _ _).
Next Obligation.
  setoid_rewrite monoid_assoc.
  reflexivity.
Qed.
Next Obligation.
  setoid_rewrite monoid_lunit.
  reflexivity.
Qed.
Next Obligation.
  setoid_rewrite monoid_runit.
  reflexivity.
Qed.

Global Instance MonVecMon M {MM : Monoid M} (k : nat) : Monoid (Vector.t M k).
Proof.
  econstructor.
  - eapply (@Vector.map2 M M M (@monoid_plus M _)).
  - eapply (Vector.const (@monoid_unit M _)).
Defined.
Global Program Instance MonLawsVecMon M {MM : Monoid M} {MLM : MonoidLaws MM} (k : nat)
  : MonoidLaws (@MonVecMon M _ k).
Next Obligation.
  intros.
  rewrite vec_map2_map2_assoc;eauto.
  setoid_rewrite monoid_assoc.
  reflexivity.
Qed.
Next Obligation.
  intros.
  rewrite vec_map2_const1.
  setoid_rewrite Vector.map_ext with (g:=fun x => x).
  + eapply Vector.map_id.
  + setoid_rewrite monoid_lunit.
    reflexivity.
Qed.
Next Obligation.
  intros.
  rewrite vec_map2_const2.
  setoid_rewrite Vector.map_ext with (g:=fun x => x).
  + eapply Vector.map_id.
  + setoid_rewrite monoid_runit.
    reflexivity.
Qed.

Global Instance MonVecNat : forall (k : nat), Monoid@{Type} (Vector.t nat k).
Proof.
  intros. exact _.
Defined.
Global Instance MonLawsVecNat (k : nat) : MonoidLaws (MonVecNat k).
Proof.
  eapply MonLawsVecMon.
Qed.

Section with_MN12.
  Context {M1 M2 N1 N2 : Type}.
  Context (hom1 : M1 -> N1) (hom2 : M2 -> N2).

  Definition pair_hom (m : M1 * M2)
    := let (m1,m2) := m in (hom1 m1, hom2 m2).

  Global Instance pair_hom_inst `(MH1 : MonoidHomomorphism _ _ hom1) `(MH2 : MonoidHomomorphism _ _ hom2)
    : MonoidHomomorphism pair_hom.
  Proof.
    econstructor.
    - intros.
      unfold pair_hom.
      destruct m1 as [m11 m12]. destruct m2 as [m21 m22].
      cbn.
      setoid_rewrite homomorph.
      reflexivity.
    - cbn.
      setoid_rewrite homomorph_unit.
      reflexivity.
  Defined.

  Global Lemma pair_iso_inst `{MI1 : MonoidIsomorphism _ _ hom1} `{MI2 : MonoidIsomorphism _ _ hom2}
    (*{MonM1 : Monoid M1} {MonM2 : Monoid M2} {MonN1 : Monoid N1} {MonN2 : Monoid N2}*)
    : MonoidIsomorphism pair_hom.
  Proof.
    econstructor.
    - eapply pair_hom_inst.
      1,2:eapply MonoidIsomorphism_homomorph.
    - intros.
      destruct m1,m2.
      cbn in H.
      inversion H.
      f_equal.
      all:eapply injective;eauto.
    - intros.
      destruct m.
      specialize (surjective n) as Q1.
      specialize (surjective n0) as Q2.
      destruct Q1, Q2.
      exists (x,x0).
      cbn.
      f_equal;eauto.
  Defined.
End with_MN12.

Section with_X.
  Context {X : Type}.

  Global Instance len_hom
    : MonoidHomomorphism (@length X).
  Proof.
    constructor.
    - setoid_rewrite app_length.
      reflexivity.
    - cbn.
      reflexivity.
  Qed.
End with_X.