The Coq mailing list

[Thomas Strathmann <thomas AT pdp7.org>]

Hallo!

The question I have is probably due to my limited understanding of Coq 
and best practises when it comes to enconding certain mathematical 
objects. I'd like to encode constraint systems on integers that are 
conjunctions of inequalities (x_1 <> x_2) and equations of the form  x_1 
+ ... + x_n = k and proof that such a system has a solution. Encoding 
the constraints as propositions is straight forward, but I do not know 
how to express the proposition that this system has a solution which on 
papar I'd write as something like: Exists x_1, ..., x_n : Z | c_1 /\ ... 
/\ c_k (where the c_i are the individual constraints). Can you suggest a 
way to do this or should I rethink the whole approach? Thank you.

        Thomas