257 lines
7 KiB
Text
257 lines
7 KiB
Text
|
|
|
|
** Michael Zhang **
|
|
** **
|
|
** zhan4854 **
|
|
|
|
|
|
|
|
~.* Question 1. *.~
|
|
|
|
let rec power n x =
|
|
match n with
|
|
| 0 -> 1.0
|
|
| _ -> x *. power (n-1) x
|
|
|
|
Prove that:
|
|
power n x = x ^ n
|
|
|
|
--- Properties ---
|
|
|
|
[1] x ^ (n + 1) = x * x ^ n, because that's how math works
|
|
|
|
--- Base Case: n = 0 ---
|
|
|
|
P(0, x) = 1.0, by the definition of power
|
|
x ^ 0 = 1.0, because that's how math works
|
|
|
|
1.0 == 1.0, so P(n, x) = x ^ n for n = 0
|
|
|
|
--- Inductive Case: n > 1 ---
|
|
|
|
Given: P(n, x) = x ^ n
|
|
Show: P(n + 1, x) = x ^ (n + 1)
|
|
|
|
P(n, x) = x ^ n, given
|
|
x * P(n, x) = x * x ^ n, multiplying both sides by x
|
|
x * P(n, x) = x ^ (n + 1), by property [1]
|
|
P(n + 1, x) = x ^ (n + 1), by the definition of power
|
|
|
|
∴ power n x = x ^ n, for all natural numbers n
|
|
|
|
|
|
|
|
~.* Question 2 *.~
|
|
|
|
type nat = Zero | Succ of nat
|
|
|
|
let toInt = function
|
|
| Zero -> 0
|
|
| Succ n -> toInt n + 1
|
|
|
|
let rec power n x =
|
|
match n with
|
|
| Zero -> 1.0
|
|
| Succ n' -> x *. power n' x
|
|
|
|
Based on the usage of nat in toInt and power, we can reliably
|
|
infer that a property of nat will also apply to Succ of nat,
|
|
which essentially equals nat + 1.
|
|
|
|
Prove that:
|
|
power n x = x ^ toInt(n), for all nat n
|
|
|
|
--- Properties ---
|
|
|
|
[1] x ^ (n + 1) = x * x ^ n, because that's how math works
|
|
|
|
--- Base Case: n = Zero ---
|
|
|
|
P(Zero, x) = 1.0, by the definition of power
|
|
x ^ toInt(Zero) = x ^ 0, by the definition of toInt
|
|
x ^ 0 = 1.0, because that's how math works
|
|
|
|
1.0 == 1.0, so P(n, x) = x ^ toInt(n) for n = Zero
|
|
|
|
--- Inductive Case: n = Succ of n' ---
|
|
|
|
Given: P(n, x) = x ^ toInt(n)
|
|
Show: P(Succ n, x) = x ^ toInt(Succ n)
|
|
|
|
P(n, x) = x ^ toInt(n), given
|
|
x * P(n, x) = x * x ^ toInt(n), multiplying both sides by x
|
|
x * P(n, x) = x ^ (toInt(n) + 1), by property [1]
|
|
x * P(n, x) = x ^ toInt(Succ n), by the definition of toInt
|
|
P(Succ n, x) = x ^ toInt(Succ n), by the definition of power
|
|
|
|
∴ power n x = x ^ toInt(n)
|
|
|
|
|
|
|
|
~.* Question 3 *.~
|
|
|
|
let rec length = function
|
|
| [] -> 0
|
|
| x:xs -> 1 + length xs
|
|
|
|
A list is always comprised of a head element and another list
|
|
(with the exception of the empty list, which is a special case).
|
|
Because on the recursive nature of list, we can reliably infer
|
|
that inductive properties of any list will also apply to the
|
|
child list of that list.
|
|
|
|
Prove that:
|
|
length (l @ r) = length l + length r
|
|
|
|
--- Properties ---
|
|
|
|
[1] [] @ x = x, because empty list is empty
|
|
[2] (l1 @ l2) @ l3 = l1 @ (l2 @ l3), because @ is like + but for lists
|
|
[3] x::xs = [x] @ xs, because that's how it works
|
|
|
|
--- Base Case: l = [] ---
|
|
|
|
length([] @ r) = length(r), by property [1]
|
|
length([]) + length(r) = 0 + length(r), by the definition of length
|
|
0 + length(r) = length(r), because identity property of 0
|
|
|
|
length r == length r, so length(l @ r) = length(l) + length(r) for l = []
|
|
|
|
--- Inductive Case: l = hd::tl ---
|
|
|
|
Given: length(l @ r) = length(l) + length(r)
|
|
Prove: length((el::l) @ r) = length(el::l) + length(r)
|
|
|
|
LET x = [el]
|
|
|
|
length(l @ r) = length(l) + length(r), given
|
|
length(x @ (l @ r)) = length(x) + (length(l) + length(r)), applying property again
|
|
length((x @ l) @ r) = length(x) + (length(l) + length(r)), by property [2]
|
|
length((x @ l) @ r) = length(x @ l) + length(r), by the given
|
|
length((el::l) @ r) = length(el::l) + length(r), substituting x @ l for el::l
|
|
|
|
∴ length (l @ r) = length l + length r
|
|
|
|
|
|
|
|
~.* Question 4 *.~
|
|
|
|
let rec reverse l =
|
|
match l with
|
|
| [] -> []
|
|
| x::xs -> reverse xs @ [x]
|
|
|
|
Prove that:
|
|
length (reverse l) = length l
|
|
|
|
--- Base Case: l = [] ---
|
|
|
|
length (reverse []) = length [], by the definition of reverse
|
|
length [] = 0, by the definition of length
|
|
|
|
Since 0 == 0, length (reverse l) = length l, for l = []
|
|
|
|
--- Inductive Case: l = hd::tail ---
|
|
|
|
Given: length (reverse l) = length l
|
|
Prove: length (reverse (el::l)) = length (el::l)
|
|
|
|
length (reverse l) = length l, given
|
|
length (reverse l) + 1 = length l + 1, adding 1 to both sides
|
|
length ((reverse l) @ [el]) = length l + 1, equivalent because appending an element gives length + 1
|
|
length (reverse (el::l)) = length l + 1, by the definition of reverse
|
|
length (reverse (el::l)) = length (el::l), equivalent because prepending an element gives length + 1
|
|
|
|
∴ length (reverse (el::l)) = length (el::l)
|
|
|
|
|
|
|
|
~.* Question 5 *.~
|
|
|
|
let rec append l1 l2 =
|
|
match l1 with
|
|
| [] -> l2
|
|
| (h::t) -> h :: (append t l2)
|
|
|
|
Prove that:
|
|
reverse (append l1 l2) = append (reverse l2) (reverse l1)
|
|
|
|
--- Properties ---
|
|
|
|
[1] append l1 l2 = l1 @ l2
|
|
Proof:
|
|
Base Case: l1 = []
|
|
append [] l2 = l2 (by definition of append), and [] @ l2 = l2
|
|
Inductive Case: l1 = (h::t)
|
|
Given that append l1 l2 = l1 @ l2
|
|
Prove that append (h::l1) l2 = (h::l1) @ l2
|
|
append (h::l1) l2 = h::(append l1 l2) = h::(l1 @ l2) = [h] @ (l1 @ l2)
|
|
(h::l1) @ l2 = ([h] @ l1) @ l2 = [h] @ (l1 @ l2)
|
|
[2] a :: b = [a] @ b
|
|
[3] [a] @ reverse (b) = reverse (b @ [a]), working backwards from the definition from reverse
|
|
Proof:
|
|
Base Case: b = []
|
|
[a] @ reverse [] = [a] @ [] = [a]
|
|
reverse ([] @ [a]) = reverse [a] = [a]
|
|
Inductive Case: l1 = (h::t)
|
|
Given that [a] @ reverse b = reverse (b @ [a])
|
|
Prove that [a] @ reverse (c::b) = reverse ((c::b) @ [a])
|
|
[a] @ reverse (c::b) = [a] @ reverse b @ [c]
|
|
reverse ((c::b) @ [a]) = reverse ([c] @ b @ [a]) = reverse (c :: (b @ [a]))
|
|
= reverse (b @ [a]) @ [c] = [a] @ reverse b @ [c]
|
|
|
|
|
|
--- Base Case: l1 = [] ---
|
|
|
|
reverse (append [] l2) = append (reverse l2) (reverse [])
|
|
reverse l2 = append (reverse l2) (reverse []), by definition of append
|
|
reverse l2 = append (reverse l2) [], by definition of reverse
|
|
reverse l2 = (reverse l2) @ [], by property [1]
|
|
reverse l2 = reverse l2, because that's how it works
|
|
|
|
reverse (append l1 l2) = append (reverse l2) (reverse l1), for l1 = []
|
|
|
|
--- Inductive Case: l1 = hd::tl ---
|
|
|
|
Given: reverse (append l1 l2) = append (reverse l2) (reverse l1)
|
|
Prove: reverse (append (hd::l1) l2) = append (reverse l2) (reverse (hd::l1))
|
|
|
|
reverse (append l1 l2) = append (reverse l2) (reverse l1)
|
|
reverse (l1 @ l2) = (reverse l2) @ (reverse l1), by property [1]
|
|
reverse (l1 @ l2) @ [hd] = ((reverse l2) @ (reverse l1)) @ [hd], adding hd to both sides
|
|
reverse (hd :: (l1 @ l2)) = (reverse l2) @ ((reverse l1) @ [hd]), by the definition of reverse
|
|
reverse ((hd::l1) @ l2) = (reverse l2) @ (reverse (hd::l1)), by the definition of reverse
|
|
reverse (append (hd::l1) l2) = append (reverse l2) (reverse (hd::l1)), by property [1]
|
|
|
|
∴ reverse (append l1 l2) = append (reverse l2) (reverse l1)
|
|
|
|
* Editor's note: I was using (l1 @ l2) mainly as syntactical sugar for (append l1 l2) because
|
|
ultimately I just turned it back into append; I didn't use any special property of @ that
|
|
didn't apply to append, so you could probably totally just read through the whole proof
|
|
substituting (l1 @ l2) with (append l1 l2) in your head.
|
|
|
|
|
|
|
|
~.* Question 6 *.~
|
|
|
|
let rec place e l =
|
|
match l with
|
|
| [ ] -> [e]
|
|
| x::xs ->
|
|
if e < x then e::x::xs
|
|
else x :: (place e xs)
|
|
|
|
let rec is_elem e l =
|
|
match l with
|
|
| [ ] -> false
|
|
| x::xs -> e = x || (e > x && is_elem e xs)
|
|
|
|
let rec sorted l =
|
|
match l with
|
|
| [ ] -> true
|
|
| x::[] -> true
|
|
| x1::x2::xs -> x1 <= x2 && sorted (x2::xs)
|
|
|
|
Prove that:
|
|
sorted l => sorted (place e l)
|
|
|