[POPLmark] Type-refinement "challenge"

[Daniel C. Wang]

Here is another micro-issue that I think could be improved a bit in all 
systems. I wouldn't call this a hard challenge by any means, but I think 
it's a good way to compare how the various systems can capture this very 
common notational pattern effectively.

Given the following theory.

n ::= z | s(n)
 
------------
 sum(z,n,n)
 
  sum(n1,n2,n3)
--------------------
sum(s(n1),n2,s(n3))

----------------
 non_zero(s(z))
 
 non_zero(n)
----------------
 non_zero(s(n))

show that
\forall n1,n2,n3.  non_zero(n1)  and sum(n1,n2,n3) implies non_zero(n3)
    and
\forall n1,n2,n3.  non_zero(n2)  and sum(n1,n2,n3) implies non_zero(n3)

Please use the relations as defined and do not use any libraries. i.e. 
do this from first principles. Some of you will notice that non_zero is 
a predicate that carves out an inductively defined subset of naturals. 
If your proof system supports type definitions or dependent pairs do the 
proof both with and without using those facilitates for representing 
non-zero naturals.

What I'm trying to capture is the common practice of defining  
refinements of a larger syntactic domain. (i.e. the values subset of 
expressions). Using more traditional notation I would have stated the 
problem as below where choice of meta-variables names implicitly 
constrains the set of objects I'm quantifying over. This is an extremely 
common practice in most every LaTeX proof I've ever seen, and all 
systems provide varying support to make this "painless". This standard 
notational practice avoids lots of tedious "obvious" validity 
assumptions. These obvious validity assumptions are the kind that are 
easy to forget if you're not careful, and very annoying to discover when 
you're stuck deep in the middle of your proof. 

n ::= z | s(n)

------------
 sum(z,n,n)
 
   sum(n1,n2,n3)
--------------------
sum(s(n1),n2,s(n3))

n+ ::= s(z)  |  s(n+)

show that
  \forall n1,n2+.\exists n3+. sum(n1,n2+,n3+) 
and
  \forall n1+,n2.\exists n3+. sum(n1+,n2,n3+)