Homework 6

The established rules apply. Do this work on your own.

This homework will test and strengthen your understanding of inductive data types, including Nat and List α, and the use of recursive functions to process and construct values of such types.

The second part will test and develop your knowledge and understanding of formal languages, and propositional logic, (PL) in particular, including the syntax and semantics of PL, and translations between formal statements in PL and corresponding concrete English-language examples.

Part 1: Inductive Types and Recursive Functions

#1: Iterated Function Application

Here are two functions, each of which takes a function, f, as an argument, and an argument, a, to that function, and returns the result of applying f to a one or more times. The first function just applies f to a once. The second function applies f to a twice. Be sure you fully understand these definitions before proceeding.

def 
apply: {α : Sort u_1} → {a : α} → (α → α) → α → α
apply {
a: α
a
Warning: unused variable `a` [linter.unusedVariables] : 
α: Sort u_1
α} : (
α: Sort u_1
α → 
α: Sort u_1
α) → 
α: Sort u_1
α → 
α: Sort u_1
α 
| 
f: α → α
f, 
a: α
a => 
f: α → α
f 
a: α
a

def 
apply_twice: {α : Sort u_1} → {a : α} → (α → α) → α → α
apply_twice {
a: α
a
Warning: unused variable `a` [linter.unusedVariables] : 
α: Sort u_1
α} : (
α: Sort u_1
α → 
α: Sort u_1
α) → 
α: Sort u_1
α → 
α: Sort u_1
α 
| 
f: α → α
f, 
a: α
a => 
f: α → α
f (
f: α → α
f 
a: α
a)

