(* Exercise: spec game *)
(* Where is another programmer? *)
(* Exercise: poly spec *)
(* [Poly] represents immutable polynomials with integer coeffcients *)
module type Poly = sig
(* [t] is the type of polynomials *)
type t
(* [eval x p] is [p] evaluated at [x]. Example: if [p] represents $3x^3 + x^2 + x$, then [eval 10 p] is [3110]. *)
val eval : int -> t -> int
(* [create lst p] is [p] created from the list of coefficients [lst]. The order of the coefficients is from the highest degree to the lowest degree. Example: [create [3; 1; 1] p] is $3x^2 + x + 1$. *)
val create : int list -> t
(* [add p1 p2] is the sum of [p1] and [p2]. Example: if [p1] represents $3x^3 + x^2 + x$ and [p2] represents $2x^2 + 2x + 2$, then [add p1 p2] is $3x^3 + 3x^2 + 3x + 3$. *)
val add : t -> t -> t
(* [mul p1 p2] is the product of [p1] and [p2]. Example: if [p1] represents $3x^3 + x^2 + x$ and [p2] represents $2x^2 + 2x + 2$, then [mul p1 p2] is $6x^5 + 8x^4 + 5x^3 + 4x^2 + 2x$. *)
val mul : t -> t -> t
(* [to_string p] is the string representation of [p]. Example: if [p] represents $3x^3 + x^2 + x$, then [to_string p] is "3x^3 + x^2 + x". *)
val to_string : t -> string
end
(* 暂时不做 Specification 部分的作业 *)
end
----- Exercise: fibi -----
Claim: forall n >= 1, fib n = fibi n (0, 1) where:
let rec fib n =
if n = 1 then 1
else if n = 2 then 1
else fib (n - 2) + fib (n - 1)
let rec fibi n (prev, curr) =
if n = 1 then curr
else fibi (n - 1) (curr, prev + curr)
Proof: By induction on n.
Base case: n = 1
Show: fib 1 = fibi 1 (0, 1)
fib 1
= { evaluation }
1
fibi 1 (0, 1)
= { evaluation }
1
Inductive case: n = k + 1
Show: fib n = fibi n (0, 1)
IH1: fib k = fibi k (0, 1)
IH2: fib (k - 1) = fibi (k - 1) (0, 1)
fib n
= { algebra }
fib (k + 1)
= { evaluation }
fib k + fib (k - 1)
= { IH1 }
fibi k (0, 1) + fibi (k - 1) (0, 1)
= { evaluation }
fibi (k - 1) (1, 1) + fibi (k - 1) (0, 1)
fibi n (0, 1)
= { algebra }
fibi (k + 1) (0, 1)
= { evaluation }
fibi k (1, 1)
= { evaluation }
fibi (k - 1) (1, 2)
The proof is hard to follow. We need to strengthen the claim.
Claim: forall n >= 1, forall m >= 1, fib (n + m) = fibi n (fib m, fib (m + 1))
Proof: By induction on n.
Base case: n = 1
Show: forall m >= 1, fib (1 + m) = fibi 1 (fib m, fib (m + 1))
fibi 1 (fib m, fib (m + 1))
= { evaluation }
fib (m + 1)
Inductive case: n = k + 1
Show: forall m >= 1, fib (k + 1 + m) = fibi (k + 1) (fib m, fib (m + 1))
IH: forall n <= k, forall m >= 1, fib (n + m) = fibi n (fib m, fib (m + 1))
fib (k + 1 + m)
= { algebra }
fib (k + (1 + m)) // WTF? Human can think of this?
= { IH }
fibi k (fib (1 + m), fib (m + 2))
fibi (k + 1) (fib m, fib (m + 1))
= { evaluation }
fibi k (fib (m + 1), fib (m + 2))
Q.E.D.
----- Exercise: expsq -----
Claim: expsq x n = exp x n, where:
let rec expsq x n =
if n = 0 then 1
else if n = 1 then x
else (if n mod 2 = 0 then 1 else x) * expsq (x * x) (n / 2)
let rec exp x n =
if n = 0 then 1 else x * exp x (n - 1)
Proof: By strong induction on n.
Base case: n = 0
Show expsq x 0 = exp x 0
expsq x 0
= { evaluation }
1
= { evaluation }
exp x 0
Base case: n = 1
Show expsq x 1 = exp x 1
expsq x 1
= { evaluation }
x
= { evaluation }
exp x 1
Inductive case: n = 2 * k + 1
Show expsq x (2 * k + 1) = exp x (2 * k + 1)
IH: forall m < 2 * k + 1, expsq x m = exp x m
expsq x (2 * k + 1)
= { evaluation }
x * expsq (x * x) k
= { IH }
x * exp (x * x) k
exp x (2 * k + 1)
= { evaluation }
x * exp x (2 * k)
= { algebra }
x * exp (x * x) k
Inductive case: n = 2 * k
Show expsq x (2 * k) = exp x (2 * k)
IH: forall m < 2 * k, expsq x m = exp x m
expsq x (2 * k)
= { evaluation }
expsq (x * x) k
= { IH }
exp (x * x) k
exp x (2 * k)
= { algebra }
exp (x * x) k
Q.E.D.
----- Exercise: propositions -----
(* I dont really understand *)
Answer from github:
Induction principle for prop:
forall properties P,
if forall x, P(Atom x)
and forall q, P(q) implies P(Neg q)
and forall q r, (P(q) and P(r)) implies P(Conj (q,r))
and forall q r, (P(q) and P(r)) implies P(Disj (q,r))
and forall q r, (P(q) and P(r)) implies P(Imp (q,r))
then forall q, P(q)