diff options
author | Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2013-12-20 18:17:35 +0100 |
---|---|---|
committer | Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2013-12-20 18:19:04 +0100 |
commit | de37a370a81c976aec56f25b2d7ddfa0dbad9145 (patch) | |
tree | 967ef366a55fc71350d85595aa0ca98f2e923fb1 /theories/Lists/List.v | |
parent | a665fd808b7fdaa11f84b35a87e0b8066cce1eda (diff) |
List: Bug 3039 weaker requirement for fold symmetric
Diffstat (limited to 'theories/Lists/List.v')
-rw-r--r-- | theories/Lists/List.v | 28 |
1 files changed, 8 insertions, 20 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 66c536a40..d5d58efc7 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -1054,29 +1054,17 @@ End Fold_Right_Recursor. Qed. Theorem fold_symmetric : - forall (A:Type) (f:A -> A -> A), - (forall x y z:A, f x (f y z) = f (f x y) z) -> - (forall x y:A, f x y = f y x) -> - forall (a0:A) (l:list A), fold_left f l a0 = fold_right f a0 l. + forall (A : Type) (f : A -> A -> A), + (forall x y z : A, f x (f y z) = f (f x y) z) -> + forall (a0 : A), (forall y : A, f a0 y = f y a0) -> + forall (l : list A), fold_left f l a0 = fold_right f a0 l. Proof. - destruct l as [| a l]. - reflexivity. - simpl. - rewrite <- H0. - generalize a0 a. - induction l as [| a3 l IHl]; simpl. - trivial. - intros. - rewrite H. - rewrite (H0 a2). - rewrite <- (H a1). - rewrite (H0 a1). - rewrite IHl. - reflexivity. + intros A f assoc a0 comma0 l. + induction l as [ | a1 l ]; [ simpl; reflexivity | ]. + simpl. rewrite <- IHl. clear IHl. revert a1. induction l; [ auto | ]. + simpl. intro. rewrite <- assoc. rewrite IHl. rewrite IHl. auto. Qed. - - (** [(list_power x y)] is [y^x], or the set of sequences of elts of [y] indexed by elts of [x], sorted in lexicographic order. *) |