diff options
| -rw-r--r-- | 2-kyu/odd-even-odd-prove-it.hs | 86 |
1 files changed, 86 insertions, 0 deletions
diff --git a/2-kyu/odd-even-odd-prove-it.hs b/2-kyu/odd-even-odd-prove-it.hs new file mode 100644 index 0000000..998ea3d --- /dev/null +++ b/2-kyu/odd-even-odd-prove-it.hs @@ -0,0 +1,86 @@ +-- https://www.codewars.com/kata/599d973255342a0ce400009b + +{-# LANGUAGE GADTs, DataKinds, + TypeFamilies, UndecidableInstances #-} + +module OddsAndEvens where + +-- | The natural numbers. +data Nat = Z | S Nat + +-- | The axioms of even numbers. +data Even (a :: Nat) :: * where + -- | Zero is even. + ZeroEven :: Even Z + -- | If n is even, then n+2 is even. + NextEven :: Even n -> Even (S (S n)) + +-- | The axioms of odd numbers. +data Odd (a :: Nat) :: * where + -- | One is odd. + OneOdd :: Odd (S Z) + -- | If n is odd, then n+2 is odd. + NextOdd :: Odd n -> Odd (S (S n)) + +-- | Proves that if n is even, n+1 is odd. +-- Notice how I use the axioms here. +evenPlusOne :: Even n -> Odd (S n) +evenPlusOne ZeroEven = OneOdd +evenPlusOne (NextEven n) = NextOdd (evenPlusOne n) + +-- | Proves that if n is odd, n+1 is even. +oddPlusOne :: Odd n -> Even (S n) +oddPlusOne OneOdd = NextEven ZeroEven +oddPlusOne (NextOdd n) = NextEven (oddPlusOne n) + +-- | Adds two natural numbers together. +-- Notice how the definition pattern matches. +type family Add (n :: Nat) (m :: Nat) :: Nat +type instance Add Z m = m +type instance Add (S n) m = S (Add n m) + +-- | Proves even + even = even +-- Notice how the pattern matching mirrors `Add`s definition. +evenPlusEven :: Even n -> Even m -> Even (Add n m) +evenPlusEven ZeroEven m = m +evenPlusEven (NextEven n) m = NextEven (evenPlusEven n m) + +-- | Proves odd + odd = even +oddPlusOdd :: Odd n -> Odd m -> Even (Add n m) +oddPlusOdd OneOdd m = oddPlusOne m +oddPlusOdd (NextOdd n) m = NextEven (oddPlusOdd n m) + +-- | Proves even + odd = odd +evenPlusOdd :: Even n -> Odd m -> Odd (Add n m) +evenPlusOdd ZeroEven m = m +evenPlusOdd (NextEven n) m = NextOdd (evenPlusOdd n m) + +-- | Proves odd + even = odd +oddPlusEven :: Odd n -> Even m -> Odd (Add n m) +oddPlusEven OneOdd m = evenPlusOne m +oddPlusEven (NextOdd n) m = NextOdd (oddPlusEven n m) + +-- | Multiplies two natural numbers. +type family Mult (n :: Nat) (m :: Nat) :: Nat +type instance Mult Z m = Z +type instance Mult (S n) m = Add m (Mult n m) + +-- | Proves even * even = even +evenTimesEven :: Even n -> Even m -> Even (Mult n m) +evenTimesEven ZeroEven b = ZeroEven +evenTimesEven (NextEven n) m = evenPlusEven m $ evenPlusEven m $ evenTimesEven n m + +-- | Proves odd * odd = odd +oddTimesOdd :: Odd n -> Odd m -> Odd (Mult n m) +oddTimesOdd OneOdd m = oddPlusEven m ZeroEven +oddTimesOdd (NextOdd n) m = oddPlusEven m $ oddPlusOdd m $ oddTimesOdd n m + +-- | Proves even * odd = even +evenTimesOdd :: Even n -> Odd m -> Even (Mult n m) +evenTimesOdd ZeroEven b = ZeroEven +evenTimesOdd (NextEven n) m = oddPlusOdd m $ oddPlusEven m $ evenTimesOdd n m + +-- | Proves odd * even = even +oddTimesEven :: Odd n -> Even m -> Even (Mult n m) +oddTimesEven OneOdd m = evenPlusEven m ZeroEven +oddTimesEven (NextOdd n) m = evenPlusEven m $ evenPlusEven m $ oddTimesEven n m |