From 4360c60205d379f349cbfc6e8c0a691a0a4d45fc Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 25 Jun 2016 19:16:34 -0400 Subject: update licensing information --- AUTHORS | 16 ++++++++++++++++ CONTRIBUTORS | 31 +++++++++++++++++++++++++++++++ LICENSE | 2 +- 3 files changed, 48 insertions(+), 1 deletion(-) create mode 100644 AUTHORS create mode 100644 CONTRIBUTORS diff --git a/AUTHORS b/AUTHORS new file mode 100644 index 000000000..31d71c211 --- /dev/null +++ b/AUTHORS @@ -0,0 +1,16 @@ +# This is the official list of fiat-crypto authors for copyright purposes. +# This file is distinct from the CONTRIBUTORS files. +# See the latter for an explanation. + +# Names should be added to this file as one of +# Organization's name +# Individual's name +# Individual's name +# See CONTRIBUTORS for the meaning of multiple email addresses. + +# Please keep the list sorted. + +Andres Erbsen +Google Inc. +Jade Philipoom +Massachusetts Institute of Technology diff --git a/CONTRIBUTORS b/CONTRIBUTORS new file mode 100644 index 000000000..cf6cd93fa --- /dev/null +++ b/CONTRIBUTORS @@ -0,0 +1,31 @@ +# This is the official list of people have contributed code to the +# fiat-crypto repository. +# +# The AUTHORS file lists the copyright holders; this file +# lists people. For example, Google employees are listed here +# but not in AUTHORS, because Google holds the copyright. +# +# When adding J Random Contributor's name to this file, +# either J's name or J's organization's name should be +# added to the AUTHORS file, depending on who holds the copyright. +# +# Names should be added to this file like so: +# Individual's name +# Individual's name +# +# An entry with multiple email addresses specifies that the +# first address should be used in the submit logs and +# that the other addresses should be recognized as the +# same person. + +# Please keep the list sorted. + +## This file allows joining different accounts of a single person. +## Cf for instance: git shortlog -nse. More details via: man git shortlog + +Adam Chlipala +Andres Erbsen +Daniel Ziegler +Jade Philipoom +Jason Gross +Robert Sloan diff --git a/LICENSE b/LICENSE index 35e3cc51d..191fe6c04 100644 --- a/LICENSE +++ b/LICENSE @@ -1,6 +1,6 @@ The MIT License (MIT) -Copyright (c) 2015 Programming Languages and Verification Group at MIT CSAIL +Copyright (c) 2015-2016 the fiat-crypto authors (see the AUTHORS file). Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal -- cgit v1.2.3 From 794b0fe8f74bb54031ca37ed0f126ecc0b46f2fb Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 25 Jun 2016 23:10:34 -0400 Subject: Update CONTRIBUTORS --- CONTRIBUTORS | 3 --- 1 file changed, 3 deletions(-) diff --git a/CONTRIBUTORS b/CONTRIBUTORS index cf6cd93fa..905edafd1 100644 --- a/CONTRIBUTORS +++ b/CONTRIBUTORS @@ -20,9 +20,6 @@ # Please keep the list sorted. -## This file allows joining different accounts of a single person. -## Cf for instance: git shortlog -nse. More details via: man git shortlog - Adam Chlipala Andres Erbsen Daniel Ziegler -- cgit v1.2.3 From 91a712295078756f162113d30412c666679c90ac Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 28 Jun 2016 16:35:49 -0700 Subject: [super_nstaz]: Handle side-conditions from [nsatz] --- src/Algebra.v | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/Algebra.v b/src/Algebra.v index eca1b2bb1..bfc61fc69 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -1006,6 +1006,12 @@ Ltac nsatz_inequality_to_equality := | [ H : not (?R ?x ?zero) |- False ] => apply H | [ H : (?R ?x ?zero -> False)%type |- False ] => apply H end. +(** Clean up tactic handling side-conditions *) +Ltac super_nsatz_post_clean_inequalities try_tac := + repeat (apply conj || split_field_inequalities); + try assumption; + prensatz_contradict; nsatz_inequality_to_equality; + try nsatz. (** Handles inequalities and fractions *) Ltac super_nsatz := (* [nsatz] gives anomalies on duplicate hypotheses, so we strip them *) @@ -1015,7 +1021,8 @@ Ltac super_nsatz := there might not be any), so we handle them all separately *) [ try conservative_common_denominator_equality_inequality_all; [ try nsatz_inequality_to_equality; try nsatz - | repeat (apply conj || split_field_inequalities); try assumption; prensatz_contradict; nsatz_inequality_to_equality; try nsatz.. ].. ]. + | .. ]; + super_nsatz_post_clean_inequalities.. ]. Section ExtraLemmas. Context {F eq zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div}. -- cgit v1.2.3 From 9314779667e9d000e07d68ea55a6dd8647a707e3 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 28 Jun 2016 16:39:10 -0700 Subject: Fix a typo in the previous commit --- src/Algebra.v | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/Algebra.v b/src/Algebra.v index bfc61fc69..c3b0434cf 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -1007,7 +1007,7 @@ Ltac nsatz_inequality_to_equality := | [ H : (?R ?x ?zero -> False)%type |- False ] => apply H end. (** Clean up tactic handling side-conditions *) -Ltac super_nsatz_post_clean_inequalities try_tac := +Ltac super_nsatz_post_clean_inequalities := repeat (apply conj || split_field_inequalities); try assumption; prensatz_contradict; nsatz_inequality_to_equality; @@ -1020,9 +1020,10 @@ Ltac super_nsatz := (* Each goal left over by [prensatz_contradict] is separate (and there might not be any), so we handle them all separately *) [ try conservative_common_denominator_equality_inequality_all; - [ try nsatz_inequality_to_equality; try nsatz - | .. ]; - super_nsatz_post_clean_inequalities.. ]. + [ try nsatz_inequality_to_equality; try nsatz; + (* [nstaz] might leave over side-conditions; we handle them if they are inequalities *) + try super_nsatz_post_clean_inequalities + | super_nsatz_post_clean_inequalities.. ].. ]. Section ExtraLemmas. Context {F eq zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div}. -- cgit v1.2.3 From 555b058390770b3caaa3b858d2dac047fda0e5cc Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 29 Jun 2016 01:28:28 -0400 Subject: Create crypto-defects.md --- crypto-defects.md | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 crypto-defects.md diff --git a/crypto-defects.md b/crypto-defects.md new file mode 100644 index 000000000..88bd6d2e9 --- /dev/null +++ b/crypto-defects.md @@ -0,0 +1,9 @@ +Here is an incomplete list of defects in cryptographic implementations. We +should make sure our verification rules out the possibility of similar mistakes +appearing in our code. + +| Reference | Specification | Implementation | Defect | +| ------------------------------------------------------------------- | --------------------------- | --------------------------- | ------------- | +| [openssl#3607](https://rt.openssl.org/Ticket/Display.html?id=3607) | P256 field element squaring | 64-bit Montgomery form, asm | limb overflow | +| | | | | +| | | | | -- cgit v1.2.3 From dba9223dd4ea46f2476718635bcfbd157671bef6 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 29 Jun 2016 01:39:27 -0400 Subject: Update crypto-defects.md --- crypto-defects.md | 1 + 1 file changed, 1 insertion(+) diff --git a/crypto-defects.md b/crypto-defects.md index 88bd6d2e9..afd06f290 100644 --- a/crypto-defects.md +++ b/crypto-defects.md @@ -5,5 +5,6 @@ appearing in our code. | Reference | Specification | Implementation | Defect | | ------------------------------------------------------------------- | --------------------------- | --------------------------- | ------------- | | [openssl#3607](https://rt.openssl.org/Ticket/Display.html?id=3607) | P256 field element squaring | 64-bit Montgomery form, asm | limb overflow | +| [go#13515](https://github.com/golang/go/issues/13515) | Modular exponentiation | uintptr-sized Montgomery form, Go | carry handling | | | | | | | | | | | -- cgit v1.2.3 From 820b662de7f6a10d8c99be3c1d9f2cc17551cb09 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 29 Jun 2016 01:47:56 -0400 Subject: Update crypto-defects.md --- crypto-defects.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/crypto-defects.md b/crypto-defects.md index afd06f290..710c53bc0 100644 --- a/crypto-defects.md +++ b/crypto-defects.md @@ -6,5 +6,4 @@ appearing in our code. | ------------------------------------------------------------------- | --------------------------- | --------------------------- | ------------- | | [openssl#3607](https://rt.openssl.org/Ticket/Display.html?id=3607) | P256 field element squaring | 64-bit Montgomery form, asm | limb overflow | | [go#13515](https://github.com/golang/go/issues/13515) | Modular exponentiation | uintptr-sized Montgomery form, Go | carry handling | -| | | | | -| | | | | +| [NaCl ed25519 (p. 2)](https://tweetnacl.cr.yp.to/tweetnacl-20131229.pdf) | F25519 mul, square | 64-bit pseudo-Mersenne, qhasm | carry handling | -- cgit v1.2.3 From 0e969e296b42e54bf423e452e83e1262015067fe Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 29 Jun 2016 02:04:42 -0400 Subject: Update crypto-defects.md --- crypto-defects.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/crypto-defects.md b/crypto-defects.md index 710c53bc0..8dd010915 100644 --- a/crypto-defects.md +++ b/crypto-defects.md @@ -4,6 +4,7 @@ appearing in our code. | Reference | Specification | Implementation | Defect | | ------------------------------------------------------------------- | --------------------------- | --------------------------- | ------------- | -| [openssl#3607](https://rt.openssl.org/Ticket/Display.html?id=3607) | P256 field element squaring | 64-bit Montgomery form, asm | limb overflow | +| [openssl#3607](https://rt.openssl.org/Ticket/Display.html?id=3607) | P256 field element squaring | 64-bit Montgomery form, AMD64 | limb overflow | | [go#13515](https://github.com/golang/go/issues/13515) | Modular exponentiation | uintptr-sized Montgomery form, Go | carry handling | -| [NaCl ed25519 (p. 2)](https://tweetnacl.cr.yp.to/tweetnacl-20131229.pdf) | F25519 mul, square | 64-bit pseudo-Mersenne, qhasm | carry handling | +| [NaCl ed25519 (p. 2)](https://tweetnacl.cr.yp.to/tweetnacl-20131229.pdf) | F25519 mul, square | 64-bit pseudo-Mersenne, AMD64 | carry handling | +| [openssl#0c687d7e](https://git.openssl.org/gitweb/?p=openssl.git;a=commitdiff;h=dc3c5067cd90f3f2159e5d53c57b92730c687d7e;ds=sidebyside) | Poly1305 | 32-bit pseudo-Mersenne, x86 and ARM | bad truncation | -- cgit v1.2.3 From e385e7da270640ad176fa90b328bf3a3170ae6bc Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 29 Jun 2016 02:13:50 -0400 Subject: Update crypto-defects.md --- crypto-defects.md | 1 + 1 file changed, 1 insertion(+) diff --git a/crypto-defects.md b/crypto-defects.md index 8dd010915..162568a9b 100644 --- a/crypto-defects.md +++ b/crypto-defects.md @@ -8,3 +8,4 @@ appearing in our code. | [go#13515](https://github.com/golang/go/issues/13515) | Modular exponentiation | uintptr-sized Montgomery form, Go | carry handling | | [NaCl ed25519 (p. 2)](https://tweetnacl.cr.yp.to/tweetnacl-20131229.pdf) | F25519 mul, square | 64-bit pseudo-Mersenne, AMD64 | carry handling | | [openssl#0c687d7e](https://git.openssl.org/gitweb/?p=openssl.git;a=commitdiff;h=dc3c5067cd90f3f2159e5d53c57b92730c687d7e;ds=sidebyside) | Poly1305 | 32-bit pseudo-Mersenne, x86 and ARM | bad truncation | +| [openssl#ef5c9b11](https://github.com/openssl/openssl/commit/29851264f11ccc70c6c0140d7e3d8d93ef5c9b11) | Modular exponentiation | 64-bit Montgomery form, AMD64 | carry handling | -- cgit v1.2.3 From c16855482a77cdbefcd336a716ec9e79c8baf485 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 29 Jun 2016 02:17:46 -0400 Subject: Update crypto-defects.md --- crypto-defects.md | 1 + 1 file changed, 1 insertion(+) diff --git a/crypto-defects.md b/crypto-defects.md index 162568a9b..022e4aa73 100644 --- a/crypto-defects.md +++ b/crypto-defects.md @@ -9,3 +9,4 @@ appearing in our code. | [NaCl ed25519 (p. 2)](https://tweetnacl.cr.yp.to/tweetnacl-20131229.pdf) | F25519 mul, square | 64-bit pseudo-Mersenne, AMD64 | carry handling | | [openssl#0c687d7e](https://git.openssl.org/gitweb/?p=openssl.git;a=commitdiff;h=dc3c5067cd90f3f2159e5d53c57b92730c687d7e;ds=sidebyside) | Poly1305 | 32-bit pseudo-Mersenne, x86 and ARM | bad truncation | | [openssl#ef5c9b11](https://github.com/openssl/openssl/commit/29851264f11ccc70c6c0140d7e3d8d93ef5c9b11) | Modular exponentiation | 64-bit Montgomery form, AMD64 | carry handling | +| [nettle#09e3ce4d](https://git.lysator.liu.se/nettle/nettle/commit/c71d2c9d20eeebb985e3872e4550137209e3ce4d) | secp-256r1 modular reduction | | carry handling | -- cgit v1.2.3 From 8a18bfd2ceef8d073250d62742d9d12d345cad16 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 29 Jun 2016 02:27:17 -0400 Subject: Update crypto-defects.md --- crypto-defects.md | 1 + 1 file changed, 1 insertion(+) diff --git a/crypto-defects.md b/crypto-defects.md index 022e4aa73..50053001e 100644 --- a/crypto-defects.md +++ b/crypto-defects.md @@ -10,3 +10,4 @@ appearing in our code. | [openssl#0c687d7e](https://git.openssl.org/gitweb/?p=openssl.git;a=commitdiff;h=dc3c5067cd90f3f2159e5d53c57b92730c687d7e;ds=sidebyside) | Poly1305 | 32-bit pseudo-Mersenne, x86 and ARM | bad truncation | | [openssl#ef5c9b11](https://github.com/openssl/openssl/commit/29851264f11ccc70c6c0140d7e3d8d93ef5c9b11) | Modular exponentiation | 64-bit Montgomery form, AMD64 | carry handling | | [nettle#09e3ce4d](https://git.lysator.liu.se/nettle/nettle/commit/c71d2c9d20eeebb985e3872e4550137209e3ce4d) | secp-256r1 modular reduction | | carry handling | +| [socat#7](http://www.dest-unreach.org/socat/contrib/socat-secadv7.html) | DH in Z*p | irrelevant | non-prime p | -- cgit v1.2.3 From a5ecf8dddb9dcd986b7237a5daeaff9a0b96a760 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 29 Jun 2016 02:33:16 -0400 Subject: Update crypto-defects.md --- crypto-defects.md | 1 + 1 file changed, 1 insertion(+) diff --git a/crypto-defects.md b/crypto-defects.md index 50053001e..59f2af61e 100644 --- a/crypto-defects.md +++ b/crypto-defects.md @@ -11,3 +11,4 @@ appearing in our code. | [openssl#ef5c9b11](https://github.com/openssl/openssl/commit/29851264f11ccc70c6c0140d7e3d8d93ef5c9b11) | Modular exponentiation | 64-bit Montgomery form, AMD64 | carry handling | | [nettle#09e3ce4d](https://git.lysator.liu.se/nettle/nettle/commit/c71d2c9d20eeebb985e3872e4550137209e3ce4d) | secp-256r1 modular reduction | | carry handling | | [socat#7](http://www.dest-unreach.org/socat/contrib/socat-secadv7.html) | DH in Z*p | irrelevant | non-prime p | +| [invalid-curve](http://euklid.org/pdf/ECC_Invalid_Curve.pdf) | NIST ECDH | irrelevant | not onCurve | -- cgit v1.2.3 From 8dc35ba3cc06d6975567bada42ed50a905f1dc10 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 29 Jun 2016 02:58:56 -0400 Subject: Update crypto-defects.md --- crypto-defects.md | 1 + 1 file changed, 1 insertion(+) diff --git a/crypto-defects.md b/crypto-defects.md index 59f2af61e..457a21303 100644 --- a/crypto-defects.md +++ b/crypto-defects.md @@ -12,3 +12,4 @@ appearing in our code. | [nettle#09e3ce4d](https://git.lysator.liu.se/nettle/nettle/commit/c71d2c9d20eeebb985e3872e4550137209e3ce4d) | secp-256r1 modular reduction | | carry handling | | [socat#7](http://www.dest-unreach.org/socat/contrib/socat-secadv7.html) | DH in Z*p | irrelevant | non-prime p | | [invalid-curve](http://euklid.org/pdf/ECC_Invalid_Curve.pdf) | NIST ECDH | irrelevant | not onCurve | +| [donna#8edc799f](https://github.com/agl/curve25519-donna/commit/2647eeba59fb628914c79ce691df794a8edc799f) | F25519 internal to wire | 32-bit pseudo-Mersenne, C | non-canonical | -- cgit v1.2.3 From 3a21f0e37c85684e5bc991f49d10a77f9ea78d6d Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 29 Jun 2016 03:11:58 -0400 Subject: Update crypto-defects.md --- crypto-defects.md | 1 + 1 file changed, 1 insertion(+) diff --git a/crypto-defects.md b/crypto-defects.md index 457a21303..1a7ecdc8c 100644 --- a/crypto-defects.md +++ b/crypto-defects.md @@ -13,3 +13,4 @@ appearing in our code. | [socat#7](http://www.dest-unreach.org/socat/contrib/socat-secadv7.html) | DH in Z*p | irrelevant | non-prime p | | [invalid-curve](http://euklid.org/pdf/ECC_Invalid_Curve.pdf) | NIST ECDH | irrelevant | not onCurve | | [donna#8edc799f](https://github.com/agl/curve25519-donna/commit/2647eeba59fb628914c79ce691df794a8edc799f) | F25519 internal to wire | 32-bit pseudo-Mersenne, C | non-canonical | +| [end-to-end#340](https://github.com/google/end-to-end/issues/340) | Curve25519 library | twisted Edwards coordinates | (0, 1) = ∞ | -- cgit v1.2.3 From 0ba1a337724893c9b0da950c4dddfc1ee736b4f7 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 29 Jun 2016 03:26:18 -0400 Subject: Update crypto-defects.md --- crypto-defects.md | 1 + 1 file changed, 1 insertion(+) diff --git a/crypto-defects.md b/crypto-defects.md index 1a7ecdc8c..bcaf7e84c 100644 --- a/crypto-defects.md +++ b/crypto-defects.md @@ -14,3 +14,4 @@ appearing in our code. | [invalid-curve](http://euklid.org/pdf/ECC_Invalid_Curve.pdf) | NIST ECDH | irrelevant | not onCurve | | [donna#8edc799f](https://github.com/agl/curve25519-donna/commit/2647eeba59fb628914c79ce691df794a8edc799f) | F25519 internal to wire | 32-bit pseudo-Mersenne, C | non-canonical | | [end-to-end#340](https://github.com/google/end-to-end/issues/340) | Curve25519 library | twisted Edwards coordinates | (0, 1) = ∞ | +| [CVE-2006-4339](https://web.archive.org/web/20071010042708/http://www.imc.org/ietf-openpgp/mail-archive/msg14307.html) | RSA-PKCS-1 sig. verification | irrelevant | padding check | -- cgit v1.2.3 From 5e85d15452a3c2cd2d79fcbd117427e040c7bd1d Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 29 Jun 2016 03:34:37 -0400 Subject: Update crypto-defects.md --- crypto-defects.md | 1 + 1 file changed, 1 insertion(+) diff --git a/crypto-defects.md b/crypto-defects.md index bcaf7e84c..90675d3d0 100644 --- a/crypto-defects.md +++ b/crypto-defects.md @@ -15,3 +15,4 @@ appearing in our code. | [donna#8edc799f](https://github.com/agl/curve25519-donna/commit/2647eeba59fb628914c79ce691df794a8edc799f) | F25519 internal to wire | 32-bit pseudo-Mersenne, C | non-canonical | | [end-to-end#340](https://github.com/google/end-to-end/issues/340) | Curve25519 library | twisted Edwards coordinates | (0, 1) = ∞ | | [CVE-2006-4339](https://web.archive.org/web/20071010042708/http://www.imc.org/ietf-openpgp/mail-archive/msg14307.html) | RSA-PKCS-1 sig. verification | irrelevant | padding check | +| [CVE-2014-3570](https://www.openssl.org/news/secadv/20150108.txt) | Bignum squaring | | | -- cgit v1.2.3 From 303fffc1e9ec910cd560a8d7917ab1b3c1e94707 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 29 Jun 2016 03:40:18 -0400 Subject: Update crypto-defects.md --- crypto-defects.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/crypto-defects.md b/crypto-defects.md index 90675d3d0..f8cf52053 100644 --- a/crypto-defects.md +++ b/crypto-defects.md @@ -16,3 +16,5 @@ appearing in our code. | [end-to-end#340](https://github.com/google/end-to-end/issues/340) | Curve25519 library | twisted Edwards coordinates | (0, 1) = ∞ | | [CVE-2006-4339](https://web.archive.org/web/20071010042708/http://www.imc.org/ietf-openpgp/mail-archive/msg14307.html) | RSA-PKCS-1 sig. verification | irrelevant | padding check | | [CVE-2014-3570](https://www.openssl.org/news/secadv/20150108.txt) | Bignum squaring | | | + +Not covered in the above list: memory mismanagement (buffer overrun, use-after-free, uninitialized read, null dereference), timing attacks (branch, cache, instruction). While these issues are very important, there are good programming disciplines for avoiding them without verifying intricate details of the computation. -- cgit v1.2.3 From 356cfb3832beca3de175d8f4070ba3d99fb9a8aa Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 29 Jun 2016 10:57:32 -0700 Subject: Clear symmetric duplicates in clear_algebraic_duplicates --- src/Algebra.v | 26 ++++++++++++++++++++++++-- 1 file changed, 24 insertions(+), 2 deletions(-) diff --git a/src/Algebra.v b/src/Algebra.v index c3b0434cf..81d1b102b 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -878,19 +878,41 @@ Ltac field_simplify_eq_hyps := Ltac field_simplify_eq_all := field_simplify_eq_hyps; try field_simplify_eq. -(** Clear duplicate hypotheses, and hypotheses of the form [R x x] for a reflexive relation [R] *) +(** Clear duplicate hypotheses, and hypotheses of the form [R x x] for a reflexive relation [R], and similarly for symmetric relations *) Ltac clear_algebraic_duplicates_step R := match goal with | [ H : R ?x ?x |- _ ] => clear H end. +Ltac clear_algebraic_duplicates_step_S R := + match goal with + | [ H : R ?x ?y, H' : R ?y ?x |- _ ] + => clear H + | [ H : not (R ?x ?y), H' : not (R ?y ?x) |- _ ] + => clear H + | [ H : (R ?x ?y -> False)%type, H' : (R ?y ?x -> False)%type |- _ ] + => clear H + | [ H : not (R ?x ?y), H' : (R ?y ?x -> False)%type |- _ ] + => clear H + end. Ltac clear_algebraic_duplicates_guarded R := let test_reflexive := constr:(_ : Reflexive R) in repeat clear_algebraic_duplicates_step R. +Ltac clear_algebraic_duplicates_guarded_S R := + let test_symmetric := constr:(_ : Symmetric R) in + repeat clear_algebraic_duplicates_step_S R. Ltac clear_algebraic_duplicates := clear_duplicates; repeat match goal with - | [ H : ?R ?x ?x |- _ ] => clear_algebraic_duplicates_guarded R + | [ H : ?R ?x ?x |- _ ] => progress clear_algebraic_duplicates_guarded R + | [ H : ?R ?x ?y, H' : ?R ?y ?x |- _ ] + => progress clear_algebraic_duplicates_guarded_S R + | [ H : not (?R ?x ?y), H' : not (?R ?y ?x) |- _ ] + => progress clear_algebraic_duplicates_guarded_S R + | [ H : not (?R ?x ?y), H' : (?R ?y ?x -> False)%type |- _ ] + => progress clear_algebraic_duplicates_guarded_S R + | [ H : (?R ?x ?y -> False)%type, H' : (?R ?y ?x -> False)%type |- _ ] + => progress clear_algebraic_duplicates_guarded_S R end. (*** Inequalities over fields *) -- cgit v1.2.3 From b707a3012eb219de8b3575c84f9e312b4007e4aa Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 29 Jun 2016 13:13:04 -0700 Subject: Handle fractions in denominators This should deal with #16 / https://github.com/mit-plv/fiat-crypto/pull/16#discussion_r69009776 --- src/Algebra.v | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/src/Algebra.v b/src/Algebra.v index 81d1b102b..c0f3b1fba 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -732,15 +732,10 @@ Ltac set_nonfraction_pieces_on T eq zero opp add sub mul inv div nonzero_tac con | appcontext[div] => lazymatch T with | div ?numerator ?denominator - => let d := fresh "d" in - pose denominator as d; - cut (not (eq d zero)); + => cut (not (eq denominator zero)); [ intro; - set_nonfraction_pieces_on - numerator eq zero opp add sub mul inv div nonzero_tac - ltac:(fun numerator' - => cont (div numerator' d)) - | subst d; nonzero_tac ] + two_arg_recr div numerator denominator + | nonzero_tac ] | opp ?x => one_arg_recr opp x | inv ?x => one_arg_recr inv x | add ?x ?y => two_arg_recr add x y -- cgit v1.2.3 From ae61d5234567ab7cf8476244d6dec6f99a03da4d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 29 Jun 2016 13:20:54 -0700 Subject: Allow side-conditions in common denom. all in hyps This should handle #16 / https://github.com/mit-plv/fiat-crypto/pull/16#discussion_r69009840 --- src/Algebra.v | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/src/Algebra.v b/src/Algebra.v index c0f3b1fba..19a536807 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -841,14 +841,30 @@ Ltac conservative_common_denominator_inequality := | let HG := fresh in intros HG; apply H'; conservative_common_denominator_in HG; [ eexact HG | .. ] ]. +Ltac conservative_common_denominator_hyps := + try match goal with + | [H: _ |- _ ] + => progress conservative_common_denominator_in H; + [ conservative_common_denominator_hyps + | .. ] + end. + +Ltac conservative_common_denominator_inequality_hyps := + try match goal with + | [H: _ |- _ ] + => progress conservative_common_denominator_inequality_in H; + [ conservative_common_denominator_inequality_hyps + | .. ] + end. + Ltac conservative_common_denominator_all := try conservative_common_denominator; - [ repeat match goal with [H: _ |- _ ] => progress conservative_common_denominator_in H; [] end + [ try conservative_common_denominator_hyps | .. ]. Ltac conservative_common_denominator_inequality_all := try conservative_common_denominator_inequality; - [ repeat match goal with [H: _ |- _ ] => progress conservative_common_denominator_inequality_in H; [] end + [ try conservative_common_denominator_inequality_hyps | .. ]. Ltac conservative_common_denominator_equality_inequality_all := -- cgit v1.2.3 From f729e58d23663c7bab0332e01e72e8c47ab5d8b3 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 29 Jun 2016 13:51:20 -0700 Subject: Fix [only_two_square_roots] to not loop It was previously posing hypotheses that were algebraic duplicates of existing hypotheses, and then clearing them. --- src/Algebra.v | 56 ++++++++++++++++++++++++++++++++++++++++---------------- 1 file changed, 40 insertions(+), 16 deletions(-) diff --git a/src/Algebra.v b/src/Algebra.v index 19a536807..79b153352 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -1092,17 +1092,37 @@ Section ExtraLemmas. End ExtraLemmas. (** We look for hypotheses of the form [x^2 = y^2] and [x^2 = z] together with [y^2 = z], and prove that [x = y] or [x = opp y] *) -Ltac pose_proof_only_two_square_roots x y H := +Ltac pose_proof_only_two_square_roots x y H eq opp mul := not constr_eq x y; - match goal with - | [ H' : ?eq (?mul x x) (?mul y y) |- _ ] - => pose proof (only_two_square_roots'_choice x y H') as H - | [ H0 : ?eq (?mul x x) ?z, H1 : ?eq (?mul y y) ?z |- _ ] - => pose proof (only_two_square_roots_choice x y z H0 H1) as H + lazymatch x with + | opp ?x' => pose_proof_only_two_square_roots x' y H eq opp mul + | _ + => lazymatch y with + | opp ?y' => pose_proof_only_two_square_roots x y' H eq opp mul + | _ + => match goal with + | [ H' : eq x y |- _ ] + => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T + | [ H' : eq y x |- _ ] + => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T + | [ H' : eq x (opp y) |- _ ] + => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T + | [ H' : eq y (opp x) |- _ ] + => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T + | [ H' : eq (opp x) y |- _ ] + => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T + | [ H' : eq (opp y) x |- _ ] + => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T + | [ H' : eq (mul x x) (mul y y) |- _ ] + => pose proof (only_two_square_roots'_choice x y H') as H + | [ H0 : eq (mul x x) ?z, H1 : eq (mul y y) ?z |- _ ] + => pose proof (only_two_square_roots_choice x y z H0 H1) as H + end + end end. -Ltac reduce_only_two_square_roots x y := +Ltac reduce_only_two_square_roots x y eq opp mul := let H := fresh in - pose_proof_only_two_square_roots x y H; + pose_proof_only_two_square_roots x y H eq opp mul; destruct H; try setoid_subst y. Ltac pre_clean_only_two_square_roots := @@ -1116,21 +1136,25 @@ Ltac post_clean_only_two_square_roots x y := | [ H : (?R ?x ?x -> False)%type |- _ ] => exfalso; apply H; reflexivity end); try setoid_subst x; try setoid_subst y. -Ltac only_two_square_roots_step := +Ltac only_two_square_roots_step eq opp mul := match goal with - | [ H : not (?eq ?x (?opp ?y)) |- _ ] + | [ H : not (eq ?x (opp ?y)) |- _ ] (* this one comes first, because it the procedure is asymmetric with respect to [x] and [y], and this order is more likely to lead to solving goals by contradiction. *) - => is_var x; is_var y; reduce_only_two_square_roots x y; post_clean_only_two_square_roots x y - | [ H : ?eq (?mul ?x ?x) (?mul ?y ?y) |- _ ] - => reduce_only_two_square_roots x y; post_clean_only_two_square_roots x y - | [ H : ?eq (?mul ?x ?x) ?z, H' : ?eq (?mul ?y ?y) ?z |- _ ] - => reduce_only_two_square_roots x y; post_clean_only_two_square_roots x y + => is_var x; is_var y; reduce_only_two_square_roots x y eq opp mul; post_clean_only_two_square_roots x y + | [ H : eq (mul ?x ?x) (mul ?y ?y) |- _ ] + => reduce_only_two_square_roots x y eq opp mul; post_clean_only_two_square_roots x y + | [ H : eq (mul ?x ?x) ?z, H' : eq (mul ?y ?y) ?z |- _ ] + => reduce_only_two_square_roots x y eq opp mul; post_clean_only_two_square_roots x y end. Ltac only_two_square_roots := pre_clean_only_two_square_roots; - repeat only_two_square_roots_step. + let fld := guess_field in + lazymatch type of fld with + | @field ?F ?eq ?zero ?one ?opp ?add ?sub ?mul ?inv ?div + => repeat only_two_square_roots_step eq opp mul + end. Section Example. Context {F zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div}. -- cgit v1.2.3 From 9f3c224e0bb968bebeca8f2d0d74e81517c6e293 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 29 Jun 2016 15:22:34 -0700 Subject: Don't generate goals [False] in conservative_common_denominator_all See also #16, https://github.com/mit-plv/fiat-crypto/pull/16/files/f1744181ad236300cfa9ba7c033684fbdf45a3e9..4e50ef26b9b02c882536281e1c7a0cf013a963d5#r69034941 --- src/Algebra.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/Algebra.v b/src/Algebra.v index 79b153352..771555cb0 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -770,10 +770,12 @@ Ltac set_nonfraction_pieces_by nonzero_tac := ltac:(fun T' => change T'); deduplicate_nonfraction_pieces mul end. +Ltac default_set_nonfraction_nonzero_tac := + try (intro; field_nonzero_mul_split; tauto). Ltac set_nonfraction_pieces_in H := - set_nonfraction_pieces_in_by H ltac:(try (intro; field_nonzero_mul_split; try tauto)). + set_nonfraction_pieces_in_by H default_set_nonfraction_nonzero_tac. Ltac set_nonfraction_pieces := - set_nonfraction_pieces_by ltac:(try (intro; field_nonzero_mul_split; tauto)). + set_nonfraction_pieces_by default_set_nonfraction_nonzero_tac. Ltac conservative_common_denominator_in H := idtac; let fld := guess_field in -- cgit v1.2.3 From 5a8e95df1df511710bee20ac12102338619fc2e4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 29 Jun 2016 15:45:55 -0700 Subject: Simplify conservative_common_denominator We no longer try to predict field_simplify_eq. This results in better behavior and less code which is more modular. In particular, the tactic responsible for hiding non-fraction pieces from field_simplify_eq no longer tries to preemptively assert that denominators are nonzero. This improvement is a result of @andres-erbsen's point in #16, https://github.com/mit-plv/fiat-crypto/pull/16#discussion_r69035102 , that we were generating too many side-conditions. --- src/Algebra.v | 45 ++++++++++++++++++--------------------------- 1 file changed, 18 insertions(+), 27 deletions(-) diff --git a/src/Algebra.v b/src/Algebra.v index 771555cb0..473571824 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -711,31 +711,26 @@ Ltac deduplicate_nonfraction_pieces mul := => subst x0 x1 end. -Ltac set_nonfraction_pieces_on T eq zero opp add sub mul inv div nonzero_tac cont := +Ltac set_nonfraction_pieces_on T eq zero opp add sub mul inv div cont := idtac; let one_arg_recr := fun op v => set_nonfraction_pieces_on - v eq zero opp add sub mul inv div nonzero_tac + v eq zero opp add sub mul inv div ltac:(fun x => cont (op x)) in let two_arg_recr := fun op v0 v1 => set_nonfraction_pieces_on - v0 eq zero opp add sub mul inv div nonzero_tac + v0 eq zero opp add sub mul inv div ltac:(fun x => set_nonfraction_pieces_on - v1 eq zero opp add sub mul inv div nonzero_tac + v1 eq zero opp add sub mul inv div ltac:(fun y => cont (op x y))) in lazymatch T with | eq ?x ?y => two_arg_recr eq x y | appcontext[div] => lazymatch T with - | div ?numerator ?denominator - => cut (not (eq denominator zero)); - [ intro; - two_arg_recr div numerator denominator - | nonzero_tac ] | opp ?x => one_arg_recr opp x | inv ?x => one_arg_recr inv x | add ?x ?y => two_arg_recr add x y @@ -748,34 +743,32 @@ Ltac set_nonfraction_pieces_on T eq zero opp add sub mul inv div nonzero_tac con pose T as x; cont x end. -Ltac set_nonfraction_pieces_in_by H nonzero_tac := +Ltac set_nonfraction_pieces_in H := idtac; let fld := guess_field in lazymatch type of fld with | @field ?T ?eq ?zero ?one ?opp ?add ?sub ?mul ?inv ?div => let T := type of H in set_nonfraction_pieces_on - T eq zero opp add sub mul inv div nonzero_tac + T eq zero opp add sub mul inv div ltac:(fun T' => change T' in H); deduplicate_nonfraction_pieces mul end. -Ltac set_nonfraction_pieces_by nonzero_tac := +Ltac set_nonfraction_pieces := idtac; let fld := guess_field in lazymatch type of fld with | @field ?T ?eq ?zero ?one ?opp ?add ?sub ?mul ?inv ?div => let T := get_goal in set_nonfraction_pieces_on - T eq zero opp add sub mul inv div nonzero_tac + T eq zero opp add sub mul inv div ltac:(fun T' => change T'); deduplicate_nonfraction_pieces mul end. -Ltac default_set_nonfraction_nonzero_tac := - try (intro; field_nonzero_mul_split; tauto). -Ltac set_nonfraction_pieces_in H := - set_nonfraction_pieces_in_by H default_set_nonfraction_nonzero_tac. -Ltac set_nonfraction_pieces := - set_nonfraction_pieces_by default_set_nonfraction_nonzero_tac. +Ltac default_conservative_common_denominator_nonzero_tac := + repeat apply conj; + try first [ assumption + | intro; field_nonzero_mul_split; tauto ]. Ltac conservative_common_denominator_in H := idtac; let fld := guess_field in @@ -786,10 +779,9 @@ Ltac conservative_common_denominator_in H := lazymatch type of H with | appcontext[div] => set_nonfraction_pieces_in H; - [ common_denominator_in H; - [ - | repeat apply conj; try assumption.. ] - | .. ]; + common_denominator_in H; + [ + | default_conservative_common_denominator_nonzero_tac.. ]; repeat match goal with H := _ |- _ => subst H end | ?T => fail 0 "no division in" H ":" T end. @@ -803,10 +795,9 @@ Ltac conservative_common_denominator := lazymatch goal with | |- appcontext[div] => set_nonfraction_pieces; - [ common_denominator; - [ - | repeat apply conj; try assumption.. ] - | .. ]; + common_denominator; + [ + | default_conservative_common_denominator_nonzero_tac.. ]; repeat match goal with H := _ |- _ => subst H end | |- ?G => fail 0 "no division in goal" G -- cgit v1.2.3 From e8214b0c7f02c23016a4e95734cae813e115de76 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 30 Jun 2016 11:39:07 -0700 Subject: Add pow_Zpow to Util.ZUtil I followed the naming scheme of things like div_Zdiv in the stdlib. --- src/Util/ZUtil.v | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index a5716fca4..c6686b63c 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -65,6 +65,12 @@ Proof. rewrite Z2Nat.inj_mul; auto using Z.pow_nonneg. Qed. +Lemma pow_Zpow : forall a n : nat, Z.of_nat (a ^ n) = Z.of_nat a ^ Z.of_nat n. +Proof with auto using Zle_0_nat, Z.pow_nonneg. + intros; apply Z2Nat.inj... + rewrite <- pow_Z2N_Zpow, !Nat2Z.id... +Qed. + Lemma mod_exp_0 : forall a x m, x > 0 -> m > 1 -> a mod m = 0 -> a ^ x mod m = 0. Proof. -- cgit v1.2.3 From 6c6c65eff384182197289797ef58ca78bcfff4dc Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 30 Jun 2016 13:24:23 -0700 Subject: Prove that a ^ k <> 0 --- src/Util/NatUtil.v | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index bc2c8425b..0cdfd784f 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -1,4 +1,5 @@ Require Import Coq.Numbers.Natural.Peano.NPeano Coq.omega.Omega. +Require Import Coq.micromega.Psatz. Import Nat. Local Open Scope nat_scope. @@ -78,3 +79,10 @@ Proof. [ rewrite (proj2 (@beq_nat_true_iff _ _) H); reflexivity | rewrite (proj2 (@beq_nat_false_iff _ _) H); reflexivity ]. Qed. + +Lemma pow_nonzero a k : a <> 0 -> a ^ k <> 0. +Proof. + intro; induction k; simpl; nia. +Qed. + +Hint Resolve pow_nonzero : arith. -- cgit v1.2.3 From 271a8c1a6c53140cf8be6903cedb504d86c9d56f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 30 Jun 2016 15:02:29 -0700 Subject: Add a tactic for making use of destructed let H' := fresh in + rename H into H'; + pose proof (Zlt_cases x y) as H; + rewrite H' in H; + clear H' + end. -- cgit v1.2.3 From 4d9f63c4feab45d2f0701157fb21148dbb85ec0e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 30 Jun 2016 17:23:38 -0700 Subject: Add a classification of n / m < 0 --- src/Util/ZUtil.v | 34 +++++++++++++++++++++++++++++++++- 1 file changed, 33 insertions(+), 1 deletion(-) diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index e0949c933..c20d59d20 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -1,5 +1,5 @@ Require Import Coq.ZArith.Zpower Coq.ZArith.Znumtheory Coq.ZArith.ZArith Coq.ZArith.Zdiv. -Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. +Require Import Coq.omega.Omega Coq.micromega.Psatz Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. Require Import Crypto.Util.NatUtil. Require Import Coq.Lists.List. Import Nat. @@ -490,3 +490,35 @@ Ltac Zltb_to_Zlt := rewrite H' in H; clear H' end. + +Ltac Zcompare_to_sgn := + repeat match goal with + | [ H : _ |- _ ] => progress rewrite <- ?Z.sgn_neg_iff, <- ?Z.sgn_pos_iff, <- ?Z.sgn_null_iff in H + | _ => progress rewrite <- ?Z.sgn_neg_iff, <- ?Z.sgn_pos_iff, <- ?Z.sgn_null_iff + end. + +Local Ltac replace_to_const c := + repeat match goal with + | [ H : ?x = ?x |- _ ] => clear H + | [ H : ?x = c, H' : context[?x] |- _ ] => rewrite H in H' + | [ H : c = ?x, H' : context[?x] |- _ ] => rewrite <- H in H' + | [ H : ?x = c |- context[?x] ] => rewrite H + | [ H : c = ?x |- context[?x] ] => rewrite <- H + end. + +Lemma Zlt_div_0 n m : n / m < 0 <-> ((n < 0 < m \/ m < 0 < n) /\ 0 < -(n / m)). +Proof. + Zcompare_to_sgn; rewrite Z.sgn_opp; simpl. + pose proof (Zdiv_sgn n m) as H. + pose proof (Z.sgn_spec (n / m)) as H'. + repeat first [ progress intuition + | progress simpl in * + | congruence + | lia + | progress replace_to_const (-1) + | progress replace_to_const 0 + | progress replace_to_const 1 + | match goal with + | [ x : Z |- _ ] => destruct x + end ]. +Qed. -- cgit v1.2.3 From 0e8adaa7c1e546f442ac7e0f6d3e81c0e7e985b8 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 30 Jun 2016 17:55:12 -0700 Subject: Add a proof of 2 * x - x = x --- src/Util/ZUtil.v | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index c20d59d20..ebfea8ebd 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -522,3 +522,6 @@ Proof. | [ x : Z |- _ ] => destruct x end ]. Qed. + +Lemma two_times_x_minus_x x : 2 * x - x = x. +Proof. lia. Qed. -- cgit v1.2.3 From f2f2f3e43f8a3058e0f5838d8bd7b24af6c99ac9 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 1 Jul 2016 08:54:23 -0700 Subject: Update .gitignore with lia, nia caches --- .gitignore | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/.gitignore b/.gitignore index f88b441c8..43e314274 100644 --- a/.gitignore +++ b/.gitignore @@ -1,10 +1,12 @@ -.#* -*~ *# *.aux *.d *.glob -Makefile.bak -Makefile.coq *.vio *.vo +*~ +.#* +Makefile.bak +Makefile.coq +lia.cache +nlia.cache -- cgit v1.2.3 From bc17dfef58081caf0862d292e4653d35a8646363 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 1 Jul 2016 08:54:38 -0700 Subject: Add fraction inequality reasoning tactics to ZUtil --- src/Util/ZUtil.v | 120 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 120 insertions(+) diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index ebfea8ebd..6d6039a6d 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -525,3 +525,123 @@ Qed. Lemma two_times_x_minus_x x : 2 * x - x = x. Proof. lia. Qed. + +(** * [Zsimplify_fractions_le] *) +(** The culmination of this series of tactics, + [Zsimplify_fractions_le], will use the fact that [a * (b / c) <= + (a * b) / c], and do some reasoning modulo associativity and + commutativity in [Z] to perform such a reduction. It may leave + over goals if it cannot prove that some denominators are non-zero. + If the rewrite [a * (b / c)] → [(a * b) / c] is safe to do on the + LHS of the goal, this tactic should not turn a solvable goal into + an unsolvable one. + + After running, the tactic does some basic rewriting to simplify + fractions, e.g., that [a * b / b = a]. *) +Ltac Zsplit_sums_step := + match goal with + | [ |- _ + _ <= _ ] + => etransitivity; [ eapply Z.add_le_mono | ] + | [ |- _ - _ <= _ ] + => etransitivity; [ eapply Z.sub_le_mono | ] + end. +Ltac Zpre_reorder_fractions_step := + match goal with + | [ |- context[?x / ?y * ?z] ] + => rewrite (Z.mul_comm (x / y) z) + | _ => let LHS := match goal with |- ?LHS <= ?RHS => LHS end in + match LHS with + | context G[?x * (?y / ?z)] + => let G' := context G[(x * y) / z] in + transitivity G' + end + end. +Ltac Zpre_reorder_fractions := + try first [ Zsplit_sums_step; [ Zpre_reorder_fractions.. | ] + | Zpre_reorder_fractions_step; [ .. | Zpre_reorder_fractions ] ]. +Ltac Zsplit_comparison := + match goal with + | [ |- ?x <= ?x ] => reflexivity + | [ H : _ >= _ |- _ ] + => apply Z.ge_le_iff in H + | [ |- ?x * ?y <= ?z * ?w ] + => lazymatch goal with + | [ H : 0 <= x |- _ ] => idtac + | [ H : x < 0 |- _ ] => fail + | _ => destruct (Z_lt_le_dec x 0) + end; + [ .. + | lazymatch goal with + | [ H : 0 <= y |- _ ] => idtac + | [ H : y < 0 |- _ ] => fail + | _ => destruct (Z_lt_le_dec y 0) + end; + [ .. + | apply Zmult_le_compat; [ | | assumption | assumption ] ] ] + | [ |- ?x / ?y <= ?z / ?y ] + => lazymatch goal with + | [ H : 0 < y |- _ ] => idtac + | [ H : y <= 0 |- _ ] => fail + | _ => destruct (Z_lt_le_dec 0 y) + end; + [ apply Z_div_le; [ apply gt_lt_symmetry; assumption | ] + | .. ] + | [ |- ?x / ?y <= ?x / ?z ] + => lazymatch goal with + | [ H : 0 <= x |- _ ] => idtac + | [ H : x < 0 |- _ ] => fail + | _ => destruct (Z_lt_le_dec x 0) + end; + [ .. + | lazymatch goal with + | [ H : 0 < z |- _ ] => idtac + | [ H : z <= 0 |- _ ] => fail + | _ => destruct (Z_lt_le_dec 0 z) + end; + [ apply Z.div_le_compat_l; [ assumption | split; [ assumption | ] ] + | .. ] ] + | [ |- _ + _ <= _ + _ ] + => apply Z.add_le_mono + | [ |- _ - _ <= _ - _ ] + => apply Z.sub_le_mono + | [ |- ?x * (?y / ?z) <= (?x * ?y) / ?z ] + => apply Z.div_mul_le + end. +Ltac Zsplit_comparison_fin_step := + match goal with + | _ => assumption + | _ => lia + | _ => progress subst + | [ H : ?n * ?m < 0 |- _ ] + => apply (proj1 (Z.lt_mul_0 n m)) in H; destruct H as [[??]|[??]] + | [ H : ?n / ?m < 0 |- _ ] + => apply (proj1 (Zlt_div_0 n m)) in H; destruct H as [[[??]|[??]]?] + | [ H : (?x^?y) <= ?n < _, H' : ?n < 0 |- _ ] + => assert (0 <= x^y) by zero_bounds; lia + | [ H : (?x^?y) < 0 |- _ ] + => assert (0 <= x^y) by zero_bounds; lia + | [ H : (?x^?y) <= 0 |- _ ] + => let H' := fresh in + assert (H' : 0 <= x^y) by zero_bounds; + assert (x^y = 0) by lia; + clear H H' + | [ H : _^_ = 0 |- _ ] + => apply Z.pow_eq_0_iff in H; destruct H as [?|[??]] + | [ H : 0 <= ?x, H' : ?x - 1 < 0 |- _ ] + => assert (x = 0) by lia; clear H H' + | [ |- ?x <= ?y ] => is_evar x; reflexivity + | [ |- ?x <= ?y ] => is_evar y; reflexivity + end. +Ltac Zsplit_comparison_fin := repeat Zsplit_comparison_fin_step. +Ltac Zsimplify_fractions_step := + match goal with + | _ => rewrite Z.div_mul by (try apply Z.pow_nonzero; zero_bounds) + | [ |- context[?x * ?y / ?x] ] + => rewrite (Z.mul_comm x y) + | [ |- ?x <= ?x ] => reflexivity + end. +Ltac Zsimplify_fractions := repeat Zsimplify_fractions_step. +Ltac Zsimplify_fractions_le := + Zpre_reorder_fractions; + [ repeat Zsplit_comparison; Zsplit_comparison_fin; zero_bounds.. + | Zsimplify_fractions ]. -- cgit v1.2.3 From bb37a1f7f16731b4a6d393fc113bdf5348a5ad78 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 1 Jul 2016 09:12:28 -0700 Subject: Add more caches to .gitignore (nra, csdp) --- .gitignore | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.gitignore b/.gitignore index 43e314274..b8cf1d4bc 100644 --- a/.gitignore +++ b/.gitignore @@ -8,5 +8,7 @@ .#* Makefile.bak Makefile.coq +csdp.cache lia.cache nlia.cache +nra.cache -- cgit v1.2.3 From 4cb63acdb7ea7e98d124274fec85d1a10d86d38d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 1 Jul 2016 09:12:41 -0700 Subject: Add tactic to split sums and differences in inequalities --- src/Util/ZUtil.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 6d6039a6d..84d9ed3da 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -545,6 +545,8 @@ Ltac Zsplit_sums_step := | [ |- _ - _ <= _ ] => etransitivity; [ eapply Z.sub_le_mono | ] end. +Ltac Zsplit_sums := + try (Zsplit_sums_step; [ Zsplit_sums | ]). Ltac Zpre_reorder_fractions_step := match goal with | [ |- context[?x / ?y * ?z] ] -- cgit v1.2.3 From cb75fd18fba514577fb465d84e31ae9c6787bcd1 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 1 Jul 2016 09:13:52 -0700 Subject: Fix a typo in Zsplit_sums --- src/Util/ZUtil.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 84d9ed3da..095d418a8 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -546,7 +546,7 @@ Ltac Zsplit_sums_step := => etransitivity; [ eapply Z.sub_le_mono | ] end. Ltac Zsplit_sums := - try (Zsplit_sums_step; [ Zsplit_sums | ]). + try (Zsplit_sums_step; [ Zsplit_sums.. | ]). Ltac Zpre_reorder_fractions_step := match goal with | [ |- context[?x / ?y * ?z] ] -- cgit v1.2.3 From aa46e457493b121e4a26076296740f70308eaf0f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 1 Jul 2016 10:41:47 -0700 Subject: Add [specialize_by] tactic --- src/Util/Tactics.v | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index abfc2499c..304ae3c20 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -229,6 +229,15 @@ Ltac destruct_sig_matcher HT := Ltac destruct_sig := destruct_all_matches destruct_sig_matcher. Ltac destruct_sig' := destruct_all_matches' destruct_sig_matcher. +(** try to specialize all non-dependent hypotheses using [tac] *) +Ltac specialize_by' tac := + idtac; + match goal with + | [ H : ?A -> ?B |- _ ] => let H' := fresh in assert (H' : A) by tac; specialize (H H'); clear H' + end. + +Ltac specialize_by tac := repeat specialize_by' tac. + (** If [tac_in H] operates in [H] and leaves side-conditions before the original goal, then [side_conditions_before_to_side_conditions_after tac_in H] does -- cgit v1.2.3 From bcc95258fa71e0ea75811227e31a3d8ef6349688 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 1 Jul 2016 11:58:24 -0700 Subject: Add some proofs about Z.div and Z.mul --- src/Util/ZUtil.v | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 095d418a8..c7671fae5 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -526,6 +526,40 @@ Qed. Lemma two_times_x_minus_x x : 2 * x - x = x. Proof. lia. Qed. +Lemma Zmul_div_le x y z + (Hx : 0 <= x) (Hy : 0 <= y) (Hz : 0 < z) + (Hyz : y <= z) + : x * y / z <= x. +Proof. + transitivity (x * z / z); [ | rewrite Z.div_mul by lia; lia ]. + apply Z_div_le; nia. +Qed. + +Lemma Zdiv_mul_diff a b c + (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c) + : c * a / b - c * (a / b) <= c. +Proof. + pose proof (Z.mod_pos_bound a b). + etransitivity; [ | apply (Zmul_div_le c (a mod b) b); lia ]. + rewrite (Z_div_mod_eq a b) at 1 by lia. + rewrite Z.mul_add_distr_l. + replace (c * (b * (a / b))) with ((c * (a / b)) * b) by lia. + rewrite Z.div_add_l by lia. + lia. +Qed. + +Lemma Zdiv_mul_le_le a b c + : 0 <= a -> 0 < b -> 0 <= c -> c * (a / b) <= c * a / b <= c * (a / b) + c. +Proof. + pose proof (Zdiv_mul_diff a b c); split; try apply Z.div_mul_le; lia. +Qed. + +Lemma Zdiv_mul_le_le_offset a b c + : 0 <= a -> 0 < b -> 0 <= c -> c * a / b - c <= c * (a / b). +Proof. + pose proof (Zdiv_mul_le_le a b c); lia. +Qed. + (** * [Zsimplify_fractions_le] *) (** The culmination of this series of tactics, [Zsimplify_fractions_le], will use the fact that [a * (b / c) <= -- cgit v1.2.3 From c5dbca9cda9dc02f9d8d946e7ae304aa7b5d1d41 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 1 Jul 2016 14:51:41 -0700 Subject: Add hint databases and a proof about Z.log2 --- src/Util/ZUtil.v | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index c7671fae5..42432cd18 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -5,6 +5,14 @@ Require Import Coq.Lists.List. Import Nat. Local Open Scope Z. +Hint Extern 1 => lia : lia. +Hint Extern 1 => lra : lra. +Hint Extern 1 => nra : nra. +Hint Extern 1 => nia : nia. +Hint Extern 1 => omega : omega. +Hint Resolve Z.log2_nonneg : zarith. +Hint Resolve Z.pow_neg_r Z.pow_0_l : zarith. + Lemma gt_lt_symmetry: forall n m, n > m <-> m < n. Proof. intros; split; omega. @@ -411,6 +419,8 @@ Ltac zero_bounds' := Ltac zero_bounds := try omega; try prime_bound; zero_bounds'. +Hint Extern 1 => progress zero_bounds : zero_bounds. + Lemma Z_ones_nonneg : forall i, (0 <= i) -> 0 <= Z.ones i. Proof. apply natlike_ind. @@ -681,3 +691,26 @@ Ltac Zsimplify_fractions_le := Zpre_reorder_fractions; [ repeat Zsplit_comparison; Zsplit_comparison_fin; zero_bounds.. | Zsimplify_fractions ]. + +Lemma Zlog2_nonneg' n a : n <= 0 -> n <= Z.log2 a. +Proof. + intros; transitivity 0; auto with zarith. +Qed. + +Hint Resolve Zlog2_nonneg' : zarith. + +(** We create separate databases for two directions of transformations + involving [Z.log2]; combining them leads to loops. *) +(* for hints that take in hypotheses of type [log2 _], and spit out conclusions of type [_ ^ _] *) +Create HintDb hyp_log2. + +(* for hints that take in hypotheses of type [_ ^ _], and spit out conclusions of type [log2 _] *) +Create HintDb concl_log2. + +Hint Resolve (fun a b H => proj1 (Z.log2_lt_pow2 a b H)) (fun a b H => proj1 (Z.log2_le_pow2 a b H)) : concl_log2. +Hint Resolve (fun a b H => proj2 (Z.log2_lt_pow2 a b H)) (fun a b H => proj2 (Z.log2_le_pow2 a b H)) : hyp_log2. + +Lemma Zle_lt_to_log2 x y z : 0 <= z -> 0 < y -> 2^x <= y < 2^z -> x <= Z.log2 y < z. +Proof. + destruct (Z_le_gt_dec 0 x); auto with concl_log2 lia. +Qed. -- cgit v1.2.3 From a0a909c0f9f99379b976aa1c348cc473c19d45c3 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 1 Jul 2016 14:56:10 -0700 Subject: Simplify a proof that no longer needs more hints [intuition] is overpowered and does [auto with *] or something --- src/BaseSystem.v | 1 - 1 file changed, 1 deletion(-) diff --git a/src/BaseSystem.v b/src/BaseSystem.v index 1985520f0..743cdfde8 100644 --- a/src/BaseSystem.v +++ b/src/BaseSystem.v @@ -136,7 +136,6 @@ Section PolynomialBaseCoefs. with (Z.pos b1); auto. rewrite Z_div_mult_full; auto. apply Z.pow_nonzero; intuition. - pose proof (Zgt_pos_0 b1); omega. Qed. Lemma poly_base_good: -- cgit v1.2.3 From 329da1d4a17814a2f6cb79e9a022bbb5aa65fed4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 1 Jul 2016 15:19:38 -0700 Subject: Add more hints to ZUtil --- src/Util/ZUtil.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 42432cd18..ecfc89974 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -13,6 +13,13 @@ Hint Extern 1 => omega : omega. Hint Resolve Z.log2_nonneg : zarith. Hint Resolve Z.pow_neg_r Z.pow_0_l : zarith. +(** Only hints that are always safe to apply (i.e., reversible), and + which can reasonably be said to "simplify" the goal, should go in + this database. *) +Create HintDb zsimplify discriminated. +Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r : zsimplify. +Hint Rewrite Z.div_mul Z.div_1_l using lia : zsimplify. + Lemma gt_lt_symmetry: forall n m, n > m <-> m < n. Proof. intros; split; omega. @@ -58,6 +65,8 @@ Lemma Z_div_mul' : forall a b : Z, b <> 0 -> (b * a) / b = a. intros. rewrite Z.mul_comm. apply Z.div_mul; auto. Qed. +Hint Rewrite Z_div_mul' using lia : zsimplify. + Lemma Zgt0_neq0 : forall x, x > 0 -> x <> 0. intuition. Qed. @@ -714,3 +723,11 @@ Lemma Zle_lt_to_log2 x y z : 0 <= z -> 0 < y -> 2^x <= y < 2^z -> x <= Z.log2 y Proof. destruct (Z_le_gt_dec 0 x); auto with concl_log2 lia. Qed. + +Lemma Zdiv_x_y_x x y : 0 < x -> 0 < y -> x / y / x = 1 / y. +Proof. + intros; rewrite Z.div_div, (Z.mul_comm y x), <- Z.div_div, Z.div_same by lia. + reflexivity. +Qed. + +Hint Rewrite Zdiv_x_y_x using lia : zsimplify. -- cgit v1.2.3 From 4018e56dc068a674b89d43acc842086a9b4527b5 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 1 Jul 2016 16:43:16 -0700 Subject: Add more ZUtil hints --- src/Util/ZUtil.v | 111 +++++++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 107 insertions(+), 4 deletions(-) diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index ecfc89974..38243c9de 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -10,15 +10,32 @@ Hint Extern 1 => lra : lra. Hint Extern 1 => nra : nra. Hint Extern 1 => nia : nia. Hint Extern 1 => omega : omega. -Hint Resolve Z.log2_nonneg : zarith. -Hint Resolve Z.pow_neg_r Z.pow_0_l : zarith. +Hint Resolve Z.log2_nonneg Z.div_small Z.mod_small Z.pow_neg_r Z.pow_0_l : zarith. +Hint Resolve (fun a b H => proj1 (Z.mod_pos_bound a b H)) (fun a b H => proj2 (Z.mod_pos_bound a b H)) : zarith. (** Only hints that are always safe to apply (i.e., reversible), and which can reasonably be said to "simplify" the goal, should go in this database. *) Create HintDb zsimplify discriminated. -Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r : zsimplify. -Hint Rewrite Z.div_mul Z.div_1_l using lia : zsimplify. +Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r : zsimplify. +Hint Rewrite Z.div_mul Z.div_1_l Z.div_same Z.mod_same Z.div_small Z.mod_small using lia : zsimplify. + +(** "push" means transform [-f x] to [f (-x)]; "pull" means go the other way *) +Hint Rewrite Z.div_opp_l_nz Z.div_opp_l_z using lia : pull_Zopp. +Hint Rewrite Z.mul_opp_l : pull_Zopp. +Hint Rewrite <- Z.opp_add_distr : pull_Zopp. +Hint Rewrite <- Z.div_opp_l_nz Z.div_opp_l_z using lia : push_Zopp. +Hint Rewrite <- Z.mul_opp_l : push_Zopp. +Hint Rewrite Z.opp_add_distr : push_Zopp. + +(** For the occasional lemma that can remove the use of [Z.div] *) +Create HintDb zstrip_div. +Hint Rewrite Z.div_small_iff using lia : zstrip_div. + +(** It's not clear that [mod] is much easier for [lia] than [Z.div], + so we separate out the transformations between [mod] and [div]. + We'll put, e.g., [mul_div_eq] into it below. *) +Create HintDb zstrip_div. Lemma gt_lt_symmetry: forall n m, n > m <-> m < n. Proof. @@ -184,6 +201,16 @@ Proof. ring. Qed. +Lemma mul_div_eq' : (forall a m, m > 0 -> (a / m) * m = (a - a mod m))%Z. +Proof. + intros. + rewrite (Z_div_mod_eq a m) at 2 by auto. + ring. +Qed. + +Hint Rewrite mul_div_eq mul_div_eq' using lia : zdiv_to_mod. +Hint Rewrite <- mul_div_eq' using lia : zmod_to_div. + Ltac prime_bound := match goal with | [ H : prime ?p |- _ ] => pose proof (prime_ge_2 p H); try omega end. @@ -731,3 +758,79 @@ Proof. Qed. Hint Rewrite Zdiv_x_y_x using lia : zsimplify. + +Lemma Zmod_opp_l_z_iff a b (H : b <> 0) : a mod b = 0 <-> (-a) mod b = 0. +Proof. + split; intro H'; apply Z.mod_opp_l_z in H'; rewrite ?Z.opp_involutive in H'; assumption. +Qed. + +Lemma Zopp_eq_0_iff a : -a = 0 <-> a = 0. +Proof. lia. Qed. + +Hint Rewrite <- Zmod_opp_l_z_iff using lia : zsimplify. +Hint Rewrite Zopp_eq_0_iff : zsimplify. + +Lemma Zsub_pos_bound a b X : 0 <= a < X -> 0 <= b < X -> -X < a - b < X. +Proof. lia. Qed. + +Lemma Zdiv_opp_l_complete a b (Hb : b <> 0) : -a/b = -(a/b) - (if Z_zerop (a mod b) then 0 else 1). +Proof. + destruct (Z_zerop (a mod b)); autorewrite with zsimplify push_Zopp; reflexivity. +Qed. + +Lemma Zdiv_opp_l_complete' a b (Hb : b <> 0) : -(a/b) = -a/b + (if Z_zerop (a mod b) then 0 else 1). +Proof. + destruct (Z_zerop (a mod b)); autorewrite with zsimplify pull_Zopp; lia. +Qed. + +Hint Rewrite Zdiv_opp_l_complete using lia : pull_Zopp. +Hint Rewrite Zdiv_opp_l_complete' using lia : push_Zopp. + +Lemma Zdiv_opp a : a <> 0 -> -a / a = -1. +Proof. + intros; autorewrite with pull_Zopp zsimplify; lia. +Qed. + +Hint Rewrite Zdiv_opp using lia : zsimplify. + +Lemma Zdiv_sub_1_0 x : x > 0 -> (x - 1) / x = 0. +Proof. auto with zarith lia. Qed. + +Hint Rewrite Zdiv_sub_1_0 using lia : zsimplify. + +Lemma Zsub_pos_bound_div a b X : 0 <= a < X -> 0 <= b < X -> -1 <= (a - b) / X <= 0. +Proof. + intros H0 H1; pose proof (Zsub_pos_bound a b X H0 H1). + assert (Hn : -X <= a - b) by lia. + assert (Hp : a - b <= X - 1) by lia. + split; etransitivity; [ | apply Z_div_le, Hn; lia | apply Z_div_le, Hp; lia | ]; + autorewrite with zsimplify; reflexivity. +Qed. + +Hint Resolve (fun a b X H0 H1 => proj1 (Zsub_pos_bound_div a b X H0 H1)) + (fun a b X H0 H1 => proj1 (Zsub_pos_bound_div a b X H0 H1)) : zarith. + +Lemma Zsub_pos_bound_div_eq a b X : 0 <= a < X -> 0 <= b < X -> (a - b) / X = if a 0); [ lia | ]. + autorewrite with zstrip_div; auto with zarith lia. } + { autorewrite with zstrip_div; auto with zarith lia. } +Qed. + +Lemma Zadd_opp_pos_bound_div_eq a b X : 0 <= a < X -> 0 <= b < X -> (-b + a) / X = if a 0 = a / b. +Proof. intros; symmetry; apply Z.div_small; assumption. Qed. + +Lemma Zmod_small_sym a b : 0 <= a < b -> a = a mod b. +Proof. intros; symmetry; apply Z.mod_small; assumption. Qed. + +Hint Resolve Zdiv_small_sym Zmod_small_sym : zarith. -- cgit v1.2.3 From 9b09171338170bb63020029ace9e3ab79c358334 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 1 Jul 2016 17:30:58 -0700 Subject: Add more hints in ZUtil --- src/Util/ZUtil.v | 32 ++++++++++++++++++++++++++++++-- 1 file changed, 30 insertions(+), 2 deletions(-) diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 38243c9de..f2e07ee4b 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -7,7 +7,6 @@ Local Open Scope Z. Hint Extern 1 => lia : lia. Hint Extern 1 => lra : lra. -Hint Extern 1 => nra : nra. Hint Extern 1 => nia : nia. Hint Extern 1 => omega : omega. Hint Resolve Z.log2_nonneg Z.div_small Z.mod_small Z.pow_neg_r Z.pow_0_l : zarith. @@ -18,9 +17,11 @@ Hint Resolve (fun a b H => proj1 (Z.mod_pos_bound a b H)) (fun a b H => proj2 (Z this database. *) Create HintDb zsimplify discriminated. Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r : zsimplify. -Hint Rewrite Z.div_mul Z.div_1_l Z.div_same Z.mod_same Z.div_small Z.mod_small using lia : zsimplify. +Hint Rewrite Z.div_mul Z.div_1_l Z.div_same Z.mod_same Z.div_small Z.mod_small Z.div_add Z.div_add_l using lia : zsimplify. (** "push" means transform [-f x] to [f (-x)]; "pull" means go the other way *) +Create HintDb push_Zopp discriminated. +Create HintDb pull_Zopp discriminated. Hint Rewrite Z.div_opp_l_nz Z.div_opp_l_z using lia : pull_Zopp. Hint Rewrite Z.mul_opp_l : pull_Zopp. Hint Rewrite <- Z.opp_add_distr : pull_Zopp. @@ -28,6 +29,11 @@ Hint Rewrite <- Z.div_opp_l_nz Z.div_opp_l_z using lia : push_Zopp. Hint Rewrite <- Z.mul_opp_l : push_Zopp. Hint Rewrite Z.opp_add_distr : push_Zopp. +Create HintDb push_Zmul discriminated. +Create HintDb pull_Zmul discriminated. +Hint Rewrite Z.mul_add_distr_l Z.mul_add_distr_r Z.mul_sub_distr_l Z.mul_sub_distr_r : push_Zmul. +Hint Rewrite <- Z.mul_add_distr_l Z.mul_add_distr_r Z.mul_sub_distr_l Z.mul_sub_distr_r : pull_Zmul. + (** For the occasional lemma that can remove the use of [Z.div] *) Create HintDb zstrip_div. Hint Rewrite Z.div_small_iff using lia : zstrip_div. @@ -834,3 +840,25 @@ Lemma Zmod_small_sym a b : 0 <= a < b -> a = a mod b. Proof. intros; symmetry; apply Z.mod_small; assumption. Qed. Hint Resolve Zdiv_small_sym Zmod_small_sym : zarith. + +Lemma Zdiv_add' a b c : c <> 0 -> (a + c * b) / c = a / c + b. +Proof. intro; rewrite <- Z.div_add, (Z.mul_comm c); try lia. Qed. + +Lemma Zdiv_add_l' a b c : b <> 0 -> (b * a + c) / b = a + c / b. +Proof. intro; rewrite <- Z.div_add_l, (Z.mul_comm b); lia. Qed. + +Hint Rewrite Zdiv_add_l' Zdiv_add' using lia : zsimplify. + +Lemma Zdiv_mul_skip a b k : 0 < b -> 0 < k -> a * b / k / b = a / k. +Proof. + intros; rewrite Z.div_div, (Z.mul_comm k), <- Z.div_div by lia. + autorewrite with zsimplify; reflexivity. +Qed. + +Lemma Zdiv_mul_skip' a b k : 0 < b -> 0 < k -> b * a / k / b = a / k. +Proof. + intros; rewrite Z.div_div, (Z.mul_comm k), <- Z.div_div by lia. + autorewrite with zsimplify; reflexivity. +Qed. + +Hint Rewrite Zdiv_mul_skip Zdiv_mul_skip' using lia : zsimplify. -- cgit v1.2.3 From d67a1312959e1ce64bcc608d0c360efc3dc6f5b3 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 1 Jul 2016 18:15:48 -0700 Subject: Add more hints to ZUtil --- src/Util/ZUtil.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index f2e07ee4b..21456fea9 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -849,6 +849,20 @@ Proof. intro; rewrite <- Z.div_add_l, (Z.mul_comm b); lia. Qed. Hint Rewrite Zdiv_add_l' Zdiv_add' using lia : zsimplify. +Lemma Zdiv_add_sub_l a b c d : b <> 0 -> (a * b + c - d) / b = a + (c - d) / b. +Proof. rewrite <- Z.add_sub_assoc; apply Z.div_add_l. Qed. + +Lemma Zdiv_add_sub_l' a b c d : b <> 0 -> (b * a + c - d) / b = a + (c - d) / b. +Proof. rewrite <- Z.add_sub_assoc; apply Zdiv_add_l'. Qed. + +Lemma Zdiv_add_sub a b c d : c <> 0 -> (a + b * c - d) / c = (a - d) / c + b. +Proof. rewrite (Z.add_comm _ (_ * _)), (Z.add_comm (_ / _)); apply Zdiv_add_sub_l. Qed. + +Lemma Zdiv_add_sub' a b c d : c <> 0 -> (a + c * b - d) / c = (a - d) / c + b. +Proof. rewrite (Z.add_comm _ (_ * _)), (Z.add_comm (_ / _)); apply Zdiv_add_sub_l'. Qed. + +Hint Rewrite Zdiv_add_sub Zdiv_add_sub' Zdiv_add_sub_l Zdiv_add_sub_l' using lia : zsimplify. + Lemma Zdiv_mul_skip a b k : 0 < b -> 0 < k -> a * b / k / b = a / k. Proof. intros; rewrite Z.div_div, (Z.mul_comm k), <- Z.div_div by lia. -- cgit v1.2.3 From be267954b7267b8564e4125b58349e0860f31967 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 1 Jul 2016 19:24:51 -0700 Subject: Add ZUtil hints --- src/Util/ZUtil.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 21456fea9..fe329d3f9 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -612,6 +612,8 @@ Proof. pose proof (Zdiv_mul_le_le a b c); lia. Qed. +Hint Resolve Zmult_le_compat_r Zmult_le_compat_l Z_div_le Zdiv_mul_le_le_offset Z.add_le_mono Z.sub_le_mono : zarith. + (** * [Zsimplify_fractions_le] *) (** The culmination of this series of tactics, [Zsimplify_fractions_le], will use the fact that [a * (b / c) <= -- cgit v1.2.3 From a825cfbb7b9a96cec2b7b891c1e76195177a7a0c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 1 Jul 2016 19:43:58 -0700 Subject: Fix for 8.4 evars --- src/Util/ZUtil.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index fe329d3f9..a8b18ffef 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -812,7 +812,7 @@ Proof. assert (Hn : -X <= a - b) by lia. assert (Hp : a - b <= X - 1) by lia. split; etransitivity; [ | apply Z_div_le, Hn; lia | apply Z_div_le, Hp; lia | ]; - autorewrite with zsimplify; reflexivity. + instantiate; autorewrite with zsimplify; try reflexivity. Qed. Hint Resolve (fun a b X H0 H1 => proj1 (Zsub_pos_bound_div a b X H0 H1)) -- cgit v1.2.3 From 2939418894d78c095cd9142ce99c615f2d61dda6 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 2 Jul 2016 11:04:46 -0700 Subject: super_nsatz: Handle x^2 = y^2 -> x <> -y -> x = y After | File Name | Before || Change ------------------------------------------------------------------------------------ 2m38.35s | Total | 2m36.78s || +0m01.57s ------------------------------------------------------------------------------------ 0m27.68s | Specific/GF25519 | 0m27.26s || +0m00.41s 0m25.00s | CompleteEdwardsCurve/ExtendedCoordinates | 0m24.87s || +0m00.12s 0m24.96s | ModularArithmetic/ModularBaseSystemProofs | 0m24.84s || +0m00.12s 0m21.55s | Experiments/SpecEd25519 | 0m21.39s || +0m00.16s 0m19.82s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m19.65s || +0m00.17s 0m08.29s | ModularArithmetic/PrimeFieldTheorems | 0m08.30s || -0m00.01s 0m07.13s | Specific/GF1305 | 0m06.69s || +0m00.43s 0m03.75s | ModularArithmetic/Tutorial | 0m03.77s || -0m00.02s 0m03.69s | ModularArithmetic/ModularBaseSystemOpt | 0m03.71s || -0m00.02s 0m03.64s | CompleteEdwardsCurve/Pre | 0m03.67s || -0m00.02s 0m02.11s | Algebra | 0m01.96s || +0m00.14s 0m01.81s | Experiments/DerivationsOptionRectLetInEncoding | 0m01.83s || -0m00.02s 0m01.73s | Experiments/EdDSARefinement | 0m01.71s || +0m00.02s 0m01.67s | ModularArithmetic/ModularArithmeticTheorems | 0m01.65s || +0m00.02s 0m00.91s | ModularArithmetic/ExtendedBaseVector | 0m00.92s || -0m00.01s 0m00.80s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.85s || -0m00.04s 0m00.60s | Encoding/ModularWordEncodingPre | 0m00.59s || +0m00.01s 0m00.59s | Encoding/ModularWordEncodingTheorems | 0m00.61s || -0m00.02s 0m00.58s | ModularArithmetic/ModularBaseSystem | 0m00.52s || +0m00.05s 0m00.57s | Spec/ModularWordEncoding | 0m00.53s || +0m00.03s 0m00.56s | Spec/EdDSA | 0m00.56s || +0m00.00s 0m00.56s | ModularArithmetic/PseudoMersenneBaseRep | 0m00.54s || +0m00.02s 0m00.36s | Spec/CompleteEdwardsCurve | 0m00.36s || +0m00.00s --- src/Algebra.v | 37 +++++++++++++++++++++++++++---------- 1 file changed, 27 insertions(+), 10 deletions(-) diff --git a/src/Algebra.v b/src/Algebra.v index 473571824..62b216b92 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -1038,32 +1038,49 @@ Ltac super_nsatz_post_clean_inequalities := try assumption; prensatz_contradict; nsatz_inequality_to_equality; try nsatz. +Ltac nsatz_equality_to_inequality_by_decide_equality := + lazymatch goal with + | [ H : not (?R _ _) |- ?R _ _ ] => idtac + | [ H : (?R _ _ -> False)%type |- ?R _ _ ] => idtac + | [ |- ?R _ _ ] => fail 0 "No hypothesis exists which negates the relation" R + | [ |- ?G ] => fail 0 "The goal is not a binary relation:" G + end; + lazymatch goal with + | [ |- ?R ?x ?y ] + => destruct (@dec (R x y) _); [ assumption | exfalso ] + end. (** Handles inequalities and fractions *) -Ltac super_nsatz := +Ltac super_nsatz_internal nsatz_alternative := (* [nsatz] gives anomalies on duplicate hypotheses, so we strip them *) clear_algebraic_duplicates; prensatz_contradict; (* Each goal left over by [prensatz_contradict] is separate (and there might not be any), so we handle them all separately *) [ try conservative_common_denominator_equality_inequality_all; - [ try nsatz_inequality_to_equality; try nsatz; - (* [nstaz] might leave over side-conditions; we handle them if they are inequalities *) - try super_nsatz_post_clean_inequalities + [ try nsatz_inequality_to_equality; + try first [ nsatz; + (* [nstaz] might leave over side-conditions; we handle them if they are inequalities *) + try super_nsatz_post_clean_inequalities + | nsatz_alternative ] | super_nsatz_post_clean_inequalities.. ].. ]. +Ltac super_nsatz := + super_nsatz_internal + (* if [nsatz] fails, we try turning the goal equality into an inequality and trying again *) + ltac:(nsatz_equality_to_inequality_by_decide_equality; + super_nsatz_internal idtac). + Section ExtraLemmas. Context {F eq zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div}. Local Infix "+" := add. Local Infix "*" := mul. Local Infix "-" := sub. Local Infix "/" := div. Local Notation "0" := zero. Local Notation "1" := one. Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + Example _only_two_square_roots_test x y : x * x = y * y -> x <> opp y -> x = y. + Proof. intros; super_nsatz. Qed. + Lemma only_two_square_roots' x y : x * x = y * y -> x <> y -> x <> opp y -> False. - Proof. - intros. - canonicalize_field_equalities; canonicalize_field_inequalities. - assert (H' : (x + y) * (x - y) <> 0) by (apply mul_nonzero_nonzero; assumption). - apply H'; nsatz. - Qed. + Proof. intros; super_nsatz. Qed. Lemma only_two_square_roots x y z : x * x = z -> y * y = z -> x <> y -> x <> opp y -> False. Proof. -- cgit v1.2.3 From cd6c4f1297a6604fa4691a5f13808b721194f13b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 2 Jul 2016 12:08:02 -0700 Subject: Make ZUtil more uniform The standard library uses Z.*, and Z* and Z_* are compatibility notations. We follow suit. Also, eliminate a few lemmas that are duplicates of ones in the standard library. --- src/BaseSystem.v | 2 +- src/BaseSystemProofs.v | 2 +- src/Encoding/ModularWordEncodingTheorems.v | 6 +- src/ModularArithmetic/ModularBaseSystemOpt.v | 8 +- src/ModularArithmetic/ModularBaseSystemProofs.v | 28 +- src/ModularArithmetic/PrimeFieldTheorems.v | 4 +- .../PseudoMersenneBaseParamProofs.v | 12 +- src/Testbit.v | 10 +- src/Util/NumTheoryUtil.v | 16 +- src/Util/ZUtil.v | 305 ++++++++++----------- 10 files changed, 190 insertions(+), 203 deletions(-) diff --git a/src/BaseSystem.v b/src/BaseSystem.v index 743cdfde8..c22af95ca 100644 --- a/src/BaseSystem.v +++ b/src/BaseSystem.v @@ -111,7 +111,7 @@ Section PolynomialBaseCoefs. rewrite in_map_iff in *. destruct H; destruct H. subst. - apply pos_pow_nat_pos. + apply Z.pos_pow_nat_pos. Qed. Lemma poly_base_defn : forall i, (i < length poly_base)%nat -> diff --git a/src/BaseSystemProofs.v b/src/BaseSystemProofs.v index 85835aabe..5746cb5f1 100644 --- a/src/BaseSystemProofs.v +++ b/src/BaseSystemProofs.v @@ -177,7 +177,7 @@ Section BaseSystemProofs. Lemma nth_error_base_nonzero : forall n x, nth_error base n = Some x -> x <> 0. Proof. - eauto using (@nth_error_value_In Z), Zgt0_neq0, base_positive. + eauto using (@nth_error_value_In Z), Z.gt0_neq0, base_positive. Qed. Hint Rewrite plus_0_r. diff --git a/src/Encoding/ModularWordEncodingTheorems.v b/src/Encoding/ModularWordEncodingTheorems.v index 41b75e216..033e99665 100644 --- a/src/Encoding/ModularWordEncodingTheorems.v +++ b/src/Encoding/ModularWordEncodingTheorems.v @@ -43,12 +43,12 @@ Section SignBit. pose proof (F_opp_spec x) as opp_spec_x. apply F_eq in opp_spec_x. rewrite FieldToZ_add in opp_spec_x. - rewrite <-opp_spec_x, Z_odd_mod in sign_zero by (pose proof prime_ge_2 m prime_m; omega). - replace (Z.odd m) with true in sign_zero by (destruct (ZUtil.prime_odd_or_2 m prime_m); auto || omega). + rewrite <-opp_spec_x, Z.odd_mod in sign_zero by (pose proof prime_ge_2 m prime_m; omega). + replace (Z.odd m) with true in sign_zero by (destruct (Z.prime_odd_or_2 m prime_m); auto || omega). rewrite Z.odd_add, F_FieldToZ_add_opp, Z.div_same, Bool.xorb_true_r in sign_zero by assumption || omega. apply Bool.xorb_eq. rewrite <-Bool.negb_xorb_l. assumption. Qed. -End SignBit. \ No newline at end of file +End SignBit. diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index 116fe10e5..9bb3128ad 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -22,7 +22,7 @@ Definition Z_div_opt := Eval compute in Z.div. Definition Z_pow_opt := Eval compute in Z.pow. Definition Z_opp_opt := Eval compute in Z.opp. Definition Z_shiftl_opt := Eval compute in Z.shiftl. -Definition Z_shiftl_by_opt := Eval compute in Z_shiftl_by. +Definition Z_shiftl_by_opt := Eval compute in Z.shiftl_by. Definition nth_default_opt {A} := Eval compute in @nth_default A. Definition set_nth_opt {A} := Eval compute in @set_nth A. @@ -499,11 +499,11 @@ Section Multiplication. cbv [BaseSystem.mul mul mul_each mul_bi mul_bi' zeros ext_base reduce]. rewrite <- mul'_opt_correct. change @base with base_opt. - rewrite map_shiftl by apply k_nonneg. + rewrite Z.map_shiftl by apply k_nonneg. rewrite c_subst. rewrite k_subst. change @map with @map_opt. - change @Z_shiftl_by with @Z_shiftl_by_opt. + change @Z.shiftl_by with @Z_shiftl_by_opt. reflexivity. Defined. @@ -668,4 +668,4 @@ Section Canonicalization. auto using freeze_opt_preserves_rep. Qed. -End Canonicalization. \ No newline at end of file +End Canonicalization. diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 6f82a8950..a8bd93097 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -110,7 +110,7 @@ Section PseudoMersenneProofs. rewrite Z.sub_sub_distr, Z.sub_diag. simpl. rewrite Z.mul_comm. - rewrite mod_mult_plus; auto using modulus_nonzero. + rewrite Z.mod_add_l; auto using modulus_nonzero. rewrite <- Zplus_mod; auto. Qed. @@ -304,8 +304,8 @@ Section CarryProofs. rewrite nth_default_base_succ by omega. rewrite Z.mul_assoc. rewrite (Z.mul_comm _ (2 ^ log_cap i)). - rewrite mul_div_eq; try ring. - apply gt_lt_symmetry. + rewrite Z.mul_div_eq; try ring. + apply Z.gt_lt_iff. apply Z.pow_pos_nonneg; omega || apply log_cap_nonneg. Qed. @@ -337,7 +337,7 @@ Section CarryProofs. rewrite <- Z.add_opp_l, <- Z.opp_sub_distr. unfold pow2_mod. rewrite Z.land_ones by apply log_cap_nonneg. - rewrite <- mul_div_eq by (apply gt_lt_symmetry; apply Z.pow_pos_nonneg; omega || apply log_cap_nonneg). + rewrite <- Z.mul_div_eq by (apply Z.gt_lt_iff; apply Z.pow_pos_nonneg; omega || apply log_cap_nonneg). rewrite Z.shiftr_div_pow2 by apply log_cap_nonneg. rewrite Zopp_mult_distr_r. rewrite Z.mul_comm. @@ -485,7 +485,7 @@ Section CanonicalizationProofs. Lemma max_bound_pos : forall i, (i < length base)%nat -> 0 < max_bound i. Proof. - unfold max_bound, log_cap; intros; apply Z_ones_pos_pos. + unfold max_bound, log_cap; intros; apply Z.ones_pos_pos. apply limb_widths_pos. rewrite nth_default_eq. apply nth_In. @@ -495,7 +495,7 @@ Section CanonicalizationProofs. Lemma max_bound_nonneg : forall i, 0 <= max_bound i. Proof. - unfold max_bound; intros; auto using Z_ones_nonneg. + unfold max_bound; intros; auto using Z.ones_nonneg. Qed. Local Hint Resolve max_bound_nonneg. @@ -874,7 +874,7 @@ Section CanonicalizationProofs. apply Z.add_le_mono. + apply carry_bounds_0_upper; auto; omega. + apply Z.mul_le_mono_pos_l; auto. - apply Z_shiftr_ones; auto; + apply Z.shiftr_ones; auto; [ | pose proof (B_compat_log_cap (pred (length base))); omega ]. split. - apply carry_bounds_lower; auto; omega. @@ -913,7 +913,7 @@ Section CanonicalizationProofs. + rewrite <-max_bound_log_cap, <-Z.add_1_l. apply Z.add_le_mono. - rewrite Z.shiftr_div_pow2 by apply log_cap_nonneg. - apply Z_div_floor; auto. + apply Z.div_floor; auto. destruct i. * simpl. eapply Z.le_lt_trans; [ apply carry_full_bounds_0; auto | ]. @@ -996,7 +996,7 @@ Section CanonicalizationProofs. + rewrite <-max_bound_log_cap, <-Z.add_1_l. rewrite Z.shiftr_div_pow2 by apply log_cap_nonneg. apply Z.add_le_mono. - - apply Z_div_floor; auto. + - apply Z.div_floor; auto. eapply Z.le_lt_trans; [ eapply carry_full_2_bounds_0; eauto | ]. replace (Z.succ 1) with (2 ^ 1) by ring. rewrite <-max_bound_log_cap. @@ -1202,7 +1202,7 @@ Section CanonicalizationProofs. Lemma max_ones_nonneg : 0 <= max_ones. Proof. unfold max_ones. - apply Z_ones_nonneg. + apply Z.ones_nonneg. pose proof limb_widths_nonneg. induction limb_widths. cbv; congruence. @@ -1217,19 +1217,19 @@ Section CanonicalizationProofs. unfold max_ones. intros ? ? x_range. rewrite Z.land_comm. - rewrite Z.land_ones by apply Z_le_fold_right_max_initial. + rewrite Z.land_ones by apply Z.le_fold_right_max_initial. apply Z.mod_small. split; try omega. eapply Z.lt_le_trans; try eapply x_range. apply Z.pow_le_mono_r; try omega. rewrite log_cap_eq. destruct (lt_dec i (length limb_widths)). - + apply Z_le_fold_right_max. + + apply Z.le_fold_right_max. - apply limb_widths_nonneg. - rewrite nth_default_eq. auto using nth_In. + rewrite nth_default_out_of_bounds by omega. - apply Z_le_fold_right_max_initial. + apply Z.le_fold_right_max_initial. Qed. Lemma full_isFull'_true : forall j us, (length us = length base) -> @@ -1817,7 +1817,7 @@ Section CanonicalizationProofs. + match goal with |- (?a ?= ?b) = (?c ?= ?d) => rewrite (Z.compare_antisym b a); rewrite (Z.compare_antisym d c) end. apply CompOpp_inj; rewrite !CompOpp_involutive. - apply gt_lt_symmetry in Hgt. + apply Z.gt_lt_iff in Hgt. etransitivity; try apply Z_compare_decode_step_lt; auto; omega. Qed. diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index 2021e8514..a2f606f30 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -460,8 +460,8 @@ Section SquareRootsPrime5Mod8. apply Z2N.inj_iff; try zero_bounds. rewrite <- Z.mul_cancel_l with (p := 2) by omega. ring_simplify. - rewrite mul_div_eq by omega. - rewrite mul_div_eq by omega. + rewrite Z.mul_div_eq by omega. + rewrite Z.mul_div_eq by omega. rewrite (Zmod_div_mod 2 8 q) by (try omega; apply Zmod_divide; omega || auto). rewrite q_5mod8. diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v index 49b1875ce..9e4e4b3ba 100644 --- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v +++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v @@ -163,7 +163,7 @@ Section PseudoMersenneBaseParamProofs. rewrite (Z.mul_comm r). subst r. assert (i + j - length base < length base)%nat by omega. - rewrite mul_div_eq by (apply gt_lt_symmetry; apply Z.mul_pos_pos; + rewrite Z.mul_div_eq by (apply Z.gt_lt_iff; apply Z.mul_pos_pos; [ | subst b; rewrite nth_default_base; try assumption ]; apply Z.pow_pos_nonneg; omega || apply k_nonneg || apply sum_firstn_limb_widths_nonneg). rewrite (Zminus_0_l_reverse (b i * b j)) at 1. @@ -172,7 +172,7 @@ Section PseudoMersenneBaseParamProofs. repeat rewrite nth_default_base by assumption. do 2 rewrite <- Z.pow_add_r by (apply sum_firstn_limb_widths_nonneg || apply k_nonneg). symmetry. - apply mod_same_pow. + apply Z.mod_same_pow. split. + apply Z.add_nonneg_nonneg; apply sum_firstn_limb_widths_nonneg || apply k_nonneg. + rewrite base_length in *; apply limb_widths_match_modulus; assumption. @@ -183,7 +183,7 @@ Section PseudoMersenneBaseParamProofs. Proof. intros. repeat rewrite nth_default_base by omega. - apply mod_same_pow. + apply Z.mod_same_pow. split; [apply sum_firstn_limb_widths_nonneg | ]. destruct (NPeano.Nat.eq_dec i 0); subst. + case_eq limb_widths; intro; unfold sum_firstn; simpl; try omega; intros l' lw_eq. @@ -218,7 +218,7 @@ Section PseudoMersenneBaseParamProofs. destruct In_b_base as [i nth_err_b]. apply nth_error_subst in nth_err_b. rewrite nth_err_b. - apply gt_lt_symmetry. + apply Z.gt_lt_iff. apply Z.pow_pos_nonneg; omega || apply sum_firstn_limb_widths_nonneg. Qed. @@ -236,9 +236,9 @@ Section PseudoMersenneBaseParamProofs. intros; subst b r. repeat rewrite nth_default_base by omega. rewrite (Z.mul_comm _ (2 ^ (sum_firstn limb_widths (i+j)))). - rewrite mul_div_eq by (apply gt_lt_symmetry; apply Z.pow_pos_nonneg; omega || apply sum_firstn_limb_widths_nonneg). + rewrite Z.mul_div_eq by (apply Z.gt_lt_iff; apply Z.pow_pos_nonneg; omega || apply sum_firstn_limb_widths_nonneg). rewrite <- Z.pow_add_r by apply sum_firstn_limb_widths_nonneg. - rewrite mod_same_pow; try ring. + rewrite Z.mod_same_pow; try ring. split; [ apply sum_firstn_limb_widths_nonneg | ]. apply limb_widths_good. rewrite <- base_length; assumption. diff --git a/src/Testbit.v b/src/Testbit.v index 2bfcc3df6..d735bbe21 100644 --- a/src/Testbit.v +++ b/src/Testbit.v @@ -107,7 +107,7 @@ Proof. rewrite <- nth_default_eq in uniform. erewrite nth_error_value_eq_nth_default in uniform; eauto. subst. - destruct r; [ | apply pos_pow_nat_pos | pose proof (Zlt_neg_0 p) ] ; omega. + destruct r; [ | apply Z.pos_pow_nat_pos | pose proof (Zlt_neg_0 p) ] ; omega. + intros. rewrite nth_default_eq. rewrite uniform; auto. @@ -151,7 +151,7 @@ Proof. induction us; boring. rewrite <- (IHus base) by (omega || eauto using no_overflow_tail). rewrite decode_cons by (eapply uniform_base_BaseVector; eauto; - rewrite gt_lt_symmetry; apply Z_pow_gt0; omega). + rewrite Z.gt_lt_iff; apply Z.pow_pos_nonneg; omega). simpl. f_equal. + symmetry. eapply no_overflow_cons; eauto. @@ -174,12 +174,12 @@ Proof. auto using Z.land_0_l. + destruct i; simpl. - rewrite nth_default_cons. - rewrite Z.shiftr_0_r, Z_land_add_land by omega. + rewrite Z.shiftr_0_r, Z.land_add_land by omega. symmetry; eapply no_overflow_cons; eauto. - rewrite nth_default_cons_S. erewrite IHus; eauto using no_overflow_tail. remember (i * limb_width)%nat as k. - rewrite Z_shiftr_add_land by omega. + rewrite Z.shiftr_add_land by omega. replace (limb_width + k - limb_width)%nat with k by omega. reflexivity. Qed. @@ -190,7 +190,7 @@ Lemma unfold_bits_testbit : forall limb_width us n, (0 < limb_width)%nat -> Proof. unfold testbit; intros. erewrite unfold_bits_indexing; eauto. - rewrite <- Z_testbit_low by + rewrite <- Z.testbit_low by (split; try apply Nat2Z.inj_lt; pose proof (mod_bound_pos n limb_width); omega). rewrite Z.shiftr_spec by apply Nat2Z.is_nonneg. f_equal. diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v index 10ce148b0..c16b87639 100644 --- a/src/Util/NumTheoryUtil.v +++ b/src/Util/NumTheoryUtil.v @@ -66,7 +66,7 @@ Qed. Lemma p_odd : Z.odd p = true. Proof. - pose proof (prime_odd_or_2 p prime_p). + pose proof (Z.prime_odd_or_2 p prime_p). destruct H; auto. Qed. @@ -124,12 +124,12 @@ Proof. assert (b mod p <> 0) as b_nonzero. { intuition. rewrite <- Z.pow_2_r in a_square. - rewrite mod_exp_0 in a_square by prime_bound. + rewrite Z.mod_exp_0 in a_square by prime_bound. rewrite <- a_square in a_nonzero. auto. } pose proof (squared_fermat_little b b_nonzero). - rewrite mod_pow in * by prime_bound. + rewrite Z.mod_pow in * by prime_bound. rewrite <- a_square. rewrite Z.mod_mod; prime_bound. Qed. @@ -172,10 +172,10 @@ Proof. intros. destruct (exists_primitive_root_power) as [y [in_ZPGroup_y [y_order gpow_y]]]; auto. destruct (gpow_y a a_range) as [j [j_range pow_y_j]]; clear gpow_y. - rewrite mod_pow in pow_a_x by prime_bound. + rewrite Z.mod_pow in pow_a_x by prime_bound. replace a with (a mod p) in pow_y_j by (apply Z.mod_small; omega). rewrite <- pow_y_j in pow_a_x. - rewrite <- mod_pow in pow_a_x by prime_bound. + rewrite <- Z.mod_pow in pow_a_x by prime_bound. rewrite <- Z.pow_mul_r in pow_a_x by omega. assert (p - 1 | j * x) as divide_mul_j_x. { rewrite <- phi_is_order in y_order. @@ -193,13 +193,13 @@ Proof. rewrite <- Z_div_plus by omega. rewrite Z.mul_comm. rewrite x_id_inv in divide_mul_j_x; auto. - apply (divide_mul_div _ j 2) in divide_mul_j_x; + apply (Z.divide_mul_div _ j 2) in divide_mul_j_x; try (apply prime_pred_divide2 || prime_bound); auto. rewrite <- Zdivide_Zdiv_eq by (auto || omega). rewrite Zplus_diag_eq_mult_2. replace (a mod p) with a in pow_y_j by (symmetry; apply Z.mod_small; omega). rewrite Z_div_mult by omega; auto. - apply divide2_even_iff. + apply Z.divide2_even_iff. apply prime_pred_even. Qed. @@ -281,7 +281,7 @@ Lemma div2_p_1mod4 : forall (p : Z) (prime_p : prime p) (neq_p_2: p <> 2), (p / 2) * 2 + 1 = p. Proof. intros. - destruct (prime_odd_or_2 p prime_p); intuition. + destruct (Z.prime_odd_or_2 p prime_p); intuition. rewrite <- Zdiv2_div. pose proof (Zdiv2_odd_eqn p); break_if; congruence || omega. Qed. diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index a8b18ffef..b3b11fc0c 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -17,7 +17,7 @@ Hint Resolve (fun a b H => proj1 (Z.mod_pos_bound a b H)) (fun a b H => proj2 (Z this database. *) Create HintDb zsimplify discriminated. Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r : zsimplify. -Hint Rewrite Z.div_mul Z.div_1_l Z.div_same Z.mod_same Z.div_small Z.mod_small Z.div_add Z.div_add_l using lia : zsimplify. +Hint Rewrite Z.div_mul Z.div_1_l Z.div_same Z.mod_same Z.div_small Z.mod_small Z.div_add Z.div_add_l Z.mod_add using lia : zsimplify. (** "push" means transform [-f x] to [f (-x)]; "pull" means go the other way *) Create HintDb push_Zopp discriminated. @@ -43,56 +43,50 @@ Hint Rewrite Z.div_small_iff using lia : zstrip_div. We'll put, e.g., [mul_div_eq] into it below. *) Create HintDb zstrip_div. -Lemma gt_lt_symmetry: forall n m, n > m <-> m < n. -Proof. - intros; split; omega. -Qed. - +Module Z. Lemma positive_is_nonzero : forall x, x > 0 -> x <> 0. -Proof. - intros; omega. -Qed. -Hint Resolve positive_is_nonzero. +Proof. intros; omega. Qed. + +Hint Resolve positive_is_nonzero : zarith. Lemma div_positive_gt_0 : forall a b, a > 0 -> b > 0 -> a mod b = 0 -> a / b > 0. Proof. - intros; rewrite gt_lt_symmetry. + intros; rewrite Z.gt_lt_iff. apply Z.div_str_pos. split; intuition. apply Z.divide_pos_le; try (apply Zmod_divide); omega. Qed. Lemma elim_mod : forall a b m, a = b -> a mod m = b mod m. -Proof. - intros; subst; auto. -Qed. -Hint Resolve elim_mod. +Proof. intros; subst; auto. Qed. -Lemma mod_mult_plus: forall a b c, (b <> 0) -> (a * b + c) mod b = c mod b. -Proof. - intros. - rewrite Zplus_mod. - rewrite Z.mod_mul; auto; simpl. - rewrite Zmod_mod; auto. -Qed. +Hint Resolve elim_mod : zarith. + +Lemma mod_add_l : forall a b c, b <> 0 -> (a * b + c) mod b = c mod b. +Proof. intros; rewrite (Z.add_comm _ c); autorewrite with zsimplify; reflexivity. Qed. +Hint Rewrite mod_add_l using lia : zsimplify. + +Lemma mod_add' : forall a b c, b <> 0 -> (a + b * c) mod b = a mod b. +Proof. intros; rewrite (Z.mul_comm _ c); autorewrite with zsimplify; reflexivity. Qed. +Lemma mod_add_l' : forall a b c, a <> 0 -> (a * b + c) mod a = c mod a. +Proof. intros; rewrite (Z.mul_comm _ b); autorewrite with zsimplify; reflexivity. Qed. +Hint Rewrite mod_add' mod_add_l' using lia : zsimplify. Lemma pos_pow_nat_pos : forall x n, Z.pos x ^ Z.of_nat n > 0. +Proof. do 2 (intros; induction n; subst; simpl in *; auto with zarith). rewrite <- Pos.add_1_r, Zpower_pos_is_exp. apply Zmult_gt_0_compat; auto; reflexivity. Qed. -Lemma Z_div_mul' : forall a b : Z, b <> 0 -> (b * a) / b = a. - intros. rewrite Z.mul_comm. apply Z.div_mul; auto. -Qed. - -Hint Rewrite Z_div_mul' using lia : zsimplify. +Lemma div_mul' : forall a b : Z, b <> 0 -> (b * a) / b = a. +Proof. intros. rewrite Z.mul_comm. apply Z.div_mul; auto. Qed. +Hint Rewrite div_mul' using lia : zsimplify. -Lemma Zgt0_neq0 : forall x, x > 0 -> x <> 0. - intuition. -Qed. +(** TODO: Should we get rid of this duplicate? *) +Notation gt0_neq0 := positive_is_nonzero (only parsing). Lemma pow_Z2N_Zpow : forall a n, 0 <= a -> ((Z.to_nat a) ^ n = Z.to_nat (a ^ Z.of_nat n)%Z)%nat. @@ -150,7 +144,7 @@ Proof. reflexivity. Qed. -Ltac Zdivide_exists_mul := let k := fresh "k" in +Ltac divide_exists_mul := let k := fresh "k" in match goal with | [ H : (?a | ?b) |- _ ] => apply Z.mod_divide in H; try apply Zmod_divides in H; destruct H as [k H] | [ |- (?a | ?b) ] => apply Z.mod_divide; try apply Zmod_divides @@ -159,9 +153,9 @@ end; (omega || auto). Lemma divide_mul_div: forall a b c (a_nonzero : a <> 0) (c_nonzero : c <> 0), (a | b * (a / c)) -> (c | a) -> (c | b). Proof. - intros ? ? ? ? ? divide_a divide_c_a; do 2 Zdivide_exists_mul. + intros ? ? ? ? ? divide_a divide_c_a; do 2 divide_exists_mul. rewrite divide_c_a in divide_a. - rewrite Z_div_mul' in divide_a by auto. + rewrite div_mul' in divide_a by auto. replace (b * k) with (k * b) in divide_a by ring. replace (c * k * k0) with (k * (k0 * c)) in divide_a by ring. rewrite Z.mul_cancel_l in divide_a by (intuition; rewrite H in divide_c_a; ring_simplify in divide_a; intuition). @@ -172,7 +166,7 @@ Lemma divide2_even_iff : forall n, (2 | n) <-> Z.even n = true. Proof. intro; split. { intro divide2_n. - Zdivide_exists_mul; [ | pose proof (Z.mod_pos_bound n 2); omega]. + divide_exists_mul; [ | pose proof (Z.mod_pos_bound n 2); omega]. rewrite divide2_n. apply Z.even_mul. } { @@ -200,7 +194,7 @@ Proof. pose proof (prime_ge_2 p prime_p); omega. Qed. -Lemma mul_div_eq : (forall a m, m > 0 -> m * (a / m) = (a - a mod m))%Z. +Lemma mul_div_eq : forall a m, m > 0 -> m * (a / m) = (a - a mod m). Proof. intros. rewrite (Z_div_mod_eq a m) at 2 by auto. @@ -221,13 +215,7 @@ Ltac prime_bound := match goal with | [ H : prime ?p |- _ ] => pose proof (prime_ge_2 p H); try omega end. -Lemma Zlt_minus_lt_0 : forall n m, m < n -> 0 < n - m. -Proof. - intros; omega. -Qed. - - -Lemma Z_testbit_low : forall n x i, (0 <= i < n) -> +Lemma testbit_low : forall n x i, (0 <= i < n) -> Z.testbit x i = Z.testbit (Z.land x (Z.ones n)) i. Proof. intros. @@ -238,24 +226,25 @@ Proof. Qed. -Lemma Z_testbit_shiftl : forall i, (0 <= i) -> forall a b n, (i < n) -> +Lemma testbit_shiftl : forall i, (0 <= i) -> forall a b n, (i < n) -> Z.testbit (a + Z.shiftl b n) i = Z.testbit a i. Proof. intros. - erewrite Z_testbit_low; eauto. + erewrite Z.testbit_low; eauto. rewrite Z.land_ones, Z.shiftl_mul_pow2 by omega. rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 n); omega). auto using Z.mod_pow2_bits_low. Qed. -Lemma Z_mod_div_eq0 : forall a b, 0 < b -> (a mod b) / b = 0. +Lemma mod_div_eq0 : forall a b, 0 < b -> (a mod b) / b = 0. Proof. intros. apply Z.div_small. auto using Z.mod_pos_bound. Qed. +Hint Rewrite mod_div_eq0 using lia : zsimplify. -Lemma Z_shiftr_add_land : forall n m a b, (n <= m)%nat -> +Lemma shiftr_add_land : forall n m a b, (n <= m)%nat -> Z.shiftr ((Z.land a (Z.ones (Z.of_nat n))) + (Z.shiftl b (Z.of_nat n))) (Z.of_nat m) = Z.shiftr b (Z.of_nat (m - n)). Proof. intros. @@ -269,10 +258,10 @@ Proof. [ pose proof (Z.pow_pos_nonneg 2 (Z.of_nat n)); omega | apply Z.pow_pos_nonneg; omega ]. rewrite Z.div_add by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat n)); omega). - rewrite Z_mod_div_eq0 by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat n)); omega); auto. + rewrite mod_div_eq0 by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat n)); omega); auto. Qed. -Lemma Z_land_add_land : forall n m a b, (m <= n)%nat -> +Lemma land_add_land : forall n m a b, (m <= n)%nat -> Z.land ((Z.land a (Z.ones (Z.of_nat n))) + (Z.shiftl b (Z.of_nat n))) (Z.ones (Z.of_nat m)) = Z.land a (Z.ones (Z.of_nat m)). Proof. intros. @@ -289,15 +278,6 @@ Proof. apply Z.divide_factor_l. Qed. -Lemma Z_pow_gt0 : forall a, 0 < a -> forall b, 0 <= b -> 0 < a ^ b. -Proof. - intros until 1. - apply natlike_ind; try (simpl; omega). - intros. - rewrite Z.pow_succ_r by assumption. - apply Z.mul_pos_pos; assumption. -Qed. - Lemma div_pow2succ : forall n x, (0 <= x) -> n / 2 ^ Z.succ x = Z.div2 (n / 2 ^ x). Proof. @@ -317,27 +297,27 @@ Proof. Qed. -Definition Z_shiftl_by n a := Z.shiftl a n. +Definition shiftl_by n a := Z.shiftl a n. -Lemma Z_shiftl_by_mul_pow2 : forall n a, 0 <= n -> Z.mul (2 ^ n) a = Z_shiftl_by n a. +Lemma shiftl_by_mul_pow2 : forall n a, 0 <= n -> Z.mul (2 ^ n) a = Z.shiftl_by n a. Proof. intros. - unfold Z_shiftl_by. + unfold Z.shiftl_by. rewrite Z.shiftl_mul_pow2 by assumption. apply Z.mul_comm. Qed. -Lemma map_shiftl : forall n l, 0 <= n -> map (Z.mul (2 ^ n)) l = map (Z_shiftl_by n) l. +Lemma map_shiftl : forall n l, 0 <= n -> map (Z.mul (2 ^ n)) l = map (Z.shiftl_by n) l. Proof. - intros; induction l; auto using Z_shiftl_by_mul_pow2. + intros; induction l; auto using Z.shiftl_by_mul_pow2. simpl. rewrite IHl. f_equal. - apply Z_shiftl_by_mul_pow2. + apply Z.shiftl_by_mul_pow2. assumption. Qed. -Lemma Z_odd_mod : forall a b, (b <> 0)%Z -> +Lemma odd_mod : forall a b, (b <> 0)%Z -> Z.odd (a mod b) = if Z.odd b then xorb (Z.odd a) (Z.odd (a / b)) else Z.odd a. Proof. intros. @@ -353,8 +333,9 @@ Proof. rewrite Z.pow_add_r by omega. apply Z_mod_mult. Qed. +Hint Rewrite mod_same_pow using lia : zsimplify. - Lemma Z_ones_succ : forall x, (0 <= x) -> + Lemma ones_succ : forall x, (0 <= x) -> Z.ones (Z.succ x) = 2 ^ x + Z.ones x. Proof. unfold Z.ones; intros. @@ -365,14 +346,14 @@ Qed. rewrite Z.pow_succ_r; omega. Qed. - Lemma Z_div_floor : forall a b c, 0 < b -> a < b * (Z.succ c) -> a / b <= c. + Lemma div_floor : forall a b c, 0 < b -> a < b * (Z.succ c) -> a / b <= c. Proof. intros. apply Z.lt_succ_r. apply Z.div_lt_upper_bound; try omega. Qed. - Lemma Z_shiftr_1_r_le : forall a b, a <= b -> + Lemma shiftr_1_r_le : forall a b, a <= b -> Z.shiftr a 1 <= Z.shiftr b 1. Proof. intros. @@ -380,7 +361,7 @@ Qed. apply Z.div_le_mono; omega. Qed. - Lemma Z_ones_pred : forall i, 0 < i -> Z.ones (Z.pred i) = Z.shiftr (Z.ones i) 1. + Lemma ones_pred : forall i, 0 < i -> Z.ones (Z.pred i) = Z.shiftr (Z.ones i) 1. Proof. induction i; [ | | pose proof (Pos2Z.neg_is_neg p) ]; try omega. intros. @@ -394,7 +375,7 @@ Qed. f_equal. omega. Qed. - Lemma Z_shiftr_ones' : forall a n, 0 <= a < 2 ^ n -> forall i, (0 <= i) -> + Lemma shiftr_ones' : forall a n, 0 <= a < 2 ^ n -> forall i, (0 <= i) -> Z.shiftr a i <= Z.ones (n - i) \/ n <= i. Proof. intros until 1. @@ -408,17 +389,17 @@ Qed. left. rewrite shiftr_succ. replace (n - Z.succ x) with (Z.pred (n - x)) by omega. - rewrite Z_ones_pred by omega. - apply Z_shiftr_1_r_le. + rewrite Z.ones_pred by omega. + apply Z.shiftr_1_r_le. assumption. Qed. - Lemma Z_shiftr_ones : forall a n i, 0 <= a < 2 ^ n -> (0 <= i) -> (i <= n) -> + Lemma shiftr_ones : forall a n i, 0 <= a < 2 ^ n -> (0 <= i) -> (i <= n) -> Z.shiftr a i <= Z.ones (n - i) . Proof. intros a n i G G0 G1. destruct (Z_le_lt_eq_dec i n G1). - + destruct (Z_shiftr_ones' a n G i G0); omega. + + destruct (Z.shiftr_ones' a n G i G0); omega. + subst; rewrite Z.sub_diag. destruct (Z_eq_dec a 0). - subst; rewrite Z.shiftr_0_l; reflexivity. @@ -426,7 +407,7 @@ Qed. apply Z.log2_lt_pow2; omega. Qed. - Lemma Z_shiftr_upper_bound : forall a n, 0 <= n -> 0 <= a <= 2 ^ n -> Z.shiftr a n <= 1. + Lemma shiftr_upper_bound : forall a n, 0 <= n -> 0 <= a <= 2 ^ n -> Z.shiftr a n <= 1. Proof. intros a ? ? [a_nonneg a_upper_bound]. apply Z_le_lt_eq_dec in a_upper_bound. @@ -463,16 +444,16 @@ Ltac zero_bounds := try omega; try prime_bound; zero_bounds'. Hint Extern 1 => progress zero_bounds : zero_bounds. -Lemma Z_ones_nonneg : forall i, (0 <= i) -> 0 <= Z.ones i. +Lemma ones_nonneg : forall i, (0 <= i) -> 0 <= Z.ones i. Proof. apply natlike_ind. + unfold Z.ones. simpl; omega. + intros. - rewrite Z_ones_succ by assumption. + rewrite Z.ones_succ by assumption. zero_bounds. Qed. -Lemma Z_ones_pos_pos : forall i, (0 < i) -> 0 < Z.ones i. +Lemma ones_pos_pos : forall i, (0 < i) -> 0 < Z.ones i. Proof. intros. unfold Z.ones. @@ -497,7 +478,7 @@ Proof. destruct (p ?=a)%positive; cbv; congruence. Qed. -Lemma Z_land_upper_bound_l : forall a b, (0 <= a) -> (0 <= b) -> +Lemma land_upper_bound_l : forall a b, (0 <= a) -> (0 <= b) -> Z.land a b <= a. Proof. intros. @@ -507,15 +488,15 @@ Proof. auto using Pos_land_upper_bound_l. Qed. -Lemma Z_land_upper_bound_r : forall a b, (0 <= a) -> (0 <= b) -> +Lemma land_upper_bound_r : forall a b, (0 <= a) -> (0 <= b) -> Z.land a b <= b. Proof. intros. rewrite Z.land_comm. - auto using Z_land_upper_bound_l. + auto using Z.land_upper_bound_l. Qed. -Lemma Z_le_fold_right_max : forall low l x, (forall y, In y l -> low <= y) -> +Lemma le_fold_right_max : forall low l x, (forall y, In y l -> low <= y) -> In x l -> x <= fold_right Z.max low l. Proof. induction l; intros ? lower_bound In_list; [cbv [In] in *; intuition | ]. @@ -527,13 +508,13 @@ Proof. - apply Z.le_max_r. Qed. -Lemma Z_le_fold_right_max_initial : forall low l, low <= fold_right Z.max low l. +Lemma le_fold_right_max_initial : forall low l, low <= fold_right Z.max low l. Proof. induction l; intros; try reflexivity. etransitivity; [ apply IHl | apply Z.le_max_r ]. Qed. -Ltac Zltb_to_Zlt := +Ltac ltb_to_lt := repeat match goal with | [ H : (?x let H' := fresh in @@ -543,7 +524,7 @@ Ltac Zltb_to_Zlt := clear H' end. -Ltac Zcompare_to_sgn := +Ltac compare_to_sgn := repeat match goal with | [ H : _ |- _ ] => progress rewrite <- ?Z.sgn_neg_iff, <- ?Z.sgn_pos_iff, <- ?Z.sgn_null_iff in H | _ => progress rewrite <- ?Z.sgn_neg_iff, <- ?Z.sgn_pos_iff, <- ?Z.sgn_null_iff @@ -558,9 +539,9 @@ Local Ltac replace_to_const c := | [ H : c = ?x |- context[?x] ] => rewrite <- H end. -Lemma Zlt_div_0 n m : n / m < 0 <-> ((n < 0 < m \/ m < 0 < n) /\ 0 < -(n / m)). +Lemma lt_div_0 n m : n / m < 0 <-> ((n < 0 < m \/ m < 0 < n) /\ 0 < -(n / m)). Proof. - Zcompare_to_sgn; rewrite Z.sgn_opp; simpl. + Z.compare_to_sgn; rewrite Z.sgn_opp; simpl. pose proof (Zdiv_sgn n m) as H. pose proof (Z.sgn_spec (n / m)) as H'. repeat first [ progress intuition @@ -578,7 +559,7 @@ Qed. Lemma two_times_x_minus_x x : 2 * x - x = x. Proof. lia. Qed. -Lemma Zmul_div_le x y z +Lemma mul_div_le x y z (Hx : 0 <= x) (Hy : 0 <= y) (Hz : 0 < z) (Hyz : y <= z) : x * y / z <= x. @@ -587,12 +568,12 @@ Proof. apply Z_div_le; nia. Qed. -Lemma Zdiv_mul_diff a b c +Lemma div_mul_diff a b c (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c) : c * a / b - c * (a / b) <= c. Proof. pose proof (Z.mod_pos_bound a b). - etransitivity; [ | apply (Zmul_div_le c (a mod b) b); lia ]. + etransitivity; [ | apply (mul_div_le c (a mod b) b); lia ]. rewrite (Z_div_mod_eq a b) at 1 by lia. rewrite Z.mul_add_distr_l. replace (c * (b * (a / b))) with ((c * (a / b)) * b) by lia. @@ -600,23 +581,23 @@ Proof. lia. Qed. -Lemma Zdiv_mul_le_le a b c +Lemma div_mul_le_le a b c : 0 <= a -> 0 < b -> 0 <= c -> c * (a / b) <= c * a / b <= c * (a / b) + c. Proof. - pose proof (Zdiv_mul_diff a b c); split; try apply Z.div_mul_le; lia. + pose proof (Z.div_mul_diff a b c); split; try apply Z.div_mul_le; lia. Qed. -Lemma Zdiv_mul_le_le_offset a b c +Lemma div_mul_le_le_offset a b c : 0 <= a -> 0 < b -> 0 <= c -> c * a / b - c <= c * (a / b). Proof. - pose proof (Zdiv_mul_le_le a b c); lia. + pose proof (Z.div_mul_le_le a b c); lia. Qed. -Hint Resolve Zmult_le_compat_r Zmult_le_compat_l Z_div_le Zdiv_mul_le_le_offset Z.add_le_mono Z.sub_le_mono : zarith. +Hint Resolve Zmult_le_compat_r Zmult_le_compat_l Z_div_le Z.div_mul_le_le_offset Z.add_le_mono Z.sub_le_mono : zarith. -(** * [Zsimplify_fractions_le] *) +(** * [Z.simplify_fractions_le] *) (** The culmination of this series of tactics, - [Zsimplify_fractions_le], will use the fact that [a * (b / c) <= + [Z.simplify_fractions_le], will use the fact that [a * (b / c) <= (a * b) / c], and do some reasoning modulo associativity and commutativity in [Z] to perform such a reduction. It may leave over goals if it cannot prove that some denominators are non-zero. @@ -626,16 +607,16 @@ Hint Resolve Zmult_le_compat_r Zmult_le_compat_l Z_div_le Zdiv_mul_le_le_offset After running, the tactic does some basic rewriting to simplify fractions, e.g., that [a * b / b = a]. *) -Ltac Zsplit_sums_step := +Ltac split_sums_step := match goal with | [ |- _ + _ <= _ ] => etransitivity; [ eapply Z.add_le_mono | ] | [ |- _ - _ <= _ ] => etransitivity; [ eapply Z.sub_le_mono | ] end. -Ltac Zsplit_sums := - try (Zsplit_sums_step; [ Zsplit_sums.. | ]). -Ltac Zpre_reorder_fractions_step := +Ltac split_sums := + try (split_sums_step; [ split_sums.. | ]). +Ltac pre_reorder_fractions_step := match goal with | [ |- context[?x / ?y * ?z] ] => rewrite (Z.mul_comm (x / y) z) @@ -646,10 +627,10 @@ Ltac Zpre_reorder_fractions_step := transitivity G' end end. -Ltac Zpre_reorder_fractions := - try first [ Zsplit_sums_step; [ Zpre_reorder_fractions.. | ] - | Zpre_reorder_fractions_step; [ .. | Zpre_reorder_fractions ] ]. -Ltac Zsplit_comparison := +Ltac pre_reorder_fractions := + try first [ split_sums_step; [ pre_reorder_fractions.. | ] + | pre_reorder_fractions_step; [ .. | pre_reorder_fractions ] ]. +Ltac split_comparison := match goal with | [ |- ?x <= ?x ] => reflexivity | [ H : _ >= _ |- _ ] @@ -674,7 +655,7 @@ Ltac Zsplit_comparison := | [ H : y <= 0 |- _ ] => fail | _ => destruct (Z_lt_le_dec 0 y) end; - [ apply Z_div_le; [ apply gt_lt_symmetry; assumption | ] + [ apply Z_div_le; [ apply Z.gt_lt_iff; assumption | ] | .. ] | [ |- ?x / ?y <= ?x / ?z ] => lazymatch goal with @@ -697,7 +678,7 @@ Ltac Zsplit_comparison := | [ |- ?x * (?y / ?z) <= (?x * ?y) / ?z ] => apply Z.div_mul_le end. -Ltac Zsplit_comparison_fin_step := +Ltac split_comparison_fin_step := match goal with | _ => assumption | _ => lia @@ -705,7 +686,7 @@ Ltac Zsplit_comparison_fin_step := | [ H : ?n * ?m < 0 |- _ ] => apply (proj1 (Z.lt_mul_0 n m)) in H; destruct H as [[??]|[??]] | [ H : ?n / ?m < 0 |- _ ] - => apply (proj1 (Zlt_div_0 n m)) in H; destruct H as [[[??]|[??]]?] + => apply (proj1 (lt_div_0 n m)) in H; destruct H as [[[??]|[??]]?] | [ H : (?x^?y) <= ?n < _, H' : ?n < 0 |- _ ] => assert (0 <= x^y) by zero_bounds; lia | [ H : (?x^?y) < 0 |- _ ] @@ -722,26 +703,26 @@ Ltac Zsplit_comparison_fin_step := | [ |- ?x <= ?y ] => is_evar x; reflexivity | [ |- ?x <= ?y ] => is_evar y; reflexivity end. -Ltac Zsplit_comparison_fin := repeat Zsplit_comparison_fin_step. -Ltac Zsimplify_fractions_step := +Ltac split_comparison_fin := repeat split_comparison_fin_step. +Ltac simplify_fractions_step := match goal with | _ => rewrite Z.div_mul by (try apply Z.pow_nonzero; zero_bounds) | [ |- context[?x * ?y / ?x] ] => rewrite (Z.mul_comm x y) | [ |- ?x <= ?x ] => reflexivity end. -Ltac Zsimplify_fractions := repeat Zsimplify_fractions_step. -Ltac Zsimplify_fractions_le := - Zpre_reorder_fractions; - [ repeat Zsplit_comparison; Zsplit_comparison_fin; zero_bounds.. - | Zsimplify_fractions ]. +Ltac simplify_fractions := repeat simplify_fractions_step. +Ltac simplify_fractions_le := + pre_reorder_fractions; + [ repeat split_comparison; split_comparison_fin; zero_bounds.. + | simplify_fractions ]. -Lemma Zlog2_nonneg' n a : n <= 0 -> n <= Z.log2 a. +Lemma log2_nonneg' n a : n <= 0 -> n <= Z.log2 a. Proof. intros; transitivity 0; auto with zarith. Qed. -Hint Resolve Zlog2_nonneg' : zarith. +Hint Resolve log2_nonneg' : zarith. (** We create separate databases for two directions of transformations involving [Z.log2]; combining them leads to loops. *) @@ -754,127 +735,133 @@ Create HintDb concl_log2. Hint Resolve (fun a b H => proj1 (Z.log2_lt_pow2 a b H)) (fun a b H => proj1 (Z.log2_le_pow2 a b H)) : concl_log2. Hint Resolve (fun a b H => proj2 (Z.log2_lt_pow2 a b H)) (fun a b H => proj2 (Z.log2_le_pow2 a b H)) : hyp_log2. -Lemma Zle_lt_to_log2 x y z : 0 <= z -> 0 < y -> 2^x <= y < 2^z -> x <= Z.log2 y < z. +Lemma le_lt_to_log2 x y z : 0 <= z -> 0 < y -> 2^x <= y < 2^z -> x <= Z.log2 y < z. Proof. destruct (Z_le_gt_dec 0 x); auto with concl_log2 lia. Qed. -Lemma Zdiv_x_y_x x y : 0 < x -> 0 < y -> x / y / x = 1 / y. +Lemma div_x_y_x x y : 0 < x -> 0 < y -> x / y / x = 1 / y. Proof. intros; rewrite Z.div_div, (Z.mul_comm y x), <- Z.div_div, Z.div_same by lia. reflexivity. Qed. -Hint Rewrite Zdiv_x_y_x using lia : zsimplify. +Hint Rewrite div_x_y_x using lia : zsimplify. -Lemma Zmod_opp_l_z_iff a b (H : b <> 0) : a mod b = 0 <-> (-a) mod b = 0. +Lemma mod_opp_l_z_iff a b (H : b <> 0) : a mod b = 0 <-> (-a) mod b = 0. Proof. split; intro H'; apply Z.mod_opp_l_z in H'; rewrite ?Z.opp_involutive in H'; assumption. Qed. -Lemma Zopp_eq_0_iff a : -a = 0 <-> a = 0. +Lemma opp_eq_0_iff a : -a = 0 <-> a = 0. Proof. lia. Qed. -Hint Rewrite <- Zmod_opp_l_z_iff using lia : zsimplify. -Hint Rewrite Zopp_eq_0_iff : zsimplify. +Hint Rewrite <- mod_opp_l_z_iff using lia : zsimplify. +Hint Rewrite opp_eq_0_iff : zsimplify. -Lemma Zsub_pos_bound a b X : 0 <= a < X -> 0 <= b < X -> -X < a - b < X. +Lemma sub_pos_bound a b X : 0 <= a < X -> 0 <= b < X -> -X < a - b < X. Proof. lia. Qed. -Lemma Zdiv_opp_l_complete a b (Hb : b <> 0) : -a/b = -(a/b) - (if Z_zerop (a mod b) then 0 else 1). +Lemma div_opp_l_complete a b (Hb : b <> 0) : -a/b = -(a/b) - (if Z_zerop (a mod b) then 0 else 1). Proof. destruct (Z_zerop (a mod b)); autorewrite with zsimplify push_Zopp; reflexivity. Qed. -Lemma Zdiv_opp_l_complete' a b (Hb : b <> 0) : -(a/b) = -a/b + (if Z_zerop (a mod b) then 0 else 1). +Lemma div_opp_l_complete' a b (Hb : b <> 0) : -(a/b) = -a/b + (if Z_zerop (a mod b) then 0 else 1). Proof. destruct (Z_zerop (a mod b)); autorewrite with zsimplify pull_Zopp; lia. Qed. -Hint Rewrite Zdiv_opp_l_complete using lia : pull_Zopp. -Hint Rewrite Zdiv_opp_l_complete' using lia : push_Zopp. +Hint Rewrite Z.div_opp_l_complete using lia : pull_Zopp. +Hint Rewrite Z.div_opp_l_complete' using lia : push_Zopp. -Lemma Zdiv_opp a : a <> 0 -> -a / a = -1. +Lemma div_opp a : a <> 0 -> -a / a = -1. Proof. intros; autorewrite with pull_Zopp zsimplify; lia. Qed. -Hint Rewrite Zdiv_opp using lia : zsimplify. +Hint Rewrite Z.div_opp using lia : zsimplify. -Lemma Zdiv_sub_1_0 x : x > 0 -> (x - 1) / x = 0. +Lemma div_sub_1_0 x : x > 0 -> (x - 1) / x = 0. Proof. auto with zarith lia. Qed. -Hint Rewrite Zdiv_sub_1_0 using lia : zsimplify. +Hint Rewrite div_sub_1_0 using lia : zsimplify. -Lemma Zsub_pos_bound_div a b X : 0 <= a < X -> 0 <= b < X -> -1 <= (a - b) / X <= 0. +Lemma sub_pos_bound_div a b X : 0 <= a < X -> 0 <= b < X -> -1 <= (a - b) / X <= 0. Proof. - intros H0 H1; pose proof (Zsub_pos_bound a b X H0 H1). + intros H0 H1; pose proof (Z.sub_pos_bound a b X H0 H1). assert (Hn : -X <= a - b) by lia. assert (Hp : a - b <= X - 1) by lia. split; etransitivity; [ | apply Z_div_le, Hn; lia | apply Z_div_le, Hp; lia | ]; instantiate; autorewrite with zsimplify; try reflexivity. Qed. -Hint Resolve (fun a b X H0 H1 => proj1 (Zsub_pos_bound_div a b X H0 H1)) - (fun a b X H0 H1 => proj1 (Zsub_pos_bound_div a b X H0 H1)) : zarith. +Hint Resolve (fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1)) + (fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1)) : zarith. -Lemma Zsub_pos_bound_div_eq a b X : 0 <= a < X -> 0 <= b < X -> (a - b) / X = if a 0 <= b < X -> (a - b) / X = if a 0); [ lia | ]. autorewrite with zstrip_div; auto with zarith lia. } { autorewrite with zstrip_div; auto with zarith lia. } Qed. -Lemma Zadd_opp_pos_bound_div_eq a b X : 0 <= a < X -> 0 <= b < X -> (-b + a) / X = if a 0 <= b < X -> (-b + a) / X = if a 0 = a / b. +Lemma div_small_sym a b : 0 <= a < b -> 0 = a / b. Proof. intros; symmetry; apply Z.div_small; assumption. Qed. -Lemma Zmod_small_sym a b : 0 <= a < b -> a = a mod b. +Lemma mod_small_sym a b : 0 <= a < b -> a = a mod b. Proof. intros; symmetry; apply Z.mod_small; assumption. Qed. -Hint Resolve Zdiv_small_sym Zmod_small_sym : zarith. +Hint Resolve div_small_sym mod_small_sym : zarith. -Lemma Zdiv_add' a b c : c <> 0 -> (a + c * b) / c = a / c + b. +Lemma div_add' a b c : c <> 0 -> (a + c * b) / c = a / c + b. Proof. intro; rewrite <- Z.div_add, (Z.mul_comm c); try lia. Qed. -Lemma Zdiv_add_l' a b c : b <> 0 -> (b * a + c) / b = a + c / b. +Lemma div_add_l' a b c : b <> 0 -> (b * a + c) / b = a + c / b. Proof. intro; rewrite <- Z.div_add_l, (Z.mul_comm b); lia. Qed. -Hint Rewrite Zdiv_add_l' Zdiv_add' using lia : zsimplify. +Hint Rewrite div_add_l' div_add' using lia : zsimplify. -Lemma Zdiv_add_sub_l a b c d : b <> 0 -> (a * b + c - d) / b = a + (c - d) / b. +Lemma div_add_sub_l a b c d : b <> 0 -> (a * b + c - d) / b = a + (c - d) / b. Proof. rewrite <- Z.add_sub_assoc; apply Z.div_add_l. Qed. -Lemma Zdiv_add_sub_l' a b c d : b <> 0 -> (b * a + c - d) / b = a + (c - d) / b. -Proof. rewrite <- Z.add_sub_assoc; apply Zdiv_add_l'. Qed. +Lemma div_add_sub_l' a b c d : b <> 0 -> (b * a + c - d) / b = a + (c - d) / b. +Proof. rewrite <- Z.add_sub_assoc; apply Z.div_add_l'. Qed. -Lemma Zdiv_add_sub a b c d : c <> 0 -> (a + b * c - d) / c = (a - d) / c + b. -Proof. rewrite (Z.add_comm _ (_ * _)), (Z.add_comm (_ / _)); apply Zdiv_add_sub_l. Qed. +Lemma div_add_sub a b c d : c <> 0 -> (a + b * c - d) / c = (a - d) / c + b. +Proof. rewrite (Z.add_comm _ (_ * _)), (Z.add_comm (_ / _)); apply Z.div_add_sub_l. Qed. -Lemma Zdiv_add_sub' a b c d : c <> 0 -> (a + c * b - d) / c = (a - d) / c + b. -Proof. rewrite (Z.add_comm _ (_ * _)), (Z.add_comm (_ / _)); apply Zdiv_add_sub_l'. Qed. +Lemma div_add_sub' a b c d : c <> 0 -> (a + c * b - d) / c = (a - d) / c + b. +Proof. rewrite (Z.add_comm _ (_ * _)), (Z.add_comm (_ / _)); apply Z.div_add_sub_l'. Qed. -Hint Rewrite Zdiv_add_sub Zdiv_add_sub' Zdiv_add_sub_l Zdiv_add_sub_l' using lia : zsimplify. +Hint Rewrite Z.div_add_sub Z.div_add_sub' Z.div_add_sub_l Z.div_add_sub_l' using lia : zsimplify. -Lemma Zdiv_mul_skip a b k : 0 < b -> 0 < k -> a * b / k / b = a / k. +Lemma div_mul_skip a b k : 0 < b -> 0 < k -> a * b / k / b = a / k. Proof. intros; rewrite Z.div_div, (Z.mul_comm k), <- Z.div_div by lia. autorewrite with zsimplify; reflexivity. Qed. -Lemma Zdiv_mul_skip' a b k : 0 < b -> 0 < k -> b * a / k / b = a / k. +Lemma div_mul_skip' a b k : 0 < b -> 0 < k -> b * a / k / b = a / k. Proof. intros; rewrite Z.div_div, (Z.mul_comm k), <- Z.div_div by lia. autorewrite with zsimplify; reflexivity. Qed. -Hint Rewrite Zdiv_mul_skip Zdiv_mul_skip' using lia : zsimplify. +Hint Rewrite Z.div_mul_skip Z.div_mul_skip' using lia : zsimplify. +End Z. + +Module Export BoundsTactics. + Ltac prime_bound := Z.prime_bound. + Ltac zero_bounds := Z.zero_bounds. +End BoundsTactics. -- cgit v1.2.3 From 77d576d027919445c57e6dbe9e4635c716fb05e3 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 2 Jul 2016 12:19:56 -0700 Subject: Indentation in ZUtil --- src/Util/ZUtil.v | 1368 +++++++++++++++++++++++++++--------------------------- 1 file changed, 684 insertions(+), 684 deletions(-) diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index b3b11fc0c..ab107b7a2 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -44,296 +44,296 @@ Hint Rewrite Z.div_small_iff using lia : zstrip_div. Create HintDb zstrip_div. Module Z. -Lemma positive_is_nonzero : forall x, x > 0 -> x <> 0. -Proof. intros; omega. Qed. - -Hint Resolve positive_is_nonzero : zarith. - -Lemma div_positive_gt_0 : forall a b, a > 0 -> b > 0 -> a mod b = 0 -> - a / b > 0. -Proof. - intros; rewrite Z.gt_lt_iff. - apply Z.div_str_pos. - split; intuition. - apply Z.divide_pos_le; try (apply Zmod_divide); omega. -Qed. - -Lemma elim_mod : forall a b m, a = b -> a mod m = b mod m. -Proof. intros; subst; auto. Qed. - -Hint Resolve elim_mod : zarith. - -Lemma mod_add_l : forall a b c, b <> 0 -> (a * b + c) mod b = c mod b. -Proof. intros; rewrite (Z.add_comm _ c); autorewrite with zsimplify; reflexivity. Qed. -Hint Rewrite mod_add_l using lia : zsimplify. - -Lemma mod_add' : forall a b c, b <> 0 -> (a + b * c) mod b = a mod b. -Proof. intros; rewrite (Z.mul_comm _ c); autorewrite with zsimplify; reflexivity. Qed. -Lemma mod_add_l' : forall a b c, a <> 0 -> (a * b + c) mod a = c mod a. -Proof. intros; rewrite (Z.mul_comm _ b); autorewrite with zsimplify; reflexivity. Qed. -Hint Rewrite mod_add' mod_add_l' using lia : zsimplify. - -Lemma pos_pow_nat_pos : forall x n, - Z.pos x ^ Z.of_nat n > 0. -Proof. - do 2 (intros; induction n; subst; simpl in *; auto with zarith). - rewrite <- Pos.add_1_r, Zpower_pos_is_exp. - apply Zmult_gt_0_compat; auto; reflexivity. -Qed. - -Lemma div_mul' : forall a b : Z, b <> 0 -> (b * a) / b = a. -Proof. intros. rewrite Z.mul_comm. apply Z.div_mul; auto. Qed. -Hint Rewrite div_mul' using lia : zsimplify. - -(** TODO: Should we get rid of this duplicate? *) -Notation gt0_neq0 := positive_is_nonzero (only parsing). - -Lemma pow_Z2N_Zpow : forall a n, 0 <= a -> - ((Z.to_nat a) ^ n = Z.to_nat (a ^ Z.of_nat n)%Z)%nat. -Proof. - intros; induction n; try reflexivity. - rewrite Nat2Z.inj_succ. - rewrite pow_succ_r by apply le_0_n. - rewrite Z.pow_succ_r by apply Zle_0_nat. - rewrite IHn. - rewrite Z2Nat.inj_mul; auto using Z.pow_nonneg. -Qed. - -Lemma pow_Zpow : forall a n : nat, Z.of_nat (a ^ n) = Z.of_nat a ^ Z.of_nat n. -Proof with auto using Zle_0_nat, Z.pow_nonneg. - intros; apply Z2Nat.inj... - rewrite <- pow_Z2N_Zpow, !Nat2Z.id... -Qed. - -Lemma mod_exp_0 : forall a x m, x > 0 -> m > 1 -> a mod m = 0 -> - a ^ x mod m = 0. -Proof. - intros. - replace x with (Z.of_nat (Z.to_nat x)) in * by (apply Z2Nat.id; omega). - induction (Z.to_nat x). { - simpl in *; omega. - } { - rewrite Nat2Z.inj_succ in *. - rewrite Z.pow_succ_r by omega. - rewrite Z.mul_mod by omega. - case_eq n; intros. { - subst. simpl. - rewrite Zmod_1_l by omega. - rewrite H1. - apply Zmod_0_l. + Lemma positive_is_nonzero : forall x, x > 0 -> x <> 0. + Proof. intros; omega. Qed. + + Hint Resolve positive_is_nonzero : zarith. + + Lemma div_positive_gt_0 : forall a b, a > 0 -> b > 0 -> a mod b = 0 -> + a / b > 0. + Proof. + intros; rewrite Z.gt_lt_iff. + apply Z.div_str_pos. + split; intuition. + apply Z.divide_pos_le; try (apply Zmod_divide); omega. + Qed. + + Lemma elim_mod : forall a b m, a = b -> a mod m = b mod m. + Proof. intros; subst; auto. Qed. + + Hint Resolve elim_mod : zarith. + + Lemma mod_add_l : forall a b c, b <> 0 -> (a * b + c) mod b = c mod b. + Proof. intros; rewrite (Z.add_comm _ c); autorewrite with zsimplify; reflexivity. Qed. + Hint Rewrite mod_add_l using lia : zsimplify. + + Lemma mod_add' : forall a b c, b <> 0 -> (a + b * c) mod b = a mod b. + Proof. intros; rewrite (Z.mul_comm _ c); autorewrite with zsimplify; reflexivity. Qed. + Lemma mod_add_l' : forall a b c, a <> 0 -> (a * b + c) mod a = c mod a. + Proof. intros; rewrite (Z.mul_comm _ b); autorewrite with zsimplify; reflexivity. Qed. + Hint Rewrite mod_add' mod_add_l' using lia : zsimplify. + + Lemma pos_pow_nat_pos : forall x n, + Z.pos x ^ Z.of_nat n > 0. + Proof. + do 2 (intros; induction n; subst; simpl in *; auto with zarith). + rewrite <- Pos.add_1_r, Zpower_pos_is_exp. + apply Zmult_gt_0_compat; auto; reflexivity. + Qed. + + Lemma div_mul' : forall a b : Z, b <> 0 -> (b * a) / b = a. + Proof. intros. rewrite Z.mul_comm. apply Z.div_mul; auto. Qed. + Hint Rewrite div_mul' using lia : zsimplify. + + (** TODO: Should we get rid of this duplicate? *) + Notation gt0_neq0 := positive_is_nonzero (only parsing). + + Lemma pow_Z2N_Zpow : forall a n, 0 <= a -> + ((Z.to_nat a) ^ n = Z.to_nat (a ^ Z.of_nat n)%Z)%nat. + Proof. + intros; induction n; try reflexivity. + rewrite Nat2Z.inj_succ. + rewrite pow_succ_r by apply le_0_n. + rewrite Z.pow_succ_r by apply Zle_0_nat. + rewrite IHn. + rewrite Z2Nat.inj_mul; auto using Z.pow_nonneg. + Qed. + + Lemma pow_Zpow : forall a n : nat, Z.of_nat (a ^ n) = Z.of_nat a ^ Z.of_nat n. + Proof with auto using Zle_0_nat, Z.pow_nonneg. + intros; apply Z2Nat.inj... + rewrite <- pow_Z2N_Zpow, !Nat2Z.id... + Qed. + + Lemma mod_exp_0 : forall a x m, x > 0 -> m > 1 -> a mod m = 0 -> + a ^ x mod m = 0. + Proof. + intros. + replace x with (Z.of_nat (Z.to_nat x)) in * by (apply Z2Nat.id; omega). + induction (Z.to_nat x). { + simpl in *; omega. + } { + rewrite Nat2Z.inj_succ in *. + rewrite Z.pow_succ_r by omega. + rewrite Z.mul_mod by omega. + case_eq n; intros. { + subst. simpl. + rewrite Zmod_1_l by omega. + rewrite H1. + apply Zmod_0_l. + } { + subst. + rewrite IHn by (rewrite Nat2Z.inj_succ in *; omega). + rewrite H1. + auto. + } + } + Qed. + + Lemma mod_pow : forall (a m b : Z), (0 <= b) -> (m <> 0) -> + a ^ b mod m = (a mod m) ^ b mod m. + Proof. + intros; rewrite <- (Z2Nat.id b) by auto. + induction (Z.to_nat b); auto. + rewrite Nat2Z.inj_succ. + do 2 rewrite Z.pow_succ_r by apply Nat2Z.is_nonneg. + rewrite Z.mul_mod by auto. + rewrite (Z.mul_mod (a mod m) ((a mod m) ^ Z.of_nat n) m) by auto. + rewrite <- IHn by auto. + rewrite Z.mod_mod by auto. + reflexivity. + Qed. + + Ltac divide_exists_mul := let k := fresh "k" in + match goal with + | [ H : (?a | ?b) |- _ ] => apply Z.mod_divide in H; try apply Zmod_divides in H; destruct H as [k H] + | [ |- (?a | ?b) ] => apply Z.mod_divide; try apply Zmod_divides + end; (omega || auto). + + Lemma divide_mul_div: forall a b c (a_nonzero : a <> 0) (c_nonzero : c <> 0), + (a | b * (a / c)) -> (c | a) -> (c | b). + Proof. + intros ? ? ? ? ? divide_a divide_c_a; do 2 divide_exists_mul. + rewrite divide_c_a in divide_a. + rewrite div_mul' in divide_a by auto. + replace (b * k) with (k * b) in divide_a by ring. + replace (c * k * k0) with (k * (k0 * c)) in divide_a by ring. + rewrite Z.mul_cancel_l in divide_a by (intuition; rewrite H in divide_c_a; ring_simplify in divide_a; intuition). + eapply Zdivide_intro; eauto. + Qed. + + Lemma divide2_even_iff : forall n, (2 | n) <-> Z.even n = true. + Proof. + intro; split. { + intro divide2_n. + divide_exists_mul; [ | pose proof (Z.mod_pos_bound n 2); omega]. + rewrite divide2_n. + apply Z.even_mul. } { - subst. - rewrite IHn by (rewrite Nat2Z.inj_succ in *; omega). - rewrite H1. - auto. + intro n_even. + pose proof (Zmod_even n). + rewrite n_even in H. + apply Zmod_divide; omega || auto. } - } -Qed. - -Lemma mod_pow : forall (a m b : Z), (0 <= b) -> (m <> 0) -> - a ^ b mod m = (a mod m) ^ b mod m. -Proof. - intros; rewrite <- (Z2Nat.id b) by auto. - induction (Z.to_nat b); auto. - rewrite Nat2Z.inj_succ. - do 2 rewrite Z.pow_succ_r by apply Nat2Z.is_nonneg. - rewrite Z.mul_mod by auto. - rewrite (Z.mul_mod (a mod m) ((a mod m) ^ Z.of_nat n) m) by auto. - rewrite <- IHn by auto. - rewrite Z.mod_mod by auto. - reflexivity. -Qed. - -Ltac divide_exists_mul := let k := fresh "k" in -match goal with -| [ H : (?a | ?b) |- _ ] => apply Z.mod_divide in H; try apply Zmod_divides in H; destruct H as [k H] -| [ |- (?a | ?b) ] => apply Z.mod_divide; try apply Zmod_divides -end; (omega || auto). - -Lemma divide_mul_div: forall a b c (a_nonzero : a <> 0) (c_nonzero : c <> 0), - (a | b * (a / c)) -> (c | a) -> (c | b). -Proof. - intros ? ? ? ? ? divide_a divide_c_a; do 2 divide_exists_mul. - rewrite divide_c_a in divide_a. - rewrite div_mul' in divide_a by auto. - replace (b * k) with (k * b) in divide_a by ring. - replace (c * k * k0) with (k * (k0 * c)) in divide_a by ring. - rewrite Z.mul_cancel_l in divide_a by (intuition; rewrite H in divide_c_a; ring_simplify in divide_a; intuition). - eapply Zdivide_intro; eauto. -Qed. - -Lemma divide2_even_iff : forall n, (2 | n) <-> Z.even n = true. -Proof. - intro; split. { - intro divide2_n. - divide_exists_mul; [ | pose proof (Z.mod_pos_bound n 2); omega]. - rewrite divide2_n. - apply Z.even_mul. - } { - intro n_even. - pose proof (Zmod_even n). - rewrite n_even in H. - apply Zmod_divide; omega || auto. - } -Qed. - -Lemma prime_odd_or_2 : forall p (prime_p : prime p), p = 2 \/ Z.odd p = true. -Proof. - intros. - apply Decidable.imp_not_l; try apply Z.eq_decidable. - intros p_neq2. - pose proof (Zmod_odd p) as mod_odd. - destruct (Sumbool.sumbool_of_bool (Z.odd p)) as [? | p_not_odd]; auto. - rewrite p_not_odd in mod_odd. - apply Zmod_divides in mod_odd; try omega. - destruct mod_odd as [c c_id]. - rewrite Z.mul_comm in c_id. - apply Zdivide_intro in c_id. - apply prime_divisors in c_id; auto. - destruct c_id; [omega | destruct H; [omega | destruct H; auto]]. - pose proof (prime_ge_2 p prime_p); omega. -Qed. - -Lemma mul_div_eq : forall a m, m > 0 -> m * (a / m) = (a - a mod m). -Proof. - intros. - rewrite (Z_div_mod_eq a m) at 2 by auto. - ring. -Qed. - -Lemma mul_div_eq' : (forall a m, m > 0 -> (a / m) * m = (a - a mod m))%Z. -Proof. - intros. - rewrite (Z_div_mod_eq a m) at 2 by auto. - ring. -Qed. - -Hint Rewrite mul_div_eq mul_div_eq' using lia : zdiv_to_mod. -Hint Rewrite <- mul_div_eq' using lia : zmod_to_div. - -Ltac prime_bound := match goal with -| [ H : prime ?p |- _ ] => pose proof (prime_ge_2 p H); try omega -end. - -Lemma testbit_low : forall n x i, (0 <= i < n) -> - Z.testbit x i = Z.testbit (Z.land x (Z.ones n)) i. -Proof. - intros. - rewrite Z.land_ones by omega. - symmetry. - apply Z.mod_pow2_bits_low. - omega. -Qed. - - -Lemma testbit_shiftl : forall i, (0 <= i) -> forall a b n, (i < n) -> - Z.testbit (a + Z.shiftl b n) i = Z.testbit a i. -Proof. - intros. - erewrite Z.testbit_low; eauto. - rewrite Z.land_ones, Z.shiftl_mul_pow2 by omega. - rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 n); omega). - auto using Z.mod_pow2_bits_low. -Qed. - -Lemma mod_div_eq0 : forall a b, 0 < b -> (a mod b) / b = 0. -Proof. - intros. - apply Z.div_small. - auto using Z.mod_pos_bound. -Qed. -Hint Rewrite mod_div_eq0 using lia : zsimplify. - -Lemma shiftr_add_land : forall n m a b, (n <= m)%nat -> - Z.shiftr ((Z.land a (Z.ones (Z.of_nat n))) + (Z.shiftl b (Z.of_nat n))) (Z.of_nat m) = Z.shiftr b (Z.of_nat (m - n)). -Proof. - intros. - rewrite Z.land_ones by apply Nat2Z.is_nonneg. - rewrite !Z.shiftr_div_pow2 by apply Nat2Z.is_nonneg. - rewrite Z.shiftl_mul_pow2 by apply Nat2Z.is_nonneg. - rewrite (le_plus_minus n m) at 1 by assumption. - rewrite Nat2Z.inj_add. - rewrite Z.pow_add_r by apply Nat2Z.is_nonneg. - rewrite <- Z.div_div by first - [ pose proof (Z.pow_pos_nonneg 2 (Z.of_nat n)); omega - | apply Z.pow_pos_nonneg; omega ]. - rewrite Z.div_add by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat n)); omega). - rewrite mod_div_eq0 by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat n)); omega); auto. -Qed. - -Lemma land_add_land : forall n m a b, (m <= n)%nat -> - Z.land ((Z.land a (Z.ones (Z.of_nat n))) + (Z.shiftl b (Z.of_nat n))) (Z.ones (Z.of_nat m)) = Z.land a (Z.ones (Z.of_nat m)). -Proof. - intros. - rewrite !Z.land_ones by apply Nat2Z.is_nonneg. - rewrite Z.shiftl_mul_pow2 by apply Nat2Z.is_nonneg. - replace (b * 2 ^ Z.of_nat n) with - ((b * 2 ^ Z.of_nat (n - m)) * 2 ^ Z.of_nat m) by - (rewrite (le_plus_minus m n) at 2; try assumption; - rewrite Nat2Z.inj_add, Z.pow_add_r by apply Nat2Z.is_nonneg; ring). - rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat m)); omega). - symmetry. apply Znumtheory.Zmod_div_mod; try (apply Z.pow_pos_nonneg; omega). - rewrite (le_plus_minus m n) by assumption. - rewrite Nat2Z.inj_add, Z.pow_add_r by apply Nat2Z.is_nonneg. - apply Z.divide_factor_l. -Qed. - -Lemma div_pow2succ : forall n x, (0 <= x) -> - n / 2 ^ Z.succ x = Z.div2 (n / 2 ^ x). -Proof. - intros. - rewrite Z.pow_succ_r, Z.mul_comm by auto. - rewrite <- Z.div_div by (try apply Z.pow_nonzero; omega). - rewrite Zdiv2_div. - reflexivity. -Qed. - -Lemma shiftr_succ : forall n x, - Z.shiftr n (Z.succ x) = Z.shiftr (Z.shiftr n x) 1. -Proof. - intros. - rewrite Z.shiftr_shiftr by omega. - reflexivity. -Qed. - - -Definition shiftl_by n a := Z.shiftl a n. - -Lemma shiftl_by_mul_pow2 : forall n a, 0 <= n -> Z.mul (2 ^ n) a = Z.shiftl_by n a. -Proof. - intros. - unfold Z.shiftl_by. - rewrite Z.shiftl_mul_pow2 by assumption. - apply Z.mul_comm. -Qed. - -Lemma map_shiftl : forall n l, 0 <= n -> map (Z.mul (2 ^ n)) l = map (Z.shiftl_by n) l. -Proof. - intros; induction l; auto using Z.shiftl_by_mul_pow2. - simpl. - rewrite IHl. - f_equal. - apply Z.shiftl_by_mul_pow2. - assumption. -Qed. - -Lemma odd_mod : forall a b, (b <> 0)%Z -> - Z.odd (a mod b) = if Z.odd b then xorb (Z.odd a) (Z.odd (a / b)) else Z.odd a. -Proof. - intros. - rewrite Zmod_eq_full by assumption. - rewrite <-Z.add_opp_r, Z.odd_add, Z.odd_opp, Z.odd_mul. - case_eq (Z.odd b); intros; rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; auto using Bool.xorb_false_r. -Qed. - -Lemma mod_same_pow : forall a b c, 0 <= c <= b -> a ^ b mod a ^ c = 0. -Proof. - intros. - replace b with (b - c + c) by ring. - rewrite Z.pow_add_r by omega. - apply Z_mod_mult. -Qed. -Hint Rewrite mod_same_pow using lia : zsimplify. + Qed. + + Lemma prime_odd_or_2 : forall p (prime_p : prime p), p = 2 \/ Z.odd p = true. + Proof. + intros. + apply Decidable.imp_not_l; try apply Z.eq_decidable. + intros p_neq2. + pose proof (Zmod_odd p) as mod_odd. + destruct (Sumbool.sumbool_of_bool (Z.odd p)) as [? | p_not_odd]; auto. + rewrite p_not_odd in mod_odd. + apply Zmod_divides in mod_odd; try omega. + destruct mod_odd as [c c_id]. + rewrite Z.mul_comm in c_id. + apply Zdivide_intro in c_id. + apply prime_divisors in c_id; auto. + destruct c_id; [omega | destruct H; [omega | destruct H; auto]]. + pose proof (prime_ge_2 p prime_p); omega. + Qed. + + Lemma mul_div_eq : forall a m, m > 0 -> m * (a / m) = (a - a mod m). + Proof. + intros. + rewrite (Z_div_mod_eq a m) at 2 by auto. + ring. + Qed. + + Lemma mul_div_eq' : (forall a m, m > 0 -> (a / m) * m = (a - a mod m))%Z. + Proof. + intros. + rewrite (Z_div_mod_eq a m) at 2 by auto. + ring. + Qed. + + Hint Rewrite mul_div_eq mul_div_eq' using lia : zdiv_to_mod. + Hint Rewrite <- mul_div_eq' using lia : zmod_to_div. + + Ltac prime_bound := match goal with + | [ H : prime ?p |- _ ] => pose proof (prime_ge_2 p H); try omega + end. + + Lemma testbit_low : forall n x i, (0 <= i < n) -> + Z.testbit x i = Z.testbit (Z.land x (Z.ones n)) i. + Proof. + intros. + rewrite Z.land_ones by omega. + symmetry. + apply Z.mod_pow2_bits_low. + omega. + Qed. + + + Lemma testbit_shiftl : forall i, (0 <= i) -> forall a b n, (i < n) -> + Z.testbit (a + Z.shiftl b n) i = Z.testbit a i. + Proof. + intros. + erewrite Z.testbit_low; eauto. + rewrite Z.land_ones, Z.shiftl_mul_pow2 by omega. + rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 n); omega). + auto using Z.mod_pow2_bits_low. + Qed. + + Lemma mod_div_eq0 : forall a b, 0 < b -> (a mod b) / b = 0. + Proof. + intros. + apply Z.div_small. + auto using Z.mod_pos_bound. + Qed. + Hint Rewrite mod_div_eq0 using lia : zsimplify. + + Lemma shiftr_add_land : forall n m a b, (n <= m)%nat -> + Z.shiftr ((Z.land a (Z.ones (Z.of_nat n))) + (Z.shiftl b (Z.of_nat n))) (Z.of_nat m) = Z.shiftr b (Z.of_nat (m - n)). + Proof. + intros. + rewrite Z.land_ones by apply Nat2Z.is_nonneg. + rewrite !Z.shiftr_div_pow2 by apply Nat2Z.is_nonneg. + rewrite Z.shiftl_mul_pow2 by apply Nat2Z.is_nonneg. + rewrite (le_plus_minus n m) at 1 by assumption. + rewrite Nat2Z.inj_add. + rewrite Z.pow_add_r by apply Nat2Z.is_nonneg. + rewrite <- Z.div_div by first + [ pose proof (Z.pow_pos_nonneg 2 (Z.of_nat n)); omega + | apply Z.pow_pos_nonneg; omega ]. + rewrite Z.div_add by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat n)); omega). + rewrite mod_div_eq0 by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat n)); omega); auto. + Qed. + + Lemma land_add_land : forall n m a b, (m <= n)%nat -> + Z.land ((Z.land a (Z.ones (Z.of_nat n))) + (Z.shiftl b (Z.of_nat n))) (Z.ones (Z.of_nat m)) = Z.land a (Z.ones (Z.of_nat m)). + Proof. + intros. + rewrite !Z.land_ones by apply Nat2Z.is_nonneg. + rewrite Z.shiftl_mul_pow2 by apply Nat2Z.is_nonneg. + replace (b * 2 ^ Z.of_nat n) with + ((b * 2 ^ Z.of_nat (n - m)) * 2 ^ Z.of_nat m) by + (rewrite (le_plus_minus m n) at 2; try assumption; + rewrite Nat2Z.inj_add, Z.pow_add_r by apply Nat2Z.is_nonneg; ring). + rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat m)); omega). + symmetry. apply Znumtheory.Zmod_div_mod; try (apply Z.pow_pos_nonneg; omega). + rewrite (le_plus_minus m n) by assumption. + rewrite Nat2Z.inj_add, Z.pow_add_r by apply Nat2Z.is_nonneg. + apply Z.divide_factor_l. + Qed. + + Lemma div_pow2succ : forall n x, (0 <= x) -> + n / 2 ^ Z.succ x = Z.div2 (n / 2 ^ x). + Proof. + intros. + rewrite Z.pow_succ_r, Z.mul_comm by auto. + rewrite <- Z.div_div by (try apply Z.pow_nonzero; omega). + rewrite Zdiv2_div. + reflexivity. + Qed. + + Lemma shiftr_succ : forall n x, + Z.shiftr n (Z.succ x) = Z.shiftr (Z.shiftr n x) 1. + Proof. + intros. + rewrite Z.shiftr_shiftr by omega. + reflexivity. + Qed. + + + Definition shiftl_by n a := Z.shiftl a n. + + Lemma shiftl_by_mul_pow2 : forall n a, 0 <= n -> Z.mul (2 ^ n) a = Z.shiftl_by n a. + Proof. + intros. + unfold Z.shiftl_by. + rewrite Z.shiftl_mul_pow2 by assumption. + apply Z.mul_comm. + Qed. + + Lemma map_shiftl : forall n l, 0 <= n -> map (Z.mul (2 ^ n)) l = map (Z.shiftl_by n) l. + Proof. + intros; induction l; auto using Z.shiftl_by_mul_pow2. + simpl. + rewrite IHl. + f_equal. + apply Z.shiftl_by_mul_pow2. + assumption. + Qed. + + Lemma odd_mod : forall a b, (b <> 0)%Z -> + Z.odd (a mod b) = if Z.odd b then xorb (Z.odd a) (Z.odd (a / b)) else Z.odd a. + Proof. + intros. + rewrite Zmod_eq_full by assumption. + rewrite <-Z.add_opp_r, Z.odd_add, Z.odd_opp, Z.odd_mul. + case_eq (Z.odd b); intros; rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; auto using Bool.xorb_false_r. + Qed. + + Lemma mod_same_pow : forall a b c, 0 <= c <= b -> a ^ b mod a ^ c = 0. + Proof. + intros. + replace b with (b - c + c) by ring. + rewrite Z.pow_add_r by omega. + apply Z_mod_mult. + Qed. + Hint Rewrite mod_same_pow using lia : zsimplify. Lemma ones_succ : forall x, (0 <= x) -> Z.ones (Z.succ x) = 2 ^ x + Z.ones x. @@ -423,442 +423,442 @@ Hint Rewrite mod_same_pow using lia : zsimplify. omega. Qed. -(* prove that combinations of known positive/nonnegative numbers are positive/nonnegative *) -Ltac zero_bounds' := - repeat match goal with - | [ |- 0 <= _ + _] => apply Z.add_nonneg_nonneg - | [ |- 0 <= _ - _] => apply Z.le_0_sub - | [ |- 0 <= _ * _] => apply Z.mul_nonneg_nonneg - | [ |- 0 <= _ / _] => apply Z.div_pos - | [ |- 0 <= _ ^ _ ] => apply Z.pow_nonneg - | [ |- 0 <= Z.shiftr _ _] => apply Z.shiftr_nonneg - | [ |- 0 < _ + _] => try solve [apply Z.add_pos_nonneg; zero_bounds']; - try solve [apply Z.add_nonneg_pos; zero_bounds'] - | [ |- 0 < _ - _] => apply Z.lt_0_sub - | [ |- 0 < _ * _] => apply Z.lt_0_mul; left; split - | [ |- 0 < _ / _] => apply Z.div_str_pos - | [ |- 0 < _ ^ _ ] => apply Z.pow_pos_nonneg - end; try omega; try prime_bound; auto. - -Ltac zero_bounds := try omega; try prime_bound; zero_bounds'. - -Hint Extern 1 => progress zero_bounds : zero_bounds. - -Lemma ones_nonneg : forall i, (0 <= i) -> 0 <= Z.ones i. -Proof. - apply natlike_ind. - + unfold Z.ones. simpl; omega. - + intros. - rewrite Z.ones_succ by assumption. - zero_bounds. -Qed. - -Lemma ones_pos_pos : forall i, (0 < i) -> 0 < Z.ones i. -Proof. - intros. - unfold Z.ones. - rewrite Z.shiftl_1_l. - apply Z.lt_succ_lt_pred. - apply Z.pow_gt_1; omega. -Qed. - -Lemma N_le_1_l : forall p, (1 <= N.pos p)%N. -Proof. - destruct p; cbv; congruence. -Qed. - -Lemma Pos_land_upper_bound_l : forall a b, (Pos.land a b <= N.pos a)%N. -Proof. - induction a; destruct b; intros; try solve [cbv; congruence]; - simpl; specialize (IHa b); case_eq (Pos.land a b); intro; simpl; - try (apply N_le_1_l || apply N.le_0_l); intro land_eq; - rewrite land_eq in *; unfold N.le, N.compare in *; - rewrite ?Pos.compare_xI_xI, ?Pos.compare_xO_xI, ?Pos.compare_xO_xO; - try assumption. - destruct (p ?=a)%positive; cbv; congruence. -Qed. - -Lemma land_upper_bound_l : forall a b, (0 <= a) -> (0 <= b) -> - Z.land a b <= a. -Proof. - intros. - destruct a, b; try solve [exfalso; auto]; try solve [cbv; congruence]. - cbv [Z.land]. - rewrite <-N2Z.inj_pos, <-N2Z.inj_le. - auto using Pos_land_upper_bound_l. -Qed. - -Lemma land_upper_bound_r : forall a b, (0 <= a) -> (0 <= b) -> - Z.land a b <= b. -Proof. - intros. - rewrite Z.land_comm. - auto using Z.land_upper_bound_l. -Qed. - -Lemma le_fold_right_max : forall low l x, (forall y, In y l -> low <= y) -> - In x l -> x <= fold_right Z.max low l. -Proof. - induction l; intros ? lower_bound In_list; [cbv [In] in *; intuition | ]. - simpl. - destruct (in_inv In_list); subst. - + apply Z.le_max_l. - + etransitivity. - - apply IHl; auto; intuition. - - apply Z.le_max_r. -Qed. - -Lemma le_fold_right_max_initial : forall low l, low <= fold_right Z.max low l. -Proof. - induction l; intros; try reflexivity. - etransitivity; [ apply IHl | apply Z.le_max_r ]. -Qed. - -Ltac ltb_to_lt := - repeat match goal with - | [ H : (?x let H' := fresh in - rename H into H'; - pose proof (Zlt_cases x y) as H; - rewrite H' in H; - clear H' - end. - -Ltac compare_to_sgn := - repeat match goal with - | [ H : _ |- _ ] => progress rewrite <- ?Z.sgn_neg_iff, <- ?Z.sgn_pos_iff, <- ?Z.sgn_null_iff in H - | _ => progress rewrite <- ?Z.sgn_neg_iff, <- ?Z.sgn_pos_iff, <- ?Z.sgn_null_iff - end. - -Local Ltac replace_to_const c := - repeat match goal with - | [ H : ?x = ?x |- _ ] => clear H - | [ H : ?x = c, H' : context[?x] |- _ ] => rewrite H in H' - | [ H : c = ?x, H' : context[?x] |- _ ] => rewrite <- H in H' - | [ H : ?x = c |- context[?x] ] => rewrite H - | [ H : c = ?x |- context[?x] ] => rewrite <- H - end. - -Lemma lt_div_0 n m : n / m < 0 <-> ((n < 0 < m \/ m < 0 < n) /\ 0 < -(n / m)). -Proof. - Z.compare_to_sgn; rewrite Z.sgn_opp; simpl. - pose proof (Zdiv_sgn n m) as H. - pose proof (Z.sgn_spec (n / m)) as H'. - repeat first [ progress intuition - | progress simpl in * - | congruence - | lia - | progress replace_to_const (-1) - | progress replace_to_const 0 - | progress replace_to_const 1 - | match goal with - | [ x : Z |- _ ] => destruct x - end ]. -Qed. - -Lemma two_times_x_minus_x x : 2 * x - x = x. -Proof. lia. Qed. - -Lemma mul_div_le x y z - (Hx : 0 <= x) (Hy : 0 <= y) (Hz : 0 < z) - (Hyz : y <= z) - : x * y / z <= x. -Proof. - transitivity (x * z / z); [ | rewrite Z.div_mul by lia; lia ]. - apply Z_div_le; nia. -Qed. - -Lemma div_mul_diff a b c - (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c) - : c * a / b - c * (a / b) <= c. -Proof. - pose proof (Z.mod_pos_bound a b). - etransitivity; [ | apply (mul_div_le c (a mod b) b); lia ]. - rewrite (Z_div_mod_eq a b) at 1 by lia. - rewrite Z.mul_add_distr_l. - replace (c * (b * (a / b))) with ((c * (a / b)) * b) by lia. - rewrite Z.div_add_l by lia. - lia. -Qed. - -Lemma div_mul_le_le a b c - : 0 <= a -> 0 < b -> 0 <= c -> c * (a / b) <= c * a / b <= c * (a / b) + c. -Proof. - pose proof (Z.div_mul_diff a b c); split; try apply Z.div_mul_le; lia. -Qed. - -Lemma div_mul_le_le_offset a b c - : 0 <= a -> 0 < b -> 0 <= c -> c * a / b - c <= c * (a / b). -Proof. - pose proof (Z.div_mul_le_le a b c); lia. -Qed. - -Hint Resolve Zmult_le_compat_r Zmult_le_compat_l Z_div_le Z.div_mul_le_le_offset Z.add_le_mono Z.sub_le_mono : zarith. - -(** * [Z.simplify_fractions_le] *) -(** The culmination of this series of tactics, - [Z.simplify_fractions_le], will use the fact that [a * (b / c) <= - (a * b) / c], and do some reasoning modulo associativity and - commutativity in [Z] to perform such a reduction. It may leave - over goals if it cannot prove that some denominators are non-zero. - If the rewrite [a * (b / c)] → [(a * b) / c] is safe to do on the - LHS of the goal, this tactic should not turn a solvable goal into - an unsolvable one. - - After running, the tactic does some basic rewriting to simplify - fractions, e.g., that [a * b / b = a]. *) -Ltac split_sums_step := - match goal with - | [ |- _ + _ <= _ ] - => etransitivity; [ eapply Z.add_le_mono | ] - | [ |- _ - _ <= _ ] - => etransitivity; [ eapply Z.sub_le_mono | ] - end. -Ltac split_sums := - try (split_sums_step; [ split_sums.. | ]). -Ltac pre_reorder_fractions_step := - match goal with - | [ |- context[?x / ?y * ?z] ] - => rewrite (Z.mul_comm (x / y) z) - | _ => let LHS := match goal with |- ?LHS <= ?RHS => LHS end in - match LHS with - | context G[?x * (?y / ?z)] - => let G' := context G[(x * y) / z] in - transitivity G' - end - end. -Ltac pre_reorder_fractions := - try first [ split_sums_step; [ pre_reorder_fractions.. | ] - | pre_reorder_fractions_step; [ .. | pre_reorder_fractions ] ]. -Ltac split_comparison := - match goal with - | [ |- ?x <= ?x ] => reflexivity - | [ H : _ >= _ |- _ ] - => apply Z.ge_le_iff in H - | [ |- ?x * ?y <= ?z * ?w ] - => lazymatch goal with - | [ H : 0 <= x |- _ ] => idtac - | [ H : x < 0 |- _ ] => fail - | _ => destruct (Z_lt_le_dec x 0) - end; - [ .. - | lazymatch goal with - | [ H : 0 <= y |- _ ] => idtac - | [ H : y < 0 |- _ ] => fail - | _ => destruct (Z_lt_le_dec y 0) + (* prove that combinations of known positive/nonnegative numbers are positive/nonnegative *) + Ltac zero_bounds' := + repeat match goal with + | [ |- 0 <= _ + _] => apply Z.add_nonneg_nonneg + | [ |- 0 <= _ - _] => apply Z.le_0_sub + | [ |- 0 <= _ * _] => apply Z.mul_nonneg_nonneg + | [ |- 0 <= _ / _] => apply Z.div_pos + | [ |- 0 <= _ ^ _ ] => apply Z.pow_nonneg + | [ |- 0 <= Z.shiftr _ _] => apply Z.shiftr_nonneg + | [ |- 0 < _ + _] => try solve [apply Z.add_pos_nonneg; zero_bounds']; + try solve [apply Z.add_nonneg_pos; zero_bounds'] + | [ |- 0 < _ - _] => apply Z.lt_0_sub + | [ |- 0 < _ * _] => apply Z.lt_0_mul; left; split + | [ |- 0 < _ / _] => apply Z.div_str_pos + | [ |- 0 < _ ^ _ ] => apply Z.pow_pos_nonneg + end; try omega; try prime_bound; auto. + + Ltac zero_bounds := try omega; try prime_bound; zero_bounds'. + + Hint Extern 1 => progress zero_bounds : zero_bounds. + + Lemma ones_nonneg : forall i, (0 <= i) -> 0 <= Z.ones i. + Proof. + apply natlike_ind. + + unfold Z.ones. simpl; omega. + + intros. + rewrite Z.ones_succ by assumption. + zero_bounds. + Qed. + + Lemma ones_pos_pos : forall i, (0 < i) -> 0 < Z.ones i. + Proof. + intros. + unfold Z.ones. + rewrite Z.shiftl_1_l. + apply Z.lt_succ_lt_pred. + apply Z.pow_gt_1; omega. + Qed. + + Lemma N_le_1_l : forall p, (1 <= N.pos p)%N. + Proof. + destruct p; cbv; congruence. + Qed. + + Lemma Pos_land_upper_bound_l : forall a b, (Pos.land a b <= N.pos a)%N. + Proof. + induction a; destruct b; intros; try solve [cbv; congruence]; + simpl; specialize (IHa b); case_eq (Pos.land a b); intro; simpl; + try (apply N_le_1_l || apply N.le_0_l); intro land_eq; + rewrite land_eq in *; unfold N.le, N.compare in *; + rewrite ?Pos.compare_xI_xI, ?Pos.compare_xO_xI, ?Pos.compare_xO_xO; + try assumption. + destruct (p ?=a)%positive; cbv; congruence. + Qed. + + Lemma land_upper_bound_l : forall a b, (0 <= a) -> (0 <= b) -> + Z.land a b <= a. + Proof. + intros. + destruct a, b; try solve [exfalso; auto]; try solve [cbv; congruence]. + cbv [Z.land]. + rewrite <-N2Z.inj_pos, <-N2Z.inj_le. + auto using Pos_land_upper_bound_l. + Qed. + + Lemma land_upper_bound_r : forall a b, (0 <= a) -> (0 <= b) -> + Z.land a b <= b. + Proof. + intros. + rewrite Z.land_comm. + auto using Z.land_upper_bound_l. + Qed. + + Lemma le_fold_right_max : forall low l x, (forall y, In y l -> low <= y) -> + In x l -> x <= fold_right Z.max low l. + Proof. + induction l; intros ? lower_bound In_list; [cbv [In] in *; intuition | ]. + simpl. + destruct (in_inv In_list); subst. + + apply Z.le_max_l. + + etransitivity. + - apply IHl; auto; intuition. + - apply Z.le_max_r. + Qed. + + Lemma le_fold_right_max_initial : forall low l, low <= fold_right Z.max low l. + Proof. + induction l; intros; try reflexivity. + etransitivity; [ apply IHl | apply Z.le_max_r ]. + Qed. + + Ltac ltb_to_lt := + repeat match goal with + | [ H : (?x let H' := fresh in + rename H into H'; + pose proof (Zlt_cases x y) as H; + rewrite H' in H; + clear H' + end. + + Ltac compare_to_sgn := + repeat match goal with + | [ H : _ |- _ ] => progress rewrite <- ?Z.sgn_neg_iff, <- ?Z.sgn_pos_iff, <- ?Z.sgn_null_iff in H + | _ => progress rewrite <- ?Z.sgn_neg_iff, <- ?Z.sgn_pos_iff, <- ?Z.sgn_null_iff + end. + + Local Ltac replace_to_const c := + repeat match goal with + | [ H : ?x = ?x |- _ ] => clear H + | [ H : ?x = c, H' : context[?x] |- _ ] => rewrite H in H' + | [ H : c = ?x, H' : context[?x] |- _ ] => rewrite <- H in H' + | [ H : ?x = c |- context[?x] ] => rewrite H + | [ H : c = ?x |- context[?x] ] => rewrite <- H + end. + + Lemma lt_div_0 n m : n / m < 0 <-> ((n < 0 < m \/ m < 0 < n) /\ 0 < -(n / m)). + Proof. + Z.compare_to_sgn; rewrite Z.sgn_opp; simpl. + pose proof (Zdiv_sgn n m) as H. + pose proof (Z.sgn_spec (n / m)) as H'. + repeat first [ progress intuition + | progress simpl in * + | congruence + | lia + | progress replace_to_const (-1) + | progress replace_to_const 0 + | progress replace_to_const 1 + | match goal with + | [ x : Z |- _ ] => destruct x + end ]. + Qed. + + Lemma two_times_x_minus_x x : 2 * x - x = x. + Proof. lia. Qed. + + Lemma mul_div_le x y z + (Hx : 0 <= x) (Hy : 0 <= y) (Hz : 0 < z) + (Hyz : y <= z) + : x * y / z <= x. + Proof. + transitivity (x * z / z); [ | rewrite Z.div_mul by lia; lia ]. + apply Z_div_le; nia. + Qed. + + Lemma div_mul_diff a b c + (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c) + : c * a / b - c * (a / b) <= c. + Proof. + pose proof (Z.mod_pos_bound a b). + etransitivity; [ | apply (mul_div_le c (a mod b) b); lia ]. + rewrite (Z_div_mod_eq a b) at 1 by lia. + rewrite Z.mul_add_distr_l. + replace (c * (b * (a / b))) with ((c * (a / b)) * b) by lia. + rewrite Z.div_add_l by lia. + lia. + Qed. + + Lemma div_mul_le_le a b c + : 0 <= a -> 0 < b -> 0 <= c -> c * (a / b) <= c * a / b <= c * (a / b) + c. + Proof. + pose proof (Z.div_mul_diff a b c); split; try apply Z.div_mul_le; lia. + Qed. + + Lemma div_mul_le_le_offset a b c + : 0 <= a -> 0 < b -> 0 <= c -> c * a / b - c <= c * (a / b). + Proof. + pose proof (Z.div_mul_le_le a b c); lia. + Qed. + + Hint Resolve Zmult_le_compat_r Zmult_le_compat_l Z_div_le Z.div_mul_le_le_offset Z.add_le_mono Z.sub_le_mono : zarith. + + (** * [Z.simplify_fractions_le] *) + (** The culmination of this series of tactics, + [Z.simplify_fractions_le], will use the fact that [a * (b / c) <= + (a * b) / c], and do some reasoning modulo associativity and + commutativity in [Z] to perform such a reduction. It may leave + over goals if it cannot prove that some denominators are non-zero. + If the rewrite [a * (b / c)] → [(a * b) / c] is safe to do on the + LHS of the goal, this tactic should not turn a solvable goal into + an unsolvable one. + + After running, the tactic does some basic rewriting to simplify + fractions, e.g., that [a * b / b = a]. *) + Ltac split_sums_step := + match goal with + | [ |- _ + _ <= _ ] + => etransitivity; [ eapply Z.add_le_mono | ] + | [ |- _ - _ <= _ ] + => etransitivity; [ eapply Z.sub_le_mono | ] + end. + Ltac split_sums := + try (split_sums_step; [ split_sums.. | ]). + Ltac pre_reorder_fractions_step := + match goal with + | [ |- context[?x / ?y * ?z] ] + => rewrite (Z.mul_comm (x / y) z) + | _ => let LHS := match goal with |- ?LHS <= ?RHS => LHS end in + match LHS with + | context G[?x * (?y / ?z)] + => let G' := context G[(x * y) / z] in + transitivity G' + end + end. + Ltac pre_reorder_fractions := + try first [ split_sums_step; [ pre_reorder_fractions.. | ] + | pre_reorder_fractions_step; [ .. | pre_reorder_fractions ] ]. + Ltac split_comparison := + match goal with + | [ |- ?x <= ?x ] => reflexivity + | [ H : _ >= _ |- _ ] + => apply Z.ge_le_iff in H + | [ |- ?x * ?y <= ?z * ?w ] + => lazymatch goal with + | [ H : 0 <= x |- _ ] => idtac + | [ H : x < 0 |- _ ] => fail + | _ => destruct (Z_lt_le_dec x 0) end; [ .. - | apply Zmult_le_compat; [ | | assumption | assumption ] ] ] - | [ |- ?x / ?y <= ?z / ?y ] - => lazymatch goal with - | [ H : 0 < y |- _ ] => idtac - | [ H : y <= 0 |- _ ] => fail - | _ => destruct (Z_lt_le_dec 0 y) - end; - [ apply Z_div_le; [ apply Z.gt_lt_iff; assumption | ] - | .. ] - | [ |- ?x / ?y <= ?x / ?z ] - => lazymatch goal with - | [ H : 0 <= x |- _ ] => idtac - | [ H : x < 0 |- _ ] => fail - | _ => destruct (Z_lt_le_dec x 0) - end; - [ .. - | lazymatch goal with - | [ H : 0 < z |- _ ] => idtac - | [ H : z <= 0 |- _ ] => fail - | _ => destruct (Z_lt_le_dec 0 z) + | lazymatch goal with + | [ H : 0 <= y |- _ ] => idtac + | [ H : y < 0 |- _ ] => fail + | _ => destruct (Z_lt_le_dec y 0) + end; + [ .. + | apply Zmult_le_compat; [ | | assumption | assumption ] ] ] + | [ |- ?x / ?y <= ?z / ?y ] + => lazymatch goal with + | [ H : 0 < y |- _ ] => idtac + | [ H : y <= 0 |- _ ] => fail + | _ => destruct (Z_lt_le_dec 0 y) end; - [ apply Z.div_le_compat_l; [ assumption | split; [ assumption | ] ] - | .. ] ] - | [ |- _ + _ <= _ + _ ] - => apply Z.add_le_mono - | [ |- _ - _ <= _ - _ ] - => apply Z.sub_le_mono - | [ |- ?x * (?y / ?z) <= (?x * ?y) / ?z ] - => apply Z.div_mul_le - end. -Ltac split_comparison_fin_step := - match goal with - | _ => assumption - | _ => lia - | _ => progress subst - | [ H : ?n * ?m < 0 |- _ ] - => apply (proj1 (Z.lt_mul_0 n m)) in H; destruct H as [[??]|[??]] - | [ H : ?n / ?m < 0 |- _ ] - => apply (proj1 (lt_div_0 n m)) in H; destruct H as [[[??]|[??]]?] - | [ H : (?x^?y) <= ?n < _, H' : ?n < 0 |- _ ] - => assert (0 <= x^y) by zero_bounds; lia - | [ H : (?x^?y) < 0 |- _ ] - => assert (0 <= x^y) by zero_bounds; lia - | [ H : (?x^?y) <= 0 |- _ ] - => let H' := fresh in - assert (H' : 0 <= x^y) by zero_bounds; - assert (x^y = 0) by lia; - clear H H' - | [ H : _^_ = 0 |- _ ] - => apply Z.pow_eq_0_iff in H; destruct H as [?|[??]] - | [ H : 0 <= ?x, H' : ?x - 1 < 0 |- _ ] - => assert (x = 0) by lia; clear H H' - | [ |- ?x <= ?y ] => is_evar x; reflexivity - | [ |- ?x <= ?y ] => is_evar y; reflexivity - end. -Ltac split_comparison_fin := repeat split_comparison_fin_step. -Ltac simplify_fractions_step := - match goal with - | _ => rewrite Z.div_mul by (try apply Z.pow_nonzero; zero_bounds) - | [ |- context[?x * ?y / ?x] ] - => rewrite (Z.mul_comm x y) - | [ |- ?x <= ?x ] => reflexivity - end. -Ltac simplify_fractions := repeat simplify_fractions_step. -Ltac simplify_fractions_le := - pre_reorder_fractions; - [ repeat split_comparison; split_comparison_fin; zero_bounds.. - | simplify_fractions ]. - -Lemma log2_nonneg' n a : n <= 0 -> n <= Z.log2 a. -Proof. - intros; transitivity 0; auto with zarith. -Qed. + [ apply Z_div_le; [ apply Z.gt_lt_iff; assumption | ] + | .. ] + | [ |- ?x / ?y <= ?x / ?z ] + => lazymatch goal with + | [ H : 0 <= x |- _ ] => idtac + | [ H : x < 0 |- _ ] => fail + | _ => destruct (Z_lt_le_dec x 0) + end; + [ .. + | lazymatch goal with + | [ H : 0 < z |- _ ] => idtac + | [ H : z <= 0 |- _ ] => fail + | _ => destruct (Z_lt_le_dec 0 z) + end; + [ apply Z.div_le_compat_l; [ assumption | split; [ assumption | ] ] + | .. ] ] + | [ |- _ + _ <= _ + _ ] + => apply Z.add_le_mono + | [ |- _ - _ <= _ - _ ] + => apply Z.sub_le_mono + | [ |- ?x * (?y / ?z) <= (?x * ?y) / ?z ] + => apply Z.div_mul_le + end. + Ltac split_comparison_fin_step := + match goal with + | _ => assumption + | _ => lia + | _ => progress subst + | [ H : ?n * ?m < 0 |- _ ] + => apply (proj1 (Z.lt_mul_0 n m)) in H; destruct H as [[??]|[??]] + | [ H : ?n / ?m < 0 |- _ ] + => apply (proj1 (lt_div_0 n m)) in H; destruct H as [[[??]|[??]]?] + | [ H : (?x^?y) <= ?n < _, H' : ?n < 0 |- _ ] + => assert (0 <= x^y) by zero_bounds; lia + | [ H : (?x^?y) < 0 |- _ ] + => assert (0 <= x^y) by zero_bounds; lia + | [ H : (?x^?y) <= 0 |- _ ] + => let H' := fresh in + assert (H' : 0 <= x^y) by zero_bounds; + assert (x^y = 0) by lia; + clear H H' + | [ H : _^_ = 0 |- _ ] + => apply Z.pow_eq_0_iff in H; destruct H as [?|[??]] + | [ H : 0 <= ?x, H' : ?x - 1 < 0 |- _ ] + => assert (x = 0) by lia; clear H H' + | [ |- ?x <= ?y ] => is_evar x; reflexivity + | [ |- ?x <= ?y ] => is_evar y; reflexivity + end. + Ltac split_comparison_fin := repeat split_comparison_fin_step. + Ltac simplify_fractions_step := + match goal with + | _ => rewrite Z.div_mul by (try apply Z.pow_nonzero; zero_bounds) + | [ |- context[?x * ?y / ?x] ] + => rewrite (Z.mul_comm x y) + | [ |- ?x <= ?x ] => reflexivity + end. + Ltac simplify_fractions := repeat simplify_fractions_step. + Ltac simplify_fractions_le := + pre_reorder_fractions; + [ repeat split_comparison; split_comparison_fin; zero_bounds.. + | simplify_fractions ]. + + Lemma log2_nonneg' n a : n <= 0 -> n <= Z.log2 a. + Proof. + intros; transitivity 0; auto with zarith. + Qed. -Hint Resolve log2_nonneg' : zarith. + Hint Resolve log2_nonneg' : zarith. -(** We create separate databases for two directions of transformations - involving [Z.log2]; combining them leads to loops. *) -(* for hints that take in hypotheses of type [log2 _], and spit out conclusions of type [_ ^ _] *) -Create HintDb hyp_log2. + (** We create separate databases for two directions of transformations + involving [Z.log2]; combining them leads to loops. *) + (* for hints that take in hypotheses of type [log2 _], and spit out conclusions of type [_ ^ _] *) + Create HintDb hyp_log2. -(* for hints that take in hypotheses of type [_ ^ _], and spit out conclusions of type [log2 _] *) -Create HintDb concl_log2. + (* for hints that take in hypotheses of type [_ ^ _], and spit out conclusions of type [log2 _] *) + Create HintDb concl_log2. -Hint Resolve (fun a b H => proj1 (Z.log2_lt_pow2 a b H)) (fun a b H => proj1 (Z.log2_le_pow2 a b H)) : concl_log2. -Hint Resolve (fun a b H => proj2 (Z.log2_lt_pow2 a b H)) (fun a b H => proj2 (Z.log2_le_pow2 a b H)) : hyp_log2. + Hint Resolve (fun a b H => proj1 (Z.log2_lt_pow2 a b H)) (fun a b H => proj1 (Z.log2_le_pow2 a b H)) : concl_log2. + Hint Resolve (fun a b H => proj2 (Z.log2_lt_pow2 a b H)) (fun a b H => proj2 (Z.log2_le_pow2 a b H)) : hyp_log2. -Lemma le_lt_to_log2 x y z : 0 <= z -> 0 < y -> 2^x <= y < 2^z -> x <= Z.log2 y < z. -Proof. - destruct (Z_le_gt_dec 0 x); auto with concl_log2 lia. -Qed. + Lemma le_lt_to_log2 x y z : 0 <= z -> 0 < y -> 2^x <= y < 2^z -> x <= Z.log2 y < z. + Proof. + destruct (Z_le_gt_dec 0 x); auto with concl_log2 lia. + Qed. -Lemma div_x_y_x x y : 0 < x -> 0 < y -> x / y / x = 1 / y. -Proof. - intros; rewrite Z.div_div, (Z.mul_comm y x), <- Z.div_div, Z.div_same by lia. - reflexivity. -Qed. + Lemma div_x_y_x x y : 0 < x -> 0 < y -> x / y / x = 1 / y. + Proof. + intros; rewrite Z.div_div, (Z.mul_comm y x), <- Z.div_div, Z.div_same by lia. + reflexivity. + Qed. -Hint Rewrite div_x_y_x using lia : zsimplify. + Hint Rewrite div_x_y_x using lia : zsimplify. -Lemma mod_opp_l_z_iff a b (H : b <> 0) : a mod b = 0 <-> (-a) mod b = 0. -Proof. - split; intro H'; apply Z.mod_opp_l_z in H'; rewrite ?Z.opp_involutive in H'; assumption. -Qed. + Lemma mod_opp_l_z_iff a b (H : b <> 0) : a mod b = 0 <-> (-a) mod b = 0. + Proof. + split; intro H'; apply Z.mod_opp_l_z in H'; rewrite ?Z.opp_involutive in H'; assumption. + Qed. -Lemma opp_eq_0_iff a : -a = 0 <-> a = 0. -Proof. lia. Qed. + Lemma opp_eq_0_iff a : -a = 0 <-> a = 0. + Proof. lia. Qed. -Hint Rewrite <- mod_opp_l_z_iff using lia : zsimplify. -Hint Rewrite opp_eq_0_iff : zsimplify. + Hint Rewrite <- mod_opp_l_z_iff using lia : zsimplify. + Hint Rewrite opp_eq_0_iff : zsimplify. -Lemma sub_pos_bound a b X : 0 <= a < X -> 0 <= b < X -> -X < a - b < X. -Proof. lia. Qed. + Lemma sub_pos_bound a b X : 0 <= a < X -> 0 <= b < X -> -X < a - b < X. + Proof. lia. Qed. -Lemma div_opp_l_complete a b (Hb : b <> 0) : -a/b = -(a/b) - (if Z_zerop (a mod b) then 0 else 1). -Proof. - destruct (Z_zerop (a mod b)); autorewrite with zsimplify push_Zopp; reflexivity. -Qed. + Lemma div_opp_l_complete a b (Hb : b <> 0) : -a/b = -(a/b) - (if Z_zerop (a mod b) then 0 else 1). + Proof. + destruct (Z_zerop (a mod b)); autorewrite with zsimplify push_Zopp; reflexivity. + Qed. -Lemma div_opp_l_complete' a b (Hb : b <> 0) : -(a/b) = -a/b + (if Z_zerop (a mod b) then 0 else 1). -Proof. - destruct (Z_zerop (a mod b)); autorewrite with zsimplify pull_Zopp; lia. -Qed. + Lemma div_opp_l_complete' a b (Hb : b <> 0) : -(a/b) = -a/b + (if Z_zerop (a mod b) then 0 else 1). + Proof. + destruct (Z_zerop (a mod b)); autorewrite with zsimplify pull_Zopp; lia. + Qed. -Hint Rewrite Z.div_opp_l_complete using lia : pull_Zopp. -Hint Rewrite Z.div_opp_l_complete' using lia : push_Zopp. + Hint Rewrite Z.div_opp_l_complete using lia : pull_Zopp. + Hint Rewrite Z.div_opp_l_complete' using lia : push_Zopp. -Lemma div_opp a : a <> 0 -> -a / a = -1. -Proof. - intros; autorewrite with pull_Zopp zsimplify; lia. -Qed. + Lemma div_opp a : a <> 0 -> -a / a = -1. + Proof. + intros; autorewrite with pull_Zopp zsimplify; lia. + Qed. -Hint Rewrite Z.div_opp using lia : zsimplify. + Hint Rewrite Z.div_opp using lia : zsimplify. -Lemma div_sub_1_0 x : x > 0 -> (x - 1) / x = 0. -Proof. auto with zarith lia. Qed. + Lemma div_sub_1_0 x : x > 0 -> (x - 1) / x = 0. + Proof. auto with zarith lia. Qed. -Hint Rewrite div_sub_1_0 using lia : zsimplify. + Hint Rewrite div_sub_1_0 using lia : zsimplify. -Lemma sub_pos_bound_div a b X : 0 <= a < X -> 0 <= b < X -> -1 <= (a - b) / X <= 0. -Proof. - intros H0 H1; pose proof (Z.sub_pos_bound a b X H0 H1). - assert (Hn : -X <= a - b) by lia. - assert (Hp : a - b <= X - 1) by lia. - split; etransitivity; [ | apply Z_div_le, Hn; lia | apply Z_div_le, Hp; lia | ]; - instantiate; autorewrite with zsimplify; try reflexivity. -Qed. + Lemma sub_pos_bound_div a b X : 0 <= a < X -> 0 <= b < X -> -1 <= (a - b) / X <= 0. + Proof. + intros H0 H1; pose proof (Z.sub_pos_bound a b X H0 H1). + assert (Hn : -X <= a - b) by lia. + assert (Hp : a - b <= X - 1) by lia. + split; etransitivity; [ | apply Z_div_le, Hn; lia | apply Z_div_le, Hp; lia | ]; + instantiate; autorewrite with zsimplify; try reflexivity. + Qed. -Hint Resolve (fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1)) - (fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1)) : zarith. + Hint Resolve (fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1)) + (fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1)) : zarith. -Lemma sub_pos_bound_div_eq a b X : 0 <= a < X -> 0 <= b < X -> (a - b) / X = if a 0); [ lia | ]. - autorewrite with zstrip_div; auto with zarith lia. } - { autorewrite with zstrip_div; auto with zarith lia. } -Qed. + Lemma sub_pos_bound_div_eq a b X : 0 <= a < X -> 0 <= b < X -> (a - b) / X = if a 0); [ lia | ]. + autorewrite with zstrip_div; auto with zarith lia. } + { autorewrite with zstrip_div; auto with zarith lia. } + Qed. -Lemma add_opp_pos_bound_div_eq a b X : 0 <= a < X -> 0 <= b < X -> (-b + a) / X = if a 0 <= b < X -> (-b + a) / X = if a 0 = a / b. -Proof. intros; symmetry; apply Z.div_small; assumption. Qed. + Lemma div_small_sym a b : 0 <= a < b -> 0 = a / b. + Proof. intros; symmetry; apply Z.div_small; assumption. Qed. -Lemma mod_small_sym a b : 0 <= a < b -> a = a mod b. -Proof. intros; symmetry; apply Z.mod_small; assumption. Qed. + Lemma mod_small_sym a b : 0 <= a < b -> a = a mod b. + Proof. intros; symmetry; apply Z.mod_small; assumption. Qed. -Hint Resolve div_small_sym mod_small_sym : zarith. + Hint Resolve div_small_sym mod_small_sym : zarith. -Lemma div_add' a b c : c <> 0 -> (a + c * b) / c = a / c + b. -Proof. intro; rewrite <- Z.div_add, (Z.mul_comm c); try lia. Qed. + Lemma div_add' a b c : c <> 0 -> (a + c * b) / c = a / c + b. + Proof. intro; rewrite <- Z.div_add, (Z.mul_comm c); try lia. Qed. -Lemma div_add_l' a b c : b <> 0 -> (b * a + c) / b = a + c / b. -Proof. intro; rewrite <- Z.div_add_l, (Z.mul_comm b); lia. Qed. + Lemma div_add_l' a b c : b <> 0 -> (b * a + c) / b = a + c / b. + Proof. intro; rewrite <- Z.div_add_l, (Z.mul_comm b); lia. Qed. -Hint Rewrite div_add_l' div_add' using lia : zsimplify. + Hint Rewrite div_add_l' div_add' using lia : zsimplify. -Lemma div_add_sub_l a b c d : b <> 0 -> (a * b + c - d) / b = a + (c - d) / b. -Proof. rewrite <- Z.add_sub_assoc; apply Z.div_add_l. Qed. + Lemma div_add_sub_l a b c d : b <> 0 -> (a * b + c - d) / b = a + (c - d) / b. + Proof. rewrite <- Z.add_sub_assoc; apply Z.div_add_l. Qed. -Lemma div_add_sub_l' a b c d : b <> 0 -> (b * a + c - d) / b = a + (c - d) / b. -Proof. rewrite <- Z.add_sub_assoc; apply Z.div_add_l'. Qed. + Lemma div_add_sub_l' a b c d : b <> 0 -> (b * a + c - d) / b = a + (c - d) / b. + Proof. rewrite <- Z.add_sub_assoc; apply Z.div_add_l'. Qed. -Lemma div_add_sub a b c d : c <> 0 -> (a + b * c - d) / c = (a - d) / c + b. -Proof. rewrite (Z.add_comm _ (_ * _)), (Z.add_comm (_ / _)); apply Z.div_add_sub_l. Qed. + Lemma div_add_sub a b c d : c <> 0 -> (a + b * c - d) / c = (a - d) / c + b. + Proof. rewrite (Z.add_comm _ (_ * _)), (Z.add_comm (_ / _)); apply Z.div_add_sub_l. Qed. -Lemma div_add_sub' a b c d : c <> 0 -> (a + c * b - d) / c = (a - d) / c + b. -Proof. rewrite (Z.add_comm _ (_ * _)), (Z.add_comm (_ / _)); apply Z.div_add_sub_l'. Qed. + Lemma div_add_sub' a b c d : c <> 0 -> (a + c * b - d) / c = (a - d) / c + b. + Proof. rewrite (Z.add_comm _ (_ * _)), (Z.add_comm (_ / _)); apply Z.div_add_sub_l'. Qed. -Hint Rewrite Z.div_add_sub Z.div_add_sub' Z.div_add_sub_l Z.div_add_sub_l' using lia : zsimplify. + Hint Rewrite Z.div_add_sub Z.div_add_sub' Z.div_add_sub_l Z.div_add_sub_l' using lia : zsimplify. -Lemma div_mul_skip a b k : 0 < b -> 0 < k -> a * b / k / b = a / k. -Proof. - intros; rewrite Z.div_div, (Z.mul_comm k), <- Z.div_div by lia. - autorewrite with zsimplify; reflexivity. -Qed. + Lemma div_mul_skip a b k : 0 < b -> 0 < k -> a * b / k / b = a / k. + Proof. + intros; rewrite Z.div_div, (Z.mul_comm k), <- Z.div_div by lia. + autorewrite with zsimplify; reflexivity. + Qed. -Lemma div_mul_skip' a b k : 0 < b -> 0 < k -> b * a / k / b = a / k. -Proof. - intros; rewrite Z.div_div, (Z.mul_comm k), <- Z.div_div by lia. - autorewrite with zsimplify; reflexivity. -Qed. + Lemma div_mul_skip' a b k : 0 < b -> 0 < k -> b * a / k / b = a / k. + Proof. + intros; rewrite Z.div_div, (Z.mul_comm k), <- Z.div_div by lia. + autorewrite with zsimplify; reflexivity. + Qed. -Hint Rewrite Z.div_mul_skip Z.div_mul_skip' using lia : zsimplify. + Hint Rewrite Z.div_mul_skip Z.div_mul_skip' using lia : zsimplify. End Z. Module Export BoundsTactics. -- cgit v1.2.3 From 7854ab5071ae4ddb6d125187865f3340dfe9f184 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 3 Jul 2016 00:16:31 -0700 Subject: Implement and prove Barrett reduction on Z (#18) Implement and prove Barrett reduction on Z This will serve as the high-level algorithm for modular reduction. We follow Wikipedia very closely, except where we can do better (I believe @jadephilipoom is updating Wikipedia). --- _CoqProject | 1 + src/ModularArithmetic/BarrettReduction/Z.v | 118 +++++++++++++++++++++++++++++ 2 files changed, 119 insertions(+) create mode 100644 src/ModularArithmetic/BarrettReduction/Z.v diff --git a/_CoqProject b/_CoqProject index 904d716b8..beac11f07 100644 --- a/_CoqProject +++ b/_CoqProject @@ -43,6 +43,7 @@ src/ModularArithmetic/PseudoMersenneBaseParamProofs.v src/ModularArithmetic/PseudoMersenneBaseParams.v src/ModularArithmetic/PseudoMersenneBaseRep.v src/ModularArithmetic/Tutorial.v +src/ModularArithmetic/BarrettReduction/Z.v src/Spec/CompleteEdwardsCurve.v src/Spec/EdDSA.v src/Spec/Encoding.v diff --git a/src/ModularArithmetic/BarrettReduction/Z.v b/src/ModularArithmetic/BarrettReduction/Z.v new file mode 100644 index 000000000..8b472d5d8 --- /dev/null +++ b/src/ModularArithmetic/BarrettReduction/Z.v @@ -0,0 +1,118 @@ +(*** Barrett Reduction *) +(** This file implements Barrett Reduction on [Z]. We follow Wikipedia. *) +Require Import Coq.ZArith.ZArith Coq.micromega.Psatz. +Require Import Crypto.Util.ZUtil Crypto.Util.Tactics. + +Local Open Scope Z_scope. + +Section barrett. + Context (n a : Z) + (n_reasonable : n <> 0). + (** Quoting Wikipedia : *) + (** In modular arithmetic, Barrett reduction is a reduction + algorithm introduced in 1986 by P.D. Barrett. A naive way of + computing *) + (** [c = a mod n] *) + (** would be to use a fast division algorithm. Barrett reduction is + an algorithm designed to optimize this operation assuming [n] is + constant, and [a < n²], replacing divisions by + multiplications. *) + + (** * General idea *) + Section general_idea. + (** Let [m = 1 / n] be the inverse of [n] as a floating point + number. Then *) + (** [a mod n = a - ⌊a m⌋ n] *) + (** where [⌊ x ⌋] denotes the floor function. The result is exact, + as long as [m] is computed with sufficient accuracy. *) + + (* [/] is [Z.div], which means truncated division *) + Local Notation "⌊am⌋" := (a / n) (only parsing). + + Theorem naive_barrett_reduction_correct + : a mod n = a - ⌊am⌋ * n. + Proof. + apply Zmod_eq_full; assumption. + Qed. + End general_idea. + + (** * Barrett algorithm *) + Section barrett_algorithm. + (** Barrett algorithm is a fixed-point analog which expresses + everything in terms of integers. Let [k] be the smallest + integer such that [2ᵏ > n]. Think of [n] as representing the + fixed-point number [n 2⁻ᵏ]. We precompute [m] such that [m = + ⌊4ᵏ / n⌋]. Then [m] represents the fixed-point number + [m 2⁻ᵏ ≈ (n 2⁻ᵏ)⁻¹]. *) + (** N.B. We don't need [k] to be the smallest such integer. *) + Context (k : Z) + (k_good : n < 2 ^ k) + (m : Z) + (m_good : m = 4^k / n). (* [/] is [Z.div], which is truncated *) + (** Wikipedia neglects to mention non-negativity, but we need it. + It might be possible to do with a relaxed assumption, such as + the sign of [a] and the sign of [n] being the same; but I + figured it wasn't worth it. *) + Context (n_pos : 0 < n) (* or just [0 <= n], since we have [n <> 0] above *) + (a_nonneg : 0 <= a). + + Lemma k_nonnegative : 0 <= k. + Proof. + destruct (Z_lt_le_dec k 0); try assumption. + rewrite !Z.pow_neg_r in * by lia; lia. + Qed. + + (** Now *) + Let q := (m * a) / 4^k. + Let r := a - q * n. + (** Because of the floor function (in Coq, because [/] means + truncated division), [q] is an integer and [r ≡ a mod n]. *) + Theorem barrett_reduction_equivalent + : r mod n = a mod n. + Proof. + subst r q m. + rewrite <- !Z.add_opp_r, !Zopp_mult_distr_l, !Z_mod_plus_full by assumption. + reflexivity. + Qed. + + Lemma qn_small + : q * n <= a. + Proof. + pose proof k_nonnegative; subst q r m. + assert (0 <= 2^(k-1)) by zero_bounds. + Z.simplify_fractions_le. + Qed. + + (** Also, if [a < n²] then [r < 2n]. *) + (** N.B. It turns out that it is sufficient to assume [a < 4ᵏ]. *) + Context (a_small : a < 4^k). + Lemma r_small : r < 2 * n. + Proof. + Hint Rewrite (Z.div_small a (4^k)) (Z.mod_small a (4^k)) using lia : zsimplify. + Hint Rewrite (Z.mul_div_eq' a n) using lia : zstrip_div. + cut (r + 1 <= 2 * n); [ lia | ]. + pose proof k_nonnegative; subst r q m. + assert (0 <= 2^(k-1)) by zero_bounds. + assert (4^k <> 0) by auto with zarith lia. + assert (a mod n < n) by auto with zarith lia. + pose proof (Z.mod_pos_bound (a * 4^k / n) (4^k)). + transitivity (a - (a * 4 ^ k / n - a) / 4 ^ k * n + 1). + { rewrite <- (Z.mul_comm a); auto 6 with zarith lia. } + rewrite (Z_div_mod_eq (_ * 4^k / n) (4^k)) by lia. + autorewrite with push_Zmul push_Zopp zsimplify zstrip_div. + break_match; auto with lia. + Qed. + + (** In that case, we have *) + Theorem barrett_reduction_small + : a mod n = if r Date: Sun, 3 Jul 2016 00:22:13 -0700 Subject: Define the spec of Weierstrass curves (#6) Define the spec of Weierstrass curves This is the start of work on P256. --- _CoqProject | 2 ++ src/Spec/WeierstrassCurve.v | 84 +++++++++++++++++++++++++++++++++++++++++++++ src/WeierstrassCurve/Pre.v | 57 ++++++++++++++++++++++++++++++ 3 files changed, 143 insertions(+) create mode 100644 src/Spec/WeierstrassCurve.v create mode 100644 src/WeierstrassCurve/Pre.v diff --git a/_CoqProject b/_CoqProject index beac11f07..22af15eb5 100644 --- a/_CoqProject +++ b/_CoqProject @@ -49,6 +49,7 @@ src/Spec/EdDSA.v src/Spec/Encoding.v src/Spec/ModularArithmetic.v src/Spec/ModularWordEncoding.v +src/Spec/WeierstrassCurve.v src/Specific/GF1305.v src/Specific/GF25519.v src/Tactics/Nsatz.v @@ -67,3 +68,4 @@ src/Util/Tuple.v src/Util/Unit.v src/Util/WordUtil.v src/Util/ZUtil.v +src/WeierstrassCurve/Pre.v diff --git a/src/Spec/WeierstrassCurve.v b/src/Spec/WeierstrassCurve.v new file mode 100644 index 000000000..7ec5d99ec --- /dev/null +++ b/src/Spec/WeierstrassCurve.v @@ -0,0 +1,84 @@ +Require Crypto.WeierstrassCurve.Pre. + +Module E. + Section WeierstrassCurves. + (* Short Weierstrass curves with addition laws. References: + * + * + * See also: + * (page 79) + *) + + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} `{Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}. + Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + Local Infix "=?" := Algebra.eq_dec (at level 70, no associativity) : type_scope. + Local Notation "x =? y" := (Sumbool.bool_of_sumbool (Algebra.eq_dec x y)) : bool_scope. + Local Infix "+" := Fadd. Local Infix "*" := Fmul. + Local Infix "-" := Fsub. Local Infix "/" := Fdiv. + Local Notation "- x" := (Fopp x). + Local Notation "x ^ 2" := (x*x) (at level 30). Local Notation "x ^ 3" := (x*x^2) (at level 30). + Local Notation "'∞'" := unit : type_scope. + Local Notation "'∞'" := (inr tt) : core_scope. + Local Notation "0" := Fzero. Local Notation "1" := Fone. + Local Notation "2" := (1+1). Local Notation "3" := (1+2). Local Notation "4" := (1+3). + Local Notation "8" := (1+(1+(1+(1+4)))). Local Notation "12" := (1+(1+(1+(1+8)))). + Local Notation "16" := (1+(1+(1+(1+12)))). Local Notation "20" := (1+(1+(1+(1+16)))). + Local Notation "24" := (1+(1+(1+(1+20)))). Local Notation "27" := (1+(1+(1+24))). + + Local Notation "( x , y )" := (inl (pair x y)). + Local Open Scope core_scope. + + Context {a b: F}. + + (** N.B. We may require more conditions to prove that points form + a group under addition (associativity, in particular. If + that's the case, more fields will be added to this class. *) + Class weierstrass_params := + { + char_gt_2 : 2 <> 0; + char_ne_3 : 3 <> 0; + nonzero_discriminant : -(16) * (4 * a^3 + 27 * b^2) <> 0 + }. + Context `{weierstrass_params}. + + Definition point := { P | match P with + | (x, y) => y^2 = x^3 + a*x + b + | ∞ => True + end }. + Definition coordinates (P:point) : (F*F + ∞) := proj1_sig P. + + (** The following points are indeed on the curve -- see [WeierstrassCurve.Pre] for proof *) + Local Obligation Tactic := + try solve [ Program.Tactics.program_simpl + | intros; apply (Pre.unifiedAdd'_onCurve _ _ (proj2_sig _) (proj2_sig _)) ]. + + Program Definition zero : point := ∞. + + Program Definition add (P1 P2:point) : point + := exist + _ + (match coordinates P1, coordinates P2 return _ with + | (x1, y1), (x2, y2) => + if x1 =? x2 then + if y2 =? -y1 then ∞ + else ((3*x1^2+a)^2 / (2*y1)^2 - x1 - x1, + (2*x1+x1)*(3*x1^2+a) / (2*y1) - (3*x1^2+a)^3/(2*y1)^3-y1) + else ((y2-y1)^2 / (x2-x1)^2 - x1 - x2, + (2*x1+x2)*(y2-y1) / (x2-x1) - (y2-y1)^3 / (x2-x1)^3 - y1) + | ∞, ∞ => ∞ + | ∞, _ => coordinates P2 + | _, ∞ => coordinates P1 + end) + _. + + Fixpoint mul (n:nat) (P : point) : point := + match n with + | O => zero + | S n' => add P (mul n' P) + end. + End WeierstrassCurves. +End E. + +Delimit Scope E_scope with E. +Infix "+" := E.add : E_scope. +Infix "*" := E.mul : E_scope. diff --git a/src/WeierstrassCurve/Pre.v b/src/WeierstrassCurve/Pre.v new file mode 100644 index 000000000..060d2f479 --- /dev/null +++ b/src/WeierstrassCurve/Pre.v @@ -0,0 +1,57 @@ +Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. +Require Import Crypto.Algebra Crypto.Tactics.Nsatz. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.Notations. + +Local Open Scope core_scope. + +Generalizable All Variables. +Section Pre. + Context {F eq zero one opp add sub mul inv div} `{field F eq zero one opp add sub mul inv div}. + Local Infix "=" := eq. Local Notation "a <> b" := (not (a = b)). + Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + Local Notation "0" := zero. Local Notation "1" := one. + Local Infix "+" := add. Local Infix "*" := mul. + Local Infix "-" := sub. Local Infix "/" := div. + Local Notation "- x" := (opp x). + Local Notation "x ^ 2" := (x*x). Local Notation "x ^ 3" := (x*x^2). + Local Notation "'∞'" := unit : type_scope. + Local Notation "'∞'" := (inr tt) : core_scope. + Local Notation "2" := (1+1). Local Notation "3" := (1+2). + Local Notation "( x , y )" := (inl (pair x y)). + + Add Field WeierstrassCurveField : (Field.field_theory_for_stdlib_tactic (T:=F)). + Add Ring WeierstrassCurveRing : (Ring.ring_theory_for_stdlib_tactic (T:=F)). + + Context {a:F}. + Context {b:F}. + + (* the canonical definitions are in Spec *) + Definition onCurve (P:F*F + ∞) := match P with + | (x, y) => y^2 = x^3 + a*x + b + | ∞ => True + end. + Definition unifiedAdd' (P1' P2':F*F + ∞) : F*F + ∞ := + match P1', P2' with + | (x1, y1), (x2, y2) + => if x1 =? x2 then + if y2 =? -y1 then + ∞ + else ((3*x1^2+a)^2 / (2*y1)^2 - x1 - x1, + (2*x1+x1)*(3*x1^2+a) / (2*y1) - (3*x1^2+a)^3/(2*y1)^3-y1) + else + ((y2-y1)^2 / (x2-x1)^2 - x1 - x2, + (2*x1+x2)*(y2-y1) / (x2-x1) - (y2-y1)^3 / (x2-x1)^3 - y1) + | ∞, ∞ => ∞ + | ∞, _ => P2' + | _, ∞ => P1' + end. + + Lemma unifiedAdd'_onCurve : forall P1 P2, + onCurve P1 -> onCurve P2 -> onCurve (unifiedAdd' P1 P2). + Proof. + unfold onCurve, unifiedAdd'; intros [[x1 y1]|] [[x2 y2]|] H1 H2; + break_match; trivial; setoid_subst_rel eq; only_two_square_roots; + field_algebra; nsatz_contradict. + Qed. +End Pre. -- cgit v1.2.3