Copyright | (C) 2017-2018 mniip |
---|---|
License | MIT |
Maintainer | mniip@mniip.com |
Stability | stable |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell2010 |
Synopsis
- induceIsZero :: KnownNat m => (forall n. KnownNat n => p (1 + n)) -> p 0 -> p m
- inducePeano :: KnownNat m => (forall n. KnownNat n => p n -> p (1 + n)) -> p 0 -> 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
- induceBaseComp :: forall r b q p m c s. (KnownNat b, b ~ (1 + c), KnownNat m) => s q -> r b -> (forall k. (KnownNat k, (1 + k) <= b) => q k) -> (forall k n. (KnownNat k, (1 + k) <= b, KnownNat n) => q k -> p n -> p ((1 + k) + (b * n))) -> p 0 -> p m
- induceUnary :: KnownNat m => (forall n. KnownNat n => p n -> p (1 + n)) -> p 1 -> p (1 + 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)
- inducePosBase :: forall r b q p m c s. (KnownNat b, b ~ (2 + c), KnownNat m) => s q -> r b -> (forall k. (KnownNat k, (1 + k) <= b) => q k) -> (forall k n. (KnownNat k, (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)
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)\)
For example:
inducePeano f z :: p 3 = f (f (f z))
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)\)
For example:
induceTwosComp f1 f2 z :: p 12 = f2 (f1 (f2 z))
induceBaseComp :: forall r b q p m c s. (KnownNat b, b ~ (1 + c), KnownNat m) => s q -> r b -> (forall k. (KnownNat k, (1 + k) <= b) => q k) -> (forall k n. (KnownNat k, (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)\)
For example:
induceBaseComp (_ :: s q) (_ :: r 10) d f z :: p 123 = (d :: q 2) `f` ((d :: q 1) `f` ((d :: q 0) `f` z)
The s q
parameter is necessary because presently GHC is unable to unify q
under the equational constraint 1 + k <= b
.
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)\)
For example:
induceUnary f o :: p 5 = f (f (f (f o)))
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)\)
For example:
inducePosBinary f0 f1 o :: p 10 = f0 (f1 (f0 o))
inducePosBase :: forall r b q p m c s. (KnownNat b, b ~ (2 + c), KnownNat m) => s q -> r b -> (forall k. (KnownNat k, (1 + k) <= b) => q k) -> (forall k n. (KnownNat k, (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)\)
For example:
inducePosBase (_ :: s q) (_ :: r 10) d f l :: p 123 = (d :: q 3) `f` ((d :: q 2) `f` l (d :: q 1))
The s q
parameter is necessary because presently GHC is unable to unify q
under the equational constraint 1 + k <= b
.