Std.Proof.LinearArithmetic.Semantics

View source →

Trusted semantic lemmas used by the linear-arithmetic proof modules. The declarations relate coefficient lists and their evaluated sums.

Functions

# fn adding_holding_affine_forms_preserves_holding(left_coefficients: List(Int), right_coefficients: List(Int), result_coefficients: List(Int), valuation: List(Int), left_constant: Int, right_constant: Int, alignment: AddedCoefficientsAt(left_coefficients, right_coefficients, result_coefficients, valuation), left_holds: IsLessThanOrEqual(dot(left_coefficients, valuation), left_constant), right_holds: IsLessThanOrEqual(dot(right_coefficients, valuation), right_constant)) -> IsLessThanOrEqual(dot(result_coefficients, valuation), add_int(left_constant, right_constant))
# fn dot_added_coefficients(left: List(Int), right: List(Int), result: List(Int), valuation: List(Int), alignment: AddedCoefficientsAt(left, right, result, valuation)) -> Equivalent(Int, dot(result, valuation), add_int(dot(left, valuation), dot(right, valuation)))
# fn dot_scaled_coefficients(scalar: Nat, source: List(Int), result: List(Int), valuation: List(Int), alignment: ScaledCoefficientsAt(scalar, source, result, valuation)) -> Equivalent(Int, dot(result, valuation), scale_nat_int(scalar, dot(source, valuation)))
# fn dot_zero_coefficients(coefficients: List(Int), valuation: Valuation, alignment: ZeroCoefficientsAt(coefficients, valuation)) -> Equivalent(Int, dot(coefficients, valuation), int_zero())
# fn folding_aligned_holding_affine_forms_preserves_holding(coefficient_sets: List(List(Int)), constants: List(Int), witness: List(Nat), result_coefficients: List(Int), result_constant: Int, valuation: List(Int), fold: WeightedAffineFold(coefficient_sets, constants, witness, result_coefficients, result_constant, valuation), holds: AllAffineFormsHold(coefficient_sets, constants, valuation)) -> IsLessThanOrEqual(dot(result_coefficients, valuation), result_constant)
# fn normalize_atom_preserves_evaluation(coefficients: List(Int), constant: Int, relation: Relation, valuation: Valuation) -> Equivalent(Bool, evaluate_atom(normalize_atom(linear_atom(coefficients, constant, relation)), valuation), evaluate_atom(linear_atom(coefficients, constant, relation), valuation))

Functions

# fn dot_added_coefficients(left: List(Int), right: List(Int), result: List(Int), valuation: List(Int), alignment: AddedCoefficientsAt(left, right, result, valuation)) -> Equivalent(Int, dot(result, valuation), add_int(dot(left, valuation), dot(right, valuation)))

# fn dot_scaled_coefficients(scalar: Nat, source: List(Int), result: List(Int), valuation: List(Int), alignment: ScaledCoefficientsAt(scalar, source, result, valuation)) -> Equivalent(Int, dot(result, valuation), scale_nat_int(scalar, dot(source, valuation)))

# fn dot_zero_coefficients(coefficients: List(Int), valuation: Valuation, alignment: ZeroCoefficientsAt(coefficients, valuation)) -> Equivalent(Int, dot(coefficients, valuation), int_zero())