coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] f_equals for <= and +
Date: Thu, 27 Oct 2016 12:26:50 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT ens-lyon.fr; spf=Pass smtp.mailfrom=gaetan.gilbert AT ens-lyon.fr; spf=None smtp.helo=postmaster AT labbe.ens-lyon.fr
Ironport-phdr: 9a23:EOIqRRasZM8gPll/dqUn8cD/LSx+4OfEezUN459isYplN5qZpc+ybnLW6fgltlLVR4KTs6sC0LuM9f+5EjRcqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ3p7xiLn5o8GbSj4LrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGwD884mosVHSODxe7kyZb1eFjUvdW4vt+PxshyWYgKC+nIaGkoXlhBFGRSNuB7zU4v4tG31t+531TOGFcDwVvUwSDOkqalxHky7wBwbPiI0pTmEwvd7i7hW9Uqs

[repeat plus_le_compat] if it's an inequality on nats, [Z.add_le_mono] for Z, etc. Use search to find the one for your type.

I don't know if there's a general tactic for it.

Gaëtan Gilbert

On 27/10/2016 12:18, Klaus Ostermann wrote:

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