Scoping problem in proof state

[Dominic Mulligan]

Hi,

I'm trying to prove the following lemma with the development version of
Idris:

total powerMultMultPower : (m : Nat) -> (n : Nat) -> (exp : Nat) ->
power m exp * power n exp = power (m * n) exp
powerMultMultPower m n O = refl
powerMultMultPower m n (S exp) =
let inductiveHypothesis = powerMultMultPower m n exp in
?powerMultMultPowerStepCase

In the proof of the step case, after performing "intros" and "compute",
I have the following proof state:

---------- Assumptions: ----------
m : Nat
n : Nat
exp : Nat
inductiveHypothesis : power m exp * (power n exp) = power (m * n) exp
---------- Goal: ----------
{ hole 4 }:
mult (mult m (power m exp)) (mult n (power n exp)) =
mult (mult m n) (power (mult m n) exp)

Applying "rewrite (multAssociative m (power m exp) (mult n (power n
exp)))" I get the following type error:

Can't unify Float -> Float with Nat.

It appears that the rewrite tactic is missing the fact that there is a
fixed variable of type Nat in the context with the name "exp" and is
instead trying to use the function "exp" of type Float -> Float (from
the Prelude?).

Also, if you mistakenly do:

"rewrite multAssociative" instead of the above, you get a message
warning about a missing error:

user error (INTERNAL ERROR: "Not an equality type"
This is probably a bug, or a missing error message.
Please consider reporting at https://github.com/edwinb/Idris-dev/issues)

Presumably this should just warn about multAssociative not being applied
to enough arguments, rather than producing an internal error.

Thanks,
Dom

[Edwin Brady]

On 28 Nov 2012, at 10:29, Dominic Mulligan <dominic.p...@googlemail.com> wrote:

> It appears that the rewrite tactic is missing the fact that there is a
> fixed variable of type Nat in the context with the name "exp" and is
> instead trying to use the function "exp" of type Float -> Float (from
> the Prelude?).

Oops, well spotted. Looks like the tactic processor that's exposed to the programmer doesn't bother checking local scope first! Will fix this… I've added it to the issue tracker so I'll hopefully get to it soon.

> Also, if you mistakenly do:
>
> "rewrite multAssociative" instead of the above, you get a message
> warning about a missing error:
>
> user error (INTERNAL ERROR: "Not an equality type"
> This is probably a bug, or a missing error message.
> Please consider reporting at https://github.com/edwinb/Idris-dev/issues)
>
> Presumably this should just warn about multAssociative not being applied
> to enough arguments, rather than producing an internal error.

Yes, it seems like a good idea to look for that sort of mistake, which is likely to be common, and to tidy up the error message in any case.

Edwin.