Skip to content

Instantly share code, notes, and snippets.

@erutuf

erutuf/fold_rightに関する未解決問題.v

Forked from yoshihiro503/fold_rightに関する未解決問題.v
Last active July 29, 2017 12:23
Show Gist options
  • Save erutuf/db75813d1b0d32499329bfb9f4217c81 to your computer and use it in GitHub Desktop.
Save erutuf/db75813d1b0d32499329bfb9f4217c81 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
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])).
rewrite <- (rev_involutive xs) at 2.
do 2 rewrite fold_left_rev_right.
rewrite rev_unit...
reflexivity.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment