Boolean partial assignments

A partial assignment records, for each named Boolean variable, either a fixed value or a live variable. Restricted functions retain the original input indexing: values supplied at fixed coordinates are ignored. This representation is convenient for random restrictions and decision trees, while conversion to InputSubstitution connects it to the library's existing semantic interface.

Sequential refinement is left-biased. In rho.refine sigma, assignments already fixed by rho remain fixed, and sigma is consulted only at variables left live by rho.

@[reducible, inline]

abbrev Algebraic.PartialAssignment (n : ℕ) : Type

A Boolean restriction on n named variables. none means that a variable is live; some value fixes it to value.

Equations

• Algebraic.PartialAssignment n = (Fin n → Option Bool)

theorem Algebraic.PartialAssignment.ext {n : ℕ} {rho sigma : PartialAssignment n} (equal : ∀ (index : Fin n), rho index = sigma index) : rho = sigma

Two partial assignments are equal when they agree on every variable.

def Algebraic.PartialAssignment.empty {n : ℕ} : PartialAssignment n

The empty partial assignment leaves every variable live.

Equations

• Algebraic.PartialAssignment.empty x✝ = none

def Algebraic.PartialAssignment.total {n : ℕ} (input : Fin n → Bool) : PartialAssignment n

A total assignment fixes every variable.

Equations

• Algebraic.PartialAssignment.total input index = some (input index)

def Algebraic.PartialAssignment.fix {n : ℕ} (selected : Fin n) (value : Bool) : PartialAssignment n

The partial assignment fixing exactly one variable.

Equations

• Algebraic.PartialAssignment.fix selected value index = if index = selected then some value else none

@[simp]

theorem Algebraic.PartialAssignment.empty_apply {n : ℕ} (index : Fin n) : empty index = none

@[simp]

theorem Algebraic.PartialAssignment.total_apply {n : ℕ} (input : Fin n → Bool) (index : Fin n) : total input index = some (input index)

@[simp]

theorem Algebraic.PartialAssignment.fix_selected {n : ℕ} (selected : Fin n) (value : Bool) : fix selected value selected = some value

@[simp]

theorem Algebraic.PartialAssignment.fix_other {n : ℕ} (selected index : Fin n) (value : Bool) (different : index ≠ selected) : fix selected value index = none

def Algebraic.PartialAssignment.apply {n : ℕ} (rho : PartialAssignment n) (input : Fin n → Bool) : Fin n → Bool

Apply a partial assignment to a complete input. Values at fixed variables are overwritten, while values at live variables are retained.

Equations

• rho.apply input index = (rho index).getD (input index)

@[simp]

theorem Algebraic.PartialAssignment.apply_of_live {n : ℕ} (rho : PartialAssignment n) (input : Fin n → Bool) {index : Fin n} (live : rho index = none) : rho.apply input index = input index

@[simp]

theorem Algebraic.PartialAssignment.apply_of_fixed {n : ℕ} (rho : PartialAssignment n) (input : Fin n → Bool) {index : Fin n} {value : Bool} (fixed : rho index = some value) : rho.apply input index = value

@[simp]

theorem Algebraic.PartialAssignment.apply_empty {n : ℕ} (input : Fin n → Bool) : empty.apply input = input

@[simp]

theorem Algebraic.PartialAssignment.apply_total {n : ℕ} (fixed input : Fin n → Bool) : (total fixed).apply input = fixed

theorem Algebraic.PartialAssignment.apply_fix_eq_self {n : ℕ} (input : Fin n → Bool) (selected : Fin n) (value : Bool) (selectedValue : input selected = value) : (fix selected value).apply input = input

Fixing a variable to the value it already has leaves a complete input unchanged.

def Algebraic.PartialAssignment.refine {n : ℕ} (rho sigma : PartialAssignment n) : PartialAssignment n

Refine rho with sigma, retaining every value already fixed by rho.

Equations

• rho.refine sigma index = match rho index with | some value => some value | none => sigma index

def Algebraic.PartialAssignment.clear {n : ℕ} (rho : PartialAssignment n) (coordinates : Finset (Fin n)) : PartialAssignment n

