Library UniMath.Algebra.IteratedBinaryOperations

Require Export UniMath.Combinatorics.StandardFiniteSets.
Require Export UniMath.Combinatorics.Lists.
Require Export UniMath.Combinatorics.FVectors.
Require Export UniMath.Combinatorics.FMatrices.
Require Export UniMath.Combinatorics.FLists.
Require Export UniMath.Algebra.RigsAndRings.
Require Export UniMath.Foundations.UnivalenceAxiom.

Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.Algebra.Groups.
Require Import UniMath.MoreFoundations.NegativePropositions.



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

Section BinaryOperations.

  Context {X:UU} (unel:X) (op:binop X).


  Definition iterop_list : list X → X :=
    foldr1 op unel.

  Definition iterop_fun {n} (x:stn n->X) : X.
  Proof.
    intros.
    induction n as [|n _].
    { exact unel. }
    { induction n as [|n I].
      { exact (x lastelement). }
      { exact (op (I (x ∘ dni lastelement)) (x lastelement)). }}
  Defined.

  Definition iterop_seq : Sequence X → X.
  Proof.
    intros x.
    exact (iterop_fun x).
  Defined.


  Definition iterop_list_list : list(list X) → X.
  Proof.
    intros w.
    exact (iterop_list (map iterop_list w)).
  Defined.

  Definition iterop_fun_fun {n} {m:stn n → nat} : (∏ i (j:stn (m i)), X) → X.
  Proof.
    intros x.
    exact (iterop_fun (λ i, iterop_fun (x i))).
  Defined.

  Definition iterop_seq_seq : Sequence (Sequence X) → X.
  Proof.
    intros x.
    exact (iterop_fun_fun (λ i j, x i j)).
  Defined.

  Definition isAssociative_list := ∏ (x:list (list X)), iterop_list (Lists.flatten x) = iterop_list_list x.

  Definition isAssociative_fun :=
    ∏ n (m:stn n → nat) (x : ∏ i (j:stn (m i)), X), iterop_fun (StandardFiniteSets.flatten' x) = iterop_fun_fun x.

  Definition isAssociative_seq :=
    ∏ (x : Sequence (Sequence X)), iterop_seq (FLists.flatten x) = iterop_seq_seq x.

  Local Open Scope stn.

  Definition isCommutative_fun :=
    ∏ n (x:⟦n⟧ → X) (f:⟦n⟧≃⟦n⟧), iterop_fun (x ∘ f) = iterop_fun x.

  Lemma assoc_fun_to_seq : isAssociative_fun → isAssociative_seq.
  Proof.
    intros assoc x.
    exact (assoc _ _ (λ i j, x i j)).
  Defined.

  Lemma assoc_seq_to_fun : isAssociative_seq → isAssociative_fun.
  Proof.
    intros assoc n m x.
    exact (assoc (functionToSequence (λ i, functionToSequence (x i)))).
  Defined.

  Definition iterop_list_step (runax : isrunit op unel) (x:X) (xs:list X) :
    iterop_list (x::xs) = op x (iterop_list xs).
  Proof.
    generalize x; clear x.
    apply (list_ind (λ xs, ∏ x : X, iterop_list (x :: xs) = op x (iterop_list xs))).
    { intro x. simpl. apply pathsinv0,runax. }
    intros y rest IH x.
    reflexivity.
  Defined.

  Definition iterop_fun_step' (lunax : islunit op unel) {m} (xs:stn m → X) (x:X) :
    iterop_fun (append_vec xs x) = op (iterop_fun xs) x.
  Proof.
    unfold iterop_fun at 1.
    simpl.
    induction m as [|m _].
    - simpl. rewrite append_vec_compute_2. apply pathsinv0. apply lunax.
    - simpl. rewrite append_vec_compute_2.
      apply (maponpaths (λ y, op y x)). apply maponpaths.
      apply append_and_drop_fun.
  Defined.

  Definition iterop_fun_step (lunax : islunit op unel) {m} (x:stn(S m) → X) :
    iterop_fun x = op (iterop_fun (x ∘ dni lastelement)) (x lastelement).
  Proof.
    intros.
    unfold iterop_fun at 1.
    simpl.
    induction m as [|m _].
    - simpl. apply pathsinv0, lunax.
    - simpl. reflexivity.
  Defined.

  Definition iterop_fun_append (lunax : islunit op unel) {m} (x:stn m → X) (y:X) :
    iterop_fun (append_vec x y) = op (iterop_fun x) y.
  Proof.
    rewrite (iterop_fun_step lunax).
    rewrite append_vec_compute_2.
    apply (maponpaths (λ x, op (iterop_fun x) y)).
    apply funextfun; intro i.
    simpl.
    rewrite append_vec_compute_1.
    reflexivity.
  Defined.

End BinaryOperations.

Local Open Scope multmonoid.

Section Monoids.

  Context {M:monoid}.

  Let oo := @op M.

  Let uu := unel M.

  Definition iterop_fun_mon {n} (x:stn n->M) : M := iterop_fun uu oo x.

  Definition iterop_list_mon : list M → M := iterop_list uu oo.

  Definition iterop_seq_mon : Sequence M → M := iterop_seq uu oo.

  Definition iterop_seq_seq_mon : Sequence (Sequence M) → M := iterop_seq_seq uu oo.

  Definition iterop_list_list_mon : list (list M) → M := iterop_list_list uu oo.


  Lemma iterop_seq_mon_len1 (x : stn 1 → M) :
    iterop_seq_mon (functionToSequence x) = x lastelement.
  Proof.
    reflexivity.
  Defined.

  Lemma iterop_seq_mon_step {n} (x:stn (S n) → M) :
    iterop_seq_mon (S n,,x) = iterop_seq_mon (n,,x ∘ dni lastelement) * x lastelement.
  Proof.
    intros. induction n as [|n _].
    - cbn. apply pathsinv0, lunax.
    - reflexivity.
  Defined.

  Lemma iterop_list_mon_nil : iterop_list_mon [] = 1.
  Proof.
    reflexivity.
  Defined.

  Lemma iterop_list_mon_step (x:M) (xs:list M) :
    iterop_list_mon (x::xs) = x * iterop_list_mon xs.
  Proof.
    apply iterop_list_step. apply runax.
  Defined.

  Lemma iterop_list_mon_singleton (x : M) : iterop_list_mon (x::[]) = x.
  Proof.
    reflexivity.
  Defined.

  Local Lemma iterop_seq_mon_append (x:Sequence M) (m:M) :
    iterop_seq_mon (append x m) = iterop_seq_mon x * m.
  Proof.
     revert x m.
     intros [n x] ?. unfold append. rewrite iterop_seq_mon_step.
     rewrite append_vec_compute_2.
     apply (maponpaths (λ a, a * m)).
     apply (maponpaths (λ x, iterop_seq_mon (n,,x))).
     apply funextfun; intros [i b]; simpl.
     now rewrite append_vec_compute_1.
  Defined.

  Local Lemma iterop_seq_seq_mon_step {n} (x:stn (S n) → Sequence M) :
    iterop_seq_seq_mon (S n,,x) = iterop_seq_seq_mon (n,,x ∘ dni lastelement) * iterop_seq_mon (x lastelement).
  Proof.
    intros.
    induction n as [|n _].
    - simpl. apply pathsinv0,lunax.
    - reflexivity.
  Defined.

  Lemma iterop_seq_mon_homot {n} (x y : stn n → M) :
    x ~ y → iterop_seq_mon(n,,x) = iterop_seq_mon(n,,y).
  Proof.
    revert x y. induction n as [|n N].
    - reflexivity.
    - intros x y h. rewrite 2 iterop_seq_mon_step.
      apply two_arg_paths.
      + apply N. apply funhomot. exact h.
      + apply h.
  Defined.

End Monoids.

Section Monoids2.

  Context (M:monoid).

  Let op := @op M.

  Let unel := unel M.

  Definition isAssociative_list_mon := isAssociative_list unel op.

  Definition isAssociative_fun_mon := isAssociative_fun unel op.

  Definition isAssociative_seq_mon := isAssociative_seq unel op.

  Definition isCommutative_fun_mon := isCommutative_fun unel op.

End Monoids2.

Lemma iterop_list_mon_concatenate {M : monoid} (l s : list M) :
  iterop_list_mon (Lists.concatenate l s) = iterop_list_mon l * iterop_list_mon s.
Proof.
  revert l. apply list_ind.
  - apply pathsinv0, lunax.
  - intros x xs J. rewrite Lists.concatenateStep.
    unfold iterop_list_mon.
    rewrite 2 (iterop_list_step _ _ (runax M)).
    rewrite assocax. apply maponpaths. exact J.
Defined.

Theorem associativityOfProducts_list (M:monoid) : isAssociative_list (unel M) (@op M).
Proof.

  unfold isAssociative_list.
  apply list_ind.
  - simpl. reflexivity.
  - intros x xs I. simpl in I.
    rewrite Lists.flattenStep. refine (iterop_list_mon_concatenate _ _ @ _).
    unfold iterop_list_list. rewrite mapStep.
    rewrite (iterop_list_step _ _ (runax M)).
    + apply (maponpaths (λ x, _ * x)). exact I.
Defined.

Theorem associativityOfProducts_seq (M:monoid) : isAssociative_seq (unel M) (@op M).
Proof.

  unfold isAssociative_seq; intros. induction x as [n x].
  induction n as [|n IHn].
  { reflexivity. }
  change (flatten _) with (flatten ((n,,x): NonemptySequence _)).
  rewrite flattenStep.
  change (lastValue _) with (x lastelement).
  unfold iterop_seq_seq. simpl.
  unfold iterop_fun_fun.
  rewrite (iterop_fun_step _ _ (lunax M)).
  generalize (x lastelement) as z; intro z.
  unfold iterop_seq.
  induction z as [m z].
  induction m as [|m IHm].
  { simpl. rewrite runax.
    simple refine (_ @ IHn (x ∘ dni lastelement)).
    rewrite concatenate'_r0.
    now apply (two_arg_paths_b (natplusr0 (stnsum (length ∘ (x ∘ dni lastelement))))). }
  change (length (S m,, z)) with (S m). change (sequenceToFunction (S m,,z)) with z.
  rewrite (iterop_fun_step _ _ (lunax M)). rewrite concatenateStep.
  generalize (z lastelement) as w; intros.
  rewrite <- assocax. unfold append.
  Opaque iterop_fun. simpl. Transparent iterop_fun.
  rewrite (iterop_fun_append _ _ (lunax M)).
  apply (maponpaths (λ u, u*w)). simpl in IHm. apply IHm.
Defined.

Corollary associativityOfProducts' {M:monoid} {n} (f:stn n → nat) (x:stn (stnsum f) → M) :
  iterop_seq_mon (stnsum f,,x) = iterop_seq_seq_mon (partition f x).
Proof.
  intros. refine (_ @ associativityOfProducts_seq M (partition f x)).
  assert (L := flatten_partition f x). apply pathsinv0. exact (iterop_seq_mon_homot _ _ L).
Defined.

Local Notation "s □ x" := (append s x) (at level 64, left associativity).

Ltac change_lhs a := match goal with |- @paths ?T ?x ?y
                                     => change (@paths T x y) with (@paths T a y) end.
Ltac change_rhs a := match goal with |- @paths ?T ?x ?y
                                     => change (@paths T x y) with (@paths T x a) end.

Local Open Scope stn.

Lemma commutativityOfProducts_helper {M:abmonoid} {n} (x:stn (S n) → M) (j:stn (S n)) :
  iterop_seq_mon (S n,,x) = iterop_seq_mon (n,,x ∘ dni j) * x j.
Proof.
  induction j as [j jlt].
  assert (jle := natlthsntoleh _ _ jlt).
  Local Open Scope transport.
  set (f := nil □ j □ S O □ n-j : stn 3 → nat).
  assert (B : stnsum f = S n).
  { unfold stnsum, f; simpl. repeat unfold append_vec; simpl. rewrite natplusassoc.
    rewrite (natpluscomm 1). rewrite <- natplusassoc.
    rewrite natpluscomm. apply (maponpaths S). rewrite natpluscomm. now apply minusplusnmm. }
  set (r := weqfibtototal _ _ (λ k, eqweqmap (maponpaths (λ n, k < n : UU) B) ) :
              stn (stnsum f) ≃ stn (S n)).
  set (x' := x ∘ r).
  intermediate_path (iterop_seq_mon (stnsum f,, x')).
  { induction B. apply iterop_seq_mon_homot. intros i. unfold x'.
    simpl. apply maponpaths.
    apply ( invmaponpathsincl _ ( isinclstntonat _ ) _ _).
    reflexivity. }
  unfold iterop_seq_mon. unfold iterop_seq.
  refine (associativityOfProducts' f x' @ _).
  unfold partition.
  rewrite 3 iterop_seq_seq_mon_step.
  change (iterop_seq_seq_mon (0,,_)) with (unel M); rewrite lunax.
  set (s0 := dni lastelement (dni lastelement (@lastelement 0))).
  unfold funcomp at 1 2 3.
  set (s1 := dni lastelement (@lastelement 1)).
  set (s2 := @lastelement 2).
  unfold partition'. unfold inverse_lexicalEnumeration.
  change (f s0) with j; change (f s1) with (S O); change (f s2) with (n-j).
  set (f' := nil □ j □ n-j : stn 2 → nat).
  assert (B' : stnsum f' = n).
  { unfold stnsum, f'; simpl. repeat unfold append_vec; simpl.
    rewrite natpluscomm. now apply minusplusnmm. }
  set (r' := weqfibtototal _ _ (λ k, eqweqmap (maponpaths (λ n, k < n : UU) B') ) :
              stn (stnsum f') ≃ stn n).
  set (x'' := x ∘ dni (j,, jlt) ∘ r').
  intermediate_path (iterop_seq_mon (stnsum f',, x'') * x (j,, jlt)).
  { assert (L := iterop_seq_mon_len1 (λ j0 : stn 1, x' ((weqstnsum1 f) (s1,, j0)))).
    unfold functionToSequence in L.
    rewrite L. rewrite assocax. refine (transportf (λ k, _*k=_) (commax _ _ _) _).
    rewrite <- assocax.
    apply two_arg_paths.
    { refine (_ @ !associativityOfProducts' f' x'').
      unfold partition.
      rewrite 2 iterop_seq_seq_mon_step.
      change (iterop_seq_seq_mon (0,,_)) with (unel M); rewrite lunax.
      apply two_arg_paths.
      { unfold funcomp. set (s0' := dni lastelement (@lastelement 0)).
        unfold partition'. change (f' s0') with j.
        apply iterop_seq_mon_homot. intro i. unfold x', x'', funcomp. apply maponpaths.
        apply subtypePath_prop.
        change_lhs (stntonat _ i).
        unfold dni. unfold di.
        unfold stntonat.
        match goal with |- context [ match ?x with _ => _ end ]
                        => induction x as [c|c] end.
        { reflexivity. }
        { apply fromempty. assert (P := c : i ≥ j); clear c.
          exact (natlthtonegnatgeh _ _ (stnlt i) P). } }
      { unfold partition'. change (f' lastelement) with (n-j).
        apply iterop_seq_mon_homot. intro i. unfold x', x'', funcomp. apply maponpaths.
        apply subtypePath_prop. change_lhs (j+1+i). unfold dni, di.
        unfold stntonat.
        match goal with |- context [ match ?x with _ => _ end ]
                        => induction x as [c|c] end.
        { apply fromempty. exact (negnatlthplusnmn j i c). }
        { change_rhs (1 + (j + i)). rewrite <- natplusassoc. rewrite (natpluscomm j 1).
          reflexivity. } } }
    unfold x'; simpl. apply maponpaths.
    apply subtypePath_prop. change (j+0 = j). apply natplusr0. }
  { apply (maponpaths (λ k, k * _)). induction (!B').
    change_rhs (iterop_seq_mon (n,, x ∘ dni (j,, jlt))).
    apply iterop_seq_mon_homot; intros i.
    unfold x''; simpl. apply maponpaths.
    apply ( invmaponpathsincl _ ( isinclstntonat _ ) _ _).
    reflexivity. }
Qed.

Theorem commutativityOfProducts {M:abmonoid} {n} (x:stn n->M) (f:stn n ≃ stn n) :
  iterop_seq_mon (n,,x) = iterop_seq_mon (n,,x∘f).
Proof.
  intros. induction n as [|n IH].
  - reflexivity.
  - set (i := @lastelement n); set (i' := f i).
    rewrite (iterop_seq_mon_step (x ∘ f)).
    change ((x ∘ f) lastelement) with (x i').
    rewrite (commutativityOfProducts_helper x i').
    apply (maponpaths (λ k, k*_)).
    set (f' := weqoncompl_ne f i (stnneq i) (stnneq i') : stn_compl i ≃ stn_compl i').
    set (g := weqdnicompl i); set (g' := weqdnicompl i').
    apply pathsinv0.
    set (h := (invweq g' ∘ f' ∘ g)%weq).
    assert (L : x ∘ f ∘ dni lastelement ~ x ∘ dni i' ∘ h).
    { intro j. unfold funcomp. apply maponpaths.
      apply (invmaponpathsincl _ ( isinclstntonat _ ) _ _).
      unfold h. rewrite 2 weqcomp_to_funcomp_app. rewrite pr1_invweq.
      induction j as [j J]. unfold g, i, f', g', stntonat.
      rewrite <- (weqdnicompl_compute i').
      unfold pr1compl_ne.
      rewrite homotweqinvweq.
      rewrite (weqoncompl_ne_compute f i (stnneq i) (stnneq i') _).
      apply maponpaths, maponpaths.
      apply subtypePath_prop.
      unfold stntonat.
      now rewrite weqdnicompl_compute. }
    rewrite (IH (x ∘ dni i') h).
    now apply iterop_seq_mon_homot.
Defined.

  Require Export UniMath.Combinatorics.FiniteSets.
  Require Export UniMath.Foundations.NaturalNumbers.

Section NatCard.

  Theorem nat_plus_associativity {n} {m:stn n->nat} (k:∏ (ij : ∑ i, stn (m i)), nat) :
    stnsum (λ i, stnsum (curry k i)) = stnsum (k ∘ lexicalEnumeration m).
  Proof.
    intros. apply weqtoeqstn.
    intermediate_weq (∑ i, stn (stnsum (curry k i))).
    { apply invweq. apply weqstnsum1. }
    intermediate_weq (∑ i j, stn (curry k i j)).
    { apply weqfibtototal; intro i. apply invweq. apply weqstnsum1. }
    intermediate_weq (∑ ij, stn (k ij)).
    { exact (weqtotal2asstol (stn ∘ m) (stn ∘ k)). }
    intermediate_weq (∑ ij, stn (k (lexicalEnumeration m ij))).
    { apply (weqbandf (inverse_lexicalEnumeration m)). intro ij. apply eqweqmap.
      apply (maponpaths stn), (maponpaths k). apply pathsinv0, homotinvweqweq. }
    apply inverse_lexicalEnumeration.
  Defined.

  Corollary nat_plus_associativity' n (m:stn n->nat) (k:∏ i, stn (m i) → nat) :
    stnsum (λ i, stnsum (k i)) = stnsum (uncurry (Z := λ _,_) k ∘ lexicalEnumeration m).
  Proof. intros. exact (nat_plus_associativity (uncurry k)). Defined.

  Lemma iterop_fun_nat {n:nat} (x:stn n->nat) : iterop_fun 0 add x = stnsum x.
  Proof.
    intros. induction n as [|n I].
    - reflexivity.
    - induction n as [|n _].
      + reflexivity.
      + simple refine (iterop_fun_step 0 add natplusl0 _ @ _ @ ! stnsum_step _).
        apply (maponpaths (λ i, i + x lastelement)). apply I.
  Defined.

  Theorem associativityNat : isAssociative_fun 0 add.
  Proof.
    intros n m x. unfold iterop_fun_fun. apply pathsinv0. rewrite 2 iterop_fun_nat.
    intermediate_path (stnsum (λ i : stn n, stnsum (x i))).
    - apply maponpaths. apply funextfun; intro. apply iterop_fun_nat.
    - now apply nat_plus_associativity'.
  Defined.

  Definition finsum' {X} (fin : isfinite X) (f : X → nat) : nat.
  Proof.
    intros. exact (fincard (isfinitetotal2 (stn∘f) fin (λ i, isfinitestn (f i)))).
  Defined.


End NatCard.

Definition MultipleOperation (X:UU) : UU := UnorderedSequence X → X.

Section Mult.

  Context {X:UU} (op : MultipleOperation X).

  Definition composeMultipleOperation : UnorderedSequence (UnorderedSequence X) → X.
  Proof.
    intros s. exact (op (composeUnorderedSequence op s)).
  Defined.

  Definition isAssociativeMultipleOperation := ∏ x, op (flattenUnorderedSequence x) = composeMultipleOperation x.

End Mult.

Definition AssociativeMultipleOperation {X} := ∑ op:MultipleOperation X, isAssociativeMultipleOperation op.

Definition iterop_unoseq_mon {M:abmonoid} : MultipleOperation M.
Proof.
  intros m.
  induction m as [J m].
  induction J as [I fin].
  simpl in m.
  unfold isfinite, finstruct in fin.
  simple refine (squash_to_set
                   (setproperty M)
                   (λ (g : finstruct I), iterop_fun_mon (m ∘ g : _ → M))
                   _
                   fin).
  intros. induction x as [n x]. induction x' as [n' x'].
  assert (p := weqtoeqstn (invweq x' ∘ x)%weq).
  induction p.
  assert (w := commutativityOfProducts (m ∘ x') (invweq x' ∘ x)%weq).
  simple refine (_ @ ! w); clear w. unfold iterop_seq_mon, iterop_fun_mon, iterop_seq.
  apply maponpaths. rewrite weqcomp_to_funcomp. apply funextfun; intro i.
  simpl. apply maponpaths. exact (! homotweqinvweq x' (x i)).
Defined.

Definition iterop_unoseq_abgr {G:abgr} : MultipleOperation G.
Proof.
  exact (iterop_unoseq_mon (M:=G)).
Defined.

Definition sum_unoseq_ring {R:ring} : MultipleOperation R.
Proof.
  exact (iterop_unoseq_mon (M:=R)).
Defined.

Definition product_unoseq_ring {R:commring} : MultipleOperation R.
Proof.
  exact (iterop_unoseq_mon (M:=ringmultabmonoid R)).
Defined.

Definition iterop_unoseq_unoseq_mon {M:abmonoid} : UnorderedSequence (UnorderedSequence M) → M.
Proof.
  intros s. exact (composeMultipleOperation iterop_unoseq_mon s).
Defined.

Definition abmonoidMultipleOperation {M:abmonoid} (op := @iterop_unoseq_mon M) : MultipleOperation M
  := iterop_unoseq_mon.

Theorem isAssociativeMultipleOperation_abmonoid {M:abmonoid}
  : isAssociativeMultipleOperation (@iterop_unoseq_mon M).
Proof.

Abort.