Is there a zero knowledge proof for divisibility by 7? For a demonstration, I would like to present a zero knowledge proof that one party has a secret number that is divisible by 7. The goal is to prove that they have such a number without releasing the number. 

Is this a reasonable thing to prove with a zero knowledge system? If so, how would I go about doing it?

For bonus points, I'd like to demonstrate it with a non-interactive zero knowledge proof.
Everyone has access to a number divisible by 7, like 0, 7, 21, 434, etc, so I will assume you mean there is a secret that a party has and is using and THAT number has to be divisible by 7.


  Is this a reasonable thing to prove with a zero knowledge system?


It does seem rather odd, but if the other party needs to be sure your secret is divisible by 7, then you need this proof.  I can't imagine such a protocol off the top of my head, but if you have one that requires it, then I guess you need it.

You can do this in Zero Knowledge if you are willing to concede pieces of information that are usually considered minor.  You can prove anything problem in NP in zero knowledge.  It would imply knowledge of the divisor, but if you know the secret number, you can already the number divided by 7.  By the nature of the cryptographic tools, you will be forced to place an upper bound on the size of $n$ and $n \over 7$.  There is also the issue of overflow.  In many cryptographic settings, $n \over 7$ could be large enough so that if you were to multiply by 7, it would wrap around and reach some normally unrelated $n$.  

If $n$ is divisible by 7, then there is an integer $k = {n \over 7}$

You can encrypt $n$ and the $k$ in exponential (additive) elgamal or use Pedersen Commitment, all of which are homomorphic.  I will use Pedersen Commitments.  With a group $G$, take generators $g, h \in G$ such that the DLOG between $g$ and $h$ is unknown.   and $r_x$ be random numbers.  $q = |G|$.

This proof consists of two distinct parts:  First, we prove that $7k \equiv n 
 \text{ mod } q$, then we prove that $7k &lt; q$.


The Prover creates two commitments $C_k = g^k h^{r_k}$ and $C_n = g^n h^{r_n}$ and sends them to the Verifier.  
The Verifier and Prover raise ${C_k}^7 = g^{7 k} h^{7 r_k} = {C_{7k}}$.
The Verifier and Prover computes $C_{7k} \cdot {C_n}^{-1} = g^{7k - n} h^{7r_k - r_n} = h^{7r_k - r_n}$.  
The Prover privately calculates $r_1 - 7r_0$
The Prover and Verifier run Schnorr's protocol on $C_{7k} \cdot {C_n}^{-1}$, with the Prover proving knowledge of the DLOG of $h^{r_n - 7r_k}$ base $h$.


NOTE:  At this point, it is proven that $k \equiv {n \over 7}$ mod $q$, but it is not proven that $k$ didn't overflow, meaning at this point $7k$ could be greater than $q$, meaning in $n = 7k \text{ mod } q$, $n$ may be divisible by $k + q$ instead of $k$.  The following steps prove $7k$ didn't overflow by representing it in a bitwise manner, essentially setting bounds on $k$ based.  This implicitly puts an upper bound on the value of $0 \leq k \lt 2^t$, where $t$ is the number of bits.  You can have as many leading zeroes as you need if $k$ is small.  


If the Verifier accepts the Schnorr proof, the Prover creates a bitwise representation of $k$.  The Prover constructs a list of $t$ bit commitments representing $k$, of the form $C_{b_i} = g^{b_i} h^{r_i}$, where $b_i$ is the bit in the $2^i$ place in $k$.  $t$ has to be 4 bits less than the number of bits (or fewer) in the order $q$ to avoid overflow and to leak as little information as possible, as multiplying will add 3 total bits to the number.  
Prove each commitment hides a bit.  There is a proof for this in the appendix of this paper: http://crypto.stanford.edu/~dabo/pubs/abstracts/provisions.html. 
If these proofs are accepted, both parties homomorphically combine the bits to get a commitment of $k$:  $C_k' = \prod_{i=0}^{t} {C_{b_i}}^{2^i} = g^k h^{r'_k}$. The Prover knows $r'_k = \sum_{i=0}^t r_i \cdot 2^i$.
The Verifier and Prover computes $C_{k} \cdot {C_k'}^{-1} = g^{k - k} h^{r_k - r'_k} = h^{r_k - r'_k}$.  The Prover calculates $r_k - r'_k$.
The Prover and Verifier run Schnorr's Protocol to prove knowledge of the DLOG of $C_{k} \cdot {C_k'}^{-1}$ base $h$, which happens to be $r_k - r'_k$.


This protocol does release some information about the secrets, namely $n &lt; 7\cdot 2^t &lt; q$, ${n \over 7} &lt; 2^t$, but usually with this kind of proof, the Prover is willing to concede these points.  You can get more precise by using a range proof to prove that $k &lt; \left \lfloor{q\over 7} \right \rfloor$ on steps 6 and 7, but you can find that on your own.  Other than these pieces of information, this protocol should be Zero Knowledge.

This protocol perfectly hides $k$ within the bounds above.  Any $k$ within those bounds can produce an identical transcript.  Even with infinite computational power (assuming true random numbers), an adversary can not figure out your $k$ afterwards.  Same mostly goes for $n$, except they know $n$ is divisible by 7.

It should be noted that nothing here makes the Prover use the appropriate $n$.  This will need to be either verified beforehand.  If you don't care which $n$ he chose, he is still bound to using the $n$ from this proof if you use the appropriate Zero Knowledge Proofs to require he use the $n$. 

This protocol can be made non interactive by taking the component Zero Knowledge Proofs and applying the Fiat-Shamir Heuristic, which replaced the Verifier's challenge with a hash of the inputs and the initial communication.

There is also the logic circuit option, which is more flexible but less efficient.  You essentially prove your bits from the $k$ can go through a multiplication logic circuit and end up with $n$.

If you haven't read it yet, I would recommend reading Hazay and Lindell's section on Zero Knowledge Proofs from the book Efficient Secure Two-Party Protocols: Techniques and Constructions (Information Security and Cryptography)