Demonstrating a Point (x, y) of natural numbers where both x and y must be >= 2

point.idr

--proof that 8 >= 2
eight_GTE_two : 8 `GTE` 2
eight_GTE_two = proof search

--proof that 8 >= 3
eight_GTE_three : 8 `GTE` 3
eight_GTE_three = proof search

--this doesn't work since it fails with the error "Can't solve goal LTE 2 1" (GTE is defined in terms of LTE in Idris)
--one_GTE_two : 1 `GTE` 2
--one_GTE_two = proof search

--necessary lemmas from http://www.davidchristiansen.dk/2014/05/21/idris-dec-techniques/
notLTESZ : LTE (S k) Z -> Void
notLTESZ LTEZero impossible

notLTE_S_S : (LTE k j -> Void) -> LTE (S k) (S j) -> Void
notLTE_S_S nope (LTESucc x) = nope x

--decide whether or not n <= m
decLTE : (n : Nat) -> (m : Nat) -> Dec (n `LTE` m)
decLTE Z m = Yes LTEZero
decLTE (S k) Z = No notLTESZ
decLTE (S k) (S j) with (decLTE k j)
  decLTE (S k) (S j) | (Yes prf) = Yes (LTESucc prf)
  decLTE (S k) (S j) | (No contra) = No $ notLTE_S_S contra

--this function can only be called if n >= 2 (you have to actually pass in a proof that n >= 2)
print_n_GTE_two : (n : Nat) -> (prf : n `GTE` 2) -> IO ()
print_n_GTE_two n prf = putStrLn $ show n ++ " >= 2"

--same as the previous function, but with a parameterized lower bound
print_first_GTE_second : (first : Nat) -> (second : Nat) -> (prf : first `GTE` second) -> IO ()
print_first_GTE_second first second prf = putStrLn $ show first ++ " >= " ++ show second

--finally the Point data type
data Point : Type where
    MakePoint : (x : Nat) -> (y : Nat) -> (prfx : x `GTE` 2) -> (prfy : y `GTE` 2) -> Point

--you can only call this function if you have constructed a valid point
printpoint : Point -> IO ()
printpoint (MakePoint x y _ _) = putStrLn $ "both x (" ++ show x ++ ") and y (" ++ show y ++ ") >= 2"

main : IO ()
main = do
    let test = 5
    case test of
        --test 1 works (8 >= 2)
        1 => print_n_GTE_two 8 eight_GTE_two

        --test 2 fails with the error "Can't solve goal LTE 2 1" (GTE is defined in terms of LTE in Idris)
        --2 => print_first_GTE_second 1 2 one_GTE_two

        --test 3 works (8 >= 3 with a parameterized lower bound)
        3 => print_first_GTE_second 8 3 eight_GTE_three

        --test 4 demonstrates a runtime check that the length of the first word >= the length of the second word
        4 => do
            args <- getArgs
            case args of
                [command, longerword, shorterword] => do
                    let (llong, lshort) = (length longerword, length shorterword)
                    case decLTE lshort llong of
                        Yes prf => print_first_GTE_second llong lshort prf
                        No _ => putStrLn $ "Cannot call print_first_GTE_second, since (length of " ++ longerword ++ ") <= (length of " ++ shorterword ++ ")"
                        --No prf => print_first_GTE_second llong lshort prf
                _ => putStrLn "Usage: ./point loooooooongerword shorterword"

        --test 5 works
        5 => printpoint (MakePoint 8 8 eight_GTE_two eight_GTE_two)

        --test 6 doesn't work
        --6 => printpoint (MakePoint 1 8 one_GTE_two eight_GTE_two)