The Coq mailing list

[Bingzhou <bingzhou.zheng AT gmail.com>]

> You could certainly write functions that discriminate on whether a type 
> is empty or not, if an appropriate proof is passed in.  However, I've 
> never seen this done, so probably the most useful thing is for you to 
> explain more context on your development, so that we can offer 
> bigger-picture advice.

Thanks Adam, 

I am trying to prove some properties about the decorated interval arithmetic. 

An interval can have one of five decorations: safe, defined, containing, 
empty,
and ill-formed. 

This system has five relations:
pSaf(f, x) : x is a nonempty subset of domain(f), and the restriction of f to 
x 
             is continuous and bounded;
pDef(f, x) : x is a nonempty subset of domain(f);
pCon(f, x) : always true;
pEmp(f, x) : x is disjoint from domain(f) (either or both of x and domain(f) 
             may be empty);
pIll(f, x) : domain(f) is empty.

For a function f and an interval vector x, I should define dec(f, x), i.e. the
decoration of f over x, as:
saf: if pSaf(f, x) holds;
def: if pSaf(f, x) fails and pDef(f, x) holds;
ill: if pIll(f, x) holds;
emp: if pIll(f, x) fails and pEmp(f, x) holds;
con: otherwise. 

So, I think the first step is to define predicates or relations such as
emptydomain, subsetOfDomain, continuous and bounded ...  

Thanks a lot,
Bingzhou