cont.txt

To get around this, we have to prove that this recursion is "welll-founded". Consider the example of `<` and `<=`. The 
relation `<` is well-founded but `<=` is not. Because in `a < b < c`, we know that `a` is strictly less than `b`. This is 
finite and terminating. Whereas we can make infinite chains of `a <= a <= a ...`. This is called "accessibility". Using this 
concept, we have to prove that our `power` function is well-founded. I cannot fully explain this here; I am still working on 
understanding it completely. But this talk by Eric Mertens, https://vimeo.com/36519234 is really great. And here's a similar 
implementation in Idris, https://github.com/idris-lang/Idris dev/blob/0d3d2d66796b172e9933360aee51993a4abc624d/libs/contrib/Data/Nat/DivMod/IteratedSubtraction.idr.

power.agda

-- link to the paper on views
-- (http://www.cs.tufts.edu/~nr/cs257/archive/phil-wadler/views.pdf)

data Parity : ℕ -> Set where
  even : (k : ℕ) -> Parity (k * 2)
  odd  : (k : ℕ) -> Parity (1 + k * 2)

parity : (n : ℕ) -> Parity n
parity zero = even zero
parity (succ n) with parity n
parity (succ .(k * 2)) | even k = odd k
parity (succ .(1 + k * 2)) | odd k = even (succ k)

power : ℕ -> ℕ -> ℕ
power m zero = 1
power m (succ n) with parity n
power m (succ .(k * 2)) | even k = power (m * m) k
power m (succ .(1 + k * 2)) | odd k = m * (power (m * m) k)

power.hs

power x Zero = 1
power x (Even n) = power (x * x) n
power x (Odd n) =  x * power (x * x) n