fun_prop rules for bounds up to constants

fun_prop proves Turing.MultiTapeTM.ComputableInO f encIn encOut T S from rules in compositional form. The bounds of each rule's conclusion are a function of the bounds of its premises, so in a goal whose bounds T and S are metavariables, fun_prop assembles them from the parts of f. The usual pattern compares the assembled bounds with the intended ones in a single step:

refine .mono (by fun_prop) k (fun a => ?_) fun a => ?_

The rules cover constants, the identity, composition, pairs and their projections, case distinction on a computed Boolean, and Option.isSome and Option.getD. Other certificates become rules in the same compositional form, for example fun x => F (g x) from Turing.MultiTapeTM.ComputableInO.comp'.

Main results

• Turing.MultiTapeTM.ComputableInO.id', .comp': the identity and composition, in the form required by fun_prop.
• Turing.MultiTapeTM.ComputableInO.optionIsSome, .optionGetD: option tests and defaults, with the bounds of the option.

theorem Turing.MultiTapeTM.ComputableInO.id' {β : Type} {encMid : β ↪ List Bool} : ComputableInO (fun (b : β) => b) encMid encMid (fun (b : β) => (encMid b).length) fun (b : β) => (encMid b).length

Copy an encoded value, within linear time and space.

theorem Turing.MultiTapeTM.ComputableInO.comp' {α β γ : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {f : β → γ} {g : α → β} {T₁ S₁ : α → ℕ} {T₂ S₂ : β → ℕ} (hf : ComputableInO f encMid encOut T₂ S₂) (hg : ComputableInO g encIn encMid T₁ S₁) : ComputableInO (fun (a : α) => f (g a)) encIn encOut (fun (a : α) => T₁ a + T₂ (g a)) fun (a : α) => S₁ a + S₂ (g a)

Turing.MultiTapeTM.ComputableInO.comp in the form required by fun_prop.

theorem Turing.MultiTapeTM.ComputableInO.optionIsSome {α β : Type} {encIn : α ↪ List Bool} {T S : α → ℕ} {enc : β ↪ List Bool} {o : α → Option β} (h : ComputableInO o encIn (encOption enc) T S) : ComputableInO (fun (a : α) => (o a).isSome) encIn encBool T S

Whether a computed option holds a value, within the bounds of the option.

theorem Turing.MultiTapeTM.ComputableInO.optionGetD {α β : Type} {encIn : α ↪ List Bool} {T S : α → ℕ} {enc : β ↪ List Bool} {o : α → Option β} (d : β) (h : ComputableInO o encIn (encOption enc) T S) : ComputableInO (fun (a : α) => (o a).getD d) encIn enc T S

The value of a computed option, or a fixed default, within the bounds of the option.