The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Klaus,

if a<=d, b<=e and c<=f are already there (as hypothesis), omega can solve 
this (for suitable sets).

Otherwise I don't think there is a generic tactic, since in general it is not 
very likely that you can prove a + b +c <= d + e + f by proving that <= holds 
for each pair. What I do in such situations is to "autoforward" certain 
easily provable results as hypothesis and then apply omega. So in your case, 
I would create one or more tactics which look if the preconditions for 
proving a<=d, b<=e or c<=f are there, and if so automatically create a 
hypothesis with this result. Then you can apply omega.

There are lemmas which have a fairly trivial conclusion but rather complex 
hypothesis and there are lemmas which have rather complex conclusions and 
rather simple hypothesis (and others of cause). The first ones are better 
used forward (working from hypothesis towards the goal) while the latter are 
better used backward (working from the goal towards the hypothesis), because 
otherwise the search branching factors are large. Coq doesn't have good built 
in support for forwarding things automatically, but one can for sure write 
tactics which do this.

Of cause you can also write a simple tactic that takes a goal a + term1 <= b 
+ term2 and converts this into two goals a<=b and term1<=term2. If you need 
help with automating forwarding (which can get quite involved) or writing 
such a simple tactic, please let me now.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928