Homework 5: Inhabitedness and Induction

The PURPOSE of this homework is to greatly strengthen your understanding of reasoning with sum and product types along with properties of being inhabited or not.

READ THIS: The collaboration rule for this homework is that you may not collaborate. You can ask friends and colleagues to help you understand the class material, but you may not discuss any of these homework problems with anyone other than one of the instructors or TAs.

Finally, what you're seeing here is the FIRST set of questions on this homework, giving you an opportunity to deepen your understanding of the Empty type and its uses.

PART 1: Inhabitedness and Logical Negation

Of particular importance in these questions is the idea that having a function value (implementation) of type α → Empty proves that α is uninhabited, in that if there were a value (a : α) then you'd be able to derive a value of type Empty, and that simply can't be done, so there must be no such (a : α). That's the great idea that we reached at the end of lecture_09.

More concretely every time you see function type that looks like (α → Empty) in what follows, you can read it as saying there is no value of type α. Second, if youwant to return a result of type (α → Empty), to showing that there can be no α value, then you need to return a function; and you will often want to do so by writing the return value as a lambda expression.

#1 Not Jam or Not Cheese Implies Not Jam and Cheese

Suppose you don't have cheese OR you don't have jam. Then it must be that you don't have (cheese AND jam). Before you go on, think about why this has to be true. Here's a proof of it in the form of a function. The function takes jam and cheese implicitly as types. It takes a value that either indicates there is no jam, or a value that indicates that there's no cheese, and you are to construct a value that shows that there can be no jam and cheese. It works by breaking the first argument into two cases: either a proof that there is no jam (there are no values of this type), or a proof that there is no cheese, and shows in either case that there can be no jam AND cheese.

New Addition: no (α : Type) := α → Empty

We can make the logical intent of our types and computations clearer by introducing a shorthand, no α for the type α → Empty. Then in each place where a type like *α → Empty appears in this homework, replace it with no α. Use the right local names in each instance, of course.

def 
no: Type → Type
no (
α: Type
α : 
Type: Type 1
Type) := 
α: Type
α → 
Empty: Type
Empty

We've now replaced each α → Empty with no α. We suggest that you go ahead and use no wherever doing so makes the logical meaning clearer.

def 
not_either_not_both: {jam cheese : Type} → no jam ⊕ no cheese → no (jam × cheese)
not_either_not_both { 
jam: Type
jam 
cheese: Type
cheese } :
  ((
no: Type → Type
no 
jam: Type
jam) ⊕ (
no: Type → Type
no 
cheese: Type
cheese)) → 
  (
no: Type → Type
no (
jam: Type
jam × 
cheese: Type
cheese)) 
| 
Sum.inl: {α : Type ?u.38} → {β : Type ?u.37} → α → α ⊕ β
Sum.inl 
nojam: no jam
nojam => (fun 
_: jam × cheese
_ => 
_: Empty
_
Error: don't know how to synthesize placeholder
context:
jam cheese : Type
nojam : no jam
x✝ : jam × cheese
⊢ Empty)
| 
Sum.inr: {α : Type ?u.65} → {β : Type ?u.64} → β → α ⊕ β
Sum.inr _ => 
_: no (jam × cheese)
_
Error: don't know how to synthesize placeholder
context:
jam cheese : Type
val✝ : no cheese
⊢ no (jam × cheese)

#2: Not One or Not the Other Implies Not Both

Now prove this principle in general by defining a function, demorgan1, of the following type. It's will be the same function, just with the names α and β for the types, rather than the more suggestive but specific names, jam and cheese.

{α β : Type} → (α → Empty ⊕ β → Empty) → (α × β → Empty).

def 
demorgan1: {α β : Type} → (α → Empty) ⊕ (β → Empty) → α × β → Empty
demorgan1  {
α: Type
α 
β: Type
β : 
Type: Type 1
Type} : ((
α: Type
α → 
Empty: Type
Empty) ⊕ (
β: Type
β → 
Empty: Type
Empty)) → (
α: Type
α × 
β: Type
β → 
Empty: Type
Empty)  
| (
Sum.inl: {α : Type ?u.260} → {β : Type ?u.259} → α → α ⊕ β
Sum.inl 
noa: α → Empty
noa) => 
_: α × β → Empty
_
Error: don't know how to synthesize placeholder
context:
α β : Type
noa : α → Empty
⊢ α × β → Empty
| (
Sum.inr: {α : Type ?u.292} → {β : Type ?u.291} → β → α ⊕ β
Sum.inr 
nob: β → Empty
nob) => 
_: α × β → Empty
_
Error: don't know how to synthesize placeholder
context:
α β : Type
nob : β → Empty
⊢ α × β → Empty

