Section foldl_coeq.
Require Export List.
Variables A B:Set.
Variable f:A -> B -> B.
Variable b0:B.

Fixpoint foldl_list (b:B) (l:list A){struct l}:B:=
match l with
  nil => b
  |cons x xs => foldl_list (f x b) xs
end.

Implicit Arguments foldl_list.

Definition h1:=fun (a:A) => fun (b:B) => fun (ls:list A) => (pair b (cons a ls)).
Definition h2 :=fun (a:A) => fun (b:B) => fun (ls:list A) => ((f a b),ls).


Lemma one: forall a:A, forall b:B, forall ls:list A,
(foldl_list   (fst (h1 a b ls)) (snd (h1  a b ls)))=(foldl_list    (fst (h2 a b ls ))(snd (h2  a b ls))).
Proof.
intuition.
Qed.


Variable C:Set.

Lemma coequalizer: forall h:B->list A->C, (forall b:B, forall a:A, forall ls:list A,
(h (fst (h1  a b ls))(snd (h1 a b ls)) )=(h (fst (h2 a b ls))(snd (h2  a b ls)) ))
   -> { f':B->C | (forall ls:list A,forall b:B,  f'(foldl_list b ls)=h b ls)
                /\ (forall (g':B->C),(forall ls:list A, forall b:B, g' (foldl_list b ls)=h  b ls)
                    -> forall b:B,g' b=f' b) }.
Proof.
intros.
exists (fun b:B =>h b nil).
split.
induction ls;intros;simpl.
trivial.
rewrite IHls.
simpl in H;rewrite H;trivial.
intros.
replace (g' b) with (g' (foldl_list b nil)).
rewrite H0.
trivial.
auto.
Qed.
End foldl_coeq.

Section fusion. 
Variables A B C:Set.
Variable f:A -> B -> B.
Variable g:A -> C -> C.
Variable theta:B -> C.
Implicit Arguments foldl_list.

Hypothesis F1:forall a:A, forall b:B, theta (f a b)=g a (theta b).

Definition unif:=fun (b:B) => fun (ls:(list A)) => foldl_list  g  (theta b) ls .

Lemma UNIF: forall b:B, forall a:A,forall ls:list A,
(unif  (fst (h1 A B  a b ls)) (snd (h1 A B a b ls)))=
               (unif (fst (h2  A B  f a b ls)) (snd (h2  A B f  a b ls)) ).
Proof.
intros.
simpl.
unfold unif.
simpl.
rewrite F1;trivial.
Defined.


Lemma unification: { K1:B -> C | (forall ls:list A,forall b:B,
K1 (foldl_list  f  b ls)=unif  b ls)
 /\ (forall (g1:B->C),(forall ls:list A, forall b:B,g1 (foldl_list  f  b ls)=unif  b ls) 
     -> forall b:B,g1 b=K1 b) } .
Proof. 
apply coequalizer.
intros;rewrite UNIF;trivial.
Defined.

Definition K:= proj1_sig unification.


Lemma prefusion: forall ls:list A, forall b:B, theta (foldl_list  f  b ls)=
   foldl_list  g  (theta b) ls.
Proof.
induction ls;intros;simpl.
intuition.
rewrite <- F1.
intuition.
Defined.

Theorem fusion: forall ls:list A, forall b:B, forall c:C, theta b=c
      -> (forall a:A, forall b:B,theta (f a  b)=g a (theta b))
        -> theta (foldl_list  f b ls)=foldl_list  g c ls.
Proof.
unfold foldl_list;intros.
rewrite prefusion.
rewrite H;trivial.
Defined.
End fusion.



