## 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