axiom/MinMax

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

Status

• Spec-only axiom module

Public API

Types

• Int

Lemmas

idempotence(a : Int) : ()

Establishes the listed proof facts in the current verification context.

Contract

ensures Int.min(a, a) == a;
ensures Int.max(a, a) == a;

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

commutativity(a : Int, b : Int) : ()

Establishes the listed proof facts in the current verification context.

Contract

ensures Int.min(a, b) == Int.min(b, a);
ensures Int.max(a, b) == Int.max(b, a);

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

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

Establishes the listed proof facts in the current verification context.

Contract

ensures Int.min(a, Int.min(b, c)) == Int.min(Int.min(a, b), c);
ensures Int.max(a, Int.max(b, c)) == Int.max(Int.max(a, b), c);

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

bounds(a : Int, b : Int) : ()

Establishes the listed proof facts in the current verification context.

Contract

ensures Int.min(a, b) <= a;
ensures Int.min(a, b) <= b;
ensures a <= Int.max(a, b);
ensures b <= Int.max(a, b);

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

ifThenElse(a : Int, b : Int) : ()

Establishes the listed proof facts in the current verification context.

Contract

requires a <= b;
ensures Int.min(a, b) == a;
ensures Int.max(a, b) == b;

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

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

Establishes the listed proof facts in the current verification context.

Contract

requires a <= b;
ensures Int.min(a, c) <= Int.min(b, c);
ensures Int.max(a, c) <= Int.max(b, c);

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/MinMax.
• Exposes 6 trusted lemmas.