#3: Not Either Implies Not One And Not The Other

Now suppose that you don't have either jam and cheese. Then you don't have jam and you don't have cheese. More generally, if you don't have an α OR a β, then you can conclude that you don't have an α Here's a function type that asserts this fact in a general way. Show it's true in general by implementing it. An implementation will show that given any types, α and β,

def 
demorgan2: {α β : Type} → (α ⊕ β → Empty) → (α → Empty) × (β → Empty)
demorgan2 {
α: Type
α 
β: Type
β : 
Type: Type 1
Type} : (
α: Type
α ⊕ 
β: Type
β → 
Empty: Type
Empty) → ((
α: Type
α → 
Empty: Type
Empty) × (
β: Type
β → 
Empty: Type
Empty))
| 
noaorb: α ⊕ β → Empty
noaorb => 
_: (α → Empty) × (β → Empty)
_
Error: don't know how to synthesize placeholder
context:
α β : Type
x✝ : α ⊕ β → Empty
noaorb : α ⊕ β → Empty := x✝
⊢ (α → Empty) × (β → Empty)

#4: Not One And Not The Other Implies Not One Or The Other

Suppose you know that there is no α AND there is no β. Then you can deduce that there can be no (α ⊕ β) object. Again we give you the function type that expresses this idea, and you must show it's true by implementing the function. Hint: You might want to use an explicit match expression in writing your solution.

def 
demorgan3: {α β : Type} → (α → Empty) × (β → Empty) → α ⊕ β → Empty
demorgan3 {
α: Type
α 
β: Type
β : 
Type: Type 1
Type} : ((
α: Type
α → 
Empty: Type
Empty) × (
β: Type
β → 
Empty: Type
Empty)) → ((
α: Type
α ⊕ 
β: Type
β) → 
Empty: Type
Empty)  
| _ => 
_: α ⊕ β → Empty
_
Error: don't know how to synthesize placeholder
context:
α β : Type
x✝ : (α → Empty) × (β → Empty)
⊢ α ⊕ β → Empty

PART 2

The following problems aim to strengthen your understanding of inductive type definitions and recusrive functions.

-- Here are some named Nat values, for testing
def n0 := Nat.zero
def n1 := Nat.succ n0
def n2 := Nat.succ n1
def n3 := Nat.succ n2
def n4 := Nat.succ n3
def n5 := Nat.succ n4

#1. Pattern Matching Enables Destructuring

#1: Defne a function, pred: Nat → Nat, that takes an any Nat, n, and, if n is zero, returns zero, otherwise analyze n as (Nat.succ n') and return n'. Yes this question should be easy. Be sure you understand destructuring and pattern matching.

-- Here



-- Test cases
#reduce
sorryAx ?m.776 true 
pred: ?m.776
pred
Error: unknown identifier 'pred'
 3: ?m.776
 3    -- expect 2
#reduce
sorryAx ?m.780 true 
pred: ?m.780
pred
Error: unknown identifier 'pred'
 0: ?m.780
 0    -- expect 0

#2. Big Doll from Smaller One n Times

Write a function, mk_doll : Nat → Doll, that takes any natural number argument, n, and that returns a doll n shells deep. The verify using #reduce that (mk_doll 3) returns the same doll as d3.

-- Answer here



-- test cases
#check 
mk_doll: ?m.784
mk_doll
Error: unknown identifier 'mk_doll'
 3: ?m.784
 3
#reduce
sorryAx ?m.786 true 
mk_doll: ?m.786
mk_doll
Error: unknown identifier 'mk_doll'
 3: ?m.786
 3

#3. A Boolean Nat Equality Predicate

Write a function, nat_eq : Nat → Nat → Bool, that takes any two natural numbers and that returns Boolean true if they're equal, and false otherwise. Finish off the definition by filling the remaining hole (_).

