Std.Proof.Math

Proof-carrying mathematics used by refinements and ordinary Cure programs.

This module deliberately contains no trusted arithmetic oracle. Operations are total Cure functions and every law is an ordinary dependent proof term checked by the kernel. Future refinement automation may search for these theorems, but it does not get to bypass them.

Functions

# fn adding_a_positive_number_is_positive(natural: Nat, positive: Nat, proof: IsPositive(positive)) -> IsPositive(plus(natural, positive))

Adding a positive right operand to any natural number remains positive.
# fn adding_the_same_number_preserves_less_than(addend: Nat, left: Nat, right: Nat, proof: IsLessThan(left, right)) -> IsLessThan(plus(addend, left), plus(addend, right))

Adding the same number to both sides preserves strict less-than.
# fn adding_the_same_number_preserves_less_than_or_equal(addend: Nat, left: Nat, right: Nat, proof: IsLessThanOrEqual(left, right)) -> IsLessThanOrEqual(plus(addend, left), plus(addend, right))

Adding the same number to both sides preserves less-than-or-equal.
# fn adding_to_a_positive_number_is_positive(positive: Nat, other: Nat, proof: IsPositive(positive)) -> IsPositive(plus(positive, other))

Adding anything to a positive left operand remains positive.
# fn boolean_comparison_is_true_when_less_than_holds(left: Nat, right: Nat, proof: IsLessThan(left, right)) -> IsTrue(natural_is_less_than(left, right))
# fn boolean_comparison_is_true_when_less_than_or_equal_holds(left: Nat, right: Nat, proof: IsLessThanOrEqual(left, right)) -> IsTrue(natural_is_less_than_or_equal(left, right))
# fn boolean_comparison_is_true_when_positive_holds(value: Nat, proof: IsPositive(value)) -> IsTrue(natural_is_positive(value))
# fn decide_is_less_than(left: Nat, right: Nat) -> Decision(IsLessThan(left, right))

Decide strict less-than with checked evidence in either branch.
# fn decide_is_less_than_or_equal(left: Nat, right: Nat) -> Decision(IsLessThanOrEqual(left, right))

Decide less-than-or-equal with checked evidence in either branch.
# fn decide_is_positive(value: Nat) -> Decision(IsPositive(value))

Decide positivity while carrying either a proof or a disproof.
# fn less_than_holds_when_boolean_comparison_is_true(left: Nat, right: Nat, evidence: IsTrue(natural_is_less_than(left, right))) -> IsLessThan(left, right)
# fn less_than_or_equal_holds_when_boolean_comparison_is_true(left: Nat, right: Nat, evidence: IsTrue(natural_is_less_than_or_equal(left, right))) -> IsLessThanOrEqual(left, right)

Reflection: the boolean comparison being true carries the same information as the inductive relation. Proved by induction, mirroring the boolean function's own match structure; uninhabited arms discharge by empty match on evidence.
# fn less_than_or_equal_is_reflexive(value: Nat) -> IsLessThanOrEqual(value, value)

Every natural number is less than or equal to itself.
# fn less_than_or_equal_is_transitive(left: Nat, middle: Nat, right: Nat, left_to_middle: IsLessThanOrEqual(left, middle), middle_to_right: IsLessThanOrEqual(middle, right)) -> IsLessThanOrEqual(left, right)

Less-than-or-equal evidence composes transitively.
# fn multiply(left: Nat, right: Nat) -> Nat

Natural-number multiplication, defined structurally on the left operand.
# fn multiplying_positive_numbers_is_positive(left: Nat, right: Nat, left_is_positive: IsPositive(left), right_is_positive: IsPositive(right)) -> IsPositive(multiply(left, right))

The product of two positive natural numbers is positive.

Matching the left proof refines left to a successor. Multiplication then reduces to right + multiply(predecessor, right), whose positivity follows directly from the proof that right is positive.
# fn natural_is_less_than(left: Nat, right: Nat) -> Bool

Boolean-valued strict "less than".
# fn natural_is_less_than_or_equal(left: Nat, right: Nat) -> Bool

Boolean-valued "less than or equal", structural on both operands.
# fn natural_is_positive(value: Nat) -> Bool

Boolean-valued positivity.
# fn positive_holds_when_boolean_comparison_is_true(value: Nat, evidence: IsTrue(natural_is_positive(value))) -> IsPositive(value)
# fn positive_means_zero_is_less_than(value: Nat, proof: IsPositive(value)) -> IsLessThan(Z, value)

Positivity is the same proposition as zero being strictly less than a value.
# fn successor_is_not_less_than_or_equal_to_zero(predecessor: Nat, proof: IsLessThanOrEqual(S(predecessor), Z)) -> Empty
# fn successor_is_not_less_than_zero(predecessor: Nat, proof: IsLessThan(S(predecessor), Z)) -> Empty
# fn successor_is_positive(predecessor: Nat) -> IsPositive(S(predecessor))

