foldR_foldL.v

(*  Proof that you can build foldR out of foldL *)


Require Import Arith List. Import ListNotations.


Fixpoint foldR {A : Type} {B : Type} (f : A -> B -> B) (v : B) (l : list A) : B :=
  match l with
  | nil => v
  | x :: xs => f x (foldR f v xs)
  end.

Fixpoint foldL {A : Type} {B : Type} (f : B -> A -> B) (v : B) (l : list A) : B :=
  match l with
  | nil => v
  | x :: xs => foldL f (f v x) xs
  end.

Definition foldR' {A B : Type} (f : B -> A -> A) (a : A) (xs : list B) :=
  foldL (fun g b x => g (f b x)) id xs a.


(* a useful induction principle that gives a stronger IH than 
   plain structural induction on l *)

Lemma list_length_ind A (P:list A -> Prop):
  ( forall l, (forall l', length l' < length l -> P l' ) -> P l) -> forall l, P l.
  intros IH.
  assert (H: forall (X Y:list A), length Y <= length X -> P Y).
  { induction X.
    - intros [|Y] Q. apply IH; inversion 1. exfalso; inversion Q. 
    - intros; apply IH; intros.
      assert (length l' <= length X).
      { inversion H. 
        rewrite H2 in *.
        apply le_S_n, H0.
        apply le_trans with (length Y).
        apply Nat.lt_le_incl, H0. apply H2. }

      apply (IHX _ H1). }
  intros l. apply (H l). reflexivity.
Qed.    



Lemma foldL_tail
      {A : Type} {B : Type}  (l : list B):
  forall a b (f : A -> B -> A),
    foldL f a (l++[b]) = f (foldL f a l) b.

  induction l;
    intros.
  reflexivity.

  simpl.
  rewrite IHl.
  reflexivity.
Qed.


Lemma foldR'_tail
      {A : Type} {B : Type}  (l : list B):
  forall a b (f : B -> A -> A),
    foldR' f a (l++[b]) = foldR' f (f b a) l.

  destruct l.
  reflexivity.

  intros.
  unfold foldR'.
  rewrite foldL_tail.
  reflexivity.
Qed.


Lemma foldR'_cons
      {A : Type} {B : Type}  (l : list B):
  forall a b (f : B -> A -> A),
    foldR' f a (b::l) = f b (foldR' f a l).
Proof.
  induction l using list_length_ind.
  rename H into IH.
  intros.

  destruct (@exists_last _ (b::l)) as [l' [a' H']].
  inversion 1.
  rewrite H'.

  rewrite foldR'_tail.

  destruct l'.
  inversion H'.
  reflexivity.

  inversion H'.
  subst.
  rewrite IH.
  rewrite foldR'_tail.
  reflexivity.

  rewrite app_length.
  apply Nat.lt_add_pos_r, Nat.lt_0_succ.
Qed.

Theorem new_foldR_eq_foldR' {A : Type} {B : Type} :
  forall
    (f : B -> A -> A) 
    (a : A)
    (l : list B),

      foldR f a l = foldR' f a l.
Proof.
  intros.
  induction l; intros.
  reflexivity.
  simpl. 
  rewrite IHl, foldR'_cons.
  reflexivity.
Qed.