Rational hitting lists: rational arithmetic

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/RationalArithmetic.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.chooseClean : Program (Fin 18)

Compute a binomial coefficient and clear its input registers.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.eval_chooseClean (n k : ℕ) : ∃ t ≤ 4000000 * (n + k + 1) ^ 10, Eval chooseClean (both 14 15 (unaryCode n) (unaryCode k)) (single 0 (n.choose k).bits) t

def Complexity.RationalHitting.StackLanguage.Procedure.choose : Procedure (pairCode unaryCode unaryCode) Nat.bits fun (a : ℕ × ℕ) => a.1.choose a.2

Compute the binomial coefficient of two unary arguments.

Equations

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

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

def Complexity.RationalHitting.StackLanguage.unpackInt {K : Type} (a sg : K) : Program K

Separate the sign from an encoded integer magnitude.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.eval_unpackInt {K : Type} [DecidableEq K] {a sg : K} (has : a ≠ sg) (s : Store K) (z : ℤ) (hz : s a = intCode z) : Eval (unpackInt a sg) s (Function.update (Function.update s a z.natAbs.bits) sg (decide (z < 0) :: s sg)) 5

def Complexity.RationalHitting.StackLanguage.rationalClean : Program (Fin 16)

Encode a rational quotient and clean its temporary sign registers.

Equations

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

@[reducible, inline]

abbrev Complexity.RationalHitting.StackLanguage.NZInt : Type

A nonzero integer used as a rational denominator.

Equations

