Divide and Conquer
------------------

-------
Summary:
Destructor style induction (at least)
------

------
Definitions:

app 
---

(list T) -> (list T) -> (list T)

(app nil L) = L
(app (cons H T) L) = (cons H (app T L)) 

bin_dc 
------

(T -> T -> T) -> T -> (list T) -> T

(bin_dc F B nil) = B
(bin_dc F B (cons X nil)) = X
L \= nil and L \= (cons (hd L) nil) ->
(bin_dc F B L) = (F (bin_dc F B (take (quot (len L) 2) L (bin_dc F B (drop (quot (len L) 2) L)))))

drop 
----

nat -> (list T) -> (list T)

(drop 0 L) = L 
(drop (s N) nil) = nil
(drop (s N) (cons H T)) = (drop N T)

foldright 
---------

(T -> T -> T) -> T -> (list T) -> T

(foldlright F A nil) = A
(foldright F A (cons H T)) = (F H (foldright F A T))map 

(A -> B) -> (list A) -> (list B)

map
---

(map F nil) = nil
(map F (cons H T)) = (cons (F H) (map F T))split 

split
-----
nat -> (list T) -> (list (list T))

(split 0 L) = (cons L nil)
(split (s 0) L) = (cons L nil)
(split (s (s X)) L) = (cons (take (quot (len L) (s (s X))) L) (split (s X) (drop (quot (len L) (s (s X))) L)))

take 
----

nat -> (list T) -> (list T)

(take 0 L) = nil
(take (s N) nil) = nil
(take (s N) (cons H T)) = (cons H (take N T))

------

Theorem:

forall f:(t -> t). forall b,x:t. forall l:(list t). forall n:nat.
(f b x) = x -> (bin_dc f b l) = (foldright f b (foldright app nil (map (map (f b)) (split n l))))

------
Comments:

Prove the equivalence of two divide_and_conquer algorithms.

------

Source:
Greg Michaelson