Skip to main content

axiom/IntAbs

Reference for mo:core/axiom/IntAbs 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/IntAbs

Status​

  • Spec-only axiom module

Public API​

Types​

  • Int

Lemmas​

nonnegativity(x : Int) : ()​

Establishes Int.fromNat(Int.abs(x)) >= 0 in the current proof context.

Contract

ensures Int.fromNat(Int.abs(x)) >= 0;

Use when: a proof needs this fact explicitly and the solver has not derived it automatically.

nonnegCase(x : Int) : ()​

Establishes Int.fromNat(Int.abs(x)) == x in the current proof context.

Contract

requires x >= 0;
ensures Int.fromNat(Int.abs(x)) == x;

Use when: a proof needs this fact explicitly and the solver has not derived it automatically.

negCase(x : Int) : ()​

Establishes Int.fromNat(Int.abs(x)) == -x in the current proof context.

Contract

requires x < 0;
ensures Int.fromNat(Int.abs(x)) == -x;

Use when: a proof needs this fact explicitly and the solver has not derived it automatically.

twoSidedBound(x : Int, n : Int) : ()​

Establishes (Int.abs(x) <= Int.toNat(n)) <==> (-n <= x and x <= n) in the current proof context.

Contract

requires n >= 0;
ensures (Int.abs(x) <= Int.toNat(n)) <==> (-n <= x and x <= n);

Use when: a proof needs this fact explicitly and the solver has not derived it automatically.

triangleIneq(x : Int, y : Int) : ()​

Establishes Int.abs(x + y) <= Int.abs(x) + Int.abs(y) in the current proof context.

Contract

ensures Int.abs(x + y) <= Int.abs(x) + Int.abs(y);

Use when: a proof needs this fact explicitly and the solver has not derived it automatically.

symmetry(x : Int) : ()​

Establishes Int.abs(-x) == Int.abs(x) in the current proof context.

Contract

ensures Int.abs(-x) == Int.abs(x);

Use when: a proof needs this fact explicitly and the solver has not derived it automatically.

Summary​

  • Spec-only axiom module under mo:core/axiom/IntAbs.
  • Exposes 6 trusted lemmas.