From Tealeaves Require Export
  Classes.Functor
  Functors.List
  Classes.Monoid
  Classes.Kleisli.DecoratedMonad.

Import List.ListNotations.
Import Monoid.Notations.


(** * Mapping over a List with History *)
(**********************************************************************)

(** ** Operation <<hmap>> *)
(**********************************************************************)
(* Map a context-sensitive function over the list, where the context
   is the prefix of the list up to the point considered. hfold = fold
   with history. *)
Fixpoint hmap {A B: Type} (f: list A * A -> B) (l: list A): list B :=
  match l with
  | nil => nil
  | cons a rest => cons (f (Ƶ, a)) (hmap (preincr f [a]) rest)
  end.

Lemma hmap_cons {A B: Type} (f: list A * A -> B) (a: A) (l: list A):
  hmap f (a :: l) = cons (f (Ƶ, a)) (hmap (preincr f [a]) l).
A, B: Type
f: list A * A -> B
a: A
l: list A
hmap f (a :: l) = f (Ƶ, a) :: hmap (f ⦿ [a]) l
Proof.
A, B: Type
f: list A * A -> B
a: A
l: list A
hmap f (a :: l) = f (Ƶ, a) :: hmap (f ⦿ [a]) l
  reflexivity.
Qed.

Lemma hmap_app:
  forall {WA WB: Type}
    (ρf: list WA * WA -> WB)
    (wa wa': list WA),
    hmap ρf (wa ● wa') =
      hmap ρf wa ● hmap (preincr ρf wa) wa'.
forall (WA WB : Type) (ρf : list WA * WA -> WB)
  (wa wa' : list WA),
hmap ρf (wa ● wa') = hmap ρf wa ● hmap (ρf ⦿ wa) wa'
Proof.
forall (WA WB : Type) (ρf : list WA * WA -> WB)
  (wa wa' : list WA),
hmap ρf (wa ● wa') = hmap ρf wa ● hmap (ρf ⦿ wa) wa'
  intros.
WA, WB: Type
ρf: list WA * WA -> WB
wa, wa': list WA
hmap ρf (wa ● wa') = hmap ρf wa ● hmap (ρf ⦿ wa) wa' generalize dependent ρf.
WA, WB: Type
wa, wa': list WA
forall ρf : list WA * WA -> WB,
hmap ρf (wa ● wa') = hmap ρf wa ● hmap (ρf ⦿ wa) wa' induction wa; intros ρf.
WA, WB: Type
wa': list WA
ρf: list WA * WA -> WB
hmap ρf ([] ● wa') = hmap ρf [] ● hmap (ρf ⦿ []) wa'
WA, WB: Type
a: WA
wa, wa': list WA
IHwa: forall ρf : list WA * WA -> WB,
hmap ρf (wa ● wa') =
hmap ρf wa ● hmap (ρf ⦿ wa) wa'
ρf: list WA * WA -> WB
hmap ρf ((a :: wa) ● wa') =
hmap ρf (a :: wa) ● hmap (ρf ⦿ (a :: wa)) wa'
  -
WA, WB: Type
wa': list WA
ρf: list WA * WA -> WB
hmap ρf ([] ● wa') = hmap ρf [] ● hmap (ρf ⦿ []) wa' change (@nil WA) with (Ƶ: list WA) at 1 3.
WA, WB: Type
wa': list WA
ρf: list WA * WA -> WB
hmap ρf ((Ƶ : list WA) ● wa') =
hmap ρf [] ● hmap (ρf ⦿ (Ƶ : list WA)) wa'
    rewrite monoid_id_l.
WA, WB: Type
wa': list WA
ρf: list WA * WA -> WB
hmap ρf wa' = hmap ρf [] ● hmap (ρf ⦿ Ƶ) wa'
    rewrite preincr_zero.
WA, WB: Type
wa': list WA
ρf: list WA * WA -> WB
hmap ρf wa' = hmap ρf [] ● hmap ρf wa'
    reflexivity.
  -
WA, WB: Type
a: WA
wa, wa': list WA
IHwa: forall ρf : list WA * WA -> WB,
hmap ρf (wa ● wa') =
hmap ρf wa ● hmap (ρf ⦿ wa) wa'
ρf: list WA * WA -> WB
hmap ρf ((a :: wa) ● wa') =
hmap ρf (a :: wa) ● hmap (ρf ⦿ (a :: wa)) wa' cbn.
WA, WB: Type
a: WA
wa, wa': list WA
IHwa: forall ρf : list WA * WA -> WB,
hmap ρf (wa ● wa') =
hmap ρf wa ● hmap (ρf ⦿ wa) wa'
ρf: list WA * WA -> WB
ρf (Ƶ, a) :: hmap (ρf ⦿ [a]) (wa ● wa') =
ρf (Ƶ, a)
:: hmap (ρf ⦿ [a]) wa ● hmap (ρf ⦿ (a :: wa)) wa' fequal.
WA, WB: Type
a: WA
wa, wa': list WA
IHwa: forall ρf : list WA * WA -> WB,
hmap ρf (wa ● wa') =
hmap ρf wa ● hmap (ρf ⦿ wa) wa'
ρf: list WA * WA -> WB
hmap (ρf ⦿ [a]) (wa ● wa') =
hmap (ρf ⦿ [a]) wa ● hmap (ρf ⦿ (a :: wa)) wa' rewrite IHwa.
WA, WB: Type
a: WA
wa, wa': list WA
IHwa: forall ρf : list WA * WA -> WB,
hmap ρf (wa ● wa') =
hmap ρf wa ● hmap (ρf ⦿ wa) wa'
ρf: list WA * WA -> WB
hmap (ρf ⦿ [a]) wa ● hmap ((ρf ⦿ [a]) ⦿ wa) wa' =
hmap (ρf ⦿ [a]) wa ● hmap (ρf ⦿ (a :: wa)) wa'
    rewrite preincr_preincr.
WA, WB: Type
a: WA
wa, wa': list WA
IHwa: forall ρf : list WA * WA -> WB,
hmap ρf (wa ● wa') =
hmap ρf wa ● hmap (ρf ⦿ wa) wa'
ρf: list WA * WA -> WB
hmap (ρf ⦿ [a]) wa ● hmap (ρf ⦿ ([a] ● wa)) wa' =
hmap (ρf ⦿ [a]) wa ● hmap (ρf ⦿ (a :: wa)) wa'
    reflexivity.
Qed.

(** ** Alternative Definition of <<hmap>> *)
(**********************************************************************)
Module Hmap_alt.

  Fixpoint hmap_rec
    {A B: Type} (f: list A * A -> B) (ctx: list A) (l: list A): list B :=
    match l with
    | nil => nil
    | cons a rest => cons (f (ctx, a)) (hmap_rec f (ctx ● [a]) rest)
    end.

  Lemma hmap_rec_cons
    {A B: Type} (f: list A * A -> B) (ctx: list A) (a: A) (l: list A):
    hmap_rec f ctx (a :: l) =
      cons (f (ctx, a)) (hmap_rec f (ctx ++ [a]) l).
A, B: Type
f: list A * A -> B
ctx: list A
a: A
l: list A
hmap_rec f ctx (a :: l) =
f (ctx, a) :: hmap_rec f (ctx ++ [a]) l
  Proof.
A, B: Type
f: list A * A -> B
ctx: list A
a: A
l: list A
hmap_rec f ctx (a :: l) =
f (ctx, a) :: hmap_rec f (ctx ++ [a]) l
    reflexivity.
  Qed.

  Definition hmap' {A B: Type} (f: list A * A -> B): list A -> list B :=
    hmap_rec f nil.

  Lemma hmap_rec_spec:
    forall {A B} (f: list A * A -> B) a,
      hmap (preincr f a) = hmap_rec f a.
forall (A B : Type) (f : list A * A -> B) (a : list A),
hmap (f ⦿ a) = hmap_rec f a
  Proof.
forall (A B : Type) (f : list A * A -> B) (a : list A),
hmap (f ⦿ a) = hmap_rec f a
    intros.
A, B: Type
f: list A * A -> B
a: list A
hmap (f ⦿ a) = hmap_rec f a ext l.
A, B: Type
f: list A * A -> B
a, l: list A
hmap (f ⦿ a) l = hmap_rec f a l
    generalize dependent a.
A, B: Type
f: list A * A -> B
l: list A
forall a : list A, hmap (f ⦿ a) l = hmap_rec f a l induction l.
A, B: Type
f: list A * A -> B
forall a : list A, hmap (f ⦿ a) [] = hmap_rec f a []
A, B: Type
f: list A * A -> B
a: A
l: list A
IHl: forall a : list A, hmap (f ⦿ a) l = hmap_rec f a l
forall a0 : list A,
hmap (f ⦿ a0) (a :: l) = hmap_rec f a0 (a :: l)
    -
A, B: Type
f: list A * A -> B
forall a : list A, hmap (f ⦿ a) [] = hmap_rec f a [] intros.
A, B: Type
f: list A * A -> B
a: list A
hmap (f ⦿ a) [] = hmap_rec f a [] reflexivity.
    -
A, B: Type
f: list A * A -> B
a: A
l: list A
IHl: forall a : list A, hmap (f ⦿ a) l = hmap_rec f a l
forall a0 : list A,
hmap (f ⦿ a0) (a :: l) = hmap_rec f a0 (a :: l) intros.
A, B: Type
f: list A * A -> B
a: A
l: list A
IHl: forall a : list A, hmap (f ⦿ a) l = hmap_rec f a l
a0: list A
hmap (f ⦿ a0) (a :: l) = hmap_rec f a0 (a :: l) cbn.
A, B: Type
f: list A * A -> B
a: A
l: list A
IHl: forall a : list A, hmap (f ⦿ a) l = hmap_rec f a l
a0: list A
(f ⦿ a0) (Ƶ, a) :: hmap ((f ⦿ a0) ⦿ [a]) l =
f (a0, a) :: hmap_rec f (a0 ● [a]) l
      rewrite preincr_preincr.
A, B: Type
f: list A * A -> B
a: A
l: list A
IHl: forall a : list A, hmap (f ⦿ a) l = hmap_rec f a l
a0: list A
(f ⦿ a0) (Ƶ, a) :: hmap (f ⦿ (a0 ● [a])) l =
f (a0, a) :: hmap_rec f (a0 ● [a]) l
      rewrite IHl.
A, B: Type
f: list A * A -> B
a: A
l: list A
IHl: forall a : list A, hmap (f ⦿ a) l = hmap_rec f a l
a0: list A
(f ⦿ a0) (Ƶ, a) :: hmap_rec f (a0 ● [a]) l =
f (a0, a) :: hmap_rec f (a0 ● [a]) l
      unfold preincr, compose, incr.
A, B: Type
f: list A * A -> B
a: A
l: list A
IHl: forall a : list A, hmap (f ⦿ a) l = hmap_rec f a l
a0: list A
f (a0 ● Ƶ, a) :: hmap_rec f (a0 ● [a]) l =
f (a0, a) :: hmap_rec f (a0 ● [a]) l
      rewrite monoid_id_r.
A, B: Type
f: list A * A -> B
a: A
l: list A
IHl: forall a : list A, hmap (f ⦿ a) l = hmap_rec f a l
a0: list A
f (a0, a) :: hmap_rec f (a0 ● [a]) l =
f (a0, a) :: hmap_rec f (a0 ● [a]) l
      reflexivity.
  Qed.

  Lemma hmap_spec:
    forall {A B} (f: list A * A -> B), hmap f = hmap' f.
forall (A B : Type) (f : list A * A -> B),
hmap f = hmap' f
  Proof.
forall (A B : Type) (f : list A * A -> B),
hmap f = hmap' f
    intros.
A, B: Type
f: list A * A -> B
hmap f = hmap' f
    replace f with
      (preincr f Ƶ) at 1 by (now rewrite preincr_zero).
A, B: Type
f: list A * A -> B
hmap (f ⦿ Ƶ) = hmap' f
    apply hmap_rec_spec.
  Qed.

End Hmap_alt.