Идрис: Докажите, что умножение комплексных чисел ассоциативно - PullRequest
Новая
       78

Идрис: Докажите, что умножение комплексных чисел ассоциативно

0 голосов
/ 02 марта 2019

Я хотел бы проверить экземпляр Ring для Data.Complex.Complex t, предполагая, конечно, t также Ring.Это было легко до Abelian Group, но с экземпляром Ring происходит что-то странное: 

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 отличается от типа, предложенного ранее,Я затрудняюсь понять, почему это меняется и почему перезапись не работает, когда она, безусловно, должна.

...