Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] f_equals for <= and +

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] f_equals for <= and +


Chronological Thread 
  • From: Ralf Jung <jung AT mpi-sws.org>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] f_equals for <= and +
  • Date: Thu, 27 Oct 2016 12:28:54 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT hera.mpi-klsb.mpg.de
  • Ironport-phdr: 9a23:1VQSUBEM1Ew5gBwfgvZKcZ1GYnF86YWxBRYc798ds5kLTJ76oMSwAkXT6L1XgUPTWs2DsrQf2rCQ7PmrATBIoc7Y9itdINoUD15NoP5VtjJjKfbNMVf8Iv/uYn5yN+V5f3ghwUuGN1NIEt31fVzYry76xzcTHhLiKVg9fbytScbkpp/ojKXqp9WTPl0J13KBZuZ5KwzzpgHMvOEXh5FjI+A/0EjnuHxNLt5fwW0gB0+VkF6o5Nq287Zm6yUVoO06sclaXvOpLOwDUbVEAWF+YCgO78rxuEyeFQY=

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




Archive powered by MHonArc 2.6.18.

Top of Page