Define Topology

[Thomas Bereknyei]

Hi, (first-time post)

I'm trying to get the hang of LiquidHaskell as a way to read papers.
At the moment I'm looking at: https://arxiv.org/pdf/1603.01446.pdf

Definition 4. A topology on a set X is a collection T of subsets of X
satisfying the following properties:
1. X ∈ T .
2. ∅ ∈ T .
3. The union of any collection of elements of T is also in T .
4. The intersection of any finite collection of elements of T is also in T .

I've been able to express and verify conditions (1) and (2) using this
(listElts and Set_mem doesn't seem to work with nested lists, hence
the need to re-invent the wheel):
```
{-@ reflect hasElem @-}
hasElem :: Eq a => a -> [a] -> Bool
hasElem x [] = False
hasElem x (y:ys) = x == y || hasElem x ys
```

Then my thought was to define:
```
{-@ data Topology a = T {
    unT :: {v: [[a]] | true }
  , unX :: {v: [a]  | true } }  @-}
data Topology a = T { unT :: [[a]], unX :: [a] }

{-@ using (Topology a) as {v:Topology a |
    true
    && hasElem empty (unT v)
    && hasElem (unX v) (unT v)
    && hasSubsetUnion (unT v)
   && hasSubsetIntersection (unT v)
    } @-}
```
I've been able to express (3) and (4) in reflected functions, but it
doesn't seem enough for LH to prove the properties. Am I on the right
track? Is there a better approach?

[Ranjit Jhala]

Hi Thomas,

(sorry for the delay - I think the slack channel may receive quicker replies!)

Thanks for the very interesting question! 

I would formalize those requirements as follows:

First, lets define a type for "subsets of X"

```

-- | Subsets a X is a Set (Set a) where each set is a subset of X
{-@ type Subsets a X = S.Set {v:S.Set a | S.isSubsetOf v X} @-}
```

Next, we can use your idea to build a "struct" as follows:

```
{-@ data Topology a = T

     { unX  :: S.Set a
     , unT  :: {t: Subsets a unX | (S.member S.empty t) && (S.member unX t) }
     , pfUn :: x1:{_| S.member x1 unT} -> x2:{_| S.member x2 unT} ->
               {v:() | S.member (S.union x1 x2) unT}
     , pfIn :: x1:{_| S.member x1 unT} -> x2:{_| S.member x2 unT} ->
               {v:() | S.member (S.intersection x1 x2) unT}
     }  
  @-}
```

Note that the requirements (1) and (2) are specified by the requirement on `unT`

For (3) and (4) I'd go with the "propositions as types" approach so the properties are:

3. The union of any collection of elements of T is also in T .
4. The intersection of any finite collection of elements of T is also in T .

Which I am rewriting (after shrinking to "pairwise" which should generalize 

to any finite collection at least?) to

- forall X1, X2 in T. (union X1 X2) in T

- forall X1, X2 in T, (inter X1 X2) in T 

which in turn become the function signatures for the `pfUn` and `pfIn`.

Does that help? Do let me know!

Best!

- Ranjit.

--
You received this message because you are subscribed to the Google Groups "liquidhaskell" group.
To unsubscribe from this group and stop receiving emails from it, send an email to liquidhaskel...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/liquidhaskell/97b3d5c3-683c-4dab-94a3-ba88b814c561%40googlegroups.com.