Library UniMath.Algebra.Tests

Require UniMath.Algebra.IteratedBinaryOperations.
Require UniMath.Foundations.NaturalNumbers.
Require UniMath.Algebra.IteratedBinaryOperations.
Require UniMath.Combinatorics.FiniteSets.

Module Test_assoc.

  Import UniMath.Algebra.IteratedBinaryOperations.
  Import UniMath.Foundations.NaturalNumbers.


  Local Notation "[]" := Lists.nil (at level 0, format "[]").
  Local Infix "::" := cons.

  Section Test.
    Context (X:UU) (e:X) (op:binop X) (w x y z:X).
    Goal iterop_list e op [] = e. reflexivity. Qed.
    Goal iterop_list e op (x::[]) = x. reflexivity. Qed.
    Goal iterop_list e op (x::y::[]) = op x y. reflexivity. Qed.
    Goal iterop_list e op (w::x::y::z::[]) = op w (op x (op y z)). reflexivity. Qed.
  End Test.

  Local Open Scope stn.

  Open Scope multmonoid.

  Goal ∏ (M:monoid) (f:stn 3 -> M),
         iterop_seq_mon(3,,f) = f(●O) * f(●1%nat) * f(●2).
  Show proof.

  Goal ∏ (M:monoid) (f:stn 3 -> Sequence M),
         iterop_seq_seq_mon(3,,f) =
                iterop_seq_mon (f(●0))
              * iterop_seq_mon (f(●1%nat))
              * iterop_seq_mon (f(●2)).
  Show proof.

  Goal ∏ (M:monoid) (x y z:M), x*y*z = (x*y)*z. Show proof.
  Goal ∏ (M:monoid) (x y z:M), x*y*z = x*(y*z). Show proof.

  Local Open Scope addmonoid.
  Import UniMath.Algebra.Monoids.AddNotation.
  Goal ∏ (M:monoid) (x y z:M), x+y+z = (x+y)+z. Show proof.
  Goal ∏ (M:monoid) (x y z:M), x+y+z = x+(y+z). Show proof.

End Test_assoc.