Clear a designated finite set of coordinates, leaving every other value unchanged. This is the inverse operation used by refinement encodings once their newly fixed support has been reconstructed.

Equations

• rho.clear coordinates index = if index ∈ coordinates then none else rho index

@[simp]

theorem Algebraic.PartialAssignment.clear_of_mem {n : ℕ} (rho : PartialAssignment n) (coordinates : Finset (Fin n)) {index : Fin n} (present : index ∈ coordinates) : rho.clear coordinates index = none

@[simp]

theorem Algebraic.PartialAssignment.clear_of_not_mem {n : ℕ} (rho : PartialAssignment n) (coordinates : Finset (Fin n)) {index : Fin n} (absent : index ∉ coordinates) : rho.clear coordinates index = rho index

@[simp]

theorem Algebraic.PartialAssignment.empty_refine {n : ℕ} (rho : PartialAssignment n) : empty.refine rho = rho

@[simp]

theorem Algebraic.PartialAssignment.refine_empty {n : ℕ} (rho : PartialAssignment n) : rho.refine empty = rho

theorem Algebraic.PartialAssignment.apply_refine {n : ℕ} (rho sigma : PartialAssignment n) (input : Fin n → Bool) : (rho.refine sigma).apply input = rho.apply (sigma.apply input)

Applying a sequential refinement is function composition on inputs.

theorem Algebraic.PartialAssignment.refine_assoc {n : ℕ} (rho sigma tau : PartialAssignment n) : (rho.refine sigma).refine tau = rho.refine (sigma.refine tau)

Sequential refinement is associative.

theorem Algebraic.PartialAssignment.fix_refine_refine_fix {n : ℕ} (rho tail : PartialAssignment n) (selected : Fin n) (pathValue satisfyingValue : Bool) (live : rho selected = none) : (fix selected pathValue).refine (rho.refine ((fix selected satisfyingValue).refine tail)) = (rho.refine (fix selected pathValue)).refine tail

Replacing the freshly assigned head coordinate by a path value commutes with retaining the rest of a refinement. The selected coordinate must be live in the original restriction.

def Algebraic.PartialAssignment.toInputSubstitution {n : ℕ} (rho : PartialAssignment n) : InputSubstitution Bool n n

View a partial assignment as a semantic input substitution on the same named variables.

Equations

• rho.toInputSubstitution index input = rho.apply input index

@[simp]

theorem Algebraic.PartialAssignment.toInputSubstitution_apply {n : ℕ} (rho : PartialAssignment n) (input : Fin n → Bool) : rho.toInputSubstitution.apply input = rho.apply input

@[simp]

theorem Algebraic.PartialAssignment.toInputSubstitution_empty {n : ℕ} : empty.toInputSubstitution = InputSubstitution.id

theorem Algebraic.PartialAssignment.toInputSubstitution_refine {n : ℕ} (rho sigma : PartialAssignment n) : (rho.refine sigma).toInputSubstitution = rho.toInputSubstitution.comp sigma.toInputSubstitution

Conversion to input substitutions preserves sequential composition.

def Algebraic.PartialAssignment.liveVariables {n : ℕ} (rho : PartialAssignment n) : Finset (Fin n)

The finite set of variables left live by a partial assignment.

Equations

• rho.liveVariables = {index : Fin n | rho index = none}

@[simp]

theorem Algebraic.PartialAssignment.mem_liveVariables {n : ℕ} (rho : PartialAssignment n) (index : Fin n) : index ∈ rho.liveVariables ↔ rho index = none

def Algebraic.PartialAssignment.liveCount {n : ℕ} (rho : PartialAssignment n) : ℕ

The number of variables left live by a partial assignment.

Equations

• rho.liveCount = rho.liveVariables.card

noncomputable def Algebraic.PartialAssignment.liveOrderIso {n : ℕ} (rho : PartialAssignment n) : Fin rho.liveCount ≃o ↥rho.liveVariables

The increasing bijection from a compact input namespace to the variables left live by a partial assignment.

Equations

