diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2025-05-15 23:20:43 +0200 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2025-05-15 23:20:43 +0200 |
| commit | 6cdbe556ddfb066a2fe205161b4ead793565c5f4 (patch) | |
| tree | 446d3f12de84cea15a246e62bac3d08d3a1016b5 | |
| parent | 6f82510ddde60b76e7c81eae2da7d947312179e5 (diff) | |
Simplify lemRankApp
| -rw-r--r-- | src/Data/Array/Mixed/Lemmas.hs | 14 |
1 files changed, 4 insertions, 10 deletions
diff --git a/src/Data/Array/Mixed/Lemmas.hs b/src/Data/Array/Mixed/Lemmas.hs index 7b3365b..7f41a06 100644 --- a/src/Data/Array/Mixed/Lemmas.hs +++ b/src/Data/Array/Mixed/Lemmas.hs @@ -56,20 +56,14 @@ lemRankApp :: forall sh1 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 + = lem (Proxy @(Rank sh1T)) Proxy Proxy $ + sym (lemRankApp ssh1 ssh2) where lem :: proxy a -> proxy b -> proxy c - -> c :~: b + a - -> b + a :~: c + -> (a + b :~: c) + -> c + 1 :~: (a + 1 + b) 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 |