Finite values and conditions within a fixed workspace budget

These fun_prop rules extend those of InSpace.FunProp to values of finite types. A function of a value of a finite type (budget_finite) costs no workspace beyond the value. Conditions may be decidable propositions (budget_iteProp), their negations (budget_decideNot), equalities on a finite type (budget_decideEq) or Boolean connectives.

The rules reach fun_prop only where this module is imported, directly or through CslibFrontier.Tactic.Space. A direct fun_prop client that needs them imports this module.

The intermediate encoding of budget_finite and budget_decideEq is not determined by the goal. When no premise determines it, as for a finite function of a component of a finite value, budget_finite_encFinite and budget_decideEq_encFinite pass through the canonical encoding encFinite. Such a value used as a component of the argument of another finite function, as in g ((r x).opp, b x), still needs its encoding stated, for example have := budget_finite (encC := encFinEnum Guard) Ref.guardOf hr.

budget_decideEq_encFinite, conjunctions and disjunctions (budget_decideAnd, budget_decideOr) and comparisons ≤ of numbers (budget_natLe) are not registered: each would be tried, and fail, on every decidable condition, which doubles the search on small certificates. The space tactic adds them when a first search without them fails; a direct fun_prop client can use attribute [local fun_prop].

Main results

• budget_iteProp, budget_decideNot, budget_decideEq: decidable conditions within the budget.
• budget_finite_encFinite: a function of a finite value, through its canonical encoding.
• budget_decideEq_encFinite, budget_decideAnd, budget_decideOr, budget_natLe: further conditions, which space tries after the registered rules.
• budget_boolNot, budget_boolAnd, budget_boolOr: Boolean connectives within the budget.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_iteProp {α β : Type} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {Bs : α → ℕ} {p : α → Prop} [DecidablePred p] {f g : α → β} (hc : ComputableInSpace (fun (x : α) => decide (p x)) encIn encBool Bs) (hf : ComputableInSpace f encIn encB Bs) (hg : ComputableInSpace g encIn encB Bs) : ComputableInSpace (fun (x : α) => if p x then f x else g x) encIn encB Bs

A conditional on a decidable proposition, within the budget.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_decideNot {α : Type} {encIn : α ↪ List Bool} {Bs : α → ℕ} {p : α → Prop} [DecidablePred p] (hp : ComputableInSpace (fun (x : α) => decide (p x)) encIn encBool Bs) : ComputableInSpace (fun (x : α) => decide ¬p x) encIn encBool Bs

The negation of a decidable proposition, within the budget. This covers ≠ conditions.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_decideEq {α β : Type} {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {Bs : α → ℕ} [Finite β] [DecidableEq β] {f g : α → β} (hf : ComputableInSpace f encIn encB Bs) (hg : ComputableInSpace g encIn encB Bs) : ComputableInSpace (fun (x : α) => decide (f x = g x)) encIn encBool Bs

Equality of two values of a finite type, within the budget.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_boolNot {α : Type} {encIn : α ↪ List Bool} {Bs : α → ℕ} {a : α → Bool} (ha : ComputableInSpace a encIn encBool Bs) : ComputableInSpace (fun (x : α) => !a x) encIn encBool Bs

The negation of a Boolean, within the budget.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_boolAnd {α : Type} {encIn : α ↪ List Bool} {Bs : α → ℕ} {a b : α → Bool} (ha : ComputableInSpace a encIn encBool Bs) (hb : ComputableInSpace b encIn encBool Bs) : ComputableInSpace (fun (x : α) => a x && b x) encIn encBool Bs

The conjunction of two Booleans, within the budget.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_boolOr {α : Type} {encIn : α ↪ List Bool} {Bs : α → ℕ} {a b : α → Bool} (ha : ComputableInSpace a encIn encBool Bs) (hb : ComputableInSpace b encIn encBool Bs) : ComputableInSpace (fun (x : α) => a x || b x) encIn encBool Bs

The disjunction of two Booleans, within the budget.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_finite_encFinite {α β γ : Type} {encIn : α ↪ List Bool} {encC : γ ↪ List Bool} {Bs : α → ℕ} {f : α → β} [Finite β] (g : β → γ) (hf : ComputableInSpace f encIn (encFinite β) Bs) : ComputableInSpace (fun (x : α) => g (f x)) encIn encC Bs

A function of a value of a finite type, through the canonical encoding of the value.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_decideEq_encFinite {α β : Type} {encIn : α ↪ List Bool} {Bs : α → ℕ} [Finite β] [DecidableEq β] {f g : α → β} (hf : ComputableInSpace f encIn (encFinite β) Bs) (hg : ComputableInSpace g encIn (encFinite β) Bs) : ComputableInSpace (fun (x : α) => decide (f x = g x)) encIn encBool Bs

Equality of two values of a finite type, through the canonical encoding of the type. Not registered with fun_prop; space tries it after the registered rules.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_decideAnd {α : Type} {encIn : α ↪ List Bool} {Bs : α → ℕ} {p q : α → Prop} [DecidablePred p] [DecidablePred q] (hp : ComputableInSpace (fun (x : α) => decide (p x)) encIn encBool Bs) (hq : ComputableInSpace (fun (x : α) => decide (q x)) encIn encBool Bs) : ComputableInSpace (fun (x : α) => decide (p x ∧ q x)) encIn encBool Bs

The conjunction of two decidable propositions, within the budget. Not registered with fun_prop; space tries it after the registered rules.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_decideOr {α : Type} {encIn : α ↪ List Bool} {Bs : α → ℕ} {p q : α → Prop} [DecidablePred p] [DecidablePred q] (hp : ComputableInSpace (fun (x : α) => decide (p x)) encIn encBool Bs) (hq : ComputableInSpace (fun (x : α) => decide (q x)) encIn encBool Bs) : ComputableInSpace (fun (x : α) => decide (p x ∨ q x)) encIn encBool Bs

The disjunction of two decidable propositions, within the budget. Not registered with fun_prop; space tries it after the registered rules.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_natLe {α : Type} {encIn : α ↪ List Bool} {Bs a b : α → ℕ} (ha : ComputableInSpace a encIn encNat Bs) (hb : ComputableInSpace b encIn encNat Bs) : ComputableInSpace (fun (x : α) => decide (a x ≤ b x)) encIn encBool Bs

The comparison ≤ of numbers, within the budget. Not registered with fun_prop; space tries it after the registered rules.