Stream: Coq users

Topic: z <= 1000

Huỳnh Trần Khanh (Nov 26 2022 at 15:29):

I need help proving this lemma:

Require Import ZArith.
Require Import Lia.
Require Import PArith.BinPos.

Open Scope Z.

Lemma helper : forall (z x y : Z) (h1 : x * y * z <= 1000000) (h2 : z <= x + y - 1) (h3 : 1 <= x <= 1000000) (h4 : 1 <= y <= 1000000) (h5 : 1 <= z <= 1000000),
z <= 1000.

I'm sure it's correct. Here's what Wolfram Alpha has to say about it: Screenshot-from-2022-11-26-15-28-59.png

Thanks in advance, and I will return the favor some day...

Paolo Giarrusso (Nov 26 2022 at 16:14):

informal sketch:

1. we can assume z > 1000 and try proving a contradiction (because z <= 1000 is decidable — use destruct (z <=? 1000) or such in Coq).
2. by algebra, we can conclude x + y > 1001 and xy < 1000 — say that exists epsilon, x + y = 1001 + epsilon
3. Using the theory associated with https://en.wikipedia.org/wiki/Inequality_of_arithmetic_and_geometric_means and/or calculus (not sure how to formalize that), we know that xy is smallest when xy are farthest away from each other, e.g. y = 1 and x = 1000 + epsilon (or symmetrically x = 1). But then xy = 1000 + epsilon; since we knew xy < 1000, we get the desired contradiction.

Paolo Giarrusso (Nov 26 2022 at 16:15):

but I've never done reals in Coq, and depending on what's available, one might search for a different sketch or automated solvers or...

Paolo Giarrusso (Nov 26 2022 at 16:20):

simpler approach: install https://github.com/coin-or/Csdp and try psatz?

Last updated: Oct 01 2023 at 19:01 UTC