Every successor natural number is positive.
# fn successors_preserve_less_than_disproof(left: Nat, right: Nat, disproof: Function(IsLessThan(left, right), Empty), proof: IsLessThan(S(left), S(right))) -> Empty
# fn successors_preserve_less_than_or_equal_disproof(left: Nat, right: Nat, disproof: Function(IsLessThanOrEqual(left, right), Empty), proof: IsLessThanOrEqual(S(left), S(right))) -> Empty
# fn zero_is_less_than_means_positive(value: Nat, proof: IsLessThan(Z, value)) -> IsPositive(value)

Strictly exceeding zero is evidence of positivity.
# fn zero_is_not_less_than_zero(proof: IsLessThan(Z, Z)) -> Empty
# fn zero_is_not_positive(proof: IsPositive(Z)) -> Empty

Zero cannot carry evidence of strict positivity.

Functions

# fn adding_a_positive_number_is_positive(natural: Nat, positive: Nat, proof: IsPositive(positive)) -> IsPositive(plus(natural, positive))

# fn adding_the_same_number_preserves_less_than(addend: Nat, left: Nat, right: Nat, proof: IsLessThan(left, right)) -> IsLessThan(plus(addend, left), plus(addend, right))

# fn adding_the_same_number_preserves_less_than_or_equal(addend: Nat, left: Nat, right: Nat, proof: IsLessThanOrEqual(left, right)) -> IsLessThanOrEqual(plus(addend, left), plus(addend, right))

# fn adding_to_a_positive_number_is_positive(positive: Nat, other: Nat, proof: IsPositive(positive)) -> IsPositive(plus(positive, other))

# fn boolean_comparison_is_true_when_less_than_holds(left: Nat, right: Nat, proof: IsLessThan(left, right)) -> IsTrue(natural_is_less_than(left, right))

# fn boolean_comparison_is_true_when_less_than_or_equal_holds(left: Nat, right: Nat, proof: IsLessThanOrEqual(left, right)) -> IsTrue(natural_is_less_than_or_equal(left, right))

# fn boolean_comparison_is_true_when_positive_holds(value: Nat, proof: IsPositive(value)) -> IsTrue(natural_is_positive(value))

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

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

# fn decide_is_positive(value: Nat) -> Decision(IsPositive(value))

# fn less_than_holds_when_boolean_comparison_is_true(left: Nat, right: Nat, evidence: IsTrue(natural_is_less_than(left, right))) -> IsLessThan(left, right)

# fn less_than_or_equal_holds_when_boolean_comparison_is_true(left: Nat, right: Nat, evidence: IsTrue(natural_is_less_than_or_equal(left, right))) -> IsLessThanOrEqual(left, right)

# fn less_than_or_equal_is_reflexive(value: Nat) -> IsLessThanOrEqual(value, value)

# fn less_than_or_equal_is_transitive(left: Nat, middle: Nat, right: Nat, left_to_middle: IsLessThanOrEqual(left, middle), middle_to_right: IsLessThanOrEqual(middle, right)) -> IsLessThanOrEqual(left, right)

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

# fn multiplying_positive_numbers_is_positive(left: Nat, right: Nat, left_is_positive: IsPositive(left), right_is_positive: IsPositive(right)) -> IsPositive(multiply(left, right))

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

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

# fn natural_is_positive(value: Nat) -> Bool

# fn positive_holds_when_boolean_comparison_is_true(value: Nat, evidence: IsTrue(natural_is_positive(value))) -> IsPositive(value)

# fn positive_means_zero_is_less_than(value: Nat, proof: IsPositive(value)) -> IsLessThan(Z, value)

# fn successor_is_not_less_than_or_equal_to_zero(predecessor: Nat, proof: IsLessThanOrEqual(S(predecessor), Z)) -> Empty

# fn successor_is_not_less_than_zero(predecessor: Nat, proof: IsLessThan(S(predecessor), Z)) -> Empty

# fn successor_is_positive(predecessor: Nat) -> IsPositive(S(predecessor))

# fn successors_preserve_less_than_disproof(left: Nat, right: Nat, disproof: Function(IsLessThan(left, right), Empty), proof: IsLessThan(S(left), S(right))) -> Empty

# fn successors_preserve_less_than_or_equal_disproof(left: Nat, right: Nat, disproof: Function(IsLessThanOrEqual(left, right), Empty), proof: IsLessThanOrEqual(S(left), S(right))) -> Empty

# fn zero_is_less_than_means_positive(value: Nat, proof: IsLessThan(Z, value)) -> IsPositive(value)

# fn zero_is_not_less_than_zero(proof: IsLessThan(Z, Z)) -> Empty

# fn zero_is_not_positive(proof: IsPositive(Z)) -> Empty