Rel.idr

module Rel

DecProofType : {a:Type} -> Dec a -> Type
DecProofType {a} (Yes _)  = a
DecProofType {a} (No _)   = a -> _|_
 
decProof : {a:Type} -> (dec : Dec a) -> DecProofType dec
decProof (Yes x)  = x
decProof (No x)   = x

DecType : {a:Type} -> Dec a -> Type
DecType {a} _ = a

-- Proofs that something is not an element of a vector
using ( x : t, y : t, xs : Vect n t )
  data NElem : t -> Vect n t -> Type where
    Empty : NElem x []
    Miss  : Not (y = x) -> NElem x xs -> NElem x (y :: xs)

  strip : NElem x (y :: xs) -> NElem x xs
  strip (Miss _ x) = x

  headInEq : NElem x (y :: xs) -> Not (y = x)
  headInEq (Miss p _) = p

total
decNElem : DecEq t => (x : t) -> (xs : Vect n t) -> Dec (NElem x xs)
decNElem x Nil       = Yes Empty
decNElem x (y :: ys) with (decEq y x)
  decNElem x (x :: ys) | (Yes yEqX) =
    No (\nElemXYYs => headInEq nElemXYYs yEqX)
  decNElem x (y :: ys) | (No f) with (decNElem x ys)
    decNElem x (y :: ys) | (No f) | (Yes z) = Yes (Miss f z)
    decNElem x (y :: ys) | (No f) | (No notNElemXYs) =
      No (\nElemXYYs => notNElemXYs (strip nElemXYYs))

namespace Uniq
  -- Vector types where each element is unique
  data Uniq : Nat -> Type -> Type where
    Nil  : Uniq 0 t
    (::) : (x : t) ->
           (xs : Uniq n t) ->
           { default (decProof (decNElem x (content xs)))
             isUniq : NElem {n} x (content xs) } ->
           Uniq (S n) t

  content : Uniq n t -> Vect n t
  content Nil        = Nil
  content ((::) a b) = a :: content b