perm2.idr

module Main

-- predicate is true for each list element
data Foreach : (Nat -> Type) -> List Nat -> Type
    where
        ForeachEmpty : (pred : Nat -> Type) -> Foreach pred []
        ForeachRec : (pred : Nat -> Type) -> (e : Nat) -> (rem : List Nat) -> Foreach pred rem ->
            Foreach pred (e :: rem)

-- predicate for list element count
data ListElemCount : List Nat -> (elem : Nat) -> (count : Nat) -> Type
    where
        Empty : ListElemCount [] 0 0
        Rec1 : (e : Nat) -> (rem : List Nat) -> (count : Nat) -> ListElemCount rem e count ->
            ListElemCount (e :: rem) e (count + 1)
        Rec0 : (e : Nat) -> (f : Nat) -> (rem : List Nat) -> (count : Nat) -> ListElemCount rem e count ->
            Not (e = f) ->
            ListElemCount (f :: rem) e count

-- predicate than both lists has the same count of given element
data SameElemCount : (elem : Nat) -> List Nat -> List Nat -> Type
    where
        SameElemCountMk : (count : Nat) -> (elem : Nat) -> (xs, ys : List Nat) ->
            ListElemCount xs elem count -> ListElemCount ys elem count ->
            SameElemCount elem xs ys

-- lists are permutations
data Perm : List Nat -> List Nat -> Type
    where
        PermMk : (xs, ys : List Nat) ->
            Foreach (\e => SameElemCount e xs ys) xs ->
            Foreach (\e => SameElemCount e ys xs) ys ->
            Perm xs ys

main : IO ()
main = putStrLn $ show $ "aa"