singleton-typelits-0.0.0.0: Singletons and induction over GHC TypeLits

Copyright (C) 2017 mniip MIT mniip@mniip.com experimental portable None Haskell2010

GHC.TypeLits.Induction

Description

Synopsis

# Natural number induction

induceIsZero :: KnownNat m => (forall n. KnownNat n => p (1 + n)) -> p 0 -> p m Source #

$$(\forall n. n > 0 \to P(n)) \to P(0) \to \forall m. P(m)$$

inducePeano :: KnownNat m => (forall n. KnownNat n => p n -> p (1 + n)) -> p 0 -> p m Source #

$$(\forall n. P(n) \to P(n + 1)) \to P(0) \to \forall m. P(m)$$

induceTwosComp :: KnownNat m => (forall n. KnownNat n => p n -> p (1 + (2 * n))) -> (forall n. KnownNat n => p n -> p (2 + (2 * n))) -> p 0 -> p m Source #

$$(\forall n. P(n) \to P(2n + 1)) \to \\ (\forall n. P(n) \to P(2n + 2)) \to \\ P(0) \to \\ \forall m. P(m)$$

induceBaseComp :: forall r b q p m. (KnownNat b, KnownNat m) => r b -> (forall m. KnownNat m => q m) -> (forall k n. (KnownNat b, (1 + k) <= b, KnownNat n) => q k -> p n -> p ((1 + k) + (b * n))) -> p 0 -> p m Source #

$$\forall b. (\prod_d Q(d)) \to \\ (\forall n. \forall d. d < b \to Q(d) \to P(n) \to P(bn + d + 1)) \to \\ \forall m. P(m)$$

# Positive number induction

induceUnary :: KnownNat m => (forall n. KnownNat n => p n -> p (1 + n)) -> p 1 -> p (1 + m) Source #

$$(\forall n. P(n) \to P(n + 1)) \to P(1) \to \forall m > 0. P(m)$$

inducePosBinary :: KnownNat m => (forall n. KnownNat n => p n -> p (2 * n)) -> (forall n. KnownNat n => p n -> p (1 + (2 * n))) -> p 1 -> p (1 + m) Source #

$$(\forall n. P(n) \to P(2n)) \to \\ (\forall n. P(n) \to P(2n + 1)) \to \\ P(1) \to \\ \forall m > 0. P(m)$$

inducePosBase :: forall r b q p m. (KnownNat b, KnownNat m) => r b -> (forall m. KnownNat m => q m) -> (forall k n. (KnownNat b, (1 + k) <= b, KnownNat n) => q k -> p n -> p (k + (b * n))) -> (forall k n. (KnownNat k, (1 + k) <= b, k ~ (1 + n)) => q k -> p k) -> p (1 + m) Source #

$$\forall b. (\prod_d Q(d)) \to \\ (\forall n. \forall d. d < b \to Q(d) \to P(n) \to P(bn + d)) \to \\ (\forall d. d > 0 \to d < b \to Q(d) \to P(d)) \to \\ \forall m > 0. P (m)$$