Search code examples
mathtypesidrisdependent-typequantifiers

Complex quantifiers in Idris?

Now I know, it's possible to express quantifiers via dependent types. So I wrote a simple realization for this "for all (a, b: N): exists (c: N): c = a + b":

f : (a : Nat) -> (b : Nat) -> (c : Nat ** c = a + b)
f a b = (a + b ** Refl)

and it works.

And now I want to know, can I express this "for all (a, b: N): exists (c: N): c > a and c < b"?

Solution

  • For Nat comparison you can use Data.Nat's GT (greater than), GTE (greater-equal than), LT (less than), LTE (less-equal than). So GT c a and LT c b for c > a and c < b.

    For and you can just put both proofs into a tuple: (GT c a, LT c b). If, for example, you would have wanted to or them, you could use Either (GT c a) (LT c b).

    Thus:

    import Data.Nat

f : (a, b : Nat) -> (c : Nat ** (GT c a, LT c b))

    (However, this exact example wouldn't work, as you cannot define f, as there is no c so c > 5 and c < 5.)