shttpd/coq/S/Vector/Fold.v

(* SPDX-License-Identifier: GPL-2.0 or GPL-3.0
   Copyright © 2019 Ariadne Devos *)

Require Import Coq.Lists.List.
Require Import Coq.Lists.SetoidList.
Require Import Coq.Classes.Equivalence.
Require Import Coq.Classes.Morphisms.
Require Import Coq.Relations.Relations.

(* Fold a vector (by addition, multiplication ...) (represented as a list),
   with some lemma's for simplification. Assumes an identity element,
   commutativity and associativity.

   The fold function (badly named all, all_morphism), is modulo any
   equivalence relation (eqv, equiv) as long as the specified operator
   respects it (op, op_morphism). *)
Section vector_fold.

Variable A : Set.
Variable eqv : A -> A -> Prop.
Hypothesis equiv : Equivalence eqv.

Variable op : A -> A -> A.
Variable op_morphism : Proper (eqv ==> eqv ==> eqv) op.
Variable identity : A.

Hypothesis op_comm : forall x y, eqv (op x y) (op y x).
Hypothesis op_assoc : forall x y z, eqv (op (op x y) z) (op x (op y z)).
Hypothesis op_comm_identity_r : forall x, eqv (op x identity) x.

Lemma op_comm_identity_l : forall x, eqv (op identity x) x.
Proof. intro x. rewrite op_comm. apply op_comm_identity_r. Qed.

Local Open Scope list_scope.

(* TODO: not a good name.
   Combine all x in l by op with neutral element identity.
   (E.g., theta, sigma) *)
(* TODO: perhaps allow non-commutative operators, in which
   case a choice must be made between fold_left and fold_right. *)
   
Definition all l : A := fold_right op identity l.

(* Depends: A eqv equiv op op_morphism identity *)
Add Morphism all with
  signature (eqlistA eqv ==> eqv) as all_morphism.
Proof.
  intros x y P.
  unfold all.
  exact (fold_right_eqlistA equiv identity op_morphism P).
Qed.

Theorem all_nil : eqv (all nil) identity.
Proof. cbn. reflexivity. Qed.

Theorem all_peel a l : eqv (op a (all l)) (all (a :: l)).
Proof.
  unfold all.
  cbn.
  reflexivity.
Qed.

Theorem all_merge l m : eqv (op (all l) (all m)) (all (l ++ m)).
Proof.
  induction l.
  + rewrite all_nil.
    apply op_comm_identity_l.
  + rewrite <- app_comm_cons.
    repeat rewrite <- all_peel.
    rewrite op_assoc.
    eapply op_morphism.
    - reflexivity.
    - assumption.
Qed.

Theorem all_identity_l0 l : eqv (all (identity :: l)) (all l).
Proof.
  rewrite <- all_peel.
  rewrite op_comm_identity_l.
  reflexivity.
Qed.

Theorem all_identity_l1 l : eqv (all ((identity :: nil) ++ l)) (all l).
Proof.
  rewrite <- all_merge.
  rewrite all_identity_l0.
  rewrite all_nil.
  rewrite op_comm_identity_l.
  reflexivity.
Qed.

Theorem all_identity_r l : eqv (all (l ++ (identity :: nil))) (all l).
Proof.
  rewrite <- all_merge.
  rewrite all_identity_l0.
  rewrite all_nil.
  rewrite op_comm_identity_r.
  reflexivity.
Qed.

End vector_fold.