
  0 | module Data.Subset
  1 | 
  2 | %default total
  3 | 
  4 | ||| Proof that a value is present in a list. This is
  5 | ||| isomorphic to `Data.List.Elem` but with (in my opinion)
  6 | ||| more fitting names for our use case.
  7 | public export
  8 | data Has : (v : a) -> (ts : List a) -> Type where
  9 |   Z : Has v (v :: vs)
 10 |   S : Has v vs -> Has v (w :: vs)
 11 | 
 12 | export
 13 | Uninhabited (Has v []) where
 14 |   uninhabited Z impossible
 15 |   uninhabited (S _) impossible
 16 | 
 17 | export
 18 | 0 lemma_has_single : Has f [x] -> x === f
 19 | lemma_has_single Z = Refl
 20 | 
 21 | public export
 22 | drop : (ts : List a) -> Has v ts -> List a
 23 | drop (x :: xs)  Z    = xs
 24 | drop (x :: xs) (S k) = x :: drop xs k
 25 | 
 26 | 
 27 | ||| Removes an element from a list. This is used to
 28 | ||| calculate the list of effects after a single effect
 29 | ||| was properly handled.
 30 | public export
 31 | (-) : (ts : List a) -> (v : a) -> (prf : Has v ts) => List a
 32 | (-) xs _ {prf} = drop xs prf
 33 | 
 34 | 
 35 | ||| Proof that one set is subset of another set.
 36 | ||| Sets are represented by `List`. There is no gaurantee for no duplicate in list though.
 37 | public export
 38 | data Subset : {0 a: Type} -> (xs, ys : List a) -> Type where
 39 |   Nil : Subset [] ys
 40 |   (::) : {0 x: a} -> (e : Has x ys) -> Subset xs ys -> Subset (x::xs) ys
 41 | 
 42 | public export
 43 | lemma_subset : Subset fs fs' -> Has f fs -> Has f fs'
 44 | lemma_subset Nil has0 impossible
 45 | lemma_subset (e :: _     ) Z = e
 46 | lemma_subset (_ :: subset) (S has) = lemma_subset subset has
 47 |