axiom/Int

Reference for mo:core/axiom/Int in the core library.

This page lists trusted proof lemmas. Calling one adds its ensures facts after its requires clauses are proven; the lemma body itself is part of the trusted base, not a verifier-checked derivation. Use these when ordinary SMT arithmetic needs a precise algebraic step.

Import

mo:core/axiom/Int

Status

• Spec-only axiom module

Public API

Types

• Int

Lemmas

All lemmas are trusted proof hints. They return () and have no computational purpose; calling one adds its ensures fact to the current verification context after any listed preconditions have been established.

addZeroRight(a : Int) : ()

Establishes 0 as the right identity for integer addition.

Ensures: a + 0 == a

Use when: normalizing arithmetic terms that contain a trailing + 0.

addZeroLeft(a : Int) : ()

Establishes 0 as the left identity for integer addition.

Ensures: 0 + a == a

Use when: normalizing arithmetic terms that contain a leading 0 +.

addComm(a : Int, b : Int) : ()

Exposes commutativity of integer addition.

Ensures: a + b == b + a

Use when: the verifier needs two sums with swapped operands to match.

addAssoc(a : Int, b : Int, c : Int) : ()

Exposes associativity of integer addition.

Ensures: (a + b) + c == a + (b + c)

Use when: regrouping nested additions so later rewrites or cancellations apply.

addCancelRightEq(a : Int, b : Int, c : Int) : ()

Cancels a common right-hand addend from an equality.

Requires: a + c == b + c

Ensures: a == b

Use when: a proof has equality after adding the same value on the right and needs equality of the original terms.

addCancelLeftEq(a : Int, b : Int, c : Int) : ()

Cancels a common left-hand addend from an equality.

Requires: c + a == c + b

Ensures: a == b

Use when: a proof has equality after adding the same value on the left and needs equality of the original terms.

addLeMonoRight(a : Int, b : Int, c : Int) : ()

Preserves non-strict order when adding the same value on the right.

Requires: a <= b

Ensures: a + c <= b + c

Use when: lifting an existing <= fact through addition.

addLeMonoLeft(a : Int, b : Int, c : Int) : ()

Preserves non-strict order when adding the same value on the left.

Requires: a <= b

Ensures: c + a <= c + b

Use when: lifting an existing <= fact through addition with the shared term first.

addLtMonoRight(a : Int, b : Int, c : Int) : ()

Preserves strict order when adding the same value on the right.

Requires: a < b

Ensures: a + c < b + c

Use when: lifting an existing < fact through addition.

addLtMonoLeft(a : Int, b : Int, c : Int) : ()

Preserves strict order when adding the same value on the left.

Requires: a < b

Ensures: c + a < c + b

Use when: lifting an existing < fact through addition with the shared term first.

subSelf(a : Int) : ()

Establishes that subtracting a value from itself yields zero.

Ensures: a - a == 0

Use when: simplifying self-differences in arithmetic postconditions.

subZeroRight(a : Int) : ()

Establishes 0 as the right identity for integer subtraction.

Ensures: a - 0 == a

Use when: normalizing arithmetic terms that subtract zero.

subZeroLeft(a : Int) : ()

Defines subtraction from zero as negation.

Ensures: 0 - a == (-a)

Use when: rewriting 0 - a into the verifier's explicit negation form.

subDef(a : Int, b : Int) : ()

Defines subtraction as addition of the negated right operand.

Ensures: a - b == a + (-b)

Use when: converting subtraction into addition so addition lemmas can apply.

negInvolutive(a : Int) : ()

Establishes that double negation returns the original integer.

Ensures: -(-a) == a

Use when: eliminating nested negation terms.

negAdd(a : Int, b : Int) : ()

Distributes negation over addition.

Ensures: -(a + b) == (-a) + (-b)

Use when: pushing negation into a sum to match the shape of another term.

negSub(a : Int, b : Int) : ()

Rewrites the negation of a difference.

Ensures: -(a - b) == (-a) + b

Use when: simplifying a negated subtraction into an addition expression.

subAddCancel(a : Int, b : Int) : ()

Cancels a subtraction followed by adding back the same value.

