{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
module Data.Array.Nested.Lemmas where

import Data.Proxy
import Data.Type.Equality
import GHC.TypeLits

import Data.Array.Nested.Mixed.Shape
import Data.Array.Nested.Permutation
import Data.Array.Nested.Shaped.Shape
import Data.Array.Nested.Types


-- * Lemmas about numbers and lists

-- ** Nat

lemLeqSuccSucc :: k + 1 <= n => Proxy k -> Proxy n -> (k <=? n - 1) :~: True
lemLeqSuccSucc :: forall (k :: Natural) (n :: Natural).
((k + 1) <= n) =>
Proxy k -> Proxy n -> (k <=? (n - 1)) :~: 'True
lemLeqSuccSucc Proxy k
_ Proxy n
_ = OrdCond (CmpNat k (n - 1)) 'True 'True 'False :~: 'True
OrdCond (Compare k (n - 1)) 'True 'True 'False :~: 'True
forall {k} (a :: k) (b :: k). a :~: b
unsafeCoerceRefl

lemLeqPlus :: n <= m => Proxy n -> Proxy m -> Proxy k -> (n <=? (m + k)) :~: 'True
lemLeqPlus :: forall (n :: Natural) (m :: Natural) (k :: Natural).
(n <= m) =>
Proxy n -> Proxy m -> Proxy k -> (n <=? (m + k)) :~: 'True
lemLeqPlus Proxy n
_ Proxy m
_ Proxy k
_ = 'True :~: 'True
OrdCond (Compare n (m + k)) 'True 'True 'False :~: 'True
forall {k} (a :: k). a :~: a
Refl

-- ** Append

lemAppNil :: l ++ '[] :~: l
lemAppNil :: forall {a} (l :: [a]). (l ++ '[]) :~: l
lemAppNil = (l ++ '[]) :~: l
forall {k} (a :: k) (b :: k). a :~: b
unsafeCoerceRefl

lemAppAssoc :: Proxy a -> Proxy b -> Proxy c -> (a ++ b) ++ c :~: a ++ (b ++ c)
lemAppAssoc :: forall {a} (a :: [a]) (b :: [a]) (c :: [a]).
Proxy a
-> Proxy b -> Proxy c -> ((a ++ b) ++ c) :~: (a ++ (b ++ c))
lemAppAssoc Proxy a
_ Proxy b
_ Proxy c
_ = ((a ++ b) ++ c) :~: (a ++ (b ++ c))
forall {k} (a :: k) (b :: k). a :~: b
unsafeCoerceRefl

lemAppLeft :: Proxy l -> a :~: b -> a ++ l :~: b ++ l
lemAppLeft :: forall {a} (l :: [a]) (a :: [a]) (b :: [a]).
Proxy l -> (a :~: b) -> (a ++ l) :~: (b ++ l)
lemAppLeft Proxy l
_ a :~: b
Refl = (a ++ l) :~: (a ++ l)
(a ++ l) :~: (b ++ l)
forall {k} (a :: k). a :~: a
Refl

-- ** Simple type families

lemReplicatePlusApp :: forall n m a. SNat n -> Proxy m -> Proxy a
                    -> Replicate (n + m) a :~: Replicate n a ++ Replicate m a
lemReplicatePlusApp :: forall {a} (n :: Natural) (m :: Natural) (a :: a).
SNat n
-> Proxy m
-> Proxy a
-> Replicate (n + m) a :~: (Replicate n a ++ Replicate m a)
lemReplicatePlusApp SNat n
sn Proxy m
_ Proxy a
_ = SNat n -> Replicate (n + m) a :~: (Replicate n a ++ Replicate m a)
forall (n' :: Natural).
SNat n'
-> Replicate (n' + m) a :~: (Replicate n' a ++ Replicate m a)
go SNat n
sn
  where
    go :: SNat n' -> Replicate (n' + m) a :~: Replicate n' a ++ Replicate m a
    go :: forall (n' :: Natural).
SNat n'
-> Replicate (n' + m) a :~: (Replicate n' a ++ Replicate m a)
go SNat n'
SZ = Replicate m a :~: Replicate m a
Replicate (n' + m) a :~: (Replicate n' a ++ Replicate m a)
forall {k} (a :: k). a :~: a
Refl
    go (SS (SNat n
n :: SNat n'm1))
      | (a : Replicate n a) :~: Replicate (n + 1) a
Refl <- forall (a2 :: a) (n :: Natural).
(a2 : Replicate n a2) :~: Replicate (n + 1) a2
forall {a1} (a2 :: a1) (n :: Natural).
(a2 : Replicate n a2) :~: Replicate (n + 1) a2
lemReplicateSucc @a @n'm1
      , Replicate (n + m) a :~: (Replicate n a ++ Replicate m a)
Refl <- SNat n -> Replicate (n + m) a :~: (Replicate n a ++ Replicate m a)
forall (n' :: Natural).
SNat n'
-> Replicate (n' + m) a :~: (Replicate n' a ++ Replicate m a)
go SNat n
n
      = ((a : Replicate (n + m) a) :~: Replicate (n' + m) a)
-> Replicate (n' + m) a :~: (a : Replicate (n + m) a)
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (forall (a2 :: a) (n :: Natural).
(a2 : Replicate n a2) :~: Replicate (n + 1) a2
forall {a1} (a2 :: a1) (n :: Natural).
(a2 : Replicate n a2) :~: Replicate (n + 1) a2
lemReplicateSucc @a @(n'm1 + m))

lemDropLenApp :: Rank l1 <= Rank l2
              => Proxy l1 -> Proxy l2 -> Proxy rest
              -> DropLen l1 l2 ++ rest :~: DropLen l1 (l2 ++ rest)
lemDropLenApp :: forall {a1} {a} (l1 :: [a1]) (l2 :: [a]) (rest :: [a]).
(Rank l1 <= Rank l2) =>
Proxy l1
-> Proxy l2
-> Proxy rest
-> (DropLen l1 l2 ++ rest) :~: DropLen l1 (l2 ++ rest)
lemDropLenApp Proxy l1
_ Proxy l2
_ Proxy rest
_ = (DropLen l1 l2 ++ rest) :~: DropLen l1 (l2 ++ rest)
forall {k} (a :: k) (b :: k). a :~: b
unsafeCoerceRefl

lemTakeLenApp :: Rank l1 <= Rank l2
              => Proxy l1 -> Proxy l2 -> Proxy rest
              -> TakeLen l1 l2 :~: TakeLen l1 (l2 ++ rest)
lemTakeLenApp :: forall {a1} {a} (l1 :: [a1]) (l2 :: [a]) (rest :: [a]).
(Rank l1 <= Rank l2) =>
Proxy l1
-> Proxy l2
-> Proxy rest
-> TakeLen l1 l2 :~: TakeLen l1 (l2 ++ rest)
lemTakeLenApp Proxy l1
_ Proxy l2
_ Proxy rest
_ = TakeLen l1 l2 :~: TakeLen l1 (l2 ++ rest)
forall {k} (a :: k) (b :: k). a :~: b
unsafeCoerceRefl

lemInitApp :: Proxy l -> Proxy x -> Init (l ++ '[x]) :~: l
lemInitApp :: forall {a} (l :: [a]) (x :: a).
Proxy l -> Proxy x -> Init (l ++ '[x]) :~: l
lemInitApp Proxy l
_ Proxy x
_ = Init (l ++ '[x]) :~: l
forall {k} (a :: k) (b :: k). a :~: b
unsafeCoerceRefl

lemLastApp :: Proxy l -> Proxy x -> Last (l ++ '[x]) :~: x
lemLastApp :: forall {k} (l :: [k]) (x :: k).
Proxy l -> Proxy x -> Last (l ++ '[x]) :~: x
lemLastApp Proxy l
_ Proxy x
_ = Last (l ++ '[x]) :~: x
forall {k} (a :: k) (b :: k). a :~: b
unsafeCoerceRefl


-- ** KnownNat

lemKnownNatSucc :: KnownNat n => Dict KnownNat (n + 1)
lemKnownNatSucc :: forall (n :: Natural). KnownNat n => Dict KnownNat (n + 1)
lemKnownNatSucc = Dict KnownNat (n + 1)
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict

lemKnownNatRank :: ShX sh i -> Dict KnownNat (Rank sh)
lemKnownNatRank :: forall (sh :: [Maybe Natural]) i.
ShX sh i -> Dict KnownNat (Rank sh)
lemKnownNatRank ShX sh i
ZSX = Dict KnownNat 0
Dict KnownNat (Rank sh)
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
lemKnownNatRank (SMayNat i SNat n
_ :$% ShX sh i
sh) | Dict KnownNat (Rank sh)
Dict <- ShX sh i -> Dict KnownNat (Rank sh)
forall (sh :: [Maybe Natural]) i.
ShX sh i -> Dict KnownNat (Rank sh)
lemKnownNatRank ShX sh i
sh = Dict KnownNat (Rank sh + 1)
Dict KnownNat (Rank sh)
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict

lemKnownNatRankSSX :: StaticShX sh -> Dict KnownNat (Rank sh)
lemKnownNatRankSSX :: forall (sh :: [Maybe Natural]).
StaticShX sh -> Dict KnownNat (Rank sh)
lemKnownNatRankSSX StaticShX sh
ZKX = Dict KnownNat 0
Dict KnownNat (Rank sh)
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
lemKnownNatRankSSX (SMayNat () SNat n
_ :!% StaticShX sh
ssh) | Dict KnownNat (Rank sh)
Dict <- StaticShX sh -> Dict KnownNat (Rank sh)
forall (sh :: [Maybe Natural]).
StaticShX sh -> Dict KnownNat (Rank sh)
lemKnownNatRankSSX StaticShX sh
ssh = Dict KnownNat (Rank sh + 1)
Dict KnownNat (Rank sh)
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict


-- * Lemmas about shapes

-- ** Known shapes

lemKnownReplicate :: SNat n -> Dict KnownShX (Replicate n Nothing)
lemKnownReplicate :: forall (n :: Natural).
SNat n -> Dict KnownShX (Replicate n 'Nothing)
lemKnownReplicate SNat n
sn = StaticShX (Replicate n 'Nothing)
-> Dict KnownShX (Replicate n 'Nothing)
forall (sh :: [Maybe Natural]). StaticShX sh -> Dict KnownShX sh
lemKnownShX (SNat n -> StaticShX (Replicate n 'Nothing)
forall (n :: Natural). SNat n -> StaticShX (Replicate n 'Nothing)
ssxFromSNat SNat n
sn)

lemKnownShX :: StaticShX sh -> Dict KnownShX sh
lemKnownShX :: forall (sh :: [Maybe Natural]). StaticShX sh -> Dict KnownShX sh
lemKnownShX StaticShX sh
ZKX = Dict KnownShX sh
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
lemKnownShX (SKnown SNat n1
SNat :!% StaticShX sh
ssh) | Dict KnownShX sh
Dict <- StaticShX sh -> Dict KnownShX sh
forall (sh :: [Maybe Natural]). StaticShX sh -> Dict KnownShX sh
lemKnownShX StaticShX sh
ssh = Dict KnownShX sh
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
lemKnownShX (SUnknown () :!% StaticShX sh
ssh) | Dict KnownShX sh
Dict <- StaticShX sh -> Dict KnownShX sh
forall (sh :: [Maybe Natural]). StaticShX sh -> Dict KnownShX sh
lemKnownShX StaticShX sh
ssh = Dict KnownShX sh
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict

lemKnownMapJust :: forall sh. KnownShS sh => Proxy sh -> Dict KnownShX (MapJust sh)
lemKnownMapJust :: forall (sh :: [Natural]).
KnownShS sh =>
Proxy sh -> Dict KnownShX (MapJust sh)
lemKnownMapJust Proxy sh
_ = StaticShX (MapJust sh) -> Dict KnownShX (MapJust sh)
forall (sh :: [Maybe Natural]). StaticShX sh -> Dict KnownShX sh
lemKnownShX (ShS sh -> StaticShX (MapJust sh)
forall (sh' :: [Natural]). ShS sh' -> StaticShX (MapJust sh')
go (forall (sh :: [Natural]). KnownShS sh => ShS sh
knownShS @sh))
  where
    go :: ShS sh' -> StaticShX (MapJust sh')
    go :: forall (sh' :: [Natural]). ShS sh' -> StaticShX (MapJust sh')
go ShS sh'
ZSS = StaticShX '[]
StaticShX (MapJust sh')
forall (sh :: [Maybe Natural]). (sh ~ '[]) => StaticShX sh
ZKX
    go (SNat n
n :$$ ShS sh
sh) = SNat n -> SMayNat () SNat ('Just n)
forall {k} (f :: k -> *) (n1 :: k) i.
f n1 -> SMayNat i f ('Just n1)
SKnown SNat n
n SMayNat () SNat ('Just n)
-> StaticShX (MapJust sh) -> StaticShX ('Just n : MapJust sh)
forall {sh1 :: [Maybe Natural]} (n :: Maybe Natural)
       (sh :: [Maybe Natural]).
((n : sh) ~ sh1) =>
SMayNat () SNat n -> StaticShX sh -> StaticShX sh1
:!% ShS sh -> StaticShX (MapJust sh)
forall (sh' :: [Natural]). ShS sh' -> StaticShX (MapJust sh')
go ShS sh
sh

-- ** Rank

lemRankApp :: forall sh1 sh2.
              StaticShX sh1 -> StaticShX sh2
           -> Rank (sh1 ++ sh2) :~: Rank sh1 + Rank sh2
lemRankApp :: forall (sh1 :: [Maybe Natural]) (sh2 :: [Maybe Natural]).
StaticShX sh1
-> StaticShX sh2 -> Rank (sh1 ++ sh2) :~: (Rank sh1 + Rank sh2)
lemRankApp StaticShX sh1
ZKX StaticShX sh2
_ = Rank sh2 :~: Rank sh2
Rank (sh1 ++ sh2) :~: (Rank sh1 + Rank sh2)
forall {k} (a :: k). a :~: a
Refl
lemRankApp (SMayNat () SNat n
_ :!% (StaticShX sh
ssh1 :: StaticShX sh1T)) StaticShX sh2
ssh2
  = Proxy (Rank sh)
-> Proxy (Rank sh2)
-> Proxy (Rank (sh ++ sh2))
-> ((Rank sh + Rank sh2) :~: Rank (sh ++ sh2))
-> (Rank (sh ++ sh2) + 1) :~: ((Rank sh + 1) + Rank sh2)
forall (proxy :: Natural -> *) (a :: Natural) (b :: Natural)
       (c :: Natural).
proxy a
-> proxy b
-> proxy c
-> ((a + b) :~: c)
-> (c + 1) :~: ((a + 1) + b)
lem (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @(Rank sh1T)) Proxy (Rank sh2)
forall {k} (t :: k). Proxy t
Proxy Proxy (Rank (sh ++ sh2))
forall {k} (t :: k). Proxy t
Proxy (((Rank sh + Rank sh2) :~: Rank (sh ++ sh2))
 -> (Rank (sh ++ sh2) + 1) :~: ((Rank sh + 1) + Rank sh2))
-> ((Rank sh + Rank sh2) :~: Rank (sh ++ sh2))
-> (Rank (sh ++ sh2) + 1) :~: ((Rank sh + 1) + Rank sh2)
forall a b. (a -> b) -> a -> b
$
      (Rank (sh ++ sh2) :~: (Rank sh + Rank sh2))
-> (Rank sh + Rank sh2) :~: Rank (sh ++ sh2)
forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
sym (StaticShX sh
-> StaticShX sh2 -> Rank (sh ++ sh2) :~: (Rank sh + Rank sh2)
forall (sh1 :: [Maybe Natural]) (sh2 :: [Maybe Natural]).
StaticShX sh1
-> StaticShX sh2 -> Rank (sh1 ++ sh2) :~: (Rank sh1 + Rank sh2)
lemRankApp StaticShX sh
ssh1 StaticShX sh2
ssh2)
  where
    lem :: proxy a -> proxy b -> proxy c
        -> (a + b :~: c)
        -> c + 1 :~: (a + 1 + b)
    lem :: forall (proxy :: Natural -> *) (a :: Natural) (b :: Natural)
       (c :: Natural).
proxy a
-> proxy b
-> proxy c
-> ((a + b) :~: c)
-> (c + 1) :~: ((a + 1) + b)
lem proxy a
_ proxy b
_ proxy c
_ (a + b) :~: c
Refl = (c + 1) :~: (c + 1)
(c + 1) :~: ((a + 1) + b)
forall {k} (a :: k). a :~: a
Refl

lemRankAppComm :: proxy sh1 -> proxy sh2
               -> Rank (sh1 ++ sh2) :~: Rank (sh2 ++ sh1)
lemRankAppComm :: forall {a} (proxy :: [a] -> *) (sh1 :: [a]) (sh2 :: [a]).
proxy sh1 -> proxy sh2 -> Rank (sh1 ++ sh2) :~: Rank (sh2 ++ sh1)
lemRankAppComm proxy sh1
_ proxy sh2
_ = Rank (sh1 ++ sh2) :~: Rank (sh2 ++ sh1)
forall {k} (a :: k) (b :: k). a :~: b
unsafeCoerceRefl

lemRankReplicate :: proxy n -> Rank (Replicate n (Nothing @Nat)) :~: n
lemRankReplicate :: forall (proxy :: Natural -> *) (n :: Natural).
proxy n -> Rank (Replicate n 'Nothing) :~: n
lemRankReplicate proxy n
_ = Rank (Replicate n 'Nothing) :~: n
forall {k} (a :: k) (b :: k). a :~: b
unsafeCoerceRefl

lemRankMapJust :: ShS sh -> Rank (MapJust sh) :~: Rank sh
lemRankMapJust :: forall (sh :: [Natural]). ShS sh -> Rank (MapJust sh) :~: Rank sh
lemRankMapJust ShS sh
ZSS = 0 :~: 0
Rank (MapJust sh) :~: Rank sh
forall {k} (a :: k). a :~: a
Refl
lemRankMapJust (SNat n
_ :$$ ShS sh
sh') | Rank (MapJust sh) :~: Rank sh
Refl <- ShS sh -> Rank (MapJust sh) :~: Rank sh
forall (sh :: [Natural]). ShS sh -> Rank (MapJust sh) :~: Rank sh
lemRankMapJust ShS sh
sh' = (Rank sh + 1) :~: (Rank sh + 1)
Rank (MapJust sh) :~: Rank sh
forall {k} (a :: k). a :~: a
Refl

-- ** Related to MapJust and/or Permutation

lemTakeLenMapJust :: Perm is -> ShS sh -> TakeLen is (MapJust sh) :~: MapJust (TakeLen is sh)
lemTakeLenMapJust :: forall (is :: [Natural]) (sh :: [Natural]).
Perm is
-> ShS sh -> TakeLen is (MapJust sh) :~: MapJust (TakeLen is sh)
lemTakeLenMapJust Perm is
PNil ShS sh
_ = '[] :~: '[]
TakeLen is (MapJust sh) :~: MapJust (TakeLen is sh)
forall {k} (a :: k). a :~: a
Refl
lemTakeLenMapJust (SNat a
_ `PCons` Perm l
is) (SNat n
_ :$$ ShS sh
sh) | TakeLen l (MapJust sh) :~: MapJust (TakeLen l sh)
Refl <- Perm l
-> ShS sh -> TakeLen l (MapJust sh) :~: MapJust (TakeLen l sh)
forall (is :: [Natural]) (sh :: [Natural]).
Perm is
-> ShS sh -> TakeLen is (MapJust sh) :~: MapJust (TakeLen is sh)
lemTakeLenMapJust Perm l
is ShS sh
sh = ('Just n : MapJust (TakeLen l sh))
:~: ('Just n : MapJust (TakeLen l sh))
TakeLen is (MapJust sh) :~: MapJust (TakeLen is sh)
forall {k} (a :: k). a :~: a
Refl
lemTakeLenMapJust (SNat a
_ `PCons` Perm l
_) ShS sh
ZSS = [Char] -> TakeLen (a : l) '[] :~: MapJust (TakeLen (a : l) '[])
forall a. HasCallStack => [Char] -> a
error [Char]
"TakeLen of empty"

lemDropLenMapJust :: Perm is -> ShS sh -> DropLen is (MapJust sh) :~: MapJust (DropLen is sh)
lemDropLenMapJust :: forall (is :: [Natural]) (sh :: [Natural]).
Perm is
-> ShS sh -> DropLen is (MapJust sh) :~: MapJust (DropLen is sh)
lemDropLenMapJust Perm is
PNil ShS sh
_ = MapJust sh :~: MapJust sh
DropLen is (MapJust sh) :~: MapJust (DropLen is sh)
forall {k} (a :: k). a :~: a
Refl
lemDropLenMapJust (SNat a
_ `PCons` Perm l
is) (SNat n
_ :$$ ShS sh
sh) | DropLen l (MapJust sh) :~: MapJust (DropLen l sh)
Refl <- Perm l
-> ShS sh -> DropLen l (MapJust sh) :~: MapJust (DropLen l sh)
forall (is :: [Natural]) (sh :: [Natural]).
Perm is
-> ShS sh -> DropLen is (MapJust sh) :~: MapJust (DropLen is sh)
lemDropLenMapJust Perm l
is ShS sh
sh = MapJust (DropLen l sh) :~: MapJust (DropLen l sh)
DropLen is (MapJust sh) :~: MapJust (DropLen is sh)
forall {k} (a :: k). a :~: a
Refl
lemDropLenMapJust (SNat a
_ `PCons` Perm l
_) ShS sh
ZSS = [Char] -> DropLen (a : l) '[] :~: MapJust (DropLen (a : l) '[])
forall a. HasCallStack => [Char] -> a
error [Char]
"DropLen of empty"

lemIndexMapJust :: SNat i -> ShS sh -> Index i (MapJust sh) :~: Just (Index i sh)
lemIndexMapJust :: forall (i :: Natural) (sh :: [Natural]).
SNat i -> ShS sh -> Index i (MapJust sh) :~: 'Just (Index i sh)
lemIndexMapJust SNat i
SZ (SNat n
_ :$$ ShS sh
_) = 'Just n :~: 'Just n
Index i (MapJust sh) :~: 'Just (Index i sh)
forall {k} (a :: k). a :~: a
Refl
lemIndexMapJust (SS (SNat n
i :: SNat i')) ((SNat n
_ :: SNat n) :$$ (ShS sh
sh :: ShS sh'))
  | Index n (MapJust sh) :~: 'Just (Index n sh)
Refl <- SNat n -> ShS sh -> Index n (MapJust sh) :~: 'Just (Index n sh)
forall (i :: Natural) (sh :: [Natural]).
SNat i -> ShS sh -> Index i (MapJust sh) :~: 'Just (Index i sh)
lemIndexMapJust SNat n
i ShS sh
sh
  , Index (n + 1) ('Just n : MapJust sh) :~: Index n (MapJust sh)
Refl <- Proxy n
-> Proxy ('Just n)
-> Proxy (MapJust sh)
-> Index (n + 1) ('Just n : MapJust sh) :~: Index n (MapJust sh)
forall {k} (i :: Natural) (a :: k) (l :: [k]).
Proxy i
-> Proxy a -> Proxy l -> Index (i + 1) (a : l) :~: Index i l
lemIndexSucc (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @i') (forall (t :: Maybe Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @(Just n)) (forall (t :: [Maybe Natural]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @(MapJust sh'))
  , Index (n + 1) (n : sh) :~: Index n sh
Refl <- Proxy n
-> Proxy n -> Proxy sh -> Index (n + 1) (n : sh) :~: Index n sh
forall {k} (i :: Natural) (a :: k) (l :: [k]).
Proxy i
-> Proxy a -> Proxy l -> Index (i + 1) (a : l) :~: Index i l
lemIndexSucc (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @i') (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) (forall (t :: [Natural]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @sh')
  = 'Just (Index n sh) :~: 'Just (Index n sh)
Index i (MapJust sh) :~: 'Just (Index i sh)
forall {k} (a :: k). a :~: a
Refl
lemIndexMapJust SNat i
_ ShS sh
ZSS = [Char] -> Index i '[] :~: 'Just (Index i '[])
forall a. HasCallStack => [Char] -> a
error [Char]
"Index of empty"

lemPermuteMapJust :: Perm is -> ShS sh -> Permute is (MapJust sh) :~: MapJust (Permute is sh)
lemPermuteMapJust :: forall (is :: [Natural]) (sh :: [Natural]).
Perm is
-> ShS sh -> Permute is (MapJust sh) :~: MapJust (Permute is sh)
lemPermuteMapJust Perm is
PNil ShS sh
_ = '[] :~: '[]
Permute is (MapJust sh) :~: MapJust (Permute is sh)
forall {k} (a :: k). a :~: a
Refl
lemPermuteMapJust (SNat a
i `PCons` Perm l
is) ShS sh
sh
  | Permute l (MapJust sh) :~: MapJust (Permute l sh)
Refl <- Perm l
-> ShS sh -> Permute l (MapJust sh) :~: MapJust (Permute l sh)
forall (is :: [Natural]) (sh :: [Natural]).
Perm is
-> ShS sh -> Permute is (MapJust sh) :~: MapJust (Permute is sh)
lemPermuteMapJust Perm l
is ShS sh
sh
  , Index a (MapJust sh) :~: 'Just (Index a sh)
Refl <- SNat a -> ShS sh -> Index a (MapJust sh) :~: 'Just (Index a sh)
forall (i :: Natural) (sh :: [Natural]).
SNat i -> ShS sh -> Index i (MapJust sh) :~: 'Just (Index i sh)
lemIndexMapJust SNat a
i ShS sh
sh
  = ('Just (Index a sh) : MapJust (Permute l sh))
:~: ('Just (Index a sh) : MapJust (Permute l sh))
Permute is (MapJust sh) :~: MapJust (Permute is sh)
forall {k} (a :: k). a :~: a
Refl

lemMapJustApp :: ShS sh1 -> Proxy sh2
              -> MapJust (sh1 ++ sh2) :~: MapJust sh1 ++ MapJust sh2
lemMapJustApp :: forall (sh1 :: [Natural]) (sh2 :: [Natural]).
ShS sh1
-> Proxy sh2
-> MapJust (sh1 ++ sh2) :~: (MapJust sh1 ++ MapJust sh2)
lemMapJustApp ShS sh1
ZSS Proxy sh2
_ = MapJust sh2 :~: MapJust sh2
MapJust (sh1 ++ sh2) :~: (MapJust sh1 ++ MapJust sh2)
forall {k} (a :: k). a :~: a
Refl
lemMapJustApp (SNat n
_ :$$ ShS sh
sh) Proxy sh2
p | MapJust (sh ++ sh2) :~: (MapJust sh ++ MapJust sh2)
Refl <- ShS sh
-> Proxy sh2 -> MapJust (sh ++ sh2) :~: (MapJust sh ++ MapJust sh2)
forall (sh1 :: [Natural]) (sh2 :: [Natural]).
ShS sh1
-> Proxy sh2
-> MapJust (sh1 ++ sh2) :~: (MapJust sh1 ++ MapJust sh2)
lemMapJustApp ShS sh
sh Proxy sh2
p = ('Just n : MapJust (sh ++ sh2)) :~: ('Just n : MapJust (sh ++ sh2))
MapJust (sh1 ++ sh2) :~: (MapJust sh1 ++ MapJust sh2)
forall {k} (a :: k). a :~: a
Refl