电感级的Idris证明

Question

考虑以下功能

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)

试图编译时，我会得到以下错误：

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)

关于tryMove的递归调用。如果我明确地传递给{prf}，如

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)

它编译正确。

为什么Idris不能在归纳步骤中自动检测到证据，而能够在函数的正常调用中进行验证？

编辑：

下面是要使用的完整要点：https://gist.github.com/marcosh/d51479ea08e8522560713fd1e5ca9624

Answer 1

您提供了prf的默认值(prf)，因此Idris试图将Oh传递到递归调用中。Oh有So True类型，Idris希望prf为So (from /= to)类型，但是由于您不破坏to和from，Idris无法知道from /= to的值，这就是您看到错误消息的原因。

您可以将签名更改为包含{auto prf: So (from /= to)}或完全删除prf参数，因为您实际上并不使用它，只需将其传递到递归调用中，而无需任何修改。