Idris证明小于

Question

我对Idris (和依赖类型)非常陌生。我试着写一个程序来检查一个字符串是否是非回文。为此，我决定计算字符串的长度，并计算

q,r = (strlen `div` 2, strlen `mod` 2)

然后按如下方式拆分字符串：

lhalf,rhalf = (substr 0 (q+r) str, substr (q-r) (q+r) str)

这可以同时处理奇数和偶数长度的字符串。问题是Idris需要证明r

我的问题是:我如何表达r的事实？

下面是我的代码的完整示例：

module Main

isPalindrome : (str : String) -> String
isPalindrome str =
  let split = half_half str
  in show ((fst split) == reverse (snd split))
  where
    strlen : Nat
    strlen = length str

    divMod : Nat -> Nat -> (Nat,Nat)
    divMod x y = (x `div` y, x `mod` y)

    half_half : String -> (String, String)
    half_half "" = ("","")
    half_half x  = let
                     (q,r) = divMod strlen 2
                   in
                     (substr 0     (q+r) x,
                      substr (q-r) (q+r) x)

main : IO ()
main = repl "> " isPalindrome

Answer 1

你不能证明r，≤，q，因为它不是真的。例如，给定字符串"a“，你有strlen = 1，因此q=0，r=1。在这个例子中，r≤q显然是假的。

注意，您可以简单地通过以下方式实现isPalindrome

isPalindrome: String -> Bool
isPalindrome str = str == reverse str