Search code examples
idris

Idris - proof on inductive step

Consider the following function

tryMove : (diskNumber : Nat) -> (from: Peg) -> (to: Peg)-> {default Oh prf: So (from /= to)} -> Disposition diskNumber -> Maybe (Disposition diskNumber)
tryMove Z from to [] = Nothing
tryMove (S k) from to (smallestDiskPosition :: restOfTheDisposition) =
        map (smallestDiskPosition ::) (tryMove k from to restOfTheDisposition)

Trying to compile I get the following error:

When checking argument prf to Hanoi.tryMove:
        Type mismatch between
                So True (Type of Oh)
        and
                So (from /= to) (Expected type)

        Specifically:
                Type mismatch between
                        True
                and
                        not (Hanoi.Peg implementation of Prelude.Interfaces.Eq, method == from to)

on the recurvise invocation of tryMove. If I explicitely pass {prf} as in

tryMove : (diskNumber : Nat) -> (from: Peg) -> (to: Peg)-> {default Oh prf: So (from /= to)} -> Disposition diskNumber -> Maybe (Disposition diskNumber)
tryMove Z from to [] = Nothing
tryMove (S k) from to {prf} (smallestDiskPosition :: restOfTheDisposition) =
        map (smallestDiskPosition ::) (tryMove k from to {prf} restOfTheDisposition)

It compiles correctly.

Why is that that Idris can not detect automatically the proof in the inductive step, while it is able to do it in a normal invocation of the function?

EDIT:

here is a complete gist to use: https://gist.github.com/marcosh/d51479ea08e8522560713fd1e5ca9624

Solution

  • You supply the default value (Oh) for prf, so Idris is trying to pass Oh into the recursive call. Oh has type So True and Idris expects prf to be of type So (from /= to), but since you don't destruct to and from, Idris cannot know the value of from /= to, that's why you see that error message.

    You can change the signature to contain {auto prf: So (from /= to)} or delete the prf argument altogether, because you don't actually use it, you just pass it into the recursive call without any modification.