Std.Proof.IntOrder

Functions

• # fn absurd(a: Type, void: Empty) -> a

  Ex falso: anything follows from a proof of the empty type.

• # fn add_int(addend: Int, x: Int) -> Int

  Total integer addition, defined by iterating the successor/predecessor on x according to the sign and magnitude of addend. FromNat(m) steps up m times; NegativeSuccessor(k) steps down k + 1 times.

• # fn add_int_associative(a: Int, b: Int, c: Int) -> Equivalent(Int, add_int(a, add_int(b, c)), add_int(add_int(a, b), c))

• # fn add_int_commutative(left: Int, right: Int) -> Equivalent(Int, add_int(left, right), add_int(right, left))

• # fn add_int_cong_left(a: Int, b: Int, c: Int, proof: Equivalent(Int, a, b)) -> Equivalent(Int, add_int(a, c), add_int(b, c))

• # fn add_int_cong_right(a: Int, b: Int, c: Int, proof: Equivalent(Int, b, c)) -> Equivalent(Int, add_int(a, b), add_int(a, c))

• # fn add_int_is_monotone(addend: Int, a: Int, b: Int, a_le_b: IsTrue(le_int(a, b))) -> IsTrue(le_int(add_int(addend, a), add_int(addend, b)))

  Integer addition is monotone in its second argument (Boolean form): a ≤ b → addend + a ≤ addend + b, by iterating succ/pred monotonicity.

• # fn add_int_is_monotone_both(a: Int, b: Int, c: Int, d: Int, ab: IsTrue(le_int(a, b)), cd: IsTrue(le_int(c, d))) -> IsTrue(le_int(add_int(a, c), add_int(b, d)))

• # fn add_int_is_monotone_first(addend: Int, left: Int, right: Int, proof: IsTrue(le_int(left, right))) -> IsTrue(le_int(add_int(left, addend), add_int(right, addend)))

  Addition is monotone in its first argument, derived from commutativity and the already-proved second-argument monotonicity.

• # fn add_int_left_inverse(value: Int) -> Equivalent(Int, add_int(negate(value), value), int_zero())

• # fn add_int_left_pred(left: Int, right: Int) -> Equivalent(Int, add_int(pred_int(left), right), pred_int(add_int(left, right)))

• # fn add_int_left_succ(left: Int, right: Int) -> Equivalent(Int, add_int(succ_int(left), right), succ_int(add_int(left, right)))

• # fn add_int_rearrange_four(a: Int, b: Int, c: Int, d: Int) -> Equivalent(Int, add_int(add_int(a, b), add_int(c, d)), add_int(add_int(a, c), add_int(b, d)))

  Four-term interchange, derived solely from associativity and commutativity: (a+b)+(c+d) = (a+c)+(b+d).

• # fn add_int_right_inverse(value: Int) -> Equivalent(Int, add_int(value, negate(value)), int_zero())

• # fn add_int_right_inverse_is_unique(value: Int, candidate: Int, proof: Equivalent(Int, add_int(value, candidate), int_zero())) -> Equivalent(Int, candidate, negate(value))

• # fn add_int_right_pred(addend: Int, value: Int) -> Equivalent(Int, add_int(addend, pred_int(value)), pred_int(add_int(addend, value)))

• # fn add_int_right_succ(addend: Int, value: Int) -> Equivalent(Int, add_int(addend, succ_int(value)), succ_int(add_int(addend, value)))

• # fn add_int_zero_left(value: Int) -> Equivalent(Int, add_int(int_zero(), value), value)

• # fn add_int_zero_right(value: Int) -> Equivalent(Int, add_int(value, int_zero()), value)

• # fn add_nat_pred(count: Nat, x: Int) -> Int

  x retreated count integer predecessors.

• # fn add_nat_pred_is_monotone(count: Nat, a: Int, b: Int, a_le_b: IsTrue(le_int(a, b))) -> IsTrue(le_int(add_nat_pred(count, a), add_nat_pred(count, b)))

  Iterating a monotone integer predecessor preserves ≤.

• # fn add_nat_pred_right_pred(count: Nat, value: Int) -> Equivalent(Int, add_nat_pred(count, pred_int(value)), pred_int(add_nat_pred(count, value)))

• # fn add_nat_pred_right_succ(count: Nat, value: Int) -> Equivalent(Int, add_nat_pred(count, succ_int(value)), succ_int(add_nat_pred(count, value)))

• # fn add_nat_pred_zero_successor(count: Nat) -> Equivalent(Int, add_nat_pred(S(count), int_zero()), NegativeSuccessor(count))

