coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] f_equals for <= and +

From: Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] f_equals for <= and +
Date: Thu, 27 Oct 2016 12:18:05 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=klaus.ostermann AT uni-tuebingen.de; spf=None smtp.mailfrom=klaus.ostermann AT uni-tuebingen.de; spf=None smtp.helo=postmaster AT mx04.uni-tuebingen.de
Ironport-phdr: 9a23:ZQzgfxGW9r/d1SDpIYpe/J1GYnF86YWxBRYc798ds5kLTJ75o8mwAkXT6L1XgUPTWs2DsrQf2rCQ7PmrATBIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWD1YLojqvqp9X6WEZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwu3cYh/V0/MlZFK7+Yq4QTLpCDT1gPXpmytfssEzgSQKS/TM7SXkbiB9BBQ6NuBL+V4rq9Czhqudn3SCcO+XrS7FxRSmv5aZtRxLuzisKYW1quFrLg9B92foI6CmqoAZyltbZ

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?

Klaus

[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