Safe Haskell | None |
---|---|
Language | Haskell2010 |
Data.Array.Nested.Lemmas
Synopsis
- lemLeqSuccSucc :: forall (k :: Natural) (n :: Natural). (k + 1) <= n => Proxy k -> Proxy n -> (k <=? (n - 1)) :~: 'True
- lemLeqPlus :: forall (n :: Natural) (m :: Natural) (k :: Natural). n <= m => Proxy n -> Proxy m -> Proxy k -> (n <=? (m + k)) :~: 'True
- lemAppNil :: forall {a} (l :: [a]). (l ++ ('[] :: [a])) :~: l
- lemAppAssoc :: forall {a1} (a2 :: [a1]) (b :: [a1]) (c :: [a1]). Proxy a2 -> Proxy b -> Proxy c -> ((a2 ++ b) ++ c) :~: (a2 ++ (b ++ c))
- lemAppLeft :: forall {a1} (l :: [a1]) (a2 :: [a1]) (b :: [a1]). Proxy l -> (a2 :~: b) -> (a2 ++ l) :~: (b ++ l)
- lemReplicatePlusApp :: forall {a1} (n :: Nat) (m :: Natural) (a2 :: a1). SNat n -> Proxy m -> Proxy a2 -> Replicate (n + m) a2 :~: (Replicate n a2 ++ Replicate m a2)
- 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)
- 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)
- lemInitApp :: forall {a} (l :: [a]) (x :: a). Proxy l -> Proxy x -> Init (l ++ '[x]) :~: l
- lemLastApp :: forall {k} (l :: [k]) (x :: k). Proxy l -> Proxy x -> Last (l ++ '[x]) :~: x
- lemKnownNatSucc :: forall (n :: Nat). KnownNat n => Dict KnownNat (n + 1)
- lemKnownNatRank :: forall (sh :: [Maybe Nat]) i. ShX sh i -> Dict KnownNat (Rank sh)
- lemKnownNatRankSSX :: forall (sh :: [Maybe Nat]). StaticShX sh -> Dict KnownNat (Rank sh)
- lemKnownReplicate :: forall (n :: Nat). SNat n -> Dict KnownShX (Replicate n ('Nothing :: Maybe Nat))
- lemKnownShX :: forall (sh :: [Maybe Nat]). StaticShX sh -> Dict KnownShX sh
- lemKnownMapJust :: forall (sh :: [Nat]). KnownShS sh => Proxy sh -> Dict KnownShX (MapJust sh)
- lemRankApp :: forall (sh1 :: [Maybe Nat]) (sh2 :: [Maybe Nat]). StaticShX sh1 -> StaticShX sh2 -> Rank (sh1 ++ sh2) :~: (Rank sh1 + Rank sh2)
- lemRankAppComm :: forall {a} proxy (sh1 :: [a]) (sh2 :: [a]). proxy sh1 -> proxy sh2 -> Rank (sh1 ++ sh2) :~: Rank (sh2 ++ sh1)
- lemRankReplicate :: forall proxy (n :: Natural). proxy n -> Rank (Replicate n ('Nothing :: Maybe Nat)) :~: n
- lemRankMapJust :: forall (sh :: [Nat]). ShS sh -> Rank (MapJust sh) :~: Rank sh
- lemTakeLenMapJust :: forall (is :: [Nat]) (sh :: [Nat]). Perm is -> ShS sh -> TakeLen is (MapJust sh) :~: MapJust (TakeLen is sh)
- lemDropLenMapJust :: forall (is :: [Nat]) (sh :: [Nat]). Perm is -> ShS sh -> DropLen is (MapJust sh) :~: MapJust (DropLen is sh)
- lemIndexMapJust :: forall (i :: Nat) (sh :: [Nat]). SNat i -> ShS sh -> Index i (MapJust sh) :~: 'Just (Index i sh)
- lemPermuteMapJust :: forall (is :: [Nat]) (sh :: [Nat]). Perm is -> ShS sh -> Permute is (MapJust sh) :~: MapJust (Permute is sh)
- lemMapJustApp :: forall (sh1 :: [Nat]) (sh2 :: [Nat]). ShS sh1 -> Proxy sh2 -> MapJust (sh1 ++ sh2) :~: (MapJust sh1 ++ MapJust sh2)
Lemmas about numbers and lists
Nat
lemLeqSuccSucc :: forall (k :: Natural) (n :: Natural). (k + 1) <= n => Proxy k -> Proxy n -> (k <=? (n - 1)) :~: 'True Source #
lemLeqPlus :: forall (n :: Natural) (m :: Natural) (k :: Natural). n <= m => Proxy n -> Proxy m -> Proxy k -> (n <=? (m + k)) :~: 'True Source #
Append
lemAppAssoc :: forall {a1} (a2 :: [a1]) (b :: [a1]) (c :: [a1]). Proxy a2 -> Proxy b -> Proxy c -> ((a2 ++ b) ++ c) :~: (a2 ++ (b ++ c)) Source #
lemAppLeft :: forall {a1} (l :: [a1]) (a2 :: [a1]) (b :: [a1]). Proxy l -> (a2 :~: b) -> (a2 ++ l) :~: (b ++ l) Source #
Simple type families
lemReplicatePlusApp :: forall {a1} (n :: Nat) (m :: Natural) (a2 :: a1). SNat n -> Proxy m -> Proxy a2 -> Replicate (n + m) a2 :~: (Replicate n a2 ++ Replicate m a2) Source #
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) Source #
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) Source #
KnownNat
Lemmas about shapes
Known shapes
lemKnownReplicate :: forall (n :: Nat). SNat n -> Dict KnownShX (Replicate n ('Nothing :: Maybe Nat)) Source #
lemKnownMapJust :: forall (sh :: [Nat]). KnownShS sh => Proxy sh -> Dict KnownShX (MapJust sh) Source #
Rank
lemRankApp :: forall (sh1 :: [Maybe Nat]) (sh2 :: [Maybe Nat]). StaticShX sh1 -> StaticShX sh2 -> Rank (sh1 ++ sh2) :~: (Rank sh1 + Rank sh2) Source #
lemRankAppComm :: forall {a} proxy (sh1 :: [a]) (sh2 :: [a]). proxy sh1 -> proxy sh2 -> Rank (sh1 ++ sh2) :~: Rank (sh2 ++ sh1) Source #
lemRankReplicate :: forall proxy (n :: Natural). proxy n -> Rank (Replicate n ('Nothing :: Maybe Nat)) :~: n Source #
Related to MapJust and/or Permutation
lemTakeLenMapJust :: forall (is :: [Nat]) (sh :: [Nat]). Perm is -> ShS sh -> TakeLen is (MapJust sh) :~: MapJust (TakeLen is sh) Source #
lemDropLenMapJust :: forall (is :: [Nat]) (sh :: [Nat]). Perm is -> ShS sh -> DropLen is (MapJust sh) :~: MapJust (DropLen is sh) Source #
lemIndexMapJust :: forall (i :: Nat) (sh :: [Nat]). SNat i -> ShS sh -> Index i (MapJust sh) :~: 'Just (Index i sh) Source #