fun_prop rules for list, option, number and test operations

These rules assemble Turing.MultiTapeTM.ComputableInO certificates with explicit time and charged-space bounds. fun_prop composes the primitives through Turing.MultiTapeTM.ComputableInO.comp'; Turing.MultiTapeTM.ComputableInO.mono then compares the assembled bounds with the client's target bounds.

The list, option and unary-number primitives are linear in their encoded arguments. The registered binary natSucc and natPred certificates instead have quadratic time and linear charged space. General equality eq' adds its explicit product-of-lengths time charge and encoded-pair space charge; clients enable it locally. Tests against a fixed value of a finite type and binary zero retain the tested computation's bounds, whereas isEmpty' adds the computed list's encoded length to both time and space. A test takes that computation as a premise, since its Boolean result does not determine the tested value's encoding.

Main results

• Turing.MultiTapeTM.ComputableInO.take', .drop': prefixes and suffixes, with a unary count.
• Turing.MultiTapeTM.ComputableInO.not', .and', .or': Boolean connectives.
• Turing.MultiTapeTM.ComputableInO.decideEq', .natIsZero': tests against a constant.
• Turing.MultiTapeTM.ComputableInO.eq': equality of computed values, enabled locally by a client.
• Turing.MultiTapeTM.ComputableInO.iteDecide: case distinction on a decidable proposition.

theorem Turing.MultiTapeTM.ComputableInO.cons' {α : Type} {enc : α ↪ List Bool} : ComputableInO (fun (p : α × List α) => p.1 :: p.2) (encPair enc (encList enc)) (encList enc) (fun (a : α × List α) => ((encPair enc (encList enc)) a).length) fun (a : α × List α) => ((encPair enc (encList enc)) a).length

theorem Turing.MultiTapeTM.ComputableInO.snoc' {α : Type} {enc : α ↪ List Bool} : ComputableInO (fun (p : List α × α) => p.1 ++ [p.2]) (encPair (encList enc) enc) (encList enc) (fun (a : List α × α) => ((encPair (encList enc) enc) a).length) fun (a : List α × α) => ((encPair (encList enc) enc) a).length

theorem Turing.MultiTapeTM.ComputableInO.append' {α : Type} {enc : α ↪ List Bool} : ComputableInO (fun (p : List α × List α) => p.1 ++ p.2) (encPair (encList enc) (encList enc)) (encList enc) (fun (a : List α × List α) => ((encPair (encList enc) (encList enc)) a).length) fun (a : List α × List α) => ((encPair (encList enc) (encList enc)) a).length

theorem Turing.MultiTapeTM.ComputableInO.tail' {α : Type} {enc : α ↪ List Bool} : ComputableInO (fun (l : List α) => l.tail) (encList enc) (encList enc) (fun (a : List α) => ((encList enc) a).length) fun (a : List α) => ((encList enc) a).length

theorem Turing.MultiTapeTM.ComputableInO.isEmpty' {α γ : Type} {enc : α ↪ List Bool} {encIn : γ ↪ List Bool} {T₁ S₁ : γ → ℕ} {l : γ → List α} (hl : ComputableInO l encIn (encList enc) T₁ S₁) : ComputableInO (fun (x : γ) => (l x).isEmpty) encIn encBool (fun (x : γ) => T₁ x + ((encList enc) (l x)).length) fun (x : γ) => S₁ x + ((encList enc) (l x)).length

Whether a computed list is empty. The list is a premise since a Boolean does not determine its encoding.

theorem Turing.MultiTapeTM.ComputableInO.headD' {α : Type} {enc : α ↪ List Bool} (d : α) : ComputableInO (fun (l : List α) => l.headD d) (encList enc) enc (fun (l : List α) => ((encList enc) l).length) fun (l : List α) => ((encList enc) l).length

theorem Turing.MultiTapeTM.ComputableInO.some' {α : Type} {enc : α ↪ List Bool} : ComputableInO (fun (a : α) => some a) enc (encOption enc) (fun (a : α) => (enc a).length) fun (a : α) => (enc a).length

theorem Turing.MultiTapeTM.ComputableInO.unarySucc' : ComputableInO (fun (n : ℕ) => n + 1) encUnary encUnary (fun (n : ℕ) => (encUnary n).length) fun (n : ℕ) => (encUnary n).length

theorem Turing.MultiTapeTM.ComputableInO.unaryPred' : ComputableInO (fun (n : ℕ) => n - 1) encUnary encUnary (fun (n : ℕ) => (encUnary n).length) fun (n : ℕ) => (encUnary n).length

theorem Turing.MultiTapeTM.ComputableInO.take' {α γ : Type} {enc : α ↪ List Bool} {encIn : γ ↪ List Bool} {T₁ S₁ T₂ S₂ : γ → ℕ} {l : γ → List α} {n : γ → ℕ} (hl : ComputableInO l encIn (encList enc) T₁ S₁) (hn : ComputableInO n encIn encUnary T₂ S₂) : ComputableInO (fun (x : γ) => List.take (n x) (l x)) encIn (encList enc) (fun (x : γ) => T₁ x + T₂ x + ((encPair (encList enc) encUnary) (l x, n x)).length) fun (x : γ) => S₁ x + S₂ x + ((encPair (encList enc) encUnary) (l x, n x)).length

The first n x elements of l x, with the count in unary.

theorem Turing.MultiTapeTM.ComputableInO.drop' {α γ : Type} {enc : α ↪ List Bool} {encIn : γ ↪ List Bool} {T₁ S₁ T₂ S₂ : γ → ℕ} {l : γ → List α} {n : γ → ℕ} (hl : ComputableInO l encIn (encList enc) T₁ S₁) (hn : ComputableInO n encIn encUnary T₂ S₂) : ComputableInO (fun (x : γ) => List.drop (n x) (l x)) encIn (encList enc) (fun (x : γ) => T₁ x + T₂ x + ((encPair (encList enc) encUnary) (l x, n x)).length) fun (x : γ) => S₁ x + S₂ x + ((encPair (encList enc) encUnary) (l x, n x)).length

All but the first n x elements of l x, with the count in unary.

theorem Turing.MultiTapeTM.ComputableInO.not' {γ : Type} {encIn : γ ↪ List Bool} {T S : γ → ℕ} {b : γ → Bool} (hb : ComputableInO b encIn encBool T S) : ComputableInO (fun (x : γ) => !b x) encIn encBool T S

The negation of a computed Boolean.

theorem Turing.MultiTapeTM.ComputableInO.and' {γ : Type} {encIn : γ ↪ List Bool} {T₁ S₁ T₂ S₂ : γ → ℕ} {a b : γ → Bool} (ha : ComputableInO a encIn encBool T₁ S₁) (hb : ComputableInO b encIn encBool T₂ S₂) : ComputableInO (fun (x : γ) => a x && b x) encIn encBool (fun (x : γ) => T₁ x + T₂ x) fun (x : γ) => S₁ x + S₂ x

The conjunction of two computed Booleans.

theorem Turing.MultiTapeTM.ComputableInO.or' {γ : Type} {encIn : γ ↪ List Bool} {T₁ S₁ T₂ S₂ : γ → ℕ} {a b : γ → Bool} (ha : ComputableInO a encIn encBool T₁ S₁) (hb : ComputableInO b encIn encBool T₂ S₂) : ComputableInO (fun (x : γ) => a x || b x) encIn encBool (fun (x : γ) => T₁ x + T₂ x) fun (x : γ) => S₁ x + S₂ x

The disjunction of two computed Booleans.

theorem Turing.MultiTapeTM.ComputableInO.eq' {α γ : Type} {enc : α ↪ List Bool} {encIn : γ ↪ List Bool} {T₁ S₁ T₂ S₂ : γ → ℕ} [DecidableEq α] {a b : γ → α} (ha : ComputableInO a encIn enc T₁ S₁) (hb : ComputableInO b encIn enc T₂ S₂) : ComputableInO (fun (x : γ) => decide (a x = b x)) encIn encBool (fun (x : γ) => T₁ x + T₂ x + ((enc (a x)).length + 1) * ((enc (a x)).length + (enc (b x)).length + 1)) fun (x : γ) => S₁ x + S₂ x + ((encPair enc enc) (a x, b x)).length

Whether two computed values agree. This is not a global fun_prop rule, since it would also apply to tests against a constant, which have cheaper rules; a client enables it locally.

theorem Turing.MultiTapeTM.ComputableInO.optionIsNone {α γ : Type} {enc : α ↪ List Bool} {encIn : γ ↪ List Bool} {T S : γ → ℕ} {o : γ → Option α} (h : ComputableInO o encIn (encOption enc) T S) : ComputableInO (fun (x : γ) => (o x).isNone) encIn encBool T S

Whether a computed option is empty, within the bounds of the option.

theorem Turing.MultiTapeTM.ComputableInO.decideEq' {α γ : Type} {enc : α ↪ List Bool} {encIn : γ ↪ List Bool} {T S : γ → ℕ} [Finite α] [DecidableEq α] (c : α) {v : γ → α} (hv : ComputableInO v encIn enc T S) : ComputableInO (fun (x : γ) => decide (v x = c)) encIn encBool T S

Whether a computed value of a finite type equals a fixed value.

theorem Turing.MultiTapeTM.ComputableInO.natIsZero' {γ : Type} {encIn : γ ↪ List Bool} {T S n : γ → ℕ} (hn : ComputableInO n encIn encNat T S) : ComputableInO (fun (x : γ) => decide (n x = 0)) encIn encBool T S

Whether a computed binary number is zero.

theorem Turing.MultiTapeTM.ComputableInO.iteDecide {γ : Type} {encIn : γ ↪ List Bool} {T₁ S₁ T₂ S₂ T₃ S₃ : γ → ℕ} {β : Type} {encOut : β ↪ List Bool} {c : γ → Prop} [DecidablePred c] {f g : γ → β} (hc : ComputableInO (fun (x : γ) => decide (c x)) encIn encBool T₁ S₁) (hf : ComputableInO f encIn encOut T₂ S₂) (hg : ComputableInO g encIn encOut T₃ S₃) : ComputableInO (fun (x : γ) => if c x then f x else g x) encIn encOut (fun (x : γ) => T₁ x + if decide (c x) = true then T₂ x else T₃ x) fun (x : γ) => S₁ x + if decide (c x) = true then S₂ x else S₃ x

Case distinction on a decidable proposition, through its computed decide.