伊德里斯不会在指数法的证明中扩展`mult`

Question

我正在尝试在伊德里斯写一个2^n * 2^m = 2^(n+m)的证据。现在我有这个：

expLaw : (power 2 n) * (power 2 m) = power 2 (n + m)
expLaw {n=Z} {m} = plusZeroRightNeutral (power 2 m)
expLaw {n=S n'} {m=m'} = 
  trans (multAssociative 2 (power 2 n') (power 2 m')) $ 
  cong {f=mult 2} $ expLaw {n=n'} {m=m'}

这给了我错误：

When checking an application of function trans:
        Type mismatch between
                mult 2 (power 2 n' * power 2 m') = mult 2 (power 2 (n' + m')) (Type of cong powExp)
        and
                mult (mult 2 (power 2 n')) (power 2 m') = plus (power 2 (plus n' m')) (plus (power 2 (plus n' m')) 0) (Expected type)

        Specifically:
                Type mismatch between
                        mult 2 (power 2 (n' + m'))
                and
                        plus (power 2 (plus n' m')) (plus (power 2 (plus n' m')) 0)

据我所知，这基本上是说它正在看到一个2 * 2^(n+m)它想要一个2^(n+m) + (2^(n+m) + 0)。但是，根据mult的定义，前者应该简单地减少到后者。特别是，以下编译没有问题：

foo : 2 * a = a + (a + 0)
foo = Refl

对我而言，这表明扩张正如我所料。但由于某些原因，在我的expLaw实现中，编译器卡住了。我想知道它是否与使用mult和plus与*和+有关，但我不确定。我怎样才能解决这个问题？

或者，如果有人有更好的方法来实施expLaw，我会很高兴听到它。

Answer 1

它有助于使用let … in …块逐步添加校样，因此您可以轻松地检查类型。错误发生在trans下，所以给出了

expLaw : (power 2 n) * (power 2 m) = power 2 (n + m)
expLaw {n=Z} {m} = plusZeroRightNeutral (power 2 m)
expLaw {n=S n'} {m=m'} =
  let prf1 = cong {f=mult 2} $ expLaw {n=n'} {m=m'} in
  let prf2 = multAssociative 2 (power 2 n') (power 2 m') in
  ?hole

> :t hole
  m' : Nat
  n' : Nat
  prf1 : plus (mult (power 2 n') (power 2 m'))
              (plus (mult (power 2 n') (power 2 m')) 0) =
         plus (power 2 (plus n' m')) (plus (power 2 (plus n' m')) 0)
  prf2 : plus (mult (power 2 n') (power 2 m'))
              (plus (mult (power 2 n') (power 2 m')) 0) =
         mult (plus (power 2 n') (plus (power 2 n') 0)) (power 2 m')
--------------------------------------
hole : mult (plus (power 2 n') (plus (power 2 n') 0)) (power 2 m') =
       plus (power 2 (plus n' m')) (plus (power 2 (plus n' m')) 0)

你可以看到等于prf2 : a = b，prf1 : a = c的顺序与trans : (a = b) -> (b = c) -> a = c不匹配。但有一个简单的sym : (a = b) -> b = a它的工作原理。所以你几乎拥有它。 :-)

 …
 let prf3 = trans (sym prf2) prf1 in
 prf3