Rational hitting lists: signed arithmetic

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/SignedArithmetic.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

def Complexity.RationalHitting.StackLanguage.intCode (z : ℤ) : List Bool

Encode an integer by its sign bit and binary magnitude.

Equations

• Complexity.RationalHitting.StackLanguage.intCode z = Complexity.RationalHitting.StackLanguage.pairCode Complexity.RationalHitting.StackLanguage.boolCode Nat.bits (decide (z < 0), z.natAbs)

@[instance_reducible]

instance Complexity.RationalHitting.StackLanguage.instCodingInt : Coding ℤ

Equations

• Complexity.RationalHitting.StackLanguage.instCodingInt = { code := Complexity.RationalHitting.StackLanguage.intCode }

@[simp]

theorem Complexity.RationalHitting.StackLanguage.intCode_length (z : ℤ) : (intCode z).length = z.natAbs.bits.length + 3

theorem Complexity.RationalHitting.StackLanguage.nat_bits_mono {a b : ℕ} (h : a ≤ b) : a.bits.length ≤ b.bits.length

theorem Complexity.RationalHitting.StackLanguage.difference_bits_length (a b : ℕ) : (↑a - ↑b).natAbs.bits.length ≤ a.bits.length + b.bits.length

def Complexity.RationalHitting.StackLanguage.differenceAbs : Program (Fin 5)

Compute the magnitude of the signed difference of two binary natural inputs.

Equations

• Complexity.RationalHitting.StackLanguage.differenceAbs = Complexity.RationalHitting.StackLanguage.signedDifference.seq (Complexity.RationalHitting.StackLanguage.clear 3)

def Complexity.RationalHitting.StackLanguage.differenceSign : Program (Fin 5)

Compute the sign of the difference of two binary natural inputs.

Equations

• Complexity.RationalHitting.StackLanguage.differenceSign = Complexity.RationalHitting.StackLanguage.signedDifference.seq (Complexity.RationalHitting.StackLanguage.clear 0)

theorem Complexity.RationalHitting.StackLanguage.eval_difference_base (a b : ℕ) : ∃ t ≤ 100 * (a.bits.length + b.bits.length + 1), Eval signedDifference (both 0 1 a.bits b.bits) (both 0 3 (↑a - ↑b).natAbs.bits [decide (a < b)]) t

theorem Complexity.RationalHitting.StackLanguage.eval_differenceAbs (a b : ℕ) : ∃ t ≤ 200 * (a.bits.length + b.bits.length + 1), Eval differenceAbs (both 0 1 a.bits b.bits) (single 0 (↑a - ↑b).natAbs.bits) t

theorem Complexity.RationalHitting.StackLanguage.eval_differenceSign (a b : ℕ) : ∃ t ≤ 200 * (a.bits.length + b.bits.length + 1), Eval differenceSign (both 0 1 a.bits b.bits) (single 3 [decide (a < b)]) t

def Complexity.RationalHitting.StackLanguage.Procedure.differenceAbs : Procedure (pairCode Nat.bits Nat.bits) Nat.bits fun (a : ℕ × ℕ) => (↑a.1 - ↑a.2).natAbs

Compute the magnitude of the signed difference of two binary natural inputs.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RationalHitting.StackLanguage.Procedure.differenceSign : Procedure (pairCode Nat.bits Nat.bits) boolCode fun (a : ℕ × ℕ) => decide (a.1 < a.2)

Compute the sign of the difference of two binary natural inputs.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.RationalHitting.StackLanguage.Poly.natDifferenceAbs : Poly fun (a : ℕ × ℕ) => (↑a.1 - ↑a.2).natAbs

theorem Complexity.RationalHitting.StackLanguage.Poly.natLt : Poly fun (a : ℕ × ℕ) => decide (a.1 < a.2)

theorem Complexity.RationalHitting.StackLanguage.Poly.natDifference : Poly fun (a : ℕ × ℕ) => ↑a.1 - ↑a.2

theorem Complexity.RationalHitting.StackLanguage.Poly.intSign : Poly fun (a : ℤ) => decide (a < 0)

theorem Complexity.RationalHitting.StackLanguage.Poly.intAbs : Poly Int.natAbs

def Complexity.RationalHitting.StackLanguage.positivePart (z : ℤ) : ℕ

The nonnegative part of an integer, represented as a natural number.

Equations

• Complexity.RationalHitting.StackLanguage.positivePart z = if decide (z < 0) = true then 0 else z.natAbs

def Complexity.RationalHitting.StackLanguage.negativePart (z : ℤ) : ℕ

The magnitude of the negative part of an integer.

Equations

• Complexity.RationalHitting.StackLanguage.negativePart z = if decide (z < 0) = true then z.natAbs else 0

theorem Complexity.RationalHitting.StackLanguage.int_decompose (z : ℤ) : ↑(positivePart z) - ↑(negativePart z) = z

theorem Complexity.RationalHitting.StackLanguage.Poly.positivePart_poly : Poly positivePart

theorem Complexity.RationalHitting.StackLanguage.Poly.negativePart_poly : Poly negativePart

theorem Complexity.RationalHitting.StackLanguage.Poly.natCastInt : Poly fun (a : ℕ) => ↑a

