data Nat = Zero | Succ Nat
data List a = Nil | Cons a (List a)
take (Succ n) (Cons x xs) = Cons x (take n xs)
take (Succ n) Nil = Nil
take Zero (Cons x xs) = Nil
take n Nil = Nil
twice f x = f (f x)
-----------------------
twice (take n) = take n
Equivalently (by function equality):
twice (take n) xs = take n xs
Proof by induction on structure of xs :: List a:
Case xs = Nil:
twice (take n) Nil = take n Nil
take n (take n Nil) = take n Nil
By cases on n :: Nat:
Case n = Zero:
take Zero (take Zero Nil) = take Zero Nil
Nil = take Zero Nil
Nil = Nil
Case n = Succ m:
take (Succ m) (take (Succ m) Nil) = take (Succ m) Nil
Nil = take (Succ m) Nil
Nil = Nil
Case xs = Cons y ys; assume twice (take n) ys = take n ys
twice (take n) (Cons y ys) = take n (Cons y ys)
take n (take n (Cons y ys)) = take n (Cons y ys)
By induction on n :: Nat:
Case n = Zero:
take Zero (take Zero (Cons y ys)) = take Zero (Cons y ys)
Nil = take Zero (Cons y ys)
Nil = Nil
Case n = Succ m; assume take m (take m (Cons y ys)) = take m (Cons y ys)
________________________________________________
take (Succ m) (take (Succ m) (Cons y ys)) = take (Succ m) (Cons y ys)
take (Succ m) (Cons y (take m ys)) = take (Succ m) (Cons y ys)
Cons y (take m (take m ys)) = take (Succ m) (Cons y ys)
Cons y (take m (take m ys)) = Cons y (take m ys)
take m (take m ys) = take m ys