• rho.liveOrderIso = rho.liveVariables.orderIsoOfFin ⋯

noncomputable def Algebraic.PartialAssignment.liveVariable {n : ℕ} (rho : PartialAssignment n) : Fin rho.liveCount → Fin n

The original input coordinate represented by a compact live-input index.

Equations

• rho.liveVariable index = ↑(rho.liveOrderIso index)

theorem Algebraic.PartialAssignment.liveVariable_mem {n : ℕ} (rho : PartialAssignment n) (index : Fin rho.liveCount) : rho.liveVariable index ∈ rho.liveVariables

theorem Algebraic.PartialAssignment.liveVariable_isLive {n : ℕ} (rho : PartialAssignment n) (index : Fin rho.liveCount) : rho (rho.liveVariable index) = none

noncomputable def Algebraic.PartialAssignment.liveIndex {n : ℕ} (rho : PartialAssignment n) (index : Fin n) (live : rho index = none) : Fin rho.liveCount

The compact index of an original coordinate known to be live.

Equations

• rho.liveIndex index live = rho.liveOrderIso.symm ⟨index, ⋯⟩

@[simp]

theorem Algebraic.PartialAssignment.liveVariable_liveIndex {n : ℕ} (rho : PartialAssignment n) (index : Fin n) (live : rho index = none) : rho.liveVariable (rho.liveIndex index live) = index

@[simp]

theorem Algebraic.PartialAssignment.liveIndex_liveVariable {n : ℕ} (rho : PartialAssignment n) (index : Fin rho.liveCount) : rho.liveIndex (rho.liveVariable index) ⋯ = index

noncomputable def Algebraic.PartialAssignment.projectLive {n : ℕ} (rho : PartialAssignment n) (input : Fin n → Bool) : Fin rho.liveCount → Bool

Read a complete input only at the coordinates left live by rho.

Equations

• rho.projectLive input index = input (rho.liveVariable index)

noncomputable def Algebraic.PartialAssignment.toLiveInputSubstitution {n : ℕ} (rho : PartialAssignment n) : InputSubstitution Bool n rho.liveCount

Express every original input as either a fixed Boolean or one of the compactly reindexed live inputs.

Equations

• rho.toLiveInputSubstitution index input = if live : rho index = none then input (rho.liveIndex index live) else (rho index).getD false

@[simp]

theorem Algebraic.PartialAssignment.toLiveInputSubstitution_of_fixed {n : ℕ} (rho : PartialAssignment n) (input : Fin rho.liveCount → Bool) {index : Fin n} {value : Bool} (fixed : rho index = some value) : rho.toLiveInputSubstitution.apply input index = value

@[simp]

theorem Algebraic.PartialAssignment.toLiveInputSubstitution_liveVariable {n : ℕ} (rho : PartialAssignment n) (input : Fin rho.liveCount → Bool) (index : Fin rho.liveCount) : rho.toLiveInputSubstitution.apply input (rho.liveVariable index) = input index

theorem Algebraic.PartialAssignment.toLiveInputSubstitution_projectLive {n : ℕ} (rho : PartialAssignment n) (input : Fin n → Bool) : rho.toLiveInputSubstitution.apply (rho.projectLive input) = rho.apply input

Projecting a complete input to its live coordinates and then restoring fixed coordinates is exactly ordinary application of the restriction.

@[simp]

theorem Algebraic.PartialAssignment.projectLive_toLiveInputSubstitution {n : ℕ} (rho : PartialAssignment n) (input : Fin rho.liveCount → Bool) : rho.projectLive (rho.toLiveInputSubstitution.apply input) = input

Compact live inputs are recovered after restoring the original input namespace.

def Algebraic.PartialAssignment.fixedVariables {n : ℕ} (rho : PartialAssignment n) : Finset (Fin n)

The finite set of variables fixed by a partial assignment.

Equations

• rho.fixedVariables = {index : Fin n | rho index ≠ none}

@[simp]

theorem Algebraic.PartialAssignment.mem_fixedVariables {n : ℕ} (rho : PartialAssignment n) (index : Fin n) : index ∈ rho.fixedVariables ↔ rho index ≠ none

