erutuf

## fold_rightに関する未解決補題その2.v
Require Import Program List.
Open Scope list_scope.

Lemma fold_right_ext : forall (A : Type)(f g : A -> A -> A) xs x0,
  (forall x y, f x y = g x y) ->
  fold_right f x0 xs = fold_right g x0 xs.
Proof with simpl in *.
  intros.
  induction xs; [auto|]...
  rewrite H.

## fold_rightに関する未解決問題.v
Require Import Program.
Open Scope list_scope.

Require Import List.

Lemma fold_right_tail : forall (A B: Type) (f: A -> B -> B) xs x b0,
List.fold_right f b0 (xs ++ [x]) = List.fold_right f (f x b0) xs.
Proof with simpl in *.
  intros.
  rewrite <- (rev_involutive (xs ++ [x])).
	Require Import Program List.
	Open Scope list_scope.

	Lemma fold_right_ext : forall (A : Type)(f g : A -> A -> A) xs x0,
	(forall x y, f x y = g x y) ->
	fold_right f x0 xs = fold_right g x0 xs.
	Proof with simpl in *.
	intros.
	induction xs; [auto\|]...
	rewrite H.
	Require Import Program.
	Open Scope list_scope.

	Require Import List.

	Lemma fold_right_tail : forall (A B: Type) (f: A -> B -> B) xs x b0,
	List.fold_right f b0 (xs ++ [x]) = List.fold_right f (f x b0) xs.
	Proof with simpl in *.
	intros.
	rewrite <- (rev_involutive (xs ++ [x])).