0 | module Data.Rel.Complement
 1 |
 2 | import Data.Rel
 3 | import Data.Fun
 4 | import Data.Fun.Extra
 5 | import Data.Vect.Quantifiers
 6 |
 7 | %default total
 8 |
 9 | ||| The logical complement of a relation.
10 | public export
11 | complement : {ts : Vect n Type} -> (p : Rel ts) -> Rel ts
12 | complement = chain Not
13 |
14 |
15 | ||| The negation of a relation for some elements
16 | ||| is equal to the complement of the relation.
17 | public export
18 | notToComplement :
19 |   {0 ts : Vect n Type}
20 |   -> (p : Rel ts)
21 |   -> (elems : HVect ts)
22 |   -> Not (uncurry p elems) = uncurry (complement {ts = ts} p) elems
23 | notToComplement p  = chainUncurry p Not
24 |