theorem Complexity.RationalHitting.StackLanguage.Poly.intNeg : Poly fun (a : ℤ) => -a

theorem Complexity.RationalHitting.StackLanguage.Poly.intAdd : Poly fun (a : ℤ × ℤ) => a.1 + a.2

theorem Complexity.RationalHitting.StackLanguage.Poly.intMul : Poly fun (a : ℤ × ℤ) => a.1 * a.2

theorem Complexity.RationalHitting.StackLanguage.Poly.natZero : Poly fun (a : ℕ) => decide (a = 0)

theorem Complexity.RationalHitting.StackLanguage.Poly.intZero : Poly fun (a : ℤ) => decide (a = 0)

theorem Complexity.RationalHitting.StackLanguage.Poly.boolNot : Poly not

theorem Complexity.RationalHitting.StackLanguage.Poly.boolAnd : Poly fun (a : Bool × Bool) => a.1 && a.2

@[simp]

theorem Complexity.RationalHitting.StackLanguage.unary_code_length (n : Unary) : (code n).length = n.val

@[simp]

theorem Complexity.RationalHitting.StackLanguage.nat_code_length (n : ℕ) : (code n).length = n.bits.length

@[simp]

theorem Complexity.RationalHitting.StackLanguage.prod_code_length {A B : Type} [Coding A] [Coding B] (a : A × B) : (code a).length = 2 * (code a.1).length + 1 + (code a.2).length

theorem Complexity.RationalHitting.StackLanguage.succ_iterate (a n : ℕ) : Nat.succ^[n] a = a + n

theorem Complexity.RationalHitting.StackLanguage.bits_length_le (n : ℕ) : n.bits.length ≤ n

def Complexity.RationalHitting.StackLanguage.Procedure.unaryPred : Procedure unaryCode unaryCode Nat.pred

A clean procedure computing unary predecessor.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.RationalHitting.StackLanguage.Poly.unaryToNat : Poly Unary.val

theorem Complexity.RationalHitting.StackLanguage.Poly.unaryPred : Poly fun (a : Unary) => { val := a.val - 1 }

theorem Complexity.RationalHitting.StackLanguage.Poly.unaryZero : Poly fun (a : Unary) => decide (a.val = 0)

theorem Complexity.RationalHitting.StackLanguage.Poly.unaryLt : Poly fun (a : Unary × Unary) => decide (a.1.val < a.2.val)

theorem Complexity.RationalHitting.StackLanguage.Poly.unaryLe : Poly fun (a : Unary × Unary) => decide (a.1.val ≤ a.2.val)

theorem Complexity.RationalHitting.StackLanguage.Poly.unaryEq : Poly fun (a : Unary × Unary) => decide (a.1.val = a.2.val)

theorem Complexity.RationalHitting.StackLanguage.Poly.unaryPred_iterate (a : Unary) (n : ℕ) : (fun (a : Unary) => { val := a.val - 1 })^[n] a = { val := a.val - n }

theorem Complexity.RationalHitting.StackLanguage.Poly.unarySub : Poly fun (a : Unary × Unary) => { val := a.1.val - a.2.val }

theorem Complexity.RationalHitting.StackLanguage.int_add_bits_le (a b : ℤ) : (a + b).natAbs.bits.length ≤ a.natAbs.bits.length + b.natAbs.bits.length

theorem Complexity.RationalHitting.StackLanguage.int_mul_bits_le (a b : ℤ) : (a * b).natAbs.bits.length ≤ a.natAbs.bits.length + b.natAbs.bits.length

@[simp]

theorem Complexity.RationalHitting.StackLanguage.int_code_length (a : ℤ) : (code a).length = a.natAbs.bits.length + 3

theorem Complexity.RationalHitting.StackLanguage.powerStep_iterate (a : ℤ × ℤ) (n : ℕ) : (fun (a : ℤ × ℤ) => (a.1, a.2 * a.1))^[n] a = (a.1, a.2 * a.1 ^ n)

theorem Complexity.RationalHitting.StackLanguage.int_pow_bits_le (a : ℤ) (n : ℕ) : (a ^ n).natAbs.bits.length ≤ 1 + n * a.natAbs.bits.length

theorem Complexity.RationalHitting.StackLanguage.Poly.intPow : Poly fun (a : ℤ × Unary) => a.1 ^ a.2.val

def Complexity.RationalHitting.StackLanguage.sumStep (a : List ℤ × ℤ) : List ℤ × ℤ

Consume the head of an integer list and add it to the accumulator.

Equations

• Complexity.RationalHitting.StackLanguage.sumStep a = (a.1.tail, a.2 + a.1.headD 0)

theorem Complexity.RationalHitting.StackLanguage.sumStep_code_le (a : List ℤ × ℤ) : (code (sumStep a)).length ≤ (code a).length

theorem Complexity.RationalHitting.StackLanguage.sumStep_code_iterate_le (a : List ℤ × ℤ) (n : ℕ) : (code (sumStep^[n] a)).length ≤ (code a).length

theorem Complexity.RationalHitting.StackLanguage.sumStep_iterate_length (l : List ℤ) (z : ℤ) : sumStep^[l.length] (l, z) = ([], z + l.sum)

theorem Complexity.RationalHitting.StackLanguage.Poly.listSum : Poly List.sum