Std.Proof.LinearArithmetic

View source →

Executable affine syntax for verified LIA reflection. This module is total and deliberately rejects malformed dimensions instead of inheriting List.zip_with's truncating semantics.

Types

type Relation = LessOrEqual | LessThan
type Hypotheses
type FarkasWitness
type Valuation

Functions

# fn add_atoms(left: LinearAtom, right: LinearAtom) -> Option(LinearAtom)
# fn add_coefficients(left: List(Int), right: List(Int)) -> Option(List(Int))
# fn all_zero(coefficients: List(Int)) -> Bool
# fn append_goal(hypotheses: Hypotheses, goal: LinearAtom) -> List(LinearAtom)
# fn atoms_match_dimension(atoms: List(LinearAtom), dimension: Nat) -> Bool
# fn check_lia_candidate(hypotheses: Hypotheses, goal: LinearAtom, witness: FarkasWitness) -> Bool

Executable P1 candidate check. Task 6 wraps the same computation in proof-relevant ValidFarkasCertificate evidence and exports check_lia.
# fn coefficients_match_dimension(coefficients: List(Int), dimension: Nat) -> Bool
# fn combine(dimension: Nat, atoms: List(LinearAtom), witness: FarkasWitness) -> Option(LinearAtom)
# fn dot(coefficients: List(Int), valuation: List(Int)) -> Int
# fn dot_cons(coefficient: Int, coefficients: List(Int), value: Int, valuation: List(Int)) -> Equivalent(Int, dot(Cons(coefficient, coefficients), Cons(value, valuation)), add_int(multiply_int(coefficient, value), dot(coefficients, valuation)))
# fn dot_empty(valuation: List(Int)) -> Equivalent(Int, dot(Nil(), valuation), int_zero())

Public defining equations: downstream proof modules consume these instead of relying on eager δ-unfolding of the recursive global on open terms.
# fn evaluate_atom(atom: LinearAtom, valuation: Valuation) -> Bool
# fn evaluate_atom_checked(atom: LinearAtom, valuation: Valuation) -> Option(Bool)
# fn evaluate_normalized_relation(relation: Relation, left: Int, right: Int) -> Bool
# fn evaluate_relation(relation: Relation, left: Int, right: Int) -> Bool
# fn is_manifest_contradiction(atom: LinearAtom) -> Bool
# fn linear_atom(coefficients: List(Int), constant: Int, relation: Relation) -> LinearAtom
# fn nat_equal(left: Nat, right: Nat) -> Bool
# fn nat_length(a: Type, values: List(a)) -> Nat
# fn negate_atom(atom: LinearAtom) -> LinearAtom

Negating lhs<=c gives -lhs < -c; negating lhs<c gives -lhs <= -c.
# fn negate_coefficients(coefficients: List(Int)) -> List(Int)
# fn normalize_atom(atom: LinearAtom) -> LinearAtom

Discrete-integer normalization: lhs<c iff lhs<=pred(c).
# fn normalize_relation_preserves_evaluation(relation: Relation, left: Int, right: Int) -> Equivalent(Bool, evaluate_normalized_relation(relation, left, right), evaluate_relation(relation, left, right))
# fn scale_atom(scalar: Nat, atom: LinearAtom) -> LinearAtom
# fn scale_coefficients(scalar: Nat, coefficients: List(Int)) -> List(Int)
# fn zero_atom(dimension: Nat) -> LinearAtom
# fn zeros(dimension: Nat) -> List(Int)

Types

Functions

# fn add_atoms(left: LinearAtom, right: LinearAtom) -> Option(LinearAtom)

# fn add_coefficients(left: List(Int), right: List(Int)) -> Option(List(Int))

# fn all_zero(coefficients: List(Int)) -> Bool

# fn append_goal(hypotheses: Hypotheses, goal: LinearAtom) -> List(LinearAtom)

# fn atoms_match_dimension(atoms: List(LinearAtom), dimension: Nat) -> Bool

# fn check_lia_candidate(hypotheses: Hypotheses, goal: LinearAtom, witness: FarkasWitness) -> Bool

# fn coefficients_match_dimension(coefficients: List(Int), dimension: Nat) -> Bool

# fn combine(dimension: Nat, atoms: List(LinearAtom), witness: FarkasWitness) -> Option(LinearAtom)

# fn dot(coefficients: List(Int), valuation: List(Int)) -> Int

# fn dot_cons(coefficient: Int, coefficients: List(Int), value: Int, valuation: List(Int)) -> Equivalent(Int, dot(Cons(coefficient, coefficients), Cons(value, valuation)), add_int(multiply_int(coefficient, value), dot(coefficients, valuation)))

# fn dot_empty(valuation: List(Int)) -> Equivalent(Int, dot(Nil(), valuation), int_zero())

# fn evaluate_atom(atom: LinearAtom, valuation: Valuation) -> Bool

# fn evaluate_atom_checked(atom: LinearAtom, valuation: Valuation) -> Option(Bool)

# fn evaluate_normalized_relation(relation: Relation, left: Int, right: Int) -> Bool

# fn evaluate_relation(relation: Relation, left: Int, right: Int) -> Bool

# fn is_manifest_contradiction(atom: LinearAtom) -> Bool

# fn linear_atom(coefficients: List(Int), constant: Int, relation: Relation) -> LinearAtom

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

# fn nat_length(a: Type, values: List(a)) -> Nat

# fn negate_atom(atom: LinearAtom) -> LinearAtom

# fn negate_coefficients(coefficients: List(Int)) -> List(Int)

# fn normalize_atom(atom: LinearAtom) -> LinearAtom

# fn normalize_relation_preserves_evaluation(relation: Relation, left: Int, right: Int) -> Equivalent(Bool, evaluate_normalized_relation(relation, left, right), evaluate_relation(relation, left, right))

# fn scale_atom(scalar: Nat, atom: LinearAtom) -> LinearAtom

# fn scale_coefficients(scalar: Nat, coefficients: List(Int)) -> List(Int)

# fn zero_atom(dimension: Nat) -> LinearAtom

# fn zeros(dimension: Nat) -> List(Int)