• # fn add_nat_succ(count: Nat, x: Int) -> Int

  x advanced count integer successors.

• # fn add_nat_succ_is_monotone(count: Nat, a: Int, b: Int, a_le_b: IsTrue(le_int(a, b))) -> IsTrue(le_int(add_nat_succ(count, a), add_nat_succ(count, b)))

  Iterating a monotone integer successor preserves ≤.

• # fn add_nat_succ_right_pred(count: Nat, value: Int) -> Equivalent(Int, add_nat_succ(count, pred_int(value)), pred_int(add_nat_succ(count, value)))

• # fn add_nat_succ_right_succ(count: Nat, value: Int) -> Equivalent(Int, add_nat_succ(count, succ_int(value)), succ_int(add_nat_succ(count, value)))

  Iterated successor/predecessor commute with one step on their argument.

• # fn add_nat_succ_zero(count: Nat) -> Equivalent(Int, add_nat_succ(count, int_zero()), FromNat(count))

• # fn add_value_to_negated_successor_scale(count: Nat, value: Int) -> Equivalent(Int, add_int(value, negate(scale_nat_int(S(count), value))), negate(scale_nat_int(count, value)))

• # fn adding_preserves_less_than_or_equal(a: Int, b: Int, c: Int, d: Int, ab: IsLessThanOrEqual(a, b), cd: IsLessThanOrEqual(c, d)) -> IsLessThanOrEqual(add_int(a, c), add_int(b, d))

• # fn adding_the_same_number_preserves_less_than_or_equal(addend: Int, left: Int, right: Int, proof: IsLessThanOrEqual(left, right)) -> IsLessThanOrEqual(add_int(addend, left), add_int(addend, right))

  Adding the same integer to both sides preserves less-than-or-equal. The sides are explicit (see the module header) since add_int_is_monotone inspects them.

• # fn at_most_is_refuted_by_boolean_refuter(left: Int, right: Int, refuter: Function(IsTrue(le_int(left, right)), Empty), proof: IsLessThanOrEqual(left, right)) -> Empty

  Invert AtMost: a refutation of the reflected Boolean evidence refutes the whole ≤ proof (its only constructor carries exactly that evidence).

• # fn decide_is_less_than(left: Int, right: Int) -> Decision(IsLessThan(left, right))

  Decide strict < on integers, carrying checked evidence either way.

• # fn decide_is_less_than_or_equal(left: Int, right: Int) -> Decision(IsLessThanOrEqual(left, right))

  Decide ≤ on integers, carrying checked evidence either way. Reuses the generic decidable-Boolean decision on le_int(left, right).

• # fn from_nat_le_evidence(l: Nat, r: Nat, ev: IsTrue(le_nat(l, r))) -> IsTrue(le_int(FromNat(l), FromNat(r)))

  A nonnegative-into-Int order witness between FromNat operands is exactly le_nat (return-type conversion reduces le_int(FromNat l, FromNat r)).

• # fn int_negative_one() -> Int

• # fn int_one() -> Int

• # fn int_zero() -> Int

  Canonical integer constants used by the reflective LIA checker. Functions, rather than a second data representation, keep every caller on Std.Int.Int.

• # fn is_less_than_or_equal_is_reflexive(value: Int) -> IsLessThanOrEqual(value, value)

  Reflexivity: every integer is ≤ itself.

• # fn is_less_than_or_equal_is_transitive(left: Int, middle: Int, right: Int, left_to_middle: IsLessThanOrEqual(left, middle), middle_to_right: IsLessThanOrEqual(middle, right)) -> IsLessThanOrEqual(left, right)

  Less-than-or-equal evidence composes transitively. The compared integers are explicit (see the module header): the reflected proof does not carry them, and le_int_transitive must inspect them.

• # fn le_int(left: Int, right: Int) -> Bool

  Boolean less-than-or-equal on the inductive integers. Nonneg/nonneg reduces to le_nat; any negative is ≤ any nonneg; no nonneg is ≤ a negative; neg/neg reverses le_nat on the successors, since -(k+1) ≤ -(j+1) ⇔ j ≤ k.

• # fn le_int_from_nat_is_reflexive(n: Nat) -> IsTrue(le_int(FromNat(n), FromNat(n)))

  le_int(FromNat(n), FromNat(n)) reduces to le_nat(n, n), which is True. Stated at the reduced result type so the conversion — not the constructor index path — performs the le_int → le_nat reduction; the witness is then syntactically what AtMost expects on the FromNat reflexivity arm.

