Division with remainder, in unary

Every index decomposition in an algorithmic constraint graph is a division: which edge of the original graph, which step of the walk, which copy of the gadget. This module names the unary quotients and remainders those constructions read. Each is defined as what it computes, the quotient or remainder of one length by another written as that many trues, and is polynomial-time by UnaryFn.div and UnaryFn.mod of Complexitylib.Classes.P.Unary. As for Nat, dividing by an empty divisor gives 0 and leaves the whole length as the remainder.

Main definitions

• Complexity.divFn, Complexity.modFn — a length divided by the length of a fixed divisor
• Complexity.divFn2, Complexity.modFn2 — one length divided by another, both read off a pair
• Complexity.halfFn — half a length

Main results

• Complexity.divFn_mem_FP, Complexity.modFn_mem_FP, Complexity.divFn2_mem_FP, Complexity.modFn2_mem_FP, Complexity.halfFn_mem_FP — all are polynomial-time
• Complexity.divFn_eq, Complexity.modFn_eq, Complexity.divFn2_eq, Complexity.modFn2_eq, Complexity.halfFn_eq — what they compute

Dividing by a fixed divisor

def Complexity.divFn (b s : List Bool) : List Bool

The quotient of a length by the length of a fixed divisor, in unary.

Equations

• Complexity.divFn b s = List.replicate (s.length / b.length) true

def Complexity.modFn (b s : List Bool) : List Bool

The remainder of a length by the length of a fixed divisor, in unary.

Equations

• Complexity.modFn b s = List.replicate (s.length % b.length) true

theorem Complexity.divFn_eq {b : List Bool} (s : List Bool) : divFn b s = List.replicate (s.length / b.length) true

theorem Complexity.modFn_eq {b : List Bool} (s : List Bool) : modFn b s = List.replicate (s.length % b.length) true

theorem Complexity.divFn_mem_FP (b : List Bool) : divFn b ∈ FP

theorem Complexity.modFn_mem_FP (b : List Bool) : modFn b ∈ FP

Dividing by a length read from the input

def Complexity.divFn2 (z : List Bool) : List Bool

The quotient of one length by another, in unary, on pair b s.

Equations

• Complexity.divFn2 z = List.replicate ((Complexity.pairSnd z).length / (Complexity.pairFst z).length) true

def Complexity.modFn2 (z : List Bool) : List Bool

The remainder of one length by another, in unary, on pair b s.

Equations

• Complexity.modFn2 z = List.replicate ((Complexity.pairSnd z).length % (Complexity.pairFst z).length) true

theorem Complexity.divFn2_eq {b : List Bool} (s : List Bool) : divFn2 (pair b s) = List.replicate (s.length / b.length) true

theorem Complexity.modFn2_eq {b : List Bool} (s : List Bool) : modFn2 (pair b s) = List.replicate (s.length % b.length) true

theorem Complexity.divFn2_mem_FP : divFn2 ∈ FP

theorem Complexity.modFn2_mem_FP : modFn2 ∈ FP

Halving

def Complexity.halfFn (s : List Bool) : List Bool

Halving a length, in unary.

Equations

• Complexity.halfFn s = List.replicate (s.length / 2) true

theorem Complexity.halfFn_mem_FP : halfFn ∈ FP

theorem Complexity.halfFn_eq (s : List Bool) : halfFn s = List.replicate (s.length / 2) true