1 files changed, 47 insertions, 0 deletions
diff --git a/src/Data/Array/Mixed/Lemmas.hs b/src/Data/Array/Mixed/Lemmas.hs
new file mode 100644
index 0000000..30ec9c0
--- /dev/null
+++ b/src/Data/Array/Mixed/Lemmas.hs
@@ -0,0 +1,47 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
+{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE DataKinds #-}
+module Data.Array.Mixed.Lemmas where
+
+import Data.Proxy
+import Data.Type.Equality
+import GHC.TypeLits
+
+import Data.Array.Mixed.Shape
+import Data.Array.Mixed.Types
+
+
+lemRankApp :: forall sh1 sh2.
+              StaticShX sh1 -> StaticShX sh2
+           -> Rank (sh1 ++ sh2) :~: Rank sh1 + Rank sh2
+lemRankApp ZKX _ = Refl
+lemRankApp (_ :!% (ssh1 :: StaticShX sh1T)) ssh2
+  = lem2 (Proxy @(Rank sh1T)) Proxy Proxy $
+      lem (Proxy @(Rank sh2)) (Proxy @(Rank sh1T)) (Proxy @(Rank (sh1T ++ sh2))) $
+        lemRankApp ssh1 ssh2
+  where
+    lem :: proxy a -> proxy b -> proxy c
+        -> c :~: b + a
+        -> b + a :~: c
+    lem _ _ _ Refl = Refl
+
+    lem2 :: proxy a -> proxy b -> proxy c
+         -> (a + b :~: c)
+         -> c + 1 :~: (a + 1 + b)
+    lem2 _ _ _ Refl = Refl
+
+lemRankAppComm :: StaticShX sh1 -> StaticShX sh2
+               -> Rank (sh1 ++ sh2) :~: Rank (sh2 ++ sh1)
+lemRankAppComm _ _ = unsafeCoerceRefl  -- TODO improve this
+
+lemKnownNatRank :: IShX sh -> Dict KnownNat (Rank sh)
+lemKnownNatRank ZSX = Dict
+lemKnownNatRank (_ :$% sh) | Dict <- lemKnownNatRank sh = Dict
+
+lemKnownNatRankSSX :: StaticShX sh -> Dict KnownNat (Rank sh)
+lemKnownNatRankSSX ZKX = Dict
+lemKnownNatRankSSX (_ :!% ssh) | Dict <- lemKnownNatRankSSX ssh = Dict