Homework #7 Part 2 -- Exam Practice

#1 Easy Functions [15 points]

Define a function, pythag, that takes three natural numbers, call them a, b, and c, and that returns true if a^2 + b^2 = c^2 and that returns false otherwise.

-- Define your function here


-- The following test cases should then pass
#eval 
Error: unknown identifier 'pythag'
 3 4 5: ?m.2
 3 4 5  -- expect true
#eval 
Error: unknown identifier 'pythag'
 6 7 8: ?m.21
 6 7 8  -- expect false

#2 Recursive Functions

Define a function, sum_cubes, that takes any natural number, n, as an argument, and that retrns the sum of the cubes of the natural numbers from 1 up to n inclusive.

-- Define your function here




-- test case: sum_cubes 4 = 1 + 8 + 27 + 64 = 100
#eval 
Error: unknown identifier 'sum_cubes'
 4: ?m.40
 4   -- expect 100

#3 Product and Sum Types

Define two functions, called prod_ors_to_or_prods, and or_prods_to_prod_ors that shows that a product of sums be converted into a sum of products in a way that the result can then be converted back into the original product of sums.

As a concrete example, you might want to show that if you have an apple or an orange and you have a cup or a bowl, then you have an apple and a cup or an apple and a bowl or an orange and a cup or an orange and a bowl.

Hints: 1. Be sure you understand the reasoning before you try to define your functions. 2. Use four cases. 3. Use type-guided, top-down programming, assisted by the Lean prover to work out a solution for each case.

def 
prod_ors_to_or_prods: {α β γ δ : Type} → (α ⊕ β) × (γ ⊕ δ) → α × γ ⊕ α × δ ⊕ β × γ ⊕ β × δ
prod_ors_to_or_prods {
α: Type
α 
β: Type
β 
γ: Type
γ 
δ: Type
δ: 
Type: Type 1
Type} :
  (
α: Type
α ⊕ 
β: Type
β) × (
γ: Type
γ ⊕ 
δ: Type
δ) → 
α: Type
α × 
γ: Type
γ ⊕ 
α: Type
α × 
δ: Type
δ ⊕ 
β: Type
β × 
γ: Type
γ ⊕ 
β: Type
β × 
δ: Type
δ 
| _ => 
_: α × γ ⊕ α × δ ⊕ β × γ ⊕ β × δ
_

Error: redundant alternative


Error: redundant alternative


Error: redundant alternative


-- Write the second function here from scratch

#4 Propositional Logic Syntax and Semantics

Extend your Homework #7 solution to implement the propositional logic iff/equivalence (↔) operator. Note that Lean does not natively define the iff Boolean operator.

Using our syntax for propositional logic, and the variable names A, O, C, and B, respectively for the propositions I have an apple, I have an orange, I have a cup, and I have a bowl write a proposition that having an orange or an apple and a bowl or a cup is equivalent to having an apple and a bowl or an apple and a cup or an orange and a bowl or an orange and a cup.

Note: There's no need here to use our implementation of propositional logic. Just write the expression here using the notation we've defined.

#5 Propositional Logic Validity

At the end of your updated Homework #7 file, use our validity checking function to check your expression for validity, in the expectation that the checker will determine that the expression is in fact valid.