The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi,

> I often have goals of the form
> 
> a + b +c <= d + e + f
> 
> and they are solved by showing a <=d, b<=e, c<=f.
> 
> For equalities, there is the f_equal tactic to split
> such goals.
> 
> Is there something similar for <= and +?
> 
> Right now, I'm proving such goals via "assert (a <= d)"
> and so forth, followed by reflexivity, but surely there
> must be a better way.
> 
> What is be the best way to automate such proofs?

If <= is registered as a relation with the Setoid mechanism, and if the
compatibility lemma of add and <= is registered, then `f_equiv` could do
the job.  If they are not registered, you could do so yourself in your code.

However, I have found the f_equiv shipped with Coq to often not work as
expected.  In our code, we are using a custom version of f_equiv that
(in our experience) more reliably applies the lemma we want it to apply.
You can find the code at
<https://gitlab.mpi-sws.org/FP/iris-coq/blob/4653cb6/prelude/tactics.v#L253>.

Kind regards,
Ralf