{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE FlexibleContexts #-}
module Type.Data.Num.Unary.Proof (
    Nat(..), Pos(..),
    natFromPos,
    addNat, addPosL, addPosR,
    AddZeroL(..), addZeroL,
    AddComm(..), addComm,
    AddAssoc(..), addAssoc,
    mulNat, mulPos,
    ) where

import Type.Data.Num.Unary
          (Natural, Positive, Zero, Succ, switchNat, switchPos, (:+:), (:*:))

data Nat x = Natural x => Nat
data Pos x = Positive x => Pos


succNat :: Nat x -> Nat (Succ x)
succNat :: Nat x -> Nat (Succ x)
succNat Nat x
Nat = Nat (Succ x)
forall x. Natural x => Nat x
Nat

prevNat :: (Natural x) => Nat (Succ x) -> Nat x
prevNat :: Nat (Succ x) -> Nat x
prevNat Nat (Succ x)
Nat = Nat x
forall x. Natural x => Nat x
Nat

posSucc :: Nat x -> Pos (Succ x)
posSucc :: Nat x -> Pos (Succ x)
posSucc Nat x
Nat = Pos (Succ x)
forall x. Positive x => Pos x
Pos

prevPos :: (Natural x) => Pos (Succ x) -> Nat x
prevPos :: Pos (Succ x) -> Nat x
prevPos Pos (Succ x)
Pos = Nat x
forall x. Natural x => Nat x
Nat


natFromPos :: Pos x -> Nat x
natFromPos :: Pos x -> Nat x
natFromPos Pos x
Pos = Nat x
forall x. Natural x => Nat x
Nat


newtype
   QuantifiedAdd condx condy prop x y =
      QuantifiedAdd {QuantifiedAdd condx condy prop x y
-> condx x -> condy y -> prop (x :+: y)
runQuantifiedAdd :: condx x -> condy y -> prop (x :+: y)}

addNat :: Nat x -> Nat y -> Nat (x :+: y)
addNat :: Nat x -> Nat y -> Nat (x :+: y)
addNat Nat x
x0 y0 :: Nat y
y0@Nat y
Nat =
   QuantifiedAdd Nat Nat Nat x y -> Nat x -> Nat y -> Nat (x :+: y)
forall (condx :: * -> *) (condy :: * -> *) (prop :: * -> *) x y.
QuantifiedAdd condx condy prop x y
-> condx x -> condy y -> prop (x :+: y)
runQuantifiedAdd
      (QuantifiedAdd Nat Nat Nat x Zero
-> (forall m. Natural m => QuantifiedAdd Nat Nat Nat x (Succ m))
-> QuantifiedAdd Nat Nat Nat x y
forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
switchNat
         ((Nat x -> Nat Zero -> Nat (x :+: Zero))
-> QuantifiedAdd Nat Nat Nat x Zero
forall (condx :: * -> *) (condy :: * -> *) (prop :: * -> *) x y.
(condx x -> condy y -> prop (x :+: y))
-> QuantifiedAdd condx condy prop x y
QuantifiedAdd Nat x -> Nat Zero -> Nat (x :+: Zero)
forall a b. a -> b -> a
const)
         ((Nat x -> Nat (Succ m) -> Nat (x :+: Succ m))
-> QuantifiedAdd Nat Nat Nat x (Succ m)
forall (condx :: * -> *) (condy :: * -> *) (prop :: * -> *) x y.
(condx x -> condy y -> prop (x :+: y))
-> QuantifiedAdd condx condy prop x y
QuantifiedAdd ((Nat x -> Nat (Succ m) -> Nat (x :+: Succ m))
 -> QuantifiedAdd Nat Nat Nat x (Succ m))
-> (Nat x -> Nat (Succ m) -> Nat (x :+: Succ m))
-> QuantifiedAdd Nat Nat Nat x (Succ m)
forall a b. (a -> b) -> a -> b
$ \Nat x
x -> Nat (x :+: m) -> Nat (Succ (x :+: m))
forall x. Nat x -> Nat (Succ x)
succNat (Nat (x :+: m) -> Nat (Succ (x :+: m)))
-> (Nat (Succ m) -> Nat (x :+: m))
-> Nat (Succ m)
-> Nat (Succ (x :+: m))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat x -> Nat m -> Nat (x :+: m)
forall x y. Nat x -> Nat y -> Nat (x :+: y)
addNat Nat x
x (Nat m -> Nat (x :+: m))
-> (Nat (Succ m) -> Nat m) -> Nat (Succ m) -> Nat (x :+: m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat (Succ m) -> Nat m
forall x. Natural x => Nat (Succ x) -> Nat x
prevNat))
      Nat x
x0 Nat y
y0

addPosR :: Nat x -> Pos y -> Pos (x :+: y)
addPosR :: Nat x -> Pos y -> Pos (x :+: y)
addPosR Nat x
x0 y0 :: Pos y
y0@Pos y
Pos =
   QuantifiedAdd Nat Pos Pos x y -> Nat x -> Pos y -> Pos (x :+: y)
forall (condx :: * -> *) (condy :: * -> *) (prop :: * -> *) x y.
QuantifiedAdd condx condy prop x y
-> condx x -> condy y -> prop (x :+: y)
runQuantifiedAdd
      ((forall m. Natural m => QuantifiedAdd Nat Pos Pos x (Succ m))
-> QuantifiedAdd Nat Pos Pos x y
forall n (f :: * -> *).
Positive n =>
(forall m. Natural m => f (Succ m)) -> f n
switchPos ((Nat x -> Pos (Succ m) -> Pos (x :+: Succ m))
-> QuantifiedAdd Nat Pos Pos x (Succ m)
forall (condx :: * -> *) (condy :: * -> *) (prop :: * -> *) x y.
(condx x -> condy y -> prop (x :+: y))
-> QuantifiedAdd condx condy prop x y
QuantifiedAdd ((Nat x -> Pos (Succ m) -> Pos (x :+: Succ m))
 -> QuantifiedAdd Nat Pos Pos x (Succ m))
-> (Nat x -> Pos (Succ m) -> Pos (x :+: Succ m))
-> QuantifiedAdd Nat Pos Pos x (Succ m)
forall a b. (a -> b) -> a -> b
$ \Nat x
x -> Nat (x :+: m) -> Pos (Succ (x :+: m))
forall x. Nat x -> Pos (Succ x)
posSucc (Nat (x :+: m) -> Pos (Succ (x :+: m)))
-> (Pos (Succ m) -> Nat (x :+: m))
-> Pos (Succ m)
-> Pos (Succ (x :+: m))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat x -> Nat m -> Nat (x :+: m)
forall x y. Nat x -> Nat y -> Nat (x :+: y)
addNat Nat x
x (Nat m -> Nat (x :+: m))
-> (Pos (Succ m) -> Nat m) -> Pos (Succ m) -> Nat (x :+: m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pos (Succ m) -> Nat m
forall x. Natural x => Pos (Succ x) -> Nat x
prevPos))
      Nat x
x0 Pos y
y0

addPosL :: Pos x -> Nat y -> Pos (x :+: y)
addPosL :: Pos x -> Nat y -> Pos (x :+: y)
addPosL Pos x
x0 y0 :: Nat y
y0@Nat y
Nat =
   QuantifiedAdd Pos Nat Pos x y -> Pos x -> Nat y -> Pos (x :+: y)
forall (condx :: * -> *) (condy :: * -> *) (prop :: * -> *) x y.
QuantifiedAdd condx condy prop x y
-> condx x -> condy y -> prop (x :+: y)
runQuantifiedAdd
      (QuantifiedAdd Pos Nat Pos x Zero
-> (forall m. Natural m => QuantifiedAdd Pos Nat Pos x (Succ m))
-> QuantifiedAdd Pos Nat Pos x y
forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
switchNat
         ((Pos x -> Nat Zero -> Pos (x :+: Zero))
-> QuantifiedAdd Pos Nat Pos x Zero
forall (condx :: * -> *) (condy :: * -> *) (prop :: * -> *) x y.
(condx x -> condy y -> prop (x :+: y))
-> QuantifiedAdd condx condy prop x y
QuantifiedAdd Pos x -> Nat Zero -> Pos (x :+: Zero)
forall a b. a -> b -> a
const)
         ((Pos x -> Nat (Succ m) -> Pos (x :+: Succ m))
-> QuantifiedAdd Pos Nat Pos x (Succ m)
forall (condx :: * -> *) (condy :: * -> *) (prop :: * -> *) x y.
(condx x -> condy y -> prop (x :+: y))
-> QuantifiedAdd condx condy prop x y
QuantifiedAdd ((Pos x -> Nat (Succ m) -> Pos (x :+: Succ m))
 -> QuantifiedAdd Pos Nat Pos x (Succ m))
-> (Pos x -> Nat (Succ m) -> Pos (x :+: Succ m))
-> QuantifiedAdd Pos Nat Pos x (Succ m)
forall a b. (a -> b) -> a -> b
$ \Pos x
x -> Nat (x :+: m) -> Pos (Succ (x :+: m))
forall x. Nat x -> Pos (Succ x)
posSucc (Nat (x :+: m) -> Pos (Succ (x :+: m)))
-> (Nat (Succ m) -> Nat (x :+: m))
-> Nat (Succ m)
-> Pos (Succ (x :+: m))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat x -> Nat m -> Nat (x :+: m)
forall x y. Nat x -> Nat y -> Nat (x :+: y)
addNat (Pos x -> Nat x
forall x. Pos x -> Nat x
natFromPos Pos x
x) (Nat m -> Nat (x :+: m))
-> (Nat (Succ m) -> Nat m) -> Nat (Succ m) -> Nat (x :+: m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat (Succ m) -> Nat m
forall x. Natural x => Nat (Succ x) -> Nat x
prevNat))
      Pos x
x0 Nat y
y0


newtype Quantified prop x = Quantified {Quantified prop x -> Nat x -> prop x
runQuantified :: Nat x -> prop x}

induction ::
   quant Zero -> (forall x. Nat x -> quant (Succ x)) ->
   Nat y -> quant y
induction :: quant Zero
-> (forall x. Nat x -> quant (Succ x)) -> Nat y -> quant y
induction quant Zero
base forall x. Nat x -> quant (Succ x)
step y :: Nat y
y@Nat y
Nat =
   Quantified quant y -> Nat y -> quant y
forall (prop :: * -> *) x. Quantified prop x -> Nat x -> prop x
runQuantified
      (Quantified quant Zero
-> (forall m. Natural m => Quantified quant (Succ m))
-> Quantified quant y
forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
switchNat
         ((Nat Zero -> quant Zero) -> Quantified quant Zero
forall (prop :: * -> *) x. (Nat x -> prop x) -> Quantified prop x
Quantified ((Nat Zero -> quant Zero) -> Quantified quant Zero)
-> (Nat Zero -> quant Zero) -> Quantified quant Zero
forall a b. (a -> b) -> a -> b
$ quant Zero -> Nat Zero -> quant Zero
forall a b. a -> b -> a
const quant Zero
base)
         ((Nat (Succ m) -> quant (Succ m)) -> Quantified quant (Succ m)
forall (prop :: * -> *) x. (Nat x -> prop x) -> Quantified prop x
Quantified ((Nat (Succ m) -> quant (Succ m)) -> Quantified quant (Succ m))
-> (Nat (Succ m) -> quant (Succ m)) -> Quantified quant (Succ m)
forall a b. (a -> b) -> a -> b
$ Nat m -> quant (Succ m)
forall x. Nat x -> quant (Succ x)
step (Nat m -> quant (Succ m))
-> (Nat (Succ m) -> Nat m) -> Nat (Succ m) -> quant (Succ m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat (Succ m) -> Nat m
forall x. Natural x => Nat (Succ x) -> Nat x
prevNat))
      Nat y
y


data AddZeroL x = (Zero:+:x) ~ x => AddZeroL

succZeroL :: AddZeroL x -> AddZeroL (Succ x)
succZeroL :: AddZeroL x -> AddZeroL (Succ x)
succZeroL AddZeroL x
AddZeroL = AddZeroL (Succ x)
forall x. ((Zero :+: x) ~ x) => AddZeroL x
AddZeroL

addZeroL :: Nat x -> AddZeroL x
addZeroL :: Nat x -> AddZeroL x
addZeroL = AddZeroL Zero
-> (forall x. Nat x -> AddZeroL (Succ x)) -> Nat x -> AddZeroL x
forall (quant :: * -> *) y.
quant Zero
-> (forall x. Nat x -> quant (Succ x)) -> Nat y -> quant y
induction AddZeroL Zero
forall x. ((Zero :+: x) ~ x) => AddZeroL x
AddZeroL (AddZeroL x -> AddZeroL (Succ x)
forall x. AddZeroL x -> AddZeroL (Succ x)
succZeroL (AddZeroL x -> AddZeroL (Succ x))
-> (Nat x -> AddZeroL x) -> Nat x -> AddZeroL (Succ x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat x -> AddZeroL x
forall x. Nat x -> AddZeroL x
addZeroL)


{-
induction step:

Succ x :+: Succ y
Succ (x :+: Succ y)
Succ (Succ (x:+:y))
Succ (Succ x :+: y)
-}
data AddSuccL x y = (Succ x :+: y) ~ Succ (x:+:y) => AddSuccL

succSuccL :: AddSuccL x y -> AddSuccL x (Succ y)
succSuccL :: AddSuccL x y -> AddSuccL x (Succ y)
succSuccL AddSuccL x y
AddSuccL = AddSuccL x (Succ y)
forall x y. ((Succ x :+: y) ~ Succ (x :+: y)) => AddSuccL x y
AddSuccL

addSuccL :: Nat x -> Nat y -> AddSuccL x y
addSuccL :: Nat x -> Nat y -> AddSuccL x y
addSuccL Nat x
x =
   AddSuccL x Zero
-> (forall x. Nat x -> AddSuccL x (Succ x))
-> Nat y
-> AddSuccL x y
forall (quant :: * -> *) y.
quant Zero
-> (forall x. Nat x -> quant (Succ x)) -> Nat y -> quant y
induction
      (case Nat x -> AddZeroL x
forall x. Nat x -> AddZeroL x
addZeroL Nat x
x of AddZeroL x
AddZeroL -> AddSuccL x Zero
forall x y. ((Succ x :+: y) ~ Succ (x :+: y)) => AddSuccL x y
AddSuccL)
      (AddSuccL x x -> AddSuccL x (Succ x)
forall x y. AddSuccL x y -> AddSuccL x (Succ y)
succSuccL (AddSuccL x x -> AddSuccL x (Succ x))
-> (Nat x -> AddSuccL x x) -> Nat x -> AddSuccL x (Succ x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat x -> Nat x -> AddSuccL x x
forall x y. Nat x -> Nat y -> AddSuccL x y
addSuccL Nat x
x)


{-
induction step:

y :+: Succ x
Succ (y :+: x)
Succ (x :+: y)
Succ x :+: y
-}
data AddComm x y = (x:+:y) ~ (y:+:x) => AddComm

succComm :: Nat x -> Nat y -> AddComm x y -> AddComm x (Succ y)
succComm :: Nat x -> Nat y -> AddComm x y -> AddComm x (Succ y)
succComm Nat x
x Nat y
y AddComm x y
AddComm = case Nat y -> Nat x -> AddSuccL y x
forall x y. Nat x -> Nat y -> AddSuccL x y
addSuccL Nat y
y Nat x
x of AddSuccL y x
AddSuccL -> AddComm x (Succ y)
forall x y. ((x :+: y) ~ (y :+: x)) => AddComm x y
AddComm

{- |
The proof is pretty expensive.
For proving (x:+:y ~ y:+:x) we need about @x*y@ reduction steps.
-}
addComm :: Nat x -> Nat y -> AddComm x y
addComm :: Nat x -> Nat y -> AddComm x y
addComm Nat x
x =
   AddComm x Zero
-> (forall x. Nat x -> AddComm x (Succ x)) -> Nat y -> AddComm x y
forall (quant :: * -> *) y.
quant Zero
-> (forall x. Nat x -> quant (Succ x)) -> Nat y -> quant y
induction
      (case Nat x -> AddZeroL x
forall x. Nat x -> AddZeroL x
addZeroL Nat x
x of AddZeroL x
AddZeroL -> AddComm x Zero
forall x y. ((x :+: y) ~ (y :+: x)) => AddComm x y
AddComm)
      (\Nat x
y -> Nat x -> Nat x -> AddComm x x -> AddComm x (Succ x)
forall x y. Nat x -> Nat y -> AddComm x y -> AddComm x (Succ y)
succComm Nat x
x Nat x
y (AddComm x x -> AddComm x (Succ x))
-> AddComm x x -> AddComm x (Succ x)
forall a b. (a -> b) -> a -> b
$ Nat x -> Nat x -> AddComm x x
forall x y. Nat x -> Nat y -> AddComm x y
addComm Nat x
x Nat x
y)


{-
induction step:

x :+: (y :+: Succ z)
x :+: Succ (y :+: z)
Succ (x :+: (y :+: z))
Succ ((x :+: y) :+: z)
(x :+: y) :+: Succ z
-}
data AddAssoc x y z = (x:+:(y:+:z)) ~ ((x:+:y):+:z) => AddAssoc

succAssoc :: AddAssoc x y z -> AddAssoc x y (Succ z)
succAssoc :: AddAssoc x y z -> AddAssoc x y (Succ z)
succAssoc AddAssoc x y z
AddAssoc = AddAssoc x y (Succ z)
forall x y z.
((x :+: (y :+: z)) ~ ((x :+: y) :+: z)) =>
AddAssoc x y z
AddAssoc

addAssoc :: Nat x -> Nat y -> Nat z -> AddAssoc x y z
addAssoc :: Nat x -> Nat y -> Nat z -> AddAssoc x y z
addAssoc Nat x
x Nat y
y = AddAssoc x y Zero
-> (forall x. Nat x -> AddAssoc x y (Succ x))
-> Nat z
-> AddAssoc x y z
forall (quant :: * -> *) y.
quant Zero
-> (forall x. Nat x -> quant (Succ x)) -> Nat y -> quant y
induction AddAssoc x y Zero
forall x y z.
((x :+: (y :+: z)) ~ ((x :+: y) :+: z)) =>
AddAssoc x y z
AddAssoc (AddAssoc x y x -> AddAssoc x y (Succ x)
forall x y z. AddAssoc x y z -> AddAssoc x y (Succ z)
succAssoc (AddAssoc x y x -> AddAssoc x y (Succ x))
-> (Nat x -> AddAssoc x y x) -> Nat x -> AddAssoc x y (Succ x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat x -> Nat y -> Nat x -> AddAssoc x y x
forall x y z. Nat x -> Nat y -> Nat z -> AddAssoc x y z
addAssoc Nat x
x Nat y
y)


newtype
   QuantifiedMul condx condy prop x y =
      QuantifiedMul {QuantifiedMul condx condy prop x y
-> condx x -> condy y -> prop (x :*: y)
runQuantifiedMul :: condx x -> condy y -> prop (x :*: y)}

mulNat :: Nat x -> Nat y -> Nat (x :*: y)
mulNat :: Nat x -> Nat y -> Nat (x :*: y)
mulNat Nat x
x0 y0 :: Nat y
y0@Nat y
Nat =
   QuantifiedMul Nat Nat Nat x y -> Nat x -> Nat y -> Nat (x :*: y)
forall (condx :: * -> *) (condy :: * -> *) (prop :: * -> *) x y.
QuantifiedMul condx condy prop x y
-> condx x -> condy y -> prop (x :*: y)
runQuantifiedMul
      (QuantifiedMul Nat Nat Nat x Zero
-> (forall m. Natural m => QuantifiedMul Nat Nat Nat x (Succ m))
-> QuantifiedMul Nat Nat Nat x y
forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
switchNat
         ((Nat x -> Nat Zero -> Nat (x :*: Zero))
-> QuantifiedMul Nat Nat Nat x Zero
forall (condx :: * -> *) (condy :: * -> *) (prop :: * -> *) x y.
(condx x -> condy y -> prop (x :*: y))
-> QuantifiedMul condx condy prop x y
QuantifiedMul ((Nat x -> Nat Zero -> Nat (x :*: Zero))
 -> QuantifiedMul Nat Nat Nat x Zero)
-> (Nat x -> Nat Zero -> Nat (x :*: Zero))
-> QuantifiedMul Nat Nat Nat x Zero
forall a b. (a -> b) -> a -> b
$ \Nat x
Nat Nat Zero
Nat -> Nat (x :*: Zero)
forall x. Natural x => Nat x
Nat)
         ((Nat x -> Nat (Succ m) -> Nat (x :*: Succ m))
-> QuantifiedMul Nat Nat Nat x (Succ m)
forall (condx :: * -> *) (condy :: * -> *) (prop :: * -> *) x y.
(condx x -> condy y -> prop (x :*: y))
-> QuantifiedMul condx condy prop x y
QuantifiedMul ((Nat x -> Nat (Succ m) -> Nat (x :*: Succ m))
 -> QuantifiedMul Nat Nat Nat x (Succ m))
-> (Nat x -> Nat (Succ m) -> Nat (x :*: Succ m))
-> QuantifiedMul Nat Nat Nat x (Succ m)
forall a b. (a -> b) -> a -> b
$ \Nat x
x -> Nat x -> Nat (x :*: m) -> Nat (x :+: (x :*: m))
forall x y. Nat x -> Nat y -> Nat (x :+: y)
addNat Nat x
x (Nat (x :*: m) -> Nat (x :+: (x :*: m)))
-> (Nat (Succ m) -> Nat (x :*: m))
-> Nat (Succ m)
-> Nat (x :+: (x :*: m))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat x -> Nat m -> Nat (x :*: m)
forall x y. Nat x -> Nat y -> Nat (x :*: y)
mulNat Nat x
x (Nat m -> Nat (x :*: m))
-> (Nat (Succ m) -> Nat m) -> Nat (Succ m) -> Nat (x :*: m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat (Succ m) -> Nat m
forall x. Natural x => Nat (Succ x) -> Nat x
prevNat))
      Nat x
x0 Nat y
y0

mulPos :: Pos x -> Pos y -> Pos (x :*: y)
mulPos :: Pos x -> Pos y -> Pos (x :*: y)
mulPos Pos x
x0 y0 :: Pos y
y0@Pos y
Pos =
   QuantifiedMul Pos Pos Pos x y -> Pos x -> Pos y -> Pos (x :*: y)
forall (condx :: * -> *) (condy :: * -> *) (prop :: * -> *) x y.
QuantifiedMul condx condy prop x y
-> condx x -> condy y -> prop (x :*: y)
runQuantifiedMul
      ((forall m. Natural m => QuantifiedMul Pos Pos Pos x (Succ m))
-> QuantifiedMul Pos Pos Pos x y
forall n (f :: * -> *).
Positive n =>
(forall m. Natural m => f (Succ m)) -> f n
switchPos
         ((Pos x -> Pos (Succ m) -> Pos (x :*: Succ m))
-> QuantifiedMul Pos Pos Pos x (Succ m)
forall (condx :: * -> *) (condy :: * -> *) (prop :: * -> *) x y.
(condx x -> condy y -> prop (x :*: y))
-> QuantifiedMul condx condy prop x y
QuantifiedMul ((Pos x -> Pos (Succ m) -> Pos (x :*: Succ m))
 -> QuantifiedMul Pos Pos Pos x (Succ m))
-> (Pos x -> Pos (Succ m) -> Pos (x :*: Succ m))
-> QuantifiedMul Pos Pos Pos x (Succ m)
forall a b. (a -> b) -> a -> b
$ \Pos x
x -> Pos x -> Nat (x :*: m) -> Pos (x :+: (x :*: m))
forall x y. Pos x -> Nat y -> Pos (x :+: y)
addPosL Pos x
x (Nat (x :*: m) -> Pos (x :+: (x :*: m)))
-> (Pos (Succ m) -> Nat (x :*: m))
-> Pos (Succ m)
-> Pos (x :+: (x :*: m))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat x -> Nat m -> Nat (x :*: m)
forall x y. Nat x -> Nat y -> Nat (x :*: y)
mulNat (Pos x -> Nat x
forall x. Pos x -> Nat x
natFromPos Pos x
x) (Nat m -> Nat (x :*: m))
-> (Pos (Succ m) -> Nat m) -> Pos (Succ m) -> Nat (x :*: m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pos (Succ m) -> Nat m
forall x. Natural x => Pos (Succ x) -> Nat x
prevPos))
      Pos x
x0 Pos y
y0