Idris won't expand `mult` in proof of exponent law

Question

I'm trying to write a proof that 2^n * 2^m = 2^(n+m) in Idris. Right now I have this:

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'}

This gives me the error:

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)

As far as I can tell, this is essentially saying that it is seeing a 2 * 2^(n+m) where it wants a 2^(n+m) + (2^(n+m) + 0). However, by the definition of mult, the former should trivially reduce to the latter. In particular, the following compiles without problem:

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

To me, this indicates that the expansion is working as I would expect. But for some reason, in my implementation of expLaw, the compiler gets stuck. I'm wondering if it might have something to do with the use of mult and plus versus * and +, but I'm not sure. How can I fix this?

Alternatively, if anyone has a better way to implement expLaw I'd be happy to hear it.

Answer 1

It helps to add proofs step by step with let … in … blocks, so you can easily inspect the types. The error occures under trans, so given

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)

You can see that the order of the equalities prf2 : a = b, prf1 : a = c don't match up with trans : (a = b) -> (b = c) -> a = c. But with a simple sym : (a = b) -> b = a it works. So you almost had it. :-)

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