//显示为∀ 的字符是：For all
Theorem triang_closed:
∀n. sumTo n = n*(n+1)/2
Copyright By PowCoder代写 加微信 powcoder
By induction on n.
Case 0: ‘sumTo 0 = 0*(0+1)/2’ (can’t be bothered)
Successor case:
Assuming ‘sumTo n = n*(n+1)/2’
Show ‘sumTo(n+1) = (n+1)*((n+1)+1)/2’
‘sumTo(n+1)’
= (by definition)
‘n + 1 + sumTo(n)’
= (by induction hypothesis)
‘n + 1 + n*(n+1)/2’
= (by laws of algebra)
‘(2n + 2)/2 + n*(n+1)/2’
‘(2n + 2 + n*(n+1))/2’
= (by distributive laws)
‘(n+1)*(n+2)/2’
Theorem add_right_ident:
∀n ∈ Nat. add n Z = n
By induction on n
‘add Z Z = Z’
= (by definition)
Case (Suc n):
Assume: ‘add n Z = n’ <-- that's not n', it's just a formula in backticks
Show: ‘add (S n) Z = S n’
‘add (S n) Z’
= (by definition add)
‘S(add n Z)’
= (by inductive hypothesis)
Theorem take_length_eq:
∀xs. take (length xs) xs = xs
By induction on xs.
Case [] (Nil): ‘take (length []) [] = []’
‘take (length []) []’
= (by def of length)
‘take Z []’
= (by def of take)
Case : (Cons):
assume ‘take (length xs) xs = xs’
show ‘take (length (x:xs)) (x:xs) = (x:xs)’
‘take (length (x:xs)) (x:xs)’
= (unfold length)
‘take (S(length xs)) (x:xs)’
= (unfold take)
‘x:take (length xs) xs’
Theorem take_length_eq:
∀xs. take 5 xs ++ drop 5 xs = xs
By induction on xs
‘take 5 [] ++ drop 5 [] = []’
(by def of take and drop and ++)
Case Cons:
Assume ‘take 5 xs ++ drop 5 xs = xs’
Show ‘take 5 (x:xs) ++ drop 5 (x:xs) = x:xs’
‘take 5 (x:xs) ++ drop 5 (x:xs)’
= (unfolding a bunch of defs)
‘x:take 4 xs ++ drop 4 xs’
... now what?
We can't apply the IH, because the IH mentions 5 not 4.
we *could* dig ourselves out of this hole by just ignoring the IH
and doing case analysis on the length of xs
Case xs = Nil
Case xs = [x]
Case xs = [x,y]
instead, we can generalise the theorem statement (by replacing a constant with a variable)
Theorem take_length_eq:
∀xs. ∀n. take n xs ++ drop n xs = xs
By induction on xs
‘∀n. take n [] ++ drop n [] = []’
(by def and some case analysis)
Case Cons:
Assume ‘∀m. take m xs ++ drop m xs = xs’
Show ‘∀n. take n (x:xs) ++ drop n (x:xs) = x:xs’
Case analysis on n
‘take Z (x:xs) ++ drop Z (x:xs) = x:xs’
follows by unfolding definitions
Case S: ‘take (S n) (x:xs) ++ drop (S n) (x:xs) = x:xs’
‘take (S n) (x:xs) ++ drop (S n) (x:xs)’
= (unfolding the defs take and drop)
‘x:take n xs ++ drop n xs’
= (by definition ++)
‘x:(take n xs ++ drop n xs)’
Theorem height_le_leaves:
∀t. height t < leaves t
By (strucutural) induction on t
Case Leaf: ‘height Leaf < leaves Leaf’
aka ‘0 < 1’ (after unfolding definitions)
Case Branch:
assuming (1) ‘height l < leaves l’
(2) ‘height r < leaves r’
show ‘height (Branch a l r) < leaves(Branch a l r)’
‘height (Branch a l r)’
= (by def)
‘1 + max(height l) (height r)’
< (by IH, and the monotonicity of max)
‘1 + max(leaves l) (leaves r)’
≤ (the missing bit)
here, we would need a lemma stating that ‘∀t. leaves t > 0’
‘leaves l + leaves r’
= (by def)
‘leaves(Branch a l r)’
Theorem height_le_leaves:
∀t. height t ≤ size t
‘∀t. height t ≤ size t’ (that’s P)
‘∀f. height’ f ≤ size’ f’ (that’s Q)
by (mutual) (structural) induction
Case Empty:
‘height’ Empty ≤ size’ Empty’
Case Cons:
(1) ‘height r ≤ size r’
(2) ‘height’ f ≤ size’ r’
Show ‘height'(Cons r f) ≤ size'(Cons r f)’
‘height'(Cons r f)’
‘max (height r) (height’ f)’
≤ (by the inductive hypotheses, and the monotonicity of max)
‘max (size r) (size’ f)’
≤ (a fact of arithmetic, that we could prove as a lemma)
‘size r + size’ f’
= (by def)
size'(Cons r f)
Case Node:
Assume: ‘height’ f ≤ size’ r’
Show ‘height(Node a f) ≤ size(Node a f)’
‘height(Node a f)’
‘1 + height’ f’
‘1 + size’ r’
= (by def)
‘size(Node a f)’
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com