fold_symmetric2.v

Require Import List.

Variable A B : Type.

Theorem fold_symmetric2 : forall (f : A -> B -> A) (g : B -> A -> A),
  (forall x y, f x y = g y x) ->
  forall x l, fold_left f l x = fold_right g x (rev l).
Proof with simpl in *; intuition.
intros f g H x l. revert x.
induction l...
rewrite IHl.
rewrite fold_right_app...
rewrite H...
Qed.

(*
fold_left と fold_right の変換をより一般的な形で
*)