def 
nat_eq: Nat → Nat → Bool
nat_eq : 
Nat: Type
Nat → 
Nat: Type
Nat → 
Bool: Type
Bool
| 
0: Nat
0, 
0: Nat
0 => 
true: Bool
true
| 
0: Nat
0, 
n': Nat
n' + 1 => 
false: Bool
false
| 
n': Nat
n' + 1, 
0: Nat
0 => 
false: Bool
false
| (
n': Nat
n' + 1), (
m': Nat
m' + 1) => 
_: Bool
_
Error: don't know how to synthesize placeholder
context:
n' m' : Nat
⊢ Bool

-- a few tests
#eval 
nat_eq: Nat → Nat → Bool
nat_eq 
0: Nat
0 
0: Nat
0
Error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
#eval 
nat_eq: Nat → Nat → Bool
nat_eq 
0: Nat
0 
1: Nat
1
Error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
#eval 
nat_eq: Nat → Nat → Bool
nat_eq 
1: Nat
1 
0: Nat
0
Error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
#eval 
nat_eq: Nat → Nat → Bool
nat_eq 
1: Nat
1 
1: Nat
1
Error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
#eval 
nat_eq: Nat → Nat → Bool
nat_eq 
2: Nat
2 
0: Nat
0
Error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
#eval 
nat_eq: Nat → Nat → Bool
nat_eq 
2: Nat
2 
1: Nat
1
Error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
#eval 
nat_eq: Nat → Nat → Bool
nat_eq 
2: Nat
2 
2: Nat
2
Error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors

#4. Natural Number Less Than Or Equal

Write a function, nat_le : Nat → Nat → Bool, that takes any two natural numbers and that returns Boolean true if the first value is less than or equal to the second, and false otherwise. Hint: what are the relevant cases? Match to destructure them then return the right result in each case.

-- Here

#5. Nat Number Addition

Complete this function definition to implement a natural number addition function.

def add : Nat → Nat → Nat
| m, 0 => m
| m, (Nat.succ n') => 
_: Nat
_
Error: don't know how to synthesize placeholder
context:
m n' : Nat
⊢ Nat   -- hint: recursion


-- Some test cases
#reduce
sorryAx (Nat → Nat → Nat) true 0 0 
add: Nat → Nat → Nat
add 
0: Nat
0 
0: Nat
0   -- expect 0
#reduce
sorryAx (Nat → Nat → Nat) true 5 0 
add: Nat → Nat → Nat
add 
5: Nat
5 
0: Nat
0   -- expect 5
#reduce
sorryAx (Nat → Nat → Nat) true 0 5 
add: Nat → Nat → Nat
add 
0: Nat
0 
5: Nat
5   -- expect 5
#reduce
sorryAx (Nat → Nat → Nat) true 5 4 
add: Nat → Nat → Nat
add 
5: Nat
5 
4: Nat
4   -- expect 9
#reduce
sorryAx (Nat → Nat → Nat) true 4 5 
add: Nat → Nat → Nat
add 
4: Nat
4 
5: Nat
5   -- expect 9
#reduce
sorryAx (Nat → Nat → Nat) true 5 5 
add: Nat → Nat → Nat
add 
5: Nat
5 
5: Nat
5   -- expect 10

#6. Natural Number Multiplication

Complete this function definition to implement a natural number multiplication function. You can't use Lean's Nat multiplication function. Your implementation should use productively the add function you just definied. Wite a few test cases to show that it appears to be working.

def 
mul: Nat → Nat → Nat
mul : 
Nat: Type
Nat → 
Nat: Type
Nat → 
Nat: Type
Nat
| 
m: Nat
m, 
0: Nat
0 => 
0: Nat
0
| 
m: Nat
m, (
Nat.succ: Nat → Nat
Nat.succ 
n': Nat
n') => 
add: Nat → Nat → Nat
add (
_: Nat
_
Error: don't know how to synthesize placeholder
context:
m n' : Nat
⊢ Nat) (
_: Nat
_
Error: don't know how to synthesize placeholder
context:
m n' : Nat
⊢ Nat)

Sum Binary Nat Function Over Range 0 to n

Define a function, sum_f, that takes a function, f : Nat → Nat and a natural number n, and that returns the sum of all of the values of (f k) for k ranging from 0 to n.

Compute expected results by hand for a few test cases and write the tests using #reduce. For example, you might use the squaring function as an argument, with a nat, n, to obtain the sum of the squares of all the numbers from 0 to and including n.

def 
sum_f: (Nat → Nat) → Nat → Nat
sum_f : (
Nat: Type
Nat → 
Nat: Type
Nat) → 
Nat: Type
Nat → 
Nat: Type
Nat 
| 
f: Nat → Nat
f, 
0: Nat
0 => 
_: Nat
_
Error: don't know how to synthesize placeholder
context:
f : Nat → Nat
⊢ Nat
| 
f: Nat → Nat
f, 
n': Nat
n' + 1 => 
_: Nat
_
Error: don't know how to synthesize placeholder
context:
f : Nat → Nat
n' : Nat
⊢ Nat