{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
{-# LANGUAGE GADTs, StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE ExplicitNamespaces #-}

{-# LANGUAGE UndecidableInstances #-}


-- |
-- Module      : OAlg.Entity.Natural
-- Description : natrual numbers promoted to type-level
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- natural numbers promotable to type-level. They serve to parameterize the length of finite lists on
-- type-level (see "OAlg.Entity.FinList").
--
-- __Note__ We need the language extension @UndecidableInstances@ for type checking the definition
--
-- > N0 * m = N0
-- > S n * m = m + n * m
--
-- for the type family t'*'.
--
-- Using @UndecidableInstances@ could cause the type checker to not terminate, but this will
-- obviously not happen for the given definition (we also use the same definition for the
-- multiplicative structure of 'N'').
module OAlg.Entity.Natural
  ( -- * Natrual Numbers
     N'(..), toN', type (+), type (*)

    -- * Attest
  , Attestable(..), Ats(..), nValue, W(..), cmpW, (++), (**), W'(..), toW'
  , SomeNatural(..), succSomeNatural, someNatural, naturals

    -- * Induction
  , induction


    -- * Propositions
    -- | The following propositions are based - for the most part - on induction.
    --   To ensure that the /proofs/ yield a terminal value, i.e. 'Refl', we
    --   used in the /proof/ of the induction hypothesis only propositions which
    --   are proofed before. So: if these propositions terminate, then also
    --   the hypothesis will terminate.
  , Any, Some

    -- | __Some basic Lemmas__
  , refl, lemma1, sbstAdd

    -- | __Some abbreviations__
  , prpAdd0, prpAdd1, prpAdd2

    -- | __Equivalence of Any__  
  , prpEqlAny, prpEqlAny'

    -- | __Injectivity of the Successor__
  , prpSuccInjective

    -- ** Addition
    -- | __Neutral Element__
    -- 
    -- t'N0' is the neutral element of t'+'.
  , prpAddNtrlL, prpAddNtrlR

    -- | __Associativity__
  , prpAddAssoc

    -- | __Commutativity__
  , lemmaAdd1, prpAddComm

    -- ** Multiplication
    -- | __Neutral Element__
    --
    -- @'N1' = 'S' t'N0'@ is the neutral element of t'*'.
  , prpMltNtrlL, prpMltNtrlR

    -- | __Distributivity on the left__
  , prpDstrL

    -- | __Associativity__
  , prpMltAssoc

    -- | __Distributivity on the right__
  , lemmaMlt1, lemmaAdd2, prpDstrR

    -- | __Commutativity__
  , prpMltComm

    -- * Some attests
    -- | generating the Haskell code and interface for witnesses.
  , codeW, itfW

  , type N0, type N1, type N2, type N3, type N4, type N5
  , type N6, type N7, type N8, type N9, type N10
{-
, type N0, w0, type N1, w1, type N2, w2, type N3, w3
, type N4, w4, type N5, w5, type N6, w6, type N7, w7
, type N8, w8, type N9, w9, type N10, w10, type N11, w11
, type N12, w12, type N13, w13, type N14, w14, type N15, w15
, type N16, w16, type N17, w17, type N18, w18, type N19, w19
, type N20, w20, type N21, w21, type N22, w22, type N23, w23
, type N24, w24, type N25, w25, type N26, w26, type N27, w27
, type N28, w28, type N29, w29, type N30, w30, type N31, w31
, type N32, w32, type N33, w33, type N34, w34, type N35, w35
, type N36, w36, type N37, w37, type N38, w38, type N39, w39
, type N40, w40, type N41, w41, type N42, w42, type N43, w43
, type N44, w44, type N45, w45, type N46, w46, type N47, w47
, type N48, w48, type N49, w49, type N50, w50, type N51, w51
, type N52, w52, type N53, w53, type N54, w54, type N55, w55
, type N56, w56, type N57, w57, type N58, w58, type N59, w59
, type N60, w60, type N61, w61, type N62, w62, type N63, w63
-}

    -- * X
  , xSomeNatural
  )
  where

import Control.Monad (join,return, (>>=))
import Control.Exception

import Data.Typeable
import Data.Type.Equality
import qualified Data.List as L

import OAlg.Prelude

import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative
import OAlg.Structure.Fibred
import OAlg.Structure.Additive hiding (prpAdd1,prpAdd2)
import OAlg.Structure.Distributive

--------------------------------------------------------------------------------
-- N' -

-- | natural number promotable to type-level.
data N' = N0 | S N' deriving (N' -> N' -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: N' -> N' -> Bool
$c/= :: N' -> N' -> Bool
== :: N' -> N' -> Bool
$c== :: N' -> N' -> Bool
Eq,Eq N'
N' -> N' -> Bool
N' -> N' -> Ordering
N' -> N' -> N'
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: N' -> N' -> N'
$cmin :: N' -> N' -> N'
max :: N' -> N' -> N'
$cmax :: N' -> N' -> N'
>= :: N' -> N' -> Bool
$c>= :: N' -> N' -> Bool
> :: N' -> N' -> Bool
$c> :: N' -> N' -> Bool
<= :: N' -> N' -> Bool
$c<= :: N' -> N' -> Bool
< :: N' -> N' -> Bool
$c< :: N' -> N' -> Bool
compare :: N' -> N' -> Ordering
$ccompare :: N' -> N' -> Ordering
Ord,Int -> N' -> ShowS
[N'] -> ShowS
N' -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [N'] -> ShowS
$cshowList :: [N'] -> ShowS
show :: N' -> String
$cshow :: N' -> String
showsPrec :: Int -> N' -> ShowS
$cshowsPrec :: Int -> N' -> ShowS
Show)

instance LengthN N' where
  lengthN :: N' -> N
lengthN N'
N0 = N
0
  lengthN (S N'
i) = N
1 forall a. Additive a => a -> a -> a
+ forall x. LengthN x => x -> N
lengthN N'
i

--------------------------------------------------------------------------------
-- toN' -

-- | mapping a natural number in 'N' to 'N''.
toN' :: N -> N'
toN' :: N -> N'
toN' N
0 = N'
N0
toN' N
i = N' -> N'
S (N -> N'
toN' (N
iN -> N -> N
>-N
1))

----------------------------------------
-- (+) -

infixr 6 +
  
-- | addition of natural numbers.
type family (+) (n :: N') (m :: k) :: N'
type instance N0 + n = n
type instance S n + (m :: N') = S (n+m)
type instance n + 0 = n
type instance n + 1 = S n
type instance n + 2 = S (S n)
type instance n + 3 = S (S (S n))

----------------------------------------
-- (*) -
infixr 7 *

-- | multiplication of natural numbers.
type family (*) (n :: k) (m :: N') :: N'
type instance N0 * m  = N0
type instance S n * m = m + (n * m)
-- the reason for switching the variables is to define (**) easely, without any infering of equality.
type instance 0 * m = N0
type instance 1 * m = m
type instance 2 * m = m + m

----------------------------------------
-- N' - CmpN' -

-- | comparing two natural numbers.
type family CmpN' (n :: N') (m :: N') :: Ordering
type instance CmpN' N0 N0    = EQ
type instance CmpN' (S _) N0 = GT
type instance CmpN' N0 (S _) = LT
type instance CmpN' (S n) (S m) = CmpN' n m

----------------------------------------
-- N' - Enum -
instance Enum N' where
  succ :: N' -> N'
succ = N' -> N'
S
  
  pred :: N' -> N'
pred N'
N0    = forall a e. Exception e => e -> a
throw AlgebraicException
NoPredecor
  pred (S N'
i) = N'
i

  toEnum :: Int -> N'
toEnum Int
0 = N'
N0
  toEnum Int
i = forall a. Enum a => a -> a
succ forall (h :: Type -> Type -> Type) a b.
Applicative h =>
h a b -> a -> b
$ forall a. Enum a => Int -> a
toEnum (Int
iforall a. Abelian a => a -> a -> a
-Int
1)

  fromEnum :: N' -> Int
fromEnum N'
N0 = Int
0
  fromEnum (S N'
i) = Int
1forall a. Additive a => a -> a -> a
+forall a. Enum a => a -> Int
fromEnum N'
i

----------------------------------------
-- N' - Entity -

instance Validable N' where
  valid :: N' -> Statement
valid N'
N0    = Statement
SValid
  valid (S N'
n) = forall a. Validable a => a -> Statement
valid N'
n

instance Entity N'

----------------------------------------
-- N' - Structure -

instance Oriented N' where
  type Point N' = ()
  orientation :: N' -> Orientation (Point N')
orientation = forall b a. b -> a -> b
const (()forall p. p -> p -> Orientation p
:>())

instance Multiplicative N' where
  one :: Point N' -> N'
one () = N' -> N'
S N'
N0
  N'
N0 * :: N' -> N' -> N'
* N'
_   = N'
N0
  S N'
n * N'
m  = N'
m forall a. Additive a => a -> a -> a
+ N'
n forall c. Multiplicative c => c -> c -> c
* N'
m -- (1+n)*m = n*m + m

instance Fibred N' where
  type Root N' = Orientation ()
instance FibredOriented N'

instance Additive N' where
  zero :: Root N' -> N'
zero Root N'
_ = N'
N0
  N'
N0 + :: N' -> N' -> N'
+ N'
m  = N'
m
  S N'
n + N'
m = N' -> N'
S (N'
n forall a. Additive a => a -> a -> a
+ N'
m)

instance Distributive N'
instance Commutative N'
instance Total N'
-- instance Number N'

--------------------------------------------------------------------------------
-- W -

-- | witness for a natural number and serves for inductively definable elements (see 'induction'). 
data W n where
  W0 :: W N0
  SW :: W n -> W (n+1)
  
deriving instance Eq (W n)

-- | comparing of two witnesses.
cmpW :: W n -> W m -> Ordering
cmpW :: forall (n :: N') (m :: N'). W n -> W m -> Ordering
cmpW W n
W0 W m
W0         = Ordering
EQ
cmpW (SW W n
_) W m
W0     = Ordering
GT
cmpW W n
W0 (SW W n
_)     = Ordering
LT
cmpW (SW W n
n) (SW W n
m) = forall (n :: N') (m :: N'). W n -> W m -> Ordering
cmpW W n
n W n
m

instance Show (W n) where
  show :: W n -> String
show W n
w = forall a. Show a => a -> String
show (forall x. LengthN x => x -> N
lengthN W n
w)

instance Validable (W n) where
  valid :: W n -> Statement
valid W n
W0     = Statement
SValid
  valid (SW W n
w) = forall a. Validable a => a -> Statement
valid W n
w

instance LengthN (W n) where
  lengthN :: W n -> N
lengthN W n
W0     = N
0
  lengthN (SW W n
i) = N
1 forall a. Additive a => a -> a -> a
+ forall x. LengthN x => x -> N
lengthN W n
i
  
--------------------------------------------------------------------------------
-- (++)

infixr 6 ++

-- | addition of witnesses.
(++) :: W n -> W m -> W (n+m)
W n
W0 ++ :: forall (n :: N') (m :: N'). W n -> W m -> W (n + m)
++ W m
m = W m
m
(SW W n
n) ++ W m
m = forall (n :: N'). W n -> W (n + 1)
SW (W n
nforall (n :: N') (m :: N'). W n -> W m -> W (n + m)
++W m
m)

--------------------------------------------------------------------------------
-- (**) -
infixr 7 **

-- | multiplication of witnesses.
(**) :: W n -> W m -> W (n*m)
W n
W0 ** :: forall (n :: N') (m :: N'). W n -> W m -> W (n * m)
** W m
_ = W N0
W0
(SW W n
n) ** W m
m = W m
m forall (n :: N') (m :: N'). W n -> W m -> W (n + m)
++ W n
nforall (n :: N') (m :: N'). W n -> W m -> W (n * m)
**W m
m

--------------------------------------------------------------------------------
-- induction-

-- | predicate for any natural number.
type Any = W

-- | induction for general type functions.
induction :: Any n -> f N0 -> (forall i . f i -> f (i+1)) -> f n
induction :: forall (n :: N') (f :: N' -> Type).
Any n -> f N0 -> (forall (i :: N'). f i -> f (i + 1)) -> f n
induction W n
W0 f N0
f0 forall (i :: N'). f i -> f (i + 1)
_    = f N0
f0
induction (SW W n
i) f N0
f0 forall (i :: N'). f i -> f (i + 1)
h = forall (i :: N'). f i -> f (i + 1)
h (forall (n :: N') (f :: N' -> Type).
Any n -> f N0 -> (forall (i :: N'). f i -> f (i + 1)) -> f n
induction W n
i f N0
f0 forall (i :: N'). f i -> f (i + 1)
h)

--------------------------------------------------------------------------------
-- Attestable -

-- | attest for any natural number.
class Typeable n => Attestable n where
  attest :: W n

instance Attestable N0 where
  attest :: W N0
attest = W N0
W0

instance Attestable n => Attestable (S n) where
  attest :: W ('S n)
attest = forall (n :: N'). W n -> W (n + 1)
SW forall (n :: N'). Attestable n => W n
attest

--------------------------------------------------------------------------------
-- Ats -

-- | witness of being attestable.
data Ats n where Ats :: Attestable n => Ats n

--------------------------------------------------------------------------------
-- nValue -

-- | the corresponding natural number in 'N' of a type parameterized by @__n__@.
nValue :: Attestable n => p n -> N
nValue :: forall (n :: N') (p :: N' -> Type). Attestable n => p n -> N
nValue p n
p = forall (p :: N' -> Type) (n :: N'). p n -> Any n -> N
nValue' p n
p forall (n :: N'). Attestable n => W n
attest where
  nValue' :: p n -> Any n -> N
  nValue' :: forall (p :: N' -> Type) (n :: N'). p n -> Any n -> N
nValue' p n
_ = forall x. LengthN x => x -> N
lengthN

--------------------------------------------------------------------------------
-- SomeNatural -

-- | witnesse of some natural.
data SomeNatural where
  SomeNatural :: Attestable n => W n -> SomeNatural

instance Show SomeNatural where
  show :: SomeNatural -> String
show (SomeNatural W n
n) = forall a. Show a => a -> String
show W n
n

-- | equality for witnesses.
eqlW :: W n -> W m -> Bool
eqlW :: forall (n :: N') (m :: N'). W n -> W m -> Bool
eqlW W n
W0 W m
W0         = Bool
True
eqlW W n
W0 (SW W n
_)     = Bool
False
eqlW (SW W n
_) W m
W0     = Bool
False
eqlW (SW W n
n) (SW W n
m) = forall (n :: N') (m :: N'). W n -> W m -> Bool
eqlW W n
n W n
m

instance Eq SomeNatural where
  SomeNatural W n
n == :: SomeNatural -> SomeNatural -> Bool
== SomeNatural W n
m = forall (n :: N') (m :: N'). W n -> W m -> Bool
eqlW W n
n W n
m

instance Validable SomeNatural where
  valid :: SomeNatural -> Statement
valid (SomeNatural W n
n) = forall a. Validable a => a -> Statement
valid W n
n

--------------------------------------------------------------------------------
-- succSomeNatural -

-- | successor of some natural number.
succSomeNatural :: SomeNatural -> SomeNatural
succSomeNatural :: SomeNatural -> SomeNatural
succSomeNatural (SomeNatural W n
n) = forall (n :: N'). Attestable n => W n -> SomeNatural
SomeNatural (forall (n :: N'). W n -> W (n + 1)
SW W n
n)

--------------------------------------------------------------------------------
-- someNatural -

-- | mapping 'N' to 'SomeNatural'.
--
--   __Note__ The implementation of this mapping is quite inefficent for high values of 'N'.
someNatural :: N -> SomeNatural
someNatural :: N -> SomeNatural
someNatural N
0 = forall (n :: N'). Attestable n => W n -> SomeNatural
SomeNatural W N0
W0
someNatural N
i = SomeNatural -> SomeNatural
succSomeNatural (N -> SomeNatural
someNatural (forall a. Enum a => a -> a
pred N
i))

--------------------------------------------------------------------------------
-- xSomeNatural -

-- | the induced random variable for some natural number.
xSomeNatural :: X N -> X SomeNatural
xSomeNatural :: X N -> X SomeNatural
xSomeNatural X N
xn = X N
xn forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: Type -> Type) a. Monad m => a -> m a
return forall (c :: Type -> Type -> Type) y z x.
Category c =>
c y z -> c x y -> c x z
. N -> SomeNatural
someNatural
    
--------------------------------------------------------------------------------
-- naturals -

-- | the infinite list of some naturals.
naturals :: [SomeNatural]
naturals :: [SomeNatural]
naturals = SomeNatural -> [SomeNatural]
nats (N -> SomeNatural
someNatural N
0) where nats :: SomeNatural -> [SomeNatural]
nats SomeNatural
n = SomeNatural
n forall a. a -> [a] -> [a]
: SomeNatural -> [SomeNatural]
nats (SomeNatural -> SomeNatural
succSomeNatural SomeNatural
n)

--------------------------------------------------------------------------------
-- W' -

-- | union of all witnesses, which is isomorphic to 'N' and 'N''.
data W' = forall n . W' (W n) 

deriving instance Show W'

instance Eq W' where
  W' W n
n == :: W' -> W' -> Bool
== W' W n
m = case forall (n :: N') (m :: N'). W n -> W m -> Ordering
cmpW W n
n W n
m of
    Ordering
EQ -> Bool
True
    Ordering
_  -> Bool
False

instance Ord W' where
  compare :: W' -> W' -> Ordering
compare (W' W n
n) (W' W n
m) = forall (n :: N') (m :: N'). W n -> W m -> Ordering
cmpW W n
n W n
m

instance LengthN W' where
  lengthN :: W' -> N
lengthN (W' W n
w) = forall x. LengthN x => x -> N
lengthN W n
w

-- | mapping a natural value in 'N' to 'W''.
toW' :: N -> W'
toW' :: N -> W'
toW' N
0 = forall (n :: N'). W n -> W'
W' W N0
W0
toW' N
n = forall a. Enum a => a -> a
succ forall (h :: Type -> Type -> Type) a b.
Applicative h =>
h a b -> a -> b
$ N -> W'
toW' (N
nN -> N -> N
>-N
1)

----------------------------------------
-- W' - Enum -
instance Enum W' where
  succ :: W' -> W'
succ (W' W n
w) = forall (n :: N'). W n -> W'
W' (forall (n :: N'). W n -> W (n + 1)
SW W n
w)

  pred :: W' -> W'
pred (W' W n
W0)     = forall a e. Exception e => e -> a
throw AlgebraicException
NoPredecor
  pred (W' (SW W n
w)) = forall (n :: N'). W n -> W'
W' W n
w

  toEnum :: Int -> W'
toEnum = N -> W'
toW' forall (c :: Type -> Type -> Type) y z x.
Category c =>
c y z -> c x y -> c x z
. forall a. Enum a => Int -> a
toEnum
  fromEnum :: W' -> Int
fromEnum = forall a. Enum a => a -> Int
fromEnum forall (c :: Type -> Type -> Type) y z x.
Category c =>
c y z -> c x y -> c x z
. forall x. LengthN x => x -> N
lengthN

----------------------------------------
-- W' - Entity -

instance Validable W' where
  valid :: W' -> Statement
valid (W' W n
w) = forall a. Validable a => a -> Statement
valid W n
w

instance Entity W'

----------------------------------------
-- W' - Structure -

instance Oriented W' where
  type Point W' = ()
  orientation :: W' -> Orientation (Point W')
orientation = forall b a. b -> a -> b
const (()forall p. p -> p -> Orientation p
:>())

instance Multiplicative W' where
  one :: Point W' -> W'
one () = forall a. Enum a => a -> a
succ (forall a. Additive a => Root a -> a
zero (()forall p. p -> p -> Orientation p
:>()))
  W' W n
W0 * :: W' -> W' -> W'
* W'
_     = forall (n :: N'). W n -> W'
W' W N0
W0
  W' (SW W n
n) * W'
m = W'
m forall a. Additive a => a -> a -> a
+ forall (n :: N'). W n -> W'
W' W n
n forall c. Multiplicative c => c -> c -> c
* W'
m

instance Fibred W' where
  type Root W' = Orientation ()
instance FibredOriented W'

instance Additive W' where
  zero :: Root W' -> W'
zero (():>()) = forall (n :: N'). W n -> W'
W' W N0
W0
  W' W n
W0     + :: W' -> W' -> W'
+ W'
m = W'
m
  W' (SW W n
n) + W'
m = forall a. Enum a => a -> a
succ (forall (n :: N'). W n -> W'
W' W n
n forall a. Additive a => a -> a -> a
+ W'
m)
  
instance Distributive W'
instance Commutative W'
instance Total W'
-- instance Number W'

---------------------------------------------------------------------------------
-- Propositon -

-- | some witness.
type Some = W'

infixl 0 >>
(>>) :: forall {k} {a :: k} {b :: k} {c :: k} . (a :~: b) -> (b :~: c) -> a :~: c
>> :: forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
(>>) = forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
trans

--------------------------------------------------------------------------------
-- refl -

-- | reflexivity.
refl :: Any x -> x :~: x
refl :: forall (x :: N'). Any x -> x :~: x
refl Any x
_ = forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- lemma1 -

-- | well definition of parameterized types.
lemma1 :: x :~: y -> f x :~: f y
lemma1 :: forall {k} {k} (x :: k) (y :: k) (f :: k -> k).
(x :~: y) -> f x :~: f y
lemma1 x :~: y
Refl = forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- sbstAdd -

-- | substitution rule for addition.
sbstAdd :: a :~: a' -> b :~: b' -> a + b :~: a' + b'
sbstAdd :: forall {k} (a :: N') (a' :: N') (b :: k) (b' :: k).
(a :~: a') -> (b :~: b') -> (a + b) :~: (a' + b')
sbstAdd a :~: a'
Refl b :~: b'
Refl = forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- prpAdd -

-- | @0@ is right neural for the addition.
prpAdd0 :: a + 0 :~: a
prpAdd0 :: forall (a :: N'). (a + 0) :~: a
prpAdd0 = forall {k} (a :: k). a :~: a
Refl

-- | adding @1@ is equal to the successor.
prpAdd1 :: a + 1 :~: S a
prpAdd1 :: forall (a :: N'). (a + 1) :~: 'S a
prpAdd1 = forall {k} (a :: k). a :~: a
Refl

-- | adding @2@ is equal to the successor of the successor.
prpAdd2 :: a + 2 :~: S (S a)
prpAdd2 :: forall (a :: N'). (a + 2) :~: 'S ('S a)
prpAdd2 = forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- prpMlt -

-- | mutlitplication with @0@ is zero.
prpMlt0 :: 0*a :~: N0
prpMlt0 :: forall (a :: N'). (0 * a) :~: N0
prpMlt0 = forall {k} (a :: k). a :~: a
Refl

-- | @1@ is left neutral for the multiplication.
prpMlt1 :: 1*a :~: a
prpMlt1 :: forall (a :: N'). (1 * a) :~: a
prpMlt1 = forall {k} (a :: k). a :~: a
Refl

prpMlt2 :: p a -> 2*a :~: a + a
prpMlt2 :: forall (p :: N' -> Type) (a :: N'). p a -> (2 * a) :~: (a + a)
prpMlt2 p a
_ = forall {k} (a :: k). a :~: a
Refl

---------------------------------------------------------------------------------
-- prpEqlAny -

-- | equality of the underlying natural number.
prpEqlAny :: Any n :~: Any m -> n :~: m
prpEqlAny :: forall (n :: N') (m :: N'). (Any n :~: Any m) -> n :~: m
prpEqlAny Any n :~: Any m
Refl = forall {k} (a :: k). a :~: a
Refl

-- | 'Any' is as parameterized type is well defined.
prpEqlAny' ::  n :~: m -> Any n :~: Any m
prpEqlAny' :: forall (n :: N') (m :: N'). (n :~: m) -> Any n :~: Any m
prpEqlAny' n :~: m
Refl = forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- prpSuccInjective -

-- | successor is injective.
prpSuccInjective :: S n :~: S m -> n :~: m
prpSuccInjective :: forall (n :: N') (m :: N'). ('S n :~: 'S m) -> n :~: m
prpSuccInjective 'S n :~: 'S m
Refl = forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- prpAddNtrlL -

-- | t'N0' is left neutral for the addition.
prpAddNtrlL :: p a -> N0 + a :~: a
prpAddNtrlL :: forall (p :: N' -> Type) (a :: N'). p a -> (N0 + a) :~: a
prpAddNtrlL p a
_ = forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- prpAddNtrlR -

-- | t'N0' is the right neutral for the addition.
prpAddNtrlR :: Any a -> a + N0 :~: a

-- anchoring -
prpAddNtrlR :: forall (a :: N'). Any a -> (a + N0) :~: a
prpAddNtrlR W a
W0     = forall {k} (a :: k). a :~: a
Refl

-- hypothesis -
prpAddNtrlR (SW W n
a) = forall (a :: N'). Any a -> ((a + 1) + N0) :~: (a + 1)
qed W n
a where
  qed :: Any a -> (a+1) + N0 :~: a+1
  qed :: forall (a :: N'). Any a -> ((a + 1) + N0) :~: (a + 1)
qed Any a
a = forall (p :: N' -> Type) (a :: N').
p a -> ((a + 1) + N0) :~: ('S a + N0)
r1 Any a
a forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (p :: N' -> Type) (a :: N').
p a -> ('S a + N0) :~: 'S (a + N0)
r2 Any a
a forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N'). Any a -> 'S (a + N0) :~: 'S a
hyp Any a
a forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (p :: N' -> Type) (a :: N'). p a -> 'S a :~: (a + 1)
r3 Any a
a

  r1  :: p a   -> (a+1) + N0 :~: S a + N0
  r2  :: p a   -> S a + N0   :~: S (a + N0)
  hyp :: Any a -> S (a + N0) :~: S a
  r3  :: p a   -> S a        :~: a+1

  r1 :: forall (p :: N' -> Type) (a :: N').
p a -> ((a + 1) + N0) :~: ('S a + N0)
r1  p a
_ = forall {k} (a :: k). a :~: a
Refl
  r2 :: forall (p :: N' -> Type) (a :: N').
p a -> ('S a + N0) :~: 'S (a + N0)
r2  p a
_ = forall {k} (a :: k). a :~: a
Refl 
  hyp :: forall (a :: N'). Any a -> 'S (a + N0) :~: 'S a
hyp Any a
a = forall {k} {k} (x :: k) (y :: k) (f :: k -> k).
(x :~: y) -> f x :~: f y
lemma1 forall (h :: Type -> Type -> Type) a b.
Applicative h =>
h a b -> a -> b
$ forall (a :: N'). Any a -> (a + N0) :~: a
prpAddNtrlR Any a
a
  r3 :: forall (p :: N' -> Type) (a :: N'). p a -> 'S a :~: (a + 1)
r3  p a
_ = forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- prpAddAssoc -

-- | addition is associative.
prpAddAssoc :: Any a -> Any b -> Any c -> (a + b) + c :~: a + (b + c)

-- anchoring -
prpAddAssoc :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + b) + c) :~: (a + (b + c))
prpAddAssoc W a
W0 Any b
_ Any c
_ = forall {k} (a :: k). a :~: a
Refl

-- hypothesis -
prpAddAssoc (SW W n
a) Any b
b Any c
c = forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b -> Any c -> (((a + 1) + b) + c) :~: ((a + 1) + (b + c))
qed W n
a Any b
b Any c
c where
  qed :: Any a -> Any b -> Any c -> ((a+1) + b) + c :~: (a+1) + (b + c)
  qed :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b -> Any c -> (((a + 1) + b) + c) :~: ((a + 1) + (b + c))
qed Any a
a Any b
b Any c
c = forall {k} {k} (a :: N') (p :: k -> Type) (b :: k) (q :: k -> Type)
       (c :: k).
Any a -> p b -> q c -> (((a + 1) + b) + c) :~: (('S a + b) + c)
r1 Any a
a Any b
b Any c
c forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (('S a + b) + c) :~: ('S (a + b) + c)
r2 Any a
a Any b
b Any c
c forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ('S (a + b) + c) :~: 'S ((a + b) + c)
r3 Any a
a Any b
b Any c
c forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> 'S ((a + b) + c) :~: 'S (a + (b + c))
hyp Any a
a Any b
b Any c
c forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> 'S (a + (b + c)) :~: ('S a + (b + c))
r4 Any a
a Any b
b Any c
c forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ('S a + (b + c)) :~: ((a + 1) + (b + c))
r5 Any a
a Any b
b Any c
c 

  r1  :: Any a -> p b   -> q c   -> ((a+1) + b) + c :~: (S a + b) + c
  r2  :: Any a -> Any b -> Any c -> (S a + b) + c   :~: S (a + b) + c
  r3  :: Any a -> Any b -> Any c -> S (a + b) + c   :~: S ((a + b) + c)
  hyp :: Any a -> Any b -> Any c -> S ((a + b) + c) :~: S (a + (b + c))
  r4  :: Any a -> Any b -> Any c -> S (a + (b + c)) :~: (S a + (b + c)) 
  r5  :: Any a -> Any b -> Any c -> S a + (b + c)   :~: (a+1) + (b + c)

  r1 :: forall {k} {k} (a :: N') (p :: k -> Type) (b :: k) (q :: k -> Type)
       (c :: k).
Any a -> p b -> q c -> (((a + 1) + b) + c) :~: (('S a + b) + c)
r1  Any a
_ p b
_ q c
_ = forall {k} (a :: k). a :~: a
Refl
  r2 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (('S a + b) + c) :~: ('S (a + b) + c)
r2  Any a
_ Any b
_ Any c
_ = forall {k} (a :: k). a :~: a
Refl
  r3 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ('S (a + b) + c) :~: 'S ((a + b) + c)
r3  Any a
_ Any b
_ Any c
_ = forall {k} (a :: k). a :~: a
Refl
  hyp :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> 'S ((a + b) + c) :~: 'S (a + (b + c))
hyp Any a
a Any b
b Any c
c = forall {k} {k} (x :: k) (y :: k) (f :: k -> k).
(x :~: y) -> f x :~: f y
lemma1 forall (h :: Type -> Type -> Type) a b.
Applicative h =>
h a b -> a -> b
$ forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + b) + c) :~: (a + (b + c))
prpAddAssoc Any a
a Any b
b Any c
c 
  r4 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> 'S (a + (b + c)) :~: ('S a + (b + c))
r4  Any a
_ Any b
_ Any c
_ = forall {k} (a :: k). a :~: a
Refl
  r5 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ('S a + (b + c)) :~: ((a + 1) + (b + c))
r5  Any a
_ Any b
_ Any c
_ = forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- lemmaAdd1 -

-- | lemma 1 for the addition.
lemmaAdd1 :: Any a -> Any b -> S a + b :~: a + S b

-- anchoring -
lemmaAdd1 :: forall (a :: N') (b :: N').
Any a -> Any b -> ('S a + b) :~: (a + 'S b)
lemmaAdd1 W a
W0 Any b
_ = forall {k} (a :: k). a :~: a
Refl

-- hypothesis -
lemmaAdd1 (SW W n
a) Any b
b = forall (a :: N') (b :: N').
Any a -> Any b -> ('S (a + 1) + b) :~: ((a + 1) + 'S b)
qed W n
a Any b
b where
  qed :: Any a -> Any b -> S (a+1) + b :~: (a+1) + S b
  qed :: forall (a :: N') (b :: N').
Any a -> Any b -> ('S (a + 1) + b) :~: ((a + 1) + 'S b)
qed Any a
a Any b
b = forall (a :: N') (b :: N').
Any a -> Any b -> ('S (a + 1) + b) :~: ('S ('S a) + b)
r1 Any a
a Any b
b forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N').
Any a -> Any b -> ('S ('S a) + b) :~: 'S ('S a + b)
r2 Any a
a Any b
b forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N').
Any a -> Any b -> 'S ('S a + b) :~: 'S (a + 'S b)
hyp Any a
a Any b
b forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N').
Any a -> Any b -> 'S (a + 'S b) :~: ('S a + 'S b)
r3 Any a
a Any b
b forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N').
Any a -> Any b -> ('S a + 'S b) :~: ((a + 1) + 'S b)
r4 Any a
a Any b
b

  r1  :: Any a -> Any b -> S (a+1) + b :~: S (S a) + b
  r2  :: Any a -> Any b -> S (S a) + b :~: S (S a + b)
  hyp :: Any a -> Any b -> S (S a + b) :~: S (a + S b)
  r3  :: Any a -> Any b -> S (a + S b) :~: S a + S b
  r4  :: Any a -> Any b -> S a + S b   :~: (a+1) + S b  

  r1 :: forall (a :: N') (b :: N').
Any a -> Any b -> ('S (a + 1) + b) :~: ('S ('S a) + b)
r1  Any a
_ Any b
_ = forall {k} (a :: k). a :~: a
Refl 
  r2 :: forall (a :: N') (b :: N').
Any a -> Any b -> ('S ('S a) + b) :~: 'S ('S a + b)
r2  Any a
_ Any b
_ = forall {k} (a :: k). a :~: a
Refl
  hyp :: forall (a :: N') (b :: N').
Any a -> Any b -> 'S ('S a + b) :~: 'S (a + 'S b)
hyp Any a
a Any b
b = forall {k} {k} (x :: k) (y :: k) (f :: k -> k).
(x :~: y) -> f x :~: f y
lemma1 forall (h :: Type -> Type -> Type) a b.
Applicative h =>
h a b -> a -> b
$ forall (a :: N') (b :: N').
Any a -> Any b -> ('S a + b) :~: (a + 'S b)
lemmaAdd1 Any a
a Any b
b
  r3 :: forall (a :: N') (b :: N').
Any a -> Any b -> 'S (a + 'S b) :~: ('S a + 'S b)
r3  Any a
_ Any b
_ = forall {k} (a :: k). a :~: a
Refl
  r4 :: forall (a :: N') (b :: N').
Any a -> Any b -> ('S a + 'S b) :~: ((a + 1) + 'S b)
r4  Any a
_ Any b
_ = forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- prpAddComm -

-- | addition is commutative.
prpAddComm :: Any a -> Any b -> a + b :~: b + a 

-- anchoring -
prpAddComm :: forall (a :: N') (b :: N'). Any a -> Any b -> (a + b) :~: (b + a)
prpAddComm W a
W0 Any b
b = forall (b :: N'). Any b -> (N0 + b) :~: (b + N0)
qed Any b
b where
  qed :: Any b -> N0 + b :~: b + N0
  qed :: forall (b :: N'). Any b -> (N0 + b) :~: (b + N0)
qed Any b
b = forall (b :: N'). Any b -> (N0 + b) :~: b
r1 Any b
b forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (b :: N'). Any b -> b :~: (b + N0)
r2 Any b
b

  r1 :: Any b -> N0 + b :~: b
  r2 :: Any b -> b      :~: b + N0

  r1 :: forall (b :: N'). Any b -> (N0 + b) :~: b
r1 = forall (p :: N' -> Type) (a :: N'). p a -> (N0 + a) :~: a
prpAddNtrlL
  r2 :: forall (b :: N'). Any b -> b :~: (b + N0)
r2 Any b
b = forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym forall (h :: Type -> Type -> Type) a b.
Applicative h =>
h a b -> a -> b
$ forall (a :: N'). Any a -> (a + N0) :~: a
prpAddNtrlR Any b
b

-- hypothesis -
prpAddComm (SW W n
a) Any b
b = forall (a :: N') (b :: N').
Any a -> Any b -> ((a + 1) + b) :~: (b + (a + 1))
qed W n
a Any b
b where
  qed :: Any a -> Any b -> (a+1) + b :~: b + (a+1)
  qed :: forall (a :: N') (b :: N').
Any a -> Any b -> ((a + 1) + b) :~: (b + (a + 1))
qed Any a
a Any b
b = forall (a :: N') (b :: N').
Any a -> Any b -> ((a + 1) + b) :~: ('S a + b)
r1 Any a
a Any b
b forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N').
Any a -> Any b -> ('S a + b) :~: 'S (a + b)
r2 Any a
a Any b
b forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N').
Any a -> Any b -> 'S (a + b) :~: 'S (b + a)
hyp Any a
a Any b
b forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N').
Any a -> Any b -> 'S (b + a) :~: ('S b + a)
r3 Any a
a Any b
b forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N').
Any a -> Any b -> ('S b + a) :~: (b + 'S a)
r4 Any a
a Any b
b forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N').
Any a -> Any b -> (b + 'S a) :~: (b + (a + 1))
r5 Any a
a Any b
b

  r1  :: Any a -> Any b -> (a+1) + b :~: S a + b
  r2  :: Any a -> Any b -> S a + b   :~: S (a + b)
  hyp :: Any a -> Any b -> S (a + b) :~: S (b + a)
  r3  :: Any a -> Any b -> S (b + a) :~: S b + a 
  r4  :: Any a -> Any b -> S b + a   :~: b + S a
  r5  :: Any a -> Any b -> b + S a   :~: b + (a+1)

  r1 :: forall (a :: N') (b :: N').
Any a -> Any b -> ((a + 1) + b) :~: ('S a + b)
r1  Any a
_ Any b
_ = forall {k} (a :: k). a :~: a
Refl 
  r2 :: forall (a :: N') (b :: N').
Any a -> Any b -> ('S a + b) :~: 'S (a + b)
r2  Any a
_ Any b
_ = forall {k} (a :: k). a :~: a
Refl
  hyp :: forall (a :: N') (b :: N').
Any a -> Any b -> 'S (a + b) :~: 'S (b + a)
hyp Any a
a Any b
b = forall {k} {k} (x :: k) (y :: k) (f :: k -> k).
(x :~: y) -> f x :~: f y
lemma1 forall (h :: Type -> Type -> Type) a b.
Applicative h =>
h a b -> a -> b
$ forall (a :: N') (b :: N'). Any a -> Any b -> (a + b) :~: (b + a)
prpAddComm Any a
a Any b
b
  r3 :: forall (a :: N') (b :: N').
Any a -> Any b -> 'S (b + a) :~: ('S b + a)
r3  Any a
_ Any b
_ = forall {k} (a :: k). a :~: a
Refl
  r4 :: forall (a :: N') (b :: N').
Any a -> Any b -> ('S b + a) :~: (b + 'S a)
r4  Any a
a Any b
b = forall (a :: N') (b :: N').
Any a -> Any b -> ('S a + b) :~: (a + 'S b)
lemmaAdd1 Any b
b Any a
a 
  r5 :: forall (a :: N') (b :: N').
Any a -> Any b -> (b + 'S a) :~: (b + (a + 1))
r5  Any a
_ Any b
_ = forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- prpMltNtrlL -

-- | 'N1' is left neutral for the multiplication.
prpMltNtrlL :: Any a -> N1*a :~: a
prpMltNtrlL :: forall (a :: N'). Any a -> (N1 * a) :~: a
prpMltNtrlL Any a
a = forall (a :: N'). Any a -> (N1 * a) :~: a
qed Any a
a where
  qed :: Any a -> N1 * a :~: a
  qed :: forall (a :: N'). Any a -> (N1 * a) :~: a
qed Any a
a = forall (a :: N'). Any a -> (N1 * a) :~: (N1 * a)
r1 Any a
a forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N'). Any a -> (N1 * a) :~: (a + (N0 * a))
r2 Any a
a forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N'). Any a -> (a + (N0 * a)) :~: (a + N0)
r3 Any a
a forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N'). Any a -> (a + N0) :~: a
r4 Any a
a

  r1  :: Any a -> N1 * a   :~: (S N0)*a
  r2  :: Any a -> (S N0)*a :~: a + N0*a
  r3  :: Any a -> a + N0*a :~: a + N0
  r4  :: Any a -> a + N0   :~: a


  r1 :: forall (a :: N'). Any a -> (N1 * a) :~: (N1 * a)
r1 Any a
_ = forall {k} (a :: k). a :~: a
Refl
  r2 :: forall (a :: N'). Any a -> (N1 * a) :~: (a + (N0 * a))
r2 Any a
_ = forall {k} (a :: k). a :~: a
Refl
  r3 :: forall (a :: N'). Any a -> (a + (N0 * a)) :~: (a + N0)
r3 Any a
_ = forall {k} (a :: k). a :~: a
Refl
  r4 :: forall (a :: N'). Any a -> (a + N0) :~: a
r4 Any a
a = forall (a :: N'). Any a -> (a + N0) :~: a
prpAddNtrlR Any a
a 

--------------------------------------------------------------------------------
-- prpMltNtrlR -

-- | 'N1' is right neutral for the multiplication.
prpMltNtrlR :: Any a -> a*N1 :~: a

-- anchoring -
prpMltNtrlR :: forall (a :: N'). Any a -> (a * N1) :~: a
prpMltNtrlR W a
W0 = forall {k} (a :: k). a :~: a
Refl

-- hypothesis -
prpMltNtrlR (SW W n
a) = forall (a :: N'). Any a -> ((a + 1) * N1) :~: (a + 1)
qed W n
a where
  qed :: Any a -> (a+1)*N1 :~: a+1
  qed :: forall (a :: N'). Any a -> ((a + 1) * N1) :~: (a + 1)
qed Any a
a = forall (a :: N'). Any a -> ((a + 1) * N1) :~: ('S a * N1)
r1 Any a
a forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N'). Any a -> ('S a * N1) :~: (N1 + (a * N1))
r2 Any a
a forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N'). Any a -> (N1 + (a * N1)) :~: (N1 + a)
hyp Any a
a forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N'). Any a -> (N1 + a) :~: (N1 + a)
r3 Any a
a forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N'). Any a -> (N1 + a) :~: (N0 + 'S a)
r4 Any a
a forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N'). Any a -> (N0 + 'S a) :~: 'S a
r5 Any a
a forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N'). Any a -> 'S a :~: (a + 1)
r6 Any a
a

  r1  :: Any a -> (a+1)*N1   :~: S a * N1
  r2  :: Any a -> S a * N1   :~: N1 + a*N1
  hyp :: Any a -> N1 + a*N1  :~: N1 + a
  r3  :: Any a -> N1 + a     :~: S N0 + a
  r4  :: Any a -> S N0 + a   :~: N0 + S a
  r5  :: Any a -> N0 + S a   :~: S a 
  r6  :: Any a -> S a        :~: a+1

  r1 :: forall (a :: N'). Any a -> ((a + 1) * N1) :~: ('S a * N1)
r1  Any a
_ = forall {k} (a :: k). a :~: a
Refl
  r2 :: forall (a :: N'). Any a -> ('S a * N1) :~: (N1 + (a * N1))
r2  Any a
_ = forall {k} (a :: k). a :~: a
Refl
  hyp :: forall (a :: N'). Any a -> (N1 + (a * N1)) :~: (N1 + a)
hyp Any a
a = forall {k} (a :: N') (a' :: N') (b :: k) (b' :: k).
(a :~: a') -> (b :~: b') -> (a + b) :~: (a' + b')
sbstAdd (forall (x :: N'). Any x -> x :~: x
refl W N1
w1) (forall (a :: N'). Any a -> (a * N1) :~: a
prpMltNtrlR Any a
a)
  r3 :: forall (a :: N'). Any a -> (N1 + a) :~: (N1 + a)
r3  Any a
_ = forall {k} (a :: k). a :~: a
Refl
  r4 :: forall (a :: N'). Any a -> (N1 + a) :~: (N0 + 'S a)
r4  Any a
a = forall (a :: N') (b :: N').
Any a -> Any b -> ('S a + b) :~: (a + 'S b)
lemmaAdd1 W N0
w0 Any a
a
  r5 :: forall (a :: N'). Any a -> (N0 + 'S a) :~: 'S a
r5  Any a
_ = forall {k} (a :: k). a :~: a
Refl
  r6 :: forall (a :: N'). Any a -> 'S a :~: (a + 1)
r6  Any a
_ = forall {k} (a :: k). a :~: a
Refl


--------------------------------------------------------------------------------
-- prpDstrL -

-- | law of left distributivity holds.
prpDstrL :: Any a -> Any b -> Any c -> (a + b)*c :~: a*c + b*c

-- anchoring -
prpDstrL :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + b) * c) :~: ((a * c) + (b * c))
prpDstrL W a
W0 Any b
_ Any c
_ = forall {k} (a :: k). a :~: a
Refl

-- hypothesis -
prpDstrL (SW W n
a) Any b
b Any c
c = forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> (((a + 1) + b) * c) :~: (((a + 1) * c) + (b * c))
qed W n
a Any b
b Any c
c where
  qed :: Any a -> Any b -> Any c -> ((a+1) + b)*c :~: (a+1)*c + b*c
  qed :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> (((a + 1) + b) * c) :~: (((a + 1) * c) + (b * c))
qed Any a
a Any b
b Any c
c =  forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (((a + 1) + b) * c) :~: (('S a + b) * c)
r1 Any a
a Any b
b Any c
c forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (('S a + b) * c) :~: ('S (a + b) * c)
r2 Any a
a Any b
b Any c
c forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ('S (a + b) * c) :~: (c + ((a + b) * c))
r3 Any a
a Any b
b Any c
c
            forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> (c + ((a + b) * c)) :~: (c + ((a * c) + (b * c)))
hyp Any a
a Any b
b Any c
c forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> (c + ((a * c) + (b * c))) :~: ((c + (a * c)) + (b * c))
r4 Any a
a Any b
b Any c
c forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> ((c + (a * c)) + (b * c)) :~: (((a + 1) * c) + (b * c))
r5 Any a
a Any b
b Any c
c

  r1  :: Any a -> Any b -> Any c -> ((a+1) + b)*c   :~: (S a + b)*c
  r2  :: Any a -> Any b -> Any c -> (S a + b)*c     :~: S (a + b) * c
  r3  :: Any a -> Any b -> Any c -> S (a + b) * c   :~: c + (a + b)*c
  hyp :: Any a -> Any b -> Any c -> c + (a + b)*c   :~: c + a*c + b*c
  r4  :: Any a -> Any b -> Any c -> c + a*c + b*c   :~: (c + a*c) + b*c
  r5  :: Any a -> Any b -> Any c -> (c + a*c) + b*c :~: (a+1)*c + b*c

  r1 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (((a + 1) + b) * c) :~: (('S a + b) * c)
r1  Any a
_ Any b
_ Any c
_ = forall {k} (a :: k). a :~: a
Refl
  r2 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (('S a + b) * c) :~: ('S (a + b) * c)
r2  Any a
_ Any b
_ Any c
_ = forall {k} (a :: k). a :~: a
Refl
  r3 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ('S (a + b) * c) :~: (c + ((a + b) * c))
r3  Any a
_ Any b
_ Any c
_ = forall {k} (a :: k). a :~: a
Refl
  hyp :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> (c + ((a + b) * c)) :~: (c + ((a * c) + (b * c)))
hyp Any a
a Any b
b Any c
c = forall {k} (a :: N') (a' :: N') (b :: k) (b' :: k).
(a :~: a') -> (b :~: b') -> (a + b) :~: (a' + b')
sbstAdd (forall (x :: N'). Any x -> x :~: x
refl Any c
c) (forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + b) * c) :~: ((a * c) + (b * c))
prpDstrL Any a
a Any b
b Any c
c)
  r4 :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> (c + ((a * c) + (b * c))) :~: ((c + (a * c)) + (b * c))
r4  Any a
a Any b
b Any c
c = forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym forall (h :: Type -> Type -> Type) a b.
Applicative h =>
h a b -> a -> b
$ forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + b) + c) :~: (a + (b + c))
prpAddAssoc Any c
c (Any a
aforall (n :: N') (m :: N'). W n -> W m -> W (n * m)
**Any c
c) (Any b
bforall (n :: N') (m :: N'). W n -> W m -> W (n * m)
**Any c
c)
  r5 :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> ((c + (a * c)) + (b * c)) :~: (((a + 1) * c) + (b * c))
r5  Any a
_ Any b
_ Any c
_ = forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- prpMltAssoc -

-- | multiplication is associative.
prpMltAssoc :: Any a -> Any b -> Any c -> (a*b)*c :~: a*(b*c)

-- anchoring -
prpMltAssoc :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a * b) * c) :~: (a * (b * c))
prpMltAssoc W a
W0 Any b
_ Any c
_ = forall {k} (a :: k). a :~: a
Refl

-- hypothesis -
prpMltAssoc (SW W n
a) Any b
b Any c
c = forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b -> Any c -> (((a + 1) * b) * c) :~: ((a + 1) * (b * c))
qed W n
a Any b
b Any c
c where
  qed :: Any a -> Any b -> Any c -> ((a+1)*b)*c :~: (a+1)*(b*c)
  qed :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b -> Any c -> (((a + 1) * b) * c) :~: ((a + 1) * (b * c))
qed Any a
a Any b
b Any c
c = forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (((a + 1) * b) * c) :~: (('S a * b) * c)
r1 Any a
a Any b
b Any c
c forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (('S a * b) * c) :~: ((b + (a * b)) * c)
r2 Any a
a Any b
b Any c
c forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> ((b + (a * b)) * c) :~: ((b * c) + ((a * b) * c))
r3 Any a
a Any b
b Any c
c forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> ((b * c) + ((a * b) * c)) :~: ((b * c) + (a * (b * c)))
hyp Any a
a Any b
b Any c
c forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b -> Any c -> ((b * c) + (a * (b * c))) :~: ('S a * (b * c))
r4 Any a
a Any b
b Any c
c forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ('S a * (b * c)) :~: ((a + 1) * (b * c))
r5 Any a
a Any b
b Any c
c

  r1  :: Any a -> Any b -> Any c -> ((a+1)*b)*c   :~: (S a * b)*c
  r2  :: Any a -> Any b -> Any c -> (S a * b)*c   :~: (b + a*b)*c 
  r3  :: Any a -> Any b -> Any c -> (b + a*b)*c   :~: b*c + (a*b)*c
  hyp :: Any a -> Any b -> Any c -> b*c + (a*b)*c :~: b*c + a*(b*c)
  r4  :: Any a -> Any b -> Any c -> b*c + a*(b*c) :~: S a * (b*c)
  r5  :: Any a -> Any b -> Any c -> S a * (b*c)   :~: (a+1)*(b*c)

  r1 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (((a + 1) * b) * c) :~: (('S a * b) * c)
r1  Any a
_ Any b
_ Any c
_ = forall {k} (a :: k). a :~: a
Refl
  r2 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (('S a * b) * c) :~: ((b + (a * b)) * c)
r2  Any a
_ Any b
_ Any c
_ = forall {k} (a :: k). a :~: a
Refl
  r3 :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> ((b + (a * b)) * c) :~: ((b * c) + ((a * b) * c))
r3  Any a
a Any b
b Any c
c = forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + b) * c) :~: ((a * c) + (b * c))
prpDstrL Any b
b (Any a
aforall (n :: N') (m :: N'). W n -> W m -> W (n * m)
**Any b
b) Any c
c
  hyp :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> ((b * c) + ((a * b) * c)) :~: ((b * c) + (a * (b * c)))
hyp Any a
a Any b
b Any c
c = forall {k} (a :: N') (a' :: N') (b :: k) (b' :: k).
(a :~: a') -> (b :~: b') -> (a + b) :~: (a' + b')
sbstAdd (forall (x :: N'). Any x -> x :~: x
refl (Any b
bforall (n :: N') (m :: N'). W n -> W m -> W (n * m)
**Any c
c)) (forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a * b) * c) :~: (a * (b * c))
prpMltAssoc Any a
a Any b
b Any c
c)
  r4 :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b -> Any c -> ((b * c) + (a * (b * c))) :~: ('S a * (b * c))
r4  Any a
_ Any b
_ Any c
_ = forall {k} (a :: k). a :~: a
Refl
  r5 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ('S a * (b * c)) :~: ((a + 1) * (b * c))
r5  Any a
_ Any b
_ Any c
_ = forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- lemmaMlt1 -

-- | right multiplication of t'N0' is t'N0'.
lemmaMlt1 :: Any a -> a*N0 :~: N0

-- anchoring -
lemmaMlt1 :: forall (a :: N'). Any a -> (a * N0) :~: N0
lemmaMlt1 W a
W0 = forall {k} (a :: k). a :~: a
Refl

-- hypothesis -
lemmaMlt1 (SW W n
a) = forall (a :: N'). Any a -> ((a + 1) * N0) :~: N0
qed W n
a where
  qed :: Any a -> (a+1)*N0 :~: N0
  qed :: forall (a :: N'). Any a -> ((a + 1) * N0) :~: N0
qed Any a
a = forall (a :: N'). Any a -> ((a + 1) * N0) :~: ('S a * N0)
r1 Any a
a forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N'). Any a -> ('S a * N0) :~: (N0 + (a * N0))
r2 Any a
a forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N'). Any a -> (N0 + (a * N0)) :~: (a * N0)
r3 Any a
a forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N'). Any a -> (a * N0) :~: N0
hyp Any a
a

  r1  :: Any a -> (a+1)*N0  :~: (S a)*N0
  r2  :: Any a -> (S a)*N0  :~: N0 + a*N0
  r3  :: Any a -> N0 + a*N0 :~: a*N0
  hyp :: Any a -> a*N0      :~: N0

  r1 :: forall (a :: N'). Any a -> ((a + 1) * N0) :~: ('S a * N0)
r1  Any a
_ = forall {k} (a :: k). a :~: a
Refl
  r2 :: forall (a :: N'). Any a -> ('S a * N0) :~: (N0 + (a * N0))
r2  Any a
_ = forall {k} (a :: k). a :~: a
Refl
  r3 :: forall (a :: N'). Any a -> (N0 + (a * N0)) :~: (a * N0)
r3  Any a
_ = forall {k} (a :: k). a :~: a
Refl
  hyp :: forall (a :: N'). Any a -> (a * N0) :~: N0
hyp Any a
a = forall (a :: N'). Any a -> (a * N0) :~: N0
lemmaMlt1 Any a
a

--------------------------------------------------------------------------------
-- lemmaAdd2 -

-- | lemma 2 for addition.
lemmaAdd2 :: Any a -> Any b -> Any c -> a + b + c :~: b + a + c
lemmaAdd2 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (a + (b + c)) :~: (b + (a + c))
lemmaAdd2 Any a
a Any b
b Any c
c = forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (a + (b + c)) :~: (b + (a + c))
qed Any a
a Any b
b Any c
c where
  qed :: Any a -> Any b -> Any c -> a + b + c :~: b + a + c
  qed :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (a + (b + c)) :~: (b + (a + c))
qed Any a
a Any b
b Any c
c = forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (a + (b + c)) :~: ((a + b) + c)
r1 Any a
a Any b
b Any c
c forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + b) + c) :~: ((b + a) + c)
r2 Any a
a Any b
b Any c
c forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((b + a) + c) :~: (b + (a + c))
r3 Any a
a Any b
b Any c
c

  r1 :: Any a -> Any b -> Any c -> a + b + c   :~: (a + b) + c
  r2 :: Any a -> Any b -> Any c -> (a + b) + c :~: (b + a) + c
  r3 :: Any a -> Any b -> Any c -> (b + a) + c :~: b + a + c

  r1 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (a + (b + c)) :~: ((a + b) + c)
r1 Any a
a Any b
b Any c
c = forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym forall (h :: Type -> Type -> Type) a b.
Applicative h =>
h a b -> a -> b
$ forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + b) + c) :~: (a + (b + c))
prpAddAssoc Any a
a Any b
b Any c
c
  r2 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + b) + c) :~: ((b + a) + c)
r2 Any a
a Any b
b Any c
c = forall {k} (a :: N') (a' :: N') (b :: k) (b' :: k).
(a :~: a') -> (b :~: b') -> (a + b) :~: (a' + b')
sbstAdd (forall (a :: N') (b :: N'). Any a -> Any b -> (a + b) :~: (b + a)
prpAddComm Any a
a Any b
b) (forall (x :: N'). Any x -> x :~: x
refl Any c
c)
  r3 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((b + a) + c) :~: (b + (a + c))
r3 Any a
a Any b
b Any c
c = forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + b) + c) :~: (a + (b + c))
prpAddAssoc Any b
b Any a
a Any c
c

--------------------------------------------------------------------------------
-- prpDstrR -

-- | law of right distributivity holds.
prpDstrR :: Any a -> Any b -> Any c -> a*(b + c) :~: a*b + a*c

-- anchoring -
prpDstrR :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (a * (b + c)) :~: ((a * b) + (a * c))
prpDstrR W a
W0 Any b
_ Any c
_ = forall {k} (a :: k). a :~: a
Refl

-- hypothesis -
prpDstrR (SW W n
a) Any b
b Any c
c = forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> ((a + 1) * (b + c)) :~: (((a + 1) * b) + ((a + 1) * c))
qed W n
a Any b
b Any c
c where
  qed :: Any a -> Any b -> Any c -> (a+1)*(b + c) :~: (a+1)*b + (a+1)*c
  qed :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> ((a + 1) * (b + c)) :~: (((a + 1) * b) + ((a + 1) * c))
qed Any a
a Any b
b Any c
c = forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + 1) * (b + c)) :~: ('S a * (b + c))
r1 Any a
a Any b
b Any c
c forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b -> Any c -> ('S a * (b + c)) :~: ((b + c) + (a * (b + c)))
r2 Any a
a Any b
b Any c
c forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> ((b + c) + (a * (b + c))) :~: ((b + c) + ((a * b) + (a * c)))
hyp Any a
a Any b
b Any c
c forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> ((b + c) + ((a * b) + (a * c)))
   :~: (b + (c + ((a * b) + (a * c))))
r3 Any a
a Any b
b Any c
c forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> (b + (c + ((a * b) + (a * c))))
   :~: (b + ((a * b) + (c + (a * c))))
r4 Any a
a Any b
b Any c
c
           forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> (b + ((a * b) + (c + (a * c))))
   :~: ((b + (a * b)) + (c + (a * c)))
r5 Any a
a Any b
b Any c
c forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> ((b + (a * b)) + (c + (a * c))) :~: (('S a * b) + ('S a * c))
r6 Any a
a Any b
b Any c
c forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> (('S a * b) + ('S a * c)) :~: (((a + 1) * b) + ((a + 1) * c))
r7 Any a
a Any b
b Any c
c

  r1  :: Any a -> Any b -> Any c -> (a+1)*(b + c)          :~: S a * (b + c)
  r2  :: Any a -> Any b -> Any c -> S a * (b + c)          :~: (b + c) + a*(b + c) 
  hyp :: Any a -> Any b -> Any c -> (b + c) + a*(b + c)    :~: (b + c) + (a*b + a*c)
  r3  :: Any a -> Any b -> Any c -> (b + c) + (a*b + a*c)  :~: b + c + a*b + a*c  
  r4  :: Any a -> Any b -> Any c ->  b + c + a*b + a*c     :~: b + a*b + c + a*c
  r5  :: Any a -> Any b -> Any c ->  b + a*b + c + a*c     :~: (b + a*b) + (c + a*c) 
  r6  :: Any a -> Any b -> Any c ->  (b + a*b) + (c + a*c) :~: (S a)*b + (S a)*c
  r7  :: Any a -> Any b -> Any c ->  (S a)*b + (S a)*c     :~: (a+1)*b + (a+1)*c

  r1 :: forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + 1) * (b + c)) :~: ('S a * (b + c))
r1  Any a
_ Any b
_ Any c
_ = forall {k} (a :: k). a :~: a
Refl
  r2 :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b -> Any c -> ('S a * (b + c)) :~: ((b + c) + (a * (b + c)))
r2  Any a
_ Any b
_ Any c
_ = forall {k} (a :: k). a :~: a
Refl
  hyp :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> ((b + c) + (a * (b + c))) :~: ((b + c) + ((a * b) + (a * c)))
hyp Any a
a Any b
b Any c
c = forall {k} (a :: N') (a' :: N') (b :: k) (b' :: k).
(a :~: a') -> (b :~: b') -> (a + b) :~: (a' + b')
sbstAdd (forall (x :: N'). Any x -> x :~: x
refl (Any b
bforall (n :: N') (m :: N'). W n -> W m -> W (n + m)
++Any c
c)) (forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (a * (b + c)) :~: ((a * b) + (a * c))
prpDstrR Any a
a Any b
b Any c
c) 
  r3 :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> ((b + c) + ((a * b) + (a * c)))
   :~: (b + (c + ((a * b) + (a * c))))
r3  Any a
a Any b
b Any c
c = forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + b) + c) :~: (a + (b + c))
prpAddAssoc Any b
b Any c
c (Any a
aforall (n :: N') (m :: N'). W n -> W m -> W (n * m)
**Any b
b forall (n :: N') (m :: N'). W n -> W m -> W (n + m)
++ Any a
aforall (n :: N') (m :: N'). W n -> W m -> W (n * m)
**Any c
c)
  r4 :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> (b + (c + ((a * b) + (a * c))))
   :~: (b + ((a * b) + (c + (a * c))))
r4  Any a
a Any b
b Any c
c = forall {k} (a :: N') (a' :: N') (b :: k) (b' :: k).
(a :~: a') -> (b :~: b') -> (a + b) :~: (a' + b')
sbstAdd (forall (x :: N'). Any x -> x :~: x
refl Any b
b) forall (h :: Type -> Type -> Type) a b.
Applicative h =>
h a b -> a -> b
$ forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (a + (b + c)) :~: (b + (a + c))
lemmaAdd2 Any c
c (Any a
aforall (n :: N') (m :: N'). W n -> W m -> W (n * m)
**Any b
b) (Any a
aforall (n :: N') (m :: N'). W n -> W m -> W (n * m)
**Any c
c)
  r5 :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> (b + ((a * b) + (c + (a * c))))
   :~: ((b + (a * b)) + (c + (a * c)))
r5  Any a
a Any b
b Any c
c = forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym forall (h :: Type -> Type -> Type) a b.
Applicative h =>
h a b -> a -> b
$ forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> ((a + b) + c) :~: (a + (b + c))
prpAddAssoc Any b
b (Any a
aforall (n :: N') (m :: N'). W n -> W m -> W (n * m)
**Any b
b) (Any c
c forall (n :: N') (m :: N'). W n -> W m -> W (n + m)
++ Any a
aforall (n :: N') (m :: N'). W n -> W m -> W (n * m)
**Any c
c)
  r6 :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> ((b + (a * b)) + (c + (a * c))) :~: (('S a * b) + ('S a * c))
r6  Any a
_ Any b
_ Any c
_ = forall {k} (a :: k). a :~: a
Refl
  r7 :: forall (a :: N') (b :: N') (c :: N').
Any a
-> Any b
-> Any c
-> (('S a * b) + ('S a * c)) :~: (((a + 1) * b) + ((a + 1) * c))
r7  Any a
_ Any b
_ Any c
_ = forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- prpMltComm -

-- | multiplication is commutative.
prpMltComm :: Any a -> Any b -> a*b :~: b*a

-- anchoring -
prpMltComm :: forall (a :: N') (b :: N'). Any a -> Any b -> (a * b) :~: (b * a)
prpMltComm W a
W0 Any b
b = forall (b :: N'). Any b -> (N0 * b) :~: (b * N0)
qed Any b
b where
  qed :: Any b -> N0 * b :~: b * N0
  qed :: forall (b :: N'). Any b -> (N0 * b) :~: (b * N0)
qed Any b
b = forall (b :: N'). Any b -> (N0 * b) :~: N0
r1 Any b
b forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (b :: N'). Any b -> N0 :~: (b * N0)
r2 Any b
b

  r1  :: Any b -> N0 * b :~: N0
  r2  :: Any b -> N0     :~: b * N0

  r1 :: forall (b :: N'). Any b -> (N0 * b) :~: N0
r1 Any b
_ = forall {k} (a :: k). a :~: a
Refl
  r2 :: forall (b :: N'). Any b -> N0 :~: (b * N0)
r2 Any b
b = forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym forall (h :: Type -> Type -> Type) a b.
Applicative h =>
h a b -> a -> b
$ forall (a :: N'). Any a -> (a * N0) :~: N0
lemmaMlt1 Any b
b

-- hypothesis -
prpMltComm (SW W n
a) Any b
b = forall (a :: N') (b :: N').
Any a -> Any b -> ((a + 1) * b) :~: (b * (a + 1))
qed W n
a Any b
b where
  qed :: Any a -> Any b -> (a+1)*b :~: b*(a+1)
  qed :: forall (a :: N') (b :: N').
Any a -> Any b -> ((a + 1) * b) :~: (b * (a + 1))
qed Any a
a Any b
b =  forall (a :: N') (b :: N').
Any a -> Any b -> ((a + 1) * b) :~: ('S a * b)
r1 Any a
a Any b
b forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N').
Any a -> Any b -> ('S a * b) :~: (b + (a * b))
r2 Any a
a Any b
b forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N').
Any a -> Any b -> (b + (a * b)) :~: (b + (b * a))
hyp Any a
a Any b
b forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N').
Any a -> Any b -> (b + (b * a)) :~: ((b * N1) + (b * a))
r3 Any a
a Any b
b forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N').
Any a -> Any b -> ((b * N1) + (b * a)) :~: (b * (N1 + a))
r4 Any a
a Any b
b
          forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N').
Any a -> Any b -> (b * (N1 + a)) :~: (b * (N1 + a))
r5 Any a
a Any b
b forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N').
Any a -> Any b -> (b * (N1 + a)) :~: (b * 'S (N0 + a))
r6 Any a
a Any b
b forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N').
Any a -> Any b -> (b * 'S (N0 + a)) :~: (b * 'S a)
r7 Any a
a Any b
b forall {k} {a :: k} {b :: k} {c :: k}.
(a :~: b) -> (b :~: c) -> a :~: c
>> forall (a :: N') (b :: N').
Any a -> Any b -> (b * 'S a) :~: (b * (a + 1))
r8 Any a
a Any b
b

  r1  :: Any a -> Any b -> (a+1)*b        :~: (S a) * b
  r2  :: Any a -> Any b -> (S a) * b      :~: b + a*b
  hyp :: Any a -> Any b -> b + a*b        :~: b + b*a
  r3  :: Any a -> Any b -> b + b*a        :~: b*N1 + b*a
  r4  :: Any a -> Any b -> b*N1 + b*a     :~: b*(N1 + a)
  r5  :: Any a -> Any b -> b*(N1 + a)     :~: b*(S N0 + a)
  r6  :: Any a -> Any b -> b*(S N0 + a)   :~: b*(S (N0 + a))
  r7  :: Any a -> Any b -> b*(S (N0 + a)) :~: b*(S a) 
  r8  :: Any a -> Any b -> b*(S a)        :~: b*(a+1)

  r1 :: forall (a :: N') (b :: N').
Any a -> Any b -> ((a + 1) * b) :~: ('S a * b)
r1  Any a
_ Any b
_ = forall {k} (a :: k). a :~: a
Refl
  r2 :: forall (a :: N') (b :: N').
Any a -> Any b -> ('S a * b) :~: (b + (a * b))
r2  Any a
_ Any b
_ = forall {k} (a :: k). a :~: a
Refl
  hyp :: forall (a :: N') (b :: N').
Any a -> Any b -> (b + (a * b)) :~: (b + (b * a))
hyp Any a
a Any b
b = forall {k} (a :: N') (a' :: N') (b :: k) (b' :: k).
(a :~: a') -> (b :~: b') -> (a + b) :~: (a' + b')
sbstAdd (forall (x :: N'). Any x -> x :~: x
refl Any b
b) (forall (a :: N') (b :: N'). Any a -> Any b -> (a * b) :~: (b * a)
prpMltComm Any a
a Any b
b)
  r3 :: forall (a :: N') (b :: N').
Any a -> Any b -> (b + (b * a)) :~: ((b * N1) + (b * a))
r3  Any a
a Any b
b = forall {k} (a :: N') (a' :: N') (b :: k) (b' :: k).
(a :~: a') -> (b :~: b') -> (a + b) :~: (a' + b')
sbstAdd (forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym forall (h :: Type -> Type -> Type) a b.
Applicative h =>
h a b -> a -> b
$ forall (a :: N'). Any a -> (a * N1) :~: a
prpMltNtrlR Any b
b) (forall (x :: N'). Any x -> x :~: x
refl (Any b
bforall (n :: N') (m :: N'). W n -> W m -> W (n * m)
**Any a
a))
  r4 :: forall (a :: N') (b :: N').
Any a -> Any b -> ((b * N1) + (b * a)) :~: (b * (N1 + a))
r4  Any a
a Any b
b = forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym forall (h :: Type -> Type -> Type) a b.
Applicative h =>
h a b -> a -> b
$ forall (a :: N') (b :: N') (c :: N').
Any a -> Any b -> Any c -> (a * (b + c)) :~: ((a * b) + (a * c))
prpDstrR Any b
b W N1
w1 Any a
a 
  r5 :: forall (a :: N') (b :: N').
Any a -> Any b -> (b * (N1 + a)) :~: (b * (N1 + a))
r5  Any a
_ Any b
_ = forall {k} (a :: k). a :~: a
Refl
  r6 :: forall (a :: N') (b :: N').
Any a -> Any b -> (b * (N1 + a)) :~: (b * 'S (N0 + a))
r6  Any a
_ Any b
_ = forall {k} (a :: k). a :~: a
Refl
  r7 :: forall (a :: N') (b :: N').
Any a -> Any b -> (b * 'S (N0 + a)) :~: (b * 'S a)
r7  Any a
_ Any b
_ = forall {k} (a :: k). a :~: a
Refl
  r8 :: forall (a :: N') (b :: N').
Any a -> Any b -> (b * 'S a) :~: (b * (a + 1))
r8  Any a
_ Any b
_ = forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- codeW -

-- | @codeW n m@ generates the haskell code for the witnesses 'W' of 'N'' from @n@ to @m@.
codeW :: N -> N -> String
codeW :: N -> N -> String
codeW N
i N
n = forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join forall (h :: Type -> Type -> Type) a b.
Applicative h =>
h a b -> a -> b
$ forall a. a -> [a] -> [a]
tween String
"\n" forall (h :: Type -> Type -> Type) a b.
Applicative h =>
h a b -> a -> b
$ N -> [String]
cdn N
i where
  cdn :: N -> [String]
cdn N
0 = String
"type N0 = 'N0"
        forall a. a -> [a] -> [a]
: String
"w0 :: W N0"
        forall a. a -> [a] -> [a]
: String
"w0 = W0"
        forall a. a -> [a] -> [a]
: N -> [String]
cdn N
1
  cdn N
i | N
i forall a. Ord a => a -> a -> Bool
<= N
n    = String
cdType forall a. a -> [a] -> [a]
: String
cdDcl forall a. a -> [a] -> [a]
: String
cdDef forall a. a -> [a] -> [a]
: N -> [String]
cdn (N
i forall a. Additive a => a -> a -> a
+ N
1)
        | Bool
otherwise = []
    where i' :: N
i' = N
iN -> N -> N
>-N
1
          ++ :: [a] -> [a] -> [a]
(++) = forall a. [a] -> [a] -> [a]
(L.++)
          cdType :: String
cdType = String
"type N" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show N
i forall a. [a] -> [a] -> [a]
++ String
" = S N" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show N
i'
          cdDcl :: String
cdDcl  = String
"w" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show N
i forall a. [a] -> [a] -> [a]
++ String
" :: W N" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show N
i
          cdDef :: String
cdDef  = String
"w" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show N
i forall a. [a] -> [a] -> [a]
++ String
" = SW " forall a. [a] -> [a] -> [a]
++ String
"w" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show N
i'  

--------------------------------------------------------------------------------
-- itfW -

-- | @itfW n m@ generates the haskell interface for the witnesses 'W' from @n@ to @m@.
itfW :: N -> N -> String
itfW :: N -> N -> String
itfW N
n N
m = forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join forall (h :: Type -> Type -> Type) a b.
Applicative h =>
h a b -> a -> b
$ forall a. a -> [a] -> [a]
tween String
"\n" forall (h :: Type -> Type -> Type) a b.
Applicative h =>
h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
L.map forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join forall (h :: Type -> Type -> Type) a b.
Applicative h =>
h a b -> a -> b
$ forall {a}. [a] -> [[a]]
splt [String]
nats where
  ++ :: [a] -> [a] -> [a]
(++) = forall a. [a] -> [a] -> [a]
(L.++)
  nats :: [String]
nats = [String
", type N" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show N
i forall a. [a] -> [a] -> [a]
++ String
", w" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show N
i | N
i <- [N
n..N
m]]
  splt :: [a] -> [[a]]
splt [] = []
  splt [a]
ss = [a]
s forall a. a -> [a] -> [a]
: [a] -> [[a]]
splt [a]
ss' where
    ([a]
s,[a]
ss') = forall a. Int -> [a] -> ([a], [a])
L.splitAt Int
4 [a]
ss

----------------------------------------
-- wi -

-- | @0@.
type N0 = 'N0
w0 :: W N0
w0 :: W N0
w0 = W N0
W0

-- | @1@.
type N1 = S N0
w1 :: W N1
w1 :: W N1
w1 = forall (n :: N'). W n -> W (n + 1)
SW W N0
w0

-- | @2@.
type N2 = S N1

-- | @3@.
type N3 = S N2

-- | @4@.
type N4 = S N3

-- | @5@.
type N5 = S N4

-- | @6@.
type N6 = S N5

-- | @7@.
type N7 = S N6

-- | @8@.
type N8 = S N7

-- | @9@.
type N9 = S N8

-- | @10@.
type N10 = S N9
{-
type N0 = 'N0
w0 :: W N0
w0 = W0
type N1 = S N0
w1 :: W N1
w1 = SW w0
type N2 = S N1
w2 :: W N2
w2 = SW w1
type N3 = S N2
w3 :: W N3
w3 = SW w2
type N4 = S N3
w4 :: W N4
w4 = SW w3
type N5 = S N4
w5 :: W N5
w5 = SW w4
type N6 = S N5
w6 :: W N6
w6 = SW w5
type N7 = S N6
w7 :: W N7
w7 = SW w6
type N8 = S N7
w8 :: W N8
w8 = SW w7
type N9 = S N8
w9 :: W N9
w9 = SW w8
type N10 = S N9
w10 :: W N10
w10 = SW w9
type N11 = S N10
w11 :: W N11
w11 = SW w10
type N12 = S N11
w12 :: W N12
w12 = SW w11
type N13 = S N12
w13 :: W N13
w13 = SW w12
type N14 = S N13
w14 :: W N14
w14 = SW w13
type N15 = S N14
w15 :: W N15
w15 = SW w14
type N16 = S N15
w16 :: W N16
w16 = SW w15
type N17 = S N16
w17 :: W N17
w17 = SW w16
type N18 = S N17
w18 :: W N18
w18 = SW w17
type N19 = S N18
w19 :: W N19
w19 = SW w18
type N20 = S N19
w20 :: W N20
w20 = SW w19
type N21 = S N20
w21 :: W N21
w21 = SW w20
type N22 = S N21
w22 :: W N22
w22 = SW w21
type N23 = S N22
w23 :: W N23
w23 = SW w22
type N24 = S N23
w24 :: W N24
w24 = SW w23
type N25 = S N24
w25 :: W N25
w25 = SW w24
type N26 = S N25
w26 :: W N26
w26 = SW w25
type N27 = S N26
w27 :: W N27
w27 = SW w26
type N28 = S N27
w28 :: W N28
w28 = SW w27
type N29 = S N28
w29 :: W N29
w29 = SW w28
type N30 = S N29
w30 :: W N30
w30 = SW w29
type N31 = S N30
w31 :: W N31
w31 = SW w30
type N32 = S N31
w32 :: W N32
w32 = SW w31
type N33 = S N32
w33 :: W N33
w33 = SW w32
type N34 = S N33
w34 :: W N34
w34 = SW w33
type N35 = S N34
w35 :: W N35
w35 = SW w34
type N36 = S N35
w36 :: W N36
w36 = SW w35
type N37 = S N36
w37 :: W N37
w37 = SW w36
type N38 = S N37
w38 :: W N38
w38 = SW w37
type N39 = S N38
w39 :: W N39
w39 = SW w38
type N40 = S N39
w40 :: W N40
w40 = SW w39
type N41 = S N40
w41 :: W N41
w41 = SW w40
type N42 = S N41
w42 :: W N42
w42 = SW w41
type N43 = S N42
w43 :: W N43
w43 = SW w42
type N44 = S N43
w44 :: W N44
w44 = SW w43
type N45 = S N44
w45 :: W N45
w45 = SW w44
type N46 = S N45
w46 :: W N46
w46 = SW w45
type N47 = S N46
w47 :: W N47
w47 = SW w46
type N48 = S N47
w48 :: W N48
w48 = SW w47
type N49 = S N48
w49 :: W N49
w49 = SW w48
type N50 = S N49
w50 :: W N50
w50 = SW w49
type N51 = S N50
w51 :: W N51
w51 = SW w50
type N52 = S N51
w52 :: W N52
w52 = SW w51
type N53 = S N52
w53 :: W N53
w53 = SW w52
type N54 = S N53
w54 :: W N54
w54 = SW w53
type N55 = S N54
w55 :: W N55
w55 = SW w54
type N56 = S N55
w56 :: W N56
w56 = SW w55
type N57 = S N56
w57 :: W N57
w57 = SW w56
type N58 = S N57
w58 :: W N58
w58 = SW w57
type N59 = S N58
w59 :: W N59
w59 = SW w58
type N60 = S N59
w60 :: W N60
w60 = SW w59
type N61 = S N60
w61 :: W N61
w61 = SW w60
type N62 = S N61
w62 :: W N62
w62 = SW w61
type N63 = S N62
w63 :: W N63
w63 = SW w62
-}