pub trait Nat {}
pub struct Succ<T>(T);

// Inductively define naturals
pub type _0 = ();
impl Nat for _0 {}
impl<T: Nat> Nat for Succ<T> {}

pub mod prelude {
    pub type _1 = Succ<_0>;
    pub type _2 = Succ<_1>;
    pub type _3 = Succ<_2>;
    pub type _4 = Succ<_3>;
    pub type _5 = Succ<_4>;
    pub type _6 = Succ<_5>;
    pub type _7 = Succ<_6>;
    pub type _8 = Succ<_7>;
    pub type _9 = Succ<_8>;
    pub type _10 = Succ<_9>;
    
    pub use super::{
        Nat,
        Succ,
        _0,
        
        eq::Eq,

        leq::Leq,
        geq::Geq,
        
        add::Add,
        mul::Mul,
        exp::Exp,

        parity::Even,
        parity::Odd
    };
}

pub mod eq {
    use super::prelude::*;

    pub trait Eq<A: Nat> {
        fn equal() -> () {}
    }

    // Define equality of naturals
    impl<A: Nat> Eq<A> for A {}
}

pub mod leq {
    use super::prelude::*;

    pub trait Leq<A: Nat> {
        fn leq() -> () {}
    }

    // Base case
    // 0 <= N for every N
    impl<A: Nat> Leq<A> for _0 {}
    
    // Induction
    // A <= B means S(A) <= S(B)
    impl<A: Nat, B: Nat> Leq<Succ<B>> for Succ<A>
    where
        A: Leq<B>
    {}
}

pub mod geq {
    use super::prelude::*;

    pub trait Geq<A: Nat> {
        fn geq() -> () {}
    }

    // If A <= B then B => A
    impl<A: Nat, B: Nat> Geq<A> for B
    where
        A: Leq<B>
    {}
}

pub mod add {
    use super::prelude::*;

    pub trait Add<RHS: Nat> {
        type Sum: Nat;
    }

    // Base case
    // N + 0 = N
    impl<T: Nat> Add<_0> for T {
        type Sum = T;
    }

    // Induction
    // A + S(B) = S(A + B)
    impl<A: Nat, B: Nat> Add<Succ<B>> for A
    where
        A: Add<B>
    {
        type Sum = Succ<<A as Add<B>>::Sum>;
    }
}

pub mod mul {
    use super::prelude::*;

    pub trait Mul<RHS: Nat> {
        type Prod: Nat;
    }

    // Base case
    // N * 0 = 0
    impl<T: Nat> Mul<_0> for T {
        type Prod = _0;
    }

    // Induction
    // A * S(B) = A * B + A
    impl<A: Nat, B: Nat> Mul<Succ<B>> for A
    where
        A: Mul<B>,
        <A as Mul<B>>::Prod: Add<A>
    {
        type Prod = <<A as Mul<B>>::Prod as Add<A>>::Sum;
    }
}

pub mod exp {
    use super::prelude::*;

    pub trait Exp<P: Nat> {
        type Pow: Nat;
    }

    // Base case
    // N ^ 0 = 1
    impl<T: Nat> Exp<_0> for T {
        type Pow = _1;
    }

    // Induction
    // A ^ S(B) = A ^ B * A
    impl<A: Nat, B: Nat> Exp<Succ<B>> for A
    where
        A: Exp<B>,
        <A as Exp<B>>::Pow: Mul<A>
    {
        type Pow =
            <<A as Exp<B>>::Pow as Mul<A>>::Prod;
    }
}

pub mod parity {
    use super::prelude::*;

    pub trait Even {
        fn even() -> () {}
    }

    pub trait Odd {
        fn odd() -> () {}
    }
    
    impl Even for _0 {}
    impl<N: Even> Even for Succ<Succ<N>> {}

    impl Odd for _1 {}
    impl<N: Odd> Odd for Succ<Succ<N>> {}
}