Skip to content

Instantly share code, notes, and snippets.

@yoshihiro503

yoshihiro503/fold_rightに関する未解決補題その2.v

Created July 29, 2017 12:14
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 3 You must be signed in to fork a gist
  • Save yoshihiro503/d07c97df937c90eb6fd263e73ae2b5d8 to your computer and use it in GitHub Desktop.
Save yoshihiro503/d07c97df937c90eb6fd263e73ae2b5d8 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
fold_rightに関する未解決補題その2.v
Require Import Program.
Open Scope list_scope.
Lemma fold_right_rev : forall (A: Type) (f: A -> A -> A) xs x0,
(forall x y z, f x (f y z) = f (f x y) z) ->
(forall x y, f x y = f y x) ->
List.fold_right f x0 xs = List.fold_right f x0 (List.rev xs).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment