Tell dependent function in conditional statement branch that condition is true

Question

I have a function with a type signature (x, y : SomeType) -> (cond x y) = True -> SomeType. When I check the condition in if-then-else/case/with statement, how do I pass to the function in a corresponding branch the fact, that condition is true?

Answer 1

You can use DecEq to make this easy:

add : (x, y : Nat) -> x + y < 10 = True -> Nat
add x y _ = x + y

main : IO ()
main =
  let x = S Z
  in let y = Z
  in case decEq (x + y < 10) True of
          Yes prf => print (add x y prf)
          No _ => putStrLn "x + y is not less than 10"

But you shouldn't.

Using booleans (via = or So) can tell you that something is true, but not why. The why is very important if you want to compose proofs together or break them apart. Imagine if add called a function which needed x + y < 20 - we can't just pass our proof that x + y < 10 = True because Idris knows nothing about the operation, just that it's true.

Instead, you should write the above with a data type which contains why it's true. LTE is a type which does that for less-than comparisons:

add : (x, y : Nat) -> LTE (x + y) 10 -> Nat
add x y _ = x + y

main : IO ()
main =
  let x = S Z
  in let y = Z
  in case isLTE (x + y) 10 of
          Yes prf => print (add x y prf)
          No _ => putStrLn "x + y is not less than 10"

Now, if add called a function which needed a LTE (x + y) 20 we can write a function to widen the constraint:

widen : a `LTE` b -> (c : Nat) -> a `LTE` (b + c)
widen LTEZero c = LTEZero
widen (LTESucc x) c = LTESucc (widen x c)

This is not something we can easily do with just booleans.