0 | module Search.Negation
 1 |
 2 | import Data.List.Quantifiers
 3 | import Data.Nat
 4 |
 5 | %default total
 6 |
 7 | ||| It is much easier to look for positive evidence than it is to look
 8 | ||| for negative evidence. So instead of looking for `Not q`, we may
 9 | ||| want to look for `p` instead
10 | public export
11 | interface Negates p q | q where
12 |   toNegation : p -> Not q
13 |
14 | public export
15 | ({0 x : a} -> Negates (p x) (q x)) => Negates (All p xs) (Any q xs) where
16 |   toNegation all = allNegAny (mapProperty toNegation all)
17 |
18 | public export
19 | ({0 x : a} -> Negates (p x) (q x)) => Negates (Any p xs) (All q xs) where
20 |   toNegation any = anyNegAll (mapProperty toNegation any)
21 |
22 | public export
23 | Negates (m `LT` n) (m `GTE` n) where
24 |   toNegation = LTImpliesNotGTE
25 |
26 | public export
27 | Negates (m `LTE` n) (m `GT` n) where
28 |   toNegation = LTEImpliesNotGT
29 |