• Complexity.RationalHitting.StackLanguage.NZInt = { z : ℤ // z ≠ 0 }

theorem Complexity.RationalHitting.StackLanguage.eval_rationalClean (a : ℤ) (b : NZInt) : ∃ t ≤ 4000 * (a.natAbs.bits.length + (↑b).natAbs.bits.length + 8) ^ 3, Eval rationalClean (both 0 5 (intCode a) (intCode ↑b)) (single 14 (encodeRat (Rat.divInt a ↑b))) t

def Complexity.RationalHitting.StackLanguage.Procedure.rationalEncode : Procedure (pairCode intCode fun (b : NZInt) => intCode ↑b) (fun (x : List Bool) => x) fun (a : ℤ × NZInt) => encodeRat (Rat.divInt a.1 ↑a.2)

A polynomially bounded procedure producing the canonical rational encoding.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.Poly.rationalEncodeNZ : Poly fun (a : ℤ × NZInt) => { val := encodeRat (Rat.divInt a.1 ↑a.2) }

theorem Complexity.RationalHitting.StackLanguage.Poly.safeDen : Poly fun (b : ℤ) => ⟨if b = 0 then 1 else b, ⋯⟩

theorem Complexity.RationalHitting.StackLanguage.Poly.rationalEncode : Poly fun (a : ℤ × ℤ) => { val := encodeRat (Rat.divInt a.1 a.2) }

theorem Complexity.RationalHitting.StackLanguage.Poly.unaryEta {A : Type} [Coding A] {f : A → Unary} (hf : Poly f) : Poly fun (a : A) => { val := (f a).val }

theorem Complexity.RationalHitting.StackLanguage.Poly.unaryAddFun {A : Type} [Coding A] {f g : A → ℕ} (hf : Poly fun (a : A) => { val := f a }) (hg : Poly fun (a : A) => { val := g a }) : Poly fun (a : A) => { val := f a + g a }

theorem Complexity.RationalHitting.StackLanguage.Poly.unarySubFun {A : Type} [Coding A] {f g : A → ℕ} (hf : Poly fun (a : A) => { val := f a }) (hg : Poly fun (a : A) => { val := g a }) : Poly fun (a : A) => { val := f a - g a }

theorem Complexity.RationalHitting.StackLanguage.Poly.unaryMulFun {A : Type} [Coding A] {f g : A → ℕ} (hf : Poly fun (a : A) => { val := f a }) (hg : Poly fun (a : A) => { val := g a }) : Poly fun (a : A) => { val := f a * g a }

theorem Complexity.RationalHitting.StackLanguage.Poly.unaryDivFun {A : Type} [Coding A] {f g : A → ℕ} (hf : Poly fun (a : A) => { val := f a }) (hg : Poly fun (a : A) => { val := g a }) : Poly fun (a : A) => { val := f a / g a }

theorem Complexity.RationalHitting.StackLanguage.Poly.unaryModFun {A : Type} [Coding A] {f g : A → ℕ} (hf : Poly fun (a : A) => { val := f a }) (hg : Poly fun (a : A) => { val := g a }) : Poly fun (a : A) => { val := f a % g a }

theorem Complexity.RationalHitting.StackLanguage.Poly.unaryPowFun {A : Type} [Coding A] {f : A → ℕ} (k : ℕ) (hf : Poly fun (a : A) => { val := f a }) : Poly fun (a : A) => { val := f a ^ k }

theorem Complexity.RationalHitting.StackLanguage.Poly.unaryCastInt : Poly fun (a : Unary) => ↑a.val

theorem Complexity.RationalHitting.StackLanguage.Poly.unaryCastIntFun {A : Type} [Coding A] {f : A → ℕ} (hf : Poly fun (a : A) => { val := f a }) : Poly fun (a : A) => ↑(f a)

theorem Complexity.RationalHitting.StackLanguage.Poly.unaryEqFun {A : Type} [Coding A] {f g : A → ℕ} (hf : Poly fun (a : A) => { val := f a }) (hg : Poly fun (a : A) => { val := g a }) : Poly fun (a : A) => decide (f a = g a)

theorem Complexity.RationalHitting.StackLanguage.Poly.unaryLtFun {A : Type} [Coding A] {f g : A → ℕ} (hf : Poly fun (a : A) => { val := f a }) (hg : Poly fun (a : A) => { val := g a }) : Poly fun (a : A) => decide (f a < g a)

theorem Complexity.RationalHitting.StackLanguage.Poly.chooseFun {A : Type} [Coding A] {f g : A → ℕ} (hf : Poly fun (a : A) => { val := f a }) (hg : Poly fun (a : A) => { val := g a }) : Poly fun (a : A) => (f a).choose (g a)

theorem Complexity.RationalHitting.StackLanguage.Poly.intPowFun {A : Type} [Coding A] {f : A → ℤ} {g : A → ℕ} (hf : Poly f) (hg : Poly fun (a : A) => { val := g a }) : Poly fun (a : A) => f a ^ g a

theorem Complexity.RationalHitting.StackLanguage.Poly.ite {A B : Type} [Coding A] [Coding B] {c : A → Prop} [DecidablePred c] {f g : A → B} (hc : Poly fun (a : A) => decide (c a)) (hf : Poly f) (hg : Poly g) : Poly fun (a : A) => if c a then f a else g a

theorem Complexity.RationalHitting.StackLanguage.Poly.sumUp {A : Type} [Coding A] {n : A → ℕ} {f : A × Unary → ℤ} (hn : Poly fun (a : A) => { val := n a }) (hf : Poly f) : Poly fun (a : A) => (List.map (fun (i : ℕ) => f (a, { val := i })) (List.range (n a))).sum

@[instance_reducible]

instance Complexity.RationalHitting.StackLanguage.Unary.instOfNat (n : ℕ) : OfNat Unary n

Equations

• Complexity.RationalHitting.StackLanguage.Unary.instOfNat n = { ofNat := { val := n } }

@[instance_reducible]

instance Complexity.RationalHitting.StackLanguage.Unary.instAdd : Add Unary

Equations

• Complexity.RationalHitting.StackLanguage.Unary.instAdd = { add := fun (a b : Complexity.RationalHitting.StackLanguage.Unary) => { val := a.val + b.val } }

@[instance_reducible]

instance Complexity.RationalHitting.StackLanguage.Unary.instSub : Sub Unary

Equations

• Complexity.RationalHitting.StackLanguage.Unary.instSub = { sub := fun (a b : Complexity.RationalHitting.StackLanguage.Unary) => { val := a.val - b.val } }

@[instance_reducible]

instance Complexity.RationalHitting.StackLanguage.Unary.instMul : Mul Unary

Equations

• Complexity.RationalHitting.StackLanguage.Unary.instMul = { mul := fun (a b : Complexity.RationalHitting.StackLanguage.Unary) => { val := a.val * b.val } }

@[instance_reducible]

instance Complexity.RationalHitting.StackLanguage.Unary.instDiv : Div Unary

Equations

• Complexity.RationalHitting.StackLanguage.Unary.instDiv = { div := fun (a b : Complexity.RationalHitting.StackLanguage.Unary) => { val := a.val / b.val } }

@[instance_reducible]

instance Complexity.RationalHitting.StackLanguage.Unary.instMod : Mod Unary

Equations

• Complexity.RationalHitting.StackLanguage.Unary.instMod = { mod := fun (a b : Complexity.RationalHitting.StackLanguage.Unary) => { val := a.val % b.val } }

@[instance_reducible]

instance Complexity.RationalHitting.StackLanguage.Unary.instPowNat : Pow Unary ℕ

Equations

• Complexity.RationalHitting.StackLanguage.Unary.instPowNat = { pow := fun (a : Complexity.RationalHitting.StackLanguage.Unary) (b : ℕ) => { val := a.val ^ b } }

def Complexity.RationalHitting.StackLanguage.Unary.toInt (a : Unary) : ℤ

Interpret a unary natural number as an integer.

Equations

• a.toInt = ↑a.val

def Complexity.RationalHitting.StackLanguage.Unary.choose (a b : Unary) : ℤ

Compute the binomial coefficient of two unary arguments.

Equations

• a.choose b = ↑(a.val.choose b.val)

def Complexity.RationalHitting.StackLanguage.Unary.powInt (a : ℤ) (b : Unary) : ℤ

Raise an integer to a unary exponent.

Equations

• Complexity.RationalHitting.StackLanguage.Unary.powInt a b = a ^ b.val

def Complexity.RationalHitting.StackLanguage.Unary.eqb (a b : Unary) : Bool

Test equality of unary natural numbers.

Equations

• a.eqb b = decide (a.val = b.val)

def Complexity.RationalHitting.StackLanguage.Unary.ltb (a b : Unary) : Bool

Test strict comparison of unary natural numbers.

Equations

• a.ltb b = decide (a.val < b.val)

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

theorem Complexity.RationalHitting.StackLanguage.Poly.uSub : Poly fun (a : Unary × Unary) => a.1 - a.2

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

theorem Complexity.RationalHitting.StackLanguage.Poly.uDiv : Poly fun (a : Unary × Unary) => a.1 / a.2

theorem Complexity.RationalHitting.StackLanguage.Poly.uMod : Poly fun (a : Unary × Unary) => a.1 % a.2

theorem Complexity.RationalHitting.StackLanguage.Poly.uPow (k : ℕ) : Poly fun (a : Unary) => a ^ k

theorem Complexity.RationalHitting.StackLanguage.Poly.uInt : Poly Unary.toInt

theorem Complexity.RationalHitting.StackLanguage.Poly.uChoose : Poly fun (a : Unary × Unary) => a.1.choose a.2

theorem Complexity.RationalHitting.StackLanguage.Poly.uPowInt : Poly fun (a : ℤ × Unary) => Unary.powInt a.1 a.2

theorem Complexity.RationalHitting.StackLanguage.Poly.uEq : Poly fun (a : Unary × Unary) => a.1.eqb a.2

theorem Complexity.RationalHitting.StackLanguage.Poly.uLt : Poly fun (a : Unary × Unary) => a.1.ltb a.2