def Algebraic.PartialAssignment.fixedCount {n : ℕ} (rho : PartialAssignment n) : ℕ

The number of variables fixed by a partial assignment.

Equations

• rho.fixedCount = rho.fixedVariables.card

@[simp]

theorem Algebraic.PartialAssignment.liveVariables_empty {n : ℕ} : empty.liveVariables = Finset.univ

@[simp]

theorem Algebraic.PartialAssignment.liveCount_empty {n : ℕ} : empty.liveCount = n

@[simp]

theorem Algebraic.PartialAssignment.fixedVariables_empty {n : ℕ} : empty.fixedVariables = ∅

@[simp]

theorem Algebraic.PartialAssignment.fixedCount_empty {n : ℕ} : empty.fixedCount = 0

@[simp]

theorem Algebraic.PartialAssignment.liveVariables_total {n : ℕ} (input : Fin n → Bool) : (total input).liveVariables = ∅

@[simp]

theorem Algebraic.PartialAssignment.liveCount_total {n : ℕ} (input : Fin n → Bool) : (total input).liveCount = 0

@[simp]

theorem Algebraic.PartialAssignment.fixedVariables_total {n : ℕ} (input : Fin n → Bool) : (total input).fixedVariables = Finset.univ

@[simp]

theorem Algebraic.PartialAssignment.fixedCount_total {n : ℕ} (input : Fin n → Bool) : (total input).fixedCount = n

theorem Algebraic.PartialAssignment.liveVariables_union_fixedVariables {n : ℕ} (rho : PartialAssignment n) : rho.liveVariables ∪ rho.fixedVariables = Finset.univ

Every variable is either live or fixed, but not both.

theorem Algebraic.PartialAssignment.disjoint_liveVariables_fixedVariables {n : ℕ} (rho : PartialAssignment n) : Disjoint rho.liveVariables rho.fixedVariables

The live and fixed variable sets are disjoint.

theorem Algebraic.PartialAssignment.liveCount_add_fixedCount {n : ℕ} (rho : PartialAssignment n) : rho.liveCount + rho.fixedCount = n

Live and fixed variables partition the input coordinates exactly.

theorem Algebraic.PartialAssignment.liveVariables_fix {n : ℕ} (selected : Fin n) (value : Bool) : (fix selected value).liveVariables = Finset.univ.erase selected

Fixing one variable removes exactly that variable from the live set.

theorem Algebraic.PartialAssignment.fixedVariables_fix {n : ℕ} (selected : Fin n) (value : Bool) : (fix selected value).fixedVariables = {selected}

A one-variable assignment fixes exactly its selected coordinate.

theorem Algebraic.PartialAssignment.liveVariables_refine {n : ℕ} (rho sigma : PartialAssignment n) : (rho.refine sigma).liveVariables = rho.liveVariables ∩ sigma.liveVariables

The live variables after sequential refinement are the variables left live by both constituent partial assignments.

theorem Algebraic.PartialAssignment.fixedVariables_refine {n : ℕ} (rho sigma : PartialAssignment n) : (rho.refine sigma).fixedVariables = rho.fixedVariables ∪ sigma.fixedVariables

The variables fixed by a sequential refinement are exactly those fixed by either constituent assignment.

theorem Algebraic.PartialAssignment.liveCount_refine_le_left {n : ℕ} (rho sigma : PartialAssignment n) : (rho.refine sigma).liveCount ≤ rho.liveCount

Sequential refinement cannot increase the number of live variables.

theorem Algebraic.PartialAssignment.liveVariables_refine_fix {n : ℕ} (rho : PartialAssignment n) (selected : Fin n) (value : Bool) : (rho.refine (fix selected value)).liveVariables = rho.liveVariables.erase selected

Refining by a one-variable assignment removes exactly that variable from the live set. If it was already fixed, the set is unchanged.

theorem Algebraic.PartialAssignment.liveCount_refine_fix_lt_of_live {n : ℕ} (rho : PartialAssignment n) (selected : Fin n) (value : Bool) (live : rho selected = none) : (rho.refine (fix selected value)).liveCount < rho.liveCount