• # fn le_int_neg_succ_is_reflexive(k: Nat) -> IsTrue(le_int(NegativeSuccessor(k), NegativeSuccessor(k)))

  Same, for le_int(NegativeSuccessor(k), NegativeSuccessor(k)) → le_nat(k, k).

• # fn le_int_transitive(a: Int, b: Int, c: Int, a_le_b: IsTrue(le_int(a, b)), b_le_c: IsTrue(le_int(b, c))) -> IsTrue(le_int(a, c))

  le_int composes transitively (Boolean form). Case-splits on the outer integers a, c, then the middle b; real cases delegate to le_nat_transitive (the neg/neg case reversed), the rest are immediate or refuted from the evidence.

• # fn le_int_transport(left: Int, left2: Int, right: Int, right2: Int, left_equal: Equivalent(Int, left, left2), right_equal: Equivalent(Int, right, right2), proof: IsTrue(le_int(left, right))) -> IsTrue(le_int(left2, right2))

• # fn le_nat(left: Nat, right: Nat) -> Bool

  Boolean less-than-or-equal on naturals, structural on the left operand.

• # fn le_nat_add_left_weakens(base: Nat, addend: Nat) -> IsTrue(le_nat(base, plus(addend, base)))

  base ≤ addend + base: adding on the left only grows a natural number.

• # fn le_nat_is_reflexive(value: Nat) -> IsTrue(le_nat(value, value))

  le_nat is reflexive: le_nat(n, n) computes to True for every n.

• # fn le_nat_multiply_is_monotone(scalar: Nat, left: Nat, right: Nat, lr: IsTrue(le_nat(left, right))) -> IsTrue(le_nat(multiply(scalar, left), multiply(scalar, right)))

  left ≤ right ⇒ scalar·left ≤ scalar·right on the Boolean test. Induction on the scalar; the successor step is multiply(S(sp), v) = plus(v, multiply(sp, v)), discharged by two-sided addition monotonicity.

• # fn le_nat_plus_is_monotone(a: Nat, b: Nat, x: Nat, y: Nat, ab: IsTrue(le_nat(a, b)), xy: IsTrue(le_nat(x, y))) -> IsTrue(le_nat(plus(a, x), plus(b, y)))

  a ≤ b and x ≤ y ⇒ a + x ≤ b + y: two-sided addition monotonicity.

• # fn le_nat_plus_is_monotone_left(a: Nat, b: Nat, y: Nat, ab: IsTrue(le_nat(a, b))) -> IsTrue(le_nat(plus(a, y), plus(b, y)))

  a ≤ b ⇒ a + y ≤ b + y: monotone in the left addend.

• # fn le_nat_plus_is_monotone_right(a: Nat, x: Nat, y: Nat, xy: IsTrue(le_nat(x, y))) -> IsTrue(le_nat(plus(a, x), plus(a, y)))

  x ≤ y ⇒ a + x ≤ a + y: monotone in the right addend.

• # fn le_nat_transitive(a: Nat, b: Nat, c: Nat, a_le_b: IsTrue(le_nat(a, b)), b_le_c: IsTrue(le_nat(b, c))) -> IsTrue(le_nat(a, c))

  le_nat composes transitively (Boolean form). A zero left operand is immediate; the impossible S(_) ≤ Z cases are refuted from the evidence.

• # fn le_nat_weaken_right(smaller: Nat, larger: Nat, evidence: IsTrue(le_nat(smaller, larger))) -> IsTrue(le_nat(smaller, S(larger)))

  le_nat(smaller, larger) ⇒ le_nat(smaller, S(larger)): weaken the bound.

• # fn less_than_or_equal_transport(left: Int, left2: Int, right: Int, right2: Int, left_equal: Equivalent(Int, left, left2), right_equal: Equivalent(Int, right, right2), proof: IsLessThanOrEqual(left, right)) -> IsLessThanOrEqual(left2, right2)

• # fn lt_int(left: Int, right: Int) -> Bool

  Boolean strictly-less-than on the inductive integers. Nonneg/nonneg reduces to lt_nat; any negative is < any nonneg; no nonneg is < a negative; neg/neg reverses lt_nat on the successors, since -(k+1) < -(j+1) ⇔ j < k.

• # fn lt_nat(left: Nat, right: Nat) -> Bool

  Boolean strictly-less-than on naturals, structural on the right operand.

