accumulating_map.v

Require Import List.

Fixpoint fold_left_raw
  (A B   : Set)
  (step  : A -> B -> B)
  (accum : B)
  (src   : list A)
         : B
:=
  match src with
  | nil    => accum
  | h :: t => fold_left_raw _ _ step (step h accum) t
  end.

Notation fold_left := (fold_left_raw _ _).

Definition reverse_raw
  (A   : Set)
       : list A -> list A
:= fold_left (fun h t => h :: t) nil.

Notation reverse := (reverse_raw _).

Definition compose
  (A B C : Set) 
  (f     : B -> C) 
  (g     : A -> B) 
         : A -> C
:=
  fun x => f (g x).

Notation "f @ g"  := (compose _ _ _ f g) (at level 50).

Definition map2_raw
  (A B : Set)
  (f   : A -> B)
       : list A -> list B
:=
  reverse @ fold_left (fun item acc => f item :: acc) nil.

Notation map2 := (map2_raw _ _).

Lemma map2_and_cons_are_distributive
  : forall A B : Set
  , forall f   : A -> B
  , forall src : list A
  , forall e   : A,

    map2 f (e :: src) = f e :: map2 f src.

Proof.
  induction src. simpl.
    intros. unfold map2_raw.
    simpl. trivial.

    intros.