Fixing a currently live variable strictly decreases the live count.

theorem Algebraic.PartialAssignment.fixedCount_refine_eq_add {n : ℕ} (rho sigma : PartialAssignment n) (newFixes : sigma.fixedVariables ⊆ rho.liveVariables) : (rho.refine sigma).fixedCount = rho.fixedCount + sigma.fixedCount

If the second assignment fixes only variables left live by the first, their fixed-variable counts add under refinement.

theorem Algebraic.PartialAssignment.clear_refine_fixedVariables {n : ℕ} (rho extension : PartialAssignment n) (newFixes : extension.fixedVariables ⊆ rho.liveVariables) : (rho.refine extension).clear extension.fixedVariables = rho

Clearing exactly the support added by a refinement recovers the original restriction, provided the refinement fixed only previously live variables.

theorem Algebraic.PartialAssignment.liveCount_refine_add_fixedCount_eq {n : ℕ} (rho sigma : PartialAssignment n) (newFixes : sigma.fixedVariables ⊆ rho.liveVariables) : (rho.refine sigma).liveCount + sigma.fixedCount = rho.liveCount

Under a refinement that fixes only live variables, the decrease in live count is exactly the second assignment's fixed count.

theorem Algebraic.PartialAssignment.apply_eq_of_agree_live {n : ℕ} (rho : PartialAssignment n) {left right : Fin n → Bool} (agree : ∀ index ∈ rho.liveVariables, left index = right index) : rho.apply left = rho.apply right

Inputs that agree on every live variable become equal after applying the partial assignment.

def Algebraic.ScalarFunction.restrict {n : ℕ} (function : ScalarFunction Bool n) (rho : PartialAssignment n) : ScalarFunction Bool n

Restrict a scalar Boolean function by a partial assignment.

Equations

• function.restrict rho input = function (rho.apply input)

@[simp]

theorem Algebraic.ScalarFunction.restrict_apply {n : ℕ} (function : ScalarFunction Bool n) (rho : PartialAssignment n) (input : Fin n → Bool) : function.restrict rho input = function (rho.apply input)

@[simp]

theorem Algebraic.ScalarFunction.restrict_empty {n : ℕ} (function : ScalarFunction Bool n) : function.restrict PartialAssignment.empty = function

theorem Algebraic.ScalarFunction.restrict_refine {n : ℕ} (function : ScalarFunction Bool n) (rho sigma : PartialAssignment n) : (function.restrict rho).restrict sigma = function.restrict (rho.refine sigma)

Restricting twice agrees with restriction by sequential refinement.

theorem Algebraic.ScalarFunction.restrict_dependsOnlyOn_live {n : ℕ} (function : ScalarFunction Bool n) (rho : PartialAssignment n) : DependsOnlyOn (function.restrict rho) rho.liveVariables

A restricted scalar function depends only on variables left live.

def Algebraic.Target.restrict {n m : ℕ} (target : Target Bool n m) (rho : PartialAssignment n) : Target Bool n m

Restrict every output of a Boolean target by a partial assignment.

Equations

• target.restrict rho = target.substitute rho.toInputSubstitution

@[simp]

theorem Algebraic.Target.restrict_apply {n m : ℕ} (target : Target Bool n m) (rho : PartialAssignment n) (input : Fin n → Bool) : target.restrict rho input = target (rho.apply input)

@[simp]

theorem Algebraic.Target.restrict_empty {n m : ℕ} (target : Target Bool n m) : target.restrict PartialAssignment.empty = target

theorem Algebraic.Target.restrict_refine {n m : ℕ} (target : Target Bool n m) (rho sigma : PartialAssignment n) : (target.restrict rho).restrict sigma = target.restrict (rho.refine sigma)

Restricting a target twice agrees with sequential refinement.

theorem Algebraic.Target.restrict_dependsOnlyOn_live {n m : ℕ} (target : Target Bool n m) (rho : PartialAssignment n) : DependsOnlyOn (target.restrict rho) rho.liveVariables

A restricted target depends only on variables left live.