• # fn multiply(left: Nat, right: Nat) -> Nat

  ── Nonnegative-scaling monotonicity ─────────────────────────────────────

  Scaling both sides of b ≤ c by a nonnegative integer preserves the order. The reduction target is natural-number multiplication (Nat → Nat → Nat), so the scalar and the operands are the nonnegative cone: scalar : Nat witnesses 0 ≤ FromNat(scalar), and left/right are the FromNat operands. On that cone the Int order proof between FromNat values is exactly the Boolean le_nat, so the whole development stays in the Boolean test world — no equational transport.

  multiply below is a local mirror of Std.Proof.Math.multiply (identical structural definition). We cannot use Std.Proof.Math: it exports its own IsLessThanOrEqual/IsLessThan/IsPositive, whose bare names collide with this module's integer order families and mis-resolve at codegen. Referencing it qualified is not an option either — a qualified cross-module reference still requires the module to be imported. The local mirror is the same total function; the lemma it proves is identical.

  Extending this to general integer operands would require first-argument monotonicity of the iterated integer add_int, deferred as out of scope for the multiply-reduction specified here. Natural-number multiplication, structural on the left operand — a local mirror of Std.Proof.Math.multiply (see the note above on why it is not imported).

• # fn multiply_int(coefficient: Int, value: Int) -> Int

  Signed coefficient application for affine evaluation. A nonnegative coefficient delegates directly to natural scaling; -(n+1) negates the result of scaling by n+1. Both recursions are therefore over Nat.

• # fn multiply_int_cong_coefficient(left: Int, right: Int, value: Int, proof: Equivalent(Int, left, right)) -> Equivalent(Int, multiply_int(left, value), multiply_int(right, value))

• # fn multiply_int_distributes_over_coefficient_add(left: Int, right: Int, value: Int) -> Equivalent(Int, multiply_int(add_int(left, right), value), add_int(multiply_int(left, value), multiply_int(right, value)))

• # fn multiply_int_distributes_over_from_nat_add(count: Nat, right: Int, value: Int) -> Equivalent(Int, multiply_int(add_int(FromNat(count), right), value), add_int(multiply_int(FromNat(count), value), multiply_int(right, value)))

• # fn multiply_int_distributes_over_negative_add(count: Nat, right: Int, value: Int) -> Equivalent(Int, multiply_int(add_int(NegativeSuccessor(count), right), value), add_int(multiply_int(NegativeSuccessor(count), value), multiply_int(right, value)))

• # fn multiply_int_from_nat(n: Nat, value: Int) -> Equivalent(Int, multiply_int(FromNat(n), value), scale_nat_int(n, value))

• # fn multiply_int_negative_successor(n: Nat, value: Int) -> Equivalent(Int, multiply_int(NegativeSuccessor(n), value), negate(scale_nat_int(S(n), value)))

• # fn multiply_int_predecessor_coefficient(coefficient: Int, value: Int) -> Equivalent(Int, multiply_int(pred_int(coefficient), value), add_int(negate(value), multiply_int(coefficient, value)))

• # fn multiply_int_scale_nat_coefficient(scalar: Nat, coefficient: Int, value: Int) -> Equivalent(Int, multiply_int(scale_nat_int(scalar, coefficient), value), scale_nat_int(scalar, multiply_int(coefficient, value)))

• # fn multiply_int_successor_coefficient(coefficient: Int, value: Int) -> Equivalent(Int, multiply_int(succ_int(coefficient), value), add_int(value, multiply_int(coefficient, value)))

• # fn negate_distributes_over_add(left: Int, right: Int) -> Equivalent(Int, negate(add_int(left, right)), add_int(negate(left), negate(right)))

• # fn nonneg_of_from_nat(n: Nat) -> IsLessThanOrEqual(FromNat(Z()), FromNat(n))

• # fn pred_int(i: Int) -> Int

  The integer predecessor i - 1. Nonnegatives shrink (to -1 at zero) and negatives grow one more negative.

• # fn pred_int_is_monotone(a: Int, b: Int, a_le_b: IsTrue(le_int(a, b))) -> IsTrue(le_int(pred_int(a), pred_int(b)))

  The integer predecessor is monotone (Boolean form): a ≤ b → a-1 ≤ b-1.

• # fn pred_succ_int(value: Int) -> Equivalent(Int, pred_int(succ_int(value)), value)

• # fn predecessors_cancel_matching_positive(count: Nat) -> Equivalent(Int, add_nat_pred(S(count), FromNat(S(count))), int_zero())