Your job now is to define a function, apply_n, that takes a function, f, a natural number, n, and an argument, a, and that returns the result of applying f to a n times. Define the result of applying f to a zero times as just a. Hint: recursion on n. That is, you will have two cases: where n is 0; and where n is greater than 0, and can thus be written as (1 + n') for some smaller natural number, n'.

-- Answer here

def 
apply_n: {α : Type} → (α → α) → α → Nat → α
apply_n {
α: Type
α : 
Type: Type 1
Type} : (
α: Type
α → 
α: Type
α) → 
α: Type
α → 
Nat: Type
Nat → 
α: Type
α  
| 
f: α → α
f
Warning: unused variable `f` [linter.unusedVariables], 
a: α
a, 
0: Nat
0 => 
a: α
a
| 
f: α → α
f, 
a: α
a, (
n': Nat
n' + 1) => 
f: α → α
f (
apply_n: {α : Type} → (α → α) → α → Nat → α
apply_n 
f: α → α
f 
a: α
a 
n': Nat
n')

-- Test cases: confirm that expectations are correct

-- apply Nat.succ to zero four times
#eval
4
 
apply_n: {α : Type} → (α → α) → α → Nat → α
apply_n 
Nat.succ: Nat → Nat
Nat.succ 
0: Nat
0 
4: Nat
4        -- expect 4

-- apply "double" to 2 four times
#eval
32
 
apply_n: {α : Type} → (α → α) → α → Nat → α
apply_n (λ 
n: Nat
n => 
2: Nat
2*
n: Nat
n) 
2: Nat
2 
4: Nat
4    -- expect 32

-- apply "square" to 2 four times
#eval
65536
 
apply_n: {α : Type} → (α → α) → α → Nat → α
apply_n (λ 
n: Nat
n => 
n: Nat
n^
2: Nat
2) 
2: Nat
2 
4: Nat
4    -- expect 65536

A Short Introduction to Lists

The polymorphic data type, List α, is used to represent lists of values of any type, α. The List type builder provides two constructors: one to create and empty list of α values, and one to construct a new non-empty list from a new element (head, of type α) and a one smaller list (tail, of type List α). Here's how the List type builder is defined (simplied just a tad).

namespace cs2120

inductive 
List: Type → Type
List (
α: Type
α : 
Type: Type 1
Type): 
Type: Type 1
Type
| 
nil: {α : Type} → List α
nil : 
List: Type → Type
List 
α: Type
α
| 
cons: {α : Type} → α → List α → List α
cons (
h: α
h : 
α: Type
α) (
t: List α
t : 
List: Type → Type
List 
α: Type
α) : 
List: Type → Type
List 
α: Type
α

end cs2120

Lean defines three useful notations for creating and destructuring lists.

• [] means List.nil
• h::t means cons h t
• [1, 2, 3] means the list, 1::[2,3]
  • which means 1::2::[3]
  • which means 1::2::3::[]
  • which means cons 1 (cons 2 (cons 3 nil))

#check
[] : List Nat (
[]: List Nat
[] : 
List: Type → Type
List 
Nat: Type
Nat)
#check
[1, 2, 3] : List Nat 
1: Nat
1::[
2: Nat
2,
3: Nat
3]
#check
[1, 2, 3] : List Nat [
1: Nat
1,
2: Nat
2,
3: Nat
3]

You can use these notations when pattern matching to analyze arguments. Here we show how this work by defining a function that takes a list and returns either (using a sum type) unit to represent the case where there is no first element, or the value at the head of the list.

def 
first_elt: List Nat → Unit ⊕ Nat
first_elt : 
List: Type → Type
List 
Nat: Type
Nat → 
Unit: Type
Unit ⊕ 
Nat: Type
Nat
| [] => 
Sum.inl: {α β : Type} → α → α ⊕ β
Sum.inl 
Unit.unit: Unit
Unit.unit
| 
h: Nat
h::_ => 
Sum.inr: {α β : Type} → β → α ⊕ β
Sum.inr 
h: Nat
h

#reduce
Sum.inl PUnit.unit 
first_elt: List Nat → Unit ⊕ Nat
first_elt 
[]: List Nat
[]    -- expect Sum.inl unit
#reduce
Sum.inr 1 
first_elt: List Nat → Unit ⊕ Nat
first_elt [
1: Nat
1,
2: Nat
2] -- expect 1 (left)

#2: List length function

Lists are defined inductively in Lean. A list of values of some type α is either the empty list of α values, denoted [], or an α value followed by a shorter list of α values, denoted h::t, where h (the head of the list) is a single value of type α, and t is a shorter list of α values. The base case is of course the empty list. Define a function called len that takes a list of values of any type, α, and that returns the length of the list.

def 
len: {α : Type} → List α → Nat
len {
α: Type
α : 
Type: Type 1
Type} : 
List: Type → Type
List 
α: Type
α → 
Nat: Type
Nat
| [] => 
0: Nat
0
| 
h: α
h
Warning: unused variable `h` [linter.unusedVariables]::
t: List α
t => 
1: Nat
1 + 
len: {α : Type} → List α → Nat
len 
t: List α
t

#eval
0
 @
len: {α : Type} → List α → Nat
len 
Nat: Type
Nat 
[]: List Nat
[]                   -- expect 0
#eval
3
 
len: {α : Type} → List α → Nat
len [
0: Nat
0,
1: Nat
1,
2: Nat
2]                   -- expect 3
#eval
3
 
len: {α : Type} → List α → Nat
len [
"I": String
"I", 
"Love": String
"Love", 
"Logic!": String
"Logic!"]   -- expect 3

#3: Reduce a List of Bool to a Bool

Define a function that takes a list of Boolean values and that "reduces" it to a single Boolean value, which it returns, where the return value is true if all elements are true and otherwise is false. Call your function reduce_and.

Hint: the answer is the result of applying and to two arguments: (1) the first element, and (2) the result of recursively reducing the rest of the list. You will have to figure out what the return value for the base case of an empty list needs to be for your function to work in all cases.

def 
reduce_and: List Bool → Bool
reduce_and : 
List: Type → Type
List 
Bool: Type
Bool → 
Bool: Type
Bool
| [] => 
true: Bool
true
| 
h: Bool
h::
t: List Bool
t => 
and: Bool → Bool → Bool
and 
h: Bool
h (
reduce_and: List Bool → Bool
reduce_and 
t: List Bool
t)

-- Test cases

#eval
true
 
reduce_and: List Bool → Bool
reduce_and [
true: Bool
true]           -- expect true
#eval
false
 
reduce_and: List Bool → Bool
reduce_and [
false: Bool
false]          -- expect false
#eval
true
 
reduce_and: List Bool → Bool
reduce_and [
true: Bool
true, 
true: Bool
true]     -- expect true
#eval
false
 
reduce_and: List Bool → Bool
reduce_and [
false: Bool
false, 
true: Bool
true]    -- expect false

#4 Negate a List of Booleans

Define a function, call it (map_not) that takes a list of Boolean values and returns a list of Boolean values, where each entry in the returned list is the negation of the corresonding element in the given list of Booleans. For example, map_not [true, false] should return [false, true].

def 
map_not: List Bool → List Bool
map_not : 
List: Type → Type
List 
Bool: Type
Bool → 
List: Type → Type
List 
Bool: Type
Bool 
| [] => 
[]: List Bool
[]
| 
h: Bool
h::
t: List Bool
t => 
not: Bool → Bool
not 
h: Bool
h :: 
map_not: List Bool → List Bool
map_not 
t: List Bool
t   -- hint: use :: to construct answer

-- test cases
#eval
[]
 
map_not: List Bool → List Bool
map_not 
[]: List Bool
[]              -- exect []
#eval
[false, true]
 
map_not: List Bool → List Bool
map_not [
true: Bool
true, 
false: Bool
false]   -- expect [false, true]

#5 List the First n Natural Numbers

Define a function called countdown that takes a natural number argument, n, and that returns a list of all the natural numbers from n to 0, inclusive.

-- Your answer here
def 
countdown: Nat → List Nat
countdown : 
Nat: Type
Nat → 
List: Type → Type
List 
Nat: Type
Nat
| 
0: Nat
0 => [
0: Nat
0]
| 
n': Nat
n' + 1 => (
n': Nat
n' + 
1: Nat
1)::
countdown: Nat → List Nat
countdown 
n': Nat
n'


-- test cases
#eval
[0]
 
countdown: Nat → List Nat
countdown 
0: Nat
0            -- expect [0]
#eval
[5, 4, 3, 2, 1, 0]
 
countdown: Nat → List Nat
countdown 
5: Nat
5            -- expect [5,4,3,2,1,0]

#6: List concatenation

Suppose Lean didn't provide the List.append function, denoted ++. Write your own list append function. Call it concat. For any type α, it takes two arguments of type List α and returns a result of type List α, the result of appending the second list to the first. Hint: do case analysis on the first argument.

-- Here

def 
concat: {α : Type} → List α → List α → List α
concat {
α: Type
α : 
Type: Type 1
Type} : 
List: Type → Type
List 
α: Type
α → 
List: Type → Type
List 
α: Type
α → 
List: Type → Type
List 
α: Type
α 
| [], 
m: List α
m => 
m: List α
m
| 
h: α
h::
t: List α
t, 
m: List α
m => 
h: α
h::
concat: {α : Type} → List α → List α → List α
concat 
t: List α
t 
m: List α
m

-- Test cases

#eval
[1, 2, 3]
 
concat: {α : Type} → List α → List α → List α
concat [
1: Nat
1,
2: Nat
2,
3: Nat
3] 
[]: List Nat
[]   -- expect [1,2,3]
#eval
[1, 2, 3]
 
concat: {α : Type} → List α → List α → List α
concat 
[]: List Nat
[] [
1: Nat
1,
2: Nat
2,
3: Nat
3]   -- expect [1,2,3]
#eval
[1, 2, 3, 4]
 
concat: {α : Type} → List α → List α → List α
concat [
1: Nat
1,
2: Nat
2] [
3: Nat
3,
4: Nat
4]  -- expect [1,2,3,4]

#7: Lift Element to List

Write a function, pure', that takes a value, a, of any type α, and that returns a value of type List α containing just that one element.

-- Here
def 
pure': String → List String
pure' : 
String: Type
String → 
List: Type → Type
List 
String: Type
String 
| 
s: String
s => [
s: String
s]

#eval
["Hi"]
 
pure': String → List String
pure' 
"Hi": String
"Hi"       -- expect ["Hi"]

Challenge: List Reverse

Define a function, list_rev, that takes a list of values of any type and that returns it in reverse order. Hint: you can't use :: with a single value on the right; it needs a list on the right. Instead, consider using concat.

-- Answer here:

def 
rev: {α : Type} → List α → List α
rev {
α: Type
α : 
Type: Type 1
Type}: 
List: Type → Type
List 
α: Type
α → 
List: Type → Type
List 
α: Type
α
| [] => 
[]: List α
[]
| 
h: α
h::
t: List α
t => 
t: List α
t++[
h: α
h]

End of Exam Practice Part 1