Forall quantifier and complex boolean propositions in Idris

Question

I'm new to dependent types and, having a Haskell experience, am slowly learning Idris. For an exercize, I want to write a Huffman encoding. Currently I'm trying to write a proof that the "flattening" of the code tree produces a prefix code, but has got stuck with the quantifiers.

I have a simple inductive proposition that one list is a prefix of an another:

using (xs : List a, ys : List a)
    data Prefix : List a -> List a -> Type where
        pEmpty : Prefix Nil ys
        pNext  : (x : a) -> Prefix xs ys -> Prefix (x :: xs) (x :: ys)

Is this a valid approach? Or something like "xs is prefix of ys if there is zs such that xs ++ zs = ys" would be better?
Was it the right way to introduce a "forall" quantifier (as far as I can understand, in Agda it would be something like pNext : ∀ {x xs ys} → Prefix xs ys → Prefix (x :: xs) (y :: ys))? Should the pNext first argument be implicit? What is the semantic differences between two variants?

Then, I want to build one for a vector where none of elements forms a prefix of another:

data PrefVect : Vect n (List a) -> Type where

Empty vector has no prefixes:

    pvEmpty : PrefVect Nil

and given an element x, a vector xs, and proofs that none element of xs is a prefix of x (and vice versa), x :: xs will hold that property:

    pvNext  : (x : [a]) -> (xs : Vect n [a]) ->
              All (\y => Not (Prefix x y)) xs ->
              All (\y => Not (Prefix y x)) xs ->
              PrefVect (x :: xs)

This is an unvalid type which I hope to fix after dealing with the first one, but there is similar question about quantifiers in pvNext: is this variant acceptable, or there is a better way to form a "negation on relation"?

Thank you.

Edwin Brady Edwin Brady · Accepted Answer · 2014-12-03T09:27:41

I think the only problem here is that you've used [a] as the type of lists of a, in the Haskell style, whereas in Idris it needs to be List a.

Your Prefix type looks fine to me, although I'd write it as:

data Prefix : List a -> List a -> Type where
     pEmpty : Prefix [] ys
     pNext : Prefix xs ys -> Prefix (x :: xs) (x :: ys)

That is, x can be implicit, and you don't need the using because Idris can infer the types of xs and ys. Whether this is the right approach or not really depends on what you plan to use the Prefix type for. It's certainly easy enough to test whether a list is the prefix of another. Something like:

testPrefix : DecEq a => (xs : List a) -> (ys : List a) -> Maybe (Prefix xs ys)
testPrefix [] ys = Just pEmpty
testPrefix (x :: xs) [] = Nothing
testPrefix (x :: xs) (y :: ys) with (decEq x y)
  testPrefix (x :: xs) (x :: ys) | (Yes Refl) = Just (pNext !(testPrefix xs ys
  testPrefix (x :: xs) (y :: ys) | (No contra) = Nothing

If you want to prove the negation, which it seems you might, you'll need the type to be:

testPrefix : DecEq a => (xs : List a) -> (ys : List a) -> Dec (Prefix xs ys)

I'll leave that one as an exercise :).

Forall quantifier and complex boolean propositions in Idris

1 Answers