• # fn scale_nat_int(scalar: Nat, value: Int) -> Int

  Scale an arbitrary signed integer by a nonnegative natural. This is repeated proof-level integer addition, structural on the certificate coefficient. Task 2 proves its monotonicity and distributive laws from these equations.

• # fn scale_nat_int_add_scalars(left: Nat, right: Nat, value: Int) -> Equivalent(Int, scale_nat_int(plus(left, right), value), add_int(scale_nat_int(left, value), scale_nat_int(right, value)))

  Addition in the natural scalar (coefficient) is represented by Nat.plus.

• # fn scale_nat_int_distributes_over_add(scalar: Nat, left: Int, right: Int) -> Equivalent(Int, scale_nat_int(scalar, add_int(left, right)), add_int(scale_nat_int(scalar, left), scale_nat_int(scalar, right)))

  Scaling distributes over integer addition. This is the scalar algebra that later lifts pointwise to coefficient vectors and dot products.

• # fn scale_nat_int_is_monotone(scalar: Nat, left: Int, right: Int, proof: IsLessThanOrEqual(left, right)) -> IsLessThanOrEqual(scale_nat_int(scalar, left), scale_nat_int(scalar, right))

  Natural scaling preserves order for arbitrary signed operands. The successor case combines the original inequality with the induction result.

• # fn scale_nat_int_successor(scalar: Nat, value: Int) -> Equivalent(Int, scale_nat_int(S(scalar), value), add_int(value, scale_nat_int(scalar, value)))

• # fn scale_nat_int_value_zero(scalar: Nat) -> Equivalent(Int, scale_nat_int(scalar, int_zero()), int_zero())

• # fn scale_nat_int_zero(value: Int) -> Equivalent(Int, scale_nat_int(Z(), value), int_zero())

• # fn scaling_by_nonneg_preserves_less_than_or_equal(scalar: Nat, left: Nat, right: Nat, proof: IsLessThanOrEqual(FromNat(left), FromNat(right))) -> IsLessThanOrEqual(FromNat(multiply(scalar, left)), FromNat(multiply(scalar, right)))

  Nonnegative scaling preserves ≤: given left ≤ right (as FromNat operands) and any scalar : Nat (i.e. 0 ≤ FromNat(scalar)), scalar·left ≤ scalar·right. Reduces to Std.Proof.Math.multiply via the Boolean monotonicity above.

• # fn strictly_below_is_refuted_by_boolean_refuter(left: Int, right: Int, refuter: Function(IsTrue(lt_int(left, right)), Empty), proof: IsLessThan(left, right)) -> Empty

  Invert StrictlyBelow likewise for strict <.

• # fn succ_int(i: Int) -> Int

  The integer successor i + 1. -(k+1)+1 folds the negative magnitude down (to zero when k = 0), and nonnegatives grow by one.

• # fn succ_int_is_monotone(a: Int, b: Int, a_le_b: IsTrue(le_int(a, b))) -> IsTrue(le_int(succ_int(a), succ_int(b)))

  The integer successor is monotone (Boolean form): a ≤ b → a+1 ≤ b+1.

• # fn succ_pred_int(value: Int) -> Equivalent(Int, succ_int(pred_int(value)), value)

  Successor and predecessor are mutually inverse on canonical integers.

• # fn successors_cancel_matching_negative(count: Nat) -> Equivalent(Int, add_nat_succ(count, NegativeSuccessor(count)), int_negative_one())

  Canonical cancellation spines used to establish the additive inverse laws.

• # fn zero_is_not_at_most_negative_one(proof: IsLessThanOrEqual(FromNat(Z()), NegativeSuccessor(Z()))) -> Empty

  0 ≤ -1 is impossible. le_int(FromNat(Z), NegativeSuccessor(Z)) reduces to False, so the carried witness inhabits IsTrue(False), refuted by true_is_not_false. (In the reflected form the refutation is not an empty match — every index pair is inhabited by AtMost — but destructuring the impossible evidence yields Empty all the same. This is LIA's contradiction extractor.)

• # fn zero_le_int_from_nat_evidence(n: Nat) -> IsTrue(le_int(FromNat(Z()), FromNat(n)))

  ── Sign lemmas ────────────────────────────────────────────────────────── 0 ≤ n for every natural n: le_int(FromNat(Z), FromNat(n)) reduces to le_nat(Z, n) = True, so the reflected witness is Confirmed(). Stated via a return-typed helper so the reduction lands in return-type conversion (the constructor-index path does not reduce le_int — see the reflexivity helpers above).