I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.
text ‹ Define a function ‹fold_right› that iteratively applies a function to the elements of a list.
More precisely ‹fold_right f [x⇩1, x⇩2, …, x⇩n] a› should compute ‹f x⇩1 (f x⇩2 (… (f x⇩n a)))›.
The following evaluate to true, for instance: › value "fold_right (+) [1,2,3] (4 :: nat) = 10" value "fold_right (#) [a,b,c] [] = [a,b,c]" text ‹ Prove that ‹fold_right› applied to the result of ‹map› can be contracted into a single ‹fold_right›: › lemma "fold_right f (map g xs) a = fold_right (f o g) xs a" text ‹Here ‹o› is the regular composition operator on functions, i.e. ‹f o g = (λx. f (g x))›.› text ‹Prove the following lemma on ‹fold_right› and ‹append›:› lemma "fold_right f (xs @ ys) a = fold_right f xs (fold_right f ys a)" text ‹ For the remainder of the homework we will consider the special case where ‹f› is the addition operation on natural numbers.
Prove that sums over natural numbers can be ``pulled apart'': › lemma "fold_right (+) (xs @ ys) (0 :: nat) = fold_right (+) xs 0 + fold_right (+) ys 0" text ‹The notation ‹(+)› is just a shorthand for ‹λx y. x + y›.› text ‹ Finally prove that calculating the sum from the right and from the left yields the same result: › lemma "fold_right (+) (reverse xs) (x :: nat) = fold_right (+) xs x" text ‹Hint: You may need a lemma about ‹snoc› and ‹fold_right›.›
theory Defs imports Main begin text \<open>Definitions and lemmas from the tutorial\<close> fun snoc :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list" where "snoc [] x = [x]" | "snoc (y # ys) x = y # (snoc ys x)" fun reverse :: "'a list \<Rightarrow> 'a list" where "reverse [] = []" | "reverse (x # xs) = snoc (reverse xs) x" lemma reverse_snoc: "reverse (snoc xs y) = y # reverse xs" by (induct xs) auto theorem reverse_reverse: "reverse (reverse xs) = xs" by (induct xs) (auto simp add: reverse_snoc) end
theory Submission
imports Defs
begin
text \<open>Define \<open>fold_right\<close> here:\<close>
fun fold_right :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
"fold_right _ _ _ = undefined"
text \<open>Test cases for \<open>fold_right\<close>\<close>
value "fold_right (+) [1,2,3] (4 :: nat) = 10"
value "fold_right (#) [a,b,c] [] = [a,b,c]"
text \<open>
Prove that \<open>fold_right\<close> applied to the result of \<open>map\<close>
can be contracted into a single \<open>fold_right\<close>:
\<close>
lemma fold_right_map:
"fold_right f (map g xs) a = fold_right (f o g) xs a"
sorry
text \<open>Prove the following lemma on \<open>fold_right\<close> and \<open>append\<close>:\<close>
lemma fold_right_append:
"fold_right f (xs @ ys) a = fold_right f xs (fold_right f ys a)"
sorry
text \<open>
For the remainder of the homework we will consider the special case where \<open>f\<close>
is the addition operation on natural numbers.
Prove that sums over natural numbers can be ``pulled apart'':
\<close>
lemma fold_right_sum_append:
"fold_right (+) (xs @ ys) (0 :: nat) = fold_right (+) xs 0 + fold_right (+) ys 0"
sorry
text \<open>
Finally prove that calculating the sum from the right and from the left yields the same result:
\<close>
lemma fold_right_sum_reverse:
"fold_right (+) (reverse xs) (x :: nat) = fold_right (+) xs x"
sorry
end
theory Check imports Submission begin text \<open>We make sure that your definition of \<open>fold_right\<close> passes the test cases:\<close> lemma "fold_right (+) [1,2,3] (4 :: nat) = 10" by simp lemma "fold_right (#) [a,b,c] [] = [a,b,c]" by simp text \<open>And we check that you proved the right theorems:\<close> lemma fold_right_map: "fold_right f (map g xs) a = fold_right (f o g) xs a" by (rule Submission.fold_right_map) lemma fold_right_append: "fold_right f (xs @ ys) a = fold_right f xs (fold_right f ys a)" by (rule Submission.fold_right_append) lemma fold_right_sum_append: "fold_right (+) (xs @ ys) (0 :: nat) = fold_right (+) xs 0 + fold_right (+) ys 0" by (rule Submission.fold_right_sum_append) lemma fold_right_sum_reverse: "fold_right (+) (reverse xs) (x :: nat) = fold_right (+) xs x" by (rule Submission.fold_right_sum_reverse) end