Require Import Arith.

Inductive list (X: Type) := nil | cons : X -> list X -> list X.
   
Implicit Arguments nil [X].
Implicit Arguments cons [X].
Notation "x :: y" := (cons x y) (at level 60, right associativity).
Notation "[ x , .. , y ]" := (cons x .. (cons y nil) ..).

Fixpoint length X (xs: list X):= match xs with
| nil => 0
| x::xr => S(length X xr)
end.

Implicit Arguments length [X].

Fixpoint app X (xs ys: list X) := match xs with
 | nil => ys
 | x::xr => x::app X xr ys
end.

Implicit Arguments app [X].
Notation "x ++ y" := (app x y) (at level 60, right associativity).

Proposition Assoc: forall X (xs ys zs: list X),
xs++(ys++zs) = (xs++ys)++zs.

Proof. intros. induction xs.
trivial.
simpl. rewrite IHxs. trivial.
Qed.

Proposition App_nil: forall X (xs: list X),
xs ++ nil = xs.

Proof. induction xs.
trivial.
simpl. rewrite IHxs. trivial.
Qed.

Fixpoint rev X (xs: list X) := match xs with
 | nil => nil
 | x::xr => rev X xr ++ ([x]: list X)
end.

Implicit Arguments rev [X].

Proposition Rev_app: forall X (xs ys: list X),
rev(xs++ys) = rev ys ++ rev xs.

Proof. intros. induction xs.
simpl. rewrite App_nil. trivial.
simpl. rewrite IHxs. rewrite Assoc. trivial.
Qed.

Proposition Rev_rev : forall X (xs: list X),
rev (rev xs) = xs.

Proof. induction xs.
trivial.
simpl. rewrite Rev_app. rewrite IHxs. trivial.
Qed.

Fixpoint foldl X Y (f: X->Y->Y) (a:Y) xs := match xs with
| nil => a
| x::xr => foldl X Y f (f x a) xr
end.

Implicit Arguments foldl [X Y].

Proposition length_foldl: forall X (xs: list X) n,
length xs + n = foldl (fun x => S) n xs.

Proof. (* Find it. Use the tactic ring_simplify. *)

Proposition rev_foldl: forall X (xs ys: list X),
rev xs ++ ys = foldl (@cons X) ys xs.

Proof. (* Find it *)

Proposition app_foldl: forall X (xs ys: list X),
xs++ys = foldl (@cons X) ys (foldl (@cons X) nil xs).

Proof. (* Find it.  Use the tactic ring_simplify. *)