Math.Tensor.Safe.Proofs

Type level equalities for generalized ranks. Used in Math.Tensor.Safe to prove impossible cases in pattern matching on singletons. Note that at the moment not every pattern match has a proof, which is reflected in the number of -Wincomplete-patterns warnings.

Tails of sane ranks are sane

saneTailRProof :: forall (r :: Rank). Sing r -> (Sane r ~ True) :- (Sane (TailR r) ~ True)

The TailR of a sane rank type is sane.

singITailRProof :: forall (r :: Rank). Sing r -> SingI r :- SingI (TailR r)

If a rank type has a SingI instance, the tail has a SingI instance.

Properties of merged ranks

saneMergeRProof :: forall (r :: Rank) (r' :: Rank) (r'' :: Rank). Sing r -> Sing r' -> (Sane r ~ True, Sane r' ~ True, MergeR r r' ~ Just r'') :- (Sane r'' ~ True)

Successfully merging two sane rank types (result is not Nothing) yields a sane rank type.

proofMergeLT :: forall (r :: Rank) (r' :: Rank) (r'' :: Rank). Sing r -> Sing r' -> (Sane r ~ True, Sane r' ~ True, MergeR r r' ~ Just r'', Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ LT) :- (MergeR (TailR r) r' ~ Just (TailR r''))

If two rank types can be merged and the first VSpace of the first rank type is less than the first VSpace of the second rank type, the TailR of the merged rank type is equal to the tail of the first rank type merged with the second rank type.

proofMergeGT :: forall (r :: Rank) (r' :: Rank) (r'' :: Rank). Sing r -> Sing r' -> (Sane r ~ True, Sane r' ~ True, MergeR r r' ~ Just r'', Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ GT) :- (MergeR r (TailR r') ~ Just (TailR r''))

If two rank types can be merged and the first VSpace of the first rank type is greater than the first VSpace of the second rank type, the TailR of the merged rank type is equal to the first rank type merged with the tail of the second rank type.

proofMergeIxNotEQ :: forall (r :: Rank) (r' :: Rank) (r'' :: Rank). Sing r -> Sing r' -> (Sane r ~ True, Sane r' ~ True, MergeR r r' ~ Just r'', Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ EQ) :- ((IxCompare (Snd (HeadR r)) (Snd (HeadR r')) == EQ) ~ False)

If two rank types can be merged and the first VSpace of the first rank type coincides with the first VSpace of the second rank type, the first index of the first rank type cannot equal the first index of the second rank type.

proofMergeIxLT :: forall (r :: Rank) (r' :: Rank) (r'' :: Rank). Sing r -> Sing r' -> (Sane r ~ True, Sane r' ~ True, MergeR r r' ~ Just r'', Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ EQ, IxCompare (Snd (HeadR r)) (Snd (HeadR r')) ~ LT) :- (MergeR (TailR r) r' ~ Just (TailR r''))

If two rank types can be merged and the first VSpace of the first rank type coincides with the first VSpace of the second rank type and the first index of the first rank type compares less than the first index of the second rank type, the TailR of the merged rank type is equal to the tail of the first rank type merged with the second rank type.

proofMergeIxGT :: forall (r :: Rank) (r' :: Rank) (r'' :: Rank). Sing r -> Sing r' -> (Sane r ~ True, Sane r' ~ True, MergeR r r' ~ Just r'', Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ EQ, IxCompare (Snd (HeadR r)) (Snd (HeadR r')) ~ GT) :- (MergeR r (TailR r') ~ Just (TailR r''))

If two rank types can be merged and the first VSpace of the first rank type coincides with the first VSpace of the second rank type and the first index of the first rank type compares greater than the first index of the second rank type, the TailR of the merged rank type is equal to the first rank type merged with the tail of the second rank type.

Properties of contractions

saneContractProof :: forall (r :: Rank). Sing r -> (Sane r ~ True) :- (Sane (ContractR r) ~ True)

If a rank type is sane, its contraction is also sane.

singletonContractProof :: forall (r :: Rank). Sing r -> (TailR r ~ '[]) :- (ContractR r ~ r)

The contraction of the empty rank type is the empty rank type.

contractTailDiffVProof :: forall (r :: Rank) (t :: Rank) (t' :: Rank). Sing r -> (t ~ TailR r, t' ~ TailR t, (Fst (HeadR r) == Fst (HeadR t)) ~ False) :- (TailR (ContractR r) ~ ContractR t)

If the first two labels of a rank type cannot be contracted because they belong to different VSpaces, the TailR of the contracted rank type is equal to the contraction of the TailR of the rank type.

contractTailSameVNoConProof :: forall (r :: Rank) (t :: Rank) (t' :: Rank) (i :: Symbol). Sing r -> (t ~ TailR r, t' ~ TailR t, (Fst (HeadR r) == Fst (HeadR t)) ~ True, Snd (HeadR r) ~ ICov i) :- (TailR (ContractR r) ~ ContractR t)

If the first two labels of a rank type cannot be contracted because the first label is covariant, the TailR of the contracted rank type is equal to the contraction of the TailR of the rank type.

contractTailSameVNoCovProof :: forall (r :: Rank) (t :: Rank) (t' :: Rank) (i :: Symbol). Sing r -> (t ~ TailR r, t' ~ TailR t, (Fst (HeadR r) == Fst (HeadR t)) ~ True, Snd (HeadR t) ~ ICon i) :- (TailR (ContractR r) ~ ContractR t)

If the first two labels of a rank type cannot be contracted because the second label is covariant, the TailR of the contracted rank type is equal to the contraction of the TailR of the rank type.

contractTailSameVDiffIProof :: forall (r :: Rank) (t :: Rank) (t' :: Rank) (i :: Symbol) (j :: Symbol). Sing r -> (t ~ TailR r, t' ~ TailR t, (Fst (HeadR r) == Fst (HeadR t)) ~ True, Snd (HeadR r) ~ ICon i, Snd (HeadR t) ~ ICov j, (i == j) ~ False) :- (TailR (ContractR r) ~ ContractR t)

If the first two labels of a rank type cannot be contracted because they differ, the TailR of the contracted rank type is equal to the contraction of the TailR of the rank type.

contractTailSameVSameIProof :: forall (r :: Rank) (t :: Rank) (t' :: Rank) (i :: Symbol) (j :: Symbol). Sing r -> (t ~ TailR r, t' ~ TailR t, (Fst (HeadR r) == Fst (HeadR t)) ~ True, Snd (HeadR r) ~ ICon i, Snd (HeadR t) ~ ICov j, (i == j) ~ True) :- (ContractR t' ~ ContractR r)

If the first two labels of a rank type can be contracted, the contracted rank type is equal to the contraction of the tail.