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).
  Proof. reflexivity. Defined.

  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)).
  Proof. reflexivity. Defined.

  Goal ∏ (M:monoid) (x y z:M), x×y×z = (x×y)*z. Proof. reflexivity. Defined.
  Goal ∏ (M:monoid) (x y z:M), x×y×z = x*(y×z). Proof. apply assocax. Defined.

  Local Open Scope addmonoid.
  Import UniMath.Algebra.Monoids.AddNotation.
  Goal ∏ (M:monoid) (x y z:M), x+y+z = (x+y)+z. Proof. reflexivity. Defined.
  Goal ∏ (M:monoid) (x y z:M), x+y+z = x+(y+z). Proof. apply assocax. Defined.

End Test_assoc.