fold_leftとfold_rightが同じになるとき

fold_leftとfold_rightの結果が同じになるときが気になったので少し調べてみた。

例えば文字列のリストを連結して一つの文字列を生成する次の例はfold_leftでもfold_rightでも同様に定義できて同じ関数になる。Coqで書くと次のような感じ。

Definition xs := "foo" :: "bar" :: "baz" :: nil.
Eval compute in (fold_left append xs "").
Eval compute in (fold_right append "" xs).

fold_leftとfold_rightの定義はそれぞれ次のとおり

Section Fold_Left_Recursor.
  Variables A B : Type.
  Variable f : A -> B -> A.

  Fixpoint fold_left (l:list B) (a0:A) : A :=
    match l with
      | nil => a0
      | cons b t => fold_left t (f a0 b)
    end.
End Fold_Left_Recursor.

Section Fold_Right_Recursor.
  Variables A B : Type.
  Variable f : B -> A -> A.
  Variable a0 : A.

  Fixpoint fold_right (l:list B) : A :=
    match l with
      | nil => a0
      | cons b t => f b (fold_right t)
    end.
End Fold_Right_Recursor.

(a0: A)と((##): A -> A -> A)に対して次の二つの条件が成り立てばfold_leftとfold_rightの結果が同じになることを示した。

• 任意の(x:A)に対して x ## a0 = a0 ## x
• (##)は結合的。つまり x ## (y ## z) = (x ## y) ## z.

Require Import List.

Section Fold_LR.

Variable A : Set.
Variable op : A -> A -> A.
Variable a0 : A.

Infix "##" := op (at level 60, right associativity).

Axiom assoc : forall (x y z:A), (x ## y) ## z = x ## (y ## z).
Axiom sym_a0 : forall x:A, a0 ## x = x ## a0.

Lemma aux : forall (bs: list A) (a b1: A),
  fold_right op a (b1::bs) = fold_left op (bs ++ (a::nil)) b1.
Proof.
 induction bs; intros.
  reflexivity.

  simpl.
  rewrite <- IHbs.
  simpl.
  rewrite assoc.
  reflexivity.
Qed.

Lemma fold_left_a0_r : forall (xs: list A) (a: A),
  fold_left op (xs ++ (a0::nil)) a = fold_left op xs a ## a0.
Proof.
 induction xs; intro.
  reflexivity.

  simpl.
  rewrite IHxs.
  reflexivity.
Qed.

Lemma fold_left_a0_l: forall (xs: list A) (a: A),
  fold_left op xs (a0 ## a) = a0 ## fold_left op xs a.
Proof.
 induction xs; intros.
  reflexivity.

  simpl.
  rewrite <- IHxs.
  rewrite assoc.
  reflexivity.
Qed.

Theorem fold_lr : forall (xs: list A),
  fold_left op xs a0 = fold_right op a0 xs.
Proof.
 destruct xs.
  reflexivity.

  rewrite aux.
  simpl.
  rewrite fold_left_a0_l.
  rewrite fold_left_a0_r.
  rewrite sym_a0.
  reflexivity.
Qed.

End Fold_LR.