Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462//! This file contains proofs related to integer multiplication (`*`).//! These are part of the math standard library.//!//! It's based on the following file from the Dafny math standard//! library://! `Source/DafnyStandardLibraries/src/Std/Arithmetic/Mul.dfy`.//! That file has the following copyright notice://! /*******************************************************************************//! * Original: Copyright (c) Microsoft Corporation *//! SPDX-License-Identifier: MIT * * Modifications and Extensions://! Copyright by the contributors to the Dafny Project *//! SPDX-License-Identifier: MIT//! *******************************************************************************/#[allow(unused_imports)]use super::super::prelude::*;
verus! {
use super::super::arithmetic::internals::mul_internals_nonlinear as MulINL;use super::super::arithmetic::internals::mul_internals::*;
/// Proof that multiplication using `*` is equivalent to/// multiplication using a recursive definition. Specifically,/// `x * y` is equivalent in that way.pub broadcast proof fn lemma_mul_is_mul_recursive(x: int, y: int) ensures #[trigger] (x * y) == mul_recursive(x, y),{ if (x >= 0) { lemma_mul_is_mul_pos(x, y); assert(x * y == mul_pos(x, y)); assert((x * y) == mul_recursive(x, y)); } else { lemma_mul_is_mul_pos(-x, y); assert(x * y == -1 * (-x * y)) by { lemma_mul_is_associative(-1, -x, y) }; // OBSERVE assert((x * y) == mul_recursive(x, y)); }}
/// Proof that multiplying two positive integers with `*` results in/// the same product as would be achieved by recursive addition./// Specifically, `x * y == mul_pos(x, y)`.pub proof fn lemma_mul_is_mul_pos(x: int, y: int) requires x >= 0, ensures x * y == mul_pos(x, y),{ reveal(mul_pos); lemma_mul_induction_auto(x, |u: int| u >= 0 ==> u * y == mul_pos(u, y));}
pub proof fn lemma_mul_basics(x: int) ensures 0 * x == 0, x * 0 == 0, x * 1 == x, 1 * x == x,{}
/// Proof of basic properties of multiplication by `x`, specifically/// what happens when multiplying by 0 or 1.pub broadcast proof fn lemma_mul_basics_1(x: int) ensures #[trigger] (0 * x) == 0,{}
/// Proof of basic properties of multiplication by `x`, specifically/// what happens when multiplying by 0 or 1.pub broadcast proof fn lemma_mul_basics_2(x: int) ensures #[trigger] (x * 0) == 0,{}
/// Proof of basic properties of multiplication by `x`, specifically/// what happens when multiplying by 0 or 1.pub broadcast proof fn lemma_mul_basics_3(x: int) ensures #[trigger] (x * 1) == x,{}
/// Proof of basic properties of multiplication by `x`, specifically/// what happens when multiplying by 0 or 1.pub broadcast proof fn lemma_mul_basics_4(x: int) ensures #[trigger] (1 * x) == x,{}
pub broadcast group group_mul_basics { lemma_mul_basics_1, lemma_mul_basics_2, lemma_mul_basics_3, lemma_mul_basics_4,}
/// Proof that `x * y` is nonzero if and only if both `x` and `y` are nonzero.pub broadcast proof fn lemma_mul_nonzero(x: int, y: int) ensures #[trigger] (x * y) != 0 <==> x != 0 && y != 0,{ MulINL::lemma_mul_nonzero(x, y);}
/// Proof that any integer multiplied by 0 results in a product of 0.pub broadcast proof fn lemma_mul_by_zero_is_zero(x: int) ensures #![trigger x * 0] #![trigger 0 * x] x * 0 == 0 && 0 * x == 0,{ assert forall|x: int| #![trigger x * 0] #![trigger 0 * x] x * 0 == 0 && 0 * x == 0 by { lemma_mul_basics(x); }}
/// Proof that multiplication is associative, specifically that/// `x * (y * z) == (x * y) * z`.pub broadcast proof fn lemma_mul_is_associative(x: int, y: int, z: int) ensures #![trigger x * (y * z)] #![trigger (x * y) * z] x * (y * z) == (x * y) * z,{ MulINL::lemma_mul_is_associative(x, y, z);}
/// Proof that multiplication is commutative, specifically that/// `x * y == y * x`.pub broadcast proof fn lemma_mul_is_commutative(x: int, y: int) ensures #[trigger] (x * y) == y * x,{}
/// Proof that, since the product of the two integers `x` and `y` is/// nonnegative, that product is greater than or equal to each of `x`/// and `y`pub broadcast proof fn lemma_mul_ordering(x: int, y: int) requires x != 0, y != 0, 0 <= x * y, ensures #[trigger] (x * y) >= x && x * y >= y,{ MulINL::lemma_mul_ordering(x, y);}
/* We don't port LemmaMulEquality or LemmaMulEqualityAuto from the Dafny standard library for arithmetic, since they're never useful. They say that `x == y ==> x * z == y * z`, which is trivial. It follows immediately from the basic SMT axiom that functions and operators (including multiplication) have equal values when applied to equal arguments.*/
/// Proof that, since `x <= y` and `z >= 0`, `x * z <= y * z`.pub broadcast proof fn lemma_mul_inequality(x: int, y: int, z: int) requires x <= y, z >= 0, ensures #[trigger] (x * z) <= #[trigger] (y * z),{ lemma_mul_induction_auto(z, |u: int| u >= 0 ==> x * u <= y * u);}
/// Proof that since `x < y` and `z > 0`, `x * z < y * z`.pub broadcast proof fn lemma_mul_strict_inequality(x: int, y: int, z: int) requires x < y, z > 0, ensures #[trigger] (x * z) < #[trigger] (y * z),{ MulINL::lemma_mul_strict_inequality(x, y, z);}
/// Proof that since `x` is bounded above by `xbound` and `y` is/// bounded above by `ybound`, the product of `x` and `y` is bounded/// above by the product of the bounds.pub broadcast proof fn lemma_mul_upper_bound(x: int, xbound: int, y: int, ybound: int) requires x <= xbound, y <= ybound, 0 <= x, 0 <= y, ensures #[trigger] (x * y) <= #[trigger] (xbound * ybound),{ lemma_mul_inequality(x, xbound, y); lemma_mul_inequality(y, ybound, xbound);}
/// Proof that when `x` has an exclusive upper bound `xbound` and `y`/// has an exclusive upper bound `ybound`, that the product of `x` and/// `y` is bounded above by the product of the predecessors of their/// upper bounds. In other words, `x * y <= (xbound - 1) * (ybound - 1)`.pub broadcast proof fn lemma_mul_strict_upper_bound(x: int, xbound: int, y: int, ybound: int) requires x < xbound, y < ybound, 0 < x, 0 < y, ensures #[trigger] (x * y) <= #[trigger] ((xbound - 1) * (ybound - 1)),{ lemma_mul_inequality(x, xbound - 1, y); lemma_mul_inequality(y, ybound - 1, xbound - 1);}
/// Proof that multiplying the positive integer `x` by respectively/// `y` and `z` maintains the order of `y` and `z`. Specifically, `y/// <= z ==> x * y <= x * z` and `y < z ==> x * y < x * z`.pub broadcast proof fn lemma_mul_left_inequality(x: int, y: int, z: int) requires 0 < x, ensures y <= z ==> #[trigger] (x * y) <= #[trigger] (x * z), y < z ==> x * y < x * z,{ lemma_mul_induction_auto(x, |u: int| u > 0 ==> y <= z ==> u * y <= u * z); lemma_mul_induction_auto(x, |u: int| u > 0 ==> y < z ==> u * y < u * z);}
/// Proof that if `x` and `y` have equal results when multiplied by/// nonzero `m`, then they're equal.pub broadcast proof fn lemma_mul_equality_converse(m: int, x: int, y: int) requires m != 0, #[trigger] (m * x) == #[trigger] (m * y), ensures x == y,{ lemma_mul_induction_auto(m, |u| x > y && 0 < u ==> x * u > y * u); lemma_mul_induction_auto(m, |u: int| x < y && 0 < u ==> x * u < y * u); lemma_mul_induction_auto(m, |u: int| x > y && 0 > u ==> x * u < y * u); lemma_mul_induction_auto(m, |u: int| x < y && 0 > u ==> x * u > y * u);}
/// Proof that since `x * z <= y * z` and `z > 0`, that `x <= y`.pub broadcast proof fn lemma_mul_inequality_converse(x: int, y: int, z: int) requires #[trigger] (x * z) <= #[trigger] (y * z), z > 0, ensures x <= y,{ lemma_mul_induction_auto(z, |u: int| x * u <= y * u && u > 0 ==> x <= y);}
/// Proof that since `x * z < y * z` and `z >= 0`, we know `x < y`.pub broadcast proof fn lemma_mul_strict_inequality_converse(x: int, y: int, z: int) requires #[trigger] (x * z) < #[trigger] (y * z), z >= 0, ensures x < y,{ lemma_mul_induction_auto(z, |u: int| x * u < y * u && u >= 0 ==> x < y);}
/// Proof that multiplication distributes over addition, specifically that/// `x * (y + z) == x * y + x * z`.pub broadcast proof fn lemma_mul_is_distributive_add(x: int, y: int, z: int) ensures #[trigger] (x * (y + z)) == x * y + x * z,{ MulINL::lemma_mul_is_distributive_add(x, y, z);}
/// Proof that multiplication distributes over addition, specifically that/// `(y + z) * x == y * x + z * x`.pub broadcast proof fn lemma_mul_is_distributive_add_other_way(x: int, y: int, z: int) ensures #[trigger] ((y + z) * x) == y * x + z * x,{ broadcast use group_mul_properties_internal;
}
/// Proof that multiplication distributes over subtraction, specifically that/// `x * (y - z) == x * y - x * z`.pub broadcast proof fn lemma_mul_is_distributive_sub(x: int, y: int, z: int) ensures #[trigger] (x * (y - z)) == x * y - x * z,{ broadcast use group_mul_properties_internal;
}
/// Proof that multiplication distributes over subtraction when the/// subtraction happens in the multiplicand (i.e., in the left-hand/// argument to `*`). Specifically, `(y - z) * x == y * x - z * x`.pub broadcast proof fn lemma_mul_is_distributive_sub_other_way(x: int, y: int, z: int) ensures #[trigger] ((y - z) * x) == y * x - z * x,{ lemma_mul_is_distributive_sub(x, y, z); lemma_mul_is_commutative(x, y - z); lemma_mul_is_commutative(x, y); lemma_mul_is_commutative(x, z);}
pub broadcast group group_mul_is_distributive { lemma_mul_is_distributive_add, lemma_mul_is_distributive_add_other_way, lemma_mul_is_distributive_sub, lemma_mul_is_distributive_sub_other_way,}
pub broadcast group group_mul_is_commutative_and_distributive { lemma_mul_is_commutative, group_mul_is_distributive,}
/// Proof that multiplication is commutative, distributes over/// addition, and distributes over subtraction, in the specific cases/// where one of the arguments to the multiplication is `x` and the/// other arguments are `y` and `z`.proof fn lemma_mul_is_distributive(x: int, y: int, z: int) ensures x * (y + z) == x * y + x * z, x * (y - z) == x * y - x * z, (y + z) * x == y * x + z * x, (y - z) * x == y * x - z * x, x * (y + z) == (y + z) * x, x * (y - z) == (y - z) * x, x * y == y * x, x * z == z * x,{ broadcast use group_mul_is_commutative_and_distributive;
}
/// Proof that multiplication distributes over addition and/// subtraction, whether the addition or subtraction happens in the/// first or the second argument to the multiplication.// pub broadcast proof fn lemma_mul_is_distributive_plus(x: int, y: int, z: int)// ensures// forall|x: int, y: int, z: int| #[trigger] (x * (y + z)) == x * y + x * z,// forall|x: int, y: int, z: int| #[trigger] (x * (y - z)) == x * y - x * z,// forall|x: int, y: int, z: int| #[trigger] ((y + z) * x) == y * x + z * x,// forall|x: int, y: int, z: int| #[trigger] ((y - z) * x) == y * x - z * x,// {// lemma_mul_is_distributive_add_auto();// lemma_mul_is_distributive_sub_auto();// broadcast use lemma_mul_is_commutative;// }/// Proof that if `x` and `y` are both positive, then their product is/// also positive.pub broadcast proof fn lemma_mul_strictly_positive(x: int, y: int) ensures (0 < x && 0 < y) ==> (0 < #[trigger] (x * y)),{ MulINL::lemma_mul_strictly_positive(x, y);}
/// Proof that since `x > 1` and `y > 0`, `y < x * y`.pub broadcast proof fn lemma_mul_strictly_increases(x: int, y: int) requires 1 < x, 0 < y, ensures y < #[trigger] (x * y),{ lemma_mul_induction_auto(x, |u: int| 1 < u ==> y < u * y);}
/// Proof that since `x` and `y` are both positive, their product is/// greater than or equal to `y`.pub broadcast proof fn lemma_mul_increases(x: int, y: int) requires 0 < x, 0 < y, ensures y <= #[trigger] (x * y),{ lemma_mul_induction_auto(x, |u: int| 0 < u ==> y <= u * y);}
/// Proof that since `x` and `y` are non-negative, their product is/// non-negative.pub broadcast proof fn lemma_mul_nonnegative(x: int, y: int) requires 0 <= x, 0 <= y, ensures 0 <= #[trigger] (x * y),{ lemma_mul_induction_auto(x, |u: int| 0 <= u ==> 0 <= u * y);}
/// Proof that negating `x` or `y` before multiplying them together/// produces the negation of the product of `x` and `y`.pub broadcast proof fn lemma_mul_unary_negation(x: int, y: int) ensures #![trigger (-x) * y] #![trigger x * (-y)] (-x) * y == -(x * y) == x * (-y),{ lemma_mul_induction_auto(x, |u: int| (-u) * y == -(u * y) == u * (-y));}
/// Proof that multiplying `-x` and `-y` produces the same product as/// multiplying `x` and `y`.pub broadcast proof fn lemma_mul_cancels_negatives(x: int, y: int) ensures #[trigger] (x * y) == (-x) * (-y),{ lemma_mul_induction_auto(x, |u: int| (-u) * y == -(u * y) == u * (-y));}
pub broadcast group group_mul_properties { group_mul_basics, lemma_mul_strict_inequality, lemma_mul_inequality, group_mul_is_commutative_and_distributive, lemma_mul_is_associative, lemma_mul_ordering, lemma_mul_nonzero, lemma_mul_nonnegative, lemma_mul_strictly_increases, lemma_mul_increases,}
// Check that the group_mul_properties broadcast group group_provides the same properties as the _auto lemma it replacesproof fn lemma_mul_properties_prove_mul_properties_auto() ensures forall|x: int, y: int| #[trigger] (x * y) == y * x, forall|x: int| #![trigger x * 1] #![trigger 1 * x] x * 1 == 1 * x == x, forall|x: int, y: int, z: int| x < y && z > 0 ==> #[trigger] (x * z) < #[trigger] (y * z), forall|x: int, y: int, z: int| x <= y && z >= 0 ==> #[trigger] (x * z) <= #[trigger] (y * z), forall|x: int, y: int, z: int| #[trigger] (x * (y + z)) == x * y + x * z, forall|x: int, y: int, z: int| #[trigger] (x * (y - z)) == x * y - x * z, forall|x: int, y: int, z: int| #[trigger] ((y + z) * x) == y * x + z * x, forall|x: int, y: int, z: int| #[trigger] ((y - z) * x) == y * x - z * x, forall|x: int, y: int, z: int| #![trigger x * (y * z)] #![trigger (x * y) * z] x * (y * z) == (x * y) * z, forall|x: int, y: int| #[trigger] (x * y) != 0 <==> x != 0 && y != 0, forall|x: int, y: int| 0 <= x && 0 <= y ==> 0 <= #[trigger] (x * y), forall|x: int, y: int| 0 < x && 0 < y && 0 <= x * y ==> x <= #[trigger] (x * y) && y <= (x * y), forall|x: int, y: int| (1 < x && 0 < y) ==> (y < #[trigger] (x * y)), forall|x: int, y: int| (0 < x && 0 < y) ==> (y <= #[trigger] (x * y)), forall|x: int, y: int| (0 < x && 0 < y) ==> (0 < #[trigger] (x * y)),{ broadcast use group_mul_properties;
}
} // verus!