coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] f_equals for <= and +, Klaus Ostermann, 10/27/2016
- Re: [Coq-Club] f_equals for <= and +, Gaetan Gilbert, 10/27/2016
- Re: [Coq-Club] f_equals for <= and +, Ralf Jung, 10/27/2016
- RE: [Coq-Club] f_equals for <= and +, Soegtrop, Michael, 10/27/2016
Archive powered by MHonArc 2.6.18.