coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Help with proving bounds on Z.land and Z.lor

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Help with proving bounds on Z.land and Z.lor
Date: Sat, 08 Apr 2017 19:36:32 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f176.google.com
Ironport-phdr: 9a23:7iiIghYRIK/DQERCXUyjmBz/LSx+4OfEezUN459isYplN5qZoMyybnLW6fgltlLVR4KTs6sC0LuK9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQtFiT6ybL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjE28G/ZhM9+gr9Frh29vBFw2ZLYbZuPOfZiYq/Qf9UXTndBUMZLUCxBB5uxYY8VAOoaOuZYqZT2qVoUrRu5HgmsH/7kxzhKhnDsxq061OIhEQ7c3AwnBNIOq3DZoc76NKcXS++1za3IwS/fYPNR3Dfw8Y7FeQ0ir/GURb98b9bdxE01Gw7Gjlics5LpMy2J2ugXrmSW7ettWOSygGA9sQ5xuCKgxsI0h4nJmI0VzlfE+D18wIkvJN24TFd3YcenEJdMri2aOZZ6T8EjTm1ytyY6zboGuZG/fCcU0pgo2xnfa/mff4iJ5BLsSvqRLC9miH55fL+znRW//Ei6xuHiSMW4zExGojdHn9TNrnwN0gbc6smDSvtz5Eeh3jOP2hjR6u5eOkA0kqzbK5E7wr43jZoTqkDOEzT5mEXzlqCWd0Ek9vK05OTgZ7XqvoWcOJNsigHiLqQundSyDvg/MggXRmSU5eC81KD48kDiW7VLjvg2krHDv5zAJMQboLS5Aw5P3Yo55Ra/FWTu7NNNln4eaVlBZRjP24PuIhTFJO3yJfa5mVWl1jlxkaPoJLrkV7fENX/F2Jj7eq1moxpewRE0y99F4IlPW5kOJfvyXgn6s9mOXUxxCBC93+uyUIY17YgZQ2/aWqI=

Hi,

I'm trying to establish bounds on Z.lor and Z.land, in particular for negative arguments. The standard library seems fairly impoverished on lemmas about N.ldiff (which is used in the definition of Z.lor and Z.land). Can anyone help me prove the following two lemmas?

Lemma land_abs_bounds a b

: a < 0 \/ b < 0

-> -(2^(Z.log2_up (Z.max (Z.abs a) (Z.abs b))))

<= Z.land a b

<= Z.max a b.

Lemma lor_abs_bounds a b

: a < 0 \/ b < 0

-> Z.min a b

<= Z.lor a b

<= 2^(Z.log2_up (Z.max (Z.abs a) (Z.abs b) + 1)) - 1.

(It doesn't matter much to me what the bounds are, as long as they don't use Z.lor/Z.land. These bounds also hold when both inputs are non-negative; I've already proven those cases)

Thanks,

Jason

[Coq-Club] Help with proving bounds on Z.land and Z.lor, Jason Gross, 04/08/2017
- Re: [Coq-Club] Help with proving bounds on Z.land and Z.lor, Jason Gross, 04/10/2017