Idris proof of less than

Question

I'm very new to Idris (and dependent types). I was trying to do write a program to check if a string is a palindrome of not. To do that, I decided to compute the length of the string, and compute

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

and then split the string as follows:

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

This takes care of both odd and even length strings. The problem is that Idris needs a proof that r < q since both q and r are Nat.

My question is: How do I express the fact that r

Here's the full sample of my code:

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

Gregg54654 Gregg54654 · Accepted Answer · 2017-10-01T01:14:34

You can't proof that r ≤ q because it's not true. For example, given the string "a" you have strlen = 1 and therefore q = 0 and r = 1. In this example r ≤ q is clearly false.

Note that you can implement isPalindrome simply by

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

Idris proof of less than

1 Answers