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.

# Homework 01

The homework corresponding to exercise sheet 01.

### More Finger Exercise with Lists

```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›.›
```

## Resources

### Definitions File

```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```

### Template File

```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```

### Check File

```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```

Terms and Conditions