Idris：证明复数乘法是结合的

Question

我想验证假设当然也是的Ring实例。在 Abelian Group 之前这很容易，但在实例中发生了一些奇怪的事情：Data.Complex.Complex ttRingRing

VerifiedRing t => VerifiedRing (Complex t) where
    ringOpIsAssociative (l :+ li) (c :+ ci) (r :+ ri) =
        ?VerifiedRing_rhs_1

现在 Idris 自己进行了一些扩展，并且该洞得到以下类型：

(l <.> (c <.> r <+> inverse (ci <.> ri)) <+> inverse (li <.> (c <.> ri <+> ci <.> r))) :+ (l <.> (c <.> ri <+> ci <.> r) <+> li <.> (c <.> r <+> inverse (ci <.> ri))) =
((l <.> c <+> inverse (li <.> ci)) <.> r <+> inverse ((l <.> ci <+> li <.> c) <.> ri)) :+ ((l <.> c <+> inverse (li <.> ci)) <.> ri <+> (l <.> ci <+> li <.> c) <.> r)

我认为为了证明相等性我需要跳过一些括号。所以我从左边的第一个开始：

rewrite ringOpIsDistributiveL l (c <.> r) (inverse (ci <.> ri)) in
?VerifiedRing_rhs1

伊德里斯对此回应称：

rewriting l <.> (c <.> r <+> inverse (ci <.> ri)) to l <.> (c <.> r) <+>
                                                 l <.>
                                                 inverse (ci <.>
                                                          ri) did not change type (l <.>
                                                                                   (c <.>
                                                                                    r <+>
                                                                                    inverse (ci <.>
                                                                                             ri)) <+>
                                                                                   inverse (li <.>
                                                                                            (c <.>
                                                                                             ri <+>
                                                                                             ci <.>
                                                                                             r)) ...

请注意，后面的类型did not change the type与之前建议的类型不同。我不明白为什么它会改变，以及为什么重写在它应该起作用的时候却不起作用。