Ensures: (a - b) + b == a

Use when: proving that a decrement and matching increment restore the original value.

addSubCancel(a : Int, b : Int) : ()

Cancels an addition followed by subtracting the same value.

Ensures: (a + b) - b == a

Use when: proving that an increment and matching decrement restore the original value.

subLeMonoLeft(a : Int, b : Int, c : Int) : ()

Preserves non-strict order when subtracting the same value from both sides.

Requires: a <= b

Ensures: a - c <= b - c

Use when: lifting an existing <= fact through subtraction of a shared right operand.

subLeMonoRight(a : Int, b : Int, c : Int) : ()

Reverses order when the ordered values appear as subtrahends of the same left operand.

Requires: a <= b

Ensures: c - b <= c - a

Use when: converting a <= b into the corresponding bound for c - a and c - b.

mulZeroRight(a : Int) : ()

Establishes 0 as a right absorbing element for multiplication.

Ensures: a * 0 == 0

Use when: simplifying products with a right-hand zero.

mulZeroLeft(a : Int) : ()

Establishes 0 as a left absorbing element for multiplication.

Ensures: 0 * a == 0

Use when: simplifying products with a left-hand zero.

mulOneRight(a : Int) : ()

Establishes 1 as the right identity for multiplication.

Ensures: a * 1 == a

Use when: normalizing products with a trailing * 1.

mulOneLeft(a : Int) : ()

Establishes 1 as the left identity for multiplication.

Ensures: 1 * a == a

Use when: normalizing products with a leading 1 *.

mulComm(a : Int, b : Int) : ()

Exposes commutativity of integer multiplication.

Ensures: a * b == b * a

Use when: the verifier needs two products with swapped operands to match.

mulAssoc(a : Int, b : Int, c : Int) : ()

Exposes associativity of integer multiplication.

Ensures: (a * b) * c == a * (b * c)

Use when: regrouping nested products so later rewrites or cancellations apply.

mulDistribLeft(a : Int, b : Int, c : Int) : ()

Distributes a left factor over addition.

Ensures: a * (b + c) == (a * b) + (a * c)

Use when: expanding a product over a sum with the shared factor on the left.

mulDistribRight(a : Int, b : Int, c : Int) : ()

Distributes a right factor over addition.

Ensures: (a + b) * c == (a * c) + (b * c)

Use when: expanding a product over a sum with the shared factor on the right.

negMulLeft(a : Int, b : Int) : ()

Moves a negated left factor outside the product.

Ensures: (-a) * b == -(a * b)

Use when: normalizing products that contain a negative left operand.

negMulRight(a : Int, b : Int) : ()

Moves a negated right factor outside the product.

Ensures: a * (-b) == -(a * b)

Use when: normalizing products that contain a negative right operand.

mulLeMonoRightNonNeg(a : Int, b : Int, c : Int) : ()

Preserves non-strict order when multiplying on the right by a non-negative factor.

Requires: a <= b, 0 <= c

Ensures: a * c <= b * c

Use when: scaling a <= fact by a known non-negative multiplier.

mulLeMonoLeftNonNeg(a : Int, b : Int, c : Int) : ()

Preserves non-strict order when multiplying on the left by a non-negative factor.

Requires: a <= b, 0 <= c

Ensures: c * a <= c * b

Use when: scaling a <= fact by a known non-negative multiplier written first.

mulLeAntiMonoRightNonPos(a : Int, b : Int, c : Int) : ()

Reverses non-strict order when multiplying on the right by a non-positive factor.

Requires: a <= b, c <= 0

Ensures: b * c <= a * c

Use when: scaling a <= fact by a known non-positive multiplier.

mulLeAntiMonoLeftNonPos(a : Int, b : Int, c : Int) : ()

Reverses non-strict order when multiplying on the left by a non-positive factor.

Requires: a <= b, c <= 0

Ensures: c * b <= c * a

Use when: scaling a <= fact by a known non-positive multiplier written first.

mulLtMonoRightPos(a : Int, b : Int, c : Int) : ()

Preserves strict order when multiplying on the right by a positive factor.

Requires: a < b, 0 < c

Ensures: a * c < b * c

Use when: scaling a < fact by a known positive multiplier.

mulLtAntiMonoRightNeg(a : Int, b : Int, c : Int) : ()

Reverses strict order when multiplying on the right by a negative factor.

Requires: a < b, c < 0

Ensures: b * c < a * c

Use when: scaling a < fact by a known negative multiplier.

mulCancelRightEq(a : Int, b : Int, c : Int) : ()

Cancels a common non-zero right factor from an equality.

Requires: c != 0, a * c == b * c

Ensures: a == b

Use when: equality is known only after both sides were multiplied by the same non-zero factor.

mulCancelLeftEq(a : Int, b : Int, c : Int) : ()

Cancels a common non-zero left factor from an equality.

Requires: c != 0, c * a == c * b

Ensures: a == b

Use when: equality is known only after both sides were multiplied by the same non-zero factor written first.

mulCancelRightLePos(a : Int, b : Int, c : Int) : ()

Cancels a positive right factor from a non-strict inequality without reversing order.

Requires: 0 < c, a * c <= b * c

Ensures: a <= b

Use when: deriving the original <= relation from a scaled inequality.

mulCancelRightLeNeg(a : Int, b : Int, c : Int) : ()

Cancels a negative right factor from a non-strict inequality and reverses order.

Requires: c < 0, a * c <= b * c

Ensures: b <= a

Use when: deriving the reversed <= relation from an inequality scaled by a negative factor.

divByOne(a : Int) : ()

Establishes that division by one leaves an integer unchanged.

Ensures: a / 1 == a

Use when: simplifying quotient terms with divisor 1.

divSelf(a : Int) : ()

Establishes that a non-zero integer divided by itself is one.

Requires: a != 0

Ensures: a / a == 1

Use when: simplifying self-division after non-zero-ness is known.

zeroDiv(c : Int) : ()

Establishes that zero divided by a non-zero integer is zero.

Requires: c != 0

Ensures: 0 / c == 0

Use when: simplifying a quotient with zero numerator.

divMulLeSelf(a : Int, c : Int) : ()

Provides the lower product bound for quotient truncation with a non-negative dividend and positive divisor.

Requires: 0 <= a, 0 < c

Ensures: (a / c) * c <= a

Use when: proving that the quotient product does not exceed the original non-negative dividend.

divMulLtSelfPos(a : Int, c : Int) : ()

Provides the strict upper product bound for floor division by a positive divisor.

Requires: 0 < c

Ensures: a < ((a / c) + 1) * c

Use when: bounding a by the next quotient bucket.

divLeMonoNumPos(a : Int, b : Int, c : Int) : ()

Preserves non-strict order through division by a positive divisor.

Requires: 0 < c, a <= b

Ensures: a / c <= b / c

Use when: lifting a numerator bound through integer division.

divLowerBoundFromEqPos(a : Int, q : Int, c : Int) : ()

Derives the lower range bound from an exact quotient equation.

Requires: 0 < c, 0 <= a, a / c == q

Ensures: q * c <= a

Use when: unpacking a / c == q into the first half of the quotient range.

divUpperBoundFromEqPos(a : Int, q : Int, c : Int) : ()

Derives the strict upper range bound from an exact quotient equation.

Requires: 0 < c, a / c == q

Ensures: a < (q + 1) * c

Use when: unpacking a / c == q into the second half of the quotient range.

divEqFromRangePos(a : Int, q : Int, c : Int) : ()

Derives an exact quotient from the tight floor-division range.

Requires: 0 < c, 0 <= a, q * c <= a, a < (q + 1) * c

Ensures: a / c == q

Use when: proving a quotient equality from lower and upper product bounds.

divLtOfLtMulPos(a : Int, b : Int, c : Int) : ()

Converts a strict product upper bound into a strict quotient bound.

Requires: 0 < c, 0 <= a, a < b * c

Ensures: a / c < b

Use when: proving an upper bound on a quotient from a < b * c.

ltMulOfDivLtPos(a : Int, b : Int, c : Int) : ()

Converts a strict quotient bound back into a strict product upper bound.

Requires: 0 < c, a / c < b

Ensures: a < b * c

Use when: expanding a / c < b into a multiplication-side bound.

divLeOfLeMulPos(a : Int, b : Int, c : Int) : ()

Converts a non-strict product upper bound into a non-strict quotient bound.

Requires: 0 < c, a <= b * c

Ensures: a / c <= b

Use when: proving an upper bound on a quotient from a <= b * c.

ltMulOfDivLePos(a : Int, b : Int, c : Int) : ()

Converts a non-strict quotient upper bound into the next strict product bound.

Requires: 0 < c, a / c <= b

Ensures: a < (b + 1) * c

Use when: moving from a / c <= b to the corresponding bucket upper bound.

divGeOfGeMulPos(a : Int, b : Int, c : Int) : ()

Converts a product lower bound into a quotient lower bound.

Requires: 0 < c, b * c <= a

Ensures: b <= a / c

Use when: proving a lower bound on a quotient from b * c <= a.

leMulOfDivGePos(a : Int, b : Int, c : Int) : ()

Converts a quotient lower bound back into a product lower bound.

Requires: 0 < c, b <= a / c

Ensures: b * c <= a

Use when: expanding b <= a / c into a multiplication-side bound.

mulDivCancelRight(a : Int, c : Int) : ()

Cancels division by a non-zero right factor after multiplication by that factor.

Requires: c != 0

Ensures: (a * c) / c == a

Use when: simplifying an exact quotient of a right-multiplied term.

mulDivCancelLeft(a : Int, c : Int) : ()

Cancels division by a non-zero factor after left multiplication by that factor.

Requires: c != 0

Ensures: (c * a) / c == a

Use when: simplifying an exact quotient of a left-multiplied term.

divAddMulExact(a : Int, k : Int, c : Int) : ()

Shows that adding a multiple of a positive divisor shifts the quotient exactly.

Requires: 0 < c, 0 <= a, 0 <= a + k * c

Ensures: (a + k * c) / c == (a / c) + k

Use when: proving quotient changes after adding or subtracting whole divisor multiples.

divAddLowerPos(a : Int, b : Int, c : Int) : ()

Provides the lower bound for the quotient of a sum of non-negative terms.

Requires: 0 < c, 0 <= a, 0 <= b

Ensures: (a / c) + (b / c) <= (a + b) / c

Use when: relating separate quotient lower bounds to the quotient of a combined amount.

divAddUpperPos(a : Int, b : Int, c : Int) : ()

Provides the upper bound for the quotient of a sum.

Requires: 0 < c

Ensures: (a + b) / c <= (a / c) + (b / c) + 1

Use when: bounding quotient growth caused by adding two numerators.

divMulLe(a : Int, b : Int, c : Int) : ()

Provides the quotient-product lower bucket bound for a non-negative product.

Requires: 0 < c, 0 <= a, 0 <= b

Ensures: ((a * b) / c) * c <= (a * b)

Use when: proving that truncating (a * b) / c and multiplying back stays below a * b.

mulDivLeNonNeg(a : Int, b : Int, c : Int) : ()

Bounds a scaled non-negative value by its original value when the scale is at most the divisor.

Requires: 0 < c, 0 <= a, 0 <= b, b <= c

Ensures: (a * b) / c <= a

Use when: proving that multiplying by b / c cannot increase a non-negative a when b <= c.

mulDivGeNonPos(a : Int, b : Int, c : Int) : ()

Bounds a scaled non-positive value below by its original value when the scale is between zero and one.

Requires: 0 < c, a <= 0, 0 <= b, b <= c

Ensures: a <= (a * b) / c

Use when: proving that multiplying a non-positive a by b / c moves it toward zero.

mulDivLtPos(a : Int, b : Int, c : Int) : ()

Provides a strict upper bound for scaling a positive value by a proper fraction.

Requires: 0 < c, 0 < a, 0 <= b, b < c

Ensures: (a * b) / c < a

Use when: proving strict decrease after multiplying a positive value by b / c with b < c.

Summary

• Spec-only axiom module under mo:core/axiom/Int.
• Exposes 65 trusted lemmas.