[TYPES] ordering lemmas about powerdomain operations

[Brian Huffman]

Quoting Thomas Streicher <streicher at mathematik.tu-darmstadt.de>:

> The lemma you mention is obvious from the way how the Smyth (i.e.   
> upper) powerdomin
> is constructed, namely as nonempty compact upward closed subsets of   
> the domain
> ordered by \supseteq. From this it is trivial.
> Moreover one has in the Smyth powerdomain  x \sqsubseteq y  if  x \cup y = x.
>
> Information about powerdomains can be found in the respective papers  
>  by Plotkin
> and Smyth from the 70ies.
> You might want to have a look at
>
>     http://homepages.inf.ed.ac.uk/gdp/publications/Domains.ps
>
> for example.
>
> Thomas

I'm not sure that I am familiar with the construction of the upper  
powerdomain that you describe, unless you are referring to the  
construction of Smyth powerdomains over flat element types from the  
linked paper. I failed to specify in my original question, but I am  
interested in element types that are arbitrary omega-bifinite domains.

In my formalization I construct three varieties of powerdomains using  
ideal completion, with a basis Pfin(K(a)) consisting of nonempty  
finite sets of compact elements, as described in Abramsky and Jung  
(1994) and elsewhere.

For the upper powerdomain, the preorder relation is
xs << ys == forall y in ys, exists x in xs, such that x << y.

That is, everything in ys is above something in xs. From this  
definition it is indeed obvious that the following property holds for  
elements of the *basis*,
where (+) is ordinary set-union and {-} is the singleton set:

xs + ys << {z} if and only if xs << {z} or ys << {z}

However, I am more interested in the version of this lemma for the  
completed powerdomain, where (+) and {-} refer to the continuous  
extensions of the union and singleton operations on the basis.

Some properties (like xs + ys << xs, or xs + ys = ys + xs) are easy to  
transfer from the basis to the ideal completion, since they are  
admissible predicates in either variable. However, a property like (xs  
+ ys << {z} --> xs << {z} or ys << {z}) is not an admissible  
predicate, because it has an implication. The only proof I could find  
is rather tricky, and relies on the underlying element type being  
bifinite.

Here is the full list of other (seemingly-obvious) lemmas that  
required a similar trick to prove:
{x} << ys + zs  iff  {x} << ys or {x} << zs  (lower)
{x} << ys + zs  iff  {x} << ys and {x} << zs  (convex)
xs + ys << {z}  iff  xs << {z} and ys << {z}  (convex)
{x} << {y}  iff  x << y  (upper, lower, and convex)

Of course, it is entirely possible that these have much easier proofs  
that I just failed to find. Alternatively, using a different  
construction besides ideal completion might yield easier proofs of  
these properties, but I have only seen such an alternative  
construction for the lower powerdomain (described in the Plotkin notes  
you linked, as well as the Wikipedia